From b05be077242eee1b42433e94216f64bc681a61a9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Nov 2020 12:28:47 +0100
Subject: [PATCH] bupd, fupd: add idempotence lemmas

---
 iris/bi/updates.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 65b06d251..0dc792e34 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -184,6 +184,12 @@ Section bupd_derived.
   Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
   Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q.
   Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
+  Lemma bupd_idemp P : (|==> |==> P) ⊣⊢ |==> P.
+  Proof.
+    apply: anti_symm.
+    - apply bupd_trans.
+    - apply bupd_intro.
+  Qed.
 
   Global Instance bupd_homomorphism :
     MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (bupd (PROP:=PROP)).
@@ -245,6 +251,12 @@ Section fupd_derived.
   Proof. exact: fupd_intro_mask. Qed.
   Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
   Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
+  Lemma fupd_idemp E P : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P.
+  Proof.
+    apply: anti_symm.
+    - apply fupd_trans.
+    - apply fupd_intro.
+  Qed.
 
   Lemma fupd_frame_l E1 E2 R Q : (R ∗ |={E1,E2}=> Q) ={E1,E2}=∗ R ∗ Q.
   Proof. rewrite !(comm _ R); apply fupd_frame_r. Qed.
-- 
GitLab