setoid_rewrite：在用2个参数的绑定下重写

Question

我可以使用一个参数在绑定下使用重写

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.

，但是我无法经历更多涉及的情况，即wrap：nat -＆gt; （nat - ＆gt; nat - ＆gt; nat） and f f'：nat-＆gt; nat-＆gt; nat-＆gt; 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.

一个问题主要是：我应该用什么作为关系？ 我不确定我在这里做错了什么。我是否使用错误的关系，还是尝试将错误的参数转移到setoid_rewrite？

Answer 1

您可以将“点角关系的重点关系”用作二进制函数的关系：

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.