Merge branch 'jh/generic_updates' into 'gen_proofmode'

Type classes for updates properties

See merge request FP/iris-coq!106

theories/base_logic/base_logic.v

@@ -23,23 +23,14 @@ Hint Immediate True_intro False_elim : I.
 Hint Immediate iff_refl internal_eq_refl : I.
 
 (* Setup of the proof mode *)
-Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
-
 Section class_instances.
 Context {M : ucmraT}.
 Implicit Types P Q R : uPred M.
 
-Global Instance from_assumption_bupd p P Q :
-  FromAssumption p P Q → FromAssumption p P (|==> Q).
-Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
-
 Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
   @IntoPure (uPredI M) (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|==> P) φ.
-Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
-
 Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
   @FromPure (uPredI M) (✓ a) (✓ a).
 Proof.
@@ -47,27 +38,6 @@ Proof.
   rewrite -cmra_valid_intro //. by apply pure_intro.
 Qed.
 
-Global Instance into_wand_bupd p q R P Q :
-  IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
-Proof.
-  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
-Qed.
-
-Global Instance into_wand_bupd_persistent p q R P Q :
-  IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
-Proof.
-  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
-Qed.
-
-Global Instance into_wand_bupd_args p q R P Q :
-  IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
-Proof.
-  rewrite /IntoWand' /IntoWand /= => ->.
-  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
-Qed.
-
 (* FromOp *)
 (* TODO: Worst case there could be a lot of backtracking on these instances,
 try to refactor. *)
@@ -110,45 +80,4 @@ Qed.
 Global Instance into_sep_ownM (a b1 b2 : M) :
   IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
-
-Global Instance from_sep_bupd P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
-Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
-
-Global Instance from_or_bupd P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
-Proof.
-  rewrite /FromOr=><-.
-  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
-Qed.
-
-Global Instance from_exist_bupd {A} P (Φ : A → uPred M) :
-  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
-Proof.
-  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
-
-Global Instance from_modal_bupd P : FromModal (|==> P) P.
-Proof. apply bupd_intro. Qed.
-
-Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
-Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-
-Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
-
-Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
-
-Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
-Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-
-Global Instance is_except_0_bupd P : IsExcept0 P → IsExcept0 (|==> P).
-Proof.
-  rewrite /IsExcept0=> HP.
-  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
-Qed.
-
-Global Instance frame_bupd p R P Q : Frame p R P Q → Frame p R (|==> P) (|==> Q).
-Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
 End class_instances.

theories/base_logic/derived.v

@@ -40,31 +40,11 @@ Proof.
   rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
   apply:persistently_cmra_valid_1.
 Qed.
-
-(** * Derived rules *)
-Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@bupd _ (@uPred_bupd M)).
-Proof. intros P Q; apply bupd_mono. Qed.
-Global Instance bupd_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@bupd _ (@uPred_bupd M)).
-Proof. intros P Q; apply bupd_mono. Qed.
-Lemma bupd_frame_l R Q : (R ∗ |==> Q) ==∗ R ∗ Q.
-Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
-Lemma bupd_wand_l P Q : (P -∗ Q) ∗ (|==> P) ==∗ Q.
-Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
-Lemma bupd_wand_r P Q : (|==> P) ∗ (P -∗ Q) ==∗ Q.
-Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
-Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q.
-Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
 Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
 Proof.
   intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
   by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
 Qed.
-Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
-Proof.
-  rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
-  by rewrite -bupd_intro -or_intro_l.
-Qed.
 
 (* Timeless instances *)
 Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
