coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Julien Narboux <Julien.Narboux AT inria.fr>
- To: Damien Ledoux <dam.ledoux AT gmail.com>, Coq Club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club]Re: [Coq-Club]Problème de démonstrat ion pas induction
- Date: Sun, 23 Apr 2006 13:19:38 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club]Problème de démonstration pas induct ion, Damien Ledoux
- [Coq-Club]Re: [Coq-Club]Problème de démonstrat ion pas induction, Julien Narboux
- [Coq-Club]Re: [Coq-Club]Problème de démonstrat ion pas induction, Jean.Duprat
- Re: [Coq-Club]Problème de d émonstration pas induction, Pierre Courtieu
Archive powered by MhonArc 2.6.16.