The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Z wrote:
> 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?
>
> On Mon, Sep 6, 2010 at 7:21 PM, Adam Chlipala <adam AT chlipala.net 
> <mailto:adam AT chlipala.net>> wrote:
>
>
>     [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.

To give an alternate answer to this question: Like I wrote above, 
[simpl] only unfolds definitions when doing so simplifies [match] 
expressions.  Unfolding [fx] in [fx 3] does not produce a term 
containing a [match] expression, so it is not possible to simplify any 
[match] expression, so no unfolding is done by [simpl].  This is a 
completely mechanical procedure with no subtleties.  Perhaps you are 
assuming that [simpl] must be "smarter" than it is; I expect your 
confusion will disappear if you can get over that assumption. ;)

Also, your reduction sequence above is incorrect.  The final result 
should still contain a [forall], and there should only be one beta step.