coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] smarter fold tactic

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] smarter fold tactic
Date: Mon, 3 Aug 2020 13:52:14 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f178.google.com
Ironport-phdr: 9a23:2Yx8WRwCi1f4CBTXCy+O+j09IxM/srCxBDY+r6Qd2uweIJqq85mqBkHD//Il1AaPAdyFra0YwLOO4ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhTexe7F/IRq5oQnMqsUbhZZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8J+jKxVvg+vqR99zI7aZ4+aO+ZxcKzGcNMGR2dMRNpdWjZdDo+iaYYEEuoPPfxfr4n4v1YCoxm+BQ6qBOPuyT9HmHv20rMk3Ok6HgHG2RYvH9MKsHjOsNr1M6ISXe6ox6TPzzXDaPVW2Tb+6IfWdhAuv++DUKl/ccrU00YvFgfFgk+MpoziOjOYz+IAuHWU4OR8T+ygkXInqx1vrTi1wMchkonEi4wVx1za6Sh13po5KNm2RkNnYtOqEJVeujyVOodoQM4vR25ltSI6x7AEp5O3YTQGxYg5yhDRdfGKcoiF7wzlWe2MLzl4g3dld6i+hxa06UWv1ur8VtOy0FlUqipFlsPAuW4Q2BzO7MWMV/hz/l+51DqRywze7vtILEM0mKbBNpIsw6I8moAOvUnBHSL6gFv6ga6Kekk5/+Wk9uDqbanjq5KTNoJ4lh3yP6EzlsGwH+g1NwkDUHSU9Om/0bDu+UP5QLtPg/04jKbWqpPXKMEYq6O6BwJY0IAu4AulATi8ytQXh3wHIUpFeB2Zi4jpPEnDIPXiAve+h1SgiS5rx+zbMrH4DJXBM3rOnbT7cbZy7E5czwUzzdRB6J5OFr4BJ/fzVlfwtNzeEBA5LxS5z/j7BNh5zI8TWmKCDrWEPK7TrVOE/P8jLuuPaYMNvTbyMfkl5/rgjX8jnl8deLGk3ZkQaHC+H/RmIFuWYX7yjdgfCmoKsQ8+Q/briF2GSzJce3GyX6ck6jEhFI2mFZvDRpyqgLGZwCi7GYRWanlaBVCIDHfnbJ6JW+wMaSKXOs9uiCYIVbmnS4871BGhrhX2y7R9LrmcxipNnJjj1cN16u6bvBc78zA8W82X02CWT2x32GoOTjk6mqF+vUNVxVKK0Kw+iPtdQ499/fRMB004MpjdzOF+Bt3aVQfIf9PPQ1GjCJ3yAzY3T9E8x9IDS0l4EtSmyBvE2nz5UPcui7WXCclsoern1H/rKpMlkiuU5Owal1AjB/B3Gyimi6p4rVaBAofIlwCAi//ve/1DjGjC82CMyWfIt0ZdAlYpDff1GEsHb06TluzXo1vYRub3W7siOwpFj8WFL/kSM4y7vRB9XP7mfe/mTSe0kma0CwyPw+rVPoXvcmQZmi7aDRpdng==

Does this work as required?:

Require Import ZArith.

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

Ltac uscore term := (*pads term maximally with underscores*)
match goal with
| _ => uscore open_constr:(term _)
| _ => fun tac => tac term
end.

Ltac myfold' head octerm :=
let pat := eval unfold head in octerm in
match goal with
|- context[?G] => unify G pat; change pat with octerm
end.

Ltac myfold head := uscore head ltac:(myfold' head).

Lemma xx (x:Z) : twice x = 0.
Proof.
unfold twice.
myfold twice.

On Mon, 3 Aug 2020 10:14:15 -0700
Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

> 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