Iris merge requestshttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests2024-06-10T14:14:10Zhttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1052Add `and_own` lemma for handling `own γ x ∧ own γ y`2024-06-10T14:14:10ZtjhanceAdd `and_own` lemma for handling `own γ x ∧ own γ y`The main purpose is to add the following result:
```coq
Lemma and_own (γ : gname) (x y : A) :
(own γ x ∧ own γ y) ⊢ ∃ z , own γ z
∗ Some x ≼ Some z
∗ Some y ≼ Some z.
```
The reason we use `Some x ≼ Some z` is be...The main purpose is to add the following result:
```coq
Lemma and_own (γ : gname) (x y : A) :
(own γ x ∧ own γ y) ⊢ ∃ z , own γ z
∗ Some x ≼ Some z
∗ Some y ≼ Some z.
```
The reason we use `Some x ≼ Some z` is because we need the comparison to be reflexive.
Here, the `≼` is defined to be an iProp version of the normal `≼`:
```coq
Definition uPred_cmra_included {Σ: gFunctors} {M: cmra} (a b : M) : iProp Σ := ∃ c , b ≡ a ⋅ c.
Infix "≼" := uPred_cmra_included (at level 70) : bi_scope.
```
We also prove some corollaries of `and_own`, e.g., for a discrete unital camera we have:
```coq
Lemma and_own_discrete_ucmra_specific {D : CmraDiscrete A} (γ : gname) (x y z : A) :
(∀ w , ✓ w → x ≼ w → y ≼ w → z ≼ w) →
(own γ x ∧ own γ y) ⊢ own γ z.
Lemma and_own_discrete_ucmra_contradiction {D : CmraDiscrete A} (γ : gname) (x y : A) :
(∀ w , ✓ w → x ≼ w → y ≼ w → False) →
(own γ x ∧ own γ y) ⊢ False.
```
All the new code is in `own.v`; I think the new `≼` should probably go somewhere else but I wasn't quite sure where.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1050Draft: Adapt to iris/stdpp!5552024-06-10T07:58:52ZMichael SammlerDraft: Adapt to iris/stdpp!555https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1049Add lemmas for big_opS and gmap singletons2024-05-28T13:51:00ZIsaac van Bakelisaac.vanbakel@inf.ethz.chAdd lemmas for big_opS and gmap singletonsThis is a particular pattern that comes up in the lifetime logic which I
want to be able to rewrite, which is why I've extracted it to a general
lemma.This is a particular pattern that comes up in the lifetime logic which I
want to be able to rewrite, which is why I've extracted it to a general
lemma.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1048Always use magic wand in `iInduction` hypothesis2024-05-08T10:08:28ZRobbert KrebbersAlways use magic wand in `iInduction` hypothesisThe current behavior is inconsistent:
```coq
Lemma foo {PROP : bi} (n : nat) (Hn : 0 < n) (P : nat → PROP) : ⊢ P n.
Proof.
iInduction n as [|n] "IH" forall (Hn); first lia.
Restart.
iInduction n as [|n] "IH"; first lia.
Abort.
```
...The current behavior is inconsistent:
```coq
Lemma foo {PROP : bi} (n : nat) (Hn : 0 < n) (P : nat → PROP) : ⊢ P n.
Proof.
iInduction n as [|n] "IH" forall (Hn); first lia.
Restart.
iInduction n as [|n] "IH"; first lia.
Abort.
```
In the first case (manual revert via `forall` clause), we get a wand; in the second case (auto revert), we get an implication.
In !789 we decided that wands are preferred, but we missed the case for the automated revert.
Small note: I am using `MakeAffinely` instead of `FromAffinely`, that is because `MakeAffinely` gives an `⊣⊢` instead of `⊢` and we actually need the other direction. This is consistent with `IntoWand` instances where we also use `MakeAffinely`. Since we use it on `⌜ _ ⌝` and not a compound assertion, this should not make a difference.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1042iFrame: Do not call `cbv` on user terms in contexts2024-04-12T13:31:29ZJannoiFrame: Do not call `cbv` on user terms in contextsI cannot believe these `cbv` calls survived for a such a long time!
I didn't find this due to the performance issues of calling `cbv` on user terms, oddly enough. I was investigating why relatively small proofs were taking upwards of 10...I cannot believe these `cbv` calls survived for a such a long time!
I didn't find this due to the performance issues of calling `cbv` on user terms, oddly enough. I was investigating why relatively small proofs were taking upwards of 10GB of memory (with pretty permissive GC parameters).
Here's the change as reported by memtrace on a small file with a total of 6 `iFrame` calls throughout the proof. All calls are on pretty a small goals with <20 total premises but I guess the terms involved are not exactly trivial when fully normalized.
Before:
![image](/uploads/5db0ddb92eaf498f80005fba292aee4a/image.png)
After:
![image](/uploads/65b2ea16c5efe6f6219c14d0eac98b70/image.png)
The file also went from 1min to less than 45s.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1041Prevent iFrame from instantiating existentials under updates.2024-03-12T17:33:19ZJannoPrevent iFrame from instantiating existentials under updates.I think these cases were accidentally left out in !1035.
We've only just managed to get to most of our iris proofs in our 8.19 bump and didn't notice breakage from this omission earlier.
/cc @snyke7I think these cases were accidentally left out in !1035.
We've only just managed to get to most of our iris proofs in our 8.19 bump and didn't notice breakage from this omission earlier.
/cc @snyke7https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1020Do not use eta-expansion in `into_forall_forall`.2024-03-05T13:30:14ZRobbert KrebbersDo not use eta-expansion in `into_forall_forall`.This fixes #551.This fixes #551.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1008More documentation about _1 and _2 lemmas.2023-10-20T20:04:08ZRobbert KrebbersMore documentation about _1 and _2 lemmas.See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97838See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97838https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1007Add notations for `<affine> ⌜ ⌝` and friends.2023-10-17T08:11:01ZRobbert KrebbersAdd notations for `<affine> ⌜ ⌝` and friends.This MR adds the following notations:
- `⌜⌜ φ ⌝⌝` for `<affine> ⌜ φ ⌝`
- `⎡⎡ P ⎤⎤` for `<affine> ⎡ P ⎤`
- `x ≡≡ y` for `<affine> (x ≡ y)`
- `x ≼≼ y` for `<affine> (x ≼ y)`
So the idea is: doubling the symbol makes it affine. This shoul...This MR adds the following notations:
- `⌜⌜ φ ⌝⌝` for `<affine> ⌜ φ ⌝`
- `⎡⎡ P ⎤⎤` for `<affine> ⎡ P ⎤`
- `x ≡≡ y` for `<affine> (x ≡ y)`
- `x ≼≼ y` for `<affine> (x ≼ y)`
So the idea is: doubling the symbol makes it affine. This should also scale to `✓✓ x := <affine> (✓ x)`, once we have `✓` for any SBI.
I think this is a more feasible alternative to earlier discussions where we planned to make the ordinary notations the affine ones, because:
1. Most users of Iris don't use linear BIs, so the alternative would be an invasive change, whereas the current MR is trivial.
2. Many lemmas don't hold for the affine version. For example `f ≡ g ⊣⊢ ∀ x, f x ≡ g x` does not hold for `≡≡`. So if the affine version is the default, we need to duplicate all our lemmas, similar to how we have duplicated all lemmas for `<pers>` and `□`. This sounds like too much work for too little gain. In proofs with the present MR, you would typically move the affine version into the persistent context, thus stripping the affine modality, allowing you to use the lemmas for the non-affine version.
3. Some lemmas would need absorbing modalities for the affine versions. For example `own γ x ⊢ ✓ x` would not hold in an affine BI if `✓` where affine. (This example only applies once we have a general `own` and `✓`, there might be other examples in our current code-base already).
4. We support instances of `Embed` where `⎡ P ⎤` is affine and where it is not, so having `<affine> ⎡ _ ⎤` as the default would not be desired. For example, the embedding of `iProp` into `ironProp` is _not_ affine, so you often want to use `⎡⎡ P ⎤⎤`. However, if `BiEmbedEmp` holds, you want to use `⎡ P ⎤` (without affine modality), so that `⎡ P ⎤` is affine if `P` is affine.
**TODO:** Since there are not many uses of these new notations, we should add some tests. In particular, we should test that `⎡ ⎡ P ⎤ ⎤` is not pretty printed as `⎡⎡ P ⎤⎤`.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1004Add `IsOp` instances for `gset`, `coPset`, `gmultiset`2023-11-10T12:26:08ZIke MulderAdd `IsOp` instances for `gset`, `coPset`, `gmultiset`This MR adds `IsOp` instances for `gset`, `coPset` and `gmultiset`, and is part of the preparation for !930.
These `IsOp` instances make `iCombine` compute prettier results on `own`s of these `cmra`s.This MR adds `IsOp` instances for `gset`, `coPset` and `gmultiset`, and is part of the preparation for !930.
These `IsOp` instances make `iCombine` compute prettier results on `own`s of these `cmra`s.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/992Draft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the pattern2023-10-04T20:18:28ZRobbert KrebbersDraft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the patternSee https://mattermost.mpi-sws.org/iris/pl/samjaqqz8jb7fqepbcefxm47io where @jung wrote:
> We have another behavior change from the [ltac2 MR](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931):
> ```coq
> Lemma test_iDestruct1_...See https://mattermost.mpi-sws.org/iris/pl/samjaqqz8jb7fqepbcefxm47io where @jung wrote:
> We have another behavior change from the [ltac2 MR](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931):
> ```coq
> Lemma test_iDestruct1_pure (Φ: nat → PROP) :
> (∃ y z:nat, Φ y) -∗ ∃ x, Φ x.
> Proof.
> iDestruct 1 as (? y) "H".
> ```
> this now fails because the ? gets name y and then the later y says that the name is already used. it used to work fine, presumably because intros ? y actually does some form of lookahead and avoids picking the name y when a later pattern uses that name?
This MR fixes this issue. Thanks to @snyke7 for the Ltac2 hackery.
Reasons for WIP:
- `iIntros "(% & %y & ?)"` still fails on the same example. The problem is that we do not collect names from the Iris intro pattern. This should be simple to fix.
- We need to figure out where to put and how to name the Ltac2 stuff.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/980Avoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.2023-08-30T09:52:55ZRobbert KrebbersAvoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.This MR is a follow up of !979.
Always preferring the projections is similar to the way we use `acquire`/`release`/etc.
This MR also adjusts the `subG` instance to use `lockG` instead of `spin_lockG`, and tests that the conditions are ...This MR is a follow up of !979.
Always preferring the projections is similar to the way we use `acquire`/`release`/etc.
This MR also adjusts the `subG` instance to use `lockG` instead of `spin_lockG`, and tests that the conditions are resolved automatically when using adequacy.
TODO: I have only done this for spin lock, the same remains to be done for ticket lock, rw lock, atomic heap.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/972Draft: experiment: use coq's ability to infer more canonical structures2023-08-28T12:02:37ZRalf Jungjung@mpi-sws.orgDraft: experiment: use coq's ability to infer more canonical structuresI wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires m...I wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires more type annotations. I don't understand why Coq cannot infer that any more.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/971Draft: Attempted fix for #539, solving slow type-checking of nested `●` terms2023-08-28T20:24:30ZIke MulderDraft: Attempted fix for #539, solving slow type-checking of nested `●` termsAn attempt to fix #539. In summary, this MR:
- makes `auth` a `Definition`, instead of a `Notation`
- provides better `Canonical` instances for seeing `auth` as an `ofe`/`cmra`/`ucmra`. Previously, those of `view` were used, which can re...An attempt to fix #539. In summary, this MR:
- makes `auth` a `Definition`, instead of a `Notation`
- provides better `Canonical` instances for seeing `auth` as an `ofe`/`cmra`/`ucmra`. Previously, those of `view` were used, which can result in some very large terms.
- changes the definition of `ucmra` to an equivalent one, which ensures that the `ucmra_cmraR` coercion can compute fast on nested terms.
I believe all 3 changes are necessary to fix #539:
- The first two make it feasible to `Time Check (● (● (● (● (● (● (● (● (● (● (● (● (()))))))))))))).`
- The last one is necessary to get problems like the following to type check quickly
```
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)))))).
```
It additionally reverts !907 and instead registers a strategy that prevents unfolding `authR` and `authO`. Unfolding those would reveal the underlying `view` structure, which may cause an exponential blow-up in unification time.
I am quite interested in the timing for this MR, also for dependencies on Iris. The changes to `ucmra` might break stuff elsewhere, or make stuff slower.. in which case this might not be the way to go.
Also note that this MR uses the [`reversible` attribute](https://coq.inria.fr/refman/addendum/implicit-coercions.html#coq:attr.reversible), which means we need Coq 8.16.1+.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/953Draft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.2023-08-05T08:32:52ZRobbert KrebbersDraft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.This addresses https://gitlab.mpi-sws.org/iris/iris/-/issues/529 in part.
**TODO**: Use `_` prefix, but do that after !931 to avoid merge conflicts.This addresses https://gitlab.mpi-sws.org/iris/iris/-/issues/529 in part.
**TODO**: Use `_` prefix, but do that after !931 to avoid merge conflicts.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/933Make bi fields non-canonical2023-10-13T14:37:45ZPaolo G. GiarrussoMake bi fields non-canonicalSuggested by @janno .Suggested by @janno .https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/930Draft: Improve validity information received from `iCombine`ing `own`s2023-11-10T12:26:50ZIke MulderDraft: Improve validity information received from `iCombine`ing `own`sDraft MR for addressing #251 and #460.
This is basically !771, but rebuilt on top of the `CombineSepAs` and `CombineSepGives` typeclasses from !872.
In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet ...Draft MR for addressing #251 and #460.
This is basically !771, but rebuilt on top of the `CombineSepAs` and `CombineSepGives` typeclasses from !872.
In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)
```
executing `iCombine "Hγ1 Hγ2" as "Hγ" gives %[Hq HE]` will now replace "Hγ1" and "Hγ2" with a new hypothesis `"Hγ" : own γ (q1 + q2, GSet (E1 ∪ E2))` and two pure hypotheses: `Hq : q1 + q2 ≤ 1` and `HE : E1 ## E2`.
In the following environment:
```
"Hγ1" : own γ (◯ (Some (q1, GSet E1)))
"Hγ2" : own γ (● (Some (q2, GSet E2)))
```
executing `iCombine "Hγ1 Hγ2" gives %H` should give you a new pure hypotheses `H : q1 ≤ q2 ∧ E1 ⊆ E2 ∧ ((q1 < q2) ∨ (q1 ≡ q2 ∧ E1 ≡ E2))`.
It works by adding three typeclasses, `IsValidOp`, `IsValidGives` and `IsIncluded`, which try to determine an `iProp` that simplifies `✓` or `≼`. Since we are looking for an `iProp`, not a pure proposition, this approach also works for higher-order ghost state.
**Engineering questions:**
- The current approach does not simplify equivalences. If directly using rewrites in introduction patterns, this may cause slowdowns. Currently an explicit `%leibniz_equiv` on the equality is needed for faster rewrites. Fixing this would require an additional typeclass or some such for doing the simplification beforehand. For now, Robbert and I propose to leave this as such, and instead improve the `IntoPure` instance.
**Style/MR questions:**
- Does not yet have instances for all CMRA building blocks provided in `iris/algebra`, but at least supports the ones used inside the iris repository, and some others I have used in the past. How complete should this be?
- I needed some additional lemmas to simplify internal validity of e.g. `viewR`. Should these be upstreamed in a separate MR? They might not very nicely mesh with Robberts `siProp`, since they lift the `view_rel` to the logic, which only works for `uPred` currently.
**TODO:**
- Documentation is missing
- Tests are still missing
- List CMRA building blocks for which support is missing
- I added additional `IsOp` instances for `gset`, `gmultiset` and `gmap`, need to wait for MR !1004.
- ~~I added some lemmas about `IdFree` at the logic level, need to wait for MR !1005~~.
- ~~I added additional `MakeOr` instances for simplifying e.g. `False ∨ P`, need to wait for MR !940~~.
- ~~I am using `∗-∗` in `IsIncluded` to make sure I'm not dropping information. I sometimes make use of the transitivity of this, need to wait for MR !941.~~
- ~~I needed some additional lemmas to simplify internal validity of e.g. `dfracR` and `authR`, need to wait for MR !942.~~
- ~~Improve the `IntoPure` instance for leibniz equivalences in a separate MR, need to wait for MR !966~~.
- ~~Add `≼` on the BI level, need to wait for !944.~~
- ~~Remove `reservation_map` support for now.~~
Feedback is most welcome!https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/916`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.2023-07-25T18:58:19ZRobbert Krebbers`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.This has the following advantages:
- We need fewer adhoc `Hint Extern` instances for the proof mode, we can just use `Unify`.
- We can consistently use the `refine` unification algorithm when trying to unify a hypothesis/conclusion of a...This has the following advantages:
- We need fewer adhoc `Hint Extern` instances for the proof mode, we can just use `Unify`.
- We can consistently use the `refine` unification algorithm when trying to unify a hypothesis/conclusion of a lemma/wand to the goal. This is currently only done by `iAssumption`, but not by `iFrame` or `iApply`.
- It might allow us to use `Typeclasses Opaque` for all std++ operational type classes. As described in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/914#note_91480, this is currently impossible.
We could probably do some bikeshedding about the name or other implementation aspects. But I might make sense to first check out the performance impact and whether it breaks anything in the reverse dependencies. So @jung could you run timing CI, please.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/903add fixpoint lemmas for plain and absorbing2024-04-02T18:07:40ZWilliam Manskyadd fixpoint lemmas for plain and absorbingAdded some lemmas about typeclass instances for fixpoints on `bi_ofeO` (as opposed to `least`/`greatest_fixpoint` in the logic).Added some lemmas about typeclass instances for fixpoints on `bi_ofeO` (as opposed to `least`/`greatest_fixpoint` in the logic).https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/888Draft: parameterize the algebra folder by the stepindex type for integration with Transfinite Iris2024-04-15T18:53:21ZLennard Gähergaeher@mpi-sws.orgDraft: parameterize the algebra folder by the stepindex type for integration with Transfinite IrisThis MR is tackling one of the steps (https://gitlab.mpi-sws.org/simonspies/iris-parametric-index/-/issues/2) towards making Iris compatible with Transfinite Iris.
It parameterizes the algebra folder by a "stepindex type" `SI`. This requ...This MR is tackling one of the steps (https://gitlab.mpi-sws.org/simonspies/iris-parametric-index/-/issues/2) towards making Iris compatible with Transfinite Iris.
It parameterizes the algebra folder by a "stepindex type" `SI`. This requires according generalizations of the notions of OFEs and COFEs.
A finite stepindex type instance for `nat` is provided. For this special case, we can re-derive the previous notions of OFEs and COFEs.
The rest of the development, in particular `bi`, `base_logic`, and everything which builds on top of these, fixes the stepindex type to `nat`.
This MR is work in progress. At least the following things need to be done:
- add more comments explaining the central definitions and the rationale
- a few rewrites with `left_id` are now failing and need more specific specialization for the correct instances to be found. We should try to fix this.