Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T11:07:41Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/215Explore getting rid of implication2019-11-01T11:07:41ZRalf Jungjung@mpi-sws.orgExplore getting rid of implicationIt seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. ...It seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. We could remove implication from the MoSeL interface and see what happens.
For Iris itself I mostly expect this to work, but the general linear case might make this harder. Or not.https://gitlab.mpi-sws.org/iris/iris/-/issues/237Stripping laterN from pure propositions when proving laterN *without except-0*2019-11-01T11:09:51ZPaolo G. GiarrussoStripping laterN from pure propositions when proving laterN *without except-0*I just proved that, for uniform predicates, when proving `▷^i Q`, you can strip `▷^i` from `"Hfoo": ▷^i ⌜ P ⌝`, for arbitrary uniform predicates. Statements:
`(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.`
`(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).`
I ...I just proved that, for uniform predicates, when proving `▷^i Q`, you can strip `▷^i` from `"Hfoo": ▷^i ⌜ P ⌝`, for arbitrary uniform predicates. Statements:
`(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.`
`(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).`
I needed this in my proof; could we add support for this in Iris? I'm not sending a MR because the code is far from ready for that.
Was this already possible? I didn't find how, and thought this would need some new variant of except-0 (an except-i modality).
- IPM suggested that wouldn't work — `iDestruct "Hfoo" as "%"` complains that `Hfoo` is not pure, even when the conclusion starts with `▷^i`.
- The proof is by case distinction on the world: in worlds `n < i`, the conclusion is trivial, while in worlds `n >= i`, we have that `▷^i ⌜ P ⌝ → P`. This must be done in the model.
My proof is easy for later, but laterN was trickier; I'm also not sure where this proof would go (since laterN is a derived connective, but the proof for laterN goes in the model).
I expect one could lift this lemma to wand as well (since `▷^i ⌜ P ⌝` is persistent, this shouldn't need going to the model).
- These lemmas are also a bit inconvenient to use; it's not clear that `IntoPure` supports such conditional tactics. A typical example, for hypothesis "Hlclw": ▷^i ⌜ nclosed_vl w 0 ⌝, is:
```
iApply (strip_pure_laterN i with "[] Hlclw").
iIntros (Hclw).
```
`iRevert "Hlclw"; iApply strip_pure_wand_laterN; iIntros (Hclw)` might also work, given a version for wand.
My proof script is:
```coq
From iris.base_logic Require Import base_logic lib.iprop.
Import uPred.
Section uPred_later_extra.
Context `{M: ucmraT}.
Implicit Types (Q: uPred M) (x: M).
Lemma laterN_pure_id i n P x: i <= n →
(▷^i uPred_pure_def P)%I n x → P.
Proof.
move => Hle H; induction i => //=.
apply IHi; first lia.
elim: i n Hle H {IHi} => [|i IHi] [|n] Hle;
unseal => // H; first lia.
apply IHi; first lia. by unseal.
Qed.
Lemma laterN_trivial i n Q x: i > n →
(▷^i Q)%I n x.
Proof.
move: i => [|i] Hle. by lia.
apply uPred_mono with i x; eauto with lia.
elim: i {Hle}; by unseal.
Qed.
Lemma strip_pure_later P Q:
(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).
Proof.
unseal; constructor => n x Hvx Hyp [|n'] // ?????.
by apply Hyp.
Qed.
Lemma strip_pure_laterN i P Q:
(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.
Proof.
unseal; constructor => n x Hvx Hyp n' //= x' ?? Hvx' H.
destruct (decide (i <= n')) as [Hle|Hge].
- by eapply Hyp, laterN_pure_id.
- by apply laterN_trivial; lia.
Qed.
End uPred_later_extra.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/235Documentation for the algebra folder2019-11-01T11:10:11ZRobbert KrebbersDocumentation for the algebra folderIt would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical...It would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical structures are used.https://gitlab.mpi-sws.org/iris/iris/-/issues/231Allow swapping later^i and forall, later, etc.2019-11-01T11:12:12ZPaolo G. GiarrussoAllow swapping later^i and forall, later, etc.For swapping later^i and forall, an instance suffices: https://gist.github.com/Blaisorblade/3f9e41b7f044617fd5789b0d3554a2d7 (I suppose this isn't good enough for a PR).
For swapping later^i and later, I'm not sure what's the typeclass, ...For swapping later^i and forall, an instance suffices: https://gist.github.com/Blaisorblade/3f9e41b7f044617fd5789b0d3554a2d7 (I suppose this isn't good enough for a PR).
For swapping later^i and later, I'm not sure what's the typeclass, but it should be possible — I do the swaps through complicated proofs, applied inline.
Generally, I suspect all the instances for later could be lifted (by induction) to later^i, and I suspect I'd be willing to do that work (once I move).https://gitlab.mpi-sws.org/iris/iris/-/issues/58Proofmode with Coq binders, and without strings2019-11-01T11:15:16ZRalf Jungjung@mpi-sws.orgProofmode with Coq binders, and without strings@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust sig...@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust significantly. We could also not use strings, which may even help with speed. (Well, strings are not very efficient in Coq -- but I kind of doubt that's out bottleneck currently.)
I'll leave it to Janno to explain the idea, because I would totally screw that up.
I any case, even if we want to go for this, this is a long-term thing... definitely post-3.0, and definitely breaking everybody using Iris horribly (if we don't just keep the string-based stuff around).https://gitlab.mpi-sws.org/iris/iris/-/issues/242Planning the Iris 3.2 release2019-11-01T12:31:44ZRalf Jungjung@mpi-sws.orgPlanning the Iris 3.2 releaseI have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I...I have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I think we should make that release soon-ish. Are there any issues or MRs that you think should be included? Let's collect them in [this milestone](https://gitlab.mpi-sws.org/iris/iris/milestones/4).
We might consider doing the release after the POPL deadline so that our Iris-using POPL submissions (if any) can claim to be compatible with Iris 3.2. But honestly I don't think that is a big factor, the artifacts should anyway bundle the right version of Iris -- and I'd rather avoid extra coordination overhead if possible.
After the release:
* [ ] Drop support for Coq 8.7, and enable the `sigT`-functor notation (at the bottom of `ofe.v`).Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/247iInv does not behave as intended when the goal is an accessor2019-11-01T12:32:42ZRalf Jungjung@mpi-sws.orgiInv does not behave as intended when the goal is an accessorWhen the goal is of the form
```
|={⊤,∅}=> ∃ ..., P ∗ (Q ={∅,⊤}=∗ Φ )
```
I would hope `iInv N` where the invariant assertion is `I` to turn it into something like
```
|={N,∅}=> ∃ ..., P ∗ (I * Q ={∅,⊤}=∗ Φ )
```
but currently we have no...When the goal is of the form
```
|={⊤,∅}=> ∃ ..., P ∗ (Q ={∅,⊤}=∗ Φ )
```
I would hope `iInv N` where the invariant assertion is `I` to turn it into something like
```
|={N,∅}=> ∃ ..., P ∗ (I * Q ={∅,⊤}=∗ Φ )
```
but currently we have no good way to even detect the goal as an accessor, so none of this can happen.https://gitlab.mpi-sws.org/iris/iris/-/issues/254Reliance on `Export` bug2019-11-01T12:48:48ZMaxime DénèsReliance on `Export` bugDear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is...Dear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is an easy way to observe the problem on Coq master: take `algebra.ufrac_auth`, and change the first line:
```coq
From iris.algebra Require Export auth frac.
```
into:
```coq
From iris.algebra Require Export auth.
From iris.algebra Require Export frac.
```
it will make the proof of `ufrac_auth_agreeN` fail because a view starts applying in the wrong direction...
Could you provide some guidance on how to make the file pass with the two separate `Export`s? It will probably make it compatible with the fix of the bug I mentioned above.
Thanks!https://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/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/196Extend `iApply` to deal with pure goals2019-11-01T12:50:03ZGlen MévelExtend `iApply` to deal with pure goalsIf I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Pr...If I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Prop) (P : iProp Σ) :
(A → B) → (P -∗ ⌜A⌝) → (P -∗ ⌜B⌝).
Proof.
iIntros (ab pa) "p".
(* what I would like to write directly: *)
Fail iApply ab. (* Tactic failure: iPoseProof: not a uPred. *)
(* what I need to write instead: *)
iApply (uPred.pure_mono _ _ ab).
iApply pa.
iExact "p".
Qed.
```
(tested with coq-iris dev.2018-04-10.0)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/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/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/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/137Iris-internal solve_proper2019-11-01T12:51:26ZRalf Jungjung@mpi-sws.orgIris-internal solve_properWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRustWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRusthttps://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/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/261Provide smart `bi` constructor for BIs that are not step-indexed2019-11-01T13:00:45ZRobbert KrebbersProvide smart `bi` constructor for BIs that are not step-indexedIn that case, we can just define the distance relation on the OFE as:
```coq
P ≡{n}≡ Q := P ⊢ Q ∧ Q ⊢ P
```
And all `Proper` axioms should be admissible.In that case, we can just define the distance relation on the OFE as:
```coq
P ≡{n}≡ Q := P ⊢ Q ∧ Q ⊢ P
```
And all `Proper` axioms should be admissible.https://gitlab.mpi-sws.org/iris/iris/-/issues/263IPM/MoSeL nested disjunction syntax2019-11-01T13:02:01ZDan FruminIPM/MoSeL nested disjunction syntaxWould it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.Would it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.