Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2024-03-24T14:54:23Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/569Add some sort of rule for `own ∧ own`2024-03-24T14:54:23ZRalf Jungjung@mpi-sws.orgAdd some sort of rule for `own ∧ own`The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v)...The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v).)
Amin suggested [something similar](https://mattermost.mpi-sws.org/iris/pl/tcsex43cn7d5ij5qwkk39ftd7h) a long time ago.
Not sure which formulation works best, but we should have something like that. :)
Whatever the rule is, it should be strong enough to prove things like
```
Lemma pointsto_and_sep (l1 l2:loc) (v1 v2:val) :
l1 ≠ l2 ->
l1 ↦ v1 ∧ l2 ↦ v2 -∗
l1 ↦ v1 ∗ l2 ↦ v2.
Lemma pointsto_and_eq l x y :
l ↦ x ∧ l ↦ y -∗ ⌜x = y⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/567[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-19T16:06:15ZRomain Tetley[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.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
7c5ce0d556f4e03f27ddc6463462bf4040f5103d 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.19, **preferably before March 31st, 2024**?
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 March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
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/405https://gitlab.mpi-sws.org/iris/iris/-/issues/564Make iFrame also instantiate telescopic existential quantifiers2024-02-19T09:40:25ZIke MulderMake iFrame also instantiate telescopic existential quantifiersFollow up on !1017: it should be possible to extend the technique for instantiating existential quantifiers to also work on telescopic quantifications `∃.. x`.
The initial attempt worked partly:
```
Global Instance frame_texist {TT : t...Follow up on !1017: it should be possible to extend the technique for instantiating existential quantifiers to also work on telescopic quantifications `∃.. x`.
The initial attempt worked partly:
```
Global Instance frame_texist {TT : tele@{bi.Quant}} p R (Φ : TT → PROP)
(C : tele@{bi.Quant}) (g : C → TT) (Ψ : C → PROP) Q :
(∀ c, FrameExistRequirements p R Φ (g c) (Ψ c)) →
TCCbnSimplTele (∃.. c, Ψ c)%I Q →
Frame p R (∃.. x, Φ x) Q.
Proof.
move=> H HQ. rewrite /FrameTExists /Frame (bi_texist_exist Φ).
by eapply frame_exist.
Qed.
```
but this turns a telescopic quantifier into a regular one whenever things get framed beneath it.
We did not yet figure out a nice way to fix this.https://gitlab.mpi-sws.org/iris/iris/-/issues/561Use `#[local] field ::` to make `inG` instances local2024-02-05T17:23:10ZRobbert KrebbersUse `#[local] field ::` to make `inG` instances localNow that support for Coq 8.17 has been dropped, we can make use of `#[local] field ::` in `Class` declarations ~~which by default appears to be `Local`~~. This would be a better fix for https://gitlab.mpi-sws.org/iris/iris/-/merge_reques...Now that support for Coq 8.17 has been dropped, we can make use of `#[local] field ::` in `Class` declarations ~~which by default appears to be `Local`~~. This would be a better fix for https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/780
See also https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1030https://gitlab.mpi-sws.org/iris/iris/-/issues/560Fix the future-coercion-class-field warnings2024-02-06T08:38:06ZRalf Jungjung@mpi-sws.orgFix the future-coercion-class-field warningsWe are getting tons of these, and I expect even more in our reverse dependencies. It might be worth having a script for that.
The following little script by Tej that we used to add all the missing `Global` might be a good starting point...We are getting tons of these, and I expect even more in our reverse dependencies. It might be worth having a script for that.
The following little script by Tej that we used to add all the missing `Global` might be a good starting point:
```
#!/usr/bin/env python3
import sys
import re
error_re = re.compile(r"""^File "(?P<file>[^"]*)", line (?P<line>[0-9]+), characters .*:""")
for line in map(str.rstrip, sys.stdin):
m = error_re.match(line)
if m:
file, line = m.group("file"), m.group("line")
print(f"sed -i '{line}s/^/Global /' '{file}'")
```https://gitlab.mpi-sws.org/iris/iris/-/issues/559iApply applies lemmas without resolving typeclass constraints2024-01-10T15:37:42ZRalf Jungjung@mpi-sws.orgiApply applies lemmas without resolving typeclass constraintsConsider this example:
```
From iris.algebra Require Import excl.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import lib.iprop lib.own.
From iris.prelude Require Import options.
Class spin_lockG Σ := LockG...Consider this example:
```
From iris.algebra Require Import excl.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import lib.iprop lib.own.
From iris.prelude Require Import options.
Class spin_lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
Local Existing Instance lock_tokG.
Definition spin_lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Global Instance subG_spin_lockΣ {Σ} : subG spin_lockΣ Σ → spin_lockG Σ.
Proof. solve_inG. Qed.
Lemma test `{!spin_lockG Σ} (P Q : iProp Σ) :
P -∗ P -∗ Q.
Proof. Admitted.
Lemma test2 {Σ} (P Q : iProp Σ) :
P -∗ Q.
Proof.
iIntros "HP".
iApply (test with "HP").
```
I would expect the `iApply` to fail, since the `test` lemma needs `spin_lockG` which is not present. Instead, it succeeds and creates a shelved goal. This is a pretty bad user experience since the shelved goal is easy to miss, so it is likely that one will continue in this proof not realizing that one has applied an impossible lemma. This can also cause very strange follow-on effects since the unresolved evar can cause unification failures and other hard-to-diagnose issues.https://gitlab.mpi-sws.org/iris/iris/-/issues/558wp_apply: bad errors when the term is not found or the lemma is used wrong2024-01-09T12:16:04ZRalf Jungjung@mpi-sws.orgwp_apply: bad errors when the term is not found or the lemma is used wrongConsider this test case:
```
From iris.algebra Require Import excl frac_auth numbers.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import lib.token lib.inva...Consider this test case:
```
From iris.algebra Require Import excl frac_auth numbers.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import lib.token lib.invariants lib.own.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation adequacy lib.par.
From iris.prelude Require Import options.
Definition newlock : val. Admitted.
Definition acquire : val. Admitted.
Definition release : val. Admitted.
Section test.
Context `{!heapGS_gen hlc Σ}.
Notation iProp := (iProp Σ).
Context (newlock_spec : ∀ R, {{{ R }}} newlock #() {{{ RET #(); True }}}).
Context (acquire_spec : ∀ R, {{{ R }}} acquire #() {{{ RET #(); True }}}).
Lemma test (P : iProp) :
P -∗ WP newlock #() {{ _, True }}.
Proof.
iIntros "HP".
Fail wp_apply acquire_spec.
Fail wp_apply (newlock_spec True%I with "HP").
```
Both of these `wp_apply` fail by just saying "No applicable tactic", which is a pretty bad user experience.
The first should fail saying something about "acquire" not having been found in the goal.
The second should fail the same way `iApply (newlock_spec True%I with "HP")` fails in that situation:
> `iSpecialize: cannot instantiate (True -∗ ▷ (True -∗ ?Goal #()) -∗ WP newlock #() {{ v, ?Goal v }})%I with P.`https://gitlab.mpi-sws.org/iris/iris/-/issues/552Consider merging "examples" into this repository2023-11-20T13:53:20ZRalf Jungjung@mpi-sws.orgConsider merging "examples" into this repositoryWe now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one reposito...We now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one repository less that Robbert and me have to port changes to.
- People trying to fix Coq CI have one repository less to worry about.
Downsides:
- `make` will require Autosubst to fully work
- `make` in Iris will take quite a bit longer
- CI will take longer before a package is published in opam
I don't have a very strong opinion on this. Very rarely I make changes that break something in iris/examples in subtle ways and debugging that would be much easier in a mono repo. But most of the time the overhead from having two repositories is not so bad, and it's nice that people don't have to install Autosubst to make `make` work.https://gitlab.mpi-sws.org/iris/iris/-/issues/551`iSpecialize` fails on `bi_forall` without eta expansion2024-02-16T16:30:51ZRobbert Krebbers`iSpecialize` fails on `bi_forall` without eta expansion```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- wit...```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- without eta expansion *)
Lemma bar {PROP : bi} {A} (P : A → PROP) x :
bi_forall P ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
(* Tactic failure: iSpecialize: cannot instantiate (∀ y, P y)%I with x. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/550Prevent iFrame from unfolding definitions?2023-11-13T10:09:58ZRalf Jungjung@mpi-sws.orgPrevent iFrame from unfolding definitions?Currently, iFrame unfolds at least some definitions. One can opt-out of that by making the definitions typeclasses opaque or adding `tc_opaque`, but many people don't know to do that and experience large `iFrame` slowdowns when piling up...Currently, iFrame unfolds at least some definitions. One can opt-out of that by making the definitions typeclasses opaque or adding `tc_opaque`, but many people don't know to do that and experience large `iFrame` slowdowns when piling up abstractions.
It'd be good to investigate whether we can somehow make definition-unfolding for `iFrame` be opt-in rather than opt-out.
One possibility is to use `Hint Extern`, [like `SetUnfold`](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/sets.v#L145). However, that does not allow users to opt-in.
Another possibility would be to use a different hint database where constants are by default opaque.
Either way this is a massive breaking change and would have to be carefully evaluated.https://gitlab.mpi-sws.org/iris/iris/-/issues/549Seal HeapLang points-to2023-11-11T09:36:07ZRobbert KrebbersSeal HeapLang points-toHeapLang defines a notation for the `gen_heap` points-to. This notation has two purposes (1) use `Some` for the value and (2) fix the arguments to the HeapLang `val` so that type inference and scopes work better.
It's currently quite ea...HeapLang defines a notation for the `gen_heap` points-to. This notation has two purposes (1) use `Some` for the value and (2) fix the arguments to the HeapLang `val` so that type inference and scopes work better.
It's currently quite easy to accidentally break abstraction. It's also easy to forget to lift a `gen_heap` lemma because it might work accidentally for the notation.
We thus should make the HeapLang points-to a definition and seal it.
See also the discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/960#note_98626https://gitlab.mpi-sws.org/iris/iris/-/issues/548How many kinds of `updateP` lemmas do we want?2023-11-10T12:37:43ZJohannes HostertHow many kinds of `updateP` lemmas do we want?Context: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/960#note_98523
There currently are two ways of specifying the `updateP` behavior of our resource algebras.
For example, for `prod`, the lemma characterizing `updateP` [are t...Context: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/960#note_98523
There currently are two ways of specifying the `updateP` behavior of our resource algebras.
For example, for `prod`, the lemma characterizing `updateP` [are the following](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/updates.v#L218):
```
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Lemma prod_updateP' P1 P2 x :
x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
```
Basically, we have the "explicit" style of `prod_updateP'`, where the set of potential update target values is explicitly stated, and we have the "Texan" style of `prod_updateP`, which has built-in weakening and looks more predicate-transformery. We also note that either is easily proven from the other (one direction uses weakening, the other just directly chooses `Q := λ y, P1 (y.1) ∧ ..`).
The question is: Do we always want both? Perhaps, one of these laws is barely used and can be removed, so that in future, only one of these laws needs to be maintained. And then, this law should be consistently used everywhere.https://gitlab.mpi-sws.org/iris/iris/-/issues/547`IsOp` classes are poorly named, fulfill two functions, yet they will be used...2023-11-10T12:26:10ZIke Mulder`IsOp` classes are poorly named, fulfill two functions, yet they will be used differently after !930We noticed in !1004 that the `IsOp`, `IsOp'` and `IsOpLR` classes are somewhat problematic.
Firstly, their names are somewhat confusing (something like `IntoOp` is imo more descriptive of what `IsOpLR` does).
Secondly, `IsOp` is used b...We noticed in !1004 that the `IsOp`, `IsOp'` and `IsOpLR` classes are somewhat problematic.
Firstly, their names are somewhat confusing (something like `IntoOp` is imo more descriptive of what `IsOpLR` does).
Secondly, `IsOp` is used both for merging (`iCombine`ing owns) and splitting (`iSplit`/`iDestruct`ing owns) ops.
This usually saves some lines of code for clients, but complicates things in other cases.
This could be fixed, but these classes will also be used somewhat differently once !930 lands.
After !930, there will be an `IsValidOp` class responsible for `iCombine`ing.
The current proposal for !930 would still rely on `IsOp`---but only for some `cmra`s (those with trivial validity),
and only for `cmra`s that occur as 'leaves' in a term (so not for `cmra`s constructed with combinators).https://gitlab.mpi-sws.org/iris/iris/-/issues/546More general definition of `big_opM`2023-11-03T13:08:03ZRodolphe LepigreMore general definition of `big_opM`Currently, `big_opM` is defined in `iris/algebra/big_op.v` using:
```coq
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_li...Currently, `big_opM` is defined in `iris/algebra/big_op.v` using:
```coq
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
```
which means that `big_opM` is hard-coded to using `gmap`. I'm wondering: why not any map type?
For instance, one could define it as
```coq
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} `{FinMap K MM} {A} (f : K → A → M)
(m : MM A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
```
or as
```coq
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} {A} `{MapFold K A MM} (f : K → A → M)
(m : MM) : M := big_opL o (λ _, uncurry f) (map_to_list m).
```
and then tweak the rest of the file, so that `big_opM` lemmas can basically work with any `FinMap`, not just `gmap`.https://gitlab.mpi-sws.org/iris/iris/-/issues/545Better error when trying mask-changing iMod on non-atomic WP goal2023-10-24T12:28:27ZRalf Jungjung@mpi-sws.orgBetter error when trying mask-changing iMod on non-atomic WP goalCurrently when you run `iMod` on a mask-changing fupd and the goal is a WP with an expression that cannot be proven atomic, we open a subgoal that asks the user to prove atomicity. In many cases, this subgoal will be unprovable. Also in ...Currently when you run `iMod` on a mask-changing fupd and the goal is a WP with an expression that cannot be proven atomic, we open a subgoal that asks the user to prove atomicity. In many cases, this subgoal will be unprovable. Also in many cases, the user will be surprised by why this shows up now but didn't show up in the tutorial when they opened an invariant.
I think instead of falling back to asking the user to prove the goal, we should fall back to showing an error message, such as with the `pm_error` infrastructure. The message should then give the user some useful hints for what to do.https://gitlab.mpi-sws.org/iris/iris/-/issues/543"iFrame" sometimes fails to frame assertions piece-by-piece but succeeds to f...2023-10-02T13:09:17ZRalf Jungjung@mpi-sws.org"iFrame" sometimes fails to frame assertions piece-by-piece but succeeds to frame them all at onceA test says more than a thousand words:
```
Section tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_iFrame_or `{!BiAffine PROP} P Q R : P -∗ Q -∗ R ∨ (P ∗ Q).
Proof.
iIntros "HP HQ". Fail iFrame "HP HQ".
iCombine...A test says more than a thousand words:
```
Section tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_iFrame_or `{!BiAffine PROP} P Q R : P -∗ Q -∗ R ∨ (P ∗ Q).
Proof.
iIntros "HP HQ". Fail iFrame "HP HQ".
iCombine "HP HQ" as "H". iFrame "H".
Qed.
```
The first `iFrame` fails since it only makes progress under one arm of the disjunction, and our current heuristic is that we accept framing under ∨ only if
- it makes progress under both arms, or
- one arm is solved completely
But those heuristics violate the principle that you can frame things incrementally. We have never stated that principle, but we implement `iFrame "H1 H2 H3"` as a loop framing things incrementally, so this is a reasonable principle to expect.
Now, IIRC we've arrived at these semantics since it used to be the case that `iFrame` worked under `∨` in cases where that was not clearly desirable. So it's not clear that we have a good solution here. But it might be worth to experiment with the approach where we frame under `∨` if either arm makes progress, similar to what we do for `∧`?https://gitlab.mpi-sws.org/iris/iris/-/issues/542Find a consistent way to deal with private lemmas2023-09-14T16:22:55ZRobbert KrebbersFind a consistent way to deal with private lemmasSee the following [discussion](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/986#note_96120) in !986.
We want a proper way to deal with "private lemmas" so that:
1. They do not pollute the namespace when importing the module
2....See the following [discussion](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/986#note_96120) in !986.
We want a proper way to deal with "private lemmas" so that:
1. They do not pollute the namespace when importing the module
2. They are not found by `Search`
`Local Lemma` solves the first, but not the latter. There are hacks such as adding `Private_` to the name to blacklist them from search, but they are ugly. They are also inconsistent with the `_` proposal for "private" Ltacs from #529.https://gitlab.mpi-sws.org/iris/iris/-/issues/541iRewrite error message when the subterm is not found refers to non-existing f...2023-08-28T17:38:28ZRalf Jungjung@mpi-sws.orgiRewrite error message when the subterm is not found refers to non-existing fresh variable nameTestcase:
```
Lemma test_iRewrite_subterm_not_found `{!BiInternalEq PROP} {A : ofe} (x y z : A) :
y ≡ z ⊢@{PROP} x ≡ z.
Proof. iIntros "H". iRewrite "H".
```
This prints
```
Error: Found no subterm matching "x0" in the current goal.
``...Testcase:
```
Lemma test_iRewrite_subterm_not_found `{!BiInternalEq PROP} {A : ofe} (x y z : A) :
y ≡ z ⊢@{PROP} x ≡ z.
Proof. iIntros "H". iRewrite "H".
```
This prints
```
Error: Found no subterm matching "x0" in the current goal.
```
but it should be saying that it did not find `y` in the goal.https://gitlab.mpi-sws.org/iris/iris/-/issues/540Inconsistent lemma statements and names: Some_equiv_eq vs the equivalent lemm...2023-08-10T06:43:42ZRalf Jungjung@mpi-sws.orgInconsistent lemma statements and names: Some_equiv_eq vs the equivalent lemma on dist```
Some_equiv_eq:
∀ {A : Type} {H : Equiv A} (mx : option A) (y : A), mx ≡ Some y ↔ (∃ y' : A, mx = Some y' ∧ y' ≡ y)
```
vs
```
dist_Some_inv_l':
∀ {A : ofe} (n : nat) (my : option A) (x : A),
Some x ≡{n}≡ my → ∃ x' : A, Some x...```
Some_equiv_eq:
∀ {A : Type} {H : Equiv A} (mx : option A) (y : A), mx ≡ Some y ↔ (∃ y' : A, mx = Some y' ∧ y' ≡ y)
```
vs
```
dist_Some_inv_l':
∀ {A : ofe} (n : nat) (my : option A) (x : A),
Some x ≡{n}≡ my → ∃ x' : A, Some x' = my ∧ x ≡{n}≡ x'
dist_Some_inv_r':
∀ {A : ofe} (n : nat) (mx : option A) (y : A),
mx ≡{n}≡ Some y → ∃ y' : A, mx = Some y' ∧ y ≡{n}≡ y'
```https://gitlab.mpi-sws.org/iris/iris/-/issues/539Stacking cmra combinators can dramatically slow down type-checking/unification2023-08-10T15:01:46ZIke MulderStacking cmra combinators can dramatically slow down type-checking/unificationAs noticed by !907, stacking too many (u)cmra combinators can dramatically slow down type-checking/unification.
A somewhat minimal example that shows the problem is the following:
```
From iris.algebra Require Import agree frac_auth.
Fr...As noticed by !907, stacking too many (u)cmra combinators can dramatically slow down type-checking/unification.
A somewhat minimal example that shows the problem is the following:
```
From iris.algebra Require Import agree frac_auth.
From iris.base_logic Require Import own.
Time Lemma stack_frac_auths2 `{!inG Σ (frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 ((●F (●F (to_agree n)))) ⊢ own γ1 ((●F (●F (to_agree n)))).
Abort.
Time Lemma stack_frac_auths3 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 (●F (●F (●F (to_agree n)))) ⊢ own γ1 (●F (●F (●F (to_agree n)))).
Abort.
Time Lemma stack_frac_auths4 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 (●F (●F (●F (●F (to_agree n))))) ⊢ own γ1 (●F (●F (●F (●F (to_agree n))))).
Abort.
Time Lemma stack_frac_auths5 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 (●F (●F (●F (●F (●F (to_agree n)))))) ⊢ own γ1 (●F (●F (●F (●F (●F (to_agree n)))))).
Abort.
```
Note that we are not entering any proof mode yet, but type-checking lemma statement `stack_frac_auths2` still takes 0.1 seconds on my machine, while I haven't waited long enough for `stack_frac_auths3` to terminate.
The problem is caused by writing `frac_authUR` while a `frac_authR` would suffice. The former returns a `ucmra`, but Coq expects a `cmra`, and so it inserts the `ucmra_cmraR` coercion. So now we have something of type `inG Σ (ucmra_cmraR $ frac_authUR _ )` while we need something of type `inG Σ (frac_authR _)` (as implicit argument to `own`), and the `_` may feature the same problem. Coq must check that these types coincide definitionally, and this takes a long time to check.
The band-aid fix from !907 is to add a [Strategy](https://coq.inria.fr/refman/proofs/writing-proofs/equality.html?highlight=strategy#coq:cmd.Strategy) command to speed up this type-checking. By unfolding some of the projections eagerly, the computation finishes faster: `stack_frac_auths2` now type-checks nearly instantly.
However, the problem persists: `stack_frac_auths3` takes 0.1 seconds, while `stack_frac_auths4` takes 4 seconds, and `stack_frac_auths5` takes about 140 seconds.
Paraphrasing from !907:
I suspect just (`Strategy`) annotations cannot make this fast. To make this fast, I think we need to have a solution for the following question:
How do we keep type-checking/unification fast for structures (like `ofe`, `cmra` and `ucmra`) that have combinators (like `optionUR : cmra → ucmra`) and coercions (like `ucmra_cmraR : cmra → ucmra`), especially when stacking alot of these combinators?