The Coq mailing list

[Z <zell08v AT orange.fr>]

Thanks foe your answer. 

According to the coq manual , sympl. did some kind of beta-iota conversion. With the fx defined as 
lambda x. (forall x, 0) 

I think if simpl. really does the beta-conversion, it should be doing like this:

( lambda x. (forall x, 0) ) 3
-->_beta (forall x, 0) [x<-3]
-->_beta 0

I do hope to know why simpl. does not give outr the result in this way?

Thanks for yorur ideas.
Zell.

On Mon, Sep 6, 2010 at 7:21 PM, Adam Chlipala <adam AT chlipala.net> wrote:

Z wrote:

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.
*********************

[simpl] never solves goals; it just simplifies them.  The proof script from your second example proves your first example, too.  In both cases, [simpl] can be left out, since [reflexivity] works modulo all legal simplifications that [simpl] might perform (and others that [simpl] will never perform).

[simpl] only unfolds definitions when doing so causes some [match] to simplify.  I hope it's not hard to see the consequences of this heuristic for the two examples, and why it leads to the [simpl] behavior you see.