Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-10-27T13:17:57Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/64Destruct patterns: Support -> and <- (at least) for pure Coq equalities, and ...2017-10-27T13:17:57ZRalf Jungjung@mpi-sws.orgDestruct patterns: Support -> and <- (at least) for pure Coq equalities, and maybe injection patternsIn lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; i...In lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %[= ->]`, i.e., there is an additional injection applied. Any way we could also get that in the proof mode? Maybe even using the "injective" typeclass so that it doesn't have to be the constructor of an inductive type (however, of course it'd also have to support all constructors, so it can't rely just on that typeclass).Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/65Wish: Prelude support for currying (and other operations) on gmap.2017-05-19T15:20:29ZJannoWish: Prelude support for currying (and other operations) on gmap.The following operations would (or could) be quite useful in my planned clean-up of iGPS:
1. Converting `gmap A (gmap B C)` to `gmap (A* B) (C)` and vice versa.
1. Converting `gmap A B` to `gmap A (A * B)` by copying the argument.
1. C...The following operations would (or could) be quite useful in my planned clean-up of iGPS:
1. Converting `gmap A (gmap B C)` to `gmap (A* B) (C)` and vice versa.
1. Converting `gmap A B` to `gmap A (A * B)` by copying the argument.
1. Converting `gmap A B` as a `gset (A * B)` (possibly by simply adding a ElemOf instance and corresponding lemma).
As Robbert already mentioned to me, these things probably should be generalized. I think there is a general map-filter function lurking in there somewhere. One that gives access to both the key and the value and returns and optional results which is used for the new gmap. I might be wrong though.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/66Use a "settings" file for setting options within the project2020-09-10T17:37:08ZRalf Jungjung@mpi-sws.orgUse a "settings" file for setting options within the projectFollowing a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to d...Following a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to discuss is the name of that file... I suggest putting it into the root, i.e. sth. like `theories/options.v`.https://gitlab.mpi-sws.org/iris/iris/-/issues/67iAssert does not support destructing existentials2017-05-19T15:20:29ZJacques-Henri JourdaniAssert does not support destructing existentialsIt seems like I cannot use something like:
```
iAssert (∃ a, P a) with "[]" as (a) "H".
```It seems like I cannot use something like:
```
iAssert (∃ a, P a) with "[]" as (a) "H".
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/68iSpecialize should work even if the wand is under a later.2017-05-19T15:20:29ZJacques-Henri JourdaniSpecialize should work even if the wand is under a later.In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/69Make `done` solve the goal when one of the Iris hypothesis is `False`2017-05-19T15:20:29ZJacques-Henri JourdanMake `done` solve the goal when one of the Iris hypothesis is `False`As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.https://gitlab.mpi-sws.org/iris/iris/-/issues/70`wp_apply` cannot deal with curried lemmas2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.org`wp_apply` cannot deal with curried lemmasThe `wp_apply` tactic was written in a time when all our lemmas were uncurried. It always distributes all the resources of the current context to one of the goals that it creates, not leaving any control to the user. I think we need some...The `wp_apply` tactic was written in a time when all our lemmas were uncurried. It always distributes all the resources of the current context to one of the goals that it creates, not leaving any control to the user. I think we need something like `wp_apply with "<spec pattern>"` to accommodate curried lemmas.
See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/lang/spawn.v#L77> and <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/typing/unsafe/cell.v#L165> for some examples.https://gitlab.mpi-sws.org/iris/iris/-/issues/71Framing in Disjunctions2019-11-01T13:20:31ZJannoFraming in Disjunctions@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize t...@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize that such an instance potentially leads to unsolvable goals more often than any of the existing framing instances. So this should probably not be the default behavior of `iFrame`. Nonetheless, the functionality was extremely convenient in some places. Often, disjunctive goals could easily be closed by framing out a bunch of resources and closing the goal with a `by` prefix or a separate `done`. No `iLeft` or `iRight` was needed.
I wonder if Iris could still benefit from such rules by adding a marker in the syntax for `iFrame`, e.g. `iFrame "!H"`, which applies the more reckless disjunction framing rules. The same could be applied for specialization patterns with something like `$!H`.
What do you think?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/72Support `iCombine "H1 H2 ..." as "Hx"`2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgSupport `iCombine "H1 H2 ..." as "Hx"`It'd be nice if `iCombine` supported passing a single string of space-separated hypothesis instead of insisting on two strings, each being a single name. Combining more than two hypothesis would be done by folding.It'd be nice if `iCombine` supported passing a single string of space-separated hypothesis instead of insisting on two strings, each being a single name. Combining more than two hypothesis would be done by folding.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/73Specialization patterns syntax extensions2017-05-19T15:20:29ZRobbert KrebbersSpecialization patterns syntax extensionsThere have been some requests to add new stuff to specialization patterns:
1. A `//` token for performing `done`. One could then write things like `[$H1 $H2 //]` or `[//]`.
2. Being able to frame in persistent specialization patterns, i...There have been some requests to add new stuff to specialization patterns:
1. A `//` token for performing `done`. One could then write things like `[$H1 $H2 //]` or `[//]`.
2. Being able to frame in persistent specialization patterns, i.e. `[# $H1 $H2]`.
3. A token, say `[$]` to solve the goal by framing, and by keeping all unused hypotheses for the subsequent goals.
However, there are some questions here:
1. I suppose we want to be able to use `//` also for pure and persistent goals. For example `[% //]` and `[# //]`.
2. What is going to happen when we do `[# H1 $H2]`. There are some obvious choices: a.) using a hypothesis without a `$` prefix is forbidden b.) ignore all hypotheses that are not prefixed with a `$` (there is no need to select hypotheses, you get all anyway, since the goal is persistent) c.) prune the context that goal.
3. What to frame? Just the spatial hypotheses, or everything (including the persistent ones)?
Anyone some ideas? I would like to have a syntax that is not too FUBARed.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/74iNext does not strip off both laters from ▷ P ∗ ▷ Q2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgiNext does not strip off both laters from ▷ P ∗ ▷ QI would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```I would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/75Build any merge request on the CI2017-05-19T15:20:29ZRobbert KrebbersBuild any merge request on the CICurrently, I have to change the `.gitlab-ci.yml` in the branch corresponding to the merge request. This is a bit cumbersome, because I have to be careful to not merge the commit in which I changed `.gitlab-ci.yml` when merging into maste...Currently, I have to change the `.gitlab-ci.yml` in the branch corresponding to the merge request. This is a bit cumbersome, because I have to be careful to not merge the commit in which I changed `.gitlab-ci.yml` when merging into master.
Would it be possible to automatically build any branch corresponding to an MR on the CI?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/76`iDestruct` for big ops2017-05-19T15:20:29ZRobbert Krebbers`iDestruct` for big opsTogether with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ ...Together with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x
we could use `iDestruct "H" as "[H1 H2]"` to turn it into:
H1 : Φ 0 y
H2 : [∗ list] k ↦ x ∈ l, Φ (S k) x
Although this is not particularly difficult to implement (it just requires one to declare suitable `IntoAnd` instances), it gives rise to some potential ambiguity, namely, what is going to happen when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x ∗ Ψ k x
Will it split through the cons, or through the star inside of the predicate in the big op?
Currently, it will split through the ∗ due to the instance `into_and_big_sepL`. Declaring yet another `IntoAnd` instance for the `cons` case is a bad idea, as it will give rise to the ambiguity above, and we end up with tactics that will behave unpredictably.
However, I think that the `cons` instance would be much more useful than the `∗` instance, hence I propose to drop the current `∗` instance, and instead declare instances for `cons` (and possibly `app`, which does not lead to ambiguity).https://gitlab.mpi-sws.org/iris/iris/-/issues/77Have iNext "pull" laters out from below other operators.2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgHave iNext "pull" laters out from below other operators.Let's say I have a goal of the shape `∃ x, ▷ Q x` (and the type of `x` is inhabited). I also have an assumption below a later. I want to strip the later from the assumption, which is okay because our goal is equivalent to `▷ ∃ x, Q x`. C...Let's say I have a goal of the shape `∃ x, ▷ Q x` (and the type of `x` is inhabited). I also have an assumption below a later. I want to strip the later from the assumption, which is okay because our goal is equivalent to `▷ ∃ x, Q x`. Currently, I have to do `rewrite -uPred.later_exist` for this.
First of all, I am wondering why `iApply uPred.later_exist` doesn't work in this context. Secondly, it'd be nice if `iNext` could also "pull" laters out of the goal if there's not yet a top-level later.https://gitlab.mpi-sws.org/iris/iris/-/issues/79Make iSplit work below existentials?2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMake iSplit work below existentials?I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; f...I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; first done.`. This works because some part of what is below the existential does not depend on the witness.
Now I wonder, would it make sense for `iSplit` to work in this case (giving me ` ⌜#l = #l⌝` and `∃ x : vec val m, ▷ l ↦∗ x` as goals)? The rewrite I did above is not very discoverable, but neither is the `iSplit`. What do you think? @jjourdan @robbertkrebbers
(You may wonder why I have things under the existential that do not depend on the witness. The reason is that lemmas of the form `∃ x y z, P` work much better with the proofmode, because I an do a single `iDestruct ... as (x y z) ...`. If I pushed the existential down, destructing things would become much more annoying.)https://gitlab.mpi-sws.org/iris/iris/-/issues/80More precise error message on missing hypothesis2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMore precise error message on missing hypothesisCurrently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found ...Currently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found (while actually, only some of them have not been found). It is also not as useful as the error would be if it would name which hypothesis has not been found.
I assume spec patterns have the same issue.https://gitlab.mpi-sws.org/iris/iris/-/issues/81Let iAlways clear the spatial context2017-10-27T12:33:40ZRalf Jungjung@mpi-sws.orgLet iAlways clear the spatial contextRight now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is simil...Right now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is similar to the difference between `iIntros "!>"` and `iNext` -- the latter may affect the context, the former will not. Furthermore, this is backwards compatible because iAlways will now only succeed in strictly more cases.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/82Consider adding a "strong" always modality2018-01-31T09:21:27ZRalf Jungjung@mpi-sws.orgConsider adding a "strong" always modalityThe idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default...The idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default should be not to add anything unless we really need it -- and we got pretty far without the strong always.
So what do we have that this would enable? (I am writing "SB" for the strong box below.)
* Propositional extensionality. Not sure how useful that would be though.
* `(|=> SB P) -> SB P`, i.e. basic updates can be removed around the strong box. That seems pretty powerful, but the only application we have so far is to make the adequacy lemma nicer to state (no more "nested laters and basic updates", but just "nested laters").
* It would be possible to have the "core of a proposition" in a clean way, defined as `∀ Q, SB (Q -> □Q) -> SB (P -> Q) → □ Q`. This works because `SB P -> □ Q` is persistent.
@robbertkrebbers I seem to remember you saying that one of the Iris-based papers added the strong box. Why again did they need it?
I am not convinced that the above is enough of a reason to add the box to the core. In particular, I feel like it would be non-trivial to explain to people why we have two box-like modalities.https://gitlab.mpi-sws.org/iris/iris/-/issues/84iDestruct on non-existing name yields "no matching clause for match"2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgiDestruct on non-existing name yields "no matching clause for match"Title says it all. Goal state:
```
============================
"Hincl" : type_incl ty1 ty2
"Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
"Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
"Hsincl" :...Title says it all. Goal state:
```
============================
"Hincl" : type_incl ty1 ty2
"Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
"Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
"Hsincl" : ∀ (κ0 : lft) (tid0 : thread_id) (l0 : loc),
ty_shr ty1 κ0 tid0 l0 -∗ ty_shr ty2 κ0 tid0 l0
--------------------------------------□
"Hshr" : ty_shr (rc ty1) κ tid l
--------------------------------------∗
ty_shr (rc ty2) κ tid l
```
Tactic: `iDestruct "Hst" as (??) "H".`
Error: `Error: No matching clauses for match.`https://gitlab.mpi-sws.org/iris/iris/-/issues/85Proof mode goals in empty context cannot be distinguished from Coq goals2017-05-19T15:20:29ZRobbert KrebbersProof mode goals in empty context cannot be distinguished from Coq goals@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We...@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We could add some special symbol to the proof mode notation with the empty context? Any suggestions?Robbert KrebbersRobbert Krebbers