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

Question

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

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，但前提是它们没有出现在 constructor/function 应用程序/（活页夹？） 下。我自己弄清楚了环境串联 +++ 的情况：

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.

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

现在，我遇到的问题是不 return 和 Env，但在 Env 上参数化的操作，即构造函数。文档有一个部分“在活页夹下重写”，在这种情况下构造函数是活页夹吗？当我听到 binder 时，我认为是 lambda 抽象，但我认为这里它们指的是构造函数，或者至少构造函数是一种 binder。

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

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

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

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，但我正在寻找重写支持。

Answer 1

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

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

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

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

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

(genralized) rewriting of an equivalent term under constructor?

coq

rewriting