The Coq mailing list

[shengyu shen <shengyushen AT icloud.com>]

according to doc of coq, there are 4 types of reduction:

beta, delta, iota or zeta. 

It seems that simple work on beta iota and zeta, while unfold work on delta only?

Shen

On Sep 3, 2015, at 6:17 PM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

You can see the behavior of simpl, cbn and unfold in the documentation.

In short: simpl is reduction heuristic. It only unfolds if some
further reduction (iota-reduction mainly I think) is triggered by the
unfolding, otherwise it does not unfold (to keep you goal small).

Remark: please use cbn instead of simpl if you are using coq-8.5. Its
behavior is most of the time better.

Hope this helps
P.



2015-09-02 16:10 GMT+02:00 shenshengyu <shengyushen AT me.com>:

Dear all:

I am a new leaner of Coq, I am reading the usage of tactics.

I am trying to prove the following theorem:

===================================
Theorem double_neg_i: forall P:Prop , P->~~P.
===================================

if I use “unfold not.” , I can transform the goal to


===================================
forall P : Prop, P -> (P -> False) -> False
===================================


But if I use “simpl not”, then nothing happen.

So my question is what is the difference of simpl and unfold?


Shen