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: Wed, 3 Feb 2021 18:55:54 -0800
Authentication-results: mail3-smtp-sop.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-io1-f45.google.com
Ironport-phdr: 9a23:imI8uxRQR1CJ7dryJcRMGjQ5SNpsv+yvbD5Q0YIujvd0So/mwa6ybRaN2/xhgRfzUJnB7Loc0qyK6vGmBTZLsMnJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRG7oR/eu8UIjodvLqQ8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9Drx2hqR5wzY7abo+WKfRwYL/ScMgASmZdRMtcTTBNDp++YoYJEuEPPfxYr474p1YWsRaxHgmsBOL0yj9ImHD23rAx3vgnEQ7c2gwvAs8FvXPOo9ruNKcSUPu1zKnWwjXAdf9ZwzH955LOch88u/2MXLNwcdbeyUQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyhGEptxt/rSKzxscwlIbJnIQVx0jA+Ch53Io4O8O0RkB1bNCkEZZcqT2WO5Z2TM0iQ29kpig3x6EatJO1YSQH1YoryhzDZvGbcoWG7R3uWeaMLDp5gn9uZbyxhxG38Ue6y+38UNG530pNripflNnDqHQN1xjJ5seZV/R940Gs0iuM2QDL8uxIP1w4mK7BJ5MiwrM8jIcfvEXCEyPsl0j7jKmbfVg+9Oey8eToeLDmq4ecN4BqjgH+NbwjmsmlDuQ5NggCRmmb+eOh2LH68030T7VHguc5kqnet5DaKsAbqbCjDwBJ1YYj7g6zDzag0NsGgXkKNExJdA6DgoTzOFzDIOr0Aeq+jlmtijtmyPDLMqXkAprXL3jDlLnhfax6605Z0Ac818tQ55JVCrEaIPL8REzxuMbCAR8/KQO0xfvoBM981oMfRWKPDbSUMKzXsVCS5+IvJ/OAa5MSuDb4M/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1beGxWKwGoBcLjRNDUnJGnP1fa2FXe0NYWScOJkyvCYDUO2IQY8gzhGjt0fTzbNhIqKA8ycYtInj2dsz7uvakx109D1oAOyS1miMSyd/mWZeFGx+57x2vUEokgTL6qN/mfENTYUOtcMMaR8zMNvn98I/C932XVicLNKASVLjQ9L/RD9tE5Q+xNgBZ0s7ENKn3EiajniaRoQNnrnOP6Qat6fV3nz/PcF4ki+U26wojl1gScxKZzT/2vxPsjPLDouMqH230r6wfP1FjiHI/WaHi2GJuRMAXQ==

Thanks, the under tactic will be useful in may cases. However, it is not just about the binders. setoid_rewrite can also fold/unfold definitions in order to unify. ssreflect rewrite doesn't try that hard:

Require Import ssreflect.
Require Import ZArith.
Open Scope Z_scope.

Definition twice (x:Z) : Z := x+x.
Definition twiced (x:Z) : Z := x+x.

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

Lemma xx (x:Z) : twice x = 0.
Proof.
unfold twice.
change (x+x) with (twiced x).
Fail progress rewrite -/twice.
progress setoid_rewrite twiceFold.

-- Abhishek

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

On Mon, Aug 3, 2020 at 11:08 AM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Hi,

sure, going under binders is always problematic. There is
the under tactic :

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

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 : List.map (fun x => x + x) nil = nil.
Proof.
under List.map_ext => m do rewrite -/(twice _).

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

but it may not be enough for your use case...

--
Laurent

On 8/3/20 7:14 PM, Abhishek Anand wrote:

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

Re: [Coq-Club] smarter fold tactic, Abhishek Anand, 02/04/2021