From 8481b20b40d3d22d38d6273d171d60926a76772f Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 8 May 2018 12:57:44 +0200
Subject: [PATCH] =?UTF-8?q?extend=20L=C3=B6b=20proof=20comment?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
theories/bi/derived_laws_sbi.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 8b40c1ed..d1afdc56 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -204,7 +204,8 @@ Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
Section löb.
- (* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem *)
+ (* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
+ Their Ψ is called Q in our proof. *)
Lemma weak_löb P : (▷ P ⊢ P) → (True ⊢ P).
Proof.
pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).
--
GitLab