Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: A simple explanation of simpl?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: A simple explanation of simpl?


chronological Thread 
  • From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
  • To: Georges Gonthier <gonthier AT microsoft.com>
  • Cc: Hugo Herbelin <hugo.herbelin AT inria.fr>, "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Re: A simple explanation of simpl?
  • Date: Wed, 19 Sep 2007 09:44:00 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page