The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

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

The historical rationale behind the implementation of simpl is the
following: a constant hidding a fixpoint is unfolded only if its name
can be directly reused in the recursive calls. In your case, the name
plus' can be reused when simplifying any expression involving plus'
such as

  Eval simpl in fun x => plus' (S x) x.

which returns "fun x : nat => S (plus' x x)", but plus3 cannot be
reused, since the recursive call in plus cannot obviously be
formulated as an expression of plus3.

This indeed leads in your case to a surprising result, since even
though the final result requires no further call to plus, plus3 is not
unfolded.

The simpl tactic is probably not the ultimate form of what ones expect
of an "intuitive" simplification mechanism, but I know nobody
currently working on making it better.

Hope it helps,

Hugo