coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] smarter fold tactic

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] smarter fold tactic
Date: Mon, 3 Aug 2020 10:14:15 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f169.google.com
Ironport-phdr: 9a23:S4TNLB9129AKrf9uRHKM819IXTAuvvDOBiVQ1KB20+scTK2v8tzYMVDF4r011RmVBNudtK4P0rKH+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhJiTanY75/Ixq6oRjNusQSnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahcN+jK1ZoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5VopXmqFsOrBu+HgmsC/3syjRVmnL227c10+I8Hgrb2wEvBckBsHTVrNXuNKcdT+O1wLPSwjXFdfxW3yry5JLJchAgvfGMUql9ccXUyUY1FgPFik+cppDiPzOQz+kAtXWQ4OV8W+y1kWEntx1xrSa1xscqkoTEgoIYxkza+Clnzog4K922RU9lbdK4DZdetyGUOYtoTs4sX2xlpCg3xqAbtJKlfiUH1Igqyh/QZfGIc4WF/xPuWeCMKjl2g3Jlfaiwhxe08UW41uL8UdO00FBUoSpBltnArG4C2AHO6sWBV/Bz/V+h1C6R2wzP7uxIO0M5mKrBJ5I8w7M9l4AfvVnCEyLynkj9kbWYeV8++uey7uTqerXmqYGYN49zkgz+N74hms27AeghMwgOW3WX9f2y1LH+/ED0RK9GjvIxkqnev5DaIdoUqrSlDA9S14Yv8xe/DzG439QEhXQLMk5JdRadg4XqO1zCOu30APa+jli2jTtmxvTLMqXkAprXL3jDlLnhfax6605Z0Ac818tQ55JVCrEaIPL8REzxuMbCAR8/KQO0xfvoBM981oMfRWKPDbSUMKzXsVCS5+IvJ/OAa5MSuDb4M/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1beGxWKwGoBcLjRNDUnJGnP1fa2FXe0NYWScOJkyvCYDUO2IQY8gzhGjt0fTzbNhIqKA8ycYtInj2dsz7uvakx109D1oAOyS1miMSyd/mWZeFGx+57x2vUEokgTL6qN/mfENTYUPtcMMaR8zMNvn98I/E8r7A1uTcdKASVLgSdKjU2loH4ABhuQWakM4IO2MyxXK3i6kGbgQzuXZC5k986aa1H/0dZ8kliT2kZI5hlxjefNhcG2rgqklqVrWDo/N1kSdzuOkLPpNmiHK82iHwCyFu0QKCAM=

Thanks. That is better, but quite as potent as setoid_rewrite with a folding lemma:

Require Import ZArith.
Require Import ssreflect.

Definition twice (x:Z) : Z := x+x.
Open Scope Z_scope.

Lemma twiceFold (x:Z) : x+x = twice x.
Proof using.
reflexivity.
Qed.

Lemma xx : forall (x:Z), x + x =0.
Proof using.
Fail progress rewrite -/(twice _).
setoid_rewrite twiceFold.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Jul 31, 2020 at 4:34 PM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Hi,

The fold version of ssreflect seems to allow _ so rewrite -/(twice _) works.

================

Require Import ZArith.
Require Import ssreflect.

Definition twice (x:Z) : Z := x+x.
Open Scope Z_scope.

Lemma twiceFold (x:Z) : x+x = twice x.
Proof using.
reflexivity.
Qed.

Lemma xx (x:Z) : twice x = 0.
Proof using.
unfold twice.
rewrite -/(twice _).
===============================

[Coq-Club] smarter fold tactic, Abhishek Anand, 08/01/2020
- Re: [Coq-Club] smarter fold tactic, Laurent Thery, 08/01/2020
  - Re: [Coq-Club] smarter fold tactic, Abhishek Anand, 08/03/2020
    - Re: [Coq-Club] smarter fold tactic, jonikelee AT gmail.com, 08/03/2020
    - Re: [Coq-Club] smarter fold tactic, Laurent Thery, 08/03/2020