coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] difference between simpl and unfold

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] difference between simpl and unfold
Date: Thu, 3 Sep 2015 16:19:39 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f181.google.com
Ironport-phdr: 9a23:EVK/gBCYzb5vxOokrDZnUyQJP3N1i/DPJgcQr6AfoPdwSP78oMbcNUDSrc9gkEXOFd2CrakU16yO7+u/ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkbjusMKLKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgyWrlAYT29exhFPGk3O6Azwdpb3qCrz8ORnjnq0J8rzGIg1VC644u9ATwLylCYKKnZt6GDakNZ9yqlcvQi9phFi64HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==

2015-09-03 14:15 GMT+02:00 shengyu shen
<shengyushen AT icloud.com>:

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

simpl also perform delta reduction when its heuristic says to do so.

unfold perform a constant unfolding and then performs also some
simplification heuristic (similar to simpl).

If you are looking for real reduction mechanism you should use compute
(or vm_compute), lazy and cbv. These are "reduction" tactics.

You can even call reduction machinery via commands:

Eval vm_compute in (plus 0 (S 0)).
Eval cbv delta beta iota zeta in (plus O (S O)).
Eval lazy delta beta iota zeta in (plus O (S O)).
Eval lazy delta[plus] beta iota zeta in (plus O (S O)).

Best
Pierre

[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