coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] smarter fold tactic

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] smarter fold tactic
Date: Sat, 1 Aug 2020 01:33:44 +0200

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