The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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