Commit 91cfdc1e authored by Robbert Krebbers's avatar Robbert Krebbers

Stop using deprecated `!#` intro pattern.

parent acd32497
......@@ -150,7 +150,7 @@ Section tests.
AllocN #n #0
{{{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}}}%I.
Proof.
iIntros (? ?) "!# _ HΦ".
iIntros (? ?) "!> _ HΦ".
wp_alloc l as "?"; first done.
by iApply "HΦ".
Qed.
......
......@@ -77,7 +77,7 @@ Section list_reverse.
Lemma rev_acc_ht hd acc xs ys :
{{ is_list hd xs is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
Proof.
iIntros "!# [Hxs Hys]".
iIntros "!> [Hxs Hys]".
iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
destruct xs as [|x xs]; iSimplifyEq.
- (* nil *) by wp_match.
......@@ -91,7 +91,7 @@ Section list_reverse.
Lemma rev_ht hd xs :
{{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
Proof.
iIntros "!# Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
iIntros "!> Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
Qed.
End list_reverse.
......@@ -204,7 +204,7 @@ Section counter_proof.
Lemma newcounter_spec :
{{ True }} newcounter #() {{ v, l, v = #l C l 0 }}.
Proof.
iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iIntros "!> _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
set (N:= nroot .@ "counter").
......@@ -216,7 +216,7 @@ Section counter_proof.
Lemma incr_spec l n :
{{ C l n }} incr #l {{ v, v = #() C l (S n) }}.
Proof.
iIntros "!# Hl /=". iLöb as "IH". wp_rec.
iIntros "!> Hl /=". iLöb as "IH". wp_rec.
iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
wp_bind (! _)%E. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c) "[Hl Hγ]".
......@@ -241,7 +241,7 @@ Section counter_proof.
Lemma read_spec l n :
{{ C l n }} read #l {{ v, m : nat, v = #m n m C l m }}.
Proof.
iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
iIntros "!> Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
iDestruct (own_valid γ (Frag n Auth c) with "[-]") as % ?%auth_frag_valid.
......
......@@ -52,7 +52,7 @@ Proof.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
wp_pures. iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
- iIntros (n) "!>". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ iMod (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). }
......@@ -60,7 +60,7 @@ Proof.
iNext; iRight; iExists n; by iFrame.
+ wp_cmpxchg_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
rewrite /one_shot_inv; eauto 10.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
- iIntros "!> /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
iAssert ( v, l v ((v = NONEV own γ Pending)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
......@@ -74,7 +74,7 @@ Proof.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto.
iModIntro. wp_pures. iIntros "!#". wp_lam.
iModIntro. wp_pures. iIntros "!>". wp_lam.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
subst; wp_match; [done|].
wp_bind (! _)%E.
......@@ -94,9 +94,9 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
}}.
Proof.
iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
- iIntros (n) "!# _". wp_apply "Hf1".
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
- iIntros (n) "!> _". wp_apply "Hf1".
- iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
Qed.
End proof.
......
......@@ -68,7 +68,7 @@ Proof.
{ iNext. iLeft. by iFrame. }
wp_pures. iModIntro. iApply ("Hf" $! _ _ (own γ (Pending (1/2)%Qp))).
iSplitL; first done. iSplit.
- iIntros (n) "!# Hγ1". wp_pures.
- iIntros (n) "!> Hγ1". wp_pures.
iApply wp_assert. wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as ">[[Hl Hγ2]|H]"; last iDestruct "H" as (m) "[Hl Hγ']".
+ iDestruct (pending_split with "[$Hγ1 $Hγ2]") as "Hγ".
......@@ -76,7 +76,7 @@ Proof.
wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
iNext; iRight; iExists n; by iFrame.
+ by iDestruct (own_valid_2 with "Hγ1 Hγ'") as %?.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
- iIntros "!> /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
iAssert ( v, l v (v = NONEV own γ (Pending (1/2)%Qp)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
......@@ -90,7 +90,7 @@ Proof.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto.
iModIntro. wp_pures. iIntros "!#". wp_lam. wp_bind (! _)%E.
iModIntro. wp_pures. iIntros "!>". wp_lam. wp_bind (! _)%E.
iInv N as "Hinv".
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
+ iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";
......@@ -111,10 +111,10 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
}}.
Proof.
iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
iExists T. iFrame "HT". iSplit.
- iIntros (n) "!# HT". wp_apply "Hf1". done.
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
- iIntros (n) "!> HT". wp_apply "Hf1". done.
- iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
Qed.
End proof.
......
......@@ -416,7 +416,7 @@ Proof. iIntros (Q R) "$ _ $". Qed.
Lemma test_iNext_iRewrite P Q : <affine> (Q P) - <affine> Q - <affine> P.
Proof.
iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
Qed.
Lemma test_iIntros_modalities `(!Absorbing P) :
......@@ -432,7 +432,7 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
Lemma test_iNext_affine P Q : <affine> (Q P) - <affine> Q - <affine> P.
Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
Lemma test_iAlways P Q R :
P - <pers> Q R - <pers> <affine> <affine> P Q.
......
......@@ -16,7 +16,7 @@ Section base_logic_tests.
( n m : nat, P1 n ((True P2 n) (n = n P3 n))) -
x = 0 x z, P3 (x + z) uPred_ownM b uPred_ownM (core b)))%I.
Proof.
iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst.
iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
{ iLeft. by iNext. }
iRight.
iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
......
......@@ -212,7 +212,7 @@ Proof.
iCombine "Hf" "HP" as "Hf".
rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
iApply (@big_sepM_impl with "Hf").
iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iIntros "!>" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]".
iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
......@@ -228,7 +228,7 @@ Proof.
[ map] γ↦b f, box_own_auth γ (E false) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
iIntros "!>" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]".
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
......
......@@ -45,7 +45,7 @@ Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof.
iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
iExists R; iFrame "HR". iApply (vs_transitive with "[$Hvs]").
iApply vs_impl. iIntros "!# HP". by iApply HPQ.
iApply vs_impl. iIntros "!> HP". by iApply HPQ.
Qed.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P.
......
......@@ -109,7 +109,7 @@ Section inv.
Lemma inv_iff N P Q : (P Q) - inv N P - inv N Q.
Proof.
iIntros "#HPQ #HI". iApply (inv_alter with "HI").
iIntros "!> !# HP". iSplitL "HP".
iIntros "!> !> HP". iSplitL "HP".
- by iApply "HPQ".
- iIntros "HQ". by iApply "HPQ".
Qed.
......@@ -169,7 +169,7 @@ Section inv.
Lemma inv_sep_l N P Q : inv N (P Q) - inv N P.
Proof.
iIntros "#HI". iApply inv_alter; eauto.
iIntros "!> !# [$ $] $".
iIntros "!> !> [$ $] $".
Qed.
Lemma inv_sep_r N P Q : inv N (P Q) - inv N Q.
......
......@@ -40,45 +40,45 @@ Global Instance vs_mono' E1 E2 : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (vs E1
Proof. solve_proper. Qed.
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
Proof. iIntros "!# []". Qed.
Proof. iIntros "!> []". Qed.
Lemma vs_timeless E P : Timeless P P ={E}=> P.
Proof. by iIntros (?) "!# > ?". Qed.
Proof. by iIntros (?) "!> > ?". Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
(P ={E1,E2}=> Q) (Q ={E2,E3}=> R) P ={E1,E3}=> R.
Proof.
iIntros "#[HvsP HvsQ] !# HP".
iIntros "#[HvsP HvsQ] !> HP".
iMod ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
Qed.
Lemma vs_reflexive E P : P ={E}=> P.
Proof. by iIntros "!# HP". Qed.
Proof. by iIntros "!> HP". Qed.
Lemma vs_impl E P Q : (P Q) P ={E}=> Q.
Proof. iIntros "#HPQ !# HP". by iApply "HPQ". Qed.
Proof. iIntros "#HPQ !> HP". by iApply "HPQ". Qed.
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) R P ={E1,E2}=> R Q.
Proof. iIntros "#Hvs !# [$ HP]". by iApply "Hvs". Qed.
Proof. iIntros "#Hvs !> [$ HP]". by iApply "Hvs". Qed.
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) P R ={E1,E2}=> Q R.
Proof. iIntros "#Hvs !# [HP $]". by iApply "Hvs". Qed.
Proof. iIntros "#Hvs !> [HP $]". by iApply "Hvs". Qed.
Lemma vs_mask_frame_r E1 E2 Ef P Q :
E1 ## Ef (P ={E1,E2}=> Q) P ={E1 Ef,E2 Ef}=> Q.
Proof.
iIntros (?) "#Hvs !# HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
iIntros (?) "#Hvs !> HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
Qed.
Lemma vs_inv N E P Q R :
N E inv N R ( R P ={E∖↑N}=> R Q) P ={E}=> Q.
Proof.
iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
iIntros (?) "#[? Hvs] !> HP". iInv N as "HR" "Hclose".
iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
by iApply "Hclose".
Qed.
Lemma vs_alloc N P : P ={N}=> inv N P.
Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
Proof. iIntros "!> HP". by iApply inv_alloc. Qed.
Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}= Q) R, R (P R ={E1,E2}=> Q).
Proof.
......
......@@ -76,7 +76,7 @@ Section definition.
constructor.
- iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
iApply (make_laterable_wand with "[] AU").
iIntros "!# AA". iApply (atomic_acc_wand with "[HP12] AA").
iIntros "!> AA". iApply (atomic_acc_wand with "[HP12] AA").
iSplit; last by eauto. iApply "HP12".
- intros ??. solve_proper.
Qed.
......@@ -255,8 +255,8 @@ Section lemmas.
rewrite atomic_update_eq {2}/atomic_update_def /=.
iIntros (Heo) "HAU".
iApply (greatest_fixpoint_coind _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
iIntros "!# *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
iApply make_laterable_wand. iIntros "!#".
iIntros "!> *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
iApply make_laterable_wand. iIntros "!>".
iApply atomic_acc_mask_weaken. done.
Qed.
......@@ -300,8 +300,8 @@ Section lemmas.
Proof.
rewrite atomic_update_eq {1}/atomic_update_def /=.
iIntros (??? HAU) "[#HP HQ]".
iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
iApply (make_laterable_intro Q with "[] HQ"). iIntros "!# >HQ".
iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> >HQ".
iApply HAU. by iFrame.
Qed.
......
......@@ -43,7 +43,7 @@ Module savedprop. Section savedprop.
Lemma saved_NA i : saved i (A i) ¬ A i.
Proof.
iIntros "#Hs !# #HA". iPoseProof "HA" as "HA'".
iIntros "#Hs !> #HA". iPoseProof "HA" as "HA'".
iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP".
iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
{ eauto. }
......@@ -194,7 +194,7 @@ Module inv. Section inv.
Lemma saved_NA i : saved i (A i) ¬A i.
Proof.
iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
iIntros "#Hi !> #HA". iPoseProof "HA" as "HA'".
iDestruct "HA'" as (P) "#[HNP Hi']".
iMod (saved_cast i (A i) P with "[]") as "HP".
{ eauto. }
......
......@@ -38,15 +38,15 @@ Section least.
Proof.
rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done.
iIntros "!#" (y) "Hy". iApply ("Hy" with "[# //]").
iIntros "!>" (y) "Hy". iApply ("Hy" with "[# //]").
Qed.
Lemma least_fixpoint_unfold_1 x :
bi_least_fixpoint F x F (bi_least_fixpoint F) x.
Proof.
iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
iIntros "!#" (z) "?". by iApply least_fixpoint_unfold_2.
iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
iIntros "!>" (z) "?". by iApply least_fixpoint_unfold_2.
Qed.
Corollary least_fixpoint_unfold x :
......@@ -67,9 +67,9 @@ Section least.
Proof.
trans ( x, bi_least_fixpoint F x - Φ x bi_least_fixpoint F x)%I.
{ iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper.
iIntros "!#" (y) "H". iSplit; first by iApply "HΦ".
iIntros "!>" (y) "H". iSplit; first by iApply "HΦ".
iApply least_fixpoint_unfold_2. iApply (bi_mono_pred with "[#] H").
by iIntros "!# * [_ ?]". }
by iIntros "!> * [_ ?]". }
by setoid_rewrite and_elim_l.
Qed.
End least.
......@@ -100,7 +100,7 @@ Section greatest.
Proof.
iDestruct 1 as (Φ) "[#Hincl HΦ]".
iApply (bi_mono_pred Φ (bi_greatest_fixpoint F) with "[#]").
- iIntros "!#" (y) "Hy". iExists Φ. auto.
- iIntros "!>" (y) "Hy". iExists Φ. auto.
- by iApply "Hincl".
Qed.
......@@ -108,8 +108,8 @@ Section greatest.
F (bi_greatest_fixpoint F) x bi_greatest_fixpoint F x.
Proof.
iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
iSplit; last done. iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
iSplit; last done. iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
iIntros "!>" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed.
Corollary greatest_fixpoint_unfold x :
......
......@@ -20,14 +20,14 @@ Section instances.
Global Instance later_laterable P : Laterable ( P).
Proof.
rewrite /Laterable. iIntros "HP". iExists P. iFrame.
iIntros "!# HP !>". done.
iIntros "!> HP !>". done.
Qed.
Global Instance timeless_laterable P :
Timeless P Laterable P.
Proof.
rewrite /Laterable. iIntros (?) "HP". iExists P%I. iFrame.
iSplitR; first by iNext. iIntros "!# >HP !>". done.
iSplitR; first by iNext. iIntros "!> >HP !>". done.
Qed.
(** This lemma is not very useful: It needs a strange assumption about
......@@ -40,7 +40,7 @@ Section instances.
Proof.
rewrite /Laterable. iIntros (???) "#HP".
iExists emp%I. iSplitL; first by iNext.
iIntros "!# >_". done.
iIntros "!> >_". done.
Qed.
Global Instance sep_laterable P Q :
......@@ -50,7 +50,7 @@ Section instances.
iDestruct (LP with "HP") as (P') "[HP' #HP]".
iDestruct (LQ with "HQ") as (Q') "[HQ' #HQ]".
iExists (P' Q')%I. iSplitL; first by iFrame.
iIntros "!# [HP' HQ']". iSplitL "HP'".
iIntros "!> [HP' HQ']". iSplitL "HP'".
- iApply "HP". done.
- iApply "HQ". done.
Qed.
......@@ -73,14 +73,14 @@ Section instances.
(Q1 - Q2) - (make_laterable Q1 - make_laterable Q2).
Proof.
iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
iExists P. iFrame. iIntros "!# HP". iApply "HQ". iApply "HQ1". done.
iExists P. iFrame. iIntros "!> HP". iApply "HQ". iApply "HQ1". done.
Qed.
Global Instance make_laterable_laterable Q :
Laterable (make_laterable Q).
Proof.
rewrite /Laterable. iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]".
iExists P. iFrame. iIntros "!# HP !>". iExists P. by iFrame.
iExists P. iFrame. iIntros "!> HP !>". iExists P. by iFrame.
Qed.
Lemma make_laterable_elim Q :
......@@ -95,7 +95,7 @@ Section instances.
Proof.
iIntros (?) "#HQ HP".
iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
iFrame. iIntros "!# HP'". iApply "HQ". iApply "HPi". done.
iFrame. iIntros "!> HP'". iApply "HQ". iApply "HPi". done.
Qed.
End instances.
......
......@@ -65,16 +65,16 @@ Global Instance ht_mono' s E :
Proof. solve_proper. Qed.
Lemma ht_alt s E P Φ e : (P WP e @ s; E {{ Φ }}) {{ P }} e @ s; E {{ Φ }}.
Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
Proof. iIntros (Hwp) "!> HP". by iApply Hwp. Qed.
Lemma ht_val s E v : {{ True }} of_val v @ s; E {{ v', v = v' }}.
Proof. iIntros "!# _". by iApply wp_value'. Qed.
Proof. iIntros "!> _". by iApply wp_value'. Qed.
Lemma ht_vs s E P P' Φ Φ' e :
(P ={E}=> P') {{ P' }} e @ s; E {{ Φ' }} ( v, Φ' v ={E}=> Φ v)
{{ P }} e @ s; E {{ Φ }}.
Proof.
iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
iIntros "(#Hvs & #Hwp & #HΦ) !> HP". iMod ("Hvs" with "HP") as "HP".
iApply wp_fupd. iApply (wp_wand with "(Hwp HP)").
iIntros (v) "Hv". by iApply "HΦ".
Qed.
......@@ -83,7 +83,7 @@ Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity s) e} :
(P ={E1,E2}=> P') {{ P' }} e @ s; E2 {{ Φ' }} ( v, Φ' v ={E2,E1}=> Φ v)
{{ P }} e @ s; E1 {{ Φ }}.
Proof.
iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
iIntros "(#Hvs & #Hwp & #HΦ) !> HP". iApply (wp_atomic _ _ E2); auto.
iMod ("Hvs" with "HP") as "HP". iModIntro.
iApply (wp_wand with "(Hwp HP)").
iIntros (v) "Hv". by iApply "HΦ".
......@@ -93,7 +93,7 @@ Lemma ht_bind `{!LanguageCtx K} s E P Φ Φ' e :
{{ P }} e @ s; E {{ Φ }} ( v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
{{ P }} K e @ s; E {{ Φ' }}.
Proof.
iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
iIntros "[#Hwpe #HwpK] !> HP". iApply wp_bind.
iApply (wp_wand with "(Hwpe HP)").
iIntros (v) "Hv". by iApply "HwpK".
Qed.
......@@ -101,30 +101,30 @@ Qed.
Lemma ht_stuck_weaken s E P Φ e :
{{ P }} e @ s; E {{ Φ }} {{ P }} e @ E ?{{ Φ }}.
Proof.
by iIntros "#Hwp !# ?"; iApply wp_stuck_weaken; iApply "Hwp".
by iIntros "#Hwp !> ?"; iApply wp_stuck_weaken; iApply "Hwp".
Qed.
Lemma ht_mask_weaken s E1 E2 P Φ e :
E1 E2 {{ P }} e @ s; E1 {{ Φ }} {{ P }} e @ s; E2 {{ Φ }}.
Proof.
iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
iIntros (?) "#Hwp !> HP". iApply (wp_mask_mono _ E1 E2); try done.
by iApply "Hwp".
Qed.
Lemma ht_frame_l s E P Φ R e :
{{ P }} e @ s; E {{ Φ }} {{ R P }} e @ s; E {{ v, R Φ v }}.
Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
Proof. iIntros "#Hwp !> [$ HP]". by iApply "Hwp". Qed.
Lemma ht_frame_r s E P Φ R e :
{{ P }} e @ s; E {{ Φ }} {{ P R }} e @ s; E {{ v, Φ v R }}.
Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
Proof. iIntros "#Hwp !> [HP $]". by iApply "Hwp". Qed.
Lemma ht_frame_step_l s E1 E2 P R1 R2 e Φ :
to_val e = None E2 E1
(R1 ={E1,E2}=> |={E2,E1}=> R2) {{ P }} e @ s; E2 {{ Φ }}
{{ R1 P }} e @ s; E1 {{ λ v, R2 Φ v }}.
Proof.
iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
iIntros (??) "[#Hvs #Hwp] !> [HR HP]".
iApply (wp_frame_step_l _ E1 E2); try done.
iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
Qed.
......@@ -134,7 +134,7 @@ Lemma ht_frame_step_r s E1 E2 P R1 R2 e Φ :
(R1 ={E1,E2}=> |={E2,E1}=> R2) {{ P }} e @ s; E2 {{ Φ }}
{{ P R1 }} e @ s; E1 {{ λ v, Φ v R2 }}.
Proof.
iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
iIntros (??) "[#Hvs #Hwp] !> [HP HR]".
iApply (wp_frame_step_r _ E1 E2); try done.
iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
Qed.
......@@ -143,7 +143,7 @@ Lemma ht_frame_step_l' s E P R e Φ :
to_val e = None
{{ P }} e @ s; E {{ Φ }} {{ R P }} e @ s; E {{ v, R Φ v }}.
Proof.
iIntros (?) "#Hwp !# [HR HP]".
iIntros (?) "#Hwp !> [HR HP]".
iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Qed.
......@@ -151,12 +151,12 @@ Lemma ht_frame_step_r' s E P Φ R e :
to_val e = None
{{ P }} e @ s; E {{ Φ }} {{ P R }} e @ s; E {{ v, Φ v R }}.
Proof.
iIntros (?) "#Hwp !# [HP HR]".
iIntros (?) "#Hwp !> [HP HR]".
iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Qed.
Lemma ht_exists (T : Type) s E (P : T iProp Σ) Φ e :
( x, {{ P x }} e @ s; E {{ Φ }}) {{ x, P x }} e @ s; E {{ Φ }}.
Proof. iIntros "#HT !# HP". iDestruct "HP" as (x) "HP". by iApply "HT". Qed.
Proof. iIntros "#HT !> HP". iDestruct "HP" as (x) "HP". by iApply "HT". Qed.
End hoare.
......@@ -43,13 +43,13 @@ Proof.
assert (NonExpansive Ψ).
{ by intros n ?? ->%(discrete_iff _ _)%leibniz_equiv. }
iApply (least_fixpoint_strong_ind _ Ψ with "[] H").
iIntros "!#" (t') "H". by iApply "IH".
iIntros "!>" (t') "H". by iApply "IH".
Qed.
Instance twptp_Permutation : Proper (() ==> ()) twptp.
Proof.
iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
iApply twptp_ind; iIntros "!#" (t1) "IH"; iIntros (t1' Ht).
iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ".
destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); try done.
iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
......@@ -59,9 +59,9 @@ Qed.
Lemma twptp_app t1 t2 : twptp t1 - twptp t2 - twptp (t1 ++ t2).
Proof.
iIntros "H1". iRevert (t2). iRevert (t1) "H1".
iApply twptp_ind; iIntros "!#" (t1) "IH1". iIntros (t2) "H2".
iApply twptp_ind; iIntros "!>" (t1) "IH1". iIntros (t2) "H2".
iRevert (t1) "IH1"; iRevert (t2) "H2".
iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1".
iApply twptp_ind; iIntros "!>" (t2) "IH2". iIntros (t1) "IH1".
rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ2 n Hstep) "Hσ1".
destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' [=Ht ?] ? Hstep]; simplify_eq/=.
apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
......@@ -74,7 +74,7 @@ Proof.
+ iMod ("IH1" with "[%] Hσ1") as (n2) "($ & Hσ & IH1 & _)"; first by econstructor.