The Coq mailing list

["Damien Ledoux" <dam.ledoux AT gmail.com>]

Bonjour,

J'ai un petit problème avec la tactique elim.
En effet quand je veux réaliser une démonstration par induction,
elle me remplace directement le terme de mon induction dans mon lemme
alors que j'aimerais l'avoir en hypothèse.

Pour etre plus clair, j'ai fait un petit exemple montrant mon problème.

Mon problème est la démonstration du lemme test.
Je dois mal utiliser les tactiques ou bien faire une mauvaise induction.
Si je ne me trompe pas il faut réaliser une induction sur "(N2nat n)" puis
après sur "r".


Merci d'avance pour votre aide,
Damien


(************** DEBUT *****************)

Inductive N : Set :=
   | base : N
   | next : N -> N.

Implicit Types n : N.

Fixpoint N2nat n : nat :=
   match n with
   | base => O
   | next n' => S (N2nat n')
   end.


Fixpoint succ_fix (n:nat) : nat  :=
match n with
   | O => (S 0)
   | S n => S (succ_fix n)
end.

Definition succ (n:N) : nat := (N2nat n) + 1.


Lemma test :
   forall (n : N) (r:nat), succ_fix (N2nat n) = r -> succ n = r.
   intro n.
   elim (N2nat n).

   (* CB : (N2nat n) *)
   simpl.

(*************** FIN ******************)