Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2023-03-04T18:40:53Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2023-03-04T18:40:53ZRalf Jungjung@mpi-sws.orgUse siProp more in building the uPred (and BI) interfacesuPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp`...uPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/418library inG instances should be local2021-06-02T14:46:21ZRalf Jungjung@mpi-sws.orglibrary inG instances should be localCurrently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.Currently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.https://gitlab.mpi-sws.org/iris/iris/-/issues/413Better errors when tactic fails to automatically resolve some side-condition2021-07-22T12:54:29ZRalf Jungjung@mpi-sws.orgBetter errors when tactic fails to automatically resolve some side-condition@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-conditio...@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-condition; we could introduce something like
```
Definition pm_error (s : string) := False
```
and add instances with `error "foo"` as their side-condition; together with some support in `iSolveSideCondition` this could be used to then show better, instance-specific error messages when `iMod` fails.
2. We could add a new typeclass like `ElimModalError` that is used to compute an error message when `ElimModal` failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.https://gitlab.mpi-sws.org/iris/iris/-/issues/412Use dfrac everywhere2023-03-18T18:30:39ZRalf Jungjung@mpi-sws.orgUse dfrac everywhere`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [x] `algebra.lib.gmap_view`
* [x] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more ...`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [x] `algebra.lib.gmap_view`
* [x] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.https://gitlab.mpi-sws.org/iris/iris/-/issues/411Taking ∃ out of ▷ without Inhabited, more easily2021-04-29T09:25:44ZYusuke MatsushitaTaking ∃ out of ▷ without Inhabited, more easilyIn Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If w...In Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If we use the lemma `later_exist_except_0` instead, we get `▷ Φ x` without having `Inhabited A`, under the `◇` modality.
In Iris we are often under the `◇` modality because the update modality `|=>` contains `◇`.
I hope the operation of taking `∃x` out of `▷` without `Inhabited` becomes easier to use.
One possibility is to let Iris Proof Mode apply `later_exist_except_0` when the goal is under the `◇` modality.https://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/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/402iFrame performance issues2022-05-06T12:56:32ZRalf Jungjung@mpi-sws.orgiFrame performance issuesThere are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into ...There are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into disjunctions at all by default?
- Also, @tchajed noticed that `iFrame` is doing a lot of `AsFractional` everywhere, which might also be a too expensive default -- this is tracked separately in https://gitlab.mpi-sws.org/iris/iris/-/issues/351.
- Cc https://gitlab.mpi-sws.org/iris/iris/-/issues/183 for the general "power vs performance" tradeoff in `iFrame`.
- https://gitlab.mpi-sws.org/iris/iris/-/issues/434 for diverging iFrame because Hint Mode is accidentally being circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/399Upstream more big_op lemmas from Perennial2021-02-17T08:49:05ZRalf Jungjung@mpi-sws.orgUpstream more big_op lemmas from PerennialPerennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.Perennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.https://gitlab.mpi-sws.org/iris/iris/-/issues/398Use `dom` instead of `∀ k, is_Some (.. !! k) ...`2021-02-17T08:48:46ZRobbert KrebbersUse `dom` instead of `∀ k, is_Some (.. !! k) ...`See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas...See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas for `dom`. However, the fact that the set (here `gset`) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.https://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/392Masks in step-taking fupd notation2020-12-10T13:37:03ZRalf Jungjung@mpi-sws.orgMasks in step-taking fupd notationEarlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gi...Earlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/391Add append-only list RA to Iris2021-05-17T16:32:27ZRalf Jungjung@mpi-sws.orgAdd append-only list RA to IrisAppend-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize l...Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/387Deprecate unqualified "Instance"2020-12-19T17:43:58ZRalf Jungjung@mpi-sws.orgDeprecate unqualified "Instance"With https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/594 (and potentially some follow-up changes), all `Hint` in Iris will be qualified with `Local` or `Global`. I think we should do the same with `Instance`.
@tchajed is there a w...With https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/594 (and potentially some follow-up changes), all `Hint` in Iris will be qualified with `Local` or `Global`. I think we should do the same with `Instance`.
@tchajed is there a way to adjust your script to do that, or will we have to ask the Coq devs for an (opt-in) deprecation warning for `Instance` first, similar to the `Hint` warning that your script is based on?https://gitlab.mpi-sws.org/iris/iris/-/issues/385reshape_expr does not recognize `fill`2020-12-05T08:58:01ZRalf Jungjung@mpi-sws.orgreshape_expr does not recognize `fill`There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-e...There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-enabling that instance locally in ReLoC, C and Actris.https://gitlab.mpi-sws.org/iris/iris/-/issues/380iDestruct does not handle some patterns that it probably could2020-11-11T16:57:53ZTej Chajedtchajed@gmail.comiDestruct does not handle some patterns that it probably couldThe pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though ...The pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though that could be processed as `iDestruct ... as H; done`. It does handle `H /=` (by running `simpl` after the destruct).https://gitlab.mpi-sws.org/iris/iris/-/issues/379Make sealing consistent and document it2020-11-10T13:15:28ZRalf Jungjung@mpi-sws.orgMake sealing consistent and document itWe should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to ...We should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to the eta-expanded term. This immediately implies that sealing should be done outside of sections.
* Add an `unseal` tactic, either as `Local Ltac` or in a module to avoid polluting the global namespace.
* There is no need to make sealed definitions `Typeclasses Opaque`.
- no eta, ergo no sections
- unseal tactic
- no TC opaque
For example, here is how sealing of a logic-level RA wrapper could look like:
```
Definition mnat_own_auth_def `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (mnat_auth_auth q n).
Definition mnat_own_auth_aux : seal (@mnat_own_auth_def). Proof. by eexists. Qed.
Definition mnat_own_auth := mnat_own_auth_aux.(unseal).
Definition mnat_own_auth_eq : @mnat_own_auth = @mnat_own_auth_def := mnat_own_auth_aux.(seal_eq).
Arguments mnat_own_auth {Σ _} γ q n.
Definition mnat_own_lb_def `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (mnat_auth_frag n).
Definition mnat_own_lb_aux : seal (@mnat_own_lb_def). Proof. by eexists. Qed.
Definition mnat_own_lb := mnat_own_lb_aux.(unseal).
Definition mnat_own_lb_eq : @mnat_own_lb = @mnat_own_lb_def := mnat_own_lb_aux.(seal_eq).
Arguments mnat_own_lb {Σ _} γ n.
Local Ltac unseal := rewrite
?mnat_own_auth_eq /mnat_own_auth_def
?mnat_own_lb_eq /mnat_own_lb_def.
```
When there are operational typeclasses involved, the `_eq` lemma should also account for those to avoid having to rewrite twice:
```
Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Arguments monPred_bupd {_}.
Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/374Avoid sequences of "_" by adjusting lemma statements2020-11-05T12:11:02ZRalf Jungjung@mpi-sws.orgAvoid sequences of "_" by adjusting lemma statementsSome Iris lemmas are prone to needing plenty of `_` almost every time they are used. I noticed this in particular for
* most big-op lemmas that access a single element, where the to-be-accessed element needs to be given explicitly, but o...Some Iris lemmas are prone to needing plenty of `_` almost every time they are used. I noticed this in particular for
* most big-op lemmas that access a single element, where the to-be-accessed element needs to be given explicitly, but often other arguments come first
* several allocation lemmas such as `inv_alloc`, where the to-be-allocated thing needs to be given explicitly, but other arguments come first
* many of the update lemmas, where typically one works with `iMod`, so the new values (e.g. new lower bound for mono_nat, or new key and value for gmap) need to be given, but they are often the last arguments
There are two ways to fix this:
* reorder arguments, so that those that are likely to be determined by unification come first
* make likely-to-be-determined-by-unification arguments implicit, so that we do not have to write out their `_`
I am in favor of the second approach because it has a better failure mode: if one of those arguments ends up *not* being determined by unification, we have use `lemma (arg:=val)` to explicitly give the value for this agument. For lemmas with many arguments, this name-based approach is anyway much easier to read and write than the position-based approach (no need to remember the exact order of arguments).
However, while implicit arguments are widely used in Iris, we usually control them on a per-section basis, not a per-lemma basis. @robbertkrebbers has objected the used of implicit arguments for this reason. (That is my understanding, anyway.)https://gitlab.mpi-sws.org/iris/iris/-/issues/371Add validI lemmas for discrete RAs2020-11-05T08:41:29ZRalf Jungjung@mpi-sws.orgAdd validI lemmas for discrete RAsOur discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `...Our discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `Prop`-level lemmas. But e.g. when proving equivalences, it can be useful to have a way to rewrite validity into an equivalent logical statement.
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/558 added the lemma for frac, but other RAs are still missing:
* [ ] `gset_disj`
* [ ] `coPset`, `coPset_disj`
* [ ] `sts`
* [ ] `dfrac`https://gitlab.mpi-sws.org/iris/iris/-/issues/369Document HeapLang2022-05-18T17:42:51ZRalf Jungjung@mpi-sws.orgDocument HeapLangThe HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently [my thesis](https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#figure.3.1) and the ["Future is Our...The HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently [my thesis](https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#figure.3.1) and the ["Future is Ours" paper](https://plv.mpi-sws.org/prophecies/paper.pdf#%5B%7B%22num%22%3A171%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C45.828%2C641.295%2Cnull%5D) describe overlapping but incomparable subsets of the operational semantics, and there are likely bits that are missing from both.