Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T13:57:21Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/212iMod: Control which modality is reduced2019-11-01T13:57:21ZRalf Jungjung@mpi-sws.orgiMod: Control which modality is reducedThe following proof script should work, but does not
```
Lemma test_iModElim_box P : □ P -∗ P.
Proof. iIntros ">H". iAssumption. Qed.
```The following proof script should work, but does not
```
Lemma test_iModElim_box P : □ P -∗ P.
Proof. iIntros ">H". iAssumption. Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/210Generic subset construction for RAs2020-09-08T20:33:39ZRalf Jungjung@mpi-sws.orgGeneric subset construction for RAsIn auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
...In auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
Related to https://gitlab.mpi-sws.org/FP/iris-coq/issues/42 (which also wants to touch `auth`).https://gitlab.mpi-sws.org/iris/iris/-/issues/203Seal off local and frame-preserving update2019-11-01T12:50:04ZRalf Jungjung@mpi-sws.orgSeal off local and frame-preserving updateThat might solve `apply` diverging all the time.That might solve `apply` diverging all the time.https://gitlab.mpi-sws.org/iris/iris/-/issues/202Use of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistent2020-11-06T14:42:49ZRobbert KrebbersUse of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistentSee the discussion here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/159#note_28898See the discussion here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/159#note_28898https://gitlab.mpi-sws.org/iris/iris/-/issues/188eauto very slow when there is a chain of Iris quantifiers2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgeauto very slow when there is a chain of Iris quantifiersSteps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e...Steps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None →
(∀ σ1, state_interp σ1 ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step. done.
(* now it gets slow *) eauto.
```
Something seems to be exponential in the number of quantifiers. We currently use `iIntros.` to introduce them all at once but that's more of a work-around. I can't even really figure out what is taking so long, but I can definitely see tons of `FromAssumption` in the trace.
Cc @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/186iAssert without any spatial assumptions should produce a persistent result2020-09-29T11:15:49ZRalf Jungjung@mpi-sws.orgiAssert without any spatial assumptions should produce a persistent resultThe following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```...The following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```
It currently fails because the update is not persistent -- however, this is an iAssert which is not provided any spatial assertions, so whatever it produces can always be put into the persistent context.https://gitlab.mpi-sws.org/iris/iris/-/issues/183Stronger/Weaker iFrame2022-12-06T22:37:13ZRalf Jungjung@mpi-sws.orgStronger/Weaker iFrameIn a situation like
```
H1: R
H2: P
----------------------*
R * (P /\ Q)
```
calling `iFrame` will turn the goal into
```
----------------------*
Q
```
This is too aggressive: Frequently, I will need `P` to prove `Q`.In a situation like
```
H1: R
H2: P
----------------------*
R * (P /\ Q)
```
calling `iFrame` will turn the goal into
```
----------------------*
Q
```
This is too aggressive: Frequently, I will need `P` to prove `Q`.https://gitlab.mpi-sws.org/iris/iris/-/issues/180Explore performance implications of gen_proofmode2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgExplore performance implications of gen_proofmodea74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> y...a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> yeah, the bottelneck is definitely notypeclasses refine: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/-/jobs/9346 took 29:47 user time
> btw we also have a 1min regression in this range: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/8799209d9c00f825e9ac059b3b864119e34f9aec...00b0c7704278028c4a73c9f0686a9070e92d3a06
> and ~30sec over https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/474f82283e423b03ccf0adeb367e36eb68346a29...8799209d9c00f825e9ac059b3b864119e34f9aec
Looking at the [performance graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1516679125714&to=now), the two commit ranges with the most sustained impact are LambdaRust-coq@c2c2b874eea8...00b0c7704278 and LambdaRust-coq@00b0c7704278...158d46797c99. They correspond to iris-coq@aa5b93f6319b9cb2d17a1c9f61947233b4033484...1a092f96b1350896c3801edb90b453f5b4d2a4cf and iris-coq@1a092f96b1350896c3801edb90b453f5b4d2a4cf...a74b8077f199e2d21ff49e91b5af0dfdcee362ff in Iris. The latter is just a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search), but the former is just a whole bunch of commits that, altogether, seem to have made things slower by 40sec in LambdaRust.
There is also some variation in [this part of the graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1518563995005&to=1520160053680) but I am not sure if that's real or just noise.https://gitlab.mpi-sws.org/iris/iris/-/issues/178`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviors2019-11-01T12:50:05ZJacques-Henri Jourdan`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviorsIn an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.In an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/175Replace booleans in proofmode typeclasses by a more informative type2019-11-01T12:51:13ZRalf Jungjung@mpi-sws.orgReplace booleans in proofmode typeclasses by a more informative typeWe have booleans in some of the proofmode typeclasses, which makes them pretty hard to read. We should use more informative types.
Right now, we seem to use booleans several times for the conditional intuitionistic modality, once for c...We have booleans in some of the proofmode typeclasses, which makes them pretty hard to read. We should use more informative types.
Right now, we seem to use booleans several times for the conditional intuitionistic modality, once for conditional affinity, and once for something completely different in `IntoLaterN`.https://gitlab.mpi-sws.org/iris/iris/-/issues/172String-free proofterms2020-09-08T16:20:11ZRalf Jungjung@mpi-sws.orgString-free prooftermsThe goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give...The goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give us significant speed-up. (We have a bet going here, with the threshold being 40% speedup. Let's see. ;)
@ppedrot, @janno and me recently spent some time thinking about this and I want to write this down before we forget. The basic idea is to have a version of `envs_entails`, say `envs_entails_nameless`, that takes two lists of propositions, instead of lists of pairs of strings and propositions. Now, we can `change` back and forth between `envs_entails named_env` and `envs_entails_nameless nameless_env` -- the two are convertible as we always have concrete lists for our environments. So before we apply any Coq tactic like `apply`, we always `change` the goal to its nameless form, and then `change` it back when we are done. These conversions are not actually recorded in the proof term; they only affect the type of the evar as stored in Coq, which is irrelevant at `Qed` time. Essentially, we use the type of the evar as per-goal mutable state to store the names in.
The main problem with this is that the `coq_tactics` would have to be written in nameless style, and the Ltac tactics wrapping them would have to take care of setting the right names in the subgoals they create. However, this is a problem that any solution to the issue will have -- if strings move out of the proof terms, we can't have them in Coq-level lemmas. Maybe Ltac2/Mtac could provide some other (less hacky) form of per-goal mutable state, but that wouldn't change this problem.https://gitlab.mpi-sws.org/iris/iris/-/issues/169Applying plain implications fails2019-11-01T12:51:28ZRalf Jungjung@mpi-sws.orgApplying plain implications failsHere's two testcases, both fail currently:
```coq
Lemma test_apply_affine_wand2 `{!BiPlainly PROP} (P : PROP) :
P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
Proof. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ"...Here's two testcases, both fail currently:
```coq
Lemma test_apply_affine_wand2 `{!BiPlainly PROP} (P : PROP) :
P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
Proof. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
Lemma test_apply_affine_impl2 `{!BiPlainly PROP} (P : PROP) :
P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).
Proof. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/168iSpecialize on implications behaves inconsistently2019-11-01T13:35:17ZRalf Jungjung@mpi-sws.orgiSpecialize on implications behaves inconsistentlyIn a goal like
```
"HP" : ■ P
--------------------------------------□
"HPQ" : ■ P → Q
--------------------------------------∗
Q
```
doing `iSpecialize ("HPQ" with "HP")` behaves as expected, but `iSpecialize ("HPQ" with "[]")` ...In a goal like
```
"HP" : ■ P
--------------------------------------□
"HPQ" : ■ P → Q
--------------------------------------∗
Q
```
doing `iSpecialize ("HPQ" with "HP")` behaves as expected, but `iSpecialize ("HPQ" with "[]")` fails saying
```
iSpecialize: (■ P → Q)%I not an implication/wand.
```
Here's a testcase:
```coq
Lemma test_plain_impl `{BiPlainly PROP} P Q :
(■ P → (■ P → Q) -∗ Q)%I.
Proof.
iIntros "#HP HPQ".
Fail iSpecialize ("HPQ" with "[]").
Fail iApply "HPQ".
iSpecialize ("HPQ" with "HP"). done.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/167iMod should be able to eliminate <pers> and <plain> in the intuitionistic con...2019-11-01T12:51:13ZRalf Jungjung@mpi-sws.orgiMod should be able to eliminate <pers> and <plain> in the intuitionistic contextWith an assumption `H: ■ P` in the intuitionistic context, I was wondering how I can eliminate that modality. Doing so relies on the fact that the intuitionistic context is affine, so this can't be done by just applying a lemma. Then I ...With an assumption `H: ■ P` in the intuitionistic context, I was wondering how I can eliminate that modality. Doing so relies on the fact that the intuitionistic context is affine, so this can't be done by just applying a lemma. Then I realized that `iMod` is what we use to eliminate modalities -- but it doesn't work here: I am told that `iMod` cannot eliminate this modality.
I suppose adding the right typeclass instances should fix this?https://gitlab.mpi-sws.org/iris/iris/-/issues/166iDestruct on a conjunction magically transforms hypothesis2019-11-01T13:33:50ZRalf Jungjung@mpi-sws.orgiDestruct on a conjunction magically transforms hypothesisThe following proof script
```
Lemma test_True_conj :
(@bi_emp PROP ∧ True) -∗ True.
Proof.
iIntros "H". iDestruct "H" as "[_ H]".
```
results in the following goal:
```
"H" : <affine> True
--------------------------------------∗...The following proof script
```
Lemma test_True_conj :
(@bi_emp PROP ∧ True) -∗ True.
Proof.
iIntros "H". iDestruct "H" as "[_ H]".
```
results in the following goal:
```
"H" : <affine> True
--------------------------------------∗
True
```
Notice how an "affinely" modality showed up suddenly. When I first saw this happen, I spent some minutes following notations and definitions to figure out where I had typed that modality without noticing. However, it turns out I did not -- the proof mode actually magically transforms my assertions! I think this is a bug.
Mostly, this is a bug because it's not at all what the user would expect. If you ask someone what `iDestruct "H" as "[_ H]".` does -- even someone familiar with the proof mode, even someone like me who thought about linear Iris quite a bit -- the answer would be "it applies `and_elim_r`". End of story. This is what the tactic does in Coq, and it is also what it does in the "old" IPM.
It is never a good idea to defy user expectations like that.
Also, I felt we had a pretty strong sense when designing the original IPM that we wouldn't mess with the users assertions unless we're asked to do so. I think that's one of the reasons IPM works so well -- it does plenty of magic under the hood, but you don't *see* it doing magic -- the effect of the magic is that whatever you think should happen, happens. We ask the user to be explicit about moving things to the persistent context, we ask them to be explicit about maintaining the current modality (like \later or the updates) when doing `iApply`. There was one exception around `True`, where `True -* P` behaves exactly like `P` in some cases, and it was pretty confusing and AFAIK was entirely removed.
So, please, let's stick to that. We have have plenty of things that are surprising to people. We should keep that to an absolute minimum.
@robbertkrebbers argued that this is about information loss. I don't even get the argument: Of course not all tactics we apply are bidirectional! Information loss is even frequently the explicit purpose of a tactic, like `clear` or `destruct foo as [_ foo]`. In the above goal, the user can write `iDestruct "H" as "#[_ H]"` if they want to remember that there are no resources here. I'm actually a little surprised this works, it seems to detect the `emp /\` as "affinely" even though I did not spell it that way?
I just noticed one can also write `iDestruct "H" as "[_ #H]"`. I'm pretty surprised that this works, because it seems to rely on the other conjunct that I already dropped -- but I'm not really offended by things "magically" working the way I told them to work. That's a totally different surprise than "I told it to do one thing and it did that and also painted my house blue".https://gitlab.mpi-sws.org/iris/iris/-/issues/165Better (?) approach to control typeclass resolution based on whether some arg...2019-11-01T13:33:12ZRalf Jungjung@mpi-sws.orgBetter (?) approach to control typeclass resolution based on whether some arguments are evarsRight now, some of our typeclasses have extra variants called `KnownXXX` that use `Hint Mode` to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.
Maybe a better approach would...Right now, some of our typeclasses have extra variants called `KnownXXX` that use `Hint Mode` to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.
Maybe a better approach would be to change the way we write some instances, and make sure they can only succeed if some arguments are not evars. I described such a solution at <https://gitlab.mpi-sws.org/FP/iris-coq/commit/a9d41b6374f44fd93629f99cfecfea3549baa0b1#note_25278>.
One possible concern is that applying such instances should fail as early as possible; if they have other premises, those shouldn't be resolved unless the evar check passes. On the other hand, the `KnownXXX` classes introduce additional coercions that typeclass resolution will try all the time, which could also be a performance issue.https://gitlab.mpi-sws.org/iris/iris/-/issues/163Dealing with nested modalities in `iModIntro`2020-06-29T10:38:08ZRobbert KrebbersDealing with nested modalities in `iModIntro`We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 →...We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
```
This instance allows introduction of e.g. updates below `monPred_at`.
When we add a `FromModal` instance for `monPred_at P i`, we end up with ambiguity when introducing `monPred_at (|==> P) i`: should `|==>` or `monPred_at` be introduced?
Concretely, we should:
- [ ] Add a `FromModal` instance for `monPred_at`
- [ ] Get the priorities of that instance and e.g. the above `from_modal_monPred_at` right
- [x] Do the same for `embed`https://gitlab.mpi-sws.org/iris/iris/-/issues/152iRewrite: Support rewriting with Coq hypotheses2019-11-01T12:51:27ZRalf Jungjung@mpi-sws.orgiRewrite: Support rewriting with Coq hypothesesiRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without `Proper` instances.
Cc @tslilyaiiRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without `Proper` instances.
Cc @tslilyaiRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/150Smarter iFrame: Prefer framing below `*` over framing below disjunction or wand2019-11-01T13:31:27ZRalf Jungjung@mpi-sws.orgSmarter iFrame: Prefer framing below `*` over framing below disjunction or wandWhen framing below a disjunction or a wand/implication, it can happen that `P` could have been framed elsewhere, and that would have been smarter. This is the case both for `(True \/ P) * P` and `(False -* P) * P`.
One possible way to ...When framing below a disjunction or a wand/implication, it can happen that `P` could have been framed elsewhere, and that would have been smarter. This is the case both for `(True \/ P) * P` and `(False -* P) * P`.
One possible way to solve this would be to have some kind of precedence for "framing positions" and not stop searching just because we found one below a disjunction/wand.https://gitlab.mpi-sws.org/iris/iris/-/issues/139Better names and documentation for proof mode typeclasses2020-11-23T02:33:06ZRalf Jungjung@mpi-sws.orgBetter names and documentation for proof mode typeclassesI think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs...I think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs, what are the outputs, what's it supposed to do?
Don't expect people know what the `Hint Mode` sigils mean, I certainly don't. ;)
I am thinking of something like
```coq
(* Input: `P`; Outputs: `Q1`, `Q2`.
Strengthen `P` into a disjunction. Used for `iLeft`, `iRight`. *)
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
(* Input: `P`; Outputs: `Q1`, `Q2`.
Weaken `P` into a disjunction. Used for disjunction elimination patterns. *)
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P ⊢ Q1 ∨ Q2.
```
For classes like `ElimModal` or `AddModal`, I have a hard time figuring out what they mean because they are stated in an extremely general way.