From a3f1b72ed94b72c376fe3ca560f4329b99827afc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Oct 2020 13:15:12 +0200
Subject: [PATCH] =?UTF-8?q?Counterexamples=20for=20Affine+EM=20and=20L?=
 =?UTF-8?q?=C3=B6b+EM.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/lib/counterexamples.v | 34 +++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index a9eaff530..f17156327 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -5,6 +5,40 @@ From iris Require Import options.
 (* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
+(** This proves that the combination of affinity [P ∗ Q ⊢ P] and the classical
+excluded-middle [P ∨ ¬P] axiom makes the separation conjunction trivial, i.e.,
+it gives [P -∗ P ∗ P]. *)
+Module affine_em. Section affine_em.
+  Context `{!BiAffine PROP}.
+  Context (em : ∀ P : PROP, ⊢ P ∨ ¬P).
+  Implicit Types P Q : PROP.
+
+  Lemma and_sep P Q : P ∧ Q -∗ P ∗ Q.
+  Proof using All.
+    iIntros "HPQ". iDestruct (em P) as "[HP|HnotP]".
+    - iFrame "HP". by iDestruct "HPQ" as "[_ HQ]".
+    - iExFalso. iApply "HnotP". by iDestruct "HPQ" as "[HP _]".
+  Qed.
+  Lemma sep_trivial P : P -∗ P ∗ P.
+  Proof using All. iIntros "HP". iApply and_sep; auto. Qed.
+End affine_em. End affine_em.
+
+(** This proves that the combination of Löb induction [(▷ P → P) ⊢ P] and the
+classical excluded-middle [P ∨ ¬P] axiom makes the later operator trivial, i.e.,
+it gives [â–· False]. *)
+Module löb_em. Section löb_em.
+  Context `{!BiLöb PROP}.
+  Context (em : ∀ P : PROP, ⊢ P ∨ ¬P).
+  Implicit Types P : PROP.
+
+  Lemma later_False : ⊢@{PROP} ▷ False.
+  Proof.
+    iDestruct (em (â–· False)%I) as "#[HP|HnotP]".
+    - done.
+    - iExFalso. iLöb as "IH". iSpecialize ("HnotP" with "IH"). done.
+  Qed.
+End löb_em. End löb_em.
+
 (** This proves that we need the â–· in a "Saved Proposition" construction with
 name-dependent allocation. *)
 Module savedprop. Section savedprop.
-- 
GitLab