Library iris.heap_lang.substitution
From iris.heap_lang Require Export lang tactics.
From iris.prelude Require Import list.
Import heap_lang.
Arguments subst x es !e /.
Lemma closed_commute x1 es1 x2 es2 e:
Closed [] es1 →
Closed [] es2 →
x1 ≠ x2 →
subst x1 es1 (subst x2 es2 e) = subst x2 es2 (subst x1 es1 e).
Proof.
revert x1 es1 x2 es2.
induction e; simplify_eq /=; intros; auto; try (f_equal; eauto; done).
- repeat (case_decide || simpl_subst); naive_solver.
- repeat (case_decide || simpl_subst); eauto. by rewrite IHe.
- repeat (case_decide || simpl_subst); eauto; by rewrite IHe1 // IHe2 //.
Qed.
Definition subst_map := gmap string expr.
Implicit Types S : subst_map.
Definition lsubst l e :=
fold_right (λ p e', subst (p.1) (p.2) e') e l.
Definition msubst S e := lsubst (map_to_list S) e.
Lemma Permutation_Forall (A: Type) P (l l': list A) :
Permutation l l' → Forall P l → Forall P l'.
Proof.
induction 1; auto.
- intros (?&?)%Forall_cons; eauto.
- intros (?&(?&?)%Forall_cons)%Forall_cons; eauto.
Qed.
Instance Permutation_Forall' (A: Type) P: Proper (Permutation ==> iff) (@Forall A P).
Proof. intros ???. split; by apply Permutation_Forall. Qed.
Lemma exists_is_closed e: ∃ l, is_closed l e.
Proof.
induction e;
try (∃ []; eauto; done);
try (eauto; done);
try (destruct IHe1 as (l1&Hclo1);
destruct IHe2 as (l2&Hclo2);
destruct IHe3 as (l3&Hclo3);
∃ (l1 ++ l2 ++ l3);
simpl; repeat (apply andb_prop_intro; split); eapply is_closed_weaken; eauto; set_solver);
try (destruct IHe1 as (l1&Hclo1);
destruct IHe2 as (l2&Hclo2);
∃ (l1 ++ l2);
simpl; repeat (apply andb_prop_intro; split); eapply is_closed_weaken; eauto; set_solver).
- ∃ [x]. rewrite /is_closed // ?bool_decide_spec.
set_solver.
- destruct IHe as (l&Hclo). ∃ l.
simpl; eapply is_closed_weaken; eauto.
set_solver.
Qed.
Lemma is_closed_hd x l e: is_closed l e → is_closed (x :: filter (λ y, y ≠ x) l) e.
Proof.
intros; eapply is_closed_weaken; eauto.
set_unfold⇒x'. rewrite elem_of_list_filter.
case (decide (x = x')); naive_solver.
Qed.
Definition ClosedSubst l S := map_Forall (λ x e, Closed l e) S.
Lemma ClosedSubst_subseteq l S1 S2: ClosedSubst l S2 → S1 ⊆ S2 → ClosedSubst l S1.
Proof.
rewrite /ClosedSubst /map_Forall map_subseteq_spec⇒Hclo Hsub x e Hlook.
by eapply Hclo, Hsub.
Qed.
Lemma ClosedSubst_map l S: ClosedSubst l S → Forall (Closed l) (map_to_list S.*2).
Proof.
rewrite /ClosedSubst map_Forall_to_list.
remember (map_to_list S) as lS eqn:Heq.
assert (Permutation lS (map_to_list S)) as Hperm.
{ rewrite Heq; reflexivity. }
clear Heq. revert S Hperm. induction lS as [|(x,e) ?]. intros Heq; eauto.
- econstructor.
- intros S Heq. rewrite -Heq //=.
intros (?&?)%Forall_cons. econstructor; eauto.
efeed pose proof (map_to_list_insert_inv S).
{ rewrite -Heq; reflexivity. }
assert (NoDup (lS.*1)).
{ apply (NoDup_cons_12 x (lS.*1)).
replace (x :: lS.*1) with (((x, e) :: lS).*1); auto.
rewrite Heq. apply NoDup_fst_map_to_list. }
eapply IHlS.
× symmetry. by apply map_to_of_list.
× rewrite map_to_of_list; eauto.
Qed.
Lemma lsubst_app l1 l2 e:
lsubst (l1 ++ l2) e = lsubst l1 (lsubst l2 e).
Proof. induction l1; auto. by rewrite //= IHl1. Qed.
Lemma lsubst_snoc l x es e:
lsubst l (subst x es e) = lsubst (l ++ [(x, es)]) e.
Proof. induction l; auto. by rewrite //= IHl. Qed.
Lemma lsubst_cons l x es e:
subst x es (lsubst l e) = lsubst ((x,es) :: l) e.
Proof. induction l; auto. Qed.
Lemma lsubst_permutation l l' e:
Forall (Closed []) (l.*2) → NoDup (l.*1) → Permutation l l' → lsubst l e = lsubst l' e.
Proof.
intros Hclo Hnd Hperm. revert Hnd Hclo e.
induction Hperm; auto.
- inversion 1. subst=>//=. intros (?&?)%Forall_cons e. f_equal. eauto.
- inversion 1 as [|?? Hnin]. subst=>//=. intros (?&(?&?)%Forall_cons)%Forall_cons e.
apply closed_commute; eauto.
intros Heq. apply Hnin; rewrite Heq; left.
- intros. rewrite IHHperm1 //= IHHperm2 //=.
× by rewrite -Hperm1.
× by rewrite -Hperm1.
Qed.
Lemma lsubst_subst_commute l x es e:
Forall (Closed []) (l.*2) → NoDup (l.*1) →
Closed [] es → x ∉ (l.*1) →
lsubst l (subst x es e) = subst x es (lsubst l e).
Proof.
intros Hclo Hnd Hclo' Hnd'.
rewrite lsubst_cons lsubst_snoc.
symmetry. apply lsubst_permutation.
- econstructor; eauto.
- econstructor; eauto.
- apply Permutation_cons_append.
Qed.
Lemma lsubst_foldl l e:
Forall (Closed []) (l.*2) → NoDup (l.*1) →
lsubst l e = fold_left (λ e' p, subst (p.1) (p.2) e') l e.
Proof.
revert e. induction l; auto. rewrite //=. intros e (?&?)%Forall_cons (?&?)%NoDup_cons.
simpl. rewrite -lsubst_subst_commute; auto.
Qed.
Lemma lsubst_closed lS l e:
Closed l e →
(∀ x, x ∈ l → x ∉ lS.*1) →
lsubst lS e = e.
Proof.
revert l e. induction lS as [|(x, es)]; auto.
rewrite //= ⇒ l e Hclo Hnin. rewrite IHlS.
- eapply is_closed_subst; eauto.
intros Hin. eapply Hnin; eauto. by left.
- intros ???. eapply Hnin; eauto. by right.
Qed.
Lemma lsubst_closing_1 lS l2 e:
Forall (Closed []) (lS.*2) →
Closed (lS.*1 ++ l2) e →
Closed l2 (lsubst lS e).
Proof.
revert l2 e. induction lS as [|(x, es)] using rev_ind; auto.
intros l2 e HcloS Hclo.
rewrite -lsubst_snoc.
eapply IHlS.
- move: HcloS. rewrite fmap_app Forall_app. naive_solver.
- apply is_closed_subst_remove; eauto.
× move: HcloS. rewrite fmap_app Forall_app Forall_singleton.
naive_solver.
× eapply is_closed_perm; eauto.
rewrite fmap_app //= app_comm_cons.
apply Permutation_app; last reflexivity.
symmetry. apply Permutation_cons_append.
Qed.
Lemma lsubst_closing_2 lS l1 l2 e:
Forall (Closed []) (lS.*2) →
Closed l1 e →
(∀ x, x ∈ l1 → x ∈ (lS.*1) ∨ x ∈ l2) →
Closed l2 (lsubst lS e).
Proof.
intros ???.
apply lsubst_closing_1; auto.
eapply is_closed_weaken; eauto.
set_solver.
Qed.
Lemma lsubst_closing_inv_1 lS l e:
Forall (Closed []) (lS.*2) →
Closed l (lsubst lS e) →
Closed (lS.*1 ++ l) e.
Proof.
revert l e. induction lS as [|(x, es)] ; auto⇒ l2 e HcloS Hclo.
simpl in Hclo.
eapply is_closed_subst_inv_1 in Hclo; last by inversion HcloS.
eapply IHlS in Hclo; last by inversion HcloS.
eapply is_closed_perm; eauto.
rewrite fmap_cons //=. rewrite app_comm_cons.
symmetry; rewrite Permutation_cons_append -assoc //.
Qed.
Lemma lsubst_closing_inv_2 lS l e:
Forall (Closed []) (lS.*2) →
Closed (lS.*1 ++ l) (lsubst lS e) →
Closed (lS.*1 ++ l) e.
Proof.
revert l e. induction lS as [|(x, es)] ; auto⇒ l2 e HcloS Hclo.
rewrite fmap_cons //= in Hclo ×.
eapply is_closed_subst_inv_2 in Hclo; last by inversion HcloS.
eapply is_closed_perm in Hclo; last first.
{ rewrite app_comm_cons Permutation_cons_append -assoc //. }
eapply IHlS in Hclo; last by inversion HcloS.
eapply is_closed_perm; eauto.
rewrite assoc -Permutation_cons_append app_comm_cons //.
Qed.
Lemma elem_of_dom_map_to_list S x:
x ∈ (map_to_list S).*1 ↔ x ∈ dom (gset string) S.
Proof.
split.
- intros ((x'&e)&?&Helem)%elem_of_list_fmap_2.
subst; eapply elem_of_dom_2, elem_of_map_to_list. eauto.
- intros [e Heq]%elem_of_dom. eapply elem_of_list_fmap_1_alt; eauto.
× apply elem_of_map_to_list; eauto.
× eauto.
Qed.
Lemma msubst_closing_1 S l l' e:
Closed l e →
ClosedSubst [] S →
(∀ x, x ∈ l → x ∈ l' ∨ x ∈ dom (gset string) S) →
Closed l' (msubst S e).
Proof.
intros Hclo HcloS Hcontains.
rewrite /msubst. eapply lsubst_closing_2; eauto.
- by apply ClosedSubst_map.
- intros x [Hin_l|Hin_dom]%Hcontains; auto.
left. by apply elem_of_dom_map_to_list.
Qed.
Lemma msubst_closing_2 S l e:
Closed l e →
ClosedSubst [] S →
(∀ x, x ∈ l → x ∈ dom (gset string) S) →
Closed [] (msubst S e).
Proof. intros; eapply msubst_closing_1; eauto. Qed.
Lemma msubst_weaken_1 e S1 S2 l:
Closed l e →
ClosedSubst [] S2 →
S1 ⊆ S2 →
(∀ x, x ∈ (dom (gset string) S2) ∖ (dom (gset string) S1) → x ∉ l) →
msubst S1 e = msubst S2 e.
Proof.
intros Hclo HcloS2 Hcontains Hdom.
generalize (map_to_list_contains _ _ Hcontains)=>Hcontains_list.
apply contains_Permutation in Hcontains_list as (lS&Heq).
rewrite /msubst. rewrite (lsubst_permutation (map_to_list S2) (lS ++ map_to_list S1)); eauto.
- rewrite lsubst_app.
pose (l' := filter (λ x, x ∉ (dom (gset string) S1)) l).
erewrite (lsubst_closed lS l'); eauto.
× eapply (lsubst_closing_2); eauto.
** eapply ClosedSubst_map, ClosedSubst_subseteq; eauto.
** rewrite /l'⇒x. rewrite elem_of_list_filter -elem_of_dom_map_to_list.
intros Hin. case (decide (x ∈ (map_to_list S1).*1)); eauto.
× rewrite /l'⇒x. rewrite elem_of_list_filter.
intros (?&?) HinS.
eapply (Hdom x); auto. set_unfold.
split; auto. rewrite -elem_of_dom_map_to_list Heq fmap_app.
set_solver.
- by eapply ClosedSubst_map.
- apply NoDup_fst_map_to_list.
- rewrite Heq. apply Permutation_app_comm.
Qed.
Lemma msubst_weaken_2 e S1 S2:
ClosedSubst [] S2 →
S1 ⊆ S2 →
(∀ l, (∀ x, x ∈ dom (gset string) S1 → x ∈ l) → is_closed l e) →
msubst S1 e = msubst S2 e.
Proof.
intros HcloS Hsub Hclosing.
eapply (msubst_weaken_1 _ _ _ (map_to_list S1.*1)); eauto.
- eapply Hclosing⇒x. rewrite elem_of_dom.
intros (es&Hlook). apply elem_of_list_fmap.
∃ (x, es); split; auto. rewrite elem_of_map_to_list //.
- set_unfold. intros x (_&Hnin).
intros ((?&es)&?&?%elem_of_map_to_list)%elem_of_list_fmap.
subst. eapply Hnin. apply elem_of_dom; eauto.
Qed.
Lemma msubst_closed e S:
Closed [] e →
msubst S e = e.
Proof.
rewrite /msubst. intros. eapply lsubst_closed; eauto.
set_solver.
Qed.
Lemma filter_cons {A} (a: A) (l: list A) (P: A → Prop) Hdec:
P a → @filter _ _ _ P Hdec (a :: l) = a :: @filter _ _ _ P Hdec l.
Proof. induction l; rewrite /filter //= =>?; case_decide; naive_solver. Qed.
Lemma filter_cons_neg {A} (a: A) (l: list A) (P: A → Prop) Hdec:
¬ P a → @filter _ _ _ P Hdec (a :: l) = @filter _ _ _ P Hdec l.
Proof. induction l; rewrite /filter //= =>?; case_decide; naive_solver. Qed.
Lemma lsubst_unfold lS e:
lsubst lS e =
match e with
| Var y ⇒ lsubst lS (Var y)
| Rec f y e ⇒
Rec f y $ (lsubst (filter (λ p, BNamed (p.1) ≠ f ∧ BNamed (p.1) ≠ y) lS) e)
| App e1 e2 ⇒ App (lsubst lS e1) (lsubst lS e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (lsubst lS e)
| BinOp op e1 e2 ⇒ BinOp op (lsubst lS e1) (lsubst lS e2)
| If e0 e1 e2 ⇒ If (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
| Pair e1 e2 ⇒ Pair (lsubst lS e1) (lsubst lS e2)
| Letp y z e1 e2 ⇒
Letp y z (lsubst lS e1) (lsubst (filter (λ p, BNamed (p.1) ≠ y ∧ BNamed (p.1) ≠ z) lS) e2)
| Fst e ⇒ Fst (lsubst lS e)
| Snd e ⇒ Snd (lsubst lS e)
| InjL e ⇒ InjL (lsubst lS e)
| InjR e ⇒ InjR (lsubst lS e)
| Case e0 e1 e2 ⇒ Case (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
| Fork e ⇒ Fork (lsubst lS e)
| Alloc e ⇒ Alloc (lsubst lS e)
| Load e ⇒ Load (lsubst lS e)
| Store e1 e2 ⇒ Store (lsubst lS e1) (lsubst lS e2)
| CAS e0 e1 e2 ⇒ CAS (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
| Swap e0 e1 ⇒ Swap (lsubst lS e0) (lsubst lS e1)
| FAI e0 ⇒ FAI (lsubst lS e0)
end.
Proof.
destruct e; auto;
try (induction lS; auto; rewrite //= IHlS; auto; done).
- revert f x e. induction lS; auto.
intros. simpl. rewrite IHlS. simpl.
case_decide; f_equal.
× rewrite filter_cons //.
× rewrite filter_cons_neg //.
- revert x y e1 e2. induction lS; auto.
intros. simpl. rewrite IHlS. simpl.
case_decide; f_equal.
× rewrite filter_cons //.
× rewrite filter_cons_neg //.
Qed.
Definition deleteB (x: binder) S :=
match x with
| BAnon ⇒ S
| BNamed x' ⇒ delete x' S
end.
Fixpoint msubst' S (e : expr) : expr :=
match e with
| Var y ⇒
match S !! y with
| None ⇒ Var y
| Some es ⇒ es
end
| Rec f y e ⇒
Rec f y $ msubst' (deleteB f (deleteB y S)) e
| App e1 e2 ⇒ App (msubst' S e1) (msubst' S e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (msubst' S e)
| BinOp op e1 e2 ⇒ BinOp op (msubst' S e1) (msubst' S e2)
| If e0 e1 e2 ⇒ If (msubst' S e0) (msubst' S e1) (msubst' S e2)
| Pair e1 e2 ⇒ Pair (msubst' S e1) (msubst' S e2)
| Letp y z e1 e2 ⇒
Letp y z (msubst' S e1) $ msubst' (deleteB y (deleteB z S)) e2
| Fst e ⇒ Fst (msubst' S e)
| Snd e ⇒ Snd (msubst' S e)
| InjL e ⇒ InjL (msubst' S e)
| InjR e ⇒ InjR (msubst' S e)
| Case e0 e1 e2 ⇒ Case (msubst' S e0) (msubst' S e1) (msubst' S e2)
| Fork e ⇒ Fork (msubst' S e)
| Alloc e ⇒ Alloc (msubst' S e)
| Load e ⇒ Load (msubst' S e)
| Store e1 e2 ⇒ Store (msubst' S e1) (msubst' S e2)
| CAS e0 e1 e2 ⇒ CAS (msubst' S e0) (msubst' S e1) (msubst' S e2)
| Swap e0 e1 ⇒ Swap (msubst' S e0) (msubst' S e1)
| FAI e0 ⇒ FAI (msubst' S e0)
end.
Lemma filter_Permutation {A: Type} P pf (l l': list A):
Permutation l l' → Permutation (@filter _ _ _ P pf l) (@filter _ _ _ P pf l').
Proof.
induction 1; auto.
- rewrite /filter //=. case_decide; naive_solver.
- rewrite /filter //= /filter //=. do 2 case_decide; try econstructor; eauto.
- etransitivity; eauto.
Qed.
Instance filter_Permutation' A P pf: Proper (Permutation ==> Permutation) (@filter A _ _ P pf).
Proof. intros ???. by apply filter_Permutation. Qed.
Lemma deleteB_insert_ne i x e m:
BNamed i ≠ x → deleteB x (<[i := e]> m) = <[i := e]> (deleteB x m).
Proof.
destruct x; rewrite //=.
intros Hne. rewrite delete_insert_ne //. naive_solver.
Qed.
Lemma lookup_deleteB_None x m j:
deleteB x m !! j = None ↔ x = (BNamed j) ∨ m !! j = None.
Proof.
destruct x; rewrite //=. naive_solver.
rewrite lookup_delete_None; naive_solver.
Qed.
Lemma filter_deleteB x y S:
Permutation (filter (λ p, BNamed (p.1) ≠ x ∧ BNamed (p.1) ≠ y) (map_to_list S))
(map_to_list (deleteB x (deleteB y S))).
Proof.
induction S using map_ind.
- rewrite /deleteB. do 2 case_match;
rewrite //= ?delete_empty ?map_to_list_empty //=.
- rewrite map_to_list_insert // /filter //=.
case_decide as Hcase.
× rewrite deleteB_insert_ne; last naive_solver.
rewrite deleteB_insert_ne; last naive_solver.
rewrite map_to_list_insert; last first.
{ rewrite ?lookup_deleteB_None. naive_solver. }
econstructor; eauto.
× rewrite IHS. apply eq_subrelation; auto.
f_equal.
destruct x as [|s], y as [|s']; rewrite //=.
** naive_solver.
** rewrite not_and_l in Hcase ×. intros [[]|Hcase%dec_stable]; first congruence.
inversion Hcase; subst.
rewrite delete_insert // delete_notin //.
** rewrite not_and_l in Hcase ×. intros [Hcase%dec_stable|[]]; last congruence.
inversion Hcase; subst.
rewrite delete_insert // delete_notin //.
** rewrite not_and_l in Hcase ×. intros [Hcase%dec_stable|Hcase%dec_stable];
inversion Hcase; subst;
case (decide (s = s')).
*** intros →. rewrite delete_insert // ?delete_notin //.
*** symmetry. rewrite delete_commute delete_insert //.
rewrite delete_commute //. f_equal.
rewrite delete_notin //.
*** intros →. rewrite delete_insert // ?delete_notin //.
*** rewrite delete_commute delete_insert //.
rewrite delete_commute //. intros. f_equal.
rewrite delete_notin //.
Qed.
Lemma ClosedSubst_delete l S x:
ClosedSubst l S → ClosedSubst l (delete x S).
Proof.
rewrite /ClosedSubst /map_Forall //=.
intros Hclo i e.
rewrite lookup_delete_Some=>?. eapply Hclo. naive_solver.
Qed.
Lemma ClosedSubst_deleteB l S x:
ClosedSubst l S → ClosedSubst l (deleteB x S).
Proof.
destruct x as [|x]; auto.
rewrite /ClosedSubst /map_Forall //=.
intros Hclo i e.
rewrite lookup_delete_Some=>?. eapply Hclo. naive_solver.
Qed.
Lemma ClosedSubst_insert l S x es:
ClosedSubst l S → Closed l es → ClosedSubst l (<[x := es]>S).
Proof.
rewrite /ClosedSubst /map_Forall //=.
intros HcloS Hclo i e.
case (decide (x = i)).
- intros →. rewrite lookup_insert //. naive_solver.
- intros ?. rewrite lookup_insert_ne //. naive_solver.
Qed.
Lemma msubst_msubst' S e:
ClosedSubst [] S →
msubst S e = msubst' S e.
Proof.
revert S. induction e⇒ S Hclo;
try (rewrite /msubst lsubst_unfold //=; f_equal; eauto; done).
- rewrite /msubst lsubst_unfold //=.
case_match.
× assert (∃ k, Permutation (map_to_list S) (k ++ [(x, e)])) as (k&Hperm).
{ setoid_rewrite Permutation_app_comm.
apply contains_Permutation.
rewrite -(map_to_of_list [(x, e)]).
× apply map_to_list_contains. set_unfold.
apply map_subseteq_spec.
intros x' e'.
case (decide (x = x')).
** intros →. rewrite lookup_insert. inversion 1; subst; auto.
** intros Hne. rewrite lookup_insert_ne //=.
× eapply NoDup_singleton. }
erewrite lsubst_permutation; eauto using ClosedSubst_map.
** rewrite lsubst_app //= decide_True //.
apply (lsubst_closed _ []).
*** naive_solver.
*** set_solver.
** apply NoDup_fst_map_to_list.
× apply (lsubst_closed _ [x]); eauto.
** rewrite /Closed /is_closed bool_decide_spec; set_solver.
** intros x'. rewrite elem_of_dom_map_to_list.
rewrite not_elem_of_dom. set_solver.
- rewrite /msubst lsubst_unfold //=.
f_equal. etransitivity; last (eapply IHe; eauto).
× symmetry. apply lsubst_permutation.
** apply ClosedSubst_map, ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
** apply NoDup_fst_map_to_list.
** symmetry. apply filter_deleteB.
× apply ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
- rewrite /msubst lsubst_unfold //=.
f_equal; eauto. etransitivity; last (eapply IHe2; eauto).
× symmetry. apply lsubst_permutation.
** apply ClosedSubst_map, ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
** apply NoDup_fst_map_to_list.
** symmetry. apply filter_deleteB.
× apply ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
Qed.
Lemma msubst_insert_1 S x es e:
ClosedSubst [] S →
Closed [] es →
S !! x = None →
msubst (<[x := es]>S) e = subst x es (msubst S e).
Proof.
intros HcloS Hclo. rewrite /msubst.
etransitivity.
- apply lsubst_permutation.
× eapply ClosedSubst_map, ClosedSubst_insert; eauto.
× eapply NoDup_fst_map_to_list.
× by rewrite map_to_list_insert.
- auto.
Qed.
Lemma msubst_insert_2 S x es e:
ClosedSubst [] S →
Closed [] es →
msubst (<[x := es]>S) e = subst x es (msubst (delete x S) e).
Proof.
intros HcloS Hclo. rewrite -insert_delete.
apply msubst_insert_1; eauto.
- by apply ClosedSubst_delete.
- by apply lookup_delete.
Qed.
Lemma msubst_insert_3 S x es e:
ClosedSubst [] S →
Closed [] es →
msubst (<[x := es]>S) e = (msubst S (subst x es e)).
Proof.
intros HcloS Hclo. rewrite /msubst.
rewrite -insert_delete.
etransitivity.
- apply lsubst_permutation.
× eapply ClosedSubst_map, ClosedSubst_insert; eauto.
apply ClosedSubst_delete; eauto.
× eapply NoDup_fst_map_to_list.
× rewrite map_to_list_insert; first apply Permutation_cons_append.
apply lookup_delete.
- rewrite -lsubst_snoc.
destruct (exists_is_closed e) as (l&Hclo').
apply (is_closed_hd x) in Hclo'.
efeed pose proof (msubst_weaken_1) as Hweak;
try (apply is_closed_subst_remove; eauto); last first.
{ move:Hweak. rewrite /msubst. eauto. }
× intros x'. rewrite dom_delete. set_unfold.
intros (?&Hin).
apply not_and_l in Hin as [?|?%dec_stable].
** naive_solver.
** subst. rewrite elem_of_list_filter. naive_solver.
× apply delete_subseteq.
× eauto.
Qed.
Lemma msubst_closing_inv_1 S l e:
ClosedSubst [] S →
Closed l (msubst S e) →
Closed (map_to_list S.*1 ++ l) e.
Proof. intros; eapply lsubst_closing_inv_1; eauto using ClosedSubst_map. Qed.
Lemma msubst_closing_inv_2 S x l e:
ClosedSubst [] S →
Closed l (msubst S e) →
Closed (x :: l) (msubst (delete x S) e).
Proof.
intros HcloS Hclo.
case_eq (S !! x).
- intros es Heq. eapply (is_closed_subst_inv_1 _ _ _ es); first by eapply HcloS.
erewrite <-msubst_insert_2; eauto.
by rewrite insert_id.
- intros. rewrite delete_notin //.
eapply is_closed_weaken; eauto. set_solver.
Qed.
Lemma msubst_closing_inv_3 S x l e:
ClosedSubst [] S →
Closed (x :: l) (msubst S e) →
Closed (x :: l) (msubst (delete x S) e).
Proof.
intros HcloS Hclo.
case_eq (S !! x).
- intros es Heq. eapply (is_closed_subst_inv_2 _ _ _ es); first by eapply HcloS.
erewrite <-msubst_insert_2; eauto.
by rewrite insert_id.
- intros. rewrite delete_notin //.
Qed.
Lemma msubst_unfold (S: subst_map) (e : expr):
ClosedSubst [] S →
msubst S e =
match e with
| Var y ⇒
match S !! y with
| None ⇒ Var y
| Some es ⇒ es
end
| Rec f y e ⇒
Rec f y $ msubst (deleteB f (deleteB y S)) e
| App e1 e2 ⇒ App (msubst S e1) (msubst S e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (msubst S e)
| BinOp op e1 e2 ⇒ BinOp op (msubst S e1) (msubst S e2)
| If e0 e1 e2 ⇒ If (msubst S e0) (msubst S e1) (msubst S e2)
| Pair e1 e2 ⇒ Pair (msubst S e1) (msubst S e2)
| Letp y z e1 e2 ⇒
Letp y z (msubst S e1) $ msubst (deleteB y (deleteB z S)) e2
| Fst e ⇒ Fst (msubst S e)
| Snd e ⇒ Snd (msubst S e)
| InjL e ⇒ InjL (msubst S e)
| InjR e ⇒ InjR (msubst S e)
| Case e0 e1 e2 ⇒ Case (msubst S e0) (msubst S e1) (msubst S e2)
| Fork e ⇒ Fork (msubst S e)
| Alloc e ⇒ Alloc (msubst S e)
| Load e ⇒ Load (msubst S e)
| Store e1 e2 ⇒ Store (msubst S e1) (msubst S e2)
| CAS e0 e1 e2 ⇒ CAS (msubst S e0) (msubst S e1) (msubst S e2)
| Swap e0 e1 ⇒ Swap (msubst S e0) (msubst S e1)
| FAI e0 ⇒ FAI (msubst S e0)
end.
Proof.
intros. destruct e; rewrite ?msubst_msubst' //; do 2 eapply ClosedSubst_deleteB; auto.
Qed.
From iris.prelude Require Import list.
Import heap_lang.
Arguments subst x es !e /.
Lemma closed_commute x1 es1 x2 es2 e:
Closed [] es1 →
Closed [] es2 →
x1 ≠ x2 →
subst x1 es1 (subst x2 es2 e) = subst x2 es2 (subst x1 es1 e).
Proof.
revert x1 es1 x2 es2.
induction e; simplify_eq /=; intros; auto; try (f_equal; eauto; done).
- repeat (case_decide || simpl_subst); naive_solver.
- repeat (case_decide || simpl_subst); eauto. by rewrite IHe.
- repeat (case_decide || simpl_subst); eauto; by rewrite IHe1 // IHe2 //.
Qed.
Definition subst_map := gmap string expr.
Implicit Types S : subst_map.
Definition lsubst l e :=
fold_right (λ p e', subst (p.1) (p.2) e') e l.
Definition msubst S e := lsubst (map_to_list S) e.
Lemma Permutation_Forall (A: Type) P (l l': list A) :
Permutation l l' → Forall P l → Forall P l'.
Proof.
induction 1; auto.
- intros (?&?)%Forall_cons; eauto.
- intros (?&(?&?)%Forall_cons)%Forall_cons; eauto.
Qed.
Instance Permutation_Forall' (A: Type) P: Proper (Permutation ==> iff) (@Forall A P).
Proof. intros ???. split; by apply Permutation_Forall. Qed.
Lemma exists_is_closed e: ∃ l, is_closed l e.
Proof.
induction e;
try (∃ []; eauto; done);
try (eauto; done);
try (destruct IHe1 as (l1&Hclo1);
destruct IHe2 as (l2&Hclo2);
destruct IHe3 as (l3&Hclo3);
∃ (l1 ++ l2 ++ l3);
simpl; repeat (apply andb_prop_intro; split); eapply is_closed_weaken; eauto; set_solver);
try (destruct IHe1 as (l1&Hclo1);
destruct IHe2 as (l2&Hclo2);
∃ (l1 ++ l2);
simpl; repeat (apply andb_prop_intro; split); eapply is_closed_weaken; eauto; set_solver).
- ∃ [x]. rewrite /is_closed // ?bool_decide_spec.
set_solver.
- destruct IHe as (l&Hclo). ∃ l.
simpl; eapply is_closed_weaken; eauto.
set_solver.
Qed.
Lemma is_closed_hd x l e: is_closed l e → is_closed (x :: filter (λ y, y ≠ x) l) e.
Proof.
intros; eapply is_closed_weaken; eauto.
set_unfold⇒x'. rewrite elem_of_list_filter.
case (decide (x = x')); naive_solver.
Qed.
Definition ClosedSubst l S := map_Forall (λ x e, Closed l e) S.
Lemma ClosedSubst_subseteq l S1 S2: ClosedSubst l S2 → S1 ⊆ S2 → ClosedSubst l S1.
Proof.
rewrite /ClosedSubst /map_Forall map_subseteq_spec⇒Hclo Hsub x e Hlook.
by eapply Hclo, Hsub.
Qed.
Lemma ClosedSubst_map l S: ClosedSubst l S → Forall (Closed l) (map_to_list S.*2).
Proof.
rewrite /ClosedSubst map_Forall_to_list.
remember (map_to_list S) as lS eqn:Heq.
assert (Permutation lS (map_to_list S)) as Hperm.
{ rewrite Heq; reflexivity. }
clear Heq. revert S Hperm. induction lS as [|(x,e) ?]. intros Heq; eauto.
- econstructor.
- intros S Heq. rewrite -Heq //=.
intros (?&?)%Forall_cons. econstructor; eauto.
efeed pose proof (map_to_list_insert_inv S).
{ rewrite -Heq; reflexivity. }
assert (NoDup (lS.*1)).
{ apply (NoDup_cons_12 x (lS.*1)).
replace (x :: lS.*1) with (((x, e) :: lS).*1); auto.
rewrite Heq. apply NoDup_fst_map_to_list. }
eapply IHlS.
× symmetry. by apply map_to_of_list.
× rewrite map_to_of_list; eauto.
Qed.
Lemma lsubst_app l1 l2 e:
lsubst (l1 ++ l2) e = lsubst l1 (lsubst l2 e).
Proof. induction l1; auto. by rewrite //= IHl1. Qed.
Lemma lsubst_snoc l x es e:
lsubst l (subst x es e) = lsubst (l ++ [(x, es)]) e.
Proof. induction l; auto. by rewrite //= IHl. Qed.
Lemma lsubst_cons l x es e:
subst x es (lsubst l e) = lsubst ((x,es) :: l) e.
Proof. induction l; auto. Qed.
Lemma lsubst_permutation l l' e:
Forall (Closed []) (l.*2) → NoDup (l.*1) → Permutation l l' → lsubst l e = lsubst l' e.
Proof.
intros Hclo Hnd Hperm. revert Hnd Hclo e.
induction Hperm; auto.
- inversion 1. subst=>//=. intros (?&?)%Forall_cons e. f_equal. eauto.
- inversion 1 as [|?? Hnin]. subst=>//=. intros (?&(?&?)%Forall_cons)%Forall_cons e.
apply closed_commute; eauto.
intros Heq. apply Hnin; rewrite Heq; left.
- intros. rewrite IHHperm1 //= IHHperm2 //=.
× by rewrite -Hperm1.
× by rewrite -Hperm1.
Qed.
Lemma lsubst_subst_commute l x es e:
Forall (Closed []) (l.*2) → NoDup (l.*1) →
Closed [] es → x ∉ (l.*1) →
lsubst l (subst x es e) = subst x es (lsubst l e).
Proof.
intros Hclo Hnd Hclo' Hnd'.
rewrite lsubst_cons lsubst_snoc.
symmetry. apply lsubst_permutation.
- econstructor; eauto.
- econstructor; eauto.
- apply Permutation_cons_append.
Qed.
Lemma lsubst_foldl l e:
Forall (Closed []) (l.*2) → NoDup (l.*1) →
lsubst l e = fold_left (λ e' p, subst (p.1) (p.2) e') l e.
Proof.
revert e. induction l; auto. rewrite //=. intros e (?&?)%Forall_cons (?&?)%NoDup_cons.
simpl. rewrite -lsubst_subst_commute; auto.
Qed.
Lemma lsubst_closed lS l e:
Closed l e →
(∀ x, x ∈ l → x ∉ lS.*1) →
lsubst lS e = e.
Proof.
revert l e. induction lS as [|(x, es)]; auto.
rewrite //= ⇒ l e Hclo Hnin. rewrite IHlS.
- eapply is_closed_subst; eauto.
intros Hin. eapply Hnin; eauto. by left.
- intros ???. eapply Hnin; eauto. by right.
Qed.
Lemma lsubst_closing_1 lS l2 e:
Forall (Closed []) (lS.*2) →
Closed (lS.*1 ++ l2) e →
Closed l2 (lsubst lS e).
Proof.
revert l2 e. induction lS as [|(x, es)] using rev_ind; auto.
intros l2 e HcloS Hclo.
rewrite -lsubst_snoc.
eapply IHlS.
- move: HcloS. rewrite fmap_app Forall_app. naive_solver.
- apply is_closed_subst_remove; eauto.
× move: HcloS. rewrite fmap_app Forall_app Forall_singleton.
naive_solver.
× eapply is_closed_perm; eauto.
rewrite fmap_app //= app_comm_cons.
apply Permutation_app; last reflexivity.
symmetry. apply Permutation_cons_append.
Qed.
Lemma lsubst_closing_2 lS l1 l2 e:
Forall (Closed []) (lS.*2) →
Closed l1 e →
(∀ x, x ∈ l1 → x ∈ (lS.*1) ∨ x ∈ l2) →
Closed l2 (lsubst lS e).
Proof.
intros ???.
apply lsubst_closing_1; auto.
eapply is_closed_weaken; eauto.
set_solver.
Qed.
Lemma lsubst_closing_inv_1 lS l e:
Forall (Closed []) (lS.*2) →
Closed l (lsubst lS e) →
Closed (lS.*1 ++ l) e.
Proof.
revert l e. induction lS as [|(x, es)] ; auto⇒ l2 e HcloS Hclo.
simpl in Hclo.
eapply is_closed_subst_inv_1 in Hclo; last by inversion HcloS.
eapply IHlS in Hclo; last by inversion HcloS.
eapply is_closed_perm; eauto.
rewrite fmap_cons //=. rewrite app_comm_cons.
symmetry; rewrite Permutation_cons_append -assoc //.
Qed.
Lemma lsubst_closing_inv_2 lS l e:
Forall (Closed []) (lS.*2) →
Closed (lS.*1 ++ l) (lsubst lS e) →
Closed (lS.*1 ++ l) e.
Proof.
revert l e. induction lS as [|(x, es)] ; auto⇒ l2 e HcloS Hclo.
rewrite fmap_cons //= in Hclo ×.
eapply is_closed_subst_inv_2 in Hclo; last by inversion HcloS.
eapply is_closed_perm in Hclo; last first.
{ rewrite app_comm_cons Permutation_cons_append -assoc //. }
eapply IHlS in Hclo; last by inversion HcloS.
eapply is_closed_perm; eauto.
rewrite assoc -Permutation_cons_append app_comm_cons //.
Qed.
Lemma elem_of_dom_map_to_list S x:
x ∈ (map_to_list S).*1 ↔ x ∈ dom (gset string) S.
Proof.
split.
- intros ((x'&e)&?&Helem)%elem_of_list_fmap_2.
subst; eapply elem_of_dom_2, elem_of_map_to_list. eauto.
- intros [e Heq]%elem_of_dom. eapply elem_of_list_fmap_1_alt; eauto.
× apply elem_of_map_to_list; eauto.
× eauto.
Qed.
Lemma msubst_closing_1 S l l' e:
Closed l e →
ClosedSubst [] S →
(∀ x, x ∈ l → x ∈ l' ∨ x ∈ dom (gset string) S) →
Closed l' (msubst S e).
Proof.
intros Hclo HcloS Hcontains.
rewrite /msubst. eapply lsubst_closing_2; eauto.
- by apply ClosedSubst_map.
- intros x [Hin_l|Hin_dom]%Hcontains; auto.
left. by apply elem_of_dom_map_to_list.
Qed.
Lemma msubst_closing_2 S l e:
Closed l e →
ClosedSubst [] S →
(∀ x, x ∈ l → x ∈ dom (gset string) S) →
Closed [] (msubst S e).
Proof. intros; eapply msubst_closing_1; eauto. Qed.
Lemma msubst_weaken_1 e S1 S2 l:
Closed l e →
ClosedSubst [] S2 →
S1 ⊆ S2 →
(∀ x, x ∈ (dom (gset string) S2) ∖ (dom (gset string) S1) → x ∉ l) →
msubst S1 e = msubst S2 e.
Proof.
intros Hclo HcloS2 Hcontains Hdom.
generalize (map_to_list_contains _ _ Hcontains)=>Hcontains_list.
apply contains_Permutation in Hcontains_list as (lS&Heq).
rewrite /msubst. rewrite (lsubst_permutation (map_to_list S2) (lS ++ map_to_list S1)); eauto.
- rewrite lsubst_app.
pose (l' := filter (λ x, x ∉ (dom (gset string) S1)) l).
erewrite (lsubst_closed lS l'); eauto.
× eapply (lsubst_closing_2); eauto.
** eapply ClosedSubst_map, ClosedSubst_subseteq; eauto.
** rewrite /l'⇒x. rewrite elem_of_list_filter -elem_of_dom_map_to_list.
intros Hin. case (decide (x ∈ (map_to_list S1).*1)); eauto.
× rewrite /l'⇒x. rewrite elem_of_list_filter.
intros (?&?) HinS.
eapply (Hdom x); auto. set_unfold.
split; auto. rewrite -elem_of_dom_map_to_list Heq fmap_app.
set_solver.
- by eapply ClosedSubst_map.
- apply NoDup_fst_map_to_list.
- rewrite Heq. apply Permutation_app_comm.
Qed.
Lemma msubst_weaken_2 e S1 S2:
ClosedSubst [] S2 →
S1 ⊆ S2 →
(∀ l, (∀ x, x ∈ dom (gset string) S1 → x ∈ l) → is_closed l e) →
msubst S1 e = msubst S2 e.
Proof.
intros HcloS Hsub Hclosing.
eapply (msubst_weaken_1 _ _ _ (map_to_list S1.*1)); eauto.
- eapply Hclosing⇒x. rewrite elem_of_dom.
intros (es&Hlook). apply elem_of_list_fmap.
∃ (x, es); split; auto. rewrite elem_of_map_to_list //.
- set_unfold. intros x (_&Hnin).
intros ((?&es)&?&?%elem_of_map_to_list)%elem_of_list_fmap.
subst. eapply Hnin. apply elem_of_dom; eauto.
Qed.
Lemma msubst_closed e S:
Closed [] e →
msubst S e = e.
Proof.
rewrite /msubst. intros. eapply lsubst_closed; eauto.
set_solver.
Qed.
Lemma filter_cons {A} (a: A) (l: list A) (P: A → Prop) Hdec:
P a → @filter _ _ _ P Hdec (a :: l) = a :: @filter _ _ _ P Hdec l.
Proof. induction l; rewrite /filter //= =>?; case_decide; naive_solver. Qed.
Lemma filter_cons_neg {A} (a: A) (l: list A) (P: A → Prop) Hdec:
¬ P a → @filter _ _ _ P Hdec (a :: l) = @filter _ _ _ P Hdec l.
Proof. induction l; rewrite /filter //= =>?; case_decide; naive_solver. Qed.
Lemma lsubst_unfold lS e:
lsubst lS e =
match e with
| Var y ⇒ lsubst lS (Var y)
| Rec f y e ⇒
Rec f y $ (lsubst (filter (λ p, BNamed (p.1) ≠ f ∧ BNamed (p.1) ≠ y) lS) e)
| App e1 e2 ⇒ App (lsubst lS e1) (lsubst lS e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (lsubst lS e)
| BinOp op e1 e2 ⇒ BinOp op (lsubst lS e1) (lsubst lS e2)
| If e0 e1 e2 ⇒ If (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
| Pair e1 e2 ⇒ Pair (lsubst lS e1) (lsubst lS e2)
| Letp y z e1 e2 ⇒
Letp y z (lsubst lS e1) (lsubst (filter (λ p, BNamed (p.1) ≠ y ∧ BNamed (p.1) ≠ z) lS) e2)
| Fst e ⇒ Fst (lsubst lS e)
| Snd e ⇒ Snd (lsubst lS e)
| InjL e ⇒ InjL (lsubst lS e)
| InjR e ⇒ InjR (lsubst lS e)
| Case e0 e1 e2 ⇒ Case (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
| Fork e ⇒ Fork (lsubst lS e)
| Alloc e ⇒ Alloc (lsubst lS e)
| Load e ⇒ Load (lsubst lS e)
| Store e1 e2 ⇒ Store (lsubst lS e1) (lsubst lS e2)
| CAS e0 e1 e2 ⇒ CAS (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
| Swap e0 e1 ⇒ Swap (lsubst lS e0) (lsubst lS e1)
| FAI e0 ⇒ FAI (lsubst lS e0)
end.
Proof.
destruct e; auto;
try (induction lS; auto; rewrite //= IHlS; auto; done).
- revert f x e. induction lS; auto.
intros. simpl. rewrite IHlS. simpl.
case_decide; f_equal.
× rewrite filter_cons //.
× rewrite filter_cons_neg //.
- revert x y e1 e2. induction lS; auto.
intros. simpl. rewrite IHlS. simpl.
case_decide; f_equal.
× rewrite filter_cons //.
× rewrite filter_cons_neg //.
Qed.
Definition deleteB (x: binder) S :=
match x with
| BAnon ⇒ S
| BNamed x' ⇒ delete x' S
end.
Fixpoint msubst' S (e : expr) : expr :=
match e with
| Var y ⇒
match S !! y with
| None ⇒ Var y
| Some es ⇒ es
end
| Rec f y e ⇒
Rec f y $ msubst' (deleteB f (deleteB y S)) e
| App e1 e2 ⇒ App (msubst' S e1) (msubst' S e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (msubst' S e)
| BinOp op e1 e2 ⇒ BinOp op (msubst' S e1) (msubst' S e2)
| If e0 e1 e2 ⇒ If (msubst' S e0) (msubst' S e1) (msubst' S e2)
| Pair e1 e2 ⇒ Pair (msubst' S e1) (msubst' S e2)
| Letp y z e1 e2 ⇒
Letp y z (msubst' S e1) $ msubst' (deleteB y (deleteB z S)) e2
| Fst e ⇒ Fst (msubst' S e)
| Snd e ⇒ Snd (msubst' S e)
| InjL e ⇒ InjL (msubst' S e)
| InjR e ⇒ InjR (msubst' S e)
| Case e0 e1 e2 ⇒ Case (msubst' S e0) (msubst' S e1) (msubst' S e2)
| Fork e ⇒ Fork (msubst' S e)
| Alloc e ⇒ Alloc (msubst' S e)
| Load e ⇒ Load (msubst' S e)
| Store e1 e2 ⇒ Store (msubst' S e1) (msubst' S e2)
| CAS e0 e1 e2 ⇒ CAS (msubst' S e0) (msubst' S e1) (msubst' S e2)
| Swap e0 e1 ⇒ Swap (msubst' S e0) (msubst' S e1)
| FAI e0 ⇒ FAI (msubst' S e0)
end.
Lemma filter_Permutation {A: Type} P pf (l l': list A):
Permutation l l' → Permutation (@filter _ _ _ P pf l) (@filter _ _ _ P pf l').
Proof.
induction 1; auto.
- rewrite /filter //=. case_decide; naive_solver.
- rewrite /filter //= /filter //=. do 2 case_decide; try econstructor; eauto.
- etransitivity; eauto.
Qed.
Instance filter_Permutation' A P pf: Proper (Permutation ==> Permutation) (@filter A _ _ P pf).
Proof. intros ???. by apply filter_Permutation. Qed.
Lemma deleteB_insert_ne i x e m:
BNamed i ≠ x → deleteB x (<[i := e]> m) = <[i := e]> (deleteB x m).
Proof.
destruct x; rewrite //=.
intros Hne. rewrite delete_insert_ne //. naive_solver.
Qed.
Lemma lookup_deleteB_None x m j:
deleteB x m !! j = None ↔ x = (BNamed j) ∨ m !! j = None.
Proof.
destruct x; rewrite //=. naive_solver.
rewrite lookup_delete_None; naive_solver.
Qed.
Lemma filter_deleteB x y S:
Permutation (filter (λ p, BNamed (p.1) ≠ x ∧ BNamed (p.1) ≠ y) (map_to_list S))
(map_to_list (deleteB x (deleteB y S))).
Proof.
induction S using map_ind.
- rewrite /deleteB. do 2 case_match;
rewrite //= ?delete_empty ?map_to_list_empty //=.
- rewrite map_to_list_insert // /filter //=.
case_decide as Hcase.
× rewrite deleteB_insert_ne; last naive_solver.
rewrite deleteB_insert_ne; last naive_solver.
rewrite map_to_list_insert; last first.
{ rewrite ?lookup_deleteB_None. naive_solver. }
econstructor; eauto.
× rewrite IHS. apply eq_subrelation; auto.
f_equal.
destruct x as [|s], y as [|s']; rewrite //=.
** naive_solver.
** rewrite not_and_l in Hcase ×. intros [[]|Hcase%dec_stable]; first congruence.
inversion Hcase; subst.
rewrite delete_insert // delete_notin //.
** rewrite not_and_l in Hcase ×. intros [Hcase%dec_stable|[]]; last congruence.
inversion Hcase; subst.
rewrite delete_insert // delete_notin //.
** rewrite not_and_l in Hcase ×. intros [Hcase%dec_stable|Hcase%dec_stable];
inversion Hcase; subst;
case (decide (s = s')).
*** intros →. rewrite delete_insert // ?delete_notin //.
*** symmetry. rewrite delete_commute delete_insert //.
rewrite delete_commute //. f_equal.
rewrite delete_notin //.
*** intros →. rewrite delete_insert // ?delete_notin //.
*** rewrite delete_commute delete_insert //.
rewrite delete_commute //. intros. f_equal.
rewrite delete_notin //.
Qed.
Lemma ClosedSubst_delete l S x:
ClosedSubst l S → ClosedSubst l (delete x S).
Proof.
rewrite /ClosedSubst /map_Forall //=.
intros Hclo i e.
rewrite lookup_delete_Some=>?. eapply Hclo. naive_solver.
Qed.
Lemma ClosedSubst_deleteB l S x:
ClosedSubst l S → ClosedSubst l (deleteB x S).
Proof.
destruct x as [|x]; auto.
rewrite /ClosedSubst /map_Forall //=.
intros Hclo i e.
rewrite lookup_delete_Some=>?. eapply Hclo. naive_solver.
Qed.
Lemma ClosedSubst_insert l S x es:
ClosedSubst l S → Closed l es → ClosedSubst l (<[x := es]>S).
Proof.
rewrite /ClosedSubst /map_Forall //=.
intros HcloS Hclo i e.
case (decide (x = i)).
- intros →. rewrite lookup_insert //. naive_solver.
- intros ?. rewrite lookup_insert_ne //. naive_solver.
Qed.
Lemma msubst_msubst' S e:
ClosedSubst [] S →
msubst S e = msubst' S e.
Proof.
revert S. induction e⇒ S Hclo;
try (rewrite /msubst lsubst_unfold //=; f_equal; eauto; done).
- rewrite /msubst lsubst_unfold //=.
case_match.
× assert (∃ k, Permutation (map_to_list S) (k ++ [(x, e)])) as (k&Hperm).
{ setoid_rewrite Permutation_app_comm.
apply contains_Permutation.
rewrite -(map_to_of_list [(x, e)]).
× apply map_to_list_contains. set_unfold.
apply map_subseteq_spec.
intros x' e'.
case (decide (x = x')).
** intros →. rewrite lookup_insert. inversion 1; subst; auto.
** intros Hne. rewrite lookup_insert_ne //=.
× eapply NoDup_singleton. }
erewrite lsubst_permutation; eauto using ClosedSubst_map.
** rewrite lsubst_app //= decide_True //.
apply (lsubst_closed _ []).
*** naive_solver.
*** set_solver.
** apply NoDup_fst_map_to_list.
× apply (lsubst_closed _ [x]); eauto.
** rewrite /Closed /is_closed bool_decide_spec; set_solver.
** intros x'. rewrite elem_of_dom_map_to_list.
rewrite not_elem_of_dom. set_solver.
- rewrite /msubst lsubst_unfold //=.
f_equal. etransitivity; last (eapply IHe; eauto).
× symmetry. apply lsubst_permutation.
** apply ClosedSubst_map, ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
** apply NoDup_fst_map_to_list.
** symmetry. apply filter_deleteB.
× apply ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
- rewrite /msubst lsubst_unfold //=.
f_equal; eauto. etransitivity; last (eapply IHe2; eauto).
× symmetry. apply lsubst_permutation.
** apply ClosedSubst_map, ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
** apply NoDup_fst_map_to_list.
** symmetry. apply filter_deleteB.
× apply ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
Qed.
Lemma msubst_insert_1 S x es e:
ClosedSubst [] S →
Closed [] es →
S !! x = None →
msubst (<[x := es]>S) e = subst x es (msubst S e).
Proof.
intros HcloS Hclo. rewrite /msubst.
etransitivity.
- apply lsubst_permutation.
× eapply ClosedSubst_map, ClosedSubst_insert; eauto.
× eapply NoDup_fst_map_to_list.
× by rewrite map_to_list_insert.
- auto.
Qed.
Lemma msubst_insert_2 S x es e:
ClosedSubst [] S →
Closed [] es →
msubst (<[x := es]>S) e = subst x es (msubst (delete x S) e).
Proof.
intros HcloS Hclo. rewrite -insert_delete.
apply msubst_insert_1; eauto.
- by apply ClosedSubst_delete.
- by apply lookup_delete.
Qed.
Lemma msubst_insert_3 S x es e:
ClosedSubst [] S →
Closed [] es →
msubst (<[x := es]>S) e = (msubst S (subst x es e)).
Proof.
intros HcloS Hclo. rewrite /msubst.
rewrite -insert_delete.
etransitivity.
- apply lsubst_permutation.
× eapply ClosedSubst_map, ClosedSubst_insert; eauto.
apply ClosedSubst_delete; eauto.
× eapply NoDup_fst_map_to_list.
× rewrite map_to_list_insert; first apply Permutation_cons_append.
apply lookup_delete.
- rewrite -lsubst_snoc.
destruct (exists_is_closed e) as (l&Hclo').
apply (is_closed_hd x) in Hclo'.
efeed pose proof (msubst_weaken_1) as Hweak;
try (apply is_closed_subst_remove; eauto); last first.
{ move:Hweak. rewrite /msubst. eauto. }
× intros x'. rewrite dom_delete. set_unfold.
intros (?&Hin).
apply not_and_l in Hin as [?|?%dec_stable].
** naive_solver.
** subst. rewrite elem_of_list_filter. naive_solver.
× apply delete_subseteq.
× eauto.
Qed.
Lemma msubst_closing_inv_1 S l e:
ClosedSubst [] S →
Closed l (msubst S e) →
Closed (map_to_list S.*1 ++ l) e.
Proof. intros; eapply lsubst_closing_inv_1; eauto using ClosedSubst_map. Qed.
Lemma msubst_closing_inv_2 S x l e:
ClosedSubst [] S →
Closed l (msubst S e) →
Closed (x :: l) (msubst (delete x S) e).
Proof.
intros HcloS Hclo.
case_eq (S !! x).
- intros es Heq. eapply (is_closed_subst_inv_1 _ _ _ es); first by eapply HcloS.
erewrite <-msubst_insert_2; eauto.
by rewrite insert_id.
- intros. rewrite delete_notin //.
eapply is_closed_weaken; eauto. set_solver.
Qed.
Lemma msubst_closing_inv_3 S x l e:
ClosedSubst [] S →
Closed (x :: l) (msubst S e) →
Closed (x :: l) (msubst (delete x S) e).
Proof.
intros HcloS Hclo.
case_eq (S !! x).
- intros es Heq. eapply (is_closed_subst_inv_2 _ _ _ es); first by eapply HcloS.
erewrite <-msubst_insert_2; eauto.
by rewrite insert_id.
- intros. rewrite delete_notin //.
Qed.
Lemma msubst_unfold (S: subst_map) (e : expr):
ClosedSubst [] S →
msubst S e =
match e with
| Var y ⇒
match S !! y with
| None ⇒ Var y
| Some es ⇒ es
end
| Rec f y e ⇒
Rec f y $ msubst (deleteB f (deleteB y S)) e
| App e1 e2 ⇒ App (msubst S e1) (msubst S e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (msubst S e)
| BinOp op e1 e2 ⇒ BinOp op (msubst S e1) (msubst S e2)
| If e0 e1 e2 ⇒ If (msubst S e0) (msubst S e1) (msubst S e2)
| Pair e1 e2 ⇒ Pair (msubst S e1) (msubst S e2)
| Letp y z e1 e2 ⇒
Letp y z (msubst S e1) $ msubst (deleteB y (deleteB z S)) e2
| Fst e ⇒ Fst (msubst S e)
| Snd e ⇒ Snd (msubst S e)
| InjL e ⇒ InjL (msubst S e)
| InjR e ⇒ InjR (msubst S e)
| Case e0 e1 e2 ⇒ Case (msubst S e0) (msubst S e1) (msubst S e2)
| Fork e ⇒ Fork (msubst S e)
| Alloc e ⇒ Alloc (msubst S e)
| Load e ⇒ Load (msubst S e)
| Store e1 e2 ⇒ Store (msubst S e1) (msubst S e2)
| CAS e0 e1 e2 ⇒ CAS (msubst S e0) (msubst S e1) (msubst S e2)
| Swap e0 e1 ⇒ Swap (msubst S e0) (msubst S e1)
| FAI e0 ⇒ FAI (msubst S e0)
end.
Proof.
intros. destruct e; rewrite ?msubst_msubst' //; do 2 eapply ClosedSubst_deleteB; auto.
Qed.