Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-05-03T13:06:04Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/184`wp_binop` is not very useful for comparing arbitrary values2018-05-03T13:06:04ZDan Frumin`wp_binop` is not very useful for comparing arbitrary valuesConsider the following piece of code:
```
From iris.heap_lang Require Export proofmode notation.
Lemma wut `{heapG Σ} (v1 v2 : val) :
(WP if: (v1 = v2) then #0 else #0 {{ _, True }})%I.
Proof.
wp_binop.
Abort.
```
The goal that I ...Consider the following piece of code:
```
From iris.heap_lang Require Export proofmode notation.
Lemma wut `{heapG Σ} (v1 v2 : val) :
(WP if: (v1 = v2) then #0 else #0 {{ _, True }})%I.
Proof.
wp_binop.
Abort.
```
The goal that I expected after executing `wp_binop`:
```
WP if: #(bool_decide (v1 = v2)) then #0 else #0 {{ _, True }}
```
Instead I got two goals:
- `bin_op_eval EqOp v1 v2 = Some ?Goal0`
- `WP if: ?Goal0 then #0 else #0 {{ _, True }}`
This is not very helpful, as it is pretty annoying to get a boolean value for ?Goal0.
I believe this is due to the way that `bin_op_eval` is defined:
it first matches `v1` and `v2` for specific types of values (integers or booleans), and only then considers the case of generalized equality checks.
Since we have generalized/dynamic equality checks in heap_lang, why not first match on the type of the operation, and only then match on the values in `bin_op_eval`?
Best
-Danhttps://gitlab.mpi-sws.org/iris/iris/-/issues/183Stronger/Weaker iFrame2021-02-03T22:31:23ZRalf 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/182done when goal is evar picks unnecessarily strong2018-07-13T08:40:31ZRalf Jungjung@mpi-sws.orgdone when goal is evar picks unnecessarily strongWhen the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spa...When the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spatial, I guess) hypothesis instead of just `True` or `emp`.
Maybe we should add `bi.True_intro` with high priority to the database?https://gitlab.mpi-sws.org/iris/iris/-/issues/181wp_apply instantiates evars too far2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgwp_apply instantiates evars too far```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s;...```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s; ?E {{ v, ?Φ v }}
```
but it should be
```
============================
--------------------------------------∗
?Q
```
This is in the generalized proofmode branch.Robbert KrebbersRobbert Krebbershttps://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/179Strengthen strong allocation lemmas to work for any infinite set2019-02-17T18:14:30ZRalf Jungjung@mpi-sws.orgStrengthen strong allocation lemmas to work for any infinite setNow that std++ has https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/blob/master/theories/infinite.v, we should be able to provide stronger versions of `own_alloc_strong` and similar lemmas.Now that std++ has https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/blob/master/theories/infinite.v, we should be able to provide stronger versions of `own_alloc_strong` and similar lemmas.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/177Improve naming of lemmas about modalities2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgImprove naming of lemmas about modalitiesThe following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1...The following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2_{swap,comm}: M1 (M2 P) ⊣⊢ M2 (M1 P)
```
However, @robbertkrebbers noted that we have plenty of lemmas of the last form. Optimizing for conciseness, we could also use
```
M1_{into,impl,entails}_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
```Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/176Reconsider normalizing `/\ emp` into `<affine>`2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgReconsider normalizing `/\ emp` into `<affine>`I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `...I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `emp`, not `True`. So, framing let's say `P` in `P ∗ Q` turns it into `emp ∗ Q`, which then get beautified into `Q`.
> In this case, you are framing `P` in `<pers> Q ∧ P`, which will turn it into `<pers> Q ∧ emp`. This is then beautified into `<affine> <pers> Q`
I think we should not perform this normalization, and just keep it as `<pers> Q /\ emp`.Generalized Proofmode Mergerhttps://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/174Confusing result by `wp_op`2018-04-22T18:08:36ZRobbert KrebbersConfusing result by `wp_op`As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(W...As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(WP if: #n = v then #true else #false {{ _, True }})%I.
Proof.
wp_op.
```
This gives
```coq
bin_op_eval EqOp #n v = Some ?Goal0
______________________________________(2/2)
--------------------------------------∗
WP if: ?Goal0 then #true else #false {{ _, True }}
```
Pre !97 this used to work because `bin_op_eval` used to match first on the operations and then on the operand. Right now, it first matches on the operands, and only then on the operation.https://gitlab.mpi-sws.org/iris/iris/-/issues/173Ambiguous reference to eqb in coq_tactics.v2018-03-12T13:17:31ZGhost UserAmbiguous reference to eqb in coq_tactics.vWhile preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theor...While preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theories/proofmode/coq_tactics.v` fails to compile due to 2 unqualified references to `eqb` not been seen as `Bool.eqb` anymore.
This issue can be fixed in a straightforward (and backward-compatible) way : replace the two occurrence of `eqb` in this file (lines 95 and 288) by `Bool.eqb` (or alternatively, add an `Import Bool` at the end of this file's header).
Sorry for not proposing a pull request directly, but apparently I do not have enough permission to fork on your gitlab.
For this fix to be correctly taken in account by our travis testing infrastructure, could you please update the `opam` file of repository `LambdaRust-coq.git` to mention a fixed version of `iris-coq` ? Currently it points to `iris-coq` version `dev.2018-02-23.0`, leading to commit `db735a4558ad`.
Thanks!
Pierre Letouzeyhttps://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/171Split derived_laws.v2018-03-21T15:05:46ZRalf Jungjung@mpi-sws.orgSplit derived_laws.v`derived_laws.v` is a very-hard-to-navigate monster. Can we find a good way to split it?
One fairly obvious thing to do is to split the `Sbi` stuff into a separate file. Then the `Bi` file will still be huge, probably... what could be a...`derived_laws.v` is a very-hard-to-navigate monster. Can we find a good way to split it?
One fairly obvious thing to do is to split the `Sbi` stuff into a separate file. Then the `Bi` file will still be huge, probably... what could be a good criterion to separate that?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/170iFresh should reserve fresh names2018-07-13T08:51:26ZJoseph TassarottiiFresh should reserve fresh namesRight now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
...Right now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
```
let H1 := iFresh in
let H2 := eval vm_compute in (match H1 with
| IAnon x => IAnon (1 + x)
| INamed x => IAnon 1
end) in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
iDestruct "H" as pat.
```
because `iDestruct` will also use `iFresh` and gets a name that conflicts with `H1`.
One solution would be to add a counter to the `envs` record which is incremented each time `iFresh` is called. This would actually also probably make `iFresh` more efficient anyway.Robbert KrebbersRobbert Krebbershttps://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.