@@ -84,12 +64,6 @@ Global Instance cmra_valid_plain {A : cmraT} (a : A) :
   Plain (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
 
-Lemma bupd_affinely_plainly P : (|==> ■ P) ⊢ P.
-Proof. by rewrite affine_affinely bupd_plainly. Qed.
-
-Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
-Proof. by rewrite -{1}(plain_plainly P) bupd_plainly. Qed.
-
 (* Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.

theories/base_logic/lib/fancy_updates.v

@@ -13,237 +13,32 @@ Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
 Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
 Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.
 
-Section fupd.
-Context `{invG Σ}.
-Implicit Types P Q : iProp Σ.
-
-Global Instance fupd_ne E1 E2 : NonExpansive (fupd E1 E2).
-Proof. rewrite uPred_fupd_eq. solve_proper. Qed.
-Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd E1 E2).
-Proof. apply ne_proper, _. Qed.
-
-Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
-Proof.
-  intros (E1''&->&?)%subseteq_disjoint_union_L.
-  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
-  by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
-Qed.
-
-Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
-Proof. rewrite uPred_fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
-
-Lemma bupd_fupd E P : (|==> P) ={E}=∗ P.
-Proof. rewrite uPred_fupd_eq. by iIntros ">? [$ $] !> !>". Qed.
-
-Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
-Proof.
-  rewrite uPred_fupd_eq. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
-Qed.
-
-Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
-Proof.
-  rewrite uPred_fupd_eq. iIntros "HP HwE".
-  iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
-Qed.
-
-Lemma fupd_mask_frame_r' E1 E2 Ef P :
-  E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
-Proof.
-  intros. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
-  iIntros "Hvs (Hw & HE1 &HEf)".
-  iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
-  iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
-  iIntros "!> !>". by iApply "HP".
-Qed.
-
-Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
-Proof. rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros "[HwP $]". Qed.
-
-Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
-  E1 ⊆ E2 →
-  (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
-Proof.
-  iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
-  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
-  iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
-  iAssert (◇ P)%I as "#HP".
-  { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
-  iMod "HP". iFrame. auto.
+Instance fupd_facts `{invG Σ} : FUpdFacts (uPredSI (iResUR Σ)).
+Proof.
+  split.
+  - apply _.
+  - rewrite uPred_fupd_eq. solve_proper.
+  - intros E1 E2 P (E1''&->&?)%subseteq_disjoint_union_L.
+    rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
+      by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
+  - rewrite uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>".
+  - rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
+  - rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
+  - rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE".
+    iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
+  - intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
+    iIntros "Hvs (Hw & HE1 &HEf)".
+    iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
+    iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
+    iIntros "!> !>". by iApply "HP".
+  - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
+  - iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
+    rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
+    iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
+    iAssert (◇ P)%I as "#HP".
+    { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
+    iMod "HP". iFrame. auto.
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
+    iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
+    iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
 Qed.
-
-Lemma later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
-Proof.
-  rewrite uPred_fupd_eq /uPred_fupd_def. iIntros "HP [Hw HE]".
-  iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
-  iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
-Qed.
-
-(** * Derived rules *)
-Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
-Proof. intros P Q; apply fupd_mono. Qed.
-Global Instance fupd_flip_mono' E1 E2 :
-  Proper (flip (⊢) ==> flip (⊢)) (fupd E1 E2).
-Proof. intros P Q; apply fupd_mono. Qed.
-
-Lemma fupd_intro E P : P ={E}=∗ P.
-Proof. iIntros "HP". by iApply bupd_fupd. Qed.
-Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> True)%I.
-Proof. exact: fupd_intro_mask. Qed.
-Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
-Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
-
-Lemma fupd_frame_l E1 E2 P Q : (P ∗ |={E1,E2}=> Q) ={E1,E2}=∗ P ∗ Q.
-Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
-Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ={E1,E2}=∗ Q.
-Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
-Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q.
-Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
-
-Lemma fupd_trans_frame E1 E2 E3 P Q :
-  ((Q ={E2,E3}=∗ True) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P.
-Proof.
-  rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
-  by rewrite fupd_frame_r left_id fupd_trans.
-Qed.
-
-Lemma fupd_mask_frame_r E1 E2 Ef P :
-  E1 ## Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
-Proof.
-  iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
-  iApply fupd_wand_r; iFrame "H"; eauto.
-Qed.
-Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=∗ P.
-Proof.
-  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
-Qed.
-
-Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
-Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
-Lemma fupd_big_sepL {A} E (Φ : nat → A → iProp Σ) (l : list A) :
-  ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ={E}=∗ [∗ list] k↦x ∈ l, Φ k x.
-Proof.
-  apply (big_opL_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-Qed.
-Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) :
-  ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=∗ [∗ map] k↦x ∈ m, Φ k x.
-Proof.
-  apply (big_opM_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-Qed.
-Lemma fupd_big_sepS `{Countable A} E (Φ : A → iProp Σ) X :
-  ([∗ set] x ∈ X, |={E}=> Φ x) ={E}=∗ [∗ set] x ∈ X, Φ x.
-Proof.
-  apply (big_opS_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-Qed.
-
-Lemma fupd_plain E1 E2 P Q `{!Plain P} :
-  E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
-Proof.
-  iIntros (HE) "HQP HQ". iApply (fupd_plain' _ _ E1 with "[HQP] HQ"); first done.
-  iIntros "?". iApply fupd_intro. by iApply "HQP".
-Qed.
-End fupd.
-
-(** Proofmode class instances *)
-Section proofmode_classes.
-  Context `{invG Σ}.
-  Implicit Types P Q : iProp Σ.
-
-  Global Instance from_pure_fupd E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
-  Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
-
-  Global Instance from_assumption_fupd E p P Q :
-    FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
-  Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
-
-  Global Instance into_wand_fupd E p q R P Q :
-    IntoWand false false R P Q →
-    IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
-  Proof.
-    rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
-    apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
-  Qed.
-
-  Global Instance into_wand_fupd_persistent E1 E2 p q R P Q :
-    IntoWand false q R P Q → IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
-  Proof.
-    rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
-    apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
-  Qed.
-
-  Global Instance into_wand_fupd_args E1 E2 p q R P Q :
-    IntoWand p false R P Q → IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
-  Proof.
-    rewrite /IntoWand' /IntoWand /= => ->.
-    apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
-  Qed.
-
-  Global Instance from_sep_fupd E P Q1 Q2 :
-    FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
-  Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
-
-  Global Instance from_or_fupd E1 E2 P Q1 Q2 :
-    FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
-  Proof. rewrite /FromOr=><-. apply or_elim; apply fupd_mono; auto with I. Qed.
-
-  Global Instance from_exist_fupd {A} E1 E2 P (Φ : A → iProp Σ) :
-    FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
-  Proof.
-    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-  Qed.
-
-  Global Instance frame_fupd p E1 E2 R P Q :
-    Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
-  Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
-
-  Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
-  Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
-
-  Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
-  Proof. rewrite /FromModal. apply fupd_intro. Qed.
-
-  Global Instance elim_modal_bupd_fupd E1 E2 P Q :
-    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
-  Proof.
-    by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
-  Qed.
-  Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
-    ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
-  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
-
-  Global Instance add_modal_fupd E1 E2 P Q :
-    AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
-  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
-End proofmode_classes.
-
-Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
-
-(** Fancy updates that take a step. *)
-
-Section step_fupd.
-Context `{invG Σ}.
-
-Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2}▷=> Q.
-Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
-
-Lemma step_fupd_mask_frame_r E1 E2 Ef P :
-  E1 ## Ef → E2 ## Ef → (|={E1,E2}▷=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}▷=> P.
-Proof.
-  iIntros (??) "HP". iApply fupd_mask_frame_r. done. iMod "HP". iModIntro.
-  iNext. by iApply fupd_mask_frame_r.
-Qed.
-
-Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
-  F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
-Proof.
-  iIntros (??) "HP".
-  iMod (fupd_intro_mask') as "HM1"; first done. iMod "HP".
-  iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
-  iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
-Qed.
-
-Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1,E2}▷=> P.
-Proof. iIntros (?) "HP". iApply (step_fupd_mask_mono E2 _ _ E2); auto. Qed.
-End step_fupd.

theories/base_logic/upred.v

@@ -601,16 +601,6 @@ Qed.
 Global Instance cmra_valid_proper {A : cmraT} :
   Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
 
-Global Instance bupd_ne : NonExpansive (@bupd _ (@uPred_bupd M)).
-Proof.
-  intros n P Q HPQ.
-  unseal; split=> n' x; split; intros HP k yf ??;
-    destruct (HP k yf) as (x'&?&?); auto;
-    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
-Qed.
-Global Instance bupd_proper :
-  Proper ((≡) ==> (≡)) (@bupd _ (@uPred_bupd M)) := ne_proper _.
-
 (** BI instances *)
 
 Global Instance uPred_affine : BiAffine (uPredI M) | 0.
@@ -686,27 +676,29 @@ Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) :
 Proof. by uPred.unseal. Qed.
 
 (* Basic update modality *)
-Lemma bupd_intro P : P ==∗ P.
-Proof.
-  unseal. split=> n x ? HP k yf ?; exists x; split; first done.
-  apply uPred_mono with n x; eauto using cmra_validN_op_l.
-Qed.
-Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ==∗ Q.
+Global Instance bupd_facts : BUpdFacts (uPredI M).
 Proof.
-  unseal. intros HPQ; split=> n x ? HP k yf ??.
-  destruct (HP k yf) as (x'&?&?); eauto.
-  exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
-Qed.
-Lemma bupd_trans P : (|==> |==> P) ==∗ P.
-Proof. unseal; split; naive_solver. Qed.
-Lemma bupd_frame_r P R : (|==> P) ∗ R ==∗ P ∗ R.
-Proof.
-  unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
-  destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto.
-  { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
-  exists (x' ⋅ x2); split; first by rewrite -assoc.
-  exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
+  split.
+  - intros n P Q HPQ.
+    unseal; split=> n' x; split; intros HP k yf ??;
+    destruct (HP k yf) as (x'&?&?); auto;
+    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
+  - unseal. split=> n x ? HP k yf ?; exists x; split; first done.
+    apply uPred_mono with n x; eauto using cmra_validN_op_l.
+  - unseal. intros HPQ; split=> n x ? HP k yf ??.
+    destruct (HP k yf) as (x'&?&?); eauto.
+    exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
+  - unseal; split; naive_solver.
+  - unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
+    destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto.
+    { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
+    exists (x' ⋅ x2); split; first by rewrite -assoc.
+    exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
+  - unseal; split => n x Hnx /= Hng.
+    destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
+    eapply uPred_mono; eauto using ucmra_unit_leastN.
 Qed.
+
 Lemma bupd_ownM_updateP x (Φ : M → Prop) :
   x ~~>: Φ → uPred_ownM x ==∗ ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
 Proof.
@@ -716,11 +708,5 @@ Proof.
   exists (y ⋅ x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma bupd_plainly P : (|==> bi_plainly P) ⊢ P.
-Proof.
-  unseal; split => n x Hnx /= Hng.
-  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
-  eapply uPred_mono; eauto using ucmra_unit_leastN.
-Qed.
 End uPred.
 End uPred.

theories/bi/monpred.v

+From stdpp Require Import coPset.
 From iris.bi Require Import bi.
 
 (** Definitions. *)
@@ -205,16 +206,43 @@ Definition monPred_ex_def (P : monPred) : monPred :=
 Definition monPred_ex_aux : seal (@monPred_ex_def). by eexists. Qed.
 Definition monPred_ex := unseal (@monPred_ex_aux).
 Definition monPred_ex_eq : @monPred_ex = _ := seal_eq _.
+
+
+Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred :=
+  (* monPred_upclosed is not actually needed, since bupd is always
+     monotone. However, this depends on BUpdFacts, and we do not want
+     this definition to depend on BUpdFacts to avoid having proofs
+     terms in logical terms. *)
+  monPred_upclosed (λ i, |==> P i)%I.
+Definition monPred_bupd_aux `{BUpd PROP} : seal monPred_bupd_def. by eexists. Qed.
+Global Instance monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
+Definition monPred_bupd_eq `{BUpd PROP} : @bupd monPred _ = _ := seal_eq _.
 End Bi.
 
 Typeclasses Opaque monPred_pure monPred_emp monPred_plainly.
 
-Program Definition monPred_later_def {I : biIndex} {PROP : sbi}
-        (P : monPred I PROP) : monPred I PROP := MonPred (λ i, ▷ (P i))%I _.
+Section Sbi.
+Context {I : biIndex} {PROP : sbi}.
+Implicit Types i : I.
+Notation monPred := (monPred I PROP).
+Implicit Types P Q : monPred.
+
+Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
 Next Obligation. solve_proper. Qed.
-Definition monPred_later_aux {I PROP} : seal (@monPred_later_def I PROP). by eexists. Qed.
-Definition monPred_later {I PROP} := unseal (@monPred_later_aux I PROP).
-Definition monPred_later_eq {I PROP} : @monPred_later I PROP = _ := seal_eq _.
+Definition monPred_later_aux : seal monPred_later_def. by eexists. Qed.
+Definition monPred_later := unseal monPred_later_aux.