The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

On Sun, 23 Apr 2006 12:54:22 +0200 "Damien Ledoux" 
<dam.ledoux AT gmail.com>
 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

Ceci n'est pas un bug, c'est le comportement normal de l'induction. Si
vous voulez "garder" l'information du cas dans lequel vous vous
trouvez, il faut créer une nouvelle variable égale à (N2nat n), sur
laquelle vous ferez l'élimination:

Lemma test :
    forall (n : N) (r:nat), succ_fix (N2nat n) = r -> succ n = r.
    intro n.
    set (X:=N2nat n). (* création de la variable X *)
    assert (hyp: N2nat n = X). (* création de l'égalité *)
    trivial.  (* preuve de l'égalité*)
    generalize hyp. clear hyp.  (* on met l'égalité dans le contexte *)
    elim X;clear X. (* on fait la récurrence sur la variable *)


Ceci passe avec un coq plus récent que la V8.0, il se peut qu'il ne
passe pas directement.

Pierre Courtieu