Commit eddf490d authored by Dan Frumin's avatar Dan Frumin

Clean up the fundamental property, and generalize it to arb mask.

Following the advice of Amin Timany
generalize all the compatibility lemmas
at the same time by declaring a mask E in a Section.
parent 2f06623a
......@@ -175,3 +175,9 @@ Proof.
intros seq. subst s. by apply H.
Qed.
Lemma fmap_insert' {A B} (x : binder) (f : A B) v (vs : stringmap A) :
f <$> <[x:=v]>vs = <[x:=f v]> (f <$> vs).
Proof.
destruct x; cbn; auto.
by rewrite fmap_insert.
Qed.
......@@ -5,11 +5,14 @@ From iris.base_logic Require Export big_op.
From iris.program_logic Require Import ectx_lifting.
Section fundamental.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr.
Implicit Types Δ : listC D.
Hint Resolve to_of_val.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr.
Implicit Types Δ : listC D.
Hint Resolve to_of_val.
Section masked.
Variable (E : coPset).
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]; repeat iModIntro.
......@@ -29,7 +32,7 @@ Section fundamental.
Lemma bin_log_related_var Γ x τ :
Γ !! x = Some τ
Γ Var x log Var x : τ.
{E,E;Γ} Var x log Var x : τ.
Proof.
iIntros (? Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Hvv' ?]"; first done.
......@@ -39,41 +42,31 @@ Section fundamental.
{ rewrite lookup_fmap. by rewrite Hvv'. }
rewrite (env_subst_lookup _ x v); last first.
{ rewrite lookup_fmap. by rewrite Hvv'. }
value_case; eauto.
iModIntro. value_case; eauto.
Qed.
(* (* TODO: mvoe it to typing.v? *) *)
(* Lemma env_subst_literal (l : Literal) (vs : stringmap val) : *)
(* env_subst vs (Lit l) = Lit l. *)
(* Proof. apply env_subst_commute_0. destruct l; eauto. Qed. *)
Lemma bin_log_related_unit Γ E : {E,E;Γ} Unit log Unit : TUnit.
Lemma bin_log_related_unit Γ : {E,E;Γ} Unit log Unit : TUnit.
Proof.
iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
value_case.
iExists UnitV; eauto.
Qed.
Lemma bin_log_related_nat Γ E n : {E,E;Γ} #n n log #n n : TNat.
Lemma bin_log_related_nat Γ n : {E,E;Γ} #n n log #n n : TNat.
Proof.
iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
value_case.
iExists (#nv _); eauto.
Qed.
Lemma bin_log_related_bool Γ E b : {E,E;Γ} # b log # b : TBool.
Lemma bin_log_related_bool Γ b : {E,E;Γ} # b log # b : TBool.
Proof.
iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
value_case.
iExists (#v _); eauto.
Qed.
(* (* TODO : move it *) *)
(* Lemma env_subst_pair (e1 e2 : expr) (vs : stringmap val) : *)
(* env_subst vs (e1, e2) = (env_subst vs e1, env_subst vs e2)%E. *)
(* Proof. by apply env_subst_commute_2. Qed. *)
Lemma bin_log_related_pair Γ E e1 e2 e1' e2' τ1 τ2 :
Lemma bin_log_related_pair Γ e1 e2 e1' e2' τ1 τ2 :
{E,E;Γ} e1 log e1' : τ1 -
{E,E;Γ} e2 log e2' : τ2 -
{E,E;Γ} Pair e1 e2 log Pair e1' e2' : TProd τ1 τ2.
......@@ -88,11 +81,7 @@ Section fundamental.
iSplit; simpl; eauto. auto.
Qed.
(* (* TODO : move it *) *)
(* Lemma env_subst_fst (e1 : expr) (vs : stringmap val) : *)
(* env_subst vs (Fst e1) = Fst (env_subst vs e1)%E. *)
(* Proof. by apply env_subst_commute_1. Qed. *)
Lemma bin_log_related_fst Γ E e e' τ1 τ2 :
Lemma bin_log_related_fst Γ e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : TProd τ1 τ2 -
{E,E;Γ} Fst e log Fst e' : τ1.
......@@ -108,11 +97,7 @@ Section fundamental.
tp_fst j; eauto.
Qed.
(* (* TODO*) *)
(* Lemma env_subst_snd (e1 : expr) (vs : stringmap val) : *)
(* env_subst vs (Snd e1) = Snd (env_subst vs e1)%E. *)
(* Proof. by apply env_subst_commute_1. Qed. *)
Lemma bin_log_related_snd Γ E e e' τ1 τ2 :
Lemma bin_log_related_snd Γ e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : TProd τ1 τ2 -
{E,E;Γ} Snd e log Snd e' : τ2.
......@@ -128,206 +113,19 @@ Section fundamental.
tp_snd j; eauto.
Qed.
(* (* TODO: move this *) *)
(* Lemma env_subst_app (e1 e2 : expr) (vs : stringmap val) : *)
(* env_subst vs (App e1 e2) = App (env_subst vs e1) (env_subst vs e2). *)
(* Proof. by apply env_subst_commute_2. Qed. *)
Lemma bin_log_related_app Γ e1 e2 e1' e2' τ1 τ2 :
Γ e1 log e1' : TArrow τ1 τ2 -
Γ e2 log e2' : τ1 -
Γ App e1 e2 log App e1' e2' : τ2.
{E,E;Γ} e1 log e1' : TArrow τ1 τ2 -
{E,E;Γ} e2 log e2' : τ1 -
{E,E;Γ} App e1 e2 log App e1' e2' : τ2.
Proof.
iIntros "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn.
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" f f' "#IH1".
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" v v' "IH2".
iSpecialize ("IH1" with "IH2 Hj").
by iMod "IH1".
Qed.
(* (* TODO: move this *) *)
(* Lemma env_subst_closed (e : expr) (vs : stringmap val) : *)
(* Closed e *)
(* env_subst vs e = e. *)
(* Proof. intros ?. apply env_subst_commute_0. intros. by eapply subst_is_closed. Qed. *)
(* TODO: Why doesn't it pick up the existing intance? *)
(* Instance: EqDecision binder. *)
(* Proof. solve_decision. Qed. *)
(* Definition isInDom {A} (x : binder) (Γ : stringmap A) := *)
(* match x with *)
(* | BAnon => False *)
(* | BNamed x' => x' dom (gset string) Γ *)
(* end. *)
(* Lemma subst_p_dom_closed X vs vs' e : *)
(* Closed X e *)
(* dom (gset string) vs X *)
(* subst_p (vs' vs) e = subst_p vs' e. *)
(* Proof. *)
(* revert X vs' vs; rewrite /Closed. *)
(* induction e => X vs' vs; simplify_option_eq; *)
(* rewrite ?bool_decide_spec; move => Hc Hd; intuition eauto 20 with set_solver; intros; destruct_and?; *)
(* repeat lazymatch goal with *)
(* | [IH : context[subst_p _ ?e = subst_p _ ?e] |- _ ] => *)
(* erewrite IH; eauto; clear IH *)
(* end; eauto. *)
(* Focus 2. *)
(* - f_equal. *)
(* destruct f as [|f], x as [|x]; simpl; cbn-[union]; eauto; *)
(* simpl in *; *)
(* rewrite ?delete_union; *)
(* eapply IHe; eauto; rewrite ?dom_delete. *)
(* all: set_solver. *)
(* - assert (vs !! x = None) as Hvsx. *)
(* { apply not_elem_of_dom. *)
(* symmetry in Hd. intro. *)
(* apply (proj1 (elem_of_disjoint _ _) Hd x Hc). done. } *)
(* remember ((vs' vs) !! x) as Hvsvs'. *)
(* destruct Hvsvs'; symmetry in HeqHvsvs'. *)
(* + destruct (proj1 (lookup_union_Some_raw _ _ _ _) HeqHvsvs') as [?|[? ?]]; *)
(* simplify_map_eq. done. *)
(* + destruct (proj1 (lookup_union_None _ _ _) HeqHvsvs') as [??]. *)
(* simplify_map_eq. done. *)
(* Qed. *)
(* Lemma union_difference_delete (x : string) (v : expr) vs ws : *)
(* ({[x := v]} vs) ({[x := v]} ws) = delete x (vs ws). *)
(* Proof. *)
(* apply map_eq => i. *)
(* destruct (decide (x = i)); subst; eauto. *)
(* + rewrite lookup_delete. *)
(* rewrite lookup_difference_None. right. exists v. *)
(* erewrite lookup_union_Some_l; eauto. apply lookup_singleton. *)
(* + rewrite lookup_delete_ne; eauto. *)
(* remember ((vs ws) !! i) as Z. *)
(* destruct Z; symmetry in HeqZ. *)
(* * rewrite lookup_difference_Some. *)
(* apply lookup_difference_Some in HeqZ. *)
(* destruct HeqZ as [HZ1 HZ2]. *)
(* split. rewrite lookup_union_Some_raw. right. *)
(* split;eauto. by apply lookup_singleton_ne. *)
(* rewrite lookup_union_None. split; eauto. *)
(* by apply lookup_singleton_ne. *)
(* * rewrite lookup_difference_None. *)
(* apply lookup_difference_None in HeqZ. *)
(* destruct HeqZ as [HZ|[z HZ]]; [left|right]. *)
(* rewrite lookup_union_None. *)
(* split;eauto. by apply lookup_singleton_ne. *)
(* exists z. rewrite lookup_union_Some_raw. right. *)
(* split;eauto. by apply lookup_singleton_ne. *)
(* Qed. *)
(* Lemma subst_p_dom_closed' vs' vs'' vs e : *)
(* Closed (dom (gset string) vs') e *)
(* (* vs ⊥ₘ vs' *) *)
(* subst_p ((vs' vs) vs'') e = subst_p (vs' vs'') e. *)
(* Proof. *)
(* revert vs' vs'' vs; rewrite /Closed. *)
(* induction e => vs' vs'' vs; simplify_option_eq; *)
(* rewrite ?bool_decide_spec; move => Hc; intuition eauto 20 with set_solver; intros; destruct_and?; *)
(* repeat lazymatch goal with *)
(* | [IH : context[subst_p _ ?e = subst_p _ ?e] |- _ ] => *)
(* erewrite IH; eauto; clear IH *)
(* end; eauto. *)
(* - apply elem_of_dom in Hc. destruct Hc as [z Hc]. *)
(* remember (vs'' !! x) as P. symmetry in HeqP. *)
(* destruct P. *)
(* + assert ((vs' vs'')!! x = None) as Hv1. *)
(* { apply lookup_difference_None. *)
(* right; eauto. } *)
(* assert (((vs' vs) vs'')!! x = None) as Hv2. *)
(* { apply lookup_difference_None. *)
(* right; eauto. } *)
(* by rewrite Hv1 Hv2. *)
(* + assert ((vs' vs'')!! x = Some z) as Hv1. *)
(* { apply lookup_difference_Some. split; eauto. } *)
(* assert (((vs' vs) vs'')!! x = Some z) as Hv2. *)
(* { apply lookup_difference_Some. split; eauto. *)
(* apply lookup_union_Some_l. done. } *)
(* by rewrite Hv1 Hv2. *)
(* - f_equal. *)
(* destruct f as [|f], x as [|x]; simpl; cbn-[union]; eauto; *)
(* simpl in *; *)
(* rewrite ?delete_union; *)
(* rewrite -?(union_difference_delete _ (Lit Unit)); *)
(* rewrite ?assoc; *)
(* eapply IHe. *)
(* by rewrite ?dom_union ?dom_singleton. *)
(* by rewrite ?dom_union ?dom_singleton. *)
(* rewrite ?dom_union ?dom_singleton. *)
(* eapply Closed_mono; eauto. set_solver. *)
(* Qed. *)
(* Lemma subst_p_dom_closed'' f x vv1 vv2 vs e : *)
(* Closed (x :b: f :b: ) e *)
(* subst_p (<[f:=vv1]>(<[x:=vv2]>vs)) e = subst_p (<[f:=vv1]>{[x:=vv2]}) e. *)
(* Proof. *)
(* intros. *)
(* replace (<[f:=vv1]> (<[x:=vv2]> vs)) *)
(* with ((<[f:=vv1]>{[x:=vv2]}) vs); last first. *)
(* { destruct x, f; *)
(* rewrite ?insert_union_singleton_l; cbn; *)
(* rewrite ?left_id ?right_id. reflexivity. *)
(* rewrite insert_empty. rewrite insert_union_singleton_l. done. *)
(* rewrite insert_union_singleton_l. done. *)
(* rewrite ?insert_union_singleton_l. rewrite assoc. done. } *)
(* rewrite -(difference_empty_map (<[f:=vv1]>{[x:=vv2]} vs)). *)
(* rewrite -{2}(difference_empty_map (<[f:=vv1]>{[x:=vv2]})). *)
(* eapply subst_p_dom_closed'. *)
(* destruct f, x; cbn; eapply Closed_mono; eauto; simplify_map_eq/=. *)
(* set_solver. *)
(* rewrite dom_singleton. set_solver. *)
(* rewrite insert_empty. rewrite dom_singleton. set_solver. *)
(* rewrite dom_insert dom_singleton. set_solver. *)
(* Qed. *)
(* TODO: this goes to binder.v *)
Lemma fmap_insert' {A B} (x : binder) (f : A B) v (vs : stringmap A) :
f <$> <[x:=v]>vs = <[x:=f v]> (f <$> vs).
Proof.
destruct x; cbn; auto.
by rewrite fmap_insert.
Qed.
(* Lemma fmap_delete_binder {A B} (x : binder) (f : A B) (vs : stringmap A) : *)
(* f <$> (delete x vs) = delete x (f <$> vs). *)
(* Proof. *)
(* destruct x; cbn; auto. *)
(* by rewrite fmap_delete. *)
(* Qed. *)
(* Instance binder_partial_alter A : PartialAlter binder A (stringmap A) := *)
(* λ f k, match k with *)
(* | BAnon => id *)
(* | BNamed s => partial_alter f s *)
(* end. *)
(* Lemma insert_empty' {A} (x : binder) (v : A) : *)
(* <[x:=v]> = {[x:=v]}. *)
(* Proof. destruct x; eauto. Qed. *)
(* Lemma env_subst_closed_1 f x vv1 vv2 vs e : *)
(* Closed (x :b: f :b: ) e *)
(* env_subst (<[f:=vv1]>(<[x:=vv2]>vs)) e = env_subst (<[f:=vv1]>{[x:=vv2]}) e. *)
(* Proof. *)
(* intros Hc. unfold env_subst. *)
(* rewrite ?fmap_insert'. rewrite fmap_empty. *)
(* rewrite insert_empty'. *)
(* by eapply subst_p_dom_closed''. *)
(* Qed. *)
(* Lemma env_subst_closed vs e X : *)
(* Closed X e *)
(* X dom (gset string) vs *)
(* Closed (env_subst vs e). *)
(* Proof. *)
(* intros Hc Hdom. eapply subst_p_allClosed; eauto. *)
(* - intros i e'. rewrite lookup_fmap. *)
(* intros He'. *)
(* assert (is_Some (vs !! i)) as [v' Hv']. *)
(* { rewrite -fmap_is_Some. exists e'; eauto. } *)
(* rewrite Hv' /= in He'. injection He' => <-. *)
(* apply (val_closed _ ). *)
(* - by rewrite dom_fmap. *)
(* Qed. *)
(* TODO: move to std++ *)
Lemma difference_union_id {A : Type} `{EqDecision A, Countable A} (X Y : gset A):
X Y Y = X Y.
......@@ -349,13 +147,11 @@ Section fundamental.
apply difference_union_id.
Qed.
(* TODO: is this strong enough? *)
Lemma bin_log_related_rec (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
Closed (x :b: f :b: dom _ Γ) e
Closed (x :b: f :b: dom _ Γ) e'
(* ( specN E) *)
(<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ) e log e' : τ2) -
Γ Rec f x e log Rec f x e' : TArrow τ1 τ2.
({E,E;<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ)} e log e' : τ2) -
{E,E;Γ} Rec f x e log Rec f x e' : TArrow τ1 τ2.
Proof.
iIntros (??) "#Ht".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
......@@ -400,8 +196,8 @@ Section fundamental.
rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
rewrite difference_union_id.
set_solver.
}
value_case; eauto. rewrite decide_left; eauto.
}
iModIntro. value_case; eauto. rewrite decide_left; eauto.
iExists (RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e')). iIntros "{$Hj} !#".
iLöb as "IH". iIntros ([v v']) "#Hiv". simpl. iIntros (j' K') "Hj".
iModIntro. simpl.
......@@ -421,46 +217,46 @@ Section fundamental.
unfold env_subst in *.
erewrite !subst_p_delete; auto. (* TODO: [auto] solve the [Closed] goal, but [solve_closed] does not *)
rewrite !(delete_commute_binder _ x f).
iApply (fupd_mask_mono E); auto.
iApply ("Ht" with "Hj").
Qed.
Lemma bin_log_related_injl Γ E e e' τ1 τ2 :
Lemma bin_log_related_injl Γ e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : τ1 -
{E,E;Γ} InjL e log InjL e' : (TSum τ1 τ2).
Proof.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn.
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
value_case.
iExists (InjLV w); iFrame.
iLeft. iExists (_,_); eauto 10.
Qed.
Lemma bin_log_related_injr Γ E e e' τ1 τ2 :
Lemma bin_log_related_injr Γ e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : τ2 -
{E,E;Γ} InjR e log InjR e' : TSum τ1 τ2.
Proof.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
value_case.
iExists (InjRV w); iFrame.
iRight. iExists (_,_); eauto 10.
Qed.
Lemma bin_log_related_case Γ E e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
( specN E)
{E,E;Γ} e0 log e0' : TSum τ1 τ2 -
{E,E;Γ} e1 log e1' : TArrow τ1 τ3 -
{E,E;Γ} e2 log e2' : TArrow τ2 τ3 -
Lemma bin_log_related_case Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
specN E
{E,E;Γ} e0 log e0' : TSum τ1 τ2 -
{E,E;Γ} e1 log e1' : TArrow τ1 τ3 -
{E,E;Γ} e2 log e2' : TArrow τ2 τ3 -
{E,E;Γ} Case e0 e1 e2 log Case e0' e1' e2' : τ3.
Proof.
iIntros (?) "IH1 IH2 IH3".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
iDestruct "IH1" as "[Hiv|Hiv]";
iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq; iApply fupd_wp.
- tp_case_inl j; eauto.
......@@ -487,8 +283,8 @@ Section fundamental.
by iApply fupd_wp.
Qed.
Lemma bin_log_related_if Γ E e0 e1 e2 e0' e1' e2' τ :
(specN E)
Lemma bin_log_related_if Γ e0 e1 e2 e0' e1' e2' τ :
specN E
{E,E;Γ} e0 log e0' : TBool -
{E,E;Γ} e1 log e1' : τ -
{E,E;Γ} e2 log e2' : τ -
......@@ -496,7 +292,7 @@ Section fundamental.
Proof.
iIntros (?) "IH1 IH2 IH3".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
- tp_if_true j; eauto. iModIntro.
iApply wp_if_true. iNext. iApply fupd_wp.
......@@ -506,16 +302,16 @@ Section fundamental.
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH3" v v' "?".
Qed.
Lemma bin_log_related_nat_binop Γ E op e1 e2 e1' e2' :
(specN E)
Lemma bin_log_related_nat_binop Γ op e1 e2 e1' e2' :
specN E
{E,E;Γ} e1 log e1' : TNat -
{E,E;Γ} e2 log e2' : TNat -
{E,E;Γ} BinOp op e1 e2 log BinOp op e1' e2' : binop_res_type op.
Proof.
iIntros (?) "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
cbn. smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
iApply fupd_wp.
......@@ -526,7 +322,7 @@ Section fundamental.
try destruct lt_dec; eauto.
Qed.
Lemma bin_log_related_tlam Γ E e e' τ :
Lemma bin_log_related_tlam Γ e e' τ :
Closed (dom _ Γ) e
Closed (dom _ Γ) e'
( specN E)
......@@ -552,43 +348,43 @@ Section fundamental.
iApply (fupd_mask_mono E); eauto.
Qed.
Lemma bin_log_related_tapp Γ E e e' τ τ' :
Lemma bin_log_related_tapp Γ e e' τ τ' :
{E,E;Γ} e log e' : TForall τ -
{E,E;Γ} TApp e log TApp e' : τ.[τ'/].
Proof.
iIntros "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
iSpecialize ("IH" $! (interp τ' Δ) with "[#]"); [iPureIntro; apply _|].
iApply wp_wand_r; iSplitL.
iSpecialize ("IH" with "* Hj").
iSpecialize ("IH" with "Hj").
iApply fupd_wp. iApply "IH".
iIntros (w).
iDestruct 1 as (w') "[Hw Hiw]".
iExists _; rewrite -interp_subst; eauto.
Qed.
Lemma bin_log_related_fold Γ E e e' τ :
Lemma bin_log_related_fold Γ e e' τ :
{E,E;Γ} e log e' : τ.[(TRec τ)/] -
{E,E;Γ} Fold e log Fold e' : TRec τ.
Proof.
iIntros "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
value_case.
iExists (FoldV v'); iFrame "Hj".
rewrite fixpoint_unfold /= -interp_subst.
iAlways; iExists (_, _); eauto.
Qed.
Lemma bin_log_related_unfold Γ E e e' τ :
(specN E)
Lemma bin_log_related_unfold Γ e e' τ :
specN E
{E,E;Γ} e log e' : TRec τ -
{E,E;Γ} Unfold e log Unfold e' : τ.[(TRec τ)/].
Proof.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
rewrite /= fixpoint_unfold /=.
change (fixpoint _) with (interp (TRec τ) Δ).
iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
......@@ -598,13 +394,13 @@ Section fundamental.
iModIntro; iNext. iExists _; iFrame. by rewrite -interp_subst.
Qed.
Lemma bin_log_related_pack Γ E e e' τ τ' :
Lemma bin_log_related_pack Γ e e' τ τ' :
{E,E;Γ} e log e' : τ.[τ'/] -
{E,E;Γ} Pack e log Pack e' : TExists τ.
Proof.
iIntros "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
value_case.
iExists (PackV v'). simpl. iFrame.
iExists (v, v'). simpl; iSplit; eauto.
......@@ -612,16 +408,15 @@ Section fundamental.
iSplit; eauto. iPureIntro. apply _.
Qed.
(* TODO: can we get rid of typing information? *)
Lemma bin_log_related_unpack Γ (E : coPset) e1 e1' e2 e2' τ τ2
(Hmasked : specN E) :
Lemma bin_log_related_unpack Γ e1 e1' e2 e2' τ τ2
(Hmasked : specN E) :
{E,E;Γ} e1 log e1' : TExists τ -
{E,E;(Autosubst_Classes.subst (ren (+1)) <$> Γ)} e2 log e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2) -
{E,E;Γ} Unpack e1 e2 log Unpack e1' e2' : τ2.
Proof.
iIntros "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
iDestruct "IH1" as ([w w']) "[% #Hτi]"; simplify_eq/=.
iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=.
iApply wp_pack; eauto. iNext.
......@@ -643,8 +438,8 @@ Section fundamental.
eauto.
Qed.
Lemma bin_log_related_fork Γ E e e' :
(specN E)
Lemma bin_log_related_fork Γ e e' :
specN E
{E,E;Γ} e log e' : TUnit -
{E,E;Γ} Fork e log Fork e' : TUnit.
Proof.
......@@ -660,14 +455,14 @@ Section fundamental.
iMod "IH". iApply (wp_wand with "IH"). eauto.
Qed.
Lemma bin_log_related_alloc Γ E e e' τ :
(specN E)
Lemma bin_log_related_alloc Γ e e' τ :
specN E
{E,E;Γ} e log e' : τ -
{E,E;Γ} Alloc e log Alloc e' : Tref τ.
Proof.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn. smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
iApply fupd_wp.
tp_alloc j as k "Hk"; eauto. iModIntro.
iApply wp_atomic; eauto.
......@@ -680,15 +475,15 @@ Section fundamental.
iFrame "Hj". iExists (l, k); eauto.
Qed.
Lemma bin_log_related_load Γ E e e' τ :
(specN E)
(logN E)
Lemma bin_log_related_load Γ e e' τ :
specN E
logN E
{E,E;Γ} e log e' : (Tref τ) -
{E,E;Γ} Load e log Load e' : τ.
Proof.
iIntros (??) "IH".