Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T13:33:12Zhttps://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/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/123Add a general constructor from an affine BI2019-11-01T13:24:47ZRalf Jungjung@mpi-sws.orgAdd a general constructor from an affine BIIn master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just...In master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just claims them to be `(ADMISSIBLE)` in a comment.
I see two ways to achieve that:
* We could provide a general way to construct a `BiMixin` from a proof of all the laws given in the appendix.
* We could do the more specific thing and first prove the appendix laws for `uPred`, and subsequently not use `unseal` when proving the `BiMixin`.https://gitlab.mpi-sws.org/iris/iris/-/issues/117Make some of the `wp_` tactics language independent2019-11-01T13:23:45ZRobbert KrebbersMake some of the `wp_` tactics language independentA large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.A large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.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/104smarter iIntros for plainly modality2019-11-01T13:16:44ZRobbert Krebberssmarter iIntros for plainly modalityThe following discussion from !71 should be addressed:
- [ ] @jung started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/71#note_20642): (+1 comment)
> Would it be a good idea or not for `iIntros` to be able...The following discussion from !71 should be addressed:
- [ ] @jung started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/71#note_20642): (+1 comment)
> Would it be a good idea or not for `iIntros` to be able to do this without us having to apply `persistently_impl_plainly`? To me, that looks very similar to how it pulls out universal quantifiers from below a box.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/89Support negative selection patterns2019-11-01T13:16:44ZRalf Jungjung@mpi-sws.orgSupport negative selection patternsIt would be nice to say something like "clear everything except for ...".It would be nice to say something like "clear everything except for ...".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/36STSs: Consider changing the def. of frame-steps2019-11-01T13:16:11ZRalf Jungjung@mpi-sws.orgSTSs: Consider changing the def. of frame-stepsJeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification...Jeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.https://gitlab.mpi-sws.org/iris/iris/-/issues/21iDestruct and iPureIntro2019-11-01T13:14:54ZGhost UseriDestruct and iPureIntroI recently bumped into a scenario like this:
```
H : heapN ⊥ N
o', n' : Z
============================
"~" : heap_ctx
"~1" : inv N
(∃ o n : Z,
(l ↦ (#o, #n) ∧ ■ (o < n))
★ (au...I recently bumped into a scenario like this:
```
H : heapN ⊥ N
o', n' : Z
============================
"~" : heap_ctx
"~1" : inv N
(∃ o n : Z,
(l ↦ (#o, #n) ∧ ■ (o < n))
★ (auth_own γ {[o := ()]} ∨ own γ (Excl ()) ★ R))
"IH" : (locked l R -★ R -★ Φ #()) -★ WP acquire #l {{ v, Φ v }}
--------------------------------------□
"H2" : ■ (o' < n')
--------------------------------------★
■ (o' < n' + 1)
```
To prove this, I have to first `iDestruct "H2" as "%"` to move `o' < n'` to Coq context, then I can `iPureIntro` and do the following proof.
My problem is, will it be good to let `iPureIntro` (or invent something on top of it) to handle the `iDestruct` here for me?
Or even more convenient, it is possible to apply pure theorems directly in this context?
Thanks!https://gitlab.mpi-sws.org/iris/iris/-/issues/29Bring back Logically Atomic Triples (Coq + docs)2019-11-01T13:09:17ZJeehoon Kangjeehoon.kang@kaist.ac.krBring back Logically Atomic Triples (Coq + docs)* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendi...* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
- Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.
---
@jung wrote
The POPL 2015 appendix has been split into two parts:
* The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/
* The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)
What, specifically, are you missing from the POPL 2015 appendix?
https://gitlab.mpi-sws.org/iris/iris/-/issues/125Make `iClear` work when there is at least one absorbing spatial hypothesis2019-11-01T13:08:25ZRobbert KrebbersMake `iClear` work when there is at least one absorbing spatial hypothesis`iClear "H"` with `H : P` currently works if either the goal is absorbing, or `P` is affine. (The same applies to `iIntros "_"`).
We could add another case: there exists at least one spatial hypothesis that is absorbing.
See also the d...`iClear "H"` with `H : P` currently works if either the goal is absorbing, or `P` is affine. (The same applies to `iIntros "_"`).
We could add another case: there exists at least one spatial hypothesis that is absorbing.
See also the discussion in !98 for a possible use-case.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/134Document language interface2019-11-01T13:08:15ZRobbert KrebbersDocument language interfaceIt would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related doc...It would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related documentation, also including the current `ProofMode.md`. We could also LaTeX-ify all Coq documentation, and add it to the already existing theoretical documentation.https://gitlab.mpi-sws.org/iris/iris/-/issues/267Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.2019-11-01T13:07:58ZDan FruminInconsistent order of arguments for `inv_alloc` and `cinv_alloc`.```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_a...```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_alloc` first takes the namespace and then the mask, but `cinv_alloc` first takes the mask and the the namespace.https://gitlab.mpi-sws.org/iris/iris/-/issues/241"Flattened" introduction patterns for intuitionistic conjunction elimination.2019-11-01T13:07:29ZDan Frumin"Flattened" introduction patterns for intuitionistic conjunction elimination.The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `...The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `P ∧ Q ∧ R` by `iDestruct "H" as "(H&_&_)"`, but it doesn't work this way.
```
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Lemma test P Q R : (P ∧ Q ∧ R) -∗ P.
Proof.
iIntros "H".
(* This works fine *)
iDestruct "H" as "(_ & _ & H)".
Undo.
iDestruct "H" as "(_ & H & _)".
Undo.
(* This results in an error *)
Fail iDestruct "H" as "(H & _ & _)".
(* "Proper" way of doing it *)
iDestruct "H" as "(H & _)".
done.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/243Avoid type-level aliases for overloading of canonical structures2019-11-01T13:05:35ZRobbert KrebbersAvoid type-level aliases for overloading of canonical structuresIn https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a...In https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a canonical structure for a type... Why cannot we define `ufrac` as something like: `Record ufrac := uf_qp { qp_uf : Qp }.`? Sure, this will require some boilerplate for projecting and boxing fractions, but hoping that such hack will keep a stable behaviors seems rather optimistic!
This applies to `ufrac` (introduced in !195) and `mnat` (introduced a long time ago).https://gitlab.mpi-sws.org/iris/iris/-/issues/264Investigate use of "Filtered Unification"2019-11-01T13:02:29ZRalf Jungjung@mpi-sws.orgInvestigate use of "Filtered Unification"When I talked with Matthieu at ICFP about our unification problems, he told me to look at "filtered unification" and thought it might help. The docs are at https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.typeclasses-filte...When I talked with Matthieu at ICFP about our unification problems, he told me to look at "filtered unification" and thought it might help. The docs are at https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.typeclasses-filtered-unification.
So, let's look at that at some point. ;)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.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/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.
```