Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-05-19T15:20:29Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/61iLöb doesn't work in the empty context.2017-05-19T15:20:29ZJannoiLöb doesn't work in the empty context.As witnessed by the following example.
```
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*".
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
Proof.
Fail (iLöb as "IH" forall (e Closed0)).
iAssert (True)%I as "T"; [by admit|].
(iLöb as "IH" forall (e Closed0)).
Abort.
```
I guess with the new unified handling of reverting hypotheses this probably applies to other tactics as well.As witnessed by the following example.
```
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*".
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
Proof.
Fail (iLöb as "IH" forall (e Closed0)).
iAssert (True)%I as "T"; [by admit|].
(iLöb as "IH" forall (e Closed0)).
Abort.
```
I guess with the new unified handling of reverting hypotheses this probably applies to other tactics as well.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/62Specialization (iApply/iMod) often diverges on missing *2017-11-16T09:36:42ZRalf Jungjung@mpi-sws.orgSpecialization (iApply/iMod) often diverges on missing *When specializing a lemma that contains Iris-level universal quantifiers, if I forget to add the `*` to the pattern, the tactic frequently diverges. This is very frustrating as it is not even clear what's wrong, or where the `*` has to be added.
If you want, I can create a minimal example. Right now, one way to see this is to remove the `*` from the `iMod` in `weakestpre.wp_atomic`, line 172.When specializing a lemma that contains Iris-level universal quantifiers, if I forget to add the `*` to the pattern, the tactic frequently diverges. This is very frustrating as it is not even clear what's wrong, or where the `*` has to be added.
If you want, I can create a minimal example. Right now, one way to see this is to remove the `*` from the `iMod` in `weakestpre.wp_atomic`, line 172.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/63gmultiset.gmultiset_eq_dec applied too eagerly?2017-05-19T15:20:29ZJannogmultiset.gmultiset_eq_dec applied too eagerly?I don't have time to debug this in more detail so I am just going to dump a representative trace here. Without exception, all my diverging type class searches (of which I have a few per hour) eventually look like this one:
[trace.txt](/uploads/1fad04b1b2cb32d92e41f976f8853f1f/trace.txt)
(Just in case somebody actually looks at it: the piece of code you can see in line 1 doesn't actually make any sense, I think.)I don't have time to debug this in more detail so I am just going to dump a representative trace here. Without exception, all my diverging type class searches (of which I have a few per hour) eventually look like this one:
[trace.txt](/uploads/1fad04b1b2cb32d92e41f976f8853f1f/trace.txt)
(Just in case somebody actually looks at it: the piece of code you can see in line 1 doesn't actually make any sense, I think.)https://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]"; 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).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. 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.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 discuss is the name of that file... I suggest putting it into the root, i.e. sth. like `theories/options.v`.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 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.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 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?@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.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.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 master.
Would it be possible to automatically build any branch corresponding to an MR on the CI?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, Φ 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).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`. 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.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/78Trouble with iApply and typeclass inference order2019-11-01T13:16:44ZRalf Jungjung@mpi-sws.orgTrouble with iApply and typeclass inference orderThe following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```The following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```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; 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.)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 (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.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.