diff --git a/theories/examples/counter.v b/theories/examples/counter.v index fa9d1a01adf789a4b3323aef5d1bfda8274e35c3..1829806088c246cf2886a134a3d36b4a776d8228 100644 --- a/theories/examples/counter.v +++ b/theories/examples/counter.v @@ -157,9 +157,8 @@ Section CG_Counter. iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro. iExists #n. iFrame. iNext. iIntros "Hx". iDestruct "Hrev" as "[Hrev _]". - iApply fupd_logrel. - iMod ("Hrev" with "[HR Hx]"). - { iExists _. iFrame. } iModIntro. simpl. + iMod ("Hrev" with "[HR Hx]") as "_". + { iExists _. iFrame. } simpl. rel_rec_l. rel_op_l. rel_cas_l_atomic. @@ -286,7 +285,7 @@ Section CG_Counter. iApply (bin_log_related_pair _ with "[]"). - rel_rec_l. - unfold CG_increment. unlock. + unlock CG_increment. rel_rec_r. rel_rec_r. replace (λ: <>, acquire # l ;; #cnt' <- #1 + (! #cnt');; release # l)%E diff --git a/theories/examples/generative.v b/theories/examples/generative.v index ac9ad509c725f390f12bee9bea2cb10ffc834193..24fe9951ab999ead394464c30d8e99c58f1bf102 100644 --- a/theories/examples/generative.v +++ b/theories/examples/generative.v @@ -68,13 +68,11 @@ Section namegen_refinement. iIntros (Δ). unlock nameGenTy nameGen1 nameGen2. rel_alloc_r as c "Hc". rel_let_r. - iApply fupd_logrel'. iMod alloc_empty_bij as (γ) "HB". pose (N:=logrelN.@"ng"). iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv". { iNext. iExists 0, ∅. iFrame. by rewrite big_sepS_empty. } - iModIntro. iApply (bin_log_related_pack _ (ngR γ)). iApply bin_log_related_pair. - (* New name *) @@ -101,7 +99,6 @@ Section namegen_refinement. { iIntros (Hx). destruct Hx as [x Hy]. rewrite (big_sepS_elem_of _ L (x,S n) Hy). iDestruct "HL" as "[_ %]". omega. } - iApply fupd_logrel. iMod (bij_alloc_alt _ _ γ _ l' (S n) with "HB") as "[HB #Hl'n]"; auto. iMod ("Hcl" with "[-]"). { iNext. iExists _,_; iFrame. @@ -109,7 +106,6 @@ Section namegen_refinement. iFrame. iSplit; eauto. iApply (big_sepS_mono _ _ L L with "HL"); first reflexivity. intros [l x] Hlx. apply uPred.sep_mono_r, uPred.pure_mono. eauto. } - iModIntro. rel_vals. iModIntro. iAlways. iExists _, _; eauto. - (* Name comparison *) diff --git a/theories/examples/stack/helping.v b/theories/examples/stack/helping.v index 8cb748dfeac352567fdf911166ca3aa9d25a617b..24e87c34c2a4da4322227e3cd3492b54900b73b3 100644 --- a/theories/examples/stack/helping.v +++ b/theories/examples/stack/helping.v @@ -305,8 +305,7 @@ Section refinement. iModIntro. iExists _; iFrame. iNext. iIntros "Hst1". rewrite stackRel_unfold. iDestruct "Hrel" as (w1 w2) "[[% %] #Hrel]"; simplify_eq/=. - iApply fupd_logrel'. - iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq; iModIntro; rel_fold_l. + iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq; rel_fold_l. - rel_case_l. rel_seq_l. rel_apply_r (CG_pop_fail_r with "Hst2 Hl"). @@ -317,9 +316,7 @@ Section refinement. rewrite stackRel_unfold. iExists _,_; iSplit; eauto. } rel_vals. iLeft. iModIntro. iExists (_,_). eauto. - - iApply fupd_logrel'. - iDestruct "Hrel" as (n t1 t2) "(>% & >% & Hrel)". simplify_eq/=. - iModIntro. + - iDestruct "Hrel" as (n t1 t2) "(>% & >% & Hrel)". simplify_eq/=. rel_case_l. rel_let_l. iMod ("Hcl" with "[-IH]"). @@ -339,11 +336,9 @@ Section refinement. iIntros (?). iNext. iIntros "Hst1". rel_if_true_l. rewrite stackRel_unfold. - iApply fupd_logrel'. iDestruct "Hrel" as (??) "[[% %] Hrel]"; simplify_eq/=. iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq. iDestruct "Hrel" as (???) "(>% & >% & Hrel)"; simplify_eq/=. - iModIntro. rel_apply_r (CG_pop_suc_r with "Hst2 Hl"). { solve_ndisj. } iIntros "Hst' Hl". @@ -382,7 +377,6 @@ Section refinement. unlock push_st. rel_rec_l. rel_let_l. unlock CG_locked_pop. rel_rec_r. rel_let_r. unlock CG_locked_push. rel_rec_r. rel_let_r. - iApply fupd_logrel. iMod (own_alloc (● to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor". { apply auth_auth_valid. apply to_offer_reg_valid. } iMod (inv_alloc stackN _ (stackInv γo st st' mb l') with "[-]") as "#Hinv". @@ -391,7 +385,6 @@ Section refinement. iSplit; eauto. iApply stackRel_empty. iSplitL; first eauto. iApply offerInv_empty. } - iModIntro. iApply bin_log_related_pair; last first. (* * Push refinement *) { iApply bin_log_related_arrow_val; eauto. @@ -421,9 +414,7 @@ Section refinement. rel_rec_l. unlock revoke_offer. rel_rec_l. iDestruct (offerInv_excl with "HN Ho") as %Hbaz. - iApply fupd_logrel'. iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. - iModIntro. rewrite {2}bin_log_related_eq /bin_log_related_def. iIntros (vvs ρ) "#Hs #HΓ". iIntros (j K) "Hj". cbn[snd fst]. @@ -582,7 +573,7 @@ Section refinement. apply bin_log_related_spec_ctx. iDestruct 1 as (ρ') "#Hspec". tp_rec j. - iApply fupd_logrel'. + iApply fupd_logrel. tp_cas_suc j. simpl. repeat (tp_pure j _). simpl. unlock CG_push. diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v index fa9cf6b9a5bc331ab88cfbbc6047cc26800e378d..b1f4580e9168851645f6d8f64bd8ab539e4af362 100644 --- a/theories/examples/stack/refinement.v +++ b/theories/examples/stack/refinement.v @@ -61,9 +61,7 @@ Section Stack_refinement. rel_apply_r (CG_push_r with "Hst' Hl"). { solve_ndisj. } iIntros "Hst' Hl". - iApply fupd_logrel'. (* TODO iMod should pick this up on its own *) iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]". - iModIntro. iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]"). { iNext. rewrite {2}/sinv. iExists _,_,_. iFrame "Hoe Hst' Hst Hl". @@ -335,7 +333,6 @@ Section Full_refinement. simpl. rel_rec_l. - iApply fupd_logrel. iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done. set (istkG := StackG _ _ γ). change γ with (@stack_name _ istkG). @@ -353,7 +350,6 @@ Section Full_refinement. { iExists _, _, _. by iFrame. } iMod (inv_alloc stackN with "[Hinv]") as "#Hinv". { iNext. iExact "Hinv". } - iModIntro. unlock FG_stack_body. unlock FG_push. repeat rel_rec_l. diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v index b5e069ffdc9a883a8c30d3d4b259403fc2517b5d..22cf4e706aea2a34150e1e1e782c2751fc423ca2 100644 --- a/theories/examples/symbol.v +++ b/theories/examples/symbol.v @@ -279,11 +279,9 @@ Section proof. rel_alloc_r as size2 "[Hs2 Hs2']"; rel_let_r. rel_alloc_l as tbl1 "[Htbl1 Htbl1']"; rel_let_l. rel_alloc_r as tbl2 "[Htbl2 Htbl2']"; rel_let_r. - iApply fupd_logrel'. iMod (own_alloc (● (0 : mnat))) as (γ) "Ha"; first done. iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv". { iNext. iExists _,_. iFrame. iApply LIST_interp_nil. } - iModIntro. rel_apply_r bin_log_related_newlock_r; first done. iIntros (l2) "Hl2". rel_let_r. pose (N:=(logrelN.@"lock1")). @@ -320,11 +318,9 @@ Section proof. rel_store_r. rel_let_r. (* Before we close the lock, we need to gather some evidence *) - iApply fupd_logrel'. iMod (conjure_0 γ) as "Hf". iMod (same_size with "[$Ha $Hf]") as "[Ha #Hf]". iMod (inc_size with "Ha") as "Ha". - iModIntro. iDestruct "Hs2" as "[Hs2 Hs2']". rewrite Nat.add_1_r. iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_". diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v index a29475bafd3b73f30dd082481632eab4fc82bc7b..c3de3c9128aa49a32ecdc9f0a97c7121daba962d 100644 --- a/theories/examples/ticket_lock.v +++ b/theories/examples/ticket_lock.v @@ -133,11 +133,9 @@ Section refinement. Proof. iIntros (Δ). pose (N:=logrelN.@"locked"). - iApply fupd_logrel'. iMod (own_alloc (● (∅ : lockPoolR))) as (γp) "HP"; first done. iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv". { iNext. iExists ∅. iFrame. by rewrite /lockPoolInv big_sepS_empty. } - iModIntro. iApply (bin_log_related_pack _ (lockInt γp)). repeat iApply bin_log_related_pair. - (* Allocating a new lock *) @@ -151,14 +149,12 @@ Section refinement. iInv N as (P) "[>HP Hpool]" "Hcl". iModIntro. iNext. iIntros (ln) "Hln". - iApply fupd_logrel'. iMod (own_alloc (● (GSet ∅) ⋅ ◯ (GSet ∅))) as (γ) "[Hγ Hγ']". { by rewrite -auth_both_op. } iMod (own_update with "HP") as "[HP Hls]". { eapply auth_update_alloc. eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} ∪ P)). apply union_subseteq_r. } - iModIntro. iDestruct (lockPool_excl _ lo ln γ l' with "Hpool Hlo") as %Hnew. iMod ("Hcl" with "[-Hls]") as "_". { iNext. iExists _; iFrame. @@ -203,12 +199,10 @@ Section refinement. iApply "Hpool". iExists _,_,_; by iFrame. } iApply "IH". + simplify_eq. - iApply fupd_logrel'. iMod (own_update with "Hseq") as "[Hseq Hticket]". { eapply auth_update_alloc. eapply (gset_disj_alloc_empty_local_update _ {[ n ]}). apply (seq_set_S_disjoint 0). } - iModIntro. rewrite -(seq_set_S_union_L 0). rewrite Nat.add_1_r. iMod ("Hcl" with "[-Hticket]") as "_". diff --git a/theories/examples/various.v b/theories/examples/various.v index 664bd2b59c2b26c2ca8cc0a2c55d30bcb6ffbc8a..6dcd903d785592e0904921c08160e9914c2d7f1f 100644 --- a/theories/examples/various.v +++ b/theories/examples/various.v @@ -74,20 +74,16 @@ Section refinement. rel_alloc_l as x "Hx". rel_alloc_r as y "Hy". rel_let_l; rel_let_r. - iApply fupd_logrel. - iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*) - iModIntro. + iMod new_pending as (γ) "Ht". iMod (inv_alloc shootN _ ((x ↦ᵢ #0 ∗ pending γ ∨ x ↦ᵢ #1 ∗ shot γ) ∗ y ↦ₛ #1)%I with "[Hx Ht $Hy]") as "#Hinv". { iNext. iLeft. iFrame. } iApply bin_log_related_arrow; auto. - iIntros "!#" (f1 f2) "Hf". + iIntros "!#" (f1 f2) "#Hf". rel_let_l. rel_let_r. rel_store_l_atomic. iInv shootN as "[[[Hx Hp] | [Hx #Hs]] Hy]" "Hcl"; iModIntro; iExists _; iFrame "Hx"; iNext; iIntros "Hx"; rel_rec_l. - - iApply fupd_logrel'. - iMod (shoot γ with "Hp") as "#Hs". - iModIntro. + - iMod (shoot γ with "Hp") as "#Hs". iMod ("Hcl" with "[$Hy Hx]") as "_". { iNext. iRight. by iFrame. } iApply (bin_log_related_seq with "[Hf]"); auto. @@ -448,11 +444,9 @@ Section refinement. iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first. { iDestruct (own_valid_2 with "Ht Ht'2") as %Hfoo. inversion Hfoo. } - iApply fupd_logrel. iMod (shoot γ with "Hp") as "#Hs". iMod ("Hcl" with "[-]") as "_". { iNext. iExists m. iRight. iFrame. done. } - iModIntro. iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto. { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]"). iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val. @@ -503,10 +497,8 @@ Section refinement. rel_let_l. rel_let_r. rel_alloc_l as c1 "Hc1". rel_alloc_r as c2 "Hc2". - iApply fupd_logrel. - iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*) + iMod new_pending as (γ) "Ht". iMod (own_alloc (Excl ())) as (γ') "Ht'"; first done. - iModIntro. iMod (inv_alloc shootN _ (i6 c1 c2 γ γ') with "[Hc1 Hc2 Ht]") as "#Hinv". { iNext. iExists 0. iLeft. iFrame. } rel_let_l. rel_let_r. diff --git a/theories/logrel/fundamental_binary.v b/theories/logrel/fundamental_binary.v index fe81673b7b3614833ce106ef2b8f75d230660d35..81836ffae96753eb539460a2f5bb43fdff2edca6 100644 --- a/theories/logrel/fundamental_binary.v +++ b/theories/logrel/fundamental_binary.v @@ -318,16 +318,13 @@ Section masked. rel_op_l. rel_op_r. destruct (decide (l1 = l1')) as [->|?]. - - iApply fupd_logrel. - iMod (interp_ref_funct _ _ _ l1' l2 l2' with "[Hl Hl']") as %->. + - iMod (interp_ref_funct _ _ _ l1' l2 l2' with "[Hl Hl']") as %->. { solve_ndisj. } { iSplit; iExists (_,_); eauto. } rewrite decide_left. - iModIntro. value_case. - destruct (decide (l2 = l2')) as [->|?]. - + iApply fupd_logrel. - iMod (interp_ref_inj _ _ _ l2' l1 l1' with "[Hl Hl']") as %->. + + iMod (interp_ref_inj _ _ _ l2' l1 l1' with "[Hl Hl']") as %->. { solve_ndisj. } { iSplit; iExists (_,_); eauto. } congruence. @@ -580,20 +577,16 @@ Section masked. destruct (decide (v' = v2)) as [|Hneq]; subst. - iSplitR; first by (iIntros (?); contradiction). iIntros (?). iNext. iIntros "Hv1". - iApply fupd_logrel'. - iAssert (▷ ⌜v2 = v2'⌝)%I with "[IH2]" as ">%". + iAssert (⌜v2 = v2'⌝)%I with "[IH2]" as %->. { rewrite ?interp_EqType_agree; trivial. } - iModIntro. rel_cas_suc_r. iMod ("Hclose" with "[-]"). { iNext; iExists (_, _); by iFrame. } rel_vals; eauto. - iSplitL; last by (iIntros (?); congruence). iIntros (?). iNext. iIntros "Hv1". - iApply fupd_logrel'. - iAssert (▷ ⌜v' ≠ v2'⌝)%I as ">%". + iAssert (⌜v' ≠ v2'⌝)%I as "%". { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. } - iModIntro. rel_cas_fail_r. iMod ("Hclose" with "[-]"). { iNext; iExists (_, _); by iFrame. } diff --git a/theories/logrel/logrel_binary.v b/theories/logrel/logrel_binary.v index 4e19ff559eb4b7237b7f9f38ccf03e1f5414d557..0c7007f35b59f2f07febe7e1fabb6844ba034c43 100644 --- a/theories/logrel/logrel_binary.v +++ b/theories/logrel/logrel_binary.v @@ -167,47 +167,45 @@ Section related_facts. Implicit Types Δ : listC D. (* We need this to be able to open and closed invariants in front of logrels *) - Lemma fupd_logrel E1 E2 Δ Γ e e' τ : - ((|={E1,E2}=> ({E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)) - -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I. + Lemma fupd_logrel E1 E2 E3 Δ Γ e e' τ : + ((|={E1,E2}=> ({E2,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ)) + -∗ {E1,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I. Proof. - rewrite bin_log_related_eq. - iIntros "H". - iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". - iMod "H". - iSpecialize ("H" with "Hs [HΓ] Hj"); eauto. - Qed. - - Lemma fupd_logrel' E1 E2 Δ Γ e e' τ : - ((|={E1}=> ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)) - -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I. - Proof. - rewrite bin_log_related_eq. + rewrite bin_log_related_eq /bin_log_related_def. iIntros "H". iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". - iMod "H". + iMod "H" as "H". iSpecialize ("H" with "Hs [HΓ] Hj"); eauto. Qed. - Global Instance elim_modal_logrel E1 E2 Δ Γ e e' P τ : + Global Instance elim_fupd_logrel E1 E2 E3 Δ Γ e e' P τ : ElimModal (|={E1,E2}=> P) P - ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) | 10. + ({E1,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E2,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ). Proof. rewrite /ElimModal. iIntros "[HP HI]". iApply fupd_logrel. iMod "HP". iApply ("HI" with "HP"). Qed. - Global Instance elim_modal_logrel' E1 E2 Δ Γ e e' P τ : - ElimModal (|={E1}=> P) P - ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) | 0. + Global Instance elim_bupd_logrel E1 E2 Δ Γ e e' P τ : + ElimModal (|==> P) P + ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ). Proof. - rewrite /ElimModal. - iIntros "[HP HI]". iApply fupd_logrel'. - iMod "HP". iApply ("HI" with "HP"). + rewrite /ElimModal (bupd_fupd E1). + apply: elim_fupd_logrel. + Qed. + + (* This + elim_modal_timless_bupd' is useful for stripping off laters of timeless propositions. *) + Global Instance is_except_0_logrel E1 E2 Δ Γ e e' τ : + IsExcept0 ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ). + Proof. + rewrite /IsExcept0. + iIntros "HL". + iApply fupd_logrel. + by iMod "HL". Qed. - Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 τ : + Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 (τ : type) : {Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗ {τi::Δ;⤉Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)]. Proof.