Merge FromSep and FromAnd classes.

theories/base_logic/lib/auth.v

@@ -75,8 +75,8 @@ Section auth.
 
   Global Instance from_sep_auth_own γ a b1 b2 :
     FromOp a b1 b2 →
-    FromSep (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
-  Proof. rewrite /FromOp /FromSep=> <-. by rewrite auth_own_op. Qed.
+    FromAnd false (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
+  Proof. rewrite /FromOp /FromAnd=> <-. by rewrite auth_own_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/fancy_updates.v

@@ -160,9 +160,9 @@ Section proofmode_classes.
     rewrite /WandWeaken' /WandWeaken=>->. apply wand_intro_l. by rewrite 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_and_fupd E P Q1 Q2 :
+    FromAnd false P Q1 Q2 → FromAnd false (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
+  Proof. rewrite /FromAnd=><-. apply fupd_sep. Qed.
 
   Global Instance or_split_fupd E1 E2 P Q1 Q2 :
     FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).

theories/base_logic/lib/fractional.v

@@ -120,23 +120,23 @@ Section fractional.
   Qed.
 
   (** Proof mode instances *)
-  Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
+  Global Instance from_and_fractional_fwd P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    FromSep P P1 P2.
-  Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
+    FromAnd false P P1 P2.
+  Proof. by rewrite /FromAnd=>-[-> ->] [-> _] [-> _]. Qed.
   Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
     AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) →
-    FromSep P P1 P2 | 10.
-  Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed.
+    FromAnd false P P1 P2 | 10.
+  Proof. by rewrite /FromAnd=>-[-> _] [-> <-] [-> _]. Qed.
 
-  Global Instance from_sep_fractional_half_fwd P Q Φ q :
+  Global Instance from_and_fractional_half_fwd P Q Φ q :
     AsFractional P Φ q → AsFractional Q Φ (q/2) →
-    FromSep P Q Q | 10.
-  Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
-  Global Instance from_sep_fractional_half_bwd P Q Φ q :
+    FromAnd false P Q Q | 10.
+  Proof. by rewrite /FromAnd -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
+  Global Instance from_and_fractional_half_bwd P Q Φ q :
     AsFractional P Φ (q/2) → AsFractional Q Φ q →
-    FromSep Q P P.
-  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
+    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 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
@@ -163,10 +163,12 @@ Section fractional.
   Inductive FrameFractionalHyps
       (p : bool) (R : uPred M) (Φ : Qp → uPred M) (RES : uPred M) : Qp → Qp → Prop :=
     | frame_fractional_hyps_l Q q q' r:
-       Frame p R (Φ q) Q → MakeSep Q (Φ q') RES →
+       Frame p R (Φ q) Q →
+       MakeSep Q (Φ q') RES →
        FrameFractionalHyps p R Φ RES r (q + q')
     | frame_fractional_hyps_r Q q q' r:
-       Frame p R (Φ q') Q → MakeSep Q (Φ q) RES →
+       Frame p R (Φ q') Q →
+       MakeSep Q (Φ q) RES →
        FrameFractionalHyps p R Φ RES r (q + q')
     | frame_fractional_hyps_half q :
        AsFractional RES Φ (q/2) →
@@ -174,6 +176,7 @@ Section fractional.
   Existing Class FrameFractionalHyps.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
+
   Global Instance frame_fractional p R r Φ P q RES:
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →

theories/base_logic/lib/own.v

@@ -186,7 +186,7 @@ Section proofmode_classes.
   Global Instance into_and_own p γ a b1 b2 :
     IntoOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
   Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
-  Global Instance from_sep_own γ a b1 b2 :
-    FromOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
-  Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
+  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.
 End proofmode_classes.

theories/proofmode/class_instances.v

@@ -300,56 +300,49 @@ Proof.
 Qed.
 
 (* FromAnd *)
-Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
+Global Instance from_and_and p P1 P2 : FromAnd p (P1 ∧ P2) P1 P2 | 100.
+Proof. by apply mk_from_and_and. Qed.
+
+Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100.
 Proof. done. Qed.
 Global Instance from_and_sep_persistent_l P1 P2 :
-  PersistentP P1 → FromAnd (P1 ∗ P2) P1 P2 | 9.
+  PersistentP P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
 Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
-  PersistentP P2 → FromAnd (P1 ∗ P2) P1 P2 | 10.
+  PersistentP P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
 Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
-Global Instance from_and_pure φ ψ : @FromAnd M ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof. by rewrite /FromAnd pure_and. Qed.
-Global Instance from_and_always P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
-Global Instance from_and_later P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
-Global Instance from_and_laterN n P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd (▷^n P) (▷^n Q1) (▷^n Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite laterN_and. Qed.
-
-(* FromSep *)
-Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
-Proof. done. Qed.
+
+Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
+Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
+Global Instance from_and_always p P Q1 Q2 :
+  FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
+Proof.
+  intros. apply mk_from_and_and.
+  by rewrite always_and_sep_l' -always_sep -(from_and _ P).
+Qed.
+Global Instance from_and_later p P Q1 Q2 :
+  FromAnd p P Q1 Q2 → FromAnd p (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /FromAnd=> <-. destruct p; by rewrite ?later_and ?later_sep. Qed.
+Global Instance from_and_laterN p n P Q1 Q2 :
+  FromAnd p P Q1 Q2 → FromAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /FromAnd=> <-. destruct p; by rewrite ?laterN_and ?laterN_sep. Qed.
+
 Global Instance from_sep_ownM (a b1 b2 : M) :
   FromOp a b1 b2 →
-  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromSep -ownM_op from_op. Qed.
-
-Global Instance from_sep_pure φ ψ : @FromSep M ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof. by rewrite /FromSep pure_and sep_and. Qed.
-Global Instance from_sep_always P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
-Global Instance from_sep_later P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
-Global Instance from_sep_laterN n P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (▷^n P) (▷^n Q1) (▷^n Q2).
-Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
+  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_bupd P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
-Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
-
-Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → uPred M) x l :
-  FromSep ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
-Proof. by rewrite /FromSep big_sepL_cons. Qed.
-Global Instance from_sep_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
-  FromSep ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
+  FromAnd false P Q1 Q2 → FromAnd false (|==> P) (|==> Q1) (|==> Q2).
+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_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 /FromSep big_sepL_app. Qed.
+Proof. by rewrite /FromAnd big_sepL_app. Qed.
 
 (* FromOp *)
 Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a ⋅ b) a b.

theories/proofmode/classes.v

@@ -75,14 +75,14 @@ Class IntoWand {M} (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q.
 Arguments into_wand {_} _ _ _ {_}.
 Hint Mode IntoWand + ! - - : typeclass_instances.
 
-Class FromAnd {M} (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P.
-Arguments from_and {_} _ _ _ {_}.
-Hint Mode FromAnd + ! - - : typeclass_instances.
-
-Class FromSep {M} (P Q1 Q2 : uPred M) := from_sep : Q1 ∗ Q2 ⊢ P.
-Arguments from_sep {_} _ _ _ {_}.
-Hint Mode FromSep + ! - - : typeclass_instances.
-Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)
+Class FromAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
+  from_and : (if p then Q1 ∧ Q2 else Q1 ∗ Q2) ⊢ P.
+Arguments from_and {_} _ _ _ _ {_}.
+Hint Mode FromAnd + + ! - - : typeclass_instances.
+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.
 
 Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
   into_and : P ⊢ if p then Q1 ∧ Q2 else Q1 ∗ Q2.

theories/proofmode/coq_tactics.v

@@ -748,16 +748,17 @@ Proof.
 Qed.
 
 (** * Conjunction splitting *)
-Lemma tac_and_split Δ P Q1 Q2 : FromAnd P Q1 Q2 → (Δ ⊢ Q1) → (Δ ⊢ Q2) → Δ ⊢ P.
-Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
+Lemma tac_and_split Δ P Q1 Q2 :
+  FromAnd true P Q1 Q2 → (Δ ⊢ Q1) → (Δ ⊢ Q2) → Δ ⊢ P.
+Proof. intros. rewrite -(from_and true P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
 Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
-  FromSep P Q1 Q2 →
+  FromAnd false P Q1 Q2 →
   envs_split lr js Δ = Some (Δ1,Δ2) →
   (Δ1 ⊢ Q1) → (Δ2 ⊢ Q2) → Δ ⊢ P.
 Proof.
-  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
+  intros. rewrite envs_split_sound // -(from_and false P). by apply sep_mono.
 Qed.
 
 (** * Combining *)
@@ -770,8 +771,8 @@ Proof. done. Qed.
 Global Instance from_seps_singleton P : FromSeps P [P] | 1.
 Proof. by rewrite /FromSeps /= right_id. Qed.
 Global Instance from_seps_cons P P' Q Qs :
-  FromSeps P' Qs → FromSep P Q P' → FromSeps P (Q :: Qs) | 2.
-Proof. by rewrite /FromSeps /FromSep /= => ->. Qed.
+  FromSeps P' Qs → FromAnd false P Q P' → FromSeps P (Q :: Qs) | 2.
+Proof. by rewrite /FromSeps /FromAnd /= => ->. Qed.
 
 Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
   envs_lookup_delete_list js false Δ1 = Some (p, Ps, Δ2) →

theories/proofmode/tactics.v

@@ -674,7 +674,7 @@ Tactic Notation "iSplit" :=
   | |- _ ⊢ _ =>
     eapply tac_and_split;
       [apply _ ||
-       let P := match goal with |- FromAnd ?P _ _ => P end in
+       let P := match goal with |- FromAnd _ ?P _ _ => P end in
        fail "iSplit:" P "not a conjunction"| |]
   end.
 
@@ -683,7 +683,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
   let Hs := words Hs in
   eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
     [apply _ ||
-     let P := match goal with |- FromSep ?P _ _ => P end in
+     let P := match goal with |- FromAnd _ ?P _ _ => P end in
      fail "iSplitL:" P "not a separating conjunction"
     |env_reflexivity ||
      let Hs := iMissingHyps Hs in
@@ -695,7 +695,7 @@ Tactic Notation "iSplitR" constr(Hs) :=
   let Hs := words Hs in
   eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
     [apply _ ||
-     let P := match goal with |- FromSep ?P _ _ => P end in
+     let P := match goal with |- FromAnd _ ?P _ _ => P end in
      fail "iSplitR:" P "not a separating conjunction"
     |env_reflexivity ||
      let Hs := iMissingHyps Hs in

theories/tests/proofmode.v

@@ -169,3 +169,7 @@ Qed.
 Lemma test_frame_persistent (M : ucmraT) (P Q : uPred M) :
   □ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∧ Q ∨ Q).
 Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
+
+Lemma test_split_box (M : ucmraT) (P Q : uPred M) :
+  □ P -∗ □ (P ∗ P).
+Proof. iIntros "#?". by iSplit. Qed.