I have an inductive type Env that is a snoclist with multiple cons constructors
Inductive Env : Set :=
| Env_Empty : Env
| Env_ConsA (env : Env) (a : A)
| Env_ConsB (env : Env) (b : B)
...
The types A and B do not matter, so I have not given them. I have defined an equivalence relation EqEnv on these environments, and have used the documentation for generalized rewriting to declare it as a reflexive, symmetric, and transitive (equivalence) relation:
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.
Note the notation =~. Now, this allows for rewriting some x into y given that x =~ y, but only when they do not appear under a constructor/function application/(binder?). I figured out the case for environment concatenation +++ on my own:
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.
(It must be said I don't fully understand the ==> in the signature. I know it combines ++> and --> but I'm confused about what these do as well).
Now, where I am stuck is on operations that do not return an Env, but are parametarized on Env, i.e. constructors. The docs have a section "Rewriting under binders", is a constructor a binder in this case? When I hear binder I think lambda abstraction, but I think here they mean constructors, or at least that constructors are a type of binder.
Inductive WfEnv : Env -> Prop := ...
I want, with some hypothesis H : x =~ y, to be able to rewrite WfEnv x to WfEnv y by calling rewrite H or if needed rewrite_setoid H. I could give a lemma x =~ y -> WfEnv x <-> WfEnv y but I'm looking for rewriting support.
For the next step, I'm looking to rewrite constructors that are parameterized over not just Env, but also other types. These types can just be required to be equal by normal (Leibniz) equality.
Inductive Foo : Env -> A -> Prop := ...
Here I'm looking to, given some hypothesis H1 : x =~ y and H2 : a = b, rewrite Foo x a to Foo y b. Again, I can write a lemma x =~y -> a = b -> Foo x a <-> Foo y b, but I am looking for rewriting support.
You could declare WfEnv to be a morphism for the relation EnvEq as follows:
Add Parametric Morphism : WfEnv
with signature EnvEq ==> iff as yourmorphism1.
Proof.
(* apply here your lemma [x =~ y -> WfEnv x <-> WfEnv y] *)
Qed.
This declaration allows to rewrite equivalent Envs under WfEnv. Idem with extra parameters:
Add Parametric Morphism : Foo
with signature EnvEq ==> (@eq A) ==> iff as yourmorphism2.
Proof.
(* x =~y -> a = b -> Foo x a <-> Foo y b *)
Qed.