The Coq mailing list

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

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