The Coq mailing list

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

Many thanks to Hugo and Georges -- that's exactly what I needed.

Thanks also to Jevgenijs Sallinens, who pointed me to this old  
message explaining things further:

    http://www.iist.unu.edu/~alumni/software/other/inria/www/coq/ 
mailing-lists/coqclub/0033.html

(One point that is not completely clear there is exactly what the  
'deltared' basic reduction rule does, but roughly it seems to stand  
in the same relation to delta as iotared does to iota -- i.e., it  
expands constants but only in the case of reduction of "primitive  
recursions" that can be folded up again after being reduced.)

   - Benjamin



On Sep 19, 2007, at 9:33 AM, Georges Gonthier wrote:

> (Copying to list)
>
> The behaviour of simpl is definitely not the one that is documented  
> -- indeed simpl would be far less useful if that were the case. My  
> experimental understanding of simpl is that it will only expand a  
> constant if this creates a head iota-redex whose constructor is the  
> head of one of the actual arguments of the constant. So, in your  
> example,
>   plus3 4
> doesn't expand plus3 because although this would expose a head  
> redex, i.e.,
>   (fix plus (m n : nat) {struct m} : nat := ...) (S 2) 4 the  
> constructor involved in that redex doesn't come from the argument  
> of plus3.
>   As an extreme example of this, the ssreflect prelude defines  
> Notation "'nosimpl' f" := match tt with tt => f end
>    (at level 10, f at level 8).
> This is used to switch off simplification for selected constants,  
> e.g.,
>   Definition minus_nosimpl := nosimpl minus.
> This works because the head redex in say (minus_nosimpl 5 n) is the  
> trivial case analysis on the unit type, which involves neither 5  
> nor n. The dummy "match tt" prevents Coq from "simplifying" this  
> term as it would do for (minus 5 n). Note that (minus_nosimpl 5 n)  
> is nonetheless convertible to (minus 5 n), and indeed the nosimpl  
> is mostly invisible because it vanishes when one unfolds  
> minus_nosimpl, by iota simplification.
>   I find nosimpl especially useful for nat arithmetic, where the  
> "simpl" is more annoying than useful, and for Structure projections  
> (rings, groups, equality, etc) where simplification would ruin  
> generic notation for the structure.
>
> Georges
>
> -----Original Message-----
> From: coq-club-admin AT pauillac.inria.fr [mailto:coq-club- 
> admin AT pauillac.inria.fr] On Behalf Of Benjamin Pierce
> Sent: 18 September 2007 23:28
> To: 
> coq-club AT pauillac.inria.fr
> Subject: [Coq-Club] Re: A simple explanation of simpl?
>
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club