From 6326a24c399c422418a67ff888c0634c9d0ade3b Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 30 Jan 2016 11:20:18 +0100
Subject: [PATCH] =?UTF-8?q?since=20we=20use=20unicode,=20let's=20write=20L?=
 =?UTF-8?q?=C3=B6b's=20name=20correctly?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 modures/logic.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/modures/logic.v b/modures/logic.v
index 51aba5c32..336efd474 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -672,7 +672,7 @@ Proof.
   intros x [|n] ??; simpl in *; [done|].
   apply uPred_weaken with x (S n); eauto using cmra_valid_S.
 Qed.
-Lemma lub P : (▷ P → P) ⊑ P.
+Lemma löb P : (▷ P → P) ⊑ P.
 Proof.
   intros x n ? HP; induction n as [|n IH]; [by apply HP|].
   apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
@@ -709,6 +709,14 @@ Proof.
 Qed.
 Lemma later_wand P Q : ▷ (P -★ Q) ⊑ (▷ P -★ ▷ Q).
 Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
+Lemma löb_all_1 {A} (P Q : A → uPred M) :
+  (∀ a, (▷(∀ b, P b → Q b) ∧ P a) ⊑ Q a) → ∀ a, P a ⊑ Q a.
+Proof.
+  intros Hlöb a. apply impl_entails. transitivity (∀ a, P a → Q a)%I; last first.
+  { by rewrite (forall_elim _ a). } clear a.
+  etransitivity; last by eapply löb.
+  apply impl_intro_l, forall_intro=>a. rewrite right_id. by apply impl_intro_r.
+Qed.
 
 (* Always *)
 Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
-- 
GitLab