From 2532b2363eabcdc77b927230288c0f024f0cb4a0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Wed, 23 Dec 2020 12:10:09 +0100
Subject: [PATCH 1/2] Fix issue #393: repair statement of
`fupd_plainly_laterN`.

iris/bi/updates.v  23 +++++++++
1 file changed, 9 insertions(+), 14 deletions()
diff git a/iris/bi/updates.v b/iris/bi/updates.v
index e63610cde..f17fc27db 100644
 a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ 463,13 +463,18 @@ Section fupd_derived.
Lemma fupd_plain_keep_r E P R `{!Plain P} : R ∗ (R ={E}=∗ P) ⊢ ={E}=> R ∗ P.
Proof. by rewrite {1}(plain P) fupd_plainly_keep_r. Qed.
+ Lemma fupd_plainly_laterN E n P : (▷^n ={E}=> ■ P) ⊢ ={E}=> ▷^n ◇ P.
+ Proof.
+ revert P. induction n as [n IH]=> P /=.
+ { by rewrite except_0_intro (fupd_plainly_elim E) fupd_trans. }
+ rewrite !later_laterN !laterN_later.
+ rewrite plainly_idemp fupd_plainly_later.
+ by rewrite except_0_plainly_1 later_plainly_1 IH except_0_later.
+ Qed.
Lemma fupd_plain_later E P `{!Plain P} : (▷ ={E}=> P) ⊢ ={E}=> ▷ ◇ P.
Proof. by rewrite {1}(plain P) fupd_plainly_later. Qed.
Lemma fupd_plain_laterN E n P `{!Plain P} : (▷^n ={E}=> P) ⊢ ={E}=> ▷^n ◇ P.
 Proof.
 induction n as [n IH]; simpl; [by rewrite except_0_intro].
 by rewrite IH fupd_plain_later except_0_laterN except_0_idemp.
 Qed.
+ Proof. by rewrite {1}(plain P) fupd_plainly_laterN. Qed.
Lemma fupd_plain_forall_2 E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
(∀ x, ={E}=> Φ x) ⊢ ={E}=> ∀ x, Φ x.
@@ 477,16 +482,6 @@ Section fupd_derived.
rewrite fupd_plainly_forall_2. apply forall_mono=> x.
by rewrite {1}(plain (Φ _)).
Qed.

 Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
 (▷^n ={E}=> P) ⊢ ={E}=> ▷^n ◇ P.
 Proof.
 revert P HP. induction n as [n IH]=> P ? /=.
  by rewrite except_0_intro.
  rewrite !later_laterN !laterN_later.
 rewrite fupd_plain_later. by rewrite IH except_0_later.
 Qed.

Lemma fupd_plain_forall E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
E2 ⊆ E1 →
(={E1,E2}=> ∀ x, Φ x) ⊣⊢ (∀ x, ={E1,E2}=> Φ x).

GitLab
From cccaa0119d32fda0c11a2e18dd80ef33bfcdc7ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Wed, 23 Dec 2020 12:11:31 +0100
Subject: [PATCH 2/2] CHANGELOG.

CHANGELOG.md  2 ++
1 file changed, 2 insertions(+)
diff git a/CHANGELOG.md b/CHANGELOG.md
index fdacba5fe..bcbf98373 100644
 a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ 73,6 +73,8 @@ HeapLang, which is now in a separate package `coqirisheaplang`.
been working properly for quite some time).
* Strengthen `persistent_sep_dup` to support propositions that are persistent
and either affine or absorbing.
+* Fix the statement of the lemma `fupd_plainly_laterN`; the old lemma was a
+ duplicate of `fupd_plain_laterN`.
**Changes in `proofmode`:**

GitLab