The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

2011/5/28 Paul Tarau <paul.tarau AT gmail.com>

Thanks a lot, the following did it!

Lemma po_ip : forall n:B, n<>e -> p (o n) = i (p n).

Proof.

intros n H.

simpl. 

Show.

case_eq n.

firstorder.

firstorder.

intros.

firstorder.

Qed.

You can do even shorter with :

Lemma po_ip : forall n:B, n<>e -> p (o n) = i (p n).
Proof.
  intros n H.
  simpl.
  case_eq n; firstorder.
Qed.

The semicolon asks Coq to apply the tactic 'firstorder' to every new subgoal.

I am still puzzled why after simpl I get:

  n : B

  H : n <> e

  ============================

   match n with

   | e => e

   | o _ => i (p n)

   | i _ => i (p n)

   end = i (p n)

where the underscores indicate that Coq is ignoring or forgetting the actual argument - this does not seem equivalent with the definition of p. Impressed that magic works:-), but is there anything that could make the proof obtained by the sequence of tactics somewhat human readable - for instance I would be curious to see what firstorder did "under the hood".

'firstorder' hasn’t done any magic, the magic comes from 'simpl'.

When Coq is simplifiying the _expression_ 'p (o n)',
If n = e, then p (o e) = e by definition.
If n = o a, then p (o n) = p (o (o a)) = i (p (o a)) = i (p n)
If n = i a, then p (o n) = p (o (i a)) = i (p (i a)) = i (p n)
In the two latter cases, the result does not depend on a (the underscore), it depends only on n.

And what is left to 'firstorder' to prove is that :
If n = e, something, but n <> e so this is true
If n is of the form (o a) or (i a), then i (p n) = i (p n) which is true.

Guillaume