Skip to Content.
Sympa Menu

coq-club - [Coq-Club]Re: [Coq-Club]Probl�me de d�monstrat ion pas induction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Re: [Coq-Club]Probl�me de d�monstrat ion pas induction


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page