coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] difference between simpl and unfold

From: shenshengyu <shengyushen AT me.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] difference between simpl and unfold
Date: Wed, 02 Sep 2015 22:10:44 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=shengyushen AT me.com; spf=Pass smtp.mailfrom=shengyushen AT me.com; spf=None smtp.helo=postmaster AT pv33p04im-asmtp001.me.com
Ironport-phdr: 9a23:1Ubd7B2MCdl/QFjtsmDT+DRfVm0co7zxezQtwd8ZsegVKfad9pjvdHbS+e9qxAeQG96Lt7Qc0aGJ7ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6OyZztnL/vs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGBCP630HUmgQnQtVS1ze7Bz8UYbsqSv3sMJ41W+ROsigHuN8Yiir86o+EEygsywALTNsqGw=

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

[Coq-Club] difference between simpl and unfold, shenshengyu, 09/02/2015
- Re: [Coq-Club] difference between simpl and unfold, Pierre Courtieu, 09/03/2015
  - Re: [Coq-Club] difference between simpl and unfold, shengyu shen, 09/03/2015
    - Re: [Coq-Club] difference between simpl and unfold, Pierre Courtieu, 09/03/2015