`FromAnd true` instances for big ops and ownership.

This way, iSplit will work when one side is persistent.

theories/base_logic/lib/auth.v

@@ -73,10 +73,18 @@ Section auth.
   Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ∗ auth_own γ b.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
 
-  Global Instance from_sep_auth_own γ a b1 b2 :
+  Global Instance from_and_auth_own γ a b1 b2 :
     FromOp a b1 b2 →
     FromAnd false (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
   Proof. rewrite /FromOp /FromAnd=> <-. by rewrite auth_own_op. Qed.
+  Global Instance from_and_auth_own_persistent γ a b1 b2 :
+    FromOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+    FromAnd true (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 91.
+  Proof.
+    intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
+    by rewrite -auth_own_op from_op.
+  Qed.
+
   Global Instance into_and_auth_own p γ a b1 b2 :
     IntoOp a b1 b2 →
     IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.

theories/base_logic/lib/fractional.v

@@ -138,9 +138,9 @@ Section fractional.
     FromAnd false Q P P.
   Proof. rewrite /FromAnd=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
 
-  Global Instance into_and_fractional b P P1 P2 Φ q1 q2 :
+  Global Instance into_and_fractional p P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    IntoAnd b P P1 P2.
+    IntoAnd p P P1 P2.
   Proof.
     (* TODO: We need a better way to handle this boolean here; always
        applying mk_into_and_sep (which only works after introducing all
@@ -150,9 +150,9 @@ Section fractional.
        "false" only, thus breaking some intro patterns. *)
     intros. apply mk_into_and_sep. rewrite [P]fractional_split //.
   Qed.
-  Global Instance into_and_fractional_half b P Q Φ q :
+  Global Instance into_and_fractional_half p P Q Φ q :
     AsFractional P Φ q → AsFractional Q Φ (q/2) →
-    IntoAnd b P Q Q | 100.
+    IntoAnd p P Q Q | 100.
   Proof. intros. apply mk_into_and_sep. rewrite [P]fractional_half //. Qed.
 
   (* The instance [frame_fractional] can be tried at all the nodes of

theories/base_logic/lib/own.v

@@ -189,4 +189,11 @@ Section proofmode_classes.
   Global Instance from_and_own γ a b1 b2 :
     FromOp a b1 b2 → FromAnd false (own γ a) (own γ b1) (own γ b2).
   Proof. intros. by rewrite /FromAnd -own_op from_op. Qed.
+  Global Instance from_and_own_persistent γ a b1 b2 :
+    FromOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+    FromAnd true (own γ a) (own γ b1) (own γ b2).
+  Proof.
+    intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
+    by rewrite -own_op from_op.
+  Qed.
 End proofmode_classes.

theories/proofmode/class_instances.v

@@ -331,6 +331,13 @@ Global Instance from_sep_ownM (a b1 b2 : M) :
   FromOp a b1 b2 →
   FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof. intros. by rewrite /FromAnd -ownM_op from_op. Qed.
+Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
+  FromOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+  FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
+  by rewrite -ownM_op from_op.
+Qed.
 
 Global Instance from_sep_bupd P Q1 Q2 :
   FromAnd false P Q1 Q2 → FromAnd false (|==> P) (|==> Q1) (|==> Q2).
@@ -339,10 +346,20 @@ Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.
 Global Instance from_and_big_sepL_cons {A} (Φ : nat → A → uPred M) x l :
   FromAnd false ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
 Proof. by rewrite /FromAnd big_sepL_cons. Qed.
+Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l :
+  PersistentP (Φ 0 x) →
+  FromAnd true ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
+Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.
+
 Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
   FromAnd false ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. by rewrite /FromAnd big_sepL_app. Qed.
+Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M) l1 l2 :
+  (∀ k y, PersistentP (Φ k y)) →
+  FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
+    ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
+Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
 
 (* FromOp *)
 Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a ⋅ b) a b.

theories/proofmode/classes.v

@@ -2,6 +2,16 @@ From iris.base_logic Require Export base_logic.
 Set Default Proof Using "Type".
 Import uPred.
 
+(* The Or class is useful for efficiency: instead of having two instances
+[P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R],
+which avoids the need to derive [P] twice. *)
+Inductive Or (P1 P2 : Type) :=
+  | Or_l : P1 → Or P1 P2
+  | Or_r : P2 → Or P1 P2.
+Existing Class Or.
+Existing Instance Or_l | 9.
+Existing Instance Or_r | 10.
+
 Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
   from_assumption : □?p P ⊢ Q.
 Arguments from_assumption {_} _ _ _ {_}.
@@ -83,6 +93,13 @@ Hint Mode FromAnd + + - ! ! : typeclass_instances. (* For iCombine *)
 Lemma mk_from_and_and {M} p (P Q1 Q2 : uPred M) :
   (Q1 ∧ Q2 ⊢ P) → FromAnd p P Q1 Q2.
 Proof. rewrite /FromAnd=><-. destruct p; auto using sep_and. Qed.
+Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
+  Or (PersistentP Q1) (PersistentP Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
+Proof.
+  intros [?|?] ?; rewrite /FromAnd.
+  - by rewrite always_and_sep_l.
+  - by rewrite always_and_sep_r.
+Qed.
 
 Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
   into_and : P ⊢ if p then Q1 ∧ Q2 else Q1 ∗ Q2.