Enable proof mode to destruct non-separating conjunctions in spatial context.

This is allowed as long as one of the conjuncts is thrown away (i.e. is a
wildcard _ in the introduction pattern). It corresponds to the principle of
"external choice" in linear logic.

heap_lang/proofmode.v

@@ -11,9 +11,9 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
-Global Instance into_sep_mapsto l q v :
-  IntoSep false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoSep heap_mapsto_op_eq Qp_div_2. Qed.
+Global Instance into_and_mapsto l q v :
+  IntoAnd false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
+Proof. by rewrite /IntoAnd heap_mapsto_op_eq Qp_div_2. Qed.
 
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →

proofmode/class_instances.v

@@ -169,44 +169,44 @@ Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
   IntoOp a b1 b2 → IntoOp (Some a) (Some b1) (Some b2).
 Proof. by constructor. Qed.
 
-(* IntoSep *)
-Global Instance into_sep_sep p P Q : IntoSep p (P ★ Q) P Q.
-Proof. by apply mk_into_sep_sep. Qed.
-Global Instance into_sep_ownM p (a b1 b2 : M) :
+(* IntoAnd *)
+Global Instance into_and_sep p P Q : IntoAnd p (P ★ Q) P Q.
+Proof. by apply mk_into_and_sep. Qed.
+Global Instance into_and_ownM p (a b1 b2 : M) :
   IntoOp a b1 b2 →
-  IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. apply mk_into_sep_sep. by rewrite (into_op a) ownM_op. Qed.
+  IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) ownM_op. Qed.
 
-Global Instance into_sep_and P Q : IntoSep true (P ∧ Q) P Q.
+Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q.
 Proof. done. Qed.
-Global Instance into_sep_and_persistent_l P Q :
-  PersistentP P → IntoSep false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
-Global Instance into_sep_and_persistent_r P Q :
-  PersistentP Q → IntoSep false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
-
-Global Instance into_sep_later p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /IntoSep=>->. destruct p; by rewrite ?later_and ?later_sep. Qed.
-
-Global Instance into_sep_big_sepM
+Global Instance into_and_and_persistent_l P Q :
+  PersistentP P → IntoAnd false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed.
+Global Instance into_and_and_persistent_r P Q :
+  PersistentP Q → IntoAnd false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.
+
+Global Instance into_and_later p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?later_and ?later_sep. Qed.
+
+Global Instance into_and_big_sepM
     `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
-  (∀ k x, IntoSep p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
-  IntoSep p ([★ map] k ↦ x ∈ m, Φ k x)
+  (∀ k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  IntoAnd p ([★ map] k ↦ x ∈ m, Φ k x)
     ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
 Proof.
-  rewrite /IntoSep=> HΦ. destruct p.
+  rewrite /IntoAnd=> HΦ. destruct p.
   - apply and_intro; apply big_sepM_mono; auto.
     + intros k x ?. by rewrite HΦ and_elim_l.
     + intros k x ?. by rewrite HΦ and_elim_r.
   - rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
 Qed.
-Global Instance into_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
-  (∀ x, IntoSep p (Φ x) (Ψ1 x) (Ψ2 x)) →
-  IntoSep p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
+Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
+  (∀ x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) →
+  IntoAnd p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
 Proof.
-  rewrite /IntoSep=> HΦ. destruct p.
+  rewrite /IntoAnd=> HΦ. destruct p.
   - apply and_intro; apply big_sepS_mono; auto.
     + intros x ?. by rewrite HΦ and_elim_l.
     + intros x ?. by rewrite HΦ and_elim_r.

proofmode/classes.v

@@ -32,12 +32,12 @@ Global Arguments from_and : clear implicits.
 Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 ★ Q2 ⊢ P.
 Global Arguments from_sep : clear implicits.
 
-Class IntoSep (p : bool) (P Q1 Q2 : uPred M) :=
-  into_sep : P ⊢ if p then Q1 ∧ Q2 else Q1 ★ Q2.
-Global Arguments into_sep : clear implicits.
+Class IntoAnd (p : bool) (P Q1 Q2 : uPred M) :=
+  into_and : P ⊢ if p then Q1 ∧ Q2 else Q1 ★ Q2.
+Global Arguments into_and : clear implicits.
 
-Lemma mk_into_sep_sep p P Q1 Q2 : (P ⊢ Q1 ★ Q2) → IntoSep p P Q1 Q2.
-Proof. rewrite /IntoSep=>->. destruct p; auto using sep_and. Qed.
+Lemma mk_into_and_sep p P Q1 Q2 : (P ⊢ Q1 ★ Q2) → IntoAnd p P Q1 Q2.
+Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
 
 Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
 Global Arguments into_op {_} _ _ _ {_}.

proofmode/coq_tactics.v

@@ -652,15 +652,29 @@ Proof.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
-Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
-  envs_lookup i Δ = Some (p, P) → IntoSep p P P1 P2 →
+Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
+  envs_lookup i Δ = Some (p, P) → IntoAnd p P P1 P2 →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_sep p P).
+  intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
   by destruct p; rewrite /= ?right_id (comm _ P1) ?always_and_sep wand_elim_r.
 Qed.
 
+(* Using this tactic, one can destruct a (non-separating) conjunction in the
+spatial context as long as one of the conjuncts is thrown away. It corresponds
+to the principle of "external choice" in linear logic. *)
+Lemma tac_and_destruct_choice Δ Δ' i p (lr : bool) j P P1 P2 Q :
+  envs_lookup i Δ = Some (p, P) → IntoAnd true P P1 P2 →
+  envs_simple_replace i p (Esnoc Enil j (if lr then P1 else P2)) Δ = Some Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q.
+Proof.
+  intros. rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id (into_and true P). destruct lr.
+  - by rewrite and_elim_l wand_elim_r.
+  - by rewrite and_elim_r wand_elim_r.
+Qed.
+
 (** * Framing *)
 Lemma tac_frame Δ Δ' i p R P Q :
   envs_lookup_delete i Δ = Some (p, R, Δ') → Frame R P Q →

proofmode/ghost_ownership.v

@@ -6,9 +6,9 @@ Section ghost.
 Context `{inG Σ A}.
 Implicit Types a b : A.
 
