The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

The point of simpl is to decide when to do a delta-reduction (expanding 
a constant) in order to generate a reduction.
To introduce a beta-redex is not a sufficent condition for 
delta-expansion (otherwise any function will be expanded by simpl): 
simpl expands a name when it will introduce a beta-redex and then a 
iota-redex (match on a constructor or fixpoint on a constructor).
In case just a beta-redex is involved, unfold fx will do the job.
The reason to design simpl instead of unfold is that when the constant 
introduces a fixpoint reduction, the simpl reduction attempts to do a 
fold after reduction, such that the fixpoint reduction rule is expressed 
in term of the function name and not of the primitive Fix construction.

C. Paulin

On 09/07/2010 07:04 AM, Z wrote:
> Thanks foe your answer.
>
> According to the coq manual , sympl. did some kind of beta-iota
> conversion. 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?
>
> Thanks for yorur ideas.
> Zell.
>
> On Mon, Sep 6, 2010 at 7:21 PM, Adam Chlipala 
> <adam AT chlipala.net
> <mailto:adam AT chlipala.net>>
>  wrote:
>
>
>     Z wrote:
>
>         I find it strange this follwoing pretty simple proof does not
>         work. Apparently, simpl. does not do the work. Someone would
>         like to give me more ideas about this failure??
>         ******************
>         Definition fx (x:nat):nat :=  0 .
>         Example test000: fx 3 = 0.
>         Proof. intros.    simpl. Qed.
>           ******************
>
>         By contrary, this following proof goes well,
>         **************
>         Inductive day:Type := |today : day |other: day.
>         Definition otherday (d: day): day := match d with |today =>
>         other |other=> today end.
>         Example test006: otherday today = other.
>         Proof. simpl. reflexivity. Qed.
>         *********************
>
>
>     [simpl] never solves goals; it just simplifies them.  The proof
>     script from your second example proves your first example, too.  In
>     both cases, [simpl] can be left out, since [reflexivity] works
>     modulo all legal simplifications that [simpl] might perform (and
>     others that [simpl] will never perform).
>
>     [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.
begin:vcard
fn:Christine Paulin-Mohring
n:Paulin-Mohring;Christine
email;internet:christine.paulin AT lri.fr
tel;work:+33 1 72 92 59 05
x-mozilla-html:FALSE
version:2.1
end:vcard