The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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.