The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

A couple of months ago I learnt about the very useful `under ext_lemma => i` tactic. Is there a way I can choose which of the parts I want to work under?

For example, my goal is something like:

 t := fun j : nat => infRobustness ψ τ (i - j) : nat -> Val
  s := fun j : nat => infRobustness ϕ τ (i - j) : nat -> Val
  ============================
  join_b 0 K (fun j : nat => t j ⊓ meet_i 0 j s) =
  (join_b 0 i (fun j : nat => infRobustness ψ τ (i - j) ⊓ meet_i 0 j s) ⊓ join_b 0 K t)

And I have a lemma

join_b_ext
     : forall (lo hi : nat) (f g : nat -> Val),
       (forall a : nat, f a = g a) -> join_b lo hi f = join_b lo hi g

If I say `under join_b_ext => j.`, it picks the first join_b in the Goal. Trying `under join_b_ext => j at 2.` does not help

On Thu, Jul 9, 2020 at 12:41 AM Kyle Stemen <bluelightning32 AT gmail.com> wrote:

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