The Coq mailing list

[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
*)