Commit 090002e0 authored by Dan Frumin's avatar Dan Frumin

Use tp_ tactics in F_mu_ref_conc.fundamental_binary

parent f378dbf0
From iris_logrel.F_mu_ref_conc Require Export logrel_binary.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import rules_binary.
From iris_logrel.F_mu_ref_conc Require Import rules_binary tactics.
From iris.base_logic Require Export big_op.
Section bin_log_def.
......@@ -93,8 +93,8 @@ Section fundamental.
iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [FstCtx])); cbn.
iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
iApply wp_fst; eauto. iNext.
iMod (step_fst with "[Hs Hv]") as "Hw"; eauto.
iApply wp_fst; eauto. iNext.
tp_fst j; eauto.
Qed.
Lemma bin_log_related_snd Γ e e' τ1 τ2
......@@ -105,7 +105,7 @@ Section fundamental.
smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [SndCtx])); cbn.
iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
iApply wp_snd; eauto. iNext.
iMod (step_snd with "[Hs Hv]") as "Hw"; eauto.
tp_snd j; eauto.
Qed.
Lemma bin_log_related_injl Γ e e' τ1 τ2
......@@ -147,14 +147,14 @@ Section fundamental.
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.
tp_case_inl j; eauto.
iApply wp_case_inl; eauto using to_of_val. fold of_val. iNext.
asimpl.
erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
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.
tp_case_inr j; eauto.
iApply wp_case_inr; eauto using to_of_val. fold of_val. iNext.
asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto.
......@@ -171,9 +171,9 @@ Section fundamental.
smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]"
('IHHtyped1 _ _ _ j (K ++ [IfCtx _ _])); cbn.
iDestruct "Hiv" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
- iMod (step_if_true _ _ j K with "[-]") as "Hz"; eauto.
- tp_if_true j; eauto.
iApply wp_if_true. iNext. iApply 'IHHtyped2; eauto.
- iMod (step_if_false _ _ j K with "[-]") as "Hz"; eauto.
- tp_if_false j; eauto.
iApply wp_if_false. iNext. iApply 'IHHtyped3; eauto.
Qed.
......@@ -190,7 +190,7 @@ Section fundamental.
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.
tp_nat_binop j; eauto.
iApply wp_nat_binop. iNext. iModIntro. iExists _; iSplitL; eauto.
destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
try destruct lt_dec; eauto.
......@@ -208,7 +208,7 @@ Section fundamental.
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_rec; auto 1 using to_of_val. iNext.
iApply fupd_wp.
iMod (step_rec _ _ j' K' _ (of_val v') v' with "* [-]") as "Hz"; eauto.
tp_rec j'; eauto.
asimpl. change (Rec ?e) with (of_val (RecV e)).
erewrite !n_closed_subst_head_simpl_2 by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped _ ((_,_) :: (v,v') :: vvs)); repeat iSplit; eauto.
......@@ -237,7 +237,7 @@ Section fundamental.
iIntros "{$Hj} /= !#"; iIntros (τi ? j' K') "Hv /=".
iApply wp_tlam; iNext.
iApply fupd_wp.
iMod (step_tlam _ _ j' K' (e'.[env_subst (vvs.*2)]) with "* [-]") as "Hz"; eauto.
tp_tlam j'; eauto.
iApply 'IHHtyped; repeat iSplit; eauto. by iApply interp_env_ren.
Qed.
......@@ -282,9 +282,9 @@ Section fundamental.
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_fold; cbn; auto.
iNext; iModIntro; iExists _; iFrame "Hz". by rewrite -interp_subst.
tp_fold j; eauto.
iApply wp_fold; cbn; auto.
iNext; iModIntro. iExists _; iFrame. by rewrite -interp_subst.
Qed.
Lemma bin_log_related_fork Γ e e'
......@@ -293,7 +293,7 @@ Section fundamental.
Proof.
iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply fupd_wp.
iMod (step_fork _ _ j K with "* [-]") as (j') "[Hj Hj']"; eauto.
tp_fork j as i "Hi"; eauto.
iApply wp_fork; iNext; iSplitL "Hj".
- iExists UnitV; eauto.
- iApply wp_wand_l; iSplitR; [|iApply ('IHHtyped _ _ _ _ [])]; eauto.
......@@ -329,8 +329,7 @@ Section fundamental.
iModIntro.
iApply (wp_load with "Hw1").
iNext. iIntros "Hw1".
iMod (step_load with "[Hv Hw2]") as "[Hv Hw2]";
[solve_ndisj|by iFrame|].
tp_load j.
iMod ("Hclose" with "[Hw1 Hw2]").
{ iNext. iExists (w,w'); by iFrame. }
iModIntro. iExists w'; by iFrame.
......@@ -352,8 +351,7 @@ Section fundamental.
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|].
tp_store j; eauto.
iMod ("Hclose" with "[Hw2 Hv2]").
{ iNext; iExists (w, w'); simpl; iFrame. iFrame "Hiw". }
iExists UnitV; iFrame; auto.
......@@ -385,9 +383,7 @@ Section fundamental.
{ rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
simpl. iApply (wp_cas_suc with "Hv1"); eauto using to_of_val.
iNext. iIntros "Hv1".
iMod (step_cas_suc
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
iFrame. iFrame "Hs".
tp_cas_suc j; subst; eauto using to_of_val.
iMod ("Hclose" with "[Hv1 Hv2]").
{ iNext; iExists (_, _); by iFrame. }
iExists (#v true); iFrame; eauto.
......@@ -395,9 +391,7 @@ Section fundamental.
{ rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
simpl. iApply (wp_cas_fail with "Hv1"); eauto.
iNext. iIntros "Hv1".
iMod (step_cas_fail
with "[$Hs Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
iFrame.
tp_cas_fail j; eauto.
iMod ("Hclose" with "[Hv1 Hv2]").
{ iNext; iExists (_, _); by iFrame. }
iExists (#v false); eauto.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment