The Coq mailing list

[Erik Martin-Dorel <e.mdorel AT gmail.com>]

Hi,

Just to give a few pointers that give further details on Laurent's suggestions:

• the name of the mathcomp library supported indexed sums is called bigop:
  https://math-comp.github.io/htmldoc/mathcomp.ssreflect.bigop.html
  
• the under tactic requires a Coq version ≥ 8.10, and is documented in:

• Coq's refman: https://coq.github.io/doc/master/refman/proof-engine/ssreflect-proof-language.html?highlight=under#rewriting-under-binders
• this presentation given at the Coq Workshop 2019:

• https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi.pdf
• https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi-slides.pdf
• https://www.irit.fr/~Erik.Martin-Dorel/exposes/coq10_demo_under.v

Best regards,

Erik MD

Le mer. 8 juil. 2020 à 21:11, Laurent Thery <Laurent.Thery AT inria.fr> a écrit :

Hi,

if you are using intensively indexed sums I would recommend to use the
mathcomp library. It has lots of support for indexed sums.

You can also only use the ssreflect tactic language extension where
there is a under tactic that does exactly what you want:

Require Import List PeanoNat.
Require Import ssreflect.

Goal forall l, map (fun x => 2 + x) l = nil.
intros l.
under map_ext do rewrite Nat.add_comm.


Otherwise you can mimic it using erewrite.

For example:

Require Import List PeanoNat.

Ltac map_tac r :=
  erewrite map_ext; [idtac |
    let x := fresh "x" in
    intros x; rewrite r; apply refl_equal].

Goal forall l, map (fun x => 2 + x) l = nil.
intros l.
map_tac Nat.add_comm.

Hope this helps!

--
Laurent

--

Érik Martin-Dorel

http://erik.martin-dorel.org/