-Global Instance into_sep_own p γ a b1 b2 :
-  IntoOp a b1 b2 → IntoSep p (own γ a) (own γ b1) (own γ b2).
-Proof. intros. apply mk_into_sep_sep. by rewrite (into_op a) own_op. Qed.
+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 b :
   FromSep (own γ (a ⋅ b)) (own γ a) (own γ b) | 90.
 Proof. by rewrite /FromSep own_op. Qed.

proofmode/tactics.v

@@ -363,7 +363,7 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
     |let P := match goal with |- IntoOr ?P _ _ => P end in
-     apply _ || fail "iOrDestruct:" P "not a disjunction"
+     apply _ || fail "iOrDestruct: cannot destruct" P
     |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
     |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].
 
@@ -395,12 +395,19 @@ Tactic Notation "iSplitR" constr(Hs) :=
 Tactic Notation "iSplitL" := iSplitR "".
 Tactic Notation "iSplitR" := iSplitL "".
 
-Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
-  eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
-    [env_cbv; reflexivity || fail "iSepDestruct:" H "not found"
-    |let P := match goal with |- IntoSep _ ?P _ _ => P end in
-     apply _ || fail "iSepDestruct:" P "not separating destructable"
-    |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].
+Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
+  eapply tac_and_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
+    [env_cbv; reflexivity || fail "iAndDestruct:" H "not found"
+    |let P := match goal with |- IntoAnd _ ?P _ _ => P end in
+     apply _ || fail "iAndDestruct: cannot destruct" P
+    |env_cbv; reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|].
+
+Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H') :=
+  eapply tac_and_destruct_choice with _ H _ lr H' _ _ _;
+    [env_cbv; reflexivity || fail "iAndDestruct:" H "not found"
+    |let P := match goal with |- IntoAnd _ ?P _ _ => P end in
+     apply _ || fail "iAndDestruct: cannot destruct" P
+    |env_cbv; reflexivity || fail "iAndDestruct:" H' " not fresh"|].
 
 Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
   eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
@@ -480,7 +487,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
   eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
     [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
     |let P := match goal with |- IntoExist ?P _ => P end in
-     apply _ || fail "iExistDestruct:" P "not an existential"|];
+     apply _ || fail "iExistDestruct: cannot destruct" P|];
   let y := fresh in
   intros y; eexists; split;
     [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
@@ -501,7 +508,7 @@ Tactic Notation "iNext":=
 Tactic Notation "iTimeless" constr(H) :=
   eapply tac_timeless with _ H _ _ _;
     [let Q := match goal with |- IsNowTrue ?Q => Q end in
-     apply _ || fail "iTimeless: cannot remove later of timeless hypothesis in goal" Q
+     apply _ || fail "iTimeless: cannot remove later when goal is" Q
     |env_cbv; reflexivity || fail "iTimeless:" H "not found"
     |let P := match goal with |- IntoNowTrue ?P _ => P end in
      apply _ || fail "iTimeless:" P "not timeless"
@@ -531,8 +538,10 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
     | IFrame => iFrame Hz
     | IName ?y => iRename Hz into y
     | IList [[]] => iExFalso; iExact Hz
+    | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as true Hz; go Hz pat1
+    | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as false Hz; go Hz pat2
     | IList [[?pat1; ?pat2]] =>
-       let Hy := iFresh in iSepDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
+       let Hy := iFresh in iAndDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
     | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
     | IPureElim => iPure Hz as ?
     | IAlwaysElim ?pat => iPersistent Hz; go Hz pat

tests/proofmode.v

@@ -81,12 +81,15 @@ Proof.
   by iIntros "# _".
 Qed.
 
+Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ★ (Q1 ∧ Q2) ⊢ P ★ Q1.
+Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
+
 Section iris.
   Context `{irisG Λ Σ}.
   Implicit Types E : coPset.
   Implicit Types P Q : iProp Σ.
 
-  Lemma demo_7 N E P Q R :
+  Lemma demo_8 N E P Q R :
     nclose N ⊆ E →
     (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q ={E}=★ R.
   Proof.