The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

I am still puzzled about simpl.  Let me ask my question from a few  
days ago again in more detail and see if anyone can enlighten me at  
least a little...

Here is the description of simpl from the reference manual:

> This tactic applies to any goal. The tactic simpl first applies βι- 
> reduction rule. Then it expands transparent constants and tries to  
> reduce T' according, once more, to βι rules. But when the ι rule  
> is not applicable then possible δ-reductions are not applied. For  
> instance trying to use simpl on (plus n O)=n does change nothing.

I am not sure I follow all the nuances of the three critical  
sentences, but according to my understanding at least both of the  
following "Eval..." experiments should yield the same result -- they  
should both simplify completely (and yield 7) or neither should.

> Definition plus' := plus.
>
> Eval simpl in plus' 3 4.
>
> Definition plus3 := plus 3.
>
> Eval simpl in plus3 4.

But in fact the first goes to 7 while the plus3 in the second stays  
un-expanded.  I would be most grateful for some intuition as to why  
this is.

Thanks,

   - Benjamin



Begin forwarded message:

> From: Benjamin Pierce 
> <bcpierce AT cis.upenn.edu>
> Date: September 9, 2007 10:06:07 PM EDT
> To: 
> coq-club AT pauillac.inria.fr
> Subject: A simple explanation of simpl?
>
> I am having a little trouble understanding the precise interplay  
> between beta- and delta-reduction in the various simplification  
> tactics...
>
> Could someone explain why the first Eval yields 7 but the second  
> does not?
>
> Thanks!
>
>     - Benjamin
>
>
> Definition plus' := plus.
>
> Eval simpl in plus' 3 4.
>
> Definition plus3 := plus 3.
>
> Eval simpl in plus3 4.