Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-12-05T08:58:01Zhttps://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/389Citation guide2020-12-08T17:17:32ZTej Chajedtchajed@mit.eduCitation guideThe docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.The docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.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/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/394Document relation between Discrete and Timeless (in appendix?)2021-01-06T13:08:34ZPaolo G. GiarrussoDocument relation between Discrete and Timeless (in appendix?)See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not s...See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not so useful; Timeless P → Discrete P does not hold; discrete propositions are unlikely to exist.
> It might be worth documenting this somewhere, but I don't know what's the best place. Maybe the appendix?https://gitlab.mpi-sws.org/iris/iris/-/issues/396Intro pattern `>` has wrong behavior with side-conditions of `iMod`2021-04-29T09:25:46ZRobbert KrebbersIntro pattern `>` has wrong behavior with side-conditions of `iMod````coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> ...```coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
Proof.
iIntros ">H".
```
fails with
```
In environment
Σ : gFunctors
heapG0 : heapG Σ
E1, E2 : coPset
P : iProp Σ
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11809)
(environments.env_spatial ?M11809) ?M11814"
with
"∀ (σ : language.state heap_lang) (e' : language.expr heap_lang) (κ :
list
(language.observation
heap_lang))
(σ' : language.state heap_lang) (efs : list (language.expr heap_lang)),
language.prim_step (#() #()) σ κ e' σ' efs
→ match stuckness_to_atomicity NotStuck with
| StronglyAtomic => is_Some (language.to_val e')
| WeaklyAtomic => irreducible e' σ'
end".
```
See also https://mattermost.mpi-sws.org/iris/pl/r47q3gcq4fddxnhpddj91yb1wyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/397`iRename` fails with bad error message when not in proof mode2021-02-17T08:48:22ZRobbert Krebbers`iRename` fails with bad error message when not in proof mode```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
wit...```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
with "True".
```
The tactic probably does not call `iStartProof` at the beginning.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/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/400Integrate Tej's simp-lang?2021-02-17T08:49:46ZRalf Jungjung@mpi-sws.orgIntegrate Tej's simp-lang?@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04...@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04KEU&feature=youtu.be)! I took a look and watched the video, and I really like it.
I propose we give this more visibility by referencing it from the Iris repo and website, and also we should find some way to ensure that the Coq code remains compatible with latest Iris. The easiest way to do that would be to add an "iris_simp_lang" package in this repository and move the code there. The README could go into the subfolder. @tchajed would that work for you, or did you have other plans? I don't want to appropriate your work, just ensure that it does not bitrot. I could imagine declaring you the maintainer of that subdirectory, so you could e.g. merge MRs for it yourself. @robbertkrebbers what do you think?
I also have some more specific low-level comments, which I leave here just so I do not forget -- but it probably make more sense to discuss the high-level points first. It's really just one remark so far:
* In `heap_ra`, I find it confusing that you end up basically copying (parts of) `gen_heap`. IMO it would make more sense to either use `gen_heap`, or else (for the purpose of exposition) to define something that specifically works for values and locations of this language, but then it should not be called "gen(eral)".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/405Tracking issue for HeapLang interpreter2021-02-16T11:03:04ZRalf Jungjung@mpi-sws.orgTracking issue for HeapLang interpreterThis is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
...This is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Generalize the monad and move it to std++, and generalize the tactics for the monad.
* Find some way to avoid the `pretty_string` instance, or move it to std++.https://gitlab.mpi-sws.org/iris/iris/-/issues/406Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs2021-03-18T08:26:06ZArmaël GuéneauSlow typechecking / nonterminating Qed when using auxiliary definitions in RAs```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Defin...```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Definition memspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition regspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition memreg_specUR := prodUR regspecUR memspecUR.
Definition exprUR : cmraT := (exclR (leibnizO nat)).
Definition cfgUR : ucmraT := prodUR (optionUR exprUR) memreg_specUR.
Class cfgSG Σ := CFGSG {
cfg_invG :> inG Σ (authR cfgUR);
cfg_name : gname }.
Section S.
Context `{cfgSG Σ}.
Lemma spec_heap_valid (e:option (excl (leibnizO nat))) a q w
(rm: gmapUR nat (prodR fracR (agreeR (leibnizO nat))))
(mm: gmapUR nat (prodR fracR (agreeR (leibnizO nat)))) :
False →
own cfg_name (● (e,(rm,mm))) ∗
own cfg_name (◯ (ε, (∅,{[ a := (q, to_agree w) ]})))
-∗ False.
Proof. intro.
iIntros "(Hown & Ha)".
iDestruct (own_valid_2 with "Hown Ha") as "HH". exfalso. assumption.
Qed.
End S.
```
The snippet above:
- works fine with Iris 3.3
- takes a very long time at Qed with Iris 3.4 (modulo replacing `cmraT` with `cmra` in the script)
The issue seems to be with the use of auxiliary definitions to define the resource algebra `cfgUR`. Manually inlining `cfgUR` and the other auxiliary definitions in the definition of `cfgSG` makes it work again with Iris 3.4.
Since the fix is relatively simple, this issue doesn't seem to be too big of a deal, but I thought that I'd report it just in case.
Coq version used: 8.12.1 in both cases.https://gitlab.mpi-sws.org/iris/iris/-/issues/407Tracking issue for list RA2021-03-17T11:50:01ZRalf Jungjung@mpi-sws.orgTracking issue for list RAThis is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper....This is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.https://gitlab.mpi-sws.org/iris/iris/-/issues/410Modality for `Timeless`2021-04-19T07:51:21ZRalf Jungjung@mpi-sws.orgModality for `Timeless`We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ ...We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.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/412Use dfrac everywhere2022-06-07T01:57:21ZRalf 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/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/414Tracking issue for monotone RA2021-05-07T08:49:48ZRalf 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/416big_sep lemmas fail to apply when goal is not eta-expanded2021-05-26T11:31:56ZRalf Jungjung@mpi-sws.orgbig_sep lemmas fail to apply when goal is not eta-expandedI just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failu...I just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failure: iApply: cannot apply
(([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, ?Goal k y1 y2)
∗-∗ ?Goal ?Goal2 ?Goal3 ?Goal4
∗ ([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, if decide (k = ?Goal2) then emp else ?Goal k y1 y2))%I. *)
iApply (big_sepL2_delete Φ).
(* This works. *)
```
For some reason Coq needs to be manually given `Φ` here. That should not be the case.
The only difference between the lemma statement and the goal is an eta-expansion of `Φ`.https://gitlab.mpi-sws.org/iris/iris/-/issues/417Revert !118: Use ∃ instead of SIgma for extension axiom2022-08-02T16:52:12ZRobbert KrebbersRevert !118: Use ∃ instead of SIgma for extension axiomI am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet ...I am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet { multiset_car : list A }.
```
And define `dist` and `(≡)` to be modulo permutations. For permutations I use https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.SetoidPermutation.html
Unfortunately, this does not work: the extension axiom of cameras does not seem provable.
```coq
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
```
The problem is that I need to construct `z1` and `z2` as a sigma type, not an ordinary exist. But the type of permutations is a `Prop`, so I cannot do this.
Here's the whole code I have so far:
```coq
From Coq Require Import SetoidPermutation.
From iris.algebra Require Export cmra.
Lemma PermutationA_mono {A} (R1 R2 : relation A) xs1 xs2 :
(∀ x1 x2, R1 x1 x2 → R2 x1 x2) →
PermutationA R1 xs1 xs2 → PermutationA R2 xs1 xs2.
Proof. induction 2; econstructor; by eauto. Qed.
Record multiset A := MultiSet { multiset_car : list A }.
Arguments MultiSet {_} _.
Arguments multiset_car {_} _.
Section multiset.
Context {A : ofe}.
Implicit Types x y : A.
Implicit Types X Y : multiset A.
Local Instance multiset_equiv_instance : Equiv (multiset A) := λ X1 X2,
∀ n, PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_dist_instance : Dist (multiset A) := λ n X1 X2,
PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_valid_instance : Valid (multiset A) := λ _, True.
Local Instance multiset_validN_instance : ValidN (multiset A) := λ _ _, True.
Local Instance multiset_unit_instance : Unit (multiset A) := MultiSet [].
Local Instance multiset_op_instance : Op (multiset A) := λ X1 X2,
MultiSet (multiset_car X1 ++ multiset_car X2).
Local Instance multiset_pcore_instance : PCore (multiset A) := λ X, Some ε.
Global Instance multiset_singleton : Singleton A (multiset A) := λ x,
MultiSet [x].
Lemma multiset_ofe_mixin : OfeMixin (multiset A).
Proof.
split; rewrite /equiv /dist /multiset_equiv_instance /multiset_dist_instance /=.
- done.
- intros n. split.
+ by intros X.
+ intros X1 X2 ?. done.
+ intros X1 X2 X3 ??. by etrans.
- intros n X1 X2. apply PermutationA_mono, dist_S.
Qed.
Canonical Structure multisetO := Ofe (multiset A) multiset_ofe_mixin.
Global Instance multiset_ofe_discrete : OfeDiscrete A → OfeDiscrete multisetO.
Proof.
intros HA [xs1] [xs2] Hxs n. revert Hxs. apply PermutationA_mono.
by intros x1 x2 ->%(discrete _).
Qed.
Lemma multiset_cmra_mixin : CmraMixin (multiset A).
Proof.
apply cmra_total_mixin; try by eauto.
- intros X n Y1 Y2 HY. by apply (PermutationA_app _).
- by intros n X1 X2.
- intros X1 X2 X3. admit. (* boring case *)
- intros X1 X2 n. apply (PermutationA_app_comm _).
- by intros X n.
- intros X1 X2 _. exists ε. by intros n.
- intros n [xs] [ys1] [ys2] _. rewrite /equiv /dist /op
/multiset_equiv_instance /multiset_dist_instance /multiset_op_instance /=.
(* Stuck here. The witness [PermutationA (dist n) xs (ys1 ++ ys2)] basically
says how the elements in [xs] are distributed over [ys1] and [ys2].
Intuitively, it says element 0 of [xs] goes to position [i0] in
[ys1 ++ ys2], element 1 of [xs] goes to position [i1] in ys1 ++ ys2 and so
on. *)
(* I would like to use the lemma [PermutationA_decompose], but that does
not work since it gives an [∃]. *)
(* I tried to prove it by induction on the list instead, but that seems
pointless. At some point I need to invert on the [PermutationA] witness,
which is not possible. *)
induction ys1 as [|y1 ys1 IH]; intros Hxs; simpl in *.
{ by exists (MultiSet []), (MultiSet xs). }
admit.
Admitted.
Canonical Structure multisetR := Cmra (multiset A) multiset_cmra_mixin.
Lemma multiset_ucmra_mixin : UcmraMixin (multiset A).
Proof. split; [done | | done]. by intros X n. Qed.
Canonical Structure multisetUR := Ucmra (multiset A) multiset_ucmra_mixin.
Global Instance multiset_cancelable X : Cancelable X.
Proof. Admitted.
Global Instance multiset_singleton_ne : NonExpansive (singleton (B:=multiset A)).
Proof. intros n x1 x2. by repeat constructor. Qed.
Global Instance multiset_singleton_proper :
Proper ((≡) ==> (≡)) (singleton (B:=multiset A)).
Proof. apply (ne_proper _). Qed.
Global Instance multiset_singleton_dist_inj n :
Inj (dist n) (dist n) (singleton (B:=multiset A)).
Proof. intros x1 x2. Admitted.
Global Instance multiset_singleton_inj :
Inj (≡) (≡) (singleton (B:=multiset A)).
Proof.
intros x1 x2 Hx. apply equiv_dist=> n. apply (inj singleton). by rewrite Hx.
Qed.
End multiset.
Global Arguments multisetO : clear implicits.
Global Arguments multisetR : clear implicits.
Global Arguments multisetUR : clear implicits.
```https://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/419Iron slowdown investigation2021-06-17T07:20:40ZRalf Jungjung@mpi-sws.orgIron slowdown investigationIron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iri...Iron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iris from `dev.2021-03-06.3.b0708b01` to `dev.2021-06-03.0.2959900d`. I am not sure if we can do anything about that, but it would be good to at least figure out which changes caused the slowdown (though it looks like there at several, so this might be "death by a thousand cuts").https://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2022-05-06T12:01:06ZRalf 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/422`iApply` does not use `FromAssumption` for goal matching2021-08-05T14:57:38ZRobbert Krebbers`iApply` does not use `FromAssumption` for goal matching```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} ...```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
(P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
```
When using `iApply` in combination with the `with` clause, it will first `iSpecialize` and then use `iApply`, which in these examples turns to the degenerate case of `iExact`. The `iExact` tactic uses `FromAssumption` to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).
When using `iApply` without the `with` clause, it will launch a search using `IntoWand` where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.
The problem is the instance:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
Here, `Q` should match exactly. I tried strengtening it to:
```coq
Global Instance into_wand_wand p q P Q P' Q' :
FromAssumption q P P' →
FromAssumption (p && q) Q' Q →
IntoWand p q (P' -∗ Q') P Q.
```
However, that causes other problems: in some cases the above instance will be triggered instead of instances like `into_wand_bupd_args` causing the following to go wrong:
```coq
Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
(P -∗ Q) -∗ |==> Q.
Proof.
iIntros "H".
iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)
```
This issue came up in practice Simuliris.https://gitlab.mpi-sws.org/iris/iris/-/issues/423⌜...⌝ uses bad scopes2021-06-18T22:07:47ZRalf Jungjung@mpi-sws.org⌜...⌝ uses bad scopes`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
...`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
```
This leads to `+` being interpreted as a type.
I think we should remove `%type` here. Not sure about `%stdpp`.https://gitlab.mpi-sws.org/iris/iris/-/issues/424Laterable cleanup2021-07-15T07:49:33ZRalf Jungjung@mpi-sws.orgLaterable cleanuphttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `late...https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `laterable_alt`).
* [ ] Rename `make_laterable` to follow our modality naming scheme... `laterably`?
* [ ] Resolve TC backtracking issue around `persistent_laterable`
* [ ] `iMod` for `make_laterable` elimination?https://gitlab.mpi-sws.org/iris/iris/-/issues/425Splitting (some of) the laws for persistence into a separate class.2022-05-12T16:54:40ZDan FruminSplitting (some of) the laws for persistence into a separate class.I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persiste...I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persistence modality that can be equipped onto an arbitrary BI.
For later, the BI interface includes the operation itself in the signature, and states a bunch of laws that are satisfied by a degenerate instance of the later modality, and the law that is _not_ satisfied by the degenerate version is in a separate class `BiLöb`.
Would something like that be possible for the persistence modality?
For example, the laws `bi_mixin_persistently_absorbing` and `bi_mixin_persistently_and_sep_elim` could be moved into a separate typeclass; then the remaining laws could be satisfied by the identity function.https://gitlab.mpi-sws.org/iris/iris/-/issues/426Notation `≼@{A}` is missing2021-07-07T11:02:38ZRobbert KrebbersNotation `≼@{A}` is missingWe are probably missing such notations for more relations. It would be good to do a sweep.We are probably missing such notations for more relations. It would be good to do a sweep.https://gitlab.mpi-sws.org/iris/iris/-/issues/427Upstreaming big_op lemmas2021-07-16T09:37:22ZMichael SammlerUpstreaming big_op lemmasRefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
len...RefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
length l1 = length l2 →
([∗ list] k↦x ∈ l1, Φ k x) -∗
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen); destruct l2 => //=; simpl in *.
iDestruct "Hl" as "[Hx1 Hl]". iSplitL "Hx1". by iApply "Himpl".
iApply ("IH" $! (Φ ∘ S) (Ψ ∘ S) l2 _ with "[] Hl").
iIntros "!>" (k y1 y2 ?) "Hl2 /= ?".
by iApply ("Himpl" with "[] [Hl2]").
Unshelve. lia.
Qed.
End sep_list.
Lemma big_sepL2_impl' {A B C D} (Φ : _ → _ → _ → PROP) (Ψ : _ → _ → _ → _) (l1 : list A) (l2 : list B) (l1' : list C) (l2' : list D) `{!BiAffine PROP} :
length l1 = length l1' → length l2 = length l2' →
([∗ list] k↦x;y ∈ l1; l2, Φ k x y) -∗
□ (∀ k x1 x2 y1 y2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ ⌜l1' !! k = Some y1⌝ -∗ ⌜l2' !! k = Some y2⌝ -∗ Φ k x1 x2 -∗ Ψ k y1 y2) -∗
[∗ list] k↦x;y ∈ l1';l2', Ψ k x y.
Proof.
iIntros (Hlen1 Hlen2) "Hl #Himpl".
rewrite !big_sepL2_alt. iDestruct "Hl" as (Hl1) "Hl".
iSplit. { iPureIntro. congruence. }
iApply (big_sepL_impl' with "Hl"). { rewrite !zip_with_length. lia. }
iIntros "!>" (k [x1 x2] [y1 y2]).
rewrite !lookup_zip_with_Some.
iDestruct 1 as %(?&?&?&?).
iDestruct 1 as %(?&?&?&?). simplify_eq. destruct_and!.
by iApply "Himpl".
Qed.
```
How can one prove these lemmas in a way that they can be upstreamed?https://gitlab.mpi-sws.org/iris/iris/-/issues/428Make `iDestruct` work on `▷ ∃` if goal is except_0/update2021-07-22T13:02:40ZRobbert KrebbersMake `iDestruct` work on `▷ ∃` if goal is except_0/updateBIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
I...BIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
Instead, you get an except-0 (`◇`) modality, which can be eliminated if the goal is, for example, an update modality.
This trick is not commonly known, so it would be great if the proof mode's `iDestruct` tactic could use `bi.later_exist_except_0` automatically instead of just failing when the domain `A` is not inhabited.
This is what happens now:
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import updates.
Lemma test `{BiFUpd PROP} {A} (Φ : A → PROP) (Q : PROP) E :
▷ (∃ x, Φ x) ={E}=∗ Q.
Proof.
iIntros "H".
(* Goal:
"H" : ▷ (∃ x : A, Φ x)
--------------------------------------∗
|={E}=> Q *)
(* Tactic failure: iExistDestruct: cannot destruct (▷ (∃ x : A, Φ x))%I. *)
Fail iDestruct "H" as (x) "H".
(* Works *)
iMod (bi.later_exist_except_0 with "H") as (x) "H".
```
I tried to implement what I proposed in this MR some day, but I could not find a satisfactory generalization of the `IntoExist` class. After all, that class then needs to take the goal into account to eliminate the ◇ modality.
An alternative, we could use the `pm_error` infrastructure from #413 (which still needs to be ported to `IntoExists`) to give an error that points the user to `bi.later_exist_except_0` in case the domain `A` is not inhabited.https://gitlab.mpi-sws.org/iris/iris/-/issues/429Enable the use of the proofmode for proving big-op lemmas2021-07-28T12:28:45ZRalf Jungjung@mpi-sws.orgEnable the use of the proofmode for proving big-op lemmasThere are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find s...There are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find some way to stratify this, so that only some core set of lemmas needs to be shown without the proofmode, and the rest can use the proofmode.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/431Add generalized implication lemma for sets, etc.2021-07-29T07:29:12ZSimon Friis VindumAdd generalized implication lemma for sets, etc.!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X...!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X1 X2 :
([∗ set] x ∈ X1, Φ k x) -∗
□ (∀ (x : X),
⌜x ∈ X2⌝ →
((⌜x ∈ X1⌝ ∧ Φ x) ∨ <affinely> ⌜x ¬∈ X1⌝) -∗
Ψ x) -∗
([∗ set] y ∈ X2, Ψ y) ∗
([∗ set] x ∈ X1∖X2, Φ x).
```https://gitlab.mpi-sws.org/iris/iris/-/issues/433Tracking issue for HeapLang improvements2021-09-26T00:23:01ZTej Chajedtchajed@mit.eduTracking issue for HeapLang improvementsWe (primarily @robbertkrebbers, @jung, @tchajed, @arthuraa) have a few ideas for improving HeapLang as a language to write programs in. One way to improve HeapLang is by adding libraries, and another way is to add primitives to the langu...We (primarily @robbertkrebbers, @jung, @tchajed, @arthuraa) have a few ideas for improving HeapLang as a language to write programs in. One way to improve HeapLang is by adding libraries, and another way is to add primitives to the language.
Libraries are nice because they don't break backwards compatibility, don't make metatheory harder, and are easy to incrementally develop, test, and improve. There are already libraries floating around, so this effort would be mainly developing good specifications and ergonomics, then distributing the libraries so people can start using them.
# Library support
Some libraries we would like to support include:
- n-ary products and sums, either on the heap or as pure values
- lists and maps, either on the heap or as pure values
Here are a few concrete tasks to get started:
- [ ] Implement pattern matching for products. It would look something like `let: ("a", "b") := "p" in ...` and would bind `"a"` and `"b"` to `Fst "p"` and `Snd "p"`. This is interesting because it's the simplest example we could come up with of a derived construct with binders.
- [ ] Experiment with a nice sum pattern matching library, desugaring to `match:` but with support for a list of variants.
- [ ] Implement a generic list matching library, for list values.
- [ ] Implement a heap linked-list library. Give it a spec in terms of `list val` and then a derived spec that takes `list_rep {A:Type} (l:list A) (Φ: A -> iProp) (v:val)`, relating the list reference `v` to a Gallina list via a representation predicate for each element.
- [ ] Implement a map library along the same lines as the heap linked-list library, using a `gmap val val` and a representation predicate.
# Language improvements
One simplification to the language's representation is to consolidate constructors. The best illustration of this is [simp_lang](https://github.com/tchajed/iris-simp-lang/blob/9ae960be92d23fcf2c96fc8108d3c70c0b790db6/src/lang.v#L75-L77) which already does this; for example, `Fst`, `Snd`, `InjL`, and `InjR` are all consolidated into a single `UnOp op` constructor with a Gallina inductive `op` to identify which operation it is. One resulting simplification is that these all share the same evaluation contexts.
We could have primitive algebraic data types. This has the strong downside of requiring metatheory like logical relations to handle them in some way, whereas right now they only need cases for binary sums and products, with a simple pattern matching construct for sums that takes two lambdas. n-ary pattern matching on sums takes an arbitrary number of lambdas, which is complicated.
Adding a type discriminator would allow a generic, polymorphic equality operator. For metatheory like logical relations, most likely most users would just forbid type discrimination (eg, by not including it in the type system or logical relation), partly because it breaks abstraction.https://gitlab.mpi-sws.org/iris/iris/-/issues/434Diverging `iFrame` with predicate evar2021-10-01T18:46:05ZRalf Jungjung@mpi-sws.orgDiverging `iFrame` with predicate evarThis is a minimized version of a diverging `iFrame` I found in Perennial:
```
Lemma test_iFrame_pred_evar (P Q : PROP) :
P -∗ ∃ (Φ : nat → PROP), ((∃ n, id (Φ n)) ∨ Q).
Proof. iIntros "HP". iExists _. iFrame "HP".
```
The goal at the t...This is a minimized version of a diverging `iFrame` I found in Perennial:
```
Lemma test_iFrame_pred_evar (P Q : PROP) :
P -∗ ∃ (Φ : nat → PROP), ((∃ n, id (Φ n)) ∨ Q).
Proof. iIntros "HP". iExists _. iFrame "HP".
```
The goal at the time of framing is
```
"HP" : P
--------------------------------------∗
(∃ n : nat, id (?Goal n)) ∨ Q
```
All these components seem necessary: when I remove the disjunction, the exisential, or the `id`, the divergence goes away.
In the trace, I can see that it is phantasizing a bigMS into existence, but I do not know why:
```
Debug: 1.1-1.1-1.1-1.1-1.12: simple apply @frame_instances.frame_big_sepMS_disj_union on
(Frame false P (id (?Goal a)) (?Ψ a)), 1 subgoal(s)
Debug:
1.1-1.1-1.1-1.1-1.12-1 : (Frame false P (([∗ mset] y ∈ ?X1, ?Φ y) ∗ ([∗ mset] y ∈ ?X2, ?Φ y)) (?Ψ a))
```
I think one part of the problem is that the extra `id` means that `(id (?Goal a))` does not start with an evar, so the `!` is circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/438Use HB.lock(-like) sealing2022-01-20T01:44:18ZRalf Jungjung@mpi-sws.orgUse HB.lock(-like) sealinghierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a dif...hierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a difference in practice.
Quoting from https://github.com/math-comp/hierarchy-builder/wiki/Locking:
```
HB.lock Definition new_concept := 999999.
Lemma test x : new_concept ^ x ^ new_concept = x ^ new_concept ^ new_concept.
Proof.
Time Fail reflexivity. (* takes 0s *)
rewrite new_concept.unlock.
Time Fail reflexivity. (* takes 7s, the original body is restored *)
Abort.
```
This is exactly the kind of locking API I always wanted: just adding a keyword in front of the `Definition`, done. This would make it a no-brainer to seal basically every `iProp` that our reusable libraries export.
TODO:
- Check if this actually works in Iris
- Decide if we want to do this, and how -- are we okay with a dependency on hierarchy-builder?https://gitlab.mpi-sws.org/iris/iris/-/issues/439Tracking issue for append-only list RA2022-01-21T21:41:49ZRalf 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.
The a...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.
The algebra part of this has been merged; what remains is the base_logic wrapper.
## Open issues
* 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/441Upstream later credits2022-05-07T06:29:38ZRalf Jungjung@mpi-sws.orgUpstream later credits@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I k...@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I keep forgetting what exactly are the `fupd` laws that we would lose by doing this, so maybe we can put that here. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/442Potentially add Frame instances for all our Fractional instances2022-01-17T02:02:14ZRalf Jungjung@mpi-sws.orgPotentially add Frame instances for all our Fractional instancesIn https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
...In https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
```
This is useful since it matches on the head symbol of the framed expression, which is a lot more efficient than `frame_fractional`.
However, we have more `Fractional` instances in the codebase, which for now do not support framing any more:
* `Fractional (λ q, mono_nat_auth_own γ q n)`
* `Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L)`
* `Fractional (λ q, k ↪[γ]{#q} v)` (for `ghost_map`)
* `Fractional (λ q, ghost_map_auth γ q m)`
* `Fractional (λ q, ghost_var γ q a)`
* `Fractional (cinv_own γ)`
If the need comes up, we should add them back. Also, if it was easier to add them (e.g. with some kind of macro), there'd be less hesitation to add these instances everywhere.https://gitlab.mpi-sws.org/iris/iris/-/issues/449Add internalised rules for derived resource algebras2022-03-04T00:38:47ZJonas KastbergAdd internalised rules for derived resource algebrasWorking with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in ...Working with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in the model), `auth_both_validN` (in the model, with step-indices), and `auth_both_validI` (in the logic).
Some derived resource algebras are missing their "internalised rules" (those of the logic).
This issue is then to address the lack of these rules.
One example of a resource algebra with missing rules are `mono_list`.
In full, to solve this issue we should:
- Identify all resource algebras with missing internalised rules
- Add the missing rules
- (Settle on a potential pipeline for future algebras to ensure that the rules are included)https://gitlab.mpi-sws.org/iris/iris/-/issues/451iPoseProof with malformed pm_trm diverges2022-04-08T06:14:55ZWilliam ManskyiPoseProof with malformed pm_trm diverges<!--
When reporting a bug, please always include the version of Iris you are using.
If you are using opam, you can determine your Iris version by running
opam show coq-iris -f version
-->
Some of my Iris students stumbled across th...<!--
When reporting a bug, please always include the version of Iris you are using.
If you are using opam, you can determine your Iris version by running
opam show coq-iris -f version
-->
Some of my Iris students stumbled across this issue: when iPoseProof and derived tactics are given a bad proof mode term, they appear to run forever instead of giving an error. A minimal example:
```
Lemma test Σ (P : iProp Σ) : P -∗ P.
Proof.
iIntros "P".
iPoseProof ("P" "P") as "H". (* diverges *)
```
This is a pretty silly example, but it's easy to stumble into if you forget the `$!` or `with` notation:
```
Lemma test2 Σ (P : expr -> iProp Σ) (x : nat) : (∀ x, P x) -∗ P #x.
Proof.
iIntros "P".
iPoseProof ("P" #x) as "H". (* diverges *)
```
This appears to be the case in versions from 3.4.0 to the current dev version (dev.2022-04-07.0.8fa39f7c).https://gitlab.mpi-sws.org/iris/iris/-/issues/452"wp_apply ... as"2022-08-23T15:48:54ZRalf 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/457"-" in selection patterns2022-04-19T22:58:30ZRalf Jungjung@mpi-sws.org"-" in selection patternsIt would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.It would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.https://gitlab.mpi-sws.org/iris/iris/-/issues/458Inconsistency in weakening of modalities in `iApply`2022-05-01T11:54:32ZRobbert 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/460Improve iCombine to derive validity properties of ghost state automatically2022-05-11T14:27:08ZIke MulderImprove iCombine to derive validity properties of ghost state automaticallyIt would be great if `iCombine` was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if `iCombin...It would be great if `iCombine` was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if `iCombine` takes an extra (optional) `gives` clause, which provides extra persistent facts (if those exist).
For example, consider the following environment:
```
"H1" : l ↦{#q1} v1
"H2" : l ↦{#q2} v2
```
executing `iCombine "H1 H2" as "H" gives %[Hq Hv]` should replace `"H1"` and `"H2"` with `"H": l ↦{#(q1 + q2)} v1` and introduces two new pure hypotheses `Hq : q1 + q2 ≤ 1` and `Hv : v1 = v2`.
The roadmap for implementing this would be split into two merge requests:
1. Change `FromSep` to only be used for `iSplit{L,R}`, change `iCombine` to rely on two new typeclasses `CombineSepAs` and `CombineSepGives`.
These would be defined as `CombineSepAs P1 P2 P := P1 ∗ P2 ⊢ P` where `P1 P2` are input, `P` output
and `CombineSepGives P1 P2 := P1 ∗ P2 ⊢ <pers> R` where `P1 P2` are input, `R` output.
This MR would provide some instances for stuff in `base_logic.lib`, `mapsto`.
The new syntax would be `iCombine "Hs" [as "H"] [gives "P"]`, where either the `as` clause or the `gives` clause must be present.
* If `as "H"` is present, all hypotheses `"Hs"` will be replaced by `"H"`, which can be an introduction pattern.
If not present, all `"Hs"` are kept as is
* If `gives "P"` is present, additionally learn persistent fact `"P"`, which can be an introduction pattern. Also supports `%?` introduction if this fact is pure.
* If more than two hypotheses are provided in `"Hs"`, repeatedly run `CombineSep` with the accumulated results
* There will be an additional boolean indicating whether `CombineSepAs` used the default instance.
2. Give general instance for `own` (= MR !771, addresses #251)
This is a summary of a discussion by @jung, @robbertkrebbers, @snyke7 and @gmalecha at the Iris Workshop. Let me know if I forgot something.https://gitlab.mpi-sws.org/iris/iris/-/issues/462iRewrite with a Coq-level equality gives bad error message2022-05-20T17:14:58ZRalf Jungjung@mpi-sws.orgiRewrite with a Coq-level equality gives bad error messageIn a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at le...In a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at least the tactic should tell me what is wrong. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/463Rename "head step"?2022-06-10T18:13:39ZRalf Jungjung@mpi-sws.orgRename "head step"?At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.https://gitlab.mpi-sws.org/iris/iris/-/issues/471Planning for dune support (draft)2022-08-16T19:09:49ZPaolo G. GiarrussoPlanning for dune support (draft)Supporting dune would let users benefit from the dune cache, composable builds, etc. OTOH, its Coq support still has rough edges; in particular, `make vos` and `make validate` have no analogue yet.
Ralf was open to supporting dune as lo...Supporting dune would let users benefit from the dune cache, composable builds, etc. OTOH, its Coq support still has rough edges; in particular, `make vos` and `make validate` have no analogue yet.
Ralf was open to supporting dune as long as somebody else volunteered to maintain suport for it: https://mattermost.mpi-sws.org/iris/pl/bjqieom1tjrqmck6ahh9zp5ipc. I volunteer to help; I'd like somebody else to do that as well.
Various increments are possible:
1. enable building stdpp without tests
2. enable building iris, without tests; here we must choose whether to assume stdpp is installed, or assume it is part of the dune workspace and use compositional builds;
3. enable using dune in CI
4. document how to take advantage of dune — adding pointers on external docs where possible
- either document work arounds to use with Proof General (add `_build/default` to `_CoqProject`), or get the issue fixed properly upstream
5. migrate tests to dune cram tests (and potentially migrate Makefile.coq.local to support the new syntax)
I have some ideas of the maintenance costs.
- Coq warning flags need be synchronized between coq_makefile and dune
- Tests need be formatted as cram testshttps://gitlab.mpi-sws.org/iris/iris/-/issues/473Logically atomic triples conflict with autosubst notation2022-08-04T21:51:13ZRalf Jungjung@mpi-sws.orgLogically atomic triples conflict with autosubst notationAutosubst uses `>>` and `>>>` as notation for some operations, which conflicts with our logically atomic triples:
```
Section notation_conflicts.
Context `{!heapGS Σ}.
(* Test compatibility with autosubst notation. *)
Reserved Not...Autosubst uses `>>` and `>>>` as notation for some operations, which conflicts with our logically atomic triples:
```
Section notation_conflicts.
Context `{!heapGS Σ}.
(* Test compatibility with autosubst notation. *)
Reserved Notation "f >>> g" (at level 56, left associativity).
Reserved Notation "sigma >> tau" (at level 56, left associativity).
Lemma conflict_test1 P Q e v :
⊢ <<< P >>> e @ ∅ <<< Q, RET v >>>.
(* Syntax error: '>>>' expected after [term level 200] (in [term]) *)
```
I tried changing the `'>>>'` in our notations to `>>>` or to `'>' '>' '>'`, neither of that helped. (We are using `} } }` for texan triples, I have no idea why.) I also tried removing the level declarations from the logatom triples, again that made no difference. I don't actually understand what is happening here anyway, these were complete shots in the dark.
We need someone who actually understand the Coq notation system for this... maybe @blaisorblade?https://gitlab.mpi-sws.org/iris/iris/-/issues/475Provide some way to "seal" a BI2022-08-12T14:53:14ZRalf Jungjung@mpi-sws.orgProvide some way to "seal" a BIOne reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms i...One reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms in general are just bigger.
It might be worth investigating some nice way to seal a BI (but that would probably have to be a macro):
- either lightweight sealing by just making it TC opaque and forwarding all instances
- or a proper seal that makes terms no convertible any more, and a *lot* of forwarding of things
We *do* seal `iProp` pretty heavily (in fact even more proper than the "proper" seal, this is the one place where we use a module type for sealing to be *really sure*), so Iris itself doesn't have this problem.
@robbertkrebbers IIRC you did an experiment along the lines of doing that by hand once? What were the results of that again?https://gitlab.mpi-sws.org/iris/iris/-/issues/476Have `known_make_absorbingly` and `make_absorbingly_default` instances in the...2022-08-15T14:17:18ZRalf Jungjung@mpi-sws.orgHave `known_make_absorbingly` and `make_absorbingly_default` instances in the same fileThe following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instan...The following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instances to `classes_make`, or move the other one here?https://gitlab.mpi-sws.org/iris/iris/-/issues/477`iFrame` peforms some surprising modality cleanup2022-08-15T15:40:00ZRalf Jungjung@mpi-sws.org`iFrame` peforms some surprising modality cleanupFraming `<affine> P` on goal `<affine> <affine> (P ∗ Q)` produces the result `<affine> Q`. I think that is rather srprising and would have expected `<affine> <affine> Q`. It seems like as it traverses the term, `iFrame` is a bit too quic...Framing `<affine> P` on goal `<affine> <affine> (P ∗ Q)` produces the result `<affine> Q`. I think that is rather srprising and would have expected `<affine> <affine> Q`. It seems like as it traverses the term, `iFrame` is a bit too quick to apply the `MakeAffine` class even when there was a literal affinely modality before that should IMO just be preserved.
For `<absorb>` and `<pers>`, `iFrame` just fails in the same situation. The same is true for `□`, but when one has `P` in the intuitionistic context, then one can frame into goal `□ □ (P ∗ Q)` and once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/842 lands that will produce `□ Q`.https://gitlab.mpi-sws.org/iris/iris/-/issues/478Adding satisfiable to Iris2022-08-17T05:24:37ZSimon SpiesAdding satisfiable to IrisSeveral Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notio...Several Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notion of `satisfiable` can be added to Iris in a meaningful way and whether it can enable more modular adequacy proofs in the future.https://gitlab.mpi-sws.org/iris/iris/-/issues/479`if b then ... else ...` is never persistent2022-08-17T16:51:28ZRalf Jungjung@mpi-sws.org`if b then ... else ...` is never persistentIn some situations it is fairly natural to write a proposition as `if b then P else Q`, where `b: bool`. However, even if both `P` and `Q` are persistent, such a proposition cannot be moved into the persistent context, which can be somew...In some situations it is fairly natural to write a proposition as `if b then P else Q`, where `b: bool`. However, even if both `P` and `Q` are persistent, such a proposition cannot be moved into the persistent context, which can be somewhat annoying.
So I wonder, should we add instances for propositions defined via `if`? Which typeclasses should get such instances? Is there some way we can make this work for *all* typeclasses in one go?