The Coq mailing list

[Julien Narboux <Julien.Narboux AT inria.fr>]

Bonjour,

Voici une solution, a priori r ne sert à rien et ce que tu prouves ne 
parle en fait que de nat et pas de N :

Lemma test :
   forall (n : nat), succ_fix n = n + 1.
Proof.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.


Lemma test2 :
  forall (n : N) (r:nat), succ_fix (N2nat n) = r -> succ n = r.
Proof.
intros.
rewrite test in H.
assumption.
Qed.


Bonne journée.

Julien

Damien Ledoux a écrit :
> 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 ******************)
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club