Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-07-19T15:06:26Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/470Overeager simplification in 'iIntros' and 'iSplit'2022-07-19T15:06:26ZRalf Jungjung@mpi-sws.orgOvereager simplification in 'iIntros' and 'iSplit'Consider the following lemma:
```
Lemma lc_test n m :
£ (S n + m) -∗ £ (S n).
Proof.
iIntros "[Hlc1 Hlc2]".
```
I would expect the state after this script to be such that `Hlc1` is `£ (S n)`, such that `iExact "Hlc1"` finishe...Consider the following lemma:
```
Lemma lc_test n m :
£ (S n + m) -∗ £ (S n).
Proof.
iIntros "[Hlc1 Hlc2]".
```
I would expect the state after this script to be such that `Hlc1` is `£ (S n)`, such that `iExact "Hlc1"` finishes the proof. However, the state we actually get is this:
```
"Hlc1" : £ 1
"Hlc2" : £
((fix add (n0 m0 : nat) {struct n0} : nat :=
match n0 with
| 0 => m0
| S p => S (add p m0)
end) n m)
```
That is clearly terrible -- something in the IPM simplification machinery seems to be going wrong...
(The workaround is to `rewrite lc_split` so that simplification has no chance of kicking in.)https://gitlab.mpi-sws.org/iris/iris/-/issues/461Universe problem: AU cannot use telescopes quantified at Iris level2022-06-08T13:45:51ZHai DangUniverse problem: AU cannot use telescopes quantified at Iris levelThis is a regression from `dev.2022-05-06.0.7b9f809f` to `dev.2022-05-06.1.1414d84`, by !781
The following snippet shows the problem. `AU_fail` is accepted in `dev.2022-05-06.0.7b9f809f` but not in `dev.2022-05-06.1.1414d84`.
I tried p...This is a regression from `dev.2022-05-06.0.7b9f809f` to `dev.2022-05-06.1.1414d84`, by !781
The following snippet shows the problem. `AU_fail` is accepted in `dev.2022-05-06.0.7b9f809f` but not in `dev.2022-05-06.1.1414d84`.
I tried putting `Unset Universe Minimization ToSet` in `bi.lib.atomic` as well as locally, but that didn't help.
```coq
Require Import stdpp.coPset.
Require Import iris.bi.telescopes.
Require Import iris.bi.lib.atomic.
Section definition.
Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
Definition AU_succeed (TA TB : tele) : Prop :=
⊢ ∀ (α : TA → PROP) (β Φ : TA → TB → PROP),
atomic_update Eo Ei α β Φ.
Fail Definition AU_fail : Prop :=
⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
atomic_update Eo Ei α β Φ.
End definition.
```
This is the error message:
```
In environment
PROP : bi
H : BiFUpd PROP
TA : tele
TB : tele
Eo, Ei : coPset
TA0 : tele
TB0 : tele
α : TA0 → PROP
β : TA0 → TB0 → PROP
Φ : TA0 → TB0 → PROP
The term "α" has type "forall _ : tele_arg@{tests.62} TA0, bi_car PROP"
while it is expected to have type
"forall _ : tele_arg@{iris.bi.lib.atomic.94} ?TA, bi_car ?PROP5".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/459Inconsistency in weakening of modalities in `iApply`2022-04-20T14:59:17ZRobbert KrebbersInconsistency in weakening of modalities in `iApply````coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens...```coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens is that the first (and failing) `iApply` directly attempts to find an `IntoWand` instance to match the conclusion of the wand with the goal. This fails because the only applicable `IntoWand` instance is:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
There is no `FromAssumption` for `Q`, so no weakening of the conclusion is performed.
In the second attempt, `iApply` will first `iSpecialize` with the wand. As such, it tries to find an `IntoWand` instance where the conclusion can be unified with an evar. Then after that, it will use `iAssumption`, which uses `FromAssumption` to weaken the modality.
## Solution
We probably should add `FromAssumption` to instances like `into_wand_wand`. I do not know if this was just an omission, or there's a reason for that. Should try.https://gitlab.mpi-sws.org/iris/iris/-/issues/452"wp_apply ... as"2023-03-18T17:54:27ZRalf Jungjung@mpi-sws.org"wp_apply ... as"Applying a typical spec in Iris usually looks something like this:
```
wp_apply (Spec with "...").
{ (* solve precondition *) }
iIntros (x) "H".
```
The `iIntros` can be quite far removed from the `wp_apply`, if proving the precondition ...Applying a typical spec in Iris usually looks something like this:
```
wp_apply (Spec with "...").
{ (* solve precondition *) }
iIntros (x) "H".
```
The `iIntros` can be quite far removed from the `wp_apply`, if proving the precondition takes some work. Also it seems a bit odd to have this separated into two tactics.
@robbertkrebbers I wonder how feasible it would be to support `wp_apply (Spec with "...") as ...`, combining the `iIntros` into the `wp_apply`? I have actually accidentally written this last week and was a bit bummed that it did not work. ;)https://gitlab.mpi-sws.org/iris/iris/-/issues/443Please create a tag for Coq 8.15 in Coq Platform 2022.022022-01-24T09:07:09ZMichael SoegtropPlease create a tag for Coq 8.15 in Coq Platform 2022.02The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an excep...The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.5.0) does not work with Coq 8.15.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
bb946806c5aa9bcb8184a8cb3bc1befecc0322a0 on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.15, preferably before February 14, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before January 25, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.15.0.
The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/193Tej Chajedtchajed@gmail.comTej Chajedtchajed@gmail.comhttps://gitlab.mpi-sws.org/iris/iris/-/issues/437Typo in documentation2021-10-26T19:12:53ZAlexandre MoineTypo in documentationHi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two l...Hi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two lines. This seems to be the only occurrencehttps://gitlab.mpi-sws.org/iris/iris/-/issues/436opam package description is not helpful2021-10-26T21:59:09ZMichael Soegtropopam package description is not helpfulThe package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_l...The package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
```
The description should more elaborate on the question what this can be used for.
See (https://coq.inria.fr/opam/released/packages/coq-iris/coq-iris.3.4.0/opam)
See (https://coq.inria.fr/opam/released/packages/coq-iris-heap-lang/coq-iris-heap-lang.3.4.0/opam)
Please note that (afaik) it is no issue to change the description of opam packages without creating a new version.https://gitlab.mpi-sws.org/iris/iris/-/issues/435Please create a tag for Coq 8.14 in Coq Platform 2021.112021-11-14T18:33:05ZMichael SoegtropPlease create a tag for Coq 8.14 in Coq Platform 2021.11The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of di...The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.4.0) does not work with Coq 8.14+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
ee6a36b3e803ebec465bf44bb5bcbf9b19fe6b62 on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag, or communicate us any existing tag that works with Coq branch v8.14, preferably before November 15, 2021?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
The working branch of Coq Platform, which already supports Coq version 8.14+rc1, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/139https://gitlab.mpi-sws.org/iris/iris/-/issues/432iApply "auto frame": bad error message2021-09-06T06:47:59ZRalf Jungjung@mpi-sws.orgiApply "auto frame": bad error messageThe following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable t...The following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable tactic.
```
There is a `fail "iSpecialize: premise cannot be solved by framing"` in the tactic code but that does not seem to work.https://gitlab.mpi-sws.org/iris/iris/-/issues/430iInduction does not work well for induction principles involving `Forall`2022-02-11T10:28:24ZRalf Jungjung@mpi-sws.orgiInduction does not work well for induction principles involving `Forall`Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind...Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind`, where `expr_ind` is a custom induction principle that uses `Forall` to handle nested lists.
Here's a self-contained testcase:
```coq
Inductive tree (T : Type) := Tree : list (tree T) → tree T.
Arguments Tree {T}.
Lemma tree_ind' T (P : tree T → Prop) :
(∀ l, Forall P l → P (Tree l)) →
∀ t, P t.
Proof.
intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
induction l as [|t l IH].
{ constructor. }
constructor; last apply IH.
apply REC.
Qed.
Lemma test_iInduction_Forall (t : tree nat) (P : PROP) : ⊢ P.
Proof. iInduction t as [] "IH" using tree_ind'.
```
This shows a goal
```
PROP : bi
l : list (tree nat)
P : PROP
============================
"IH" : <pers> ?P
--------------------------------------□
P
```
An `unshelve` shows that the `IntoIH` simply was not resolved, which seems like a bug in its own right -- `iInduction` should fail in that case.
In fact this testcase is interesting in the sense that even adding the instance from Simuliris (even after getting rid of the `BiAffine` assumption) does not help:
```coq
Section tactics.
Import iris.bi.bi.
Import iris.proofmode.base environments classes modality_instances.
Import bi.
Import env_notations.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
Import coq_tactics.
Local Instance into_ih_Forall {A} (φ : A → Prop) (l : list A) Δ Φ :
(∀ x, x ∈ l → IntoIH (φ x) Δ (Φ x)) → IntoIH (Forall φ l) Δ (∀ x, ⌜x ∈ l⌝ → Φ x) | 2.
Proof.
rewrite /IntoIH Forall_forall => HΔ Hf. apply forall_intro=> x.
iIntros "Henv %Hl". iApply (HΔ with "Henv"); eauto.
Qed.
End tactics.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/421Bad error message for failing iInduction2021-06-14T13:59:19ZRalf Jungjung@mpi-sws.orgBad error message for failing iInductionI am not sure what is going wrong with the following `iInduction`, and IPM's error doesn't tell me:
```
Inductive val :=
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Lemma test {Σ} (val_rel : val → val → iProp Σ) v_t...I am not sure what is going wrong with the following `iInduction`, and IPM's error doesn't tell me:
```
Inductive val :=
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Lemma test {Σ} (val_rel : val → val → iProp Σ) v_t v_s :
val_rel v_t v_s -∗ True.
Proof. iInduction v_t as [| |] "IH" forall v_s.
(* Error: No matching clauses for match. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/415Tracking issue for append-only list RA2021-11-22T17:58:29ZRalf Jungjung@mpi-sws.orgTracking issue for append-only list RAThis is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Op...This is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Do we really want notation for the mono_list algebra elements? The main "pro" reason here is that `dfrac` otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation
and add them on-demand.
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use. This is discussed in more generality at https://gitlab.mpi-sws.org/iris/iris/-/issues/412.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/414Tracking issue for monotone RA2023-09-11T07:41:21ZRalf Jungjung@mpi-sws.orgTracking issue for monotone RAThis is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open iss...This is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* How should the RA be called? `monotone` is a very general term, it would be good to find something more specific. Currently it is called `mra` which is short but cryptic. `principal` should then likely become `mra_principal` and all lemmas be prefixed with `mra` as well.
* Do a solid review of the API surface.
Cc @amintimany @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/409Proposed change to naming convention for "dataful" `*G`s2021-06-03T09:08:26ZRalf Jungjung@mpi-sws.orgProposed change to naming convention for "dataful" `*G`sSome of our `*G` typeclasses are different than others: they contain not just `inG` but actual relevant data; usually a `gname` but in the case of `irisG` also some further information about how the Iris program logic is being instantiat...Some of our `*G` typeclasses are different than others: they contain not just `inG` but actual relevant data; usually a `gname` but in the case of `irisG` also some further information about how the Iris program logic is being instantiated. These dataful classes come with a `*PreG` that represent their `inG` (dataless) part.
Dataful `*G`s need to be treated differently, e.g. they have special initialization lemmas and they should not be bundled in library's `*G` as that leads to duplication of said data. So I propose to adjust our naming convention such that one can tell from the name whether a `*G` is dataful or not.
The new naming convention is up for bikeshedding; here are some proposals coming to my mind:
1. We call the dataful class `*DataG` and its `inG`-only part `*G`. So e.g. `heapG` → `heapDataG` and `heapPreG` → `heapG`.
2. We call the dataful class `*DataG` and its `inG`-only part `*PreG`. So e.g. `heapG` → `heapDataG`; `heapPreG` stays.
2. We call the dataful class `*DG` and its `inG`-only part `*PreG`. So e.g. `heapG` → `heapDG`; `heapPreG` stays.
I think I prefer (2) or (3) over (1) because it prevents confusion due to accidentally using the `inG`-only part, and also because it is easier for migration since we don't reuse an old name for a different purpose.
@robbertkrebbers @tchajed @jtassaro what do you think?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/408bi.weakestpre imports a module from program_logic2021-06-18T13:09:56ZRalf Jungjung@mpi-sws.orgbi.weakestpre imports a module from program_logic`bi.weakestpre` imports `program_logic.language`, which is a layering violation. We should somehow fix this, either by breaking the dependency or by moving one of the two modules to the other side.`bi.weakestpre` imports `program_logic.language`, which is a layering violation. We should somehow fix this, either by breaking the dependency or by moving one of the two modules to the other side.https://gitlab.mpi-sws.org/iris/iris/-/issues/404Make string-ident a standard part of Iris2021-03-24T11:03:52ZLennard Gähergaeher@mpi-sws.orgMake string-ident a standard part of IrisSince support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this w...Since support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this would have the benefits of
* not having to explicitly require the user to install the plugin in developments using Iris,
* and thus be beneficial to overall code quality of developments using Iris (since there would be a clear argument for using the new intro pattern instead of using auto-generated names).
@jung suggested I create an issue for this.https://gitlab.mpi-sws.org/iris/iris/-/issues/403Iris 3.42021-03-06T12:22:13ZRalf Jungjung@mpi-sws.orgIris 3.4There was a Coq 8.13 release, so following our promise for the Coq Platform, we should make a compatible release ASAP (the Coq release was already more than a month ago).
[Milestone with potential release blockers](https://gitlab.mpi-sw...There was a Coq 8.13 release, so following our promise for the Coq Platform, we should make a compatible release ASAP (the Coq release was already more than a month ago).
[Milestone with potential release blockers](https://gitlab.mpi-sws.org/iris/iris/-/milestones/6)https://gitlab.mpi-sws.org/iris/iris/-/issues/401wp_bind does not report a failure message2021-03-05T17:25:13ZTej Chajedtchajed@gmail.comwp_bind does not report a failure messageThe `first [ t1 | fail ]` here is incorrect: https://gitlab.mpi-sws.org/iris/iris/-/blob/4c96a5043ab4f648f4082f2398888c879efd3c36/iris_heap_lang/proofmode.v#L200
```coq
first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind...The `first [ t1 | fail ]` here is incorrect: https://gitlab.mpi-sws.org/iris/iris/-/blob/4c96a5043ab4f648f4082f2398888c879efd3c36/iris_heap_lang/proofmode.v#L200
```coq
first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
| fail "wp_bind: cannot find" efoc "in" e ]
```
The failure causes the entire construct to fail with a generic error message; what was intended is `fail 1` to bubble it up. Furthermore there's no test of this failure.
This bug was originally reported by François Pottier against https://github.com/tchajed/iris-simp-lang/, which inherited this bug from heap_lang.Tej Chajedtchajed@gmail.comTej Chajedtchajed@gmail.comhttps://gitlab.mpi-sws.org/iris/iris/-/issues/395Generalize frac to dfrac in view camera2021-03-03T16:01:46ZSimon Friis VindumGeneralize frac to dfrac in view cameraThe use of `frac` in the view camera could be generalized to `dfrac`. This would make it possible to "freeze" or persist the authorative element. I don't have a use case for this myself, but, if I recall correctly, @jung or @tchajed had ...The use of `frac` in the view camera could be generalized to `dfrac`. This would make it possible to "freeze" or persist the authorative element. I don't have a use case for this myself, but, if I recall correctly, @jung or @tchajed had one?
The notation would be the same as for the points-to predicate, and in the future the custom entries `dfrac` notation could be reused for this. The view camera is rather new, so breaking changes here are less critical, and it thus seems like a fine place to start with regards to trying to use `dfrac` more.
What do you think? I'd like to work on this if there is support.https://gitlab.mpi-sws.org/iris/iris/-/issues/393fupd_plainly_laterN = fupd_plain_laterN ?2020-12-23T11:12:46ZPaolo G. Giarrussofupd_plainly_laterN = fupd_plain_laterN ?It seems `fupd_plainly_laterN` is a misnamed copy of `fupd_plain_laterN`. I confirmed this by giving the following proof to the existing statement:
```coq
Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
(▷^n |={E}=> P) ⊢ |={...It seems `fupd_plainly_laterN` is a misnamed copy of `fupd_plain_laterN`. I confirmed this by giving the following proof to the existing statement:
```coq
Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
(▷^n |={E}=> P) ⊢ |={E}=> ▷^n ◇ P.
Proof. exact: fupd_plain_laterN. Qed.
```
I'm happy to leave the fix to anybody else.