Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How does the simpl. tactics behave?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How does the simpl. tactics behave?


chronological Thread 
  • From: Z <zell08v AT orange.fr>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] How does the simpl. tactics behave?
  • Date: Mon, 6 Sep 2010 19:15:55 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=bwbpgxNwhZb0YPL+isaaSmdsNBdQZaAaZQu/CK6uOmMlH/nDcq0WQe1sF9Fc+OVxOD WPKog+3cPqabQAX/M5y7qnIflGNue5XW66dW1RLxeZzd3oXSSeHQyfi2HiSReN113rxY uUF6xeGejwUPYB7EeiAzpwus1QFvaXI0SdEOU=
Hello,

I find it strange this follwoing pretty simple proof does not work. Apparently, simpl. does not do the work. Someone would like to give me more ideas about this failure??
******************
Definition fx (x:nat):nat :=  0 .
Example test000: fx 3 = 0.
Proof. intros.    simpl. Qed.
 ******************

By contrary, this following proof goes well,
**************
Inductive day:Type := |today : day |other: day.
Definition otherday (d: day): day := match d with |today => other |other=> today end.
Example test006: otherday today = other.
Proof. simpl. reflexivity. Qed.
*********************
Sorry that I can not well understand the manual of Coq, which mentions this problem in its explanation for the simpl. tactic

Thanks for your ideas.
Zell

Archive powered by MhonArc 2.6.16.

Top of Page