The Coq mailing list

[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.

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".

Paul

On May 28, 2011, at 9:38 AM, Guillaume Brunerie wrote:

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

I have defined a simple predecessor function "p" for bijective base-2
arithmetic on type B as:

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
 | o e => e
 | o a => i (p a)
 | i a => o a
 end.

Eval compute in p (p (i (i (o e)))).

(* The definition seems accepted and "Eval compute" works as expected *)

(* I would like to apply the definition of p and prove the following lemma. *)

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

(* Unfortunately none of the tactics I have tried work at this point and the
ref. manual does not seem to have one that does allows you to a apply a
function definition directly (or maybe it is there and I could not find it?).
What should I do next to convince Coq to use the option o n => i (p a) in the
definition of p to prove the lemma?

Thanks,

Paul
*)

You can use the tactic 'simpl', which will unfold the definition of p.
After that, the tactic 'case_eq' will allow you to prove the result for every case, while retaining the value of n (try 'case' instead to see what I mean).
And 'firstorder' will then do the job.

Guillaume