diff --git a/algebra/upred.v b/algebra/upred.v index 0f2b58463444f95c44f0515963108bfc808a4c95..1bd35b4c9de6550b762a3a002cc779ce8a72e960 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -339,6 +339,7 @@ Definition uPred_now_True {M} (P : uPred M) : uPred M := ▷ False ∨ P. Notation "◇ P" := (uPred_now_True P) (at level 20, right associativity) : uPred_scope. Instance: Params (@uPred_now_True) 1. +Typeclasses Opaque uPred_now_True. Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P. Arguments timelessP {_} _ {_}. diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v index 808f1785bc12e4d335cc379f9cefb3d27c22f502..ce5af9d66b3729cc14d145eeb369324577690677 100644 --- a/program_logic/adequacy.v +++ b/program_logic/adequacy.v @@ -52,11 +52,10 @@ Proof. rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]". { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. } rewrite pvs_eq /pvs_def. - iVs ("H" \$! σ1 with "Hσ [Hw HE]") as "[H|(Hw & HE & _ & H)]"; first by iFrame. - { iVsIntro; iNext. by iExFalso. } + iVs ("H" \$! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame. iVsIntro; iNext. - by iVs ("H" \$! e2 σ2 ef with "[%] [Hw HE]") as "[?|(\$ & \$ & \$ & \$)]"; - [done|by iFrame|rewrite /uPred_now_True; eauto|]. + iVs ("H" \$! e2 σ2 ef with "[%] [Hw HE]") + as ">(\$ & \$ & \$ & \$)"; try iFrame; eauto. Qed. Lemma wptp_step e1 t1 t2 σ1 σ2 Φ : @@ -84,8 +83,7 @@ Proof. { inversion_clear 1; iIntros "?"; eauto 10. } iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']]. iVs (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq. - iVsIntro; iNext; iVs "H" as "[?|?]"; first (iVsIntro; iNext; by iExFalso). - by iApply IH. + iVsIntro; iNext; iVs "H" as ">?". by iApply IH. Qed. Instance rvs_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |=r=> ▷ P)%I). @@ -99,8 +97,7 @@ Proof. intros. rewrite wptp_steps // (Nat_iter_S_r (S n)); apply rvs_iter_mono. iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq. iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def. - iVs ("H" with "[Hw HE]") as "[?|(_ & _ & \$)]"; [by iFrame| |done]. - iVsIntro; iNext; by iExFalso. + iVs ("H" with "[Hw HE]") as ">(_ & _ & \$)"; iFrame; auto. Qed. Lemma wp_safe e σ Φ : @@ -108,8 +105,8 @@ Lemma wp_safe e σ Φ : Proof. rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]". { iDestruct "H" as (v) "[% _]"; eauto 10. } - rewrite pvs_eq. iVs ("H" with "* Hσ [-]") as "[H|(?&?&%&?)]"; first by iFrame. - iVsIntro; iNext; by iExFalso. eauto 10. + rewrite pvs_eq. iVs ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame. + eauto 10. Qed. Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ : diff --git a/program_logic/invariants.v b/program_logic/invariants.v index f87869dafa64ace6700eb006633cf571e88dbf7d..59373ce40bbfdf64b45a077fd081e828e321621c 100644 --- a/program_logic/invariants.v +++ b/program_logic/invariants.v @@ -49,9 +49,9 @@ Proof. iDestruct "Hi" as % ?%elem_of_subseteq_singleton. rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver. rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver. - iIntros "(Hw & [HE \$] & \$)"; iVsIntro; iRight. + iIntros "(Hw & [HE \$] & \$)"; iVsIntro; iApply now_True_intro. iDestruct (ownI_open i P with "[Hw HE]") as "(\$ & \$ & HD)"; first by iFrame. - iIntros "HP [Hw \$] !==>"; iRight. iApply ownI_close; by iFrame. + iIntros "HP [Hw \$] !==>"; iApply now_True_intro. iApply ownI_close; by iFrame. Qed. Lemma inv_open_timeless E N P `{!TimelessP P} : diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v index e437c640d40fb5261659093021049ddec3d94ae6..1e98139e2fd6accded715109b7a6c8c8e8c1db13 100644 --- a/program_logic/pviewshifts.v +++ b/program_logic/pviewshifts.v @@ -44,17 +44,17 @@ Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=> Proof. intros (E1''&->&?)%subseteq_disjoint_union_L. rewrite pvs_eq /pvs_def ownE_op //; iIntros "H (\$ & \$ & HE) !==>". - iApply now_True_intro. iApply "H". iIntros "[\$ \$] !==>". iRight; eauto. + iApply now_True_intro. iApply "H". + iIntros "[\$ \$] !==>". by iApply now_True_intro. Qed. Lemma now_True_pvs E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=> P. Proof. - rewrite pvs_eq. iIntros "[?|H] [Hw HE]". - - rewrite /uPred_now_True; eauto. - - iApply "H"; by iFrame. + rewrite pvs_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame. Qed. Lemma rvs_pvs E P : (|=r=> P) ={E}=> P. Proof. - rewrite pvs_eq /pvs_def. iIntros "H [\$ \$]". by rewrite -uPred.now_True_intro. + rewrite pvs_eq /pvs_def. iIntros "H [\$ \$]"; iVs "H". + iVsIntro. by iApply now_True_intro. Qed. Lemma pvs_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q. Proof. @@ -64,18 +64,15 @@ Qed. Lemma pvs_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P. Proof. rewrite pvs_eq /pvs_def. iIntros "HP HwE". - iVs ("HP" with "HwE") as "[?|(Hw & HE & HP)]". - - rewrite /uPred_now_True; eauto. - - iApply "HP"; by iFrame. + iVs ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame. Qed. Lemma pvs_mask_frame_r' E1 E2 Ef P : E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=> P. Proof. intros. rewrite pvs_eq /pvs_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)". - iVs ("Hvs" with "[Hw HE1]") as "[?|(\$ & HE2 & HP)]"; first by iFrame. - - rewrite /uPred_now_True; eauto. - - iDestruct (ownE_op' with "[HE2 HEf]") as "[? \$]"; first by iFrame. - iVsIntro; iRight; by iApply "HP". + iVs ("Hvs" with "[Hw HE1]") as ">(\$ & HE2 & HP)"; first by iFrame. + iDestruct (ownE_op' with "[HE2 HEf]") as "[? \$]"; first by iFrame. + iVsIntro; iApply now_True_intro. by iApply "HP". Qed. Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q. Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP \$]". Qed.