The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

I use the setoid_rewrite tactic to do rewrites under the map function. To enable it, you have to show that map is a pointwise_relation,

Require Import Coq.Classes.Morphisms.

Require Import Coq.Setoids.Setoid.

Require Import List.

Import ListNotations.

Instance map_ext_inst {T U: Type} :

  Proper (pointwise_relation T eq ==> eq ==> eq) (@map T U).

Proof.

  intros f g Hf_g l1 l2 Hl1_l2.

  rewrite Hl1_l2.

  apply map_ext.

  assumption.

Qed.

Note that you may have to explicitly specify all of the parameters to get the setoid_rewrite to work. That's why the example below has (fun n => f n) instead of (f).

Example map_ext_rewrite_test : forall (f g: nat -> nat) l,

  (forall a, f a = g a) ->

  map (fun n => f n) l = map (fun n => g n) l.

Proof.

  intros f g l Heq.

  setoid_rewrite Heq.

  reflexivity.

Qed.

On Wed, Jul 8, 2020 at 4:57 PM Agnishom Chattopadhyay agnishom-at-cmi.ac.in |coq-club/Example Allow| <x0mk80tcezojwqt AT sneakemail.com> wrote:

Thanks for pointing out this feature of => i. I will look into the documentation and try to understand how it works.

On Wed, Jul 8, 2020 at 6:49 PM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Hi,

I am not sure I follow everything but it seems that in your particular
example you could use Nat.min_0_r.

More generally if you look at the documentation of under you can
handle binders :

https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html

For example, interactively this gives:

From mathcomp Require Import ssreflect.
Require Import List PeanoNat.

Goal forall l, (map (fun i => i + 1) l) = l.
Proof.
move=> l.
under map_ext => i.
  replace (i + 1) with (1 + i); last first.
    by rewrite Nat.add_comm.
  over.

Hope this helps

--
Laurent