广义重写构造函数下的等效术语？

如何解决广义重写构造函数下的等效术语？

我有一个归纳类型 Env，它是一个带有多个 cons 构造函数的 snoclist

Inductive Env : Set :=
 | Env_Empty : Env
 | Env_ConsA (env : Env) (a : A)
 | Env_ConsB (env : Env) (b : B)
 ...

A 和 B 类型无关紧要，所以我没有给出它们。我在这些环境中定义了一个等价关系 EqEnv，并使用 generalized rewriting 的文档将其声明为自反、对称和传递（等价）关系：

Inductive EnvEq : Env -> Env -> Prop := ...
Notation "A =~ B" := (EnvEq A B) (at level 70) : type_scope.

Add Relation Env EnvEq
  reflexivity  proved by eq_env_refl
  symmetry     proved by eq_env_sym
  transitivity proved by eq_env_trans
    as eq_env_rel.

注意符号 =~。现在，这允许在给定 x =~ y 的情况下将一些 x 重写为 y，但前提是它们没有出现在构造函数/函数应用程序/（binder？）下。我自己想出了环境串联 +++ 的情况：

Fixpoint env_concat (env1 : Env) (env2 : Env) : Env := ...
Notation "A +++ B" := (env_concat A B) (at level 60).

Theorem env_concat_compat :
    forall x x' : Env,EnvEq x x' ->
    forall y y' : Env,EnvEq y y' ->
           EnvEq (x +++ y) (x' +++ y').

Add Morphism env_concat
  with signature EnvEq ==> EnvEq ==> EnvEq as eq_env_conc.
Proof.
  exact env_concat_compat.
Qed.

（必须说我不完全理解签名中的 ==>。我知道它结合了 ++> 和 --> 但我对它们的作用感到困惑).

现在，我被困在不返回 Env 而是在 Env 上参数化的操作，即构造函数。文档中有一节“在活页夹下重写”，在这种情况下，构造函数是活页夹吗？当我听到 binder 时，我会想到 lambda 抽象，但我认为在这里它们是指构造函数，或者至少构造函数是一种类型的 binder。

Inductive WfEnv : Env -> Prop := ...

我希望，根据一些假设 H : x =~ y，能够通过调用 WfEnv x 或（如果需要）WfEnv y 将 rewrite H 重写为 rewrite_setoid H。我可以给出一个引理 x =~ y -> WfEnv x <-> WfEnv y，但我正在寻找重写支持。

对于下一步，我希望重写不仅通过 Env 参数化而且还通过其他类型参数化的构造函数。这些类型可以通过正常（莱布尼茨）相等来要求相等。

Inductive Foo : Env -> A -> Prop := ...

这里我希望，给定一些 hypothesis H1 : x =~ y 和 H2 : a = b，将 Foo x a 重写为 Foo y b。同样，我可以写一个引理 x =~y -> a = b -> Foo x a <-> Foo y b，但我正在寻找重写支持。

解决方法

您可以将 WfEnv 声明为关系 EnvEq 的态射，如下所示：

Add Parametric Morphism : WfEnv
    with signature EnvEq ==> iff as yourmorphism1.
Proof.
  (* apply here your lemma [x =~ y -> WfEnv x <-> WfEnv y] *)
Qed.

此声明允许重写 Env 下的等效 WfEnv。带有额外参数的同上：

Add Parametric Morphism : Foo
    with signature EnvEq ==> (@eq A) ==> iff as yourmorphism2.
Proof.
  (* x =~y -> a = b -> Foo x a <-> Foo y b *)
Qed.