From 907940283759a66c43f23b1d1213fd0d7f8eda91 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Nov 2020 13:06:01 +0100
Subject: [PATCH] Rename `mono_nat_own_update_with_lb` into
 `mono_nat_own_update`.

Remove the weaker version with the `_lb` since the stronger version is just
as easy to use in the proofmode.
---
 iris/base_logic/lib/mono_nat.v | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 7a725a90a..edb87d413 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -102,17 +102,13 @@ Section mono_nat.
     auto with iFrame.
   Qed.
 
-  Lemma mono_nat_own_update n' γ n :
-    n ≤ n' →
-    mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n'.
-  Proof. unseal. intros. by apply own_update, mono_nat_update. Qed.
-
-  Lemma mono_nat_own_update_with_lb γ n n' :
+  Lemma mono_nat_own_update γ n n' :
     n ≤ n' →
     mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n' ∗ mono_nat_lb_own γ n'.
   Proof.
-    iIntros (Hlb) "Hauth".
-    iMod (mono_nat_own_update n' with "Hauth") as "Hauth"; auto.
-    iDestruct (mono_nat_lb_own_get with "Hauth") as "#Hlb"; auto.
+    iIntros (?) "Hauth".
+    iAssert (mono_nat_auth_own γ 1 n') with "[> Hauth]" as "Hauth".
+    { unseal. iApply (own_update with "Hauth"). by apply mono_nat_update. }
+    iModIntro. iSplit; [done|]. by iApply mono_nat_lb_own_get.
   Qed.
 End mono_nat.
-- 
GitLab