From dcf62c10a42c995034d9e622693003a214104699 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Thu, 1 Jun 2023 12:08:46 +0200
Subject: [PATCH] Added `MakeOr` and `MakeAnd` instances for `False`.

---
 iris/proofmode/class_instances_make.v |  8 ++++++++
 tests/proofmode.ref                   | 20 ++++++++++++++++++++
 tests/proofmode.v                     | 23 +++++++++++++++++++++--
 3 files changed, 49 insertions(+), 2 deletions(-)

diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index a6fc44e18..ce592a54f 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -62,6 +62,10 @@ Global Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
 Proof. apply emp_and. Qed.
 Global Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
 Proof. apply and_emp. Qed.
+Global Instance make_and_false_l P : KnownLMakeAnd False P False.
+Proof. apply left_absorb, _. Qed.
+Global Instance make_and_false_r P : KnownRMakeAnd P False False.
+Proof. by rewrite /KnownRMakeAnd /MakeAnd right_absorb. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
 
@@ -74,6 +78,10 @@ Global Instance make_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
 Proof. apply emp_or. Qed.
 Global Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
 Proof. apply or_emp. Qed.
+Global Instance make_or_false_l P : KnownLMakeOr False P P.
+Proof. apply left_id, _. Qed.
+Global Instance make_or_false_r P : KnownRMakeOr P False P.
+Proof. by rewrite /KnownRMakeOr /MakeOr right_id. Qed.
 Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
 Proof. by rewrite /MakeOr. Qed.
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3520a7b0b..5d08d96a1 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -269,6 +269,17 @@ Tactic failure: iSpecialize: Q not persistent.
      : string
 The command has indeed failed with message:
 Tactic failure: iSpecialize: (|==> P)%I not persistent.
+"test_iFrame_conjunction_3"
+     : string
+1 goal
+  
+  PROP : bi
+  P, Q : PROP
+  Absorbing0 : Absorbing Q
+  ============================
+  "HQ" : Q
+  --------------------------------------∗
+  False
 "test_iFrame_affinely_emp"
      : string
 1 goal
@@ -308,6 +319,15 @@ Tactic failure: iSpecialize: (|==> P)%I not persistent.
   ============================
   --------------------------------------∗
   ▷ (∃ x : nat, emp ∧ ⌜x = 0⌝ ∨ emp)
+"test_iFrame_or_3"
+     : string
+1 goal
+  
+  PROP : bi
+  P1, P2, P3 : PROP
+  ============================
+  --------------------------------------∗
+  ▷ (∃ x : nat, ⌜x = 0⌝)
 "test_iFrame_or_affine_1"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f7008326a..2326056ad 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -44,10 +44,10 @@ Proof.
   (* To test destruct: can also be part of the intro-pattern *)
   iDestruct "foo" as "[_ meh]".
   repeat iSplit; [|by iLeft|iIntros "#[]"].
-  iFrame "H2".
+  iFrame "H2". (* also simplifies the [∧ False] and [∨ False] *)
   (* split takes a list of hypotheses just for the LHS *)
   iSplitL "H3".
-  - iFrame "H3". iRight. auto.
+  - by iFrame "H3".
   - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
 Qed.
 
@@ -654,6 +654,15 @@ Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 Lemma test_iFrame_conjunction_2 P Q :
   P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
 Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+Check "test_iFrame_conjunction_3".
+Lemma test_iFrame_conjunction_3 P Q `{!Absorbing Q} :
+  P -∗ Q -∗ ((P ∗ False) ∧ Q).
+Proof.
+  iIntros "HP HQ".
+  iFrame "HP".
+  (* [iFrame] should simplify [False ∧ Q] to just [False]. *)
+  Show.
+Abort.
 
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.
@@ -707,6 +716,16 @@ Proof.
   is not simplified to [emp]. *)
   iExists 0. auto.
 Qed.
+Check "test_iFrame_or_3".
+Lemma test_iFrame_or_3 P1 P2 P3 :
+  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ (False ∗ P3)).
+Proof.
+  iIntros "($ & $ & $)".
+  Show. (* After framing [P3], the disjunction becomes [⌜x = 0⌝ ∨ False].
+  The simplification of disjunctions by [iFrame] will now get rid of the
+  [∨ False], to just [⌜x = 0⌝] *)
+  by iExists 0.
+Qed.
 Check "test_iFrame_or_affine_1".
 Lemma test_iFrame_or_affine_1 `{!BiAffine PROP} P1 P2 P3 :
   P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ P3).
-- 
GitLab