From 7253dafb6c2b6df781e70d8ea1c83fb4719fe1d8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 May 2020 16:56:11 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20different=20versions=20of=20L=C3=B6b=20?=
 =?UTF-8?q?rule.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index 7f3d4bd4e..f62455a3b 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -108,6 +108,33 @@ Proof.
   rewrite impl_elim_r. done.
 Qed.
 
+Lemma löb_wand_intuitionistically `{!BiLöb PROP} P : □ (□ ▷ P -∗ P) ⊢ P.
+Proof.
+  rewrite -{3}(intuitionistically_elim P) -(löb (□ P)%I). apply impl_intro_l.
+  rewrite {1}intuitionistically_into_persistently_1 later_persistently.
+  rewrite persistently_and_intuitionistically_sep_l.
+  rewrite -{1}(intuitionistically_idemp (â–· P)%I) intuitionistically_sep_2.
+  by rewrite wand_elim_r.
+Qed.
+Lemma löb_wand `{!BiLöb PROP} P : □ (▷ P -∗ P) ⊢ P.
+Proof.
+  by rewrite -(intuitionistically_elim (▷ P)%I) löb_wand_intuitionistically.
+Qed.
+
+(** The proof of the right-to-left direction relies on the BI being affine. It
+is unclear how to generalize the lemma or proof to support non-affine BIs. *)
+Lemma löb_alt `{!BiAffine PROP} : BiLöb PROP ↔ ∀ P, □ (▷ P -∗ P) ⊢ P.
+Proof.
+  split; intros Hlöb P; [by apply löb_wand|].
+  rewrite bi.impl_alt. apply bi.exist_elim=> R. apply impl_elim_r'.
+  rewrite -(Hlöb (R → P)%I) -intuitionistically_into_persistently.
+  apply intuitionistically_intro', wand_intro_l, impl_intro_l.
+  rewrite -persistently_and_intuitionistically_sep_r assoc
+    persistently_and_intuitionistically_sep_r intuitionistically_elim.
+  rewrite -{1}(idemp bi_and R) -(assoc _ R) {2}(later_intro R).
+  by rewrite -later_and impl_elim_r (comm _ R) wand_elim_r.
+Qed.
+
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@bi_laterN PROP m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.
-- 
GitLab