Coral.RelExtra: more relational combinators
Require Import Infrastructure.
Require Import Rel.
Require Import Env.
Require Import Transp.
Require Import RelGood.
Require Import RelStable.
Require Import SupportFacts.
Require Import EquivarianceFacts.
simplAPP
Definition simplAPP R1 R2 :=
Rel (env term) term
(fun e v ⇒
∃ v1 v2,
in_rel R1 e v1 ∧
in_rel R2 e v2 ∧
eval (App v1 v2) v
)
.
Rel (env term) term
(fun e v ⇒
∃ v1 v2,
in_rel R1 e v1 ∧
in_rel R2 e v2 ∧
eval (App v1 v2) v
)
.
Lemma APP_simplify R1 R2:
stable_rel R1 →
good_rel R2 →
RelEquiv (APP R1 R2) (simplAPP R1 R2).
Proof.
intros Hstable1 Hgood2. intros e v. split; intro H.
- destruct H as [e' [v1 [v2 [Hleq [H1 [H2 Heval]]]]]].
∃ v1, v2. split; [| split]; auto.
eapply Hstable1; eauto.
- destruct H as [v1 [v2 [H1 [H2 Heval]]]].
∃ e, v1, v2. split; [| split; [| split ]]; auto.
reflexivity.
Qed.
stable_rel R1 →
good_rel R2 →
RelEquiv (APP R1 R2) (simplAPP R1 R2).
Proof.
intros Hstable1 Hgood2. intros e v. split; intro H.
- destruct H as [e' [v1 [v2 [Hleq [H1 [H2 Heval]]]]]].
∃ v1, v2. split; [| split]; auto.
eapply Hstable1; eauto.
- destruct H as [v1 [v2 [H1 [H2 Heval]]]].
∃ e, v1, v2. split; [| split; [| split ]]; auto.
reflexivity.
Qed.
RelLet
Definition RelLet S x R1 R2 :=
RelClose S (lambda_rel x (RelCloseV (fun v ⇒ RelCompose (RelPush R1 x v) R2))).
Lemma RelLet_incl S S' R1 R2 x S1 S2:
S' [<=] S →
RelIncl R1 S1 →
RelIncl R2 S2 →
RelIncl (RelLet S x R1 R2) (RelLet S' x S1 S2).
Proof.
intros HS H1 H2 e v H. unfold RelLet in ×.
destruct H as [y [HyS H]].
∃ y. split; auto.
unfold lambda_rel in ×.
unfold transp_rel in ×.
unfold in_rel at 1 in H.
unfold in_rel at 1.
rewrite <- RelRemove_rewrite in H.
rewrite <- RelRemove_rewrite.
apply (RelRemove_incl _ _ _ _ _ H2 H1 _ _).
assumption.
Qed.
Add Parametric Morphism : RelLet
with signature AtomSetImpl.Subset --> eq ==> RelIncl ++> RelIncl ++> RelIncl
as RelLet_morphism_incl.
Proof.
intros. apply RelLet_incl; assumption.
Qed.
Lemma RelLet_equiv S S' x R1 R2 S1 S2:
S [=] S' →
RelEquiv R1 S1 →
RelEquiv R2 S2 →
RelEquiv (RelLet S x R1 R2) (RelLet S' x S1 S2).
Proof.
intros H1 HS H2. apply RelIncl_antisym; apply RelLet_incl; auto; fsetdec.
Qed.
Add Parametric Morphism: RelLet
with signature AtomSetImpl.Equal ==> eq ==> RelEquiv ==> RelEquiv ==> RelEquiv
as RelLet_morphism_equiv.
Proof.
intros. apply RelLet_equiv; assumption.
Qed.
Lemma RelLet_rel_equivariant x y S z R1 R2:
RelEquiv (transp_rel x y (RelLet S z R1 R2))
(RelLet (transp_atoms x y S)
(transp_atom x y z)
(transp_rel x y R1)
(transp_rel x y R2)).
Proof.
unfold RelLet.
rewrite RelClose_rel_equivariant.
apply RelClose_morphism_equiv.
rewrite lambda_rel_equivariant.
apply lambda_rel_morphism_family_equiv; auto.
rewrite <- RelRemove_rewrite.
rewrite RelRemove_rel_equivariant.
rewrite RelRemove_rewrite.
reflexivity.
Qed.
RelClose S (lambda_rel x (RelCloseV (fun v ⇒ RelCompose (RelPush R1 x v) R2))).
Lemma RelLet_incl S S' R1 R2 x S1 S2:
S' [<=] S →
RelIncl R1 S1 →
RelIncl R2 S2 →
RelIncl (RelLet S x R1 R2) (RelLet S' x S1 S2).
Proof.
intros HS H1 H2 e v H. unfold RelLet in ×.
destruct H as [y [HyS H]].
∃ y. split; auto.
unfold lambda_rel in ×.
unfold transp_rel in ×.
unfold in_rel at 1 in H.
unfold in_rel at 1.
rewrite <- RelRemove_rewrite in H.
rewrite <- RelRemove_rewrite.
apply (RelRemove_incl _ _ _ _ _ H2 H1 _ _).
assumption.
Qed.
Add Parametric Morphism : RelLet
with signature AtomSetImpl.Subset --> eq ==> RelIncl ++> RelIncl ++> RelIncl
as RelLet_morphism_incl.
Proof.
intros. apply RelLet_incl; assumption.
Qed.
Lemma RelLet_equiv S S' x R1 R2 S1 S2:
S [=] S' →
RelEquiv R1 S1 →
RelEquiv R2 S2 →
RelEquiv (RelLet S x R1 R2) (RelLet S' x S1 S2).
Proof.
intros H1 HS H2. apply RelIncl_antisym; apply RelLet_incl; auto; fsetdec.
Qed.
Add Parametric Morphism: RelLet
with signature AtomSetImpl.Equal ==> eq ==> RelEquiv ==> RelEquiv ==> RelEquiv
as RelLet_morphism_equiv.
Proof.
intros. apply RelLet_equiv; assumption.
Qed.
Lemma RelLet_rel_equivariant x y S z R1 R2:
RelEquiv (transp_rel x y (RelLet S z R1 R2))
(RelLet (transp_atoms x y S)
(transp_atom x y z)
(transp_rel x y R1)
(transp_rel x y R2)).
Proof.
unfold RelLet.
rewrite RelClose_rel_equivariant.
apply RelClose_morphism_equiv.
rewrite lambda_rel_equivariant.
apply lambda_rel_morphism_family_equiv; auto.
rewrite <- RelRemove_rewrite.
rewrite RelRemove_rel_equivariant.
rewrite RelRemove_rewrite.
reflexivity.
Qed.
Under suitable wellformedness conditions, the composition of
RelLetStrong with lambda_rel coincides with RelLet.
Lemma RelLet_rewrite S R1 R2 x :
x `notin` S →
supported_rel S R1 →
RelEquiv
(RelLet_strong S (lambda_rel x R2) R1)
(RelLet S x R1 R2).
Proof.
intros Hx Hsupp1.
intros e v. split; intro H; simpl in ×.
- destruct H as [y [Hy [v' [H1 H2]]]].
∃ y. split; [assumption|].
∃ (transp_term y x v').
∃ (x ¬ transp_term y x v' ++ transp_env_term y x e).
split; [ split; [ reflexivity | ] | ].
+ rewrite <- (Hsupp1 y x); auto. simpl.
rewrite transp_env_term_involution.
rewrite transp_term_involution.
assumption.
+ simpl_env in H2.
rewrite transp_env_term_app in H2.
rewrite transp_env_term_one in H2.
rewrite transp_atom_thisL in H2.
assumption.
- destruct H as [y [Hy [v' [e' [[Heq H1] H2]]]]]. subst.
∃ y. split; [assumption|].
∃ (transp_term y x v'). split.
+ rewrite <- (Hsupp1 y x); auto. simpl.
rewrite transp_term_involution.
assumption.
+ simpl_env.
rewrite transp_env_term_app.
rewrite transp_env_term_one.
rewrite transp_atom_thisL.
rewrite transp_term_involution.
assumption.
Qed.
Lemma RelLet_good S x R1 R2 :
x `notin` S →
supported_rel S R1 →
good_rel R1 →
good_rel R2 →
good_rel (RelLet S x R1 R2).
Proof.
intros Hx Hsupp1 Hgood1 Hgood2.
rewrite <- RelLet_rewrite; auto.
apply good_rel_RelLet_strong; auto.
intros y Hy. apply good_rel_equivariant. assumption.
Qed.
Hint Resolve RelLet_good : good_rel.
Lemma RelLet_stable S x R1 R2 :
x `notin` S →
supported_rel S R1 →
stable_rel R1 →
good_rel R2 →
stable_rel R2 →
stable_rel (RelLet S x R1 R2).
Proof.
intros Hx Hsupp1 Hstable1 Hgood2 Hstable2.
rewrite <- RelLet_rewrite; auto.
apply stable_RelLet_strong; auto.
- intros y Hy. apply good_rel_equivariant. assumption.
- intros y Hy. apply stable_equivariant. assumption.
Qed.
Hint Resolve RelLet_stable : stable_rel.
Lemma RelLet_supported S x R1 R2 :
x `notin` S →
supported_rel S R1 →
supported_rel (add x S) R2 →
supported_rel S (RelLet S x R1 R2).
Proof.
intros Hx Hsupp1 Hsupp2.
rewrite <- RelLet_rewrite; auto.
apply RelLet_strong_supported_rel; auto.
apply supported_family_iff. split.
- apply parametric_family_rel_lambda_rel. assumption.
- intros z Hz. unfold lambda_rel.
apply (supported_rel_equivariant z x) in Hsupp2.
rewrite add_equivariant in Hsupp2.
rewrite transp_atom_thisR in Hsupp2.
rewrite transp_atoms_fresh_eq in Hsupp2; auto.
Qed.
Hint Resolve RelLet_supported : supported_rel.
x `notin` S →
supported_rel S R1 →
RelEquiv
(RelLet_strong S (lambda_rel x R2) R1)
(RelLet S x R1 R2).
Proof.
intros Hx Hsupp1.
intros e v. split; intro H; simpl in ×.
- destruct H as [y [Hy [v' [H1 H2]]]].
∃ y. split; [assumption|].
∃ (transp_term y x v').
∃ (x ¬ transp_term y x v' ++ transp_env_term y x e).
split; [ split; [ reflexivity | ] | ].
+ rewrite <- (Hsupp1 y x); auto. simpl.
rewrite transp_env_term_involution.
rewrite transp_term_involution.
assumption.
+ simpl_env in H2.
rewrite transp_env_term_app in H2.
rewrite transp_env_term_one in H2.
rewrite transp_atom_thisL in H2.
assumption.
- destruct H as [y [Hy [v' [e' [[Heq H1] H2]]]]]. subst.
∃ y. split; [assumption|].
∃ (transp_term y x v'). split.
+ rewrite <- (Hsupp1 y x); auto. simpl.
rewrite transp_term_involution.
assumption.
+ simpl_env.
rewrite transp_env_term_app.
rewrite transp_env_term_one.
rewrite transp_atom_thisL.
rewrite transp_term_involution.
assumption.
Qed.
Lemma RelLet_good S x R1 R2 :
x `notin` S →
supported_rel S R1 →
good_rel R1 →
good_rel R2 →
good_rel (RelLet S x R1 R2).
Proof.
intros Hx Hsupp1 Hgood1 Hgood2.
rewrite <- RelLet_rewrite; auto.
apply good_rel_RelLet_strong; auto.
intros y Hy. apply good_rel_equivariant. assumption.
Qed.
Hint Resolve RelLet_good : good_rel.
Lemma RelLet_stable S x R1 R2 :
x `notin` S →
supported_rel S R1 →
stable_rel R1 →
good_rel R2 →
stable_rel R2 →
stable_rel (RelLet S x R1 R2).
Proof.
intros Hx Hsupp1 Hstable1 Hgood2 Hstable2.
rewrite <- RelLet_rewrite; auto.
apply stable_RelLet_strong; auto.
- intros y Hy. apply good_rel_equivariant. assumption.
- intros y Hy. apply stable_equivariant. assumption.
Qed.
Hint Resolve RelLet_stable : stable_rel.
Lemma RelLet_supported S x R1 R2 :
x `notin` S →
supported_rel S R1 →
supported_rel (add x S) R2 →
supported_rel S (RelLet S x R1 R2).
Proof.
intros Hx Hsupp1 Hsupp2.
rewrite <- RelLet_rewrite; auto.
apply RelLet_strong_supported_rel; auto.
apply supported_family_iff. split.
- apply parametric_family_rel_lambda_rel. assumption.
- intros z Hz. unfold lambda_rel.
apply (supported_rel_equivariant z x) in Hsupp2.
rewrite add_equivariant in Hsupp2.
rewrite transp_atom_thisR in Hsupp2.
rewrite transp_atoms_fresh_eq in Hsupp2; auto.
Qed.
Hint Resolve RelLet_supported : supported_rel.
RelLam
Definition RelLam S x R1 R2 :=
depFUN S R1 (fun v ⇒ RelClose S (lambda_rel x (RelCompose (RelPush R1 x v) R2))).
Lemma RelLam_incl S S' x R1 R2 S1 S2:
S' [<=] S →
RelEquiv R1 S1 →
RelIncl R2 S2 →
RelIncl (RelLam S x R1 R2) (RelLam S' x S1 S2).
Proof.
intros HS H1 H2 e v [Hedom [Hegood [Hvgood H]]]. unfold RelLam in ×.
split; [| split; [| split ] ]; auto.
- fsetdec.
- intros e' Hleq v1 Hv1 v2 Heval.
apply H1 in Hv1.
specialize (H e' Hleq v1 Hv1 v2 Heval).
destruct H as [y [HyS [v' [[Heq HR1] HR2]]]].
∃ y. split; auto. ∃ v'. split.
+ split; auto. apply H1. assumption.
+ apply H2. assumption.
Qed.
Add Parametric Morphism : RelLam
with signature AtomSetImpl.Subset --> eq ==> RelEquiv ==> RelIncl ++> RelIncl
as RelLam_morphism_incl.
Proof.
intros. apply RelLam_incl; assumption.
Qed.
Lemma RelLam_equiv S S' x R1 R2 S1 S2:
S [=] S' →
RelEquiv R1 S1 →
RelEquiv R2 S2 →
RelEquiv (RelLam S x R1 R2) (RelLam S' x S1 S2).
Proof.
intros H1 HS H2. apply RelIncl_antisym; apply RelLam_incl; auto.
- fsetdec.
- fsetdec.
- symmetry. assumption.
Qed.
Add Parametric Morphism: RelLam
with signature AtomSetImpl.Equal ==> eq ==> RelEquiv ==> RelEquiv ==> RelEquiv
as RelLam_morphism_equiv.
Proof.
intros. apply RelLam_equiv; assumption.
Qed.
Lemma RelLam_rel_equivariant x y S z R1 R2:
RelEquiv (transp_rel x y (RelLam S z R1 R2))
(RelLam (transp_atoms x y S)
(transp_atom x y z)
(transp_rel x y R1)
(transp_rel x y R2)).
Proof.
unfold RelLam.
rewrite depFUN_rel_equivariant.
apply depFUN_morphism_equiv; [ reflexivity | reflexivity | ].
intros v.
rewrite RelClose_rel_equivariant.
apply RelClose_morphism_equiv.
rewrite lambda_rel_equivariant.
apply lambda_rel_morphism_family_equiv; [ reflexivity | ].
rewrite RelCompose_RelPush_equivariant.
rewrite transp_term_involution.
reflexivity.
Qed.
Lemma RelLam_good S x R1 R2 :
good_rel (RelLam S x R1 R2).
Proof.
intros e v [Hedom [Hegood [Hvgood H]]]. auto.
Qed.
Hint Resolve RelLam_good : good_rel.
Lemma RelLam_stable S x R1 R2 :
stable_rel (RelLam S x R1 R2).
Proof.
apply stable_depFUN.
Qed.
Hint Resolve RelLam_stable : stable_rel.
Lemma RelCompose_RelPush_transp_term {A} x1 x2 R1 x v (R2: rel _ A) :
good_rel R1 →
RelEquiv (RelCompose (RelPush R1 x (transp_term x1 x2 v)) R2)
(RelCompose (RelPush R1 x v) R2).
Proof.
intro Hgood1.
revert v.
assert (∀ v, RelIncl (RelCompose (RelPush R1 x (transp_term x1 x2 v)) R2)
(RelCompose (RelPush R1 x v) R2)).
{ intros v e t. intros [e' [[Heq H1] H2]]; subst.
assert (good_value v).
{ apply (good_value_equivariant x1 x2). eauto. }
assert (fv v [<=] empty) by auto.
rewrite (transp_term_fresh_eq x1 x2) in H1; [ | fsetdec | fsetdec ].
rewrite (transp_term_fresh_eq x1 x2) in H2; [ | fsetdec | fsetdec ].
∃ (x ¬ v ++ e). split; [ split; [ reflexivity | assumption ] | assumption ].
}
intros v e t; split; intro H0.
- apply H. assumption.
- rewrite <- (transp_term_involution x1 x2 v) in H0.
apply H in H0. assumption.
Qed.
Lemma RelLam_supported S x R1 R2 :
good_rel R1 →
supported_rel S R1 →
supported_rel (add x S) R2 →
supported_rel S (RelLam S x R1 R2).
Proof.
intros Hgood1 Hsupp1 Hsupp2.
apply depFUN_supported_rel; auto; try reflexivity.
intros x1 x2 Hx1 Hx2 v.
rewrite RelClose_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
rewrite lambda_rel_equivariant.
apply RelClose_morphism_equiv.
intros z Hz. unfold lambda_rel.
repeat rewrite RelCompose_RelPush_equivariant.
rewrite (Hsupp1 x1 x2); auto.
rewrite transp_term_involution.
repeat rewrite transp_atom_thisR.
destruct (x1 == x2); [ | destruct (z == x)]; subst.
- rewrite transp_atom_refl.
rewrite transp_rel_refl.
reflexivity.
- repeat rewrite transp_rel_refl.
rewrite transp_term_refl.
destruct (x1 == x); [ | destruct (x2 == x) ]; subst.
+ rewrite transp_atom_thisL.
rewrite transp_rel_involution.
rewrite (Hsupp1 x x2); auto.
rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_thisR.
rewrite (transp_rel_swap x1 x).
rewrite transp_rel_involution.
rewrite (Hsupp1 x x1); auto.
rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_other; auto.
repeat rewrite transp_rel_refl.
rewrite transp_term_refl.
rewrite (Hsupp2 x1 x2); auto.
reflexivity.
- destruct (x1 == x); [ | destruct (x2 == x) ]; subst.
+ rewrite transp_atom_thisL.
rewrite (Hsupp1 z x2); auto.
rewrite (Hsupp1 z x); auto.
rewrite (transp_rel_swap x x2).
rewrite (transp_rel_trans (add x S)); auto.
repeat rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_thisR.
rewrite (Hsupp1 z x1); auto.
rewrite (Hsupp1 z x); auto.
rewrite (transp_rel_trans (add x S)); auto.
repeat rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_other; auto.
rewrite (Hsupp2 x1 x2); auto.
reflexivity.
Qed.
Hint Resolve RelLam_supported : supported_rel.
depFUN S R1 (fun v ⇒ RelClose S (lambda_rel x (RelCompose (RelPush R1 x v) R2))).
Lemma RelLam_incl S S' x R1 R2 S1 S2:
S' [<=] S →
RelEquiv R1 S1 →
RelIncl R2 S2 →
RelIncl (RelLam S x R1 R2) (RelLam S' x S1 S2).
Proof.
intros HS H1 H2 e v [Hedom [Hegood [Hvgood H]]]. unfold RelLam in ×.
split; [| split; [| split ] ]; auto.
- fsetdec.
- intros e' Hleq v1 Hv1 v2 Heval.
apply H1 in Hv1.
specialize (H e' Hleq v1 Hv1 v2 Heval).
destruct H as [y [HyS [v' [[Heq HR1] HR2]]]].
∃ y. split; auto. ∃ v'. split.
+ split; auto. apply H1. assumption.
+ apply H2. assumption.
Qed.
Add Parametric Morphism : RelLam
with signature AtomSetImpl.Subset --> eq ==> RelEquiv ==> RelIncl ++> RelIncl
as RelLam_morphism_incl.
Proof.
intros. apply RelLam_incl; assumption.
Qed.
Lemma RelLam_equiv S S' x R1 R2 S1 S2:
S [=] S' →
RelEquiv R1 S1 →
RelEquiv R2 S2 →
RelEquiv (RelLam S x R1 R2) (RelLam S' x S1 S2).
Proof.
intros H1 HS H2. apply RelIncl_antisym; apply RelLam_incl; auto.
- fsetdec.
- fsetdec.
- symmetry. assumption.
Qed.
Add Parametric Morphism: RelLam
with signature AtomSetImpl.Equal ==> eq ==> RelEquiv ==> RelEquiv ==> RelEquiv
as RelLam_morphism_equiv.
Proof.
intros. apply RelLam_equiv; assumption.
Qed.
Lemma RelLam_rel_equivariant x y S z R1 R2:
RelEquiv (transp_rel x y (RelLam S z R1 R2))
(RelLam (transp_atoms x y S)
(transp_atom x y z)
(transp_rel x y R1)
(transp_rel x y R2)).
Proof.
unfold RelLam.
rewrite depFUN_rel_equivariant.
apply depFUN_morphism_equiv; [ reflexivity | reflexivity | ].
intros v.
rewrite RelClose_rel_equivariant.
apply RelClose_morphism_equiv.
rewrite lambda_rel_equivariant.
apply lambda_rel_morphism_family_equiv; [ reflexivity | ].
rewrite RelCompose_RelPush_equivariant.
rewrite transp_term_involution.
reflexivity.
Qed.
Lemma RelLam_good S x R1 R2 :
good_rel (RelLam S x R1 R2).
Proof.
intros e v [Hedom [Hegood [Hvgood H]]]. auto.
Qed.
Hint Resolve RelLam_good : good_rel.
Lemma RelLam_stable S x R1 R2 :
stable_rel (RelLam S x R1 R2).
Proof.
apply stable_depFUN.
Qed.
Hint Resolve RelLam_stable : stable_rel.
Lemma RelCompose_RelPush_transp_term {A} x1 x2 R1 x v (R2: rel _ A) :
good_rel R1 →
RelEquiv (RelCompose (RelPush R1 x (transp_term x1 x2 v)) R2)
(RelCompose (RelPush R1 x v) R2).
Proof.
intro Hgood1.
revert v.
assert (∀ v, RelIncl (RelCompose (RelPush R1 x (transp_term x1 x2 v)) R2)
(RelCompose (RelPush R1 x v) R2)).
{ intros v e t. intros [e' [[Heq H1] H2]]; subst.
assert (good_value v).
{ apply (good_value_equivariant x1 x2). eauto. }
assert (fv v [<=] empty) by auto.
rewrite (transp_term_fresh_eq x1 x2) in H1; [ | fsetdec | fsetdec ].
rewrite (transp_term_fresh_eq x1 x2) in H2; [ | fsetdec | fsetdec ].
∃ (x ¬ v ++ e). split; [ split; [ reflexivity | assumption ] | assumption ].
}
intros v e t; split; intro H0.
- apply H. assumption.
- rewrite <- (transp_term_involution x1 x2 v) in H0.
apply H in H0. assumption.
Qed.
Lemma RelLam_supported S x R1 R2 :
good_rel R1 →
supported_rel S R1 →
supported_rel (add x S) R2 →
supported_rel S (RelLam S x R1 R2).
Proof.
intros Hgood1 Hsupp1 Hsupp2.
apply depFUN_supported_rel; auto; try reflexivity.
intros x1 x2 Hx1 Hx2 v.
rewrite RelClose_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
rewrite lambda_rel_equivariant.
apply RelClose_morphism_equiv.
intros z Hz. unfold lambda_rel.
repeat rewrite RelCompose_RelPush_equivariant.
rewrite (Hsupp1 x1 x2); auto.
rewrite transp_term_involution.
repeat rewrite transp_atom_thisR.
destruct (x1 == x2); [ | destruct (z == x)]; subst.
- rewrite transp_atom_refl.
rewrite transp_rel_refl.
reflexivity.
- repeat rewrite transp_rel_refl.
rewrite transp_term_refl.
destruct (x1 == x); [ | destruct (x2 == x) ]; subst.
+ rewrite transp_atom_thisL.
rewrite transp_rel_involution.
rewrite (Hsupp1 x x2); auto.
rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_thisR.
rewrite (transp_rel_swap x1 x).
rewrite transp_rel_involution.
rewrite (Hsupp1 x x1); auto.
rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_other; auto.
repeat rewrite transp_rel_refl.
rewrite transp_term_refl.
rewrite (Hsupp2 x1 x2); auto.
reflexivity.
- destruct (x1 == x); [ | destruct (x2 == x) ]; subst.
+ rewrite transp_atom_thisL.
rewrite (Hsupp1 z x2); auto.
rewrite (Hsupp1 z x); auto.
rewrite (transp_rel_swap x x2).
rewrite (transp_rel_trans (add x S)); auto.
repeat rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_thisR.
rewrite (Hsupp1 z x1); auto.
rewrite (Hsupp1 z x); auto.
rewrite (transp_rel_trans (add x S)); auto.
repeat rewrite RelCompose_RelPush_transp_term; auto.
reflexivity.
+ rewrite transp_atom_other; auto.
rewrite (Hsupp2 x1 x2); auto.
reflexivity.
Qed.
Hint Resolve RelLam_supported : supported_rel.
RelLam is contravariant on its first relation operand and
covariant in its second.
Lemma RelLam_sub S x R1 R2 S1 S2:
x `notin` S →
good_rel R1 →
supported_rel S S1 →
RelIncl S1 R1 →
RelIncl R2 S2 →
RelIncl (RelLam S x R1 R2) (RelLam S x S1 S2).
Proof.
intros Hx Hgood Hsupp H1 H2 e v [Hedom [Hegood [Hvgood H]]]. unfold RelLam in ×.
split; [| split; [| split ] ]; auto.
- intros e' Hleq v1 Hv1 v2 Heval.
specialize (H e' Hleq v1 (H1 _ _ Hv1) v2 Heval).
destruct H as [y [HyS [v' [[Heq HR1] HR2]]]].
∃ y. split; auto. ∃ v'. split.
+ split; auto. rewrite <- (Hsupp y x); auto.
simpl. rewrite transp_env_term_involution.
assert (fv v1 [<=] empty) as Hfv by eauto.
rewrite transp_term_fresh_eq.
× assumption.
× rewrite Hfv. auto.
× rewrite Hfv. auto.
+ apply H2. assumption.
Qed.
x `notin` S →
good_rel R1 →
supported_rel S S1 →
RelIncl S1 R1 →
RelIncl R2 S2 →
RelIncl (RelLam S x R1 R2) (RelLam S x S1 S2).
Proof.
intros Hx Hgood Hsupp H1 H2 e v [Hedom [Hegood [Hvgood H]]]. unfold RelLam in ×.
split; [| split; [| split ] ]; auto.
- intros e' Hleq v1 Hv1 v2 Heval.
specialize (H e' Hleq v1 (H1 _ _ Hv1) v2 Heval).
destruct H as [y [HyS [v' [[Heq HR1] HR2]]]].
∃ y. split; auto. ∃ v'. split.
+ split; auto. rewrite <- (Hsupp y x); auto.
simpl. rewrite transp_env_term_involution.
assert (fv v1 [<=] empty) as Hfv by eauto.
rewrite transp_term_fresh_eq.
× assumption.
× rewrite Hfv. auto.
× rewrite Hfv. auto.
+ apply H2. assumption.
Qed.
Definition RelLam_strong S (R1: rel (env term) term) (R2: atom → rel (env term) term)
: rel (env term) term :=
depFUN S R1 (fun v ⇒ RelClose S (fun x ⇒ RelCompose (RelPush R1 x v) (R2 x))).
: rel (env term) term :=
depFUN S R1 (fun v ⇒ RelClose S (fun x ⇒ RelCompose (RelPush R1 x v) (R2 x))).
Under suitable wellformedness conditions, the composition of
RelLamStrong with lambda_rel coincides with RelLam.
Lemma RelLam_rewrite S x R1 R2:
x `notin` S →
good_rel R1 →
supported_rel S R1 →
RelEquiv
(RelLam_strong S R1 (lambda_rel x R2))
(RelLam S x R1 R2).
Proof.
intros Hx Hgood1 Hsupp1.
apply depFUN_morphism_equiv; [ reflexivity | reflexivity |].
intros t e v. split; intro H.
- destruct H as [y [Hy [e' [[Heq H1] H2]]]]. subst.
∃ y. split; [ assumption |].
unfold lambda_rel. rewrite RelCompose_RelPush_equivariant.
rewrite transp_atom_thisR.
rewrite (Hsupp1 y x); auto.
rewrite RelCompose_RelPush_transp_term; auto.
∃ (y ¬ t ++ e). split; [ split; [ reflexivity | assumption ] | assumption ].
- destruct H as [y [Hy H]].
∃ y. split; [ assumption |].
unfold lambda_rel in H. unfold transp_rel in H. unfold in_rel at 1 in H.
rewrite <- (RelCompose_RelPush_transp_term y x) in H; auto.
rewrite <- (Hsupp1 y x) in H; auto.
destruct H as [e' [[Heq H1] H2]]. subst.
simpl in H1.
rewrite transp_env_term_involution in H1.
rewrite transp_term_involution in H1.
∃ (y ¬ t ++ e). split; [ split; [ reflexivity | assumption ] | ].
unfold lambda_rel. unfold transp_rel. unfold in_rel at 1.
rewrite transp_env_term_app. rewrite transp_env_term_one.
rewrite transp_atom_thisL.
assumption.
Qed.
Add Parametric Morphism : RelLam_strong
with signature AtomSetImpl.Equal ==> RelEquiv ==> pointwise RelEquiv ==> RelEquiv
as RelLam_strong_morphism_equiv.
Proof.
intros S1 S2 HS R1 R2 H12 R3 R4 H34.
unfold RelLam_strong.
apply depFUN_morphism_equiv; auto.
intro v.
rewrite HS. apply RelClose_morphism_equiv.
intros x Hx.
rewrite H12. rewrite (H34 x).
reflexivity.
Qed.
Add Parametric Morphism S : (RelLam_strong S)
with signature RelEquiv ==> FamilyRelEquiv S ==> RelEquiv
as RelLam_strong_morphism_family_equiv.
Proof.
intros R1 R2 H12 R3 R4 H34.
unfold RelLam_strong.
apply depFUN_morphism_equiv; auto; try reflexivity.
intro v.
apply RelClose_morphism_equiv.
intros x Hx.
rewrite H12. rewrite (H34 x Hx).
reflexivity.
Qed.
Lemma RelLam_strong_equivariant x y S R1 R2:
RelEquiv (transp_rel x y (RelLam_strong S R1 R2))
(RelLam_strong (transp_atoms x y S)
(transp_rel x y R1)
(transp_family_rel x y R2)).
Proof.
revert S R1 R2.
assert (∀ S R1 R2,
RelIncl (transp_rel x y (RelLam_strong S R1 R2))
(RelLam_strong (transp_atoms x y S)
(transp_rel x y R1)
(transp_family_rel x y R2))).
{ intros S R1 R2 e v H.
unfold RelLam_strong in ×.
rewrite depFUN_rel_equivariant in H.
destruct H as [Hedom [Hegood [Hvgood H]]].
split; [| split; [| split]]; auto.
intros e' Hleq v1 H1 v2 Heval.
specialize (H e' Hleq v1 H1 v2 Heval).
rewrite RelClose_rel_equivariant in H.
destruct H as [z [Hz H]].
∃ z. split; [ assumption |].
unfold transp_family_rel in H. unfold transp_rel in H. unfold in_rel at 1 in H.
assert (in_rel
(transp_rel x y
(RelCompose (RelPush R1 (transp_atom x y z) (transp_term x y v1))
(R2 (transp_atom x y z)))
)
e' v2) as H' by assumption.
clear H.
rewrite RelCompose_RelPush_equivariant in H'.
rewrite transp_atom_involution in H'.
rewrite transp_term_involution in H'.
assumption.
}
intros S R1 R2 e v. split; intro H0.
- apply H. assumption.
- apply (in_rel_equivariant x y) in H0.
apply H in H0. rewrite transp_atoms_involution in H0.
rewrite transp_rel_involution in H0.
rewrite transp_family_rel_involution in H0.
assumption.
Qed.
Lemma RelLam_strong_good S R1 R2:
good_rel (RelLam_strong S R1 R2).
Proof.
intros e v [Hedom [Hegood [Hvgood H]]]. split; assumption.
Qed.
Hint Resolve RelLam_strong_good : good_rel.
Lemma RelLam_strong_stable S R1 R2:
stable_rel (RelLam_strong S R1 R2).
Proof.
apply stable_depFUN.
Qed.
Hint Resolve RelLam_strong_stable : stable_rel.
Lemma RelLam_strong_supported S R1 R2 :
good_rel R1 →
supported_rel S R1 →
supported_family_rel S R2 →
supported_rel S (RelLam_strong S R1 R2).
Proof.
intros Hgood1 Hsupp1 Hsupp2.
apply depFUN_supported_rel; auto; try reflexivity.
intros x1 x2 Hx1 Hx2 v.
rewrite RelClose_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
apply RelClose_morphism_equiv.
intros z Hz. unfold transp_family_rel.
repeat rewrite RelCompose_RelPush_equivariant.
rewrite (Hsupp1 x1 x2); auto.
rewrite transp_term_involution.
rewrite transp_atom_involution.
rewrite (Hsupp2 x1 x2 Hx1 Hx2 z Hz).
reflexivity.
Qed.
Hint Resolve RelLam_strong_supported : supported_rel.
x `notin` S →
good_rel R1 →
supported_rel S R1 →
RelEquiv
(RelLam_strong S R1 (lambda_rel x R2))
(RelLam S x R1 R2).
Proof.
intros Hx Hgood1 Hsupp1.
apply depFUN_morphism_equiv; [ reflexivity | reflexivity |].
intros t e v. split; intro H.
- destruct H as [y [Hy [e' [[Heq H1] H2]]]]. subst.
∃ y. split; [ assumption |].
unfold lambda_rel. rewrite RelCompose_RelPush_equivariant.
rewrite transp_atom_thisR.
rewrite (Hsupp1 y x); auto.
rewrite RelCompose_RelPush_transp_term; auto.
∃ (y ¬ t ++ e). split; [ split; [ reflexivity | assumption ] | assumption ].
- destruct H as [y [Hy H]].
∃ y. split; [ assumption |].
unfold lambda_rel in H. unfold transp_rel in H. unfold in_rel at 1 in H.
rewrite <- (RelCompose_RelPush_transp_term y x) in H; auto.
rewrite <- (Hsupp1 y x) in H; auto.
destruct H as [e' [[Heq H1] H2]]. subst.
simpl in H1.
rewrite transp_env_term_involution in H1.
rewrite transp_term_involution in H1.
∃ (y ¬ t ++ e). split; [ split; [ reflexivity | assumption ] | ].
unfold lambda_rel. unfold transp_rel. unfold in_rel at 1.
rewrite transp_env_term_app. rewrite transp_env_term_one.
rewrite transp_atom_thisL.
assumption.
Qed.
Add Parametric Morphism : RelLam_strong
with signature AtomSetImpl.Equal ==> RelEquiv ==> pointwise RelEquiv ==> RelEquiv
as RelLam_strong_morphism_equiv.
Proof.
intros S1 S2 HS R1 R2 H12 R3 R4 H34.
unfold RelLam_strong.
apply depFUN_morphism_equiv; auto.
intro v.
rewrite HS. apply RelClose_morphism_equiv.
intros x Hx.
rewrite H12. rewrite (H34 x).
reflexivity.
Qed.
Add Parametric Morphism S : (RelLam_strong S)
with signature RelEquiv ==> FamilyRelEquiv S ==> RelEquiv
as RelLam_strong_morphism_family_equiv.
Proof.
intros R1 R2 H12 R3 R4 H34.
unfold RelLam_strong.
apply depFUN_morphism_equiv; auto; try reflexivity.
intro v.
apply RelClose_morphism_equiv.
intros x Hx.
rewrite H12. rewrite (H34 x Hx).
reflexivity.
Qed.
Lemma RelLam_strong_equivariant x y S R1 R2:
RelEquiv (transp_rel x y (RelLam_strong S R1 R2))
(RelLam_strong (transp_atoms x y S)
(transp_rel x y R1)
(transp_family_rel x y R2)).
Proof.
revert S R1 R2.
assert (∀ S R1 R2,
RelIncl (transp_rel x y (RelLam_strong S R1 R2))
(RelLam_strong (transp_atoms x y S)
(transp_rel x y R1)
(transp_family_rel x y R2))).
{ intros S R1 R2 e v H.
unfold RelLam_strong in ×.
rewrite depFUN_rel_equivariant in H.
destruct H as [Hedom [Hegood [Hvgood H]]].
split; [| split; [| split]]; auto.
intros e' Hleq v1 H1 v2 Heval.
specialize (H e' Hleq v1 H1 v2 Heval).
rewrite RelClose_rel_equivariant in H.
destruct H as [z [Hz H]].
∃ z. split; [ assumption |].
unfold transp_family_rel in H. unfold transp_rel in H. unfold in_rel at 1 in H.
assert (in_rel
(transp_rel x y
(RelCompose (RelPush R1 (transp_atom x y z) (transp_term x y v1))
(R2 (transp_atom x y z)))
)
e' v2) as H' by assumption.
clear H.
rewrite RelCompose_RelPush_equivariant in H'.
rewrite transp_atom_involution in H'.
rewrite transp_term_involution in H'.
assumption.
}
intros S R1 R2 e v. split; intro H0.
- apply H. assumption.
- apply (in_rel_equivariant x y) in H0.
apply H in H0. rewrite transp_atoms_involution in H0.
rewrite transp_rel_involution in H0.
rewrite transp_family_rel_involution in H0.
assumption.
Qed.
Lemma RelLam_strong_good S R1 R2:
good_rel (RelLam_strong S R1 R2).
Proof.
intros e v [Hedom [Hegood [Hvgood H]]]. split; assumption.
Qed.
Hint Resolve RelLam_strong_good : good_rel.
Lemma RelLam_strong_stable S R1 R2:
stable_rel (RelLam_strong S R1 R2).
Proof.
apply stable_depFUN.
Qed.
Hint Resolve RelLam_strong_stable : stable_rel.
Lemma RelLam_strong_supported S R1 R2 :
good_rel R1 →
supported_rel S R1 →
supported_family_rel S R2 →
supported_rel S (RelLam_strong S R1 R2).
Proof.
intros Hgood1 Hsupp1 Hsupp2.
apply depFUN_supported_rel; auto; try reflexivity.
intros x1 x2 Hx1 Hx2 v.
rewrite RelClose_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
apply RelClose_morphism_equiv.
intros z Hz. unfold transp_family_rel.
repeat rewrite RelCompose_RelPush_equivariant.
rewrite (Hsupp1 x1 x2); auto.
rewrite transp_term_involution.
rewrite transp_atom_involution.
rewrite (Hsupp2 x1 x2 Hx1 Hx2 z Hz).
reflexivity.
Qed.
Hint Resolve RelLam_strong_supported : supported_rel.
RelLam is more precise than the combinator we originally
considered (composition of FUN and RelLet), because of the
existential closure in RelLet.
Lemma RelLam_better_than_former_RelLam S x R1 R2 :
RelIncl
(RelLam S x R1 R2)
(FUN S R1 (RelLet S x R1 R2)).
Proof.
intros e v [Hedom [Hegood [Hvgood H]]].
split; [| split; [| split ] ]; auto.
intros e' Hleq v1 Hv1 v2 Heval.
specialize (H e' Hleq v1 Hv1 v2 Heval).
destruct H as [y [Hy H]].
∃ y. split; [ assumption |].
∃ v1. assumption.
Qed.
RelIncl
(RelLam S x R1 R2)
(FUN S R1 (RelLet S x R1 R2)).
Proof.
intros e v [Hedom [Hegood [Hvgood H]]].
split; [| split; [| split ] ]; auto.
intros e' Hleq v1 Hv1 v2 Heval.
specialize (H e' Hleq v1 Hv1 v2 Heval).
destruct H as [y [Hy H]].
∃ y. split; [ assumption |].
∃ v1. assumption.
Qed.
Renaming lemmas
Lemma RelClose_lambda_rel_var_rename S x y R:
y `notin` S →
supported_rel (add x S) R →
RelEquiv (RelClose S (lambda_rel x R))
(RelClose S (lambda_rel y (transp_rel x y R))).
Proof.
intros Hy Hsupp.
destruct (x == y); subst.
- rewrite transp_rel_refl. reflexivity.
- intros e v. split; intros [z [Hz H]]; simpl in ×.
+ ∃ z. split; auto.
destruct (z == x); [| destruct (z == y)]; subst.
× rewrite transp_env_term_refl in H. rewrite transp_term_refl in H.
rewrite transp_env_term_involution. rewrite transp_term_involution.
assumption.
× rewrite transp_env_term_refl. rewrite transp_env_term_swap.
rewrite transp_term_refl. rewrite transp_term_swap.
assumption.
× rewrite <- (Hsupp y z) in H; auto. simpl in H.
rewrite transp_env_term_compose in H.
rewrite transp_term_compose in H.
rewrite transp_atom_thisR in H.
rewrite transp_atom_other in H; auto.
rewrite (transp_env_term_swap x y).
rewrite (transp_env_term_swap z y).
rewrite (transp_term_swap x y).
rewrite (transp_term_swap z y).
assumption.
+ ∃ z. split; auto.
destruct (z == x); [| destruct (z == y)]; subst.
× rewrite transp_env_term_refl. rewrite transp_term_refl.
rewrite transp_env_term_involution in H. rewrite transp_term_involution in H.
assumption.
× rewrite transp_env_term_refl in H. rewrite transp_env_term_swap in H.
rewrite transp_term_refl in H. rewrite transp_term_swap in H.
assumption.
× rewrite <- (Hsupp y z); auto. simpl.
rewrite transp_env_term_compose.
rewrite transp_term_compose.
rewrite transp_atom_thisR.
rewrite transp_atom_other; auto.
rewrite (transp_env_term_swap y x).
rewrite (transp_env_term_swap y z).
rewrite (transp_term_swap y x).
rewrite (transp_term_swap y z).
assumption.
Qed.
y `notin` S →
supported_rel (add x S) R →
RelEquiv (RelClose S (lambda_rel x R))
(RelClose S (lambda_rel y (transp_rel x y R))).
Proof.
intros Hy Hsupp.
destruct (x == y); subst.
- rewrite transp_rel_refl. reflexivity.
- intros e v. split; intros [z [Hz H]]; simpl in ×.
+ ∃ z. split; auto.
destruct (z == x); [| destruct (z == y)]; subst.
× rewrite transp_env_term_refl in H. rewrite transp_term_refl in H.
rewrite transp_env_term_involution. rewrite transp_term_involution.
assumption.
× rewrite transp_env_term_refl. rewrite transp_env_term_swap.
rewrite transp_term_refl. rewrite transp_term_swap.
assumption.
× rewrite <- (Hsupp y z) in H; auto. simpl in H.
rewrite transp_env_term_compose in H.
rewrite transp_term_compose in H.
rewrite transp_atom_thisR in H.
rewrite transp_atom_other in H; auto.
rewrite (transp_env_term_swap x y).
rewrite (transp_env_term_swap z y).
rewrite (transp_term_swap x y).
rewrite (transp_term_swap z y).
assumption.
+ ∃ z. split; auto.
destruct (z == x); [| destruct (z == y)]; subst.
× rewrite transp_env_term_refl. rewrite transp_term_refl.
rewrite transp_env_term_involution in H. rewrite transp_term_involution in H.
assumption.
× rewrite transp_env_term_refl in H. rewrite transp_env_term_swap in H.
rewrite transp_term_refl in H. rewrite transp_term_swap in H.
assumption.
× rewrite <- (Hsupp y z); auto. simpl.
rewrite transp_env_term_compose.
rewrite transp_term_compose.
rewrite transp_atom_thisR.
rewrite transp_atom_other; auto.
rewrite (transp_env_term_swap y x).
rewrite (transp_env_term_swap y z).
rewrite (transp_term_swap y x).
rewrite (transp_term_swap y z).
assumption.
Qed.
Assume that R1 is supported by S and that R2 is supported by
add x S, where x is fresh for S. It is sound to replace the
variable x in RelLet S x R1 R2 with any variable y such that y
is fresh for S.
Lemma RelLet_bound_var_rename S x y R1 R2:
x `notin` S →
y `notin` S →
supported_rel S R1 →
supported_rel (add x S) R2 →
RelEquiv (RelLet S x R1 R2)
(RelLet S y R1 (transp_rel x y R2)).
Proof.
intros Hx Hy Hsupp1 Hsupp2.
rewrite <- (transp_rel_fresh_eq S x y (RelLet S x R1 R2)); auto with supported_rel.
rewrite RelLet_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
rewrite transp_atom_thisL.
rewrite (transp_rel_fresh_eq S x y R1); auto.
reflexivity.
Qed.
x `notin` S →
y `notin` S →
supported_rel S R1 →
supported_rel (add x S) R2 →
RelEquiv (RelLet S x R1 R2)
(RelLet S y R1 (transp_rel x y R2)).
Proof.
intros Hx Hy Hsupp1 Hsupp2.
rewrite <- (transp_rel_fresh_eq S x y (RelLet S x R1 R2)); auto with supported_rel.
rewrite RelLet_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
rewrite transp_atom_thisL.
rewrite (transp_rel_fresh_eq S x y R1); auto.
reflexivity.
Qed.
Assume that R1 is supported by S and that R2 is supported by
add x S, where x is fresh for S. It is sound to replace the
variable x in RelLam S x R1 R2 with any variable y such that y
is fresh for S.
Lemma RelLam_bound_var_rename S x y R1 R2:
x `notin` S →
y `notin` S →
good_rel R1 →
supported_rel S R1 →
supported_rel (add x S) R2 →
RelEquiv (RelLam S x R1 R2)
(RelLam S y R1 (transp_rel x y R2)).
Proof.
intros Hx Hy Hgood1 Hsupp1 Hsupp2.
rewrite <- (transp_rel_fresh_eq S x y (RelLam S x R1 R2)); auto with supported_rel.
rewrite RelLam_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
rewrite transp_atom_thisL.
rewrite (transp_rel_fresh_eq S x y R1); auto.
reflexivity.
Qed.
x `notin` S →
y `notin` S →
good_rel R1 →
supported_rel S R1 →
supported_rel (add x S) R2 →
RelEquiv (RelLam S x R1 R2)
(RelLam S y R1 (transp_rel x y R2)).
Proof.
intros Hx Hy Hgood1 Hsupp1 Hsupp2.
rewrite <- (transp_rel_fresh_eq S x y (RelLam S x R1 R2)); auto with supported_rel.
rewrite RelLam_rel_equivariant.
rewrite transp_atoms_fresh_eq; auto.
rewrite transp_atom_thisL.
rewrite (transp_rel_fresh_eq S x y R1); auto.
reflexivity.
Qed.
Lemma good_rel_RelClose_lambda_rel S x R:
good_rel R →
good_rel (RelClose S (lambda_rel x R)).
Proof.
intros Hgood e v [y [Hy Hev]].
unfold lambda_rel in Hev.
apply (good_rel_equivariant y x) in Hgood.
apply Hgood in Hev.
assumption.
Qed.
Hint Resolve good_rel_RelClose_lambda_rel : good_rel.
Lemma RelClose_lambda_rel_dom_rel S x R:
x `notin` S →
dom_rel S R →
dom_rel S (RelClose S (lambda_rel x R)).
Proof.
intros Hx Hdom e v [y [Hy Hev]].
unfold lambda_rel in Hev.
apply (dom_rel_equivariant_rel y x) in Hdom.
apply Hdom in Hev.
rewrite transp_atoms_fresh_eq in Hev; auto.
Qed.
Hint Resolve RelClose_lambda_rel_dom_rel: dom_rel.
Lemma RelLam_dom_rel S x R1 R2:
dom_rel S (RelLam S x R1 R2).
Proof.
intros e v Hev. simpl in Hev. tauto.
Qed.
Hint Resolve RelLam_dom_rel: dom_rel.