The Coq mailing list

["Jean.Duprat" <duprat AT ens-lyon.fr>]

Bonjour,

En choisissant de faire l'elimination sur (N2nat n) les valeurs de n ne 
sont pas reportees
dans l'expression succ n, d'ou l'echec de ta demonstration.
Si tu tiens a "elim (N2nat n).", je te suggere la demonstration suivante :
   unfold succ in |- *; intro n.
   elim (N2nat n); simpl in |- *; intros.
    trivial.
    rewrite <- H0; apply f_equal with (f := S).
      apply H; trivial.
Mais je te conseille de choisir plutot les variables dont le type est un 
inductif pour
faire une elimination, ici n. Ce qui donne par exemple :
   unfold succ in |- *; induction n; simpl in |- *; intros.
    trivial.
    rewrite (IHn (succ_fix (N2nat n))); auto.
Amities

   Jean Duprat


Damien Ledoux wrote:

> 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