From 9a6976e26a513ed1e56feb9a1f091b342ac025fa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Oct 2020 20:05:04 +0200
Subject: [PATCH] =?UTF-8?q?prove=20a=20funny=20consequence=20of=20L=C3=B6b?=
 =?UTF-8?q?=20induction?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/derived_laws_later.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index 06084c0be..a683467de 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -165,6 +165,12 @@ Proof.
   by rewrite -later_and impl_elim_r (comm _ R) wand_elim_r.
 Qed.
 
+(** A funny consequence of Löb induction.
+This shows that Löb induction is incompatible with classical logic.
+See [lib/counterexamples.v] for a fully worked-out proof of that fact. *)
+Lemma not_not_later_False `{!BiLöb PROP} : ⊢@{PROP} ¬ ¬ ▷ False.
+Proof. apply entails_impl, löb. Qed.
+
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@bi_laterN PROP m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.
-- 
GitLab