The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

Thanks - that explains the magic indeed! After adding a matching successor function and showing that sx <> e, I have:

Inductive B : Set :=

|  e : B

|  o : B -> B

|  i : B -> B.

Delimit Scope b_scope with B.

Bind Scope b_scope with B.

Arguments Scope o [b_scope].

Arguments Scope i [b_scope].

Fixpoint p (x : B) : B := 

  match x with

  | e => e (* this should rather be undefined or an exception *)

  | o e => e

  | o a => i (p a) 

  | i a => o a

  end.

Fixpoint s (x : B) : B :=

  match x with

  | e => o e

  | o a => i a

  | i a => o (s a)

  end.

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

Proof.

  intros n H.

  simpl.

  case_eq n; firstorder.

Qed.

Lemma s_discr : forall x:B, x <> s x.

Proof.

  destruct x; discriminate.

Qed.

Lemma pos_ips : forall x:B, p (o (s x)) = i (p (s x)).

Proof.

intros.

case_eq x;firstorder.

Qed.

Lemma psi_os : forall n:B, p (s (i n)) = p (o (s n)).

Proof.

intro n; auto.

Qed.

Eval compute in p (p (s (s e))).

Lemma sp_inv : forall n:B, p (s n) = n.

Proof.

intros.

case_eq n;firstorder.

Show.

(* which gives:

  n : B

  b : B

  H : n = i b

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

   p (s (i b)) = i b

I would like Coq to reason along the following equations:

    p (s (i b)) = p (o (s b)) = i (p (s b)) = i b

where I want to use, as an inductive hypothesis, that p (s b) = b holds.

I tried "apply psi_os" (that I just proved) but it seems to want both sides

of an equation - is there any way to make it just rewrite p (s (i b)) as

p (o (s b)) according to Lemma psi_os?

> apply psi_os.

>       ^^^^^^

Error: Impossible to unify "p (s (i ?55)) = p (o (s ?55))" with

 "p (s (i b)) = i b".

Paul

*)

On May 28, 2011, at 10:52 AM, Guillaume Brunerie wrote:

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