Coral.Transp: name transpositions
Require Export TranspCore.
Require Import Infrastructure.
Require Import Env.
Require Import SubstEnv.
Require Import Rel.
Transpositions on terms
Definitions and basic properties
Fixpoint transp_term x y (t: term) : term :=
match t with
| Var z ⇒ Var (transp_atom x y z)
| BVar n ⇒ BVar n
| Let t1 t2 ⇒ Let (transp_term x y t1) (transp_term x y t2)
| Lam t ⇒ Lam (transp_term x y t)
| App t1 t2 ⇒ App (transp_term x y t1) (transp_term x y t2)
| Unit ⇒ Unit
| Pair t1 t2 ⇒ Pair (transp_term x y t1) (transp_term x y t2)
| Fst t ⇒ Fst (transp_term x y t)
| Snd t ⇒ Snd (transp_term x y t)
| InjL t ⇒ InjL (transp_term x y t)
| InjR t ⇒ InjR (transp_term x y t)
| Match t0 t1 t2 ⇒ Match (transp_term x y t0) (transp_term x y t1) (transp_term x y t2)
end.
Lemma transp_term_size x y t:
size (transp_term y x t) = size t.
Proof.
induction t; simpl; auto.
Qed.
match t with
| Var z ⇒ Var (transp_atom x y z)
| BVar n ⇒ BVar n
| Let t1 t2 ⇒ Let (transp_term x y t1) (transp_term x y t2)
| Lam t ⇒ Lam (transp_term x y t)
| App t1 t2 ⇒ App (transp_term x y t1) (transp_term x y t2)
| Unit ⇒ Unit
| Pair t1 t2 ⇒ Pair (transp_term x y t1) (transp_term x y t2)
| Fst t ⇒ Fst (transp_term x y t)
| Snd t ⇒ Snd (transp_term x y t)
| InjL t ⇒ InjL (transp_term x y t)
| InjR t ⇒ InjR (transp_term x y t)
| Match t0 t1 t2 ⇒ Match (transp_term x y t0) (transp_term x y t1) (transp_term x y t2)
end.
Lemma transp_term_size x y t:
size (transp_term y x t) = size t.
Proof.
induction t; simpl; auto.
Qed.
This is the property "Symmetry" on page 10 of the ICFP'20 paper.
Lemma transp_term_swap x y t:
transp_term x y t = transp_term y x t.
Proof.
induction t; simpl; auto;
try rewrite transp_atom_swap; congruence.
Qed.
Lemma transp_term_fresh_eq x y t:
x `notin` fv t →
y `notin` fv t →
transp_term x y t = t.
Proof.
intros Hx Hy.
induction t; simpl in *; auto; f_equal;
try rewrite transp_atom_other; auto; try rewrite IHe; auto.
Qed.
transp_term x y t = transp_term y x t.
Proof.
induction t; simpl; auto;
try rewrite transp_atom_swap; congruence.
Qed.
Lemma transp_term_fresh_eq x y t:
x `notin` fv t →
y `notin` fv t →
transp_term x y t = t.
Proof.
intros Hx Hy.
induction t; simpl in *; auto; f_equal;
try rewrite transp_atom_other; auto; try rewrite IHe; auto.
Qed.
This is the property "Reflexivity" on page 10 of the ICFP'20 paper.
Lemma transp_term_refl x t :
transp_term x x t = t.
Proof.
induction t; simpl; auto; f_equal;
try rewrite transp_atom_refl; auto.
Qed.
transp_term x x t = t.
Proof.
induction t; simpl; auto; f_equal;
try rewrite transp_atom_refl; auto.
Qed.
This is the property "Transitivity" on page 10 of the ICFP'20 paper.
Lemma transp_term_trans x1 x2 x3 t:
x1 `notin` fv t →
x2 `notin` fv t →
transp_term x1 x2 (transp_term x2 x3 t) = transp_term x1 x3 t.
Proof.
intros H1 H2.
induction t; simpl in *; auto; f_equal;
try rewrite transp_atom_trans; auto;
try rewrite IHe; auto.
Qed.
x1 `notin` fv t →
x2 `notin` fv t →
transp_term x1 x2 (transp_term x2 x3 t) = transp_term x1 x3 t.
Proof.
intros H1 H2.
induction t; simpl in *; auto; f_equal;
try rewrite transp_atom_trans; auto;
try rewrite IHe; auto.
Qed.
This is the property "Involution" on page 10 of the ICFP'20 paper.
Lemma transp_term_involution x y t:
transp_term x y (transp_term x y t) = t.
Proof.
induction t; simpl; auto; f_equal;
try rewrite transp_atom_involution; auto.
Qed.
transp_term x y (transp_term x y t) = t.
Proof.
induction t; simpl; auto; f_equal;
try rewrite transp_atom_involution; auto.
Qed.
This is the property "Composition" on page 10 of the ICFP'20 paper.
Lemma transp_term_compose x1 x2 y1 y2 t:
transp_term x1 x2 (transp_term y1 y2 t) =
transp_term
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_term x1 x2 t).
Proof.
induction t; simpl; auto; f_equal;
try rewrite transp_atom_compose; auto.
Qed.
Lemma transp_term_freshL_is_subst x y t:
x `notin` fv t →
transp_term x y t = subst (Var x) y t.
Proof.
intro Hx. induction t; simpl in *; f_equal; auto.
- destruct (x0 == y); subst.
+ rewrite transp_atom_thisR. reflexivity.
+ rewrite transp_atom_other; auto.
Qed.
Lemma transp_term_freshR_is_subst x y t:
y `notin` fv t →
transp_term x y t = subst (Var y) x t.
Proof.
intro Hx. rewrite transp_term_swap.
apply transp_term_freshL_is_subst; auto.
Qed.
transp_term x1 x2 (transp_term y1 y2 t) =
transp_term
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_term x1 x2 t).
Proof.
induction t; simpl; auto; f_equal;
try rewrite transp_atom_compose; auto.
Qed.
Lemma transp_term_freshL_is_subst x y t:
x `notin` fv t →
transp_term x y t = subst (Var x) y t.
Proof.
intro Hx. induction t; simpl in *; f_equal; auto.
- destruct (x0 == y); subst.
+ rewrite transp_atom_thisR. reflexivity.
+ rewrite transp_atom_other; auto.
Qed.
Lemma transp_term_freshR_is_subst x y t:
y `notin` fv t →
transp_term x y t = subst (Var y) x t.
Proof.
intro Hx. rewrite transp_term_swap.
apply transp_term_freshL_is_subst; auto.
Qed.
Lemma fv_equivariant x y t:
transp_atoms x y (fv t) [=] fv (transp_term x y t).
Proof.
induction t; simpl; auto using empty_equivariant, singleton_equivariant;
try solve
[ rewrite union_equivariant; rewrite IHt1; rewrite IHt2; reflexivity
| repeat rewrite union_equivariant; rewrite IHt1; rewrite IHt2; rewrite IHt3; reflexivity
].
Qed.
Lemma open_rec_equivariant x y n t1 t2:
transp_term x y (open_rec n t1 t2) = open_rec n (transp_term x y t1) (transp_term x y t2).
Proof.
revert n. induction t2; intros; simpl in *; f_equal; auto.
- destruct (lt_eq_lt_dec n n0); simpl; auto.
destruct s; simpl; auto.
Qed.
Lemma open_equivariant x y t1 t2:
transp_term x y (open t1 t2) = open (transp_term x y t1) (transp_term x y t2).
Proof.
unfold open. apply open_rec_equivariant.
Qed.
Lemma close_rec_equivariant x y n z t:
transp_term x y (close_rec n z t) = close_rec n (transp_atom x y z) (transp_term x y t).
Proof.
revert n. induction t; intros; simpl in *; f_equal; auto.
- destruct (lt_ge_dec n n0); simpl; auto.
- destruct (z == x0); subst; simpl; auto.
+ destruct (transp_atom x y x0 == transp_atom x y x0); congruence.
+ destruct (transp_atom x y z == transp_atom x y x0); try congruence.
exfalso. apply n0. clear n0.
rewrite <- (transp_atom_involution x y z).
rewrite <- (transp_atom_involution x y x0).
congruence.
Qed.
Lemma close_equivariant x y z t:
transp_term x y (close z t) = close (transp_atom x y z) (transp_term x y t).
Proof.
unfold close. apply close_rec_equivariant.
Qed.
Lemma close_inverse x1 t1 x2 t2:
close x1 t1 = close x2 t2 →
transp_term x1 x2 t1 = t2.
Proof.
intro H.
destruct (x1 == x2); subst.
- apply close_inj in H. rewrite transp_term_refl. assumption.
- rewrite transp_term_freshR_is_subst.
+ rewrite subst_spec. rewrite H. apply open_close.
+ assert (x2 `notin` fv (close x2 t2)) as Hx2.
{ rewrite fv_close. auto. }
rewrite <- H in Hx2. rewrite fv_close in Hx2. fsetdec.
Qed.
Lemma close_rename x1 x2 t:
(x1 = x2 ∨ x2 `notin` fv t) →
close x1 t = close x2 (transp_term x1 x2 t).
Proof.
intros [Heq | Hfresh].
- subst. rewrite transp_term_refl. reflexivity.
- rewrite <- (transp_term_fresh_eq x1 x2 (close x1 t)).
+ rewrite (close_equivariant x1 x2 x1 t).
rewrite transp_atom_thisL. reflexivity.
+ rewrite fv_close. auto.
+ rewrite fv_close. auto.
Qed.
Lemma subst_equivariant x y t1 z t2:
transp_term x y (subst t1 z t2) = subst (transp_term x y t1) (transp_atom x y z) (transp_term x y t2).
Proof.
induction t2; simpl; f_equal; auto.
- destruct (x0 == z); subst.
+ destruct (transp_atom x y z == transp_atom x y z); congruence.
+ simpl. destruct (y == x0); subst.
× { rewrite transp_atom_thisR. destruct (x == z); subst.
- rewrite transp_atom_thisL. destruct (z == x0); congruence.
- rewrite transp_atom_other; auto. destruct (x == z); congruence.
}
× { destruct (x == x0); subst.
- rewrite transp_atom_thisL. destruct (y == z); subst.
+ rewrite transp_atom_thisR. destruct (z == x0); congruence.
+ rewrite transp_atom_other; auto. destruct (y == z); congruence.
- rewrite transp_atom_other; auto. destruct (x == z); [| destruct (y == z)]; subst.
+ rewrite transp_atom_thisL. destruct (x0 == y); congruence.
+ rewrite transp_atom_thisR. destruct (x0 == x); congruence.
+ rewrite transp_atom_other; auto. destruct (x0 == z); congruence.
}
Qed.
Lemma fv_transp_term_newL x y t:
x `notin` fv t →
y `in` fv t →
fv (transp_term x y t) [=] add x (remove y (fv t)).
Proof.
intros Hx Hy.
rewrite <- fv_equivariant.
rewrite transp_atoms_swap.
apply transp_atoms_freshR; assumption.
Qed.
Lemma fv_transp_term_newR x y t:
x `in` fv t →
y `notin` fv t →
fv (transp_term x y t) [=] add y (remove x (fv t)).
Proof.
intros Hx Hy.
rewrite <- fv_equivariant.
rewrite transp_atoms_swap.
apply transp_atoms_freshL; assumption.
Qed.
Lemma fv_transp_term_not_new x y t:
x `in` fv t →
y `in` fv t →
fv (transp_term x y t) [=] fv t.
Proof.
intros Hx Hy.
rewrite <- fv_equivariant.
apply transp_atoms_not_new_eq; assumption.
Qed.
Support for terms
Definition supported_term (S: atoms) (t: term) : Prop :=
∀ x y, x `notin` S → y `notin` S → transp_term x y t = t.
∀ x y, x `notin` S → y `notin` S → transp_term x y t = t.
supported_term is covariant in its first argument.
Lemma supported_term_subset S1 S2 t:
S1 [<=] S2 →
supported_term S1 t →
supported_term S2 t.
Proof.
intros Hincl Hsupp x y Hx Hy.
apply Hsupp; fsetdec.
Qed.
S1 [<=] S2 →
supported_term S1 t →
supported_term S2 t.
Proof.
intros Hincl Hsupp x y Hx Hy.
apply Hsupp; fsetdec.
Qed.
The support of a term are its free variables. This is Lemma 3.2 of
the ICFP'20 paper.
Lemma supported_term_fv S t:
supported_term S t ↔ fv t [<=] S.
Proof.
split; intro H.
- intros x Hx.
assert (x `in` S ∨ x `notin` S) as [HxS|HxS] by fsetdec; [ assumption |].
exfalso.
pick fresh y for (add x S `union` fv t).
assert (x `in` fv (transp_term x y t)) as Hx2 by (rewrite (H x y); auto).
rewrite fv_transp_term_newR in Hx2; auto.
fsetdec.
- intros x y Hx Hy.
apply transp_term_fresh_eq; auto.
Qed.
supported_term S t ↔ fv t [<=] S.
Proof.
split; intro H.
- intros x Hx.
assert (x `in` S ∨ x `notin` S) as [HxS|HxS] by fsetdec; [ assumption |].
exfalso.
pick fresh y for (add x S `union` fv t).
assert (x `in` fv (transp_term x y t)) as Hx2 by (rewrite (H x y); auto).
rewrite fv_transp_term_newR in Hx2; auto.
fsetdec.
- intros x y Hx Hy.
apply transp_term_fresh_eq; auto.
Qed.
Definition transp_env_term x y (e: env term) : env term :=
map (transp_term x y) (transp_dom x y e).
Lemma transp_env_term_app y x (e1 e2: env term) :
transp_env_term y x (e1 ++ e2) = transp_env_term y x e1 ++ transp_env_term y x e2.
Proof.
unfold transp_env_term.
rewrite transp_dom_app. rewrite map_app. reflexivity.
Qed.
Lemma transp_env_term_one y x z t:
transp_env_term y x (z ¬ t) = (transp_atom y x z ¬ transp_term y x t).
Proof.
reflexivity.
Qed.
Lemma transp_env_term_length y x (e: env term) :
length (transp_env_term y x e) = length e.
Proof.
unfold transp_env_term.
unfold map. rewrite map_length. rewrite transp_dom_length. reflexivity.
Qed.
Lemma transp_env_term_swap x y (e: env term):
transp_env_term x y e = transp_env_term y x e.
Proof.
unfold transp_env_term.
rewrite (transp_dom_swap x y).
unfold map. apply map_ext.
intros [z t]. rewrite transp_term_swap. reflexivity.
Qed.
Lemma transp_env_term_fresh_eq x y (e: env term):
all_env (fun t ⇒ fv t [<=] empty) e →
x `notin` dom e →
y `notin` dom e →
transp_env_term x y e = e.
Proof.
intros He Hx Hy.
unfold transp_env_term.
rewrite (transp_dom_fresh_eq x y); auto.
unfold map. rewrite <- map_id. apply map_ext_in.
intros [z t] Hin.
assert (fv t [<=] empty).
{ rewrite all_env_in in He. eapply He; eauto. }
rewrite transp_term_fresh_eq; auto; fsetdec.
Qed.
Lemma transp_env_term_refl x (e: env term) :
transp_env_term x x e = e.
Proof.
unfold transp_env_term.
rewrite transp_dom_refl.
unfold map. rewrite <- map_id. apply map_ext.
intros [y t]. rewrite transp_term_refl. auto.
Qed.
Lemma transp_env_term_trans x1 x2 x3 (e: env term) :
all_env (fun t ⇒ fv t [<=] empty) e →
x1 `notin` dom e →
x2 `notin` dom e →
transp_env_term x1 x2 (transp_env_term x2 x3 e) = transp_env_term x1 x3 e.
Proof.
intros He H1 H2.
unfold transp_env_term. rewrite <- transp_dom_map.
rewrite transp_dom_trans; auto.
unfold map. rewrite map_map. apply map_ext_in.
intros [y t] Hy.
assert (fv t [<=] empty).
{ rewrite transp_dom_swap in Hy.
rewrite <- (transp_atom_involution x3 x1 y) in Hy.
apply in_transp_dom in Hy; auto.
rewrite all_env_in in He. eapply He; eauto.
}
rewrite transp_term_trans; auto.
- fsetdec.
- fsetdec.
Qed.
Lemma transp_env_term_involution x y (e: env term):
transp_env_term x y (transp_env_term x y e) = e.
Proof.
unfold transp_env_term.
rewrite <- transp_dom_map.
rewrite transp_dom_involution.
unfold map. rewrite map_map.
rewrite <- map_id. apply map_ext.
intros [z t]. rewrite transp_term_involution. reflexivity.
Qed.
Lemma transp_env_term_compose x1 x2 y1 y2 (e: env term):
transp_env_term x1 x2 (transp_env_term y1 y2 e) =
transp_env_term
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_env_term x1 x2 e).
Proof.
unfold transp_env_term.
repeat rewrite <- transp_dom_map.
unfold map. repeat rewrite map_map.
rewrite transp_dom_compose.
apply map_ext.
intros [z t]. rewrite transp_term_compose. reflexivity.
Qed.
Properties of get
Lemma get_transp_env_term_equivariant x y z (e: env term):
option_map (transp_term x y) (get z e) = get (transp_atom x y z) (transp_env_term x y e).
Proof.
unfold transp_env_term.
rewrite get_map. rewrite <- get_transp_dom_equivariant.
reflexivity.
Qed.
Lemma get_transp_env_term_Some_equivariant x y z t (e: env term):
get z e = Some t ↔ get (transp_atom x y z) (transp_env_term x y e) = Some (transp_term x y t).
Proof.
rewrite <- get_transp_env_term_equivariant.
split; intro H.
- rewrite H. reflexivity.
- case_eq (get z e); intros.
+ f_equal.
rewrite H0 in H. simpl in H.
inversion H; subst.
rewrite <- (transp_term_involution x y t0).
rewrite H2. rewrite transp_term_involution.
reflexivity.
+ rewrite H0 in H. simpl in H. discriminate.
Qed.
Lemma get_transp_env_term_None_equivariant x y z (e: env term):
get z e = None ↔ get (transp_atom x y z) (transp_env_term x y e) = None.
Proof.
rewrite <- get_transp_env_term_equivariant.
split; intro H.
- rewrite H. reflexivity.
- case_eq (get z e); intros.
+ rewrite H0 in H. simpl in H. discriminate.
+ reflexivity.
Qed.
Lemma get_transp_env_term_this x y (e: env term):
all_env (fun t ⇒ fv t [<=] empty) e →
y `notin` dom e →
get y (transp_env_term x y e) = get x e.
Proof.
intros He Hy.
unfold transp_env_term.
rewrite get_map.
rewrite get_transp_dom_this; auto.
case_eq (get x e); intros; auto.
assert (fv t [<=] empty) by (eapply all_env_get in He; eauto).
rewrite transp_term_fresh_eq; auto; fsetdec.
Qed.
Lemma get_transp_env_term_old x y (e: env term):
y `notin` dom e →
y ≠ x →
get x (transp_env_term x y e) = get y e.
Proof.
intros Hy Hneq.
unfold transp_env_term.
rewrite get_map. rewrite get_transp_dom_old; auto.
case_eq (get y e); intros; auto.
apply get_in_dom in H. fsetdec.
Qed.
Lemma get_transp_env_term_old_removed x y (e: env term):
y `notin` dom e →
y ≠ x →
get x (transp_env_term x y e) = None.
Proof.
intros Hy Hneq.
rewrite get_transp_env_term_old; auto.
apply get_notin_dom. auto.
Qed.
Lemma get_transp_env_term_other z x y (e: env term):
z ≠ y →
z ≠ x →
get z (transp_env_term x y e) = option_map (transp_term x y) (get z e).
Proof.
intros Hz1 Hz2.
unfold transp_env_term, option_map.
rewrite get_map. rewrite get_transp_dom_other; auto.
Qed.
Lemma get_transp_env_term x y z (e: env term):
y `notin` dom e →
get (transp_atom x y z) (transp_env_term x y e) = option_map (transp_term x y) (get z e).
Proof.
intro Hy.
unfold transp_env_term, option_map.
rewrite get_map. rewrite get_transp_dom; auto.
Qed.
Properties of In
Lemma in_transp_env_term_this x y a (e: env term):
y `notin` dom e →
In (y, a) (transp_env_term x y e) ↔ In (x, transp_term x y a) e.
Proof.
intro Hy.
unfold transp_env_term.
unfold map. rewrite in_map_iff.
split.
- intros [[z t] [Heq H]]. inversion Heq; subst. clear Heq.
rewrite in_transp_dom_this in H; auto.
rewrite transp_term_involution. assumption.
- intro H.
∃ (y, transp_term x y a). split.
+ rewrite transp_term_involution. reflexivity.
+ rewrite in_transp_dom_this; auto.
Qed.
Lemma in_transp_env_term_old x y a (e: env term):
y `notin` dom e →
y ≠ x →
In (x, a) (transp_env_term x y e) ↔ In (y, transp_term x y a) e.
Proof.
intros Hy Hneq.
unfold transp_env_term.
unfold map. rewrite in_map_iff.
split.
- intros [[z t] [Heq H]].
inversion Heq; subst. clear Heq.
rewrite in_transp_dom_old in H; auto.
rewrite transp_term_involution. assumption.
- intro H.
∃ (x, transp_term x y a). split.
+ rewrite transp_term_involution. reflexivity.
+ rewrite in_transp_dom_old; auto.
Qed.
Lemma in_transp_env_term_old_removed x y a (e: env term):
y `notin` dom e →
y ≠ x →
¬ In (x, a) (transp_env_term x y e).
Proof.
intros Hy Hneq.
unfold transp_env_term.
unfold map. rewrite in_map_iff.
intros [[z t] [Heq H]].
inversion Heq; subst. clear Heq.
eapply in_transp_dom_old_removed; eauto.
Qed.
Lemma in_transp_env_term_other z x y a (e: env term):
z ≠ y →
z ≠ x →
In (z, a) (transp_env_term x y e) ↔ In (z, transp_term x y a) e.
Proof.
intros Hz1 Hz2.
unfold transp_env_term.
unfold map. rewrite in_map_iff.
split.
- intros [[z' t] [Heq H]].
inversion Heq; subst. clear Heq.
rewrite in_transp_dom_other in H; auto.
rewrite transp_term_involution. assumption.
- intro H. ∃ (z, transp_term x y a). split.
+ rewrite transp_term_involution. reflexivity.
+ rewrite in_transp_dom_other; auto.
Qed.
Lemma in_transp_env_term x y z a (e: env term):
y `notin` dom e →
In (transp_atom x y z, transp_term x y a) (transp_env_term x y e) ↔ In (z, a) e.
Proof.
intro Hy.
unfold transp_env_term.
unfold map. rewrite in_map_iff.
split.
- intros [[z' t] [Heq H]].
inversion Heq; subst. clear Heq.
assert (t = a); subst.
{ rewrite <- (transp_term_involution x y t).
rewrite <- (transp_term_involution x y a).
congruence.
}
apply in_transp_dom in H; auto.
- intro H. ∃ (transp_atom x y z, a). split; auto.
apply in_transp_dom; auto.
Qed.
Properties of dom
Lemma dom_equivariant_term x y (e: env term):
transp_atoms x y (dom e) [=] dom (transp_env_term x y e).
Proof.
unfold transp_env_term.
rewrite dom_map.
apply dom_equivariant.
Qed.
Lemma dom_transp_env_term_fresh_eq x y (e: env term):
x `notin` dom e →
y `notin` dom e →
dom (transp_env_term x y e) [=] dom e.
Proof.
intros Hx Hy.
unfold transp_env_term.
rewrite dom_map.
apply dom_transp_dom_fresh_eq; auto.
Qed.
Lemma dom_transp_env_term_newL x y (e: env term):
x `notin` dom e →
y `in` dom e →
dom (transp_env_term x y e) [=] add x (remove y (dom e)).
Proof.
intros Hx Hy.
unfold transp_env_term.
rewrite dom_map.
apply dom_transp_dom_newL; auto.
Qed.
Lemma dom_transp_env_term_newR x y (e: env term):
x `in` dom e →
y `notin` dom e →
dom (transp_env_term x y e) [=] add y (remove x (dom e)).
Proof.
intros Hx Hy.
unfold transp_env_term.
rewrite dom_map.
apply dom_transp_dom_newR; auto.
Qed.
Lemma dom_transp_env_term_not_new x y (e: env term):
x `in` dom e →
y `in` dom e →
dom (transp_env_term x y e) [=] dom e.
Proof.
intros Hx Hy.
unfold transp_env_term.
rewrite dom_map.
apply dom_transp_dom_not_new; auto.
Qed.
Lemma subst_env_equivariant x y e t:
transp_term x y (subst_env e t) = subst_env (transp_env_term x y e) (transp_term x y t).
Proof.
revert t. env induction e; intros; simpl; auto.
rewrite IHe. rewrite subst_equivariant. reflexivity.
Qed.
Transpositions and support on relations between environments of terms and terms
Definitions and basic properties
Definition transp_rel x y (R: rel (env term) term) : rel (env term) term :=
Rel _ _
(fun e v ⇒ in_rel R (transp_env_term x y e) (transp_term x y v)).
Rel _ _
(fun e v ⇒ in_rel R (transp_env_term x y e) (transp_term x y v)).
This is Definition 3.1 "Supporting set" page 11 of the ICFP'20
paper, that is specialized on relations.
Definition supported_rel (S: atoms) (R: rel (env term) term) : Prop :=
∀ x y, x `notin` S → y `notin` S → RelEquiv (transp_rel x y R) R.
Lemma supported_rel_subset (S1 S2: atoms) R:
S1 [<=] S2 →
supported_rel S1 R →
supported_rel S2 R.
Proof.
intros HS H1 x y Hx Hy.
apply (H1 x y); auto.
Qed.
Lemma transp_rel_swap x y R:
RelEquiv (transp_rel x y R) (transp_rel y x R).
Proof.
intros e v.
split; intro H; simpl in *;
rewrite transp_env_term_swap; rewrite transp_term_swap; assumption.
Qed.
Lemma transp_rel_fresh_eq S x y R:
supported_rel S R →
x `notin` S →
y `notin` S →
RelEquiv (transp_rel x y R) R.
Proof.
intros HS Hx Hy. eauto.
Qed.
Lemma transp_rel_refl x R :
RelEquiv (transp_rel x x R) R.
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_env_term_refl in H. rewrite transp_term_refl in H. assumption.
- rewrite transp_env_term_refl. rewrite transp_term_refl. assumption.
Qed.
Lemma transp_rel_trans S x1 x2 x3 R:
supported_rel S R →
x1 `notin` S →
x2 `notin` S →
RelEquiv (transp_rel x1 x2 (transp_rel x2 x3 R)) (transp_rel x1 x3 R).
Proof.
intros HS H1 H2.
destruct (x1 == x2); subst.
- rewrite transp_rel_refl. reflexivity.
- intros e v; split; intro Hev; simpl in ×.
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_env_term_swap x2 x3) in Hev.
rewrite transp_env_term_involution in Hev.
rewrite (transp_term_swap x2 x3) in Hev.
rewrite transp_term_involution in Hev.
rewrite transp_env_term_refl.
rewrite transp_term_refl.
assumption.
× rewrite transp_env_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× apply (HS x1 x2) in Hev; auto.
simpl in Hev.
rewrite transp_env_term_compose in Hev.
rewrite transp_term_compose in Hev.
rewrite transp_atom_thisR in Hev.
rewrite transp_atom_other in Hev; auto.
rewrite transp_env_term_involution in Hev.
rewrite transp_term_involution in Hev.
assumption.
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_env_term_swap x2 x3).
rewrite transp_env_term_involution.
rewrite (transp_term_swap x2 x3).
rewrite transp_term_involution.
rewrite transp_env_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× rewrite transp_env_term_refl.
rewrite transp_term_refl.
assumption.
× apply (HS x1 x2); auto.
simpl.
rewrite transp_env_term_compose.
rewrite transp_term_compose.
rewrite transp_atom_thisR.
rewrite transp_atom_other; auto.
rewrite transp_env_term_involution.
rewrite transp_term_involution.
assumption.
Qed.
Lemma transp_rel_involution x y R:
RelEquiv (transp_rel x y (transp_rel x y R)) R.
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_env_term_involution in H. rewrite transp_term_involution in H. assumption.
- rewrite transp_env_term_involution. rewrite transp_term_involution. assumption.
Qed.
Lemma transp_rel_compose x1 x2 y1 y2 R:
RelEquiv
(transp_rel x1 x2 (transp_rel y1 y2 R))
(transp_rel
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_rel x1 x2 R)).
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_env_term_compose. rewrite transp_term_compose.
repeat rewrite transp_atom_involution.
assumption.
- rewrite transp_env_term_compose in H. rewrite transp_term_compose in H.
repeat rewrite transp_atom_involution in H.
assumption.
Qed.
∀ x y, x `notin` S → y `notin` S → RelEquiv (transp_rel x y R) R.
Lemma supported_rel_subset (S1 S2: atoms) R:
S1 [<=] S2 →
supported_rel S1 R →
supported_rel S2 R.
Proof.
intros HS H1 x y Hx Hy.
apply (H1 x y); auto.
Qed.
Lemma transp_rel_swap x y R:
RelEquiv (transp_rel x y R) (transp_rel y x R).
Proof.
intros e v.
split; intro H; simpl in *;
rewrite transp_env_term_swap; rewrite transp_term_swap; assumption.
Qed.
Lemma transp_rel_fresh_eq S x y R:
supported_rel S R →
x `notin` S →
y `notin` S →
RelEquiv (transp_rel x y R) R.
Proof.
intros HS Hx Hy. eauto.
Qed.
Lemma transp_rel_refl x R :
RelEquiv (transp_rel x x R) R.
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_env_term_refl in H. rewrite transp_term_refl in H. assumption.
- rewrite transp_env_term_refl. rewrite transp_term_refl. assumption.
Qed.
Lemma transp_rel_trans S x1 x2 x3 R:
supported_rel S R →
x1 `notin` S →
x2 `notin` S →
RelEquiv (transp_rel x1 x2 (transp_rel x2 x3 R)) (transp_rel x1 x3 R).
Proof.
intros HS H1 H2.
destruct (x1 == x2); subst.
- rewrite transp_rel_refl. reflexivity.
- intros e v; split; intro Hev; simpl in ×.
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_env_term_swap x2 x3) in Hev.
rewrite transp_env_term_involution in Hev.
rewrite (transp_term_swap x2 x3) in Hev.
rewrite transp_term_involution in Hev.
rewrite transp_env_term_refl.
rewrite transp_term_refl.
assumption.
× rewrite transp_env_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× apply (HS x1 x2) in Hev; auto.
simpl in Hev.
rewrite transp_env_term_compose in Hev.
rewrite transp_term_compose in Hev.
rewrite transp_atom_thisR in Hev.
rewrite transp_atom_other in Hev; auto.
rewrite transp_env_term_involution in Hev.
rewrite transp_term_involution in Hev.
assumption.
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_env_term_swap x2 x3).
rewrite transp_env_term_involution.
rewrite (transp_term_swap x2 x3).
rewrite transp_term_involution.
rewrite transp_env_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× rewrite transp_env_term_refl.
rewrite transp_term_refl.
assumption.
× apply (HS x1 x2); auto.
simpl.
rewrite transp_env_term_compose.
rewrite transp_term_compose.
rewrite transp_atom_thisR.
rewrite transp_atom_other; auto.
rewrite transp_env_term_involution.
rewrite transp_term_involution.
assumption.
Qed.
Lemma transp_rel_involution x y R:
RelEquiv (transp_rel x y (transp_rel x y R)) R.
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_env_term_involution in H. rewrite transp_term_involution in H. assumption.
- rewrite transp_env_term_involution. rewrite transp_term_involution. assumption.
Qed.
Lemma transp_rel_compose x1 x2 y1 y2 R:
RelEquiv
(transp_rel x1 x2 (transp_rel y1 y2 R))
(transp_rel
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_rel x1 x2 R)).
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_env_term_compose. rewrite transp_term_compose.
repeat rewrite transp_atom_involution.
assumption.
- rewrite transp_env_term_compose in H. rewrite transp_term_compose in H.
repeat rewrite transp_atom_involution in H.
assumption.
Qed.
Lemma RelEquiv_equivariant x y R1 R2:
RelEquiv R1 R2 ↔ RelEquiv (transp_rel x y R1) (transp_rel x y R2).
Proof.
revert R1 R2.
assert (∀ R1 R2, RelEquiv R1 R2 → RelEquiv (transp_rel x y R1) (transp_rel x y R2)).
{ intros R1 R2 H12 e v. split; intro H; simpl in *; apply H12; auto. }
intros R1 R2; split; intro H12; auto.
apply H in H12.
repeat rewrite transp_rel_involution in H12.
assumption.
Qed.
Lemma RelIncl_equivariant x y R1 R2:
RelIncl R1 R2 ↔ RelIncl (transp_rel x y R1) (transp_rel x y R2).
Proof.
revert R1 R2.
assert (∀ R1 R2, RelIncl R1 R2 → RelIncl (transp_rel x y R1) (transp_rel x y R2)).
{ intros R1 R2 H12 e v H; simpl in *; apply H12; auto. }
intros R1 R2; split; intro H12; auto.
apply H in H12.
repeat rewrite transp_rel_involution in H12.
assumption.
Qed.
Lemma in_rel_equivariant x y R e v:
in_rel R e v ↔ in_rel (transp_rel x y R) (transp_env_term x y e) (transp_term x y v).
Proof.
simpl.
rewrite transp_env_term_involution.
rewrite transp_term_involution.
reflexivity.
Qed.
Add Parametric Morphism: transp_rel
with signature eq ==> eq ==> RelEquiv ==> RelEquiv
as transp_rel_morphism_eq.
Proof.
intros x y R1 R2 HR.
intros e v. split; intro Hev; simpl in *; apply HR; assumption.
Qed.
Add Parametric Morphism: transp_rel
with signature eq ==> eq ==> RelIncl ==> RelIncl
as transp_rel_morphism_incl.
Proof.
intros x y R1 R2 HR.
intros e v Hev; simpl in ×.
apply HR. assumption.
Qed.
Add Parametric Morphism: supported_rel
with signature AtomSetImpl.Equal ==> RelEquiv ==> iff
as supported_rel_morphism_equiv.
Proof.
intros S1 S2 HS R1 R2 HR.
split; intros H x y Hx Hy.
- rewrite <- HR. rewrite <- HS in Hx. rewrite <- HS in Hy. apply (H x y); auto.
- rewrite HR. rewrite HS in Hx. rewrite HS in Hy. apply (H x y); auto.
Qed.
Lemma supported_rel_equivariant x y S R:
supported_rel (transp_atoms x y S) (transp_rel x y R) ↔ supported_rel S R.
Proof.
revert S R.
assert (∀ S R, supported_rel (transp_atoms x y S) (transp_rel x y R) →
supported_rel S R).
{ intros S R H.
intros z1 z2 Hz1 Hz2.
apply (RelEquiv_equivariant x y).
rewrite transp_rel_compose.
apply (notin_equivariant x y) in Hz1.
apply (notin_equivariant x y) in Hz2.
apply (H _ _ Hz1 Hz2).
}
intros S R; split; intro H'; auto.
rewrite <- (transp_atoms_involution x y) in H'.
rewrite <- (transp_rel_involution x y) in H'.
apply H in H'.
assumption.
Qed.
Definition transp_family_rel x y (R: atom → rel (env term) term) : atom → rel (env term) term :=
fun z ⇒ transp_rel x y (R (transp_atom x y z)).
Lemma transp_family_rel_swap x y S R:
FamilyRelEquiv S (transp_family_rel x y R) (transp_family_rel y x R).
Proof.
intros z Hz e v.
split; intro H; simpl in *;
rewrite transp_atom_swap;
rewrite transp_env_term_swap;
rewrite transp_term_swap;
assumption.
Qed.
Definition supported_family_rel (S: atoms) (R: atom → rel (env term) term) : Prop :=
∀ x y, x `notin` S → y `notin` S → FamilyRelEquiv S (transp_family_rel x y R) R.
Lemma supported_family_rel_subset (S1 S2: atoms) R:
S1 [<=] S2 →
supported_family_rel S1 R →
supported_family_rel S2 R.
Proof.
intros HS H1 x y Hx Hy.
eapply FamilyRelEquiv_subset; eauto.
apply (H1 x y); auto.
Qed.
Lemma transp_family_rel_fresh_eq S x y R:
supported_family_rel S R →
x `notin` S →
y `notin` S →
FamilyRelEquiv S (transp_family_rel x y R) R.
Proof.
intros HS Hx Hy. eauto.
Qed.
Lemma transp_family_rel_refl x S R :
FamilyRelEquiv S (transp_family_rel x x R) R.
Proof.
intros z Hz e v. split; intro H; simpl in ×.
- rewrite transp_atom_refl in H.
rewrite transp_env_term_refl in H.
rewrite transp_term_refl in H.
assumption.
- rewrite transp_atom_refl.
rewrite transp_env_term_refl.
rewrite transp_term_refl.
assumption.
Qed.
Lemma transp_family_rel_trans S x1 x2 x3 R:
supported_family_rel S R →
x1 `notin` S →
x2 `notin` S →
x3 `notin` S →
FamilyRelEquiv S
(transp_family_rel x1 x2 (transp_family_rel x2 x3 R))
(transp_family_rel x1 x3 R).
Proof.
intros HS H1 H2 H3.
destruct (x1 == x2); subst.
- rewrite transp_family_rel_refl. reflexivity.
- intros z Hz e v; split; intro Hev; simpl in ×.
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_atom_swap x2 x3) in Hev.
rewrite transp_atom_involution in Hev.
rewrite (transp_env_term_swap x2 x3) in Hev.
rewrite transp_env_term_involution in Hev.
rewrite (transp_term_swap x2 x3) in Hev.
rewrite transp_term_involution in Hev.
rewrite transp_atom_refl.
rewrite transp_env_term_refl.
rewrite transp_term_refl.
assumption.
× rewrite transp_atom_refl in Hev.
rewrite transp_env_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× { apply (HS x1 x2) in Hev; auto.
- simpl in Hev.
rewrite transp_atom_compose in Hev.
rewrite transp_env_term_compose in Hev.
rewrite transp_term_compose in Hev.
rewrite transp_atom_thisR in Hev.
rewrite (transp_atom_other x1 x2 x3) in Hev; auto.
rewrite transp_atom_involution in Hev.
rewrite transp_env_term_involution in Hev.
rewrite transp_term_involution in Hev.
assumption.
- destruct (z == x1); [| destruct (z == x2)]; subst.
+ repeat rewrite transp_atom_thisL. assumption.
+ rewrite transp_atom_thisR. rewrite transp_atom_other; auto.
+ rewrite (transp_atom_other x1 x2); auto.
destruct (x3 == z); subst.
× rewrite transp_atom_thisR. assumption.
× rewrite (transp_atom_other x2 x3); auto.
}
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_atom_swap x2 x3).
rewrite transp_atom_involution.
rewrite (transp_env_term_swap x2 x3).
rewrite transp_env_term_involution.
rewrite (transp_term_swap x2 x3).
rewrite transp_term_involution.
rewrite transp_atom_refl in Hev.
rewrite transp_env_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× rewrite transp_atom_refl.
rewrite transp_env_term_refl.
rewrite transp_term_refl.
assumption.
× { apply (HS x1 x2); auto.
- destruct (z == x1); [| destruct (z == x2)]; subst.
+ repeat rewrite transp_atom_thisL. assumption.
+ rewrite transp_atom_thisR. rewrite transp_atom_other; auto.
+ rewrite (transp_atom_other x1 x2); auto.
destruct (x3 == z); subst.
× rewrite transp_atom_thisR. assumption.
× rewrite (transp_atom_other x2 x3); auto.
- simpl.
rewrite transp_atom_compose.
rewrite transp_env_term_compose.
rewrite transp_term_compose.
rewrite transp_atom_thisR.
rewrite (transp_atom_other x1 x2 x3); auto.
rewrite transp_atom_involution.
rewrite transp_env_term_involution.
rewrite transp_term_involution.
assumption.
}
Qed.
Lemma transp_family_rel_involution x y S R:
FamilyRelEquiv S (transp_family_rel x y (transp_family_rel x y R)) R.
Proof.
intros z Hz e v. split; intro H; simpl in ×.
- rewrite transp_atom_involution in H.
rewrite transp_env_term_involution in H.
rewrite transp_term_involution in H.
assumption.
- rewrite transp_atom_involution.
rewrite transp_env_term_involution.
rewrite transp_term_involution.
assumption.
Qed.
Lemma transp_family_rel_compose x1 x2 y1 y2 S R:
FamilyRelEquiv S
(transp_family_rel x1 x2 (transp_family_rel y1 y2 R))
(transp_family_rel
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_family_rel x1 x2 R)).
Proof.
intros z Hz e v. split; intro H; simpl in ×.
- rewrite transp_atom_compose.
rewrite transp_env_term_compose.
rewrite transp_term_compose.
repeat rewrite transp_atom_involution.
assumption.
- rewrite transp_atom_compose in H.
rewrite transp_env_term_compose in H.
rewrite transp_term_compose in H.
repeat rewrite transp_atom_involution in H.
assumption.
Qed.
Definition parametric_family_rel S R : Prop :=
∀ x y,
x `notin` S →
y `notin` S →
RelEquiv (transp_rel x y (R x)) (R y).
Lemma supported_family_rel_intro S R:
(∀ z, z `notin` S → supported_rel (add z S) (R z)) →
parametric_family_rel S R →
supported_family_rel S R.
Proof.
intros H Hrename x y Hx Hy.
destruct (x == y); subst.
- rewrite transp_family_rel_refl. reflexivity.
- intros z Hz e v. simpl.
destruct (x == z); [| destruct (y == z)]; subst.
+ rewrite transp_atom_thisL.
rewrite <- (Hrename y z); auto.
rewrite (transp_rel_swap y z).
rewrite (in_rel_equivariant z y).
rewrite transp_env_term_involution.
rewrite transp_term_involution.
reflexivity.
+ rewrite transp_atom_thisR.
rewrite <- (Hrename x z); auto.
rewrite (in_rel_equivariant x z).
rewrite transp_env_term_involution.
rewrite transp_term_involution.
reflexivity.
+ rewrite <- (H z Hz x y); auto.
simpl.
rewrite transp_atom_other; auto.
reflexivity.
Qed.
Lemma supported_family_parametric S R:
supported_family_rel S R →
parametric_family_rel S R.
Proof.
intros H x y Hx Hy e v. simpl.
transitivity (in_rel (transp_family_rel x y R y) e v).
- simpl. rewrite transp_atom_thisR. reflexivity.
- rewrite (H x y Hx Hy y); auto.
reflexivity.
Qed.
Lemma supported_family_instantiate S R:
supported_family_rel S R →
(∀ z, z `notin` S → supported_rel (add z S) (R z)).
Proof.
intros H z Hz x y Hx Hy e v. simpl.
transitivity (in_rel (transp_family_rel x y R (transp_atom x y z)) e v).
- simpl. rewrite transp_atom_involution. reflexivity.
- assert (x `notin` S) as Hx2 by fsetdec.
assert (y `notin` S) as Hy2 by fsetdec.
rewrite (H x y Hx2 Hy2 (transp_atom x y z)); auto.
+ rewrite transp_atom_other; auto.
reflexivity.
+ rewrite transp_atom_other; auto.
Qed.
Lemma supported_family_iff S R:
supported_family_rel S R
↔ (parametric_family_rel S R ∧ (∀ z, z `notin` S → supported_rel (add z S) (R z))).
Proof.
split; intro.
- split.
+ apply supported_family_parametric. assumption.
+ apply supported_family_instantiate. assumption.
- apply supported_family_rel_intro; tauto.
Qed.
Lemma parametric_family_rel_subset S1 S2 R:
S1 [<=] S2 →
parametric_family_rel S1 R →
parametric_family_rel S2 R.
Proof.
intros HS H x y Hx Hy. apply H; fsetdec.
Qed.
Definition lambda_rel (x: atom) (R: rel (env term) term) : atom → rel (env term) term :=
fun y ⇒ transp_rel y x R.
Add Parametric Morphism : lambda_rel
with signature eq ==> RelEquiv ==> pointwise RelEquiv
as lambda_rel_morphism_pointwise_equiv.
Proof.
intros x R1 R2 HR.
intros y.
intros e v. split; intro Hev; simpl in *; apply HR; assumption.
Qed.
Add Parametric Morphism : lambda_rel
with signature eq ==> RelEquiv ==> eq ==> RelEquiv
as lambda_rel_morphism_equiv.
Proof.
intros x R1 R2 HR. apply lambda_rel_morphism_pointwise_equiv; auto.
Qed.
Add Parametric Morphism S: lambda_rel
with signature eq ==> RelEquiv ==> (FamilyRelEquiv S)
as lambda_rel_morphism_family_equiv.
Proof.
intros x R1 R2 HR.
rewrite HR. reflexivity.
Qed.
Add Parametric Morphism : lambda_rel
with signature eq ==> RelIncl ==> pointwise RelIncl
as lambda_rel_morphism_pointwise_incl.
Proof.
intros x R1 R2 HR.
intros y.
intros e v. intro Hev; simpl in *; apply HR; assumption.
Qed.
Add Parametric Morphism : lambda_rel
with signature eq ==> RelIncl ==> eq ==> RelIncl
as lambda_rel_morphism_incl.
Proof.
intros x R1 R2 HR. apply lambda_rel_morphism_pointwise_incl; auto.
Qed.
Lemma parametric_family_rel_lambda_rel S x R:
supported_rel (add x S) R →
parametric_family_rel S (lambda_rel x R).
Proof.
intros Hsupp y z Hy Hz.
unfold lambda_rel.
destruct (x == y); [| destruct (x == z)]; subst.
- rewrite transp_rel_refl. rewrite transp_rel_swap. reflexivity.
- rewrite transp_rel_involution. rewrite transp_rel_refl. reflexivity.
- rewrite (transp_rel_swap y z).
rewrite transp_rel_trans; eauto.
reflexivity.
Qed.
Lemma lambda_rel_self x R:
RelEquiv (lambda_rel x R x) R.
Proof.
unfold lambda_rel. rewrite transp_rel_refl. reflexivity.
Qed.
Lemma lambda_rel_ext S x R:
x `notin` S →
parametric_family_rel S R →
FamilyRelEquiv S (lambda_rel x (R x)) R.
Proof.
intros Hx H z Hz z1 z2. unfold lambda_rel.
rewrite transp_rel_swap.
rewrite (H x z); auto.
reflexivity.
Qed.
Lemma lambda_rel_equivariant S x y z R:
FamilyRelEquiv S
(transp_family_rel x y (lambda_rel z R))
(lambda_rel (transp_atom x y z) (transp_rel x y R)).
Proof.
intros z' Hz' t1 t2.
simpl.
rewrite (transp_env_term_compose x y).
rewrite transp_atom_involution.
rewrite (transp_term_compose x y).
rewrite transp_atom_involution.
reflexivity.
Qed.
Add Parametric Morphism x y S: (transp_family_rel x y)
with signature FamilyRelEquiv S ==> FamilyRelEquiv (transp_atoms x y S)
as transp_family_rel_morphism_eq.
Proof.
intros R1 R2 HR.
intros z Hz e v. simpl.
apply (notin_equivariant x y) in Hz.
rewrite transp_atoms_involution in Hz.
rewrite (HR _ Hz).
reflexivity.
Qed.
Add Parametric Morphism S: (supported_family_rel S)
with signature FamilyRelEquiv S ==> iff
as supported_family_rel_morphism_equiv.
Proof.
intros R1 R2 HR.
split; intros H x y Hx Hy z Hz e v.
- simpl.
specialize (H _ _ Hx Hy _ Hz e v).
simpl in H.
rewrite (HR (transp_atom x y z)) in H.
+ rewrite (HR z) in H; auto.
+ destruct (z == x); [| destruct (z == y)]; subst.
× rewrite transp_atom_thisL. assumption.
× rewrite transp_atom_thisR. assumption.
× rewrite transp_atom_other; auto.
- simpl.
specialize (H _ _ Hx Hy _ Hz e v).
simpl in H.
rewrite (HR (transp_atom x y z)).
+ rewrite (HR z); auto.
+ destruct (z == x); [| destruct (z == y)]; subst.
× rewrite transp_atom_thisL. assumption.
× rewrite transp_atom_thisR. assumption.
× rewrite transp_atom_other; auto.
Qed.
Add Parametric Morphism: supported_family_rel
with signature AtomSetImpl.Equal ==> eq ==> iff
as supported_family_rel_morphism_equiv_set.
Proof.
intros S1 S2 HS R.
split; intros H x y Hx Hy.
- rewrite <- HS. rewrite <- HS in Hx. rewrite <- HS in Hy. apply (H x y); auto.
- rewrite HS. rewrite HS in Hx. rewrite HS in Hy. apply (H x y); auto.
Qed.
Add Parametric Morphism S: (parametric_family_rel S)
with signature FamilyRelEquiv S ==> iff
as parametric_family_rel_morphism_equiv.
Proof.
intros R1 R2 HR.
split; intros H x y Hx Hy.
- rewrite <- (HR x); auto. rewrite <- (HR y); auto.
- rewrite (HR x); auto. rewrite (HR y); auto.
Qed.
Add Parametric Morphism: parametric_family_rel
with signature AtomSetImpl.Equal ==> eq ==> iff
as parametric_family_rel_morphism_equiv_set.
Proof.
intros S1 S2 HS R.
split; intros H x y Hx Hy.
- rewrite <- HS in Hx. rewrite <- HS in Hy. apply (H x y); auto.
- rewrite HS in Hx. rewrite HS in Hy. apply (H x y); auto.
Qed.
Lemma FamilyRelEquiv_equivariant x y S R1 R2:
FamilyRelEquiv S R1 R2 ↔ FamilyRelEquiv (transp_atoms x y S) (transp_family_rel x y R1) (transp_family_rel x y R2).
Proof.
revert S R1 R2.
assert (∀ S R1 R2, FamilyRelEquiv S R1 R2 → FamilyRelEquiv (transp_atoms x y S) (transp_family_rel x y R1) (transp_family_rel x y R2)).
{ intros S R1 R2 H12 z Hz e v.
apply (notin_equivariant x y) in Hz.
rewrite transp_atoms_involution in Hz.
split; intro H; simpl in *; apply H12; auto.
}
intros S R1 R2; split; intro H12; auto.
apply H in H12.
rewrite transp_atoms_involution in H12.
repeat rewrite transp_family_rel_involution in H12.
assumption.
Qed.
Lemma supported_family_rel_equivariant x y S R:
supported_family_rel (transp_atoms x y S) (transp_family_rel x y R) ↔ supported_family_rel S R.
Proof.
split; intros H z1 z2 Hz1 Hz2.
- apply (FamilyRelEquiv_equivariant x y).
rewrite transp_family_rel_compose.
apply (notin_equivariant x y) in Hz1.
apply (notin_equivariant x y) in Hz2.
apply (H _ _ Hz1 Hz2).
- apply (notin_equivariant x y) in Hz1.
rewrite transp_atoms_involution in Hz1.
apply (notin_equivariant x y) in Hz2.
rewrite transp_atoms_involution in Hz2.
specialize (H _ _ Hz1 Hz2).
intros z Hz.
apply (notin_equivariant x y) in Hz.
rewrite transp_atoms_involution in Hz.
specialize (H _ Hz).
intros e v.
simpl.
specialize (H (transp_env_term x y e) (transp_term x y v)).
simpl in H.
rewrite transp_atom_compose.
rewrite transp_env_term_compose.
rewrite transp_term_compose.
assumption.
Qed.
Lemma parametric_family_rel_equivariant x y S R:
parametric_family_rel (transp_atoms x y S) (transp_family_rel x y R) ↔ parametric_family_rel S R.
Proof.
revert S R.
assert (∀ S R, parametric_family_rel (transp_atoms x y S) (transp_family_rel x y R) →
parametric_family_rel S R).
{ intros S R H.
intros z1 z2 Hz1 Hz2.
unfold parametric_family_rel in H.
apply (notin_equivariant x y) in Hz1.
apply (notin_equivariant x y) in Hz2.
specialize (H _ _ Hz1 Hz2).
apply (RelEquiv_equivariant x y) in H.
rewrite transp_rel_compose in H.
repeat rewrite transp_atom_involution in H.
intros e v.
specialize (H e v).
simpl in H.
repeat rewrite transp_atom_involution in H.
repeat rewrite transp_env_term_involution in H.
repeat rewrite transp_term_involution in H.
rewrite <- H.
reflexivity.
}
intros S R; split; intro H'; auto.
rewrite <- (transp_atoms_involution x y) in H'.
rewrite <- (transp_family_rel_involution x y) in H'.
apply H in H'.
assumption.
Qed.
Definition transp_vrel x y (R: rel term term) : rel term term :=
Rel _ _
(fun v1 v2 ⇒ in_rel R (transp_term x y v1) (transp_term x y v2)).
Definition supported_vrel (S: atoms) (R: rel term term) : Prop :=
∀ x y, x `notin` S → y `notin` S → RelEquiv (transp_vrel x y R) R.
Lemma supported_vrel_subset (S1 S2: atoms) R:
S1 [<=] S2 →
supported_vrel S1 R →
supported_vrel S2 R.
Proof.
intros HS H1 x y Hx Hy.
apply (H1 x y); auto.
Qed.
Lemma transp_vrel_swap x y R:
RelEquiv (transp_vrel x y R) (transp_vrel y x R).
Proof.
intros e v.
split; intro H; simpl in ×.
- repeat rewrite (transp_term_swap y x). assumption.
- repeat rewrite (transp_term_swap x y). assumption.
Qed.
Lemma transp_vrel_fresh_eq S x y R:
supported_vrel S R →
x `notin` S →
y `notin` S →
RelEquiv (transp_vrel x y R) R.
Proof.
intros HS Hx Hy. eauto.
Qed.
Lemma transp_vrel_refl x R :
RelEquiv (transp_vrel x x R) R.
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_term_refl in H. rewrite transp_term_refl in H. assumption.
- rewrite transp_term_refl. rewrite transp_term_refl. assumption.
Qed.
Lemma transp_vrel_trans S x1 x2 x3 R:
supported_vrel S R →
x1 `notin` S →
x2 `notin` S →
RelEquiv (transp_vrel x1 x2 (transp_vrel x2 x3 R)) (transp_vrel x1 x3 R).
Proof.
intros HS H1 H2.
destruct (x1 == x2); subst.
- rewrite transp_vrel_refl. reflexivity.
- intros e v; split; intro Hev; simpl in ×.
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_term_swap x2 x3) in Hev.
rewrite transp_term_involution in Hev.
rewrite (transp_term_swap x2 x3) in Hev.
rewrite transp_term_involution in Hev.
rewrite transp_term_refl.
rewrite transp_term_refl.
assumption.
× rewrite transp_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× apply (HS x1 x2) in Hev; auto.
simpl in Hev.
rewrite (transp_term_compose x1 x2 x2 x3) in Hev.
rewrite (transp_term_compose x1 x2 x2 x3) in Hev.
rewrite transp_atom_thisR in Hev.
rewrite transp_atom_other in Hev; auto.
rewrite transp_term_involution in Hev.
rewrite transp_term_involution in Hev.
assumption.
+ destruct (x1 == x3); [| destruct (x2 == x3)]; subst.
× rewrite (transp_term_swap x2 x3).
rewrite transp_term_involution.
rewrite (transp_term_swap x2 x3).
rewrite transp_term_involution.
rewrite transp_term_refl in Hev.
rewrite transp_term_refl in Hev.
assumption.
× rewrite transp_term_refl.
rewrite transp_term_refl.
assumption.
× apply (HS x1 x2); auto.
simpl.
rewrite (transp_term_compose x1 x2 x2 x3).
rewrite (transp_term_compose x1 x2 x2 x3).
rewrite transp_atom_thisR.
rewrite transp_atom_other; auto.
rewrite transp_term_involution.
rewrite transp_term_involution.
assumption.
Qed.
Lemma transp_vrel_involution x y R:
RelEquiv (transp_vrel x y (transp_vrel x y R)) R.
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite transp_term_involution in H. rewrite transp_term_involution in H. assumption.
- rewrite transp_term_involution. rewrite transp_term_involution. assumption.
Qed.
Lemma transp_vrel_compose x1 x2 y1 y2 R:
RelEquiv
(transp_vrel x1 x2 (transp_vrel y1 y2 R))
(transp_vrel
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_vrel x1 x2 R)).
Proof.
intros e v. split; intro H; simpl in ×.
- rewrite (transp_term_compose x1 x2).
repeat rewrite transp_atom_involution.
rewrite (transp_term_compose x1 x2).
repeat rewrite transp_atom_involution.
assumption.
- rewrite (transp_term_compose x1 x2) in H.
repeat rewrite transp_atom_involution in H.
rewrite (transp_term_compose x1 x2) in H.
repeat rewrite transp_atom_involution in H.
assumption.
Qed.
Lemma RelEquiv_equivariant_vrel x y R1 R2:
RelEquiv R1 R2 ↔ RelEquiv (transp_vrel x y R1) (transp_vrel x y R2).
Proof.
revert R1 R2.
assert (∀ R1 R2, RelEquiv R1 R2 → RelEquiv (transp_vrel x y R1) (transp_vrel x y R2)).
{ intros R1 R2 H12 e v. split; intro H; simpl in *; apply H12; auto. }
intros R1 R2; split; intro H12; auto.
apply H in H12.
repeat rewrite transp_vrel_involution in H12.
assumption.
Qed.
Lemma in_vrel_equivariant x y R v1 v2:
in_rel R v1 v2 ↔ in_rel (transp_vrel x y R) (transp_term x y v1) (transp_term x y v2).
Proof.
simpl.
rewrite transp_term_involution.
rewrite transp_term_involution.
reflexivity.
Qed.
Add Parametric Morphism: transp_vrel
with signature eq ==> eq ==> RelEquiv ==> RelEquiv
as transp_vrel_morphism_eq.
Proof.
intros x y R1 R2 HR.
intros e v. split; intro Hev; simpl in *; apply HR; assumption.
Qed.
Add Parametric Morphism: transp_vrel
with signature eq ==> eq ==> RelIncl ==> RelIncl
as transp_vrel_morphism_incl.
Proof.
intros x y R1 R2 HR.
intros e v Hev; simpl in ×.
apply HR. assumption.
Qed.
Add Parametric Morphism: supported_vrel
with signature AtomSetImpl.Equal ==> RelEquiv ==> iff
as supported_vrel_morphism_equiv.
Proof.
intros S1 S2 HS R1 R2 HR.
split; intros H x y Hx Hy.
- rewrite <- HR. rewrite <- HS in Hx. rewrite <- HS in Hy. apply (H x y); auto.
- rewrite HR. rewrite HS in Hx. rewrite HS in Hy. apply (H x y); auto.
Qed.
Fixpoint env_rel_equiv {A B} (e1 e2: env (rel A B)) { struct e1 } : Prop :=
match e1, e2 with
| nil, nil ⇒ True
| _ :: _, nil | nil, _ :: _ ⇒ False
| (x1, R1) :: e1, (x2, R2) :: e2 ⇒
x1 = x2 ∧ RelEquiv R1 R2 ∧ env_rel_equiv e1 e2
end.
Lemma env_rel_equiv_refl {A B} (e: env (rel A B)):
env_rel_equiv e e.
Proof.
env induction e; simpl; auto.
split; [| split]; auto.
reflexivity.
Qed.
Lemma env_rel_equiv_sym {A B} (e1 e2: env (rel A B)):
env_rel_equiv e1 e2 →
env_rel_equiv e2 e1.
Proof.
revert e2.
env induction e1; intros; (destruct e2; [| destruct p]); simpl in *; auto.
destruct H as [? [? ?]]; subst.
split; [| split]; auto.
symmetry. assumption.
Qed.
Lemma env_rel_equiv_trans {A B} (e1 e2 e3: env (rel A B)):
env_rel_equiv e1 e2 →
env_rel_equiv e2 e3 →
env_rel_equiv e1 e3.
Proof.
revert e2 e3.
env induction e1; intros;
(destruct e2 as [| p2 e2]; [| destruct p2]);
(destruct e3 as [| p3 e3]; [| destruct p3]);
simpl in *; auto; try contradiction.
destruct H as [? [? ?]].
destruct H0 as [? [? ?]].
subst.
split; [| split]; eauto.
etransitivity; eassumption.
Qed.
Properties of get
Lemma env_rel_equiv_get {A B} x (R1 R2: rel A B) e1 e2:
env_rel_equiv e1 e2 →
get x e1 = Some R1 →
get x e2 = Some R2 →
RelEquiv R1 R2.
Proof.
revert R1 e2 R2.
env induction e1; intros; destruct e2 as [| [y Ry] e2]; simpl in *;
auto; try discriminate.
destruct H as [? [? ?]]. subst.
destruct (x == y); subst.
- inversion H0; subst. clear H0. inversion H1; subst. clear H1.
assumption.
- eauto.
Qed.
Lemma env_rel_equiv_get_None {A B} x (e1 e2: env (rel A B)):
env_rel_equiv e1 e2 →
get x e1 = None ↔ get x e2 = None.
Proof.
revert x e1 e2.
assert (∀ x (e1 e2: env (rel A B)),
env_rel_equiv e1 e2 → get x e1 = None → get x e2 = None).
{ intros x e1.
env induction e1; intros; destruct e2 as [| [y Ry] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]. subst.
destruct (x == y); subst; try discriminate.
eauto.
}
intros x e1 e2 H12. split; intro Hx; eauto.
apply env_rel_equiv_sym in H12. eauto.
Qed.
Properties of map
Lemma env_rel_equiv_map_in {A B C D}
(f1: rel A B → rel C D) e1 (f2: rel A B → rel C D) e2:
(∀ x R1 R2, In (x, R1) e1 → RelEquiv R1 R2 → RelEquiv (f1 R1) (f2 R2)) →
env_rel_equiv e1 e2 →
env_rel_equiv (map f1 e1) (map f2 e2).
Proof.
intro Hf. revert e2.
env induction e1; intros; destruct e2 as [| [x2 R2] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]. subst.
split; [| split]; auto.
- eapply Hf; eauto.
- eauto.
Qed.
Lemma env_rel_equiv_map {A B C D}
(f1: rel A B → rel C D) e1 (f2: rel A B → rel C D) e2:
(∀ R1 R2, RelEquiv R1 R2 → RelEquiv (f1 R1) (f2 R2)) →
env_rel_equiv e1 e2 →
env_rel_equiv (map f1 e1) (map f2 e2).
Proof.
intro Hf. revert e2.
env induction e1; intros; destruct e2 as [| [x2 R2] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]. subst.
split; [| split]; auto.
Qed.
Properties of dom
Lemma env_rel_equiv_dom {A B} (e1 e2: env (rel A B)):
env_rel_equiv e1 e2 →
dom e1 [=] dom e2.
Proof.
intros H x. split; intro Hx.
- case_eq (get x e2); intros; eauto using get_in_dom.
rewrite <- env_rel_equiv_get_None in H0; eauto.
apply get_notin_dom in H0. fsetdec.
- case_eq (get x e1); intros; eauto using get_in_dom.
rewrite env_rel_equiv_get_None in H0; eauto.
apply get_notin_dom in H0. fsetdec.
Qed.
Add Parametric Relation A B: (env (rel A B)) (@env_rel_equiv A B)
reflexivity proved by env_rel_equiv_refl
symmetry proved by env_rel_equiv_sym
transitivity proved by env_rel_equiv_trans
as env_rel_equiv_rel.
Add Parametric Morphism : (@app (atom × rel (env term) term))
with signature env_rel_equiv ==> env_rel_equiv ==> env_rel_equiv
as app_morphism_env_rel_equiv.
Proof.
intros e1 e3 H13 e2 e4 H24.
revert e3 H13 e2 e4 H24.
env induction e1; intros; destruct e3 as [| [y Ry] e3]; simpl in *;
auto; try contradiction.
destruct H13 as [? [? ?]]. subst. split; [| split]; auto.
Qed.
Add Parametric Morphism A B: (@dom (rel A B))
with signature env_rel_equiv ==> AtomSetImpl.Equal
as dom_morphism_env_rel_equiv.
Proof.
exact env_rel_equiv_dom.
Qed.
Add Parametric Morphism : RelGather
with signature env_rel_equiv ==> RelEquiv
as RelGather_morphism_equiv.
Proof.
intros E1 E2 H.
intros e v; split; intros [Hegood [Hvgood Hev]]; (split; [| split]); auto.
- intros x R Hx.
case_eq (get x E1); intros.
+ specialize (Hev _ _ H0). destruct Hev as [v' [Hget Hr]].
∃ v'. split; auto.
assert (RelEquiv r R) as Heq by eauto using env_rel_equiv_get.
rewrite <- Heq. assumption.
+ rewrite (env_rel_equiv_get_None x E1 E2) in H0; auto. congruence.
- intros x R Hx.
case_eq (get x E2); intros.
+ specialize (Hev _ _ H0). destruct Hev as [v' [Hget Hr]].
∃ v'. split; auto.
assert (RelEquiv R r) as Heq by eauto using env_rel_equiv_get.
rewrite Heq. assumption.
+ rewrite <- (env_rel_equiv_get_None x E1 E2) in H0; auto. congruence.
Qed.
Add Parametric Morphism A B: (@uniq (rel A B))
with signature env_rel_equiv ==> iff
as uniq_morphism_equiv.
Proof.
intros e1.
env induction e1; intros [| [y R2] e2] Hequiv; simpl in Hequiv; try contradiction.
- reflexivity.
- destruct Hequiv as [Heq [HRelEquiv HEnvEquiv]]. subst y.
simpl. specialize (IHe1 _ HEnvEquiv).
split; intro H; inversion H; subst; apply IHe1 in H2.
+ rewrite HEnvEquiv in H4. auto.
+ rewrite <- HEnvEquiv in H4. auto.
Qed.
Add Parametric Morphism A B (P: rel A B → Prop)
(HPmorphism: ∀ R1 R2, RelEquiv R1 R2 → P R1 ↔ P R2):
(all_env P)
with signature env_rel_equiv ==> iff
as all_env_morphism_env_rel_equiv.
Proof.
intros E1.
env induction E1; intros [| [x2 R2] E2] HequivE; simpl in *; try tauto.
destruct HequivE as [Heqx [HequivR HequivE]]. subst x2.
rewrite (HPmorphism _ _ HequivR).
rewrite (IHE1 _ HequivE).
reflexivity.
Qed.
Fixpoint env_rel_incl {A B} (e1 e2: env (rel A B)) { struct e1 } : Prop :=
match e1, e2 with
| nil, nil ⇒ True
| _ :: _, nil | nil, _ :: _ ⇒ False
| (x1, R1) :: e1, (x2, R2) :: e2 ⇒
x1 = x2 ∧ RelIncl R1 R2 ∧ env_rel_incl e1 e2
end.
Lemma env_rel_incl_refl_equiv {A B} (e1 e2: env (rel A B)):
env_rel_equiv e1 e2 →
env_rel_incl e1 e2.
Proof.
revert e2.
env induction e1; intros e2 H; simpl; auto.
destruct e2 as [| [x2 a2]]; simpl in *; try contradiction.
destruct H as [? [? ?]].
split; [| split]; auto.
Qed.
Lemma env_rel_incl_refl {A B} (e: env (rel A B)):
env_rel_incl e e.
Proof.
apply env_rel_incl_refl_equiv. reflexivity.
Qed.
Lemma env_rel_incl_antisym {A B} (e1 e2: env (rel A B)):
env_rel_incl e1 e2 →
env_rel_incl e2 e1 →
env_rel_equiv e1 e2.
Proof.
revert e2.
env induction e1; intros;
(destruct e2 as [| p2 e2]; [| destruct p2]);
simpl in *; auto; try contradiction.
destruct H as [? [? ?]].
destruct H0 as [? [? ?]].
subst.
split; [| split]; eauto using RelIncl_antisym.
Qed.
Lemma env_rel_incl_trans {A B} (e1 e2 e3: env (rel A B)):
env_rel_incl e1 e2 →
env_rel_incl e2 e3 →
env_rel_incl e1 e3.
Proof.
revert e2 e3.
env induction e1; intros;
(destruct e2 as [| p2 e2]; [| destruct p2]);
(destruct e3 as [| p3 e3]; [| destruct p3]);
simpl in *; auto; try contradiction.
destruct H as [? [? ?]].
destruct H0 as [? [? ?]].
subst.
split; [| split]; eauto.
etransitivity; eassumption.
Qed.
Properties of get
Lemma env_rel_incl_get {A B} x R1 R2 (e1 e2: env (rel A B)):
env_rel_incl e1 e2 →
get x e1 = Some R1 →
get x e2 = Some R2 →
RelIncl R1 R2.
Proof.
revert R1 e2 R2.
env induction e1; intros; destruct e2 as [| [y Ry] e2]; simpl in *;
auto; try discriminate.
destruct H as [? [? ?]]. subst.
destruct (x == y); subst.
- inversion H0; subst. clear H0. inversion H1; subst. clear H1.
assumption.
- eauto.
Qed.
Lemma env_rel_incl_get_None {A B} x (e1 e2: env (rel A B)):
env_rel_incl e1 e2 →
get x e1 = None ↔ get x e2 = None.
Proof.
revert e2.
env induction e1; intros; destruct e2 as [| [y Ry] e2]; simpl in *;
auto; try tauto.
destruct H as [? [? ?]]. subst.
destruct (x == y); subst.
- split; intro; discriminate.
- eauto.
Qed.
Properties of map
Lemma env_rel_incl_map_in {A B C D}
(f1: rel A B → rel C D) e1 (f2: rel A B → rel C D) e2:
(∀ x R1 R2, In (x, R1) e1 → RelIncl R1 R2 → RelIncl (f1 R1) (f2 R2)) →
env_rel_incl e1 e2 →
env_rel_incl (map f1 e1) (map f2 e2).
Proof.
intro Hf. revert e2.
env induction e1; intros; destruct e2 as [| [x2 R2] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]. subst.
split; [| split]; auto.
- eapply Hf; eauto.
- eauto.
Qed.
Lemma env_rel_incl_map {A B C D}
(f1: rel A B → rel C D) e1 (f2: rel A B → rel C D) e2:
(∀ R1 R2, RelIncl R1 R2 → RelIncl (f1 R1) (f2 R2)) →
env_rel_incl e1 e2 →
env_rel_incl (map f1 e1) (map f2 e2).
Proof.
intro Hf. revert e2.
env induction e1; intros; destruct e2 as [| [x2 R2] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]. subst.
split; [| split]; auto.
Qed.
Properties of dom
Lemma env_rel_incl_dom {A B} (e1 e2: env (rel A B)):
env_rel_incl e1 e2 →
dom e1 [=] dom e2.
Proof.
intros H x. split; intro Hx.
- case_eq (get x e2); intros; eauto using get_in_dom.
rewrite <- env_rel_incl_get_None in H0; eauto.
apply get_notin_dom in H0. fsetdec.
- case_eq (get x e1); intros; eauto using get_in_dom.
rewrite env_rel_incl_get_None in H0; eauto.
apply get_notin_dom in H0. fsetdec.
Qed.
Add Parametric Relation A B: (env (rel A B)) (@env_rel_incl A B)
reflexivity proved by env_rel_incl_refl
transitivity proved by env_rel_incl_trans
as env_rel_incl_rel.
Add Parametric Morphism A B: (@env_rel_incl A B)
with signature env_rel_equiv ==> env_rel_equiv ==> iff
as env_rel_incl_morphism_env_rel_equiv.
Proof.
intros e1 e2 H12 e3 e4 H34. split; intro H.
- transitivity e1.
+ symmetry in H12. apply env_rel_incl_refl_equiv in H12. assumption.
+ transitivity e3; [ assumption |].
apply env_rel_incl_refl_equiv in H34. assumption.
- transitivity e2.
+ apply env_rel_incl_refl_equiv in H12. assumption.
+ transitivity e4; [ assumption |].
symmetry in H34. apply env_rel_incl_refl_equiv in H34. assumption.
Qed.
Add Parametric Morphism : (@app (atom × rel (env term) term))
with signature env_rel_incl ==> env_rel_incl ==> env_rel_incl
as app_morphism_env_rel_incl.
Proof.
intros e1 e3 H13 e2 e4 H24.
revert e3 H13 e2 e4 H24.
env induction e1; intros; destruct e3 as [| [y Ry] e3]; simpl in *;
auto; try contradiction.
destruct H13 as [? [? ?]]. subst. split; [| split]; auto.
Qed.
Add Parametric Morphism A B: (@dom (rel A B))
with signature env_rel_incl ==> AtomSetImpl.Equal
as dom_morphism_env_rel_incl.
Proof.
exact env_rel_incl_dom.
Qed.
Add Parametric Morphism : RelGather
with signature env_rel_incl ==> RelIncl
as RelGather_morphism_incl.
Proof.
intros E1 E2 H.
intros e v [Hegood [Hvgood Hev]]; (split; [| split]); auto.
- intros x R Hx.
case_eq (get x E1); intros.
+ specialize (Hev _ _ H0). destruct Hev as [v' [Hget Hr]].
∃ v'. split; auto.
assert (RelIncl r R) as Hincl by eauto using env_rel_incl_get.
apply Hincl. assumption.
+ rewrite (env_rel_incl_get_None x E1 E2) in H0; auto. congruence.
Qed.
Add Parametric Morphism A B: (@uniq (rel A B))
with signature env_rel_incl ==> iff
as uniq_morphism_incl.
Proof.
intros e1.
env induction e1; intros [| [y R2] e2] Hincl; simpl in Hincl; try contradiction.
- reflexivity.
- destruct Hincl as [Heq [HRelIncl HEnvIncl]]. subst y.
simpl. specialize (IHe1 _ HEnvIncl).
split; intro H; inversion H; subst; apply IHe1 in H2.
+ rewrite HEnvIncl in H4. auto.
+ rewrite <- HEnvIncl in H4. auto.
Qed.
Add Parametric Morphism A B (P: rel A B → Prop)
(HPmorphism: ∀ R1 R2, RelIncl R1 R2 → P R1 → P R2):
(all_env P)
with signature env_rel_incl ==> impl
as all_env_morphism_env_rel_incl.
Proof.
intros E1.
env induction E1; intros [| [x2 R2] E2] HinclE; simpl in *; try tauto.
- reflexivity.
- destruct HinclE as [Heqx [HinclR HinclE]]. subst x2.
intros [HR HE].
apply (HPmorphism _ _ HinclR) in HR.
apply (IHE1 _ HinclE) in HE.
auto.
Qed.
Transpositions and suppport on environments of relations between environments of terms and terms
Definitions and basic properties
Definition transp_env_rel x y (e: env (rel (env term) term)) : env (rel (env term) term) :=
map (transp_rel x y) (transp_dom x y e).
Definition supported_env_rel (S: atoms) (e: env (rel (env term) term)) : Prop :=
∀ x y, x `notin` S → y `notin` S → env_rel_equiv (transp_env_rel x y e) e.
Lemma supported_env_rel_subset (S1 S2: atoms) R:
S1 [<=] S2 →
supported_env_rel S1 R →
supported_env_rel S2 R.
Proof.
intros HS H1 x y Hx Hy.
apply (H1 x y); auto.
Qed.
Lemma supported_env_rel_in_rel S e x Rx:
supported_env_rel S e →
In (x, Rx) e →
supported_rel S Rx.
Proof.
intros HS Hx. env induction e; simpl in *; auto; try contradiction.
destruct Hx as [Hx | Hx].
- inversion Hx; subst.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
- apply IHe; auto.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
Qed.
Lemma supported_env_rel_in_atom S e x Rx:
supported_env_rel S e →
In (x, Rx) e →
∀ z1 z2, z1 `notin` S → z2 `notin` S → transp_atom z1 z2 x = x.
Proof.
intros HS Hx. env induction e; simpl in *; auto; try contradiction.
destruct Hx as [Hx | Hx].
- inversion Hx; subst.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
- apply IHe; auto.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
Qed.
Lemma supported_env_rel_contains_dom S e:
supported_env_rel S e →
dom e [<=] S.
Proof.
intros HS x Hx.
assert (x `in` S ∨ x `notin` S) as [HxS|HxS] by fsetdec; auto.
exfalso.
case_eq (get x e); intros.
- apply get_Some_in in H.
pick fresh y for ({{x}} `union` S).
assert (y `notin` S) as HyS by fsetdec.
specialize (supported_env_rel_in_atom _ _ _ _ HS H x y HxS HyS); auto.
rewrite transp_atom_thisL. fsetdec.
- apply get_notin_dom in H. fsetdec.
Qed.
Lemma supported_env_rel_cons S z R E:
supported_env_rel S (z ¬ R ++ E)
↔ (z `in` S ∧ supported_rel S R ∧ supported_env_rel S E).
Proof.
split.
- intro. split; [| split].
+ apply supported_env_rel_contains_dom in H.
simpl in H. fsetdec.
+ assert (In (z, R) (z ¬ R ++ E)).
{ left. reflexivity. }
eapply supported_env_rel_in_rel; eauto.
+ intros x y Hx Hy.
specialize (H _ _ Hx Hy).
simpl in H.
tauto.
- intros [Hz [HR HE]].
intros x y Hx Hy. simpl. split; [| split]; auto.
+ rewrite transp_atom_other; congruence.
+ apply (HE x y Hx Hy).
Qed.
Lemma transp_env_rel_app y x (e1 e2: env (rel (env term) term)) :
transp_env_rel y x (e1 ++ e2) = transp_env_rel y x e1 ++ transp_env_rel y x e2.
Proof.
unfold transp_env_rel.
rewrite transp_dom_app. rewrite map_app. reflexivity.
Qed.
Lemma transp_env_rel_one y x z R:
transp_env_rel y x (z ¬ R) = (transp_atom y x z ¬ transp_rel y x R).
Proof.
reflexivity.
Qed.
Lemma transp_env_rel_length y x (e: env (rel (env term) term)) :
length (transp_env_rel y x e) = length e.
Proof.
unfold transp_env_rel.
unfold map. rewrite map_length. rewrite transp_dom_length. reflexivity.
Qed.
Lemma transp_env_rel_swap x y (e: env (rel (env term) term)):
env_rel_equiv
(transp_env_rel x y e)
(transp_env_rel y x e).
Proof.
unfold transp_env_rel.
apply env_rel_equiv_map.
- intros R1 R2 H.
rewrite transp_rel_swap.
apply transp_rel_morphism_eq; auto.
- rewrite (transp_dom_swap x y). apply env_rel_equiv_refl.
Qed.
Lemma transp_env_rel_fresh_eq S x y (e: env (rel (env term) term)):
supported_env_rel S e →
x `notin` S →
y `notin` S →
env_rel_equiv (transp_env_rel x y e) e.
Proof.
intros HS Hx Hy. eauto.
Qed.
Lemma transp_env_rel_refl x (e: env (rel (env term) term)) :
env_rel_equiv (transp_env_rel x x e) e.
Proof.
unfold transp_env_rel.
rewrite transp_dom_refl.
transitivity (map id e).
- apply env_rel_equiv_map.
+ intros R1 R2 H. rewrite transp_rel_refl. assumption.
+ reflexivity.
- unfold map. rewrite <- map_id.
rewrite (map_ext _ id).
+ reflexivity.
+ intros [? ?]. reflexivity.
Qed.
Lemma transp_env_rel_trans S x1 x2 x3 e:
supported_env_rel S e →
x1 `notin` S →
x2 `notin` S →
env_rel_equiv (transp_env_rel x1 x2 (transp_env_rel x2 x3 e)) (transp_env_rel x1 x3 e).
Proof.
intros HS H1 H2.
destruct (x1 == x2); subst.
- rewrite transp_env_rel_refl. reflexivity.
- unfold transp_env_rel.
rewrite <- transp_dom_map.
rewrite map_map'.
apply env_rel_equiv_map_in.
+ intros x R1 R2 Hx HR.
rewrite (transp_rel_trans S); auto.
× rewrite HR. reflexivity.
× apply (in_transp_dom_equivariant x1 x2) in Hx.
rewrite transp_dom_involution in Hx.
apply (in_transp_dom_equivariant x2 x3) in Hx.
rewrite transp_dom_involution in Hx.
eapply supported_env_rel_in_rel; eauto.
+ apply supported_env_rel_contains_dom in HS.
rewrite transp_dom_trans.
× reflexivity.
× fsetdec.
× fsetdec.
Qed.
Lemma transp_env_rel_involution x y (e: env (rel (env term) term)):
env_rel_equiv (transp_env_rel x y (transp_env_rel x y e)) e.
Proof.
unfold transp_env_rel.
rewrite <- transp_dom_map.
rewrite transp_dom_involution.
rewrite map_map'.
rewrite <- map_id'.
apply env_rel_equiv_map.
- intros ? ? ?. rewrite transp_rel_involution. assumption.
- reflexivity.
Qed.
Lemma transp_env_rel_compose x1 x2 y1 y2 (e: env (rel (env term) term)):
env_rel_equiv
(transp_env_rel x1 x2 (transp_env_rel y1 y2 e))
(transp_env_rel
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_env_rel x1 x2 e)).
Proof.
unfold transp_env_rel.
repeat rewrite <- transp_dom_map.
repeat rewrite map_map'.
rewrite transp_dom_compose.
apply env_rel_equiv_map.
- intros R1 R2 H. rewrite transp_rel_compose. rewrite H. reflexivity.
- reflexivity.
Qed.
Properties of get
Lemma supported_env_rel_get S e x Rx:
supported_env_rel S e →
get x e = Some Rx →
supported_rel S Rx.
Proof.
intros HS Hx.
apply get_Some_in in Hx.
eapply supported_env_rel_in_rel; eauto.
Qed.
Lemma get_transp_env_rel_equivariant x y z (e: env (rel (env term) term)):
option_map (transp_rel x y) (get z e) = get (transp_atom x y z) (transp_env_rel x y e).
Proof.
unfold transp_env_rel.
rewrite get_map. rewrite <- get_transp_dom_equivariant.
reflexivity.
Qed.
Lemma get_transp_env_rel_Some_equivariant x y z R (e: env (rel (env term) term)):
get z e = Some R → get (transp_atom x y z) (transp_env_rel x y e) = Some (transp_rel x y R).
Proof.
rewrite <- get_transp_env_rel_equivariant.
intro H. rewrite H. reflexivity.
Qed.
Lemma get_transp_env_rel_Some_equivariant_inv x y z R (e: env (rel (env term) term)):
get z (transp_env_rel x y e) = Some R →
∃ R', get (transp_atom x y z) e = Some R' ∧ RelEquiv R' (transp_rel x y R).
Proof.
intro H.
env induction e; simpl in ×.
- discriminate.
- destruct (z == transp_atom x y x0); subst.
+ inversion H; subst.
∃ a. split.
× rewrite transp_atom_involution.
destruct (x0 == x0); congruence.
× rewrite transp_rel_involution. reflexivity.
+ apply IHe in H. clear IHe.
destruct H as [R' [Hget Hequiv]].
∃ R'. split; auto.
destruct (transp_atom x y z == x0); subst.
× rewrite transp_atom_involution in n. contradiction.
× assumption.
Qed.
Lemma get_transp_env_rel_None_equivariant x y z (e: env (rel (env term) term)):
get z e = None ↔ get (transp_atom x y z) (transp_env_rel x y e) = None.
Proof.
rewrite <- get_transp_env_rel_equivariant.
split; intro H.
- rewrite H. reflexivity.
- case_eq (get z e); intros.
+ rewrite H0 in H. simpl in H. discriminate.
+ reflexivity.
Qed.
Lemma get_transp_env_rel_this x y (e: env (rel (env term) term)):
y `notin` dom e →
get y (transp_env_rel x y e) = option_map (transp_rel x y) (get x e).
Proof.
intros Hy.
unfold transp_env_rel.
rewrite get_map.
rewrite get_transp_dom_this; auto.
Qed.
Lemma get_transp_env_rel_old x y (e: env (rel (env term) term)):
y `notin` dom e →
y ≠ x →
get x (transp_env_rel x y e) = option_map (transp_rel x y) (get y e).
Proof.
intros Hy Hneq.
unfold transp_env_rel.
rewrite get_map. rewrite get_transp_dom_old; auto.
Qed.
Lemma get_transp_env_rel_old_removed x y (e: env (rel (env term) term)):
y `notin` dom e →
y ≠ x →
get x (transp_env_rel x y e) = None.
Proof.
intros Hy Hneq.
rewrite get_transp_env_rel_old; auto.
apply get_notin_dom in Hy. rewrite Hy. reflexivity.
Qed.
Lemma get_transp_env_rel_other z x y (e: env (rel (env term) term)):
z ≠ y →
z ≠ x →
get z (transp_env_rel x y e) = option_map (transp_rel x y) (get z e).
Proof.
intros Hz1 Hz2.
unfold transp_env_rel, option_map.
rewrite get_map. rewrite get_transp_dom_other; auto.
Qed.
Lemma get_transp_env_rel x y z (e: env (rel (env term) term)):
y `notin` dom e →
get (transp_atom x y z) (transp_env_rel x y e) = option_map (transp_rel x y) (get z e).
Proof.
intro Hy.
unfold transp_env_rel, option_map.
rewrite get_map. rewrite get_transp_dom; auto.
Qed.
Properties of dom
Lemma dom_equivariant_rel x y (e: env (rel (env term) term)):
transp_atoms x y (dom e) [=] dom (transp_env_rel x y e).
Proof.
unfold transp_env_rel.
rewrite dom_map.
apply dom_equivariant.
Qed.
Lemma dom_transp_env_rel_fresh_eq x y (e: env (rel (env term) term)):
x `notin` dom e →
y `notin` dom e →
dom (transp_env_rel x y e) [=] dom e.
Proof.
intros Hx Hy.
unfold transp_env_rel.
rewrite dom_map.
apply dom_transp_dom_fresh_eq; auto.
Qed.
Lemma dom_transp_env_rel_newL x y (e: env (rel (env term) term)):
x `notin` dom e →
y `in` dom e →
dom (transp_env_rel x y e) [=] add x (remove y (dom e)).
Proof.
intros Hx Hy.
unfold transp_env_rel.
rewrite dom_map.
apply dom_transp_dom_newL; auto.
Qed.
Lemma dom_transp_env_rel_newR x y (e: env (rel (env term) term)):
x `in` dom e →
y `notin` dom e →
dom (transp_env_rel x y e) [=] add y (remove x (dom e)).
Proof.
intros Hx Hy.
unfold transp_env_rel.
rewrite dom_map.
apply dom_transp_dom_newR; auto.
Qed.
Lemma dom_transp_env_rel_not_new x y (e: env (rel (env term) term)):
x `in` dom e →
y `in` dom e →
dom (transp_env_rel x y e) [=] dom e.
Proof.
intros Hx Hy.
unfold transp_env_rel.
rewrite dom_map.
apply dom_transp_dom_not_new; auto.
Qed.
Add Parametric Morphism A B: (@dom (rel A B))
with signature env_rel_equiv ==> AtomSetImpl.Equal
as dom_morphism_rel_env_equiv.
Proof.
intros e1 e2 He. revert e2 He.
env induction e1; intros; destruct e2 as [| [y Ry] e2];
simpl in *; auto; try contradiction.
- reflexivity.
- destruct He as [Heq [Hy He]]. subst.
rewrite (IHe1 _ He); auto.
reflexivity.
Qed.
Add Parametric Morphism : transp_env_rel
with signature eq ==> eq ==> env_rel_equiv ==> env_rel_equiv
as transp_env_rel_morphism_env_rel_equiv.
Proof.
intros x y e1 e2 H.
generalize dependent e2.
env induction e1; intros; destruct e2 as [| [z2 R2] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]; subst.
split; [| split]; eauto.
apply RelEquiv_equivariant. auto.
Qed.
Add Parametric Morphism : transp_env_rel
with signature eq ==> eq ==> env_rel_incl ==> env_rel_incl
as transp_env_rel_morphism_env_rel_incl.
Proof.
intros x y e1 e2 H.
generalize dependent e2.
env induction e1; intros; destruct e2 as [| [z2 R2] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]; subst.
split; [| split]; eauto.
apply RelIncl_equivariant. auto.
Qed.
Add Parametric Morphism: supported_env_rel
with signature AtomSetImpl.Equal ==> env_rel_equiv ==> iff
as supported_env_rel_morphism_equiv.
Proof.
intros S1 S2 HS e1 e2 He.
split; intros H x y Hx Hy.
- rewrite <- He. rewrite <- HS in Hx. rewrite <- HS in Hy. apply (H x y); auto.
- rewrite He. rewrite HS in Hx. rewrite HS in Hy. apply (H x y); auto.
Qed.
Lemma env_rel_equiv_equivariant x y e1 e2:
env_rel_equiv e1 e2 ↔ env_rel_equiv (transp_env_rel x y e1) (transp_env_rel x y e2).
Proof.
revert e1 e2.
assert (∀ e1 e2, env_rel_equiv e1 e2 → env_rel_equiv (transp_env_rel x y e1) (transp_env_rel x y e2)).
{ intros e1 e2 H12. rewrite H12. reflexivity. }
intros e1 e2; split; intro H12; auto.
apply H in H12.
rewrite transp_env_rel_involution in H12.
rewrite transp_env_rel_involution in H12.
assumption.
Qed.
Lemma env_rel_incl_equivariant x y e1 e2:
env_rel_incl e1 e2 ↔ env_rel_incl (transp_env_rel x y e1) (transp_env_rel x y e2).
Proof.
revert e1 e2.
assert (∀ e1 e2, env_rel_incl e1 e2 → env_rel_incl (transp_env_rel x y e1) (transp_env_rel x y e2)).
{ intros e1 e2 H12. rewrite H12. reflexivity. }
intros e1 e2; split; intro H12; auto.
apply H in H12.
rewrite transp_env_rel_involution in H12.
rewrite transp_env_rel_involution in H12.
assumption.
Qed.
Lemma supported_env_rel_equivariant x y S e:
supported_env_rel (transp_atoms x y S) (transp_env_rel x y e) ↔ supported_env_rel S e.
Proof.
revert S e.
assert (∀ S e, supported_env_rel (transp_atoms x y S) (transp_env_rel x y e) →
supported_env_rel S e).
{ intros S e H.
intros z1 z2 Hz1 Hz2.
apply (env_rel_equiv_equivariant x y).
rewrite transp_env_rel_compose.
apply (notin_equivariant x y) in Hz1.
apply (notin_equivariant x y) in Hz2.
apply (H _ _ Hz1 Hz2).
}
intros S e; split; intro H'; auto.
rewrite <- (transp_atoms_involution x y) in H'.
rewrite <- (transp_env_rel_involution x y) in H'.
apply H in H'.
assumption.
Qed.
Lemma uniq_rel_equivariant x y e:
uniq (transp_env_rel x y e) ↔ uniq e.
Proof.
env induction e.
- reflexivity.
- rewrite transp_env_rel_app. rewrite transp_env_rel_one.
split; intro H; inversion H; subst.
+ rewrite <- dom_equivariant_rel in H4.
apply notin_equivariant in H4.
apply IHe in H2.
auto.
+ apply (notin_equivariant x y) in H4.
rewrite dom_equivariant_rel in H4.
apply IHe in H2.
auto.
Qed.
Transpositions and support on environments of relations between terms
Definitions and basic properties
Definition transp_env_vrel x y (e: env (rel term term)) : env (rel term term) :=
map (transp_vrel x y) (transp_dom x y e).
Definition supported_env_vrel (S: atoms) (e: env (rel term term)) : Prop :=
∀ x y, x `notin` S → y `notin` S → env_rel_equiv (transp_env_vrel x y e) e.
Lemma supported_env_vrel_subset (S1 S2: atoms) R:
S1 [<=] S2 →
supported_env_vrel S1 R →
supported_env_vrel S2 R.
Proof.
intros HS H1 x y Hx Hy.
apply (H1 x y); auto.
Qed.
Lemma supported_env_vrel_in_rel S e x Rx:
supported_env_vrel S e →
In (x, Rx) e →
supported_vrel S Rx.
Proof.
intros HS Hx. env induction e; simpl in *; auto; try contradiction.
destruct Hx as [Hx | Hx].
- inversion Hx; subst.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
- apply IHe; auto.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
Qed.
Lemma supported_env_vrel_in_atom S e x Rx:
supported_env_vrel S e →
In (x, Rx) e →
∀ z1 z2, z1 `notin` S → z2 `notin` S → transp_atom z1 z2 x = x.
Proof.
intros HS Hx. env induction e; simpl in *; auto; try contradiction.
destruct Hx as [Hx | Hx].
- inversion Hx; subst.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
- apply IHe; auto.
intros z1 z2 Hz1 Hz2.
specialize (HS _ _ Hz1 Hz2).
simpl in HS. tauto.
Qed.
Lemma supported_env_vrel_contains_dom S e:
supported_env_vrel S e →
dom e [<=] S.
Proof.
intros HS x Hx.
assert (x `in` S ∨ x `notin` S) as [HxS|HxS] by fsetdec; auto.
exfalso.
case_eq (get x e); intros.
- apply get_Some_in in H.
pick fresh y for ({{x}} `union` S).
assert (y `notin` S) as HyS by fsetdec.
specialize (supported_env_vrel_in_atom _ _ _ _ HS H x y HxS HyS); auto.
rewrite transp_atom_thisL. fsetdec.
- apply get_notin_dom in H. fsetdec.
Qed.
Lemma supported_env_vrel_cons S z R E:
supported_env_vrel S (z ¬ R ++ E)
↔ (z `in` S ∧ supported_vrel S R ∧ supported_env_vrel S E).
Proof.
split.
- intro. split; [| split].
+ apply supported_env_vrel_contains_dom in H.
simpl in H. fsetdec.
+ assert (In (z, R) (z ¬ R ++ E)).
{ left. reflexivity. }
eapply supported_env_vrel_in_rel; eauto.
+ intros x y Hx Hy.
specialize (H _ _ Hx Hy).
simpl in H.
tauto.
- intros [Hz [HR HE]].
intros x y Hx Hy. simpl. split; [| split]; auto.
+ rewrite transp_atom_other; congruence.
+ apply (HE x y Hx Hy).
Qed.
Lemma transp_env_vrel_app y x (e1 e2: env (rel term term)) :
transp_env_vrel y x (e1 ++ e2) = transp_env_vrel y x e1 ++ transp_env_vrel y x e2.
Proof.
unfold transp_env_vrel.
rewrite transp_dom_app. rewrite map_app. reflexivity.
Qed.
Lemma transp_env_vrel_one y x z R:
transp_env_vrel y x (z ¬ R) = (transp_atom y x z ¬ transp_vrel y x R).
Proof.
reflexivity.
Qed.
Lemma transp_env_vrel_length y x (e: env (rel term term)) :
length (transp_env_vrel y x e) = length e.
Proof.
unfold transp_env_vrel.
unfold map. rewrite map_length. rewrite transp_dom_length. reflexivity.
Qed.
Lemma transp_env_vrel_swap x y (e: env (rel term term)):
env_rel_equiv
(transp_env_vrel x y e)
(transp_env_vrel y x e).
Proof.
unfold transp_env_vrel.
apply env_rel_equiv_map.
- intros R1 R2 H.
rewrite transp_vrel_swap.
apply transp_vrel_morphism_eq; auto.
- rewrite (transp_dom_swap x y). apply env_rel_equiv_refl.
Qed.
Lemma transp_env_vrel_fresh_eq S x y (e: env (rel term term)):
supported_env_vrel S e →
x `notin` S →
y `notin` S →
env_rel_equiv (transp_env_vrel x y e) e.
Proof.
intros HS Hx Hy. eauto.
Qed.
Lemma transp_env_vrel_refl x (e: env (rel term term)) :
env_rel_equiv (transp_env_vrel x x e) e.
Proof.
unfold transp_env_vrel.
rewrite transp_dom_refl.
transitivity (map id e).
- apply env_rel_equiv_map.
+ intros R1 R2 H. rewrite transp_vrel_refl. assumption.
+ reflexivity.
- unfold map. rewrite <- map_id.
rewrite (map_ext _ id).
+ reflexivity.
+ intros [? ?]. reflexivity.
Qed.
Lemma transp_env_vrel_trans S x1 x2 x3 e:
supported_env_vrel S e →
x1 `notin` S →
x2 `notin` S →
env_rel_equiv (transp_env_vrel x1 x2 (transp_env_vrel x2 x3 e)) (transp_env_vrel x1 x3 e).
Proof.
intros HS H1 H2.
destruct (x1 == x2); subst.
- rewrite transp_env_vrel_refl. reflexivity.
- unfold transp_env_vrel.
rewrite <- transp_dom_map.
rewrite map_map'.
apply env_rel_equiv_map_in.
+ intros x R1 R2 Hx HR.
rewrite (transp_vrel_trans S); auto.
× rewrite HR. reflexivity.
× apply (in_transp_dom_equivariant x1 x2) in Hx.
rewrite transp_dom_involution in Hx.
apply (in_transp_dom_equivariant x2 x3) in Hx.
rewrite transp_dom_involution in Hx.
eapply supported_env_vrel_in_rel; eauto.
+ apply supported_env_vrel_contains_dom in HS.
rewrite transp_dom_trans.
× reflexivity.
× fsetdec.
× fsetdec.
Qed.
Lemma transp_env_vrel_involution x y (e: env (rel term term)):
env_rel_equiv (transp_env_vrel x y (transp_env_vrel x y e)) e.
Proof.
unfold transp_env_vrel.
rewrite <- transp_dom_map.
rewrite transp_dom_involution.
rewrite map_map'.
rewrite <- map_id'.
apply env_rel_equiv_map.
- intros ? ? ?. rewrite transp_vrel_involution. assumption.
- reflexivity.
Qed.
Lemma transp_env_vrel_compose x1 x2 y1 y2 (e: env (rel term term)):
env_rel_equiv
(transp_env_vrel x1 x2 (transp_env_vrel y1 y2 e))
(transp_env_vrel
(transp_atom x1 x2 y1)
(transp_atom x1 x2 y2)
(transp_env_vrel x1 x2 e)).
Proof.
unfold transp_env_vrel.
repeat rewrite <- transp_dom_map.
repeat rewrite map_map'.
rewrite transp_dom_compose.
apply env_rel_equiv_map.
- intros R1 R2 H. rewrite transp_vrel_compose. rewrite H. reflexivity.
- reflexivity.
Qed.
Properties of get
Lemma supported_env_vrel_get S e x Rx:
supported_env_vrel S e →
get x e = Some Rx →
supported_vrel S Rx.
Proof.
intros HS Hx.
apply get_Some_in in Hx.
eapply supported_env_vrel_in_rel; eauto.
Qed.
Lemma get_transp_env_vrel_equivariant x y z (e: env (rel term term)):
option_map (transp_vrel x y) (get z e) = get (transp_atom x y z) (transp_env_vrel x y e).
Proof.
unfold transp_env_vrel.
rewrite get_map. rewrite <- get_transp_dom_equivariant.
reflexivity.
Qed.
Lemma get_transp_env_vrel_Some_equivariant x y z R (e: env (rel term term)):
get z e = Some R → get (transp_atom x y z) (transp_env_vrel x y e) = Some (transp_vrel x y R).
Proof.
rewrite <- get_transp_env_vrel_equivariant.
intro H. rewrite H. reflexivity.
Qed.
Lemma get_transp_env_vrel_Some_equivariant_inv x y z R (e: env (rel term term)):
get z (transp_env_vrel x y e) = Some R →
∃ R', get (transp_atom x y z) e = Some R' ∧ RelEquiv R' (transp_vrel x y R).
Proof.
intro H.
env induction e; simpl in ×.
- discriminate.
- destruct (z == transp_atom x y x0); subst.
+ inversion H; subst.
∃ a. split.
× rewrite transp_atom_involution.
destruct (x0 == x0); congruence.
× rewrite transp_vrel_involution. reflexivity.
+ apply IHe in H. clear IHe.
destruct H as [R' [Hget Hequiv]].
∃ R'. split; auto.
destruct (transp_atom x y z == x0); subst.
× rewrite transp_atom_involution in n. contradiction.
× assumption.
Qed.
Lemma get_transp_env_vrel_None_equivariant x y z (e: env (rel term term)):
get z e = None ↔ get (transp_atom x y z) (transp_env_vrel x y e) = None.
Proof.
rewrite <- get_transp_env_vrel_equivariant.
split; intro H.
- rewrite H. reflexivity.
- case_eq (get z e); intros.
+ rewrite H0 in H. simpl in H. discriminate.
+ reflexivity.
Qed.
Lemma get_transp_env_vrel_this x y (e: env (rel term term)):
y `notin` dom e →
get y (transp_env_vrel x y e) = option_map (transp_vrel x y) (get x e).
Proof.
intros Hy.
unfold transp_env_vrel.
rewrite get_map.
rewrite get_transp_dom_this; auto.
Qed.
Lemma get_transp_env_vrel_old x y (e: env (rel term term)):
y `notin` dom e →
y ≠ x →
get x (transp_env_vrel x y e) = option_map (transp_vrel x y) (get y e).
Proof.
intros Hy Hneq.
unfold transp_env_vrel.
rewrite get_map. rewrite get_transp_dom_old; auto.
Qed.
Lemma get_transp_env_vrel_old_removed x y (e: env (rel term term)):
y `notin` dom e →
y ≠ x →
get x (transp_env_vrel x y e) = None.
Proof.
intros Hy Hneq.
rewrite get_transp_env_vrel_old; auto.
apply get_notin_dom in Hy. rewrite Hy. reflexivity.
Qed.
Lemma get_transp_env_vrel_other z x y (e: env (rel term term)):
z ≠ y →
z ≠ x →
get z (transp_env_vrel x y e) = option_map (transp_vrel x y) (get z e).
Proof.
intros Hz1 Hz2.
unfold transp_env_vrel, option_map.
rewrite get_map. rewrite get_transp_dom_other; auto.
Qed.
Lemma get_transp_env_vrel x y z (e: env (rel term term)):
y `notin` dom e →
get (transp_atom x y z) (transp_env_vrel x y e) = option_map (transp_vrel x y) (get z e).
Proof.
intro Hy.
unfold transp_env_vrel, option_map.
rewrite get_map. rewrite get_transp_dom; auto.
Qed.
Properties of dom
Lemma dom_equivariant_vrel x y (e: env (rel term term)):
transp_atoms x y (dom e) [=] dom (transp_env_vrel x y e).
Proof.
unfold transp_env_vrel.
rewrite dom_map.
apply dom_equivariant.
Qed.
Lemma dom_transp_env_vrel_fresh_eq x y (e: env (rel term term)):
x `notin` dom e →
y `notin` dom e →
dom (transp_env_vrel x y e) [=] dom e.
Proof.
intros Hx Hy.
unfold transp_env_vrel.
rewrite dom_map.
apply dom_transp_dom_fresh_eq; auto.
Qed.
Lemma dom_transp_env_vrel_newL x y (e: env (rel term term)):
x `notin` dom e →
y `in` dom e →
dom (transp_env_vrel x y e) [=] add x (remove y (dom e)).
Proof.
intros Hx Hy.
unfold transp_env_vrel.
rewrite dom_map.
apply dom_transp_dom_newL; auto.
Qed.
Lemma dom_transp_env_vrel_newR x y (e: env (rel term term)):
x `in` dom e →
y `notin` dom e →
dom (transp_env_vrel x y e) [=] add y (remove x (dom e)).
Proof.
intros Hx Hy.
unfold transp_env_vrel.
rewrite dom_map.
apply dom_transp_dom_newR; auto.
Qed.
Lemma dom_transp_env_vrel_not_new x y (e: env (rel term term)):
x `in` dom e →
y `in` dom e →
dom (transp_env_vrel x y e) [=] dom e.
Proof.
intros Hx Hy.
unfold transp_env_vrel.
rewrite dom_map.
apply dom_transp_dom_not_new; auto.
Qed.
Add Parametric Morphism : transp_env_vrel
with signature eq ==> eq ==> env_rel_equiv ==> env_rel_equiv
as transp_env_vrel_morphism_env_rel_equiv.
Proof.
intros x y e1 e2 H.
generalize dependent e2.
env induction e1; intros; destruct e2 as [| [z2 R2] e2]; simpl in *;
auto; try contradiction.
destruct H as [? [? ?]]; subst.
split; [| split]; eauto.
apply RelEquiv_equivariant_vrel. auto.
Qed.
Add Parametric Morphism: supported_env_vrel
with signature AtomSetImpl.Equal ==> env_rel_equiv ==> iff
as supported_env_vrel_morphism_equiv.
Proof.
intros S1 S2 HS e1 e2 He.
split; intros H x y Hx Hy.
- rewrite <- He. rewrite <- HS in Hx. rewrite <- HS in Hy. apply (H x y); auto.
- rewrite He. rewrite HS in Hx. rewrite HS in Hy. apply (H x y); auto.
Qed.
Lemma env_rel_equiv_equivariant_vrel x y e1 e2:
env_rel_equiv e1 e2 ↔ env_rel_equiv (transp_env_vrel x y e1) (transp_env_vrel x y e2).
Proof.
revert e1 e2.
assert (∀ e1 e2, env_rel_equiv e1 e2 → env_rel_equiv (transp_env_vrel x y e1) (transp_env_vrel x y e2)).
{ intros e1 e2 H12. rewrite H12. reflexivity. }
intros e1 e2; split; intro H12; auto.
apply H in H12.
rewrite transp_env_vrel_involution in H12.
rewrite transp_env_vrel_involution in H12.
assumption.
Qed.
Lemma supported_env_vrel_equivariant x y S e:
supported_env_vrel (transp_atoms x y S) (transp_env_vrel x y e) ↔ supported_env_vrel S e.
Proof.
revert S e.
assert (∀ S e, supported_env_vrel (transp_atoms x y S) (transp_env_vrel x y e) →
supported_env_vrel S e).
{ intros S e H.
intros z1 z2 Hz1 Hz2.
apply (env_rel_equiv_equivariant_vrel x y).
rewrite transp_env_vrel_compose.
apply (notin_equivariant x y) in Hz1.
apply (notin_equivariant x y) in Hz2.
apply (H _ _ Hz1 Hz2).
}
intros S e; split; intro H'; auto.
rewrite <- (transp_atoms_involution x y) in H'.
rewrite <- (transp_env_vrel_involution x y) in H'.
apply H in H'.
assumption.
Qed.