From iris.algebra Require Import list. From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary. From iris.proofmode Require Import tactics. From iris_examples.logrel.F_mu_ref_conc Require Import rules_binary. From iris.program_logic Require Export lifting. Section bin_log_def. Context `{heapIG Σ, cfgSG Σ}. Notation D := (prodC valC valC -n> iProp Σ). Definition bin_log_related (Γ : list type) (e e' : expr) (τ : type) := ∀ Δ vvs ρ, env_Persistent Δ → spec_ctx ρ ∧ ⟦ Γ ⟧* Δ vvs ⊢ ⟦ τ ⟧ₑ Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)]). End bin_log_def. Notation "Γ ⊨ e '≤log≤' e' : τ" := (bin_log_related Γ e e' τ) (at level 74, e, e', τ at next level). 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. Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w) constr(Hv) uconstr(Hp) := iApply (wp_bind (fill [ctx])); iApply (wp_wand with "[-]"); [iApply Hp; iFrame "#"; trivial|]; iIntros (v); iDestruct 1 as (w) Hv; simpl. (* Put all quantifiers at the outer level *) Lemma bin_log_related_alt {Γ e e' τ} : Γ ⊨ e ≤log≤ e' : τ → ∀ Δ vvs ρ j K, env_Persistent Δ → spec_ctx ρ ∗ ⟦ Γ ⟧* Δ vvs ∗ j ⤇ fill K (e'.[env_subst (vvs.*2)]) ⊢ WP e.[env_subst (vvs.*1)] {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ interp τ Δ (v, v') }}. Proof. iIntros (Hlog Δ vvs ρ j K ?) "(#Hs & HΓ & Hj)". iApply (Hlog with "[HΓ] *"); iFrame; eauto. Qed. Notation "'` H" := (bin_log_related_alt H) (at level 8). Lemma bin_log_related_var Γ x τ : Γ !! x = Some τ → Γ ⊨ Var x ≤log≤ Var x : τ. Proof. iIntros (? Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Heq ?]"; first done. iDestruct "Heq" as %Heq. erewrite !env_subst_lookup; rewrite ?list_lookup_fmap ?Heq; eauto. iApply wp_value; eauto. Qed. Lemma bin_log_related_unit Γ : Γ ⊨ Unit ≤log≤ Unit : TUnit. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply wp_value. iExists UnitV; eauto. Qed. Lemma bin_log_related_nat Γ n : Γ ⊨ #n n ≤log≤ #n n : TNat. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply wp_value. iExists (#nv _); eauto. Qed. Lemma bin_log_related_bool Γ b : Γ ⊨ #♭ b ≤log≤ #♭ b : TBool. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply wp_value. iExists (#♭v _); eauto. Qed. Lemma bin_log_related_pair Γ e1 e2 e1' e2' τ1 τ2 (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : τ1) (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ2) : Γ ⊨ Pair e1 e2 ≤log≤ Pair e1' e2' : TProd τ1 τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (PairLCtx e2.[env_subst _]) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((PairLCtx e2'.[env_subst _]) :: K)). smart_wp_bind (PairRCtx v) w w' "[Hw #Hiw]" ('`IHHtyped2 _ _ _ j ((PairRCtx v') :: K)). iApply wp_value. iExists (PairV v' w'); iFrame "Hw". iExists (v, v'), (w, w'); simpl; repeat iSplit; trivial. Qed. Lemma bin_log_related_fst Γ e e' τ1 τ2 (IHHtyped : Γ ⊨ e ≤log≤ e' : TProd τ1 τ2) : Γ ⊨ Fst e ≤log≤ Fst e' : τ1. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (FstCtx :: K)); cbn. iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq. iApply wp_pure_step_later; eauto. iNext. iMod (step_fst with "[Hs Hv]") as "Hw"; eauto. iApply wp_value; eauto. Qed. Lemma bin_log_related_snd Γ e e' τ1 τ2 (IHHtyped : Γ ⊨ e ≤log≤ e' : TProd τ1 τ2) : Γ ⊨ Snd e ≤log≤ Snd e' : τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (SndCtx :: K)); cbn. iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq. iApply wp_pure_step_later; eauto. iNext. iMod (step_snd with "[Hs Hv]") as "Hw"; eauto. iApply wp_value; eauto. Qed. Lemma bin_log_related_injl Γ e e' τ1 τ2 (IHHtyped : Γ ⊨ e ≤log≤ e' : τ1) : Γ ⊨ InjL e ≤log≤ InjL e' : (TSum τ1 τ2). Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (InjLCtx :: K)); cbn. iApply wp_value. iExists (InjLV v'); iFrame "Hv". iLeft; iExists (_,_); eauto 10. Qed. Lemma bin_log_related_injr Γ e e' τ1 τ2 (IHHtyped : Γ ⊨ e ≤log≤ e' : τ2) : Γ ⊨ InjR e ≤log≤ InjR e' : TSum τ1 τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (InjRCtx :: K)); cbn. iApply wp_value. iExists (InjRV v'); iFrame "Hv". iRight; iExists (_,_); eauto 10. Qed. Lemma bin_log_related_case Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 (Hclosed2 : ∀ f, e1.[upn (S (length Γ)) f] = e1) (Hclosed3 : ∀ f, e2.[upn (S (length Γ)) f] = e2) (Hclosed2' : ∀ f, e1'.[upn (S (length Γ)) f] = e1') (Hclosed3' : ∀ f, e2'.[upn (S (length Γ)) f] = e2') (IHHtyped1 : Γ ⊨ e0 ≤log≤ e0' : TSum τ1 τ2) (IHHtyped2 : τ1 :: Γ ⊨ e1 ≤log≤ e1' : τ3) (IHHtyped3 : τ2 :: Γ ⊨ e2 ≤log≤ e2' : τ3) : Γ ⊨ Case e0 e1 e2 ≤log≤ Case e0' e1' e2' : τ3. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iDestruct (interp_env_length with "HΓ") as %?. smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((CaseCtx _ _) :: K)); cbn. iDestruct "Hiv" as "[Hiv|Hiv]"; iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq. - iApply fupd_wp. iMod (step_case_inl with "[Hs Hv]") as "Hz"; eauto. iApply wp_pure_step_later; auto. fold of_val. iModIntro. iNext. asimpl. iApply ('`IHHtyped2 _ ((w,w') :: vvs)). repeat iSplit; eauto. iApply interp_env_cons; auto. - iApply fupd_wp. iMod (step_case_inr with "[Hs Hv]") as "Hz"; eauto. iApply wp_pure_step_later; auto. fold of_val. iModIntro. iNext. asimpl. iApply ('`IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto. iApply interp_env_cons; auto. Qed. Lemma bin_log_related_if Γ e0 e1 e2 e0' e1' e2' τ (IHHtyped1 : Γ ⊨ e0 ≤log≤ e0' : TBool) (IHHtyped2 : Γ ⊨ e1 ≤log≤ e1' : τ) (IHHtyped3 : Γ ⊨ e2 ≤log≤ e2' : τ) : Γ ⊨ If e0 e1 e2 ≤log≤ If e0' e1' e2' : τ. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((IfCtx _ _) :: K)); cbn. iDestruct "Hiv" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp. - iMod (step_if_true _ _ j K with "[-]") as "Hz"; eauto. iApply wp_pure_step_later; auto. iModIntro. iNext. iApply '`IHHtyped2; eauto. - iMod (step_if_false _ _ j K with "[-]") as "Hz"; eauto. iApply wp_pure_step_later; auto. iModIntro. iNext. iApply '`IHHtyped3; eauto. Qed. Lemma bin_log_related_nat_binop Γ op e1 e2 e1' e2' (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : TNat) (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : TNat) : Γ ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : binop_res_type op. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (BinOpLCtx _ _) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((BinOpLCtx _ _) :: K)); cbn. smart_wp_bind (BinOpRCtx _ _) w w' "[Hw #Hiw]" ('`IHHtyped2 _ _ _ j ((BinOpRCtx _ _) :: K)); cbn. iDestruct "Hiv" as (n) "[% %]"; simplify_eq/=. iDestruct "Hiw" as (n') "[% %]"; simplify_eq/=. iApply fupd_wp. iMod (step_nat_binop _ _ j K with "[-]") as "Hz"; eauto. iApply wp_pure_step_later; auto. iModIntro. iNext. iApply wp_value. iExists _; iSplitL; eauto. destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec; try destruct lt_dec; eauto. Qed. Lemma bin_log_related_rec Γ (e e' : expr) τ1 τ2 (Hclosed : ∀ f, e.[upn (S (S (length Γ))) f] = e) (Hclosed' : ∀ f, e'.[upn (S (S (length Γ))) f] = e') (IHHtyped : TArrow τ1 τ2 :: τ1 :: Γ ⊨ e ≤log≤ e' : τ2) : Γ ⊨ Rec e ≤log≤ Rec e' : TArrow τ1 τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply wp_value. iExists (RecV _). iIntros "{$Hj} !#". iLöb as "IH". iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj". iDestruct (interp_env_length with "HΓ") as %?. iApply wp_pure_step_later; auto 1 using to_of_val. iNext. iApply fupd_wp. iMod (step_rec _ _ j' K' _ (of_val v') v' with "* [-]") as "Hz"; eauto. asimpl. change (Rec ?e) with (of_val (RecV e)). iApply ('`IHHtyped _ ((_,_) :: (v,v') :: vvs)); repeat iSplit; eauto. iModIntro. rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto. Qed. Lemma bin_log_related_lam Γ (e e' : expr) τ1 τ2 (Hclosed : ∀ f, e.[upn (S (length Γ)) f] = e) (Hclosed' : ∀ f, e'.[upn (S (length Γ)) f] = e') (IHHtyped : τ1 :: Γ ⊨ e ≤log≤ e' : τ2) : Γ ⊨ Lam e ≤log≤ Lam e' : TArrow τ1 τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply wp_value. iExists (LamV _). iIntros "{$Hj} !#". iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj". iDestruct (interp_env_length with "HΓ") as %?. iApply wp_pure_step_later; auto 1 using to_of_val. iNext. iApply fupd_wp. iMod (step_lam _ _ j' K' _ (of_val v') v' with "* [-]") as "Hz"; eauto. asimpl. iFrame "#". change (Lam ?e) with (of_val (LamV e)). iApply ('`IHHtyped _ ((v,v') :: vvs)); repeat iSplit; eauto. iModIntro. rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto. Qed. Lemma bin_log_related_letin Γ (e1 e2 e1' e2' : expr) τ1 τ2 (Hclosed2 : ∀ f, e2.[upn (S (length Γ)) f] = e2) (Hclosed2' : ∀ f, e2'.[upn (S (length Γ)) f] = e2') (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : τ1) (IHHtyped2 : τ1 :: Γ ⊨ e2 ≤log≤ e2' : τ2) : Γ ⊨ LetIn e1 e2 ≤log≤ LetIn e1' e2': τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iDestruct (interp_env_length with "HΓ") as %?. smart_wp_bind (LetInCtx _) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((LetInCtx _) :: K)); cbn. iMod (step_letin _ _ j K with "[-]") as "Hz"; eauto. iApply wp_pure_step_later; auto. iModIntro. asimpl. iApply ('`IHHtyped2 _ ((v, v') :: vvs)); repeat iSplit; eauto. rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto. Qed. Lemma bin_log_related_seq Γ (e1 e2 e1' e2' : expr) τ1 τ2 (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : τ1) (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ2) : Γ ⊨ Seq e1 e2 ≤log≤ Seq e1' e2': τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iDestruct (interp_env_length with "HΓ") as %?. smart_wp_bind (SeqCtx _) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((SeqCtx _) :: K)); cbn. iMod (step_seq _ _ j K with "[-]") as "Hz"; eauto. iApply wp_pure_step_later; auto. iModIntro. asimpl. iApply '`IHHtyped2; repeat iSplit; eauto. Qed. Lemma bin_log_related_app Γ e1 e2 e1' e2' τ1 τ2 (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : TArrow τ1 τ2) (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ1) : Γ ⊨ App e1 e2 ≤log≤ App e1' e2' : τ2. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (AppLCtx (e2.[env_subst (vvs.*1)])) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j (((AppLCtx (e2'.[env_subst (vvs.*2)]))) :: K)); cbn. smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]" ('`IHHtyped2 _ _ _ j ((AppRCtx v') :: K)); cbn. iApply ("Hiv" $! (w, w') with "Hiw *"); simpl; eauto. Qed. Lemma bin_log_related_tlam Γ e e' τ (IHHtyped : (subst (ren (+1)) <$> Γ) ⊨ e ≤log≤ e' : τ) : Γ ⊨ TLam e ≤log≤ TLam e' : TForall τ. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply wp_value. iExists (TLamV _). iIntros "{$Hj} /= !#"; iIntros (τi ? j' K') "Hv /=". iApply wp_pure_step_later; auto. iNext. iApply fupd_wp. iMod (step_tlam _ _ j' K' (e'.[env_subst (vvs.*2)]) with "* [-]") as "Hz"; eauto. iApply '`IHHtyped; repeat iSplit; eauto. iModIntro. rewrite interp_env_ren; auto. Qed. Lemma bin_log_related_tapp Γ e e' τ τ' (IHHtyped : Γ ⊨ e ≤log≤ e' : TForall τ) : Γ ⊨ TApp e ≤log≤ TApp e' : τ.[τ'/]. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (TAppCtx) v v' "[Hj #Hv]" ('`IHHtyped _ _ _ j (TAppCtx :: K)); cbn. iApply wp_wand_r; iSplitL. { iSpecialize ("Hv" $! (interp τ' Δ) with "[#]"); [iPureIntro; apply _|]. iApply "Hv"; eauto. } iIntros (w). iDestruct 1 as (w') "[Hw Hiw]". iExists _; rewrite -interp_subst; eauto. Qed. Lemma bin_log_related_fold Γ e e' τ (IHHtyped : Γ ⊨ e ≤log≤ e' : τ.[(TRec τ)/]) : Γ ⊨ Fold e ≤log≤ Fold e' : TRec τ. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply (wp_bind (fill [FoldCtx])); iApply wp_wand_l; iSplitR; [|iApply ('`IHHtyped _ _ _ j (FoldCtx :: K)); simpl; repeat iSplitR; trivial]. iIntros (v); iDestruct 1 as (w) "[Hv #Hiv]". iApply wp_value. iExists (FoldV w); iFrame "Hv". rewrite fixpoint_interp_rec1_eq /= -interp_subst. iAlways; iExists (_, _); eauto. Qed. Lemma bin_log_related_unfold Γ e e' τ (IHHtyped : Γ ⊨ e ≤log≤ e' : TRec τ) : Γ ⊨ Unfold e ≤log≤ Unfold e' : τ.[(TRec τ)/]. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply (wp_bind (fill [UnfoldCtx])); iApply wp_wand_l; iSplitR; [|iApply ('`IHHtyped _ _ _ j (UnfoldCtx :: K)); simpl; repeat iSplitR; trivial]. iIntros (v). iDestruct 1 as (v') "[Hw #Hiw]". rewrite /= fixpoint_interp_rec1_eq /=. change (fixpoint _) with (interp (TRec τ) Δ). iDestruct "Hiw" as ([w w']) "#[% Hiz]"; simplify_eq/=. iApply fupd_wp. iMod (step_Fold _ _ j K (of_val w') w' with "* [-]") as "Hz"; eauto. iApply wp_pure_step_later; auto. iModIntro. iApply wp_value. iNext; iExists _; iFrame "Hz". by rewrite -interp_subst. Qed. Lemma bin_log_related_fork Γ e e' (IHHtyped : Γ ⊨ e ≤log≤ e' : TUnit) : Γ ⊨ Fork e ≤log≤ Fork e' : TUnit. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". iApply fupd_wp. iMod (step_fork _ _ j K with "* [-]") as (j') "[Hj Hj']"; eauto. iApply wp_fork; iModIntro. rewrite -bi.later_sep. iNext; iSplitL "Hj". - iExists UnitV; eauto. - iApply wp_wand_l; iSplitR; [|iApply ('`IHHtyped _ _ _ _ [])]; eauto. Qed. Lemma bin_log_related_alloc Γ e e' τ (IHHtyped : Γ ⊨ e ≤log≤ e' : τ) : Γ ⊨ Alloc e ≤log≤ Alloc e' : Tref τ. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (AllocCtx :: K)). iApply fupd_wp. iMod (step_alloc _ _ j K (of_val v') v' with "* [-]") as (l') "[Hj Hl]"; eauto. iApply wp_atomic; eauto. iApply wp_alloc; eauto. do 2 iModIntro. iNext. iIntros (l) "Hl'". iMod (inv_alloc (logN .@ (l,l')) _ (∃ w : val * val, l ↦ᵢ w.1 ∗ l' ↦ₛ w.2 ∗ interp τ Δ w)%I with "[Hl Hl']") as "HN"; eauto. { iNext. iExists (v, v'); iFrame. iFrame "Hiv". } iModIntro; iExists (LocV l'). iFrame "Hj". iExists (l, l'); eauto. Qed. Lemma bin_log_related_load Γ e e' τ (IHHtyped : Γ ⊨ e ≤log≤ e' : (Tref τ)) : Γ ⊨ Load e ≤log≤ Load e' : τ. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (LoadCtx :: K)). iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=. iApply wp_atomic; eauto. iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl. (* TODO: why can we eliminate the next modality here? ↑ *) iModIntro. iApply (wp_load with "Hw1"). iNext. iIntros "Hw1". iMod (step_load with "[Hv Hw2]") as "[Hv Hw2]"; [solve_ndisj|by iFrame|]. iMod ("Hclose" with "[Hw1 Hw2]"). { iNext. iExists (w,w'); by iFrame. } iModIntro. iExists w'; by iFrame. Qed. Lemma bin_log_related_store Γ e1 e2 e1' e2' τ (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : (Tref τ)) (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ) : Γ ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (StoreLCtx _) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((StoreLCtx _) :: K)). smart_wp_bind (StoreRCtx _) w w' "[Hw #Hiw]" ('`IHHtyped2 _ _ _ j ((StoreRCtx _) :: K)). iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=. iApply wp_atomic; eauto. iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose". iModIntro. iApply (wp_store with "Hv1"); auto using to_of_val. iNext. iIntros "Hw2". iMod (step_store with "[$Hs Hw Hv2]") as "[Hw Hv2]"; eauto; [solve_ndisj | by iFrame|]. iMod ("Hclose" with "[Hw2 Hv2]"). { iNext; iExists (w, w'); simpl; iFrame. iFrame "Hiw". } iExists UnitV; iFrame; auto. Qed. Lemma bin_log_related_CAS Γ e1 e2 e3 e1' e2' e3' τ (HEqτ : EqType τ) (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : Tref τ) (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ) (IHHtyped3 : Γ ⊨ e3 ≤log≤ e3' : τ) : Γ ⊨ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' : TBool. Proof. iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=". smart_wp_bind (CasLCtx _ _) v v' "[Hv #Hiv]" ('`IHHtyped1 _ _ _ j ((CasLCtx _ _) :: K)). smart_wp_bind (CasMCtx _ _) w w' "[Hw #Hiw]" ('`IHHtyped2 _ _ _ j ((CasMCtx _ _) :: K)). smart_wp_bind (CasRCtx _ _) u u' "[Hu #Hiu]" ('`IHHtyped3 _ _ _ j ((CasRCtx _ _) :: K)). iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=. iApply wp_atomic; eauto. iMod (interp_ref_open' _ _ l l' with "[]") as (v v') "(>Hl & >Hl' & #Hiv & Heq & Hcl)"; eauto. { iExists (_, _); eauto. } iModIntro. destruct (decide (v = w)) as [|Hneq]; subst. - iApply (wp_cas_suc with "Hl"); eauto using to_of_val; eauto. iNext. iIntros "Hl". iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)". iDestruct "Heq" as %[-> _]; last trivial. iMod (step_cas_suc with "[Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj. { iFrame. iFrame "Hs". } iMod ("Hcl" with "[Hl Hl']"). { iNext; iExists (_, _); by iFrame. } iExists (#♭v true); iFrame; eauto. - iApply (wp_cas_fail with "Hl"); eauto using to_of_val; eauto. iNext. iIntros "Hl". iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)". iDestruct "Heq" as %[_ Heq]. assert (v' ≠ w'). { by intros ?; apply Hneq; rewrite Heq. } iMod (step_cas_fail with "[$Hs Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj. iFrame. iMod ("Hcl" with "[Hl Hl']"). { iNext; iExists (_, _); by iFrame. } iExists (#♭v false); eauto. Qed. Theorem binary_fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e ≤log≤ e : τ. Proof. induction 1. - by apply bin_log_related_var. - by apply bin_log_related_unit. - by apply bin_log_related_nat. - by apply bin_log_related_bool. - apply bin_log_related_nat_binop; eauto. - apply bin_log_related_pair; eauto. - eapply bin_log_related_fst; eauto. - eapply bin_log_related_snd; eauto. - eapply bin_log_related_injl; eauto. - eapply bin_log_related_injr; eauto. - eapply bin_log_related_case; eauto; match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. - eapply bin_log_related_if; eauto. - eapply bin_log_related_rec; eauto; match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. - eapply bin_log_related_lam; eauto; match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. - eapply bin_log_related_letin; eauto; match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. - eapply bin_log_related_seq; eauto. - eapply bin_log_related_app; eauto. - eapply bin_log_related_tlam; eauto with typeclass_instances. - eapply bin_log_related_tapp; eauto. - eapply bin_log_related_fold; eauto. - eapply bin_log_related_unfold; eauto. - eapply bin_log_related_fork; eauto. - eapply bin_log_related_alloc; eauto. - eapply bin_log_related_load; eauto. - eapply bin_log_related_store; eauto. - eapply bin_log_related_CAS; eauto. Qed. End fundamental.