The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

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.