setoid_rewrite: rewrite under bindings with 2 parameters

Question

I'm able to use rewrite under bindings with one parameter

Require Import Setoid.
Require Import Relation_Definitions.
Require Import FunctionalExtensionality.

Parameters f f' : nat -> nat.
Parameter wrap : nat -> (nat -> nat) -> nat.
Axiom ff'_eq : forall x, f x = f' x.

Add Parametric Morphism :
  wrap
    with signature (Logic.eq ==> pointwise_relation nat Logic.eq ==> Logic.eq) 
  as wrap_mor.
Proof.
  cbv. intros x f f' H.
  apply functional_extensionality in H.
  rewrite H.
  reflexivity.
Qed.

Lemma test_lemma y :
  wrap y (fun x => f x) = wrap y (fun x => f' x).
  setoid_rewrite ff'_eq.
  reflexivity.
Qed.

But I'm not able to go through a bit more involved case, namely when wrap : nat -> (nat -> nat -> nat) and f f' : nat -> nat -> nat -> nat.

Require Import Setoid.
Require Import Relation_Definitions.
Require Import FunctionalExtensionality.

Parameter f f' : nat -> nat -> nat -> nat.
Parameter wrap : nat -> (nat -> nat -> nat) -> nat.
(* Axiom ff'_eq : forall x y z, f x y z = f' x y z. *)
Axiom ff''_eq : forall z, (forall x y, f x y z = f' x y z).

Definition pointwise_relation2 :
    forall (A1 A2 : Type) {B : Type}, relation B -> relation (A1 -> A2 -> B) := 
    let U := Type in
    fun (A1 A2 B : U) (R : relation B) (f g : A1 -> A2 -> B) =>
        forall (a1 : A1) (a2 : A2), R (f a1 a2) (g a1 a2).

Axiom test1 : forall (x : nat) (f g : nat -> nat -> nat),
    pointwise_relation2 nat nat Logic.eq f g -> wrap x f = wrap x g.

Add Parametric Morphism :
    wrap with signature 
    (Logic.eq ==> pointwise_relation2 nat nat Logic.eq ==> Logic.eq) 
    as wrap_mor.
Proof. exact test1. Qed.

Lemma test_lemma2 y z:
    wrap y (fun x1 x2 => f x1 x2 z) = wrap y (fun x1 x2 => f' x1 x2 z).
    specialize (ff''_eq z) as feq.
    Fail setoid_rewrite feq.

A question mainly is: what should I use as a relation? I'm not sure what namely i'm doing wrong here. Do I use wrong relation or do I try to pass wrong argument to setoid_rewrite?

Answer 1

You can use the "pointwise relation of a pointwise relation" as a relation on binary functions:

Require Import Setoid Morphisms.

Parameter f f' : nat -> nat -> nat -> nat.
Parameter wrap : nat -> (nat -> nat -> nat) -> nat.
(* Axiom ff'_eq : forall x y z, f x y z = f' x y z. *)
Axiom ff''_eq : forall z, (forall x y, f x y z = f' x y z).

(* The "Add Parametric Morphism" command expands to this instance, which is simpler to write... *)
Axiom test1 : Proper (eq ==> pointwise_relation nat (pointwise_relation nat eq) ==> eq) wrap.
Existing Instance test1.

Lemma test_lemma2 y z:
    wrap y (fun x1 x2 => f x1 x2 z) = wrap y (fun x1 x2 => f' x1 x2 z).
Proof.
    specialize (ff''_eq z) as feq.
    setoid_rewrite feq.