Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T12:48:48Zhttps://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/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/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/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/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/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/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/266`iDestruct 1` does not work when `Z_scope` is open2019-09-20T12:30:26ZJacques-Henri Jourdan`iDestruct 1` does not work when `Z_scope` is openIn this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.In this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.https://gitlab.mpi-sws.org/iris/iris/-/issues/265Add an "iStopProof" tactic2019-09-11T14:48:57ZJonas KastbergAdd an "iStopProof" tacticThere is currently no tactic to escape the IPM.
This make it so that pre-existing tactics that have been developed for the logic can no longer be used, once you are in the proof mode.
This is applicable assuming that someone migrates to ...There is currently no tactic to escape the IPM.
This make it so that pre-existing tactics that have been developed for the logic can no longer be used, once you are in the proof mode.
This is applicable assuming that someone migrates to IPM from an existing development, and want to keep being able to use their tactics, in-between progress made with IPM.
A WIP solution is as follows:
```
Lemma stop_proof {PROP : bi} c (P : PROP) :
P ->
environments.envs_entails
{|
environments.env_intuitionistic := environments.Enil;
environments.env_spatial := environments.Enil;
environments.env_counter := c |} P.
Proof. rewrite environments.envs_entails_eq. iIntros. iApply H. Qed.
Ltac iStopProof := apply stop_proof.
Ltac iStopProof' := iRevert "#∗"; iStopProof.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/256Consisent direction for `CMRA_NAME_op` lemmas.2019-08-13T16:01:57ZDan FruminConsisent direction for `CMRA_NAME_op` lemmas.I've noticed something which can be seen as a discrepancy in the lemmas.
These ones follow the pattern "constructor of the multiplication is equal to the multiplication of constructors".
```
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ ...I've noticed something which can be seen as a discrepancy in the lemmas.
These ones follow the pattern "constructor of the multiplication is equal to the multiplication of constructors".
```
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
```
These ones go the other way around: "multiplication of constructors is equal to the constructor of multiplications":
```
Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a').
Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b').
Lemma pair_op (a a' : A) (b b' : B) : (a, b) ⋅ (a', b') = (a ⋅ a', b ⋅ b').
```
Should this be changed or am I nitpicking and the (breaking) change will be too invasive?https://gitlab.mpi-sws.org/iris/iris/-/issues/260Confusing error message if iLoeb is not available (non-step indexed BI)2019-08-13T11:22:50ZDan FruminConfusing error message if iLoeb is not available (non-step indexed BI)Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : bi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH".
```
(PROP should have type `sbi`)
Error message:
```
In nested Ltac calls to...Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : bi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH".
```
(PROP should have type `sbi`)
Error message:
```
In nested Ltac calls to "iLöb as (constr)", "iLöbRevert (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)",
"go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iLöbCore as IH), "tac" (bound to iLöbCore as IH),
"iLöbCore as (constr)" and "notypeclasses refine (uconstr)", last call failed.
In environment
PROP : bi
k : nat
Φ : nat → PROP
The term "coq_tactics.tac_löb ?Δ "IH" ?Q ?e ?y" has type
"environments.envs_entails ?Δ ?Q" while it is expected to have type
"--------------------------------------∗
Φ k -∗ Φ (S k)
".
```
I don't know if it is even possible, but it would be nice to detect this error and emit a nicer message.https://gitlab.mpi-sws.org/iris/iris/-/issues/245Add IntoAnd instance (and more) for array2019-08-13T11:19:53ZRodolphe LepigreAdd IntoAnd instance (and more) for arrayWe should add `IntoAnd` instances (and friends) for `array`.
This has been discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/267#note_37037).We should add `IntoAnd` instances (and friends) for `array`.
This has been discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/267#note_37037).Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/259Confusing error message from iLoeb: `Variable x should be bound to a term but...2019-08-13T11:07:52ZDan FruminConfusing error message from iLoeb: `Variable x should be bound to a term but is bound to a ident.`Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : sbi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH" forall (k1).
```
(notice that `k1` should be `k` in the `forall` clause)
It fa...Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : sbi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH" forall (k1).
```
(notice that `k1` should be `k` in the `forall` clause)
It fails with a cryptic message:
```
Error:
In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
"iLöbRevert (constr) with (tactic3)", "iRevertIntros (constr) with (tactic3)",
"go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)",
"go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
"tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
"iRevertIntros ( (ident) ) (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )), "iRevert ( (ident) )",
"iForallRevert (ident)" and "x" (with IH:="IH", Hs:=""), last term evaluation
failed.
Variable x should be bound to a term but is bound to a ident.
```
What's bit strange is that the identifier `x` is not used in the code.https://gitlab.mpi-sws.org/iris/iris/-/issues/248Comparison with `=` and with CAS is not the same2019-07-01T14:46:59ZRalf Jungjung@mpi-sws.orgComparison with `=` and with CAS is not the sameCurrently, `heap_lang` allows more things to be compared with `=` than with `CAS`: for the latter, one of the two values-to-be-compared has to be "unboxed", meaning that it is a literal or inl/inr of a literal. If this condition is not m...Currently, `heap_lang` allows more things to be compared with `=` than with `CAS`: for the latter, one of the two values-to-be-compared has to be "unboxed", meaning that it is a literal or inl/inr of a literal. If this condition is not met, the program is stuck.
@robbertkrebbers proposes that we should restrict `=` in a similar way. On the other hand, it is nice that `=` is a total operation currently.https://gitlab.mpi-sws.org/iris/iris/-/issues/250equivI lemma for sigT2019-06-25T10:41:37ZPaolo G. GiarrussoequivI lemma for sigTTo use the new `sigT` construction, it helps to have an `equivI` lemma such as:
```coq
Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
x ≡ y ⊣⊢
∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y : iProp Σ.
...To use the new `sigT` construction, it helps to have an `equivI` lemma such as:
```coq
Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
x ≡ y ⊣⊢
∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y : iProp Σ.
Proof. by unseal. Qed.
```
@robbertkrebbers asks: should we have this just for iProp, or for any `sbi`?https://gitlab.mpi-sws.org/iris/iris/-/issues/118Notation `A -c> B` makes no sense2019-06-18T17:44:46ZRobbert KrebbersNotation `A -c> B` makes no senseThe `c` goes back to the time we solely used COFEs, now that we use OFEs, this notation makes no sense whatsoever.The `c` goes back to the time we solely used COFEs, now that we use OFEs, this notation makes no sense whatsoever.Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/52iMod and evar instantiation2019-06-17T07:54:22ZRalf Jungjung@mpi-sws.orgiMod and evar instantiationSee <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391>: `iMod ... as [$ ?]` fails even though `iMod ... as [H ?]; iFrame "H"` works fine.
@jjourdan suggests it may be related to C...See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391>: `iMod ... as [$ ?]` fails even though `iMod ... as [H ?]; iFrame "H"` works fine.
@jjourdan suggests it may be related to Coq lazily propagating instantiated evars, and adding a magic tactic that does the propagation in the right point of executing the `iMod` could help.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/246iEval (eauto) "corrupts" goal2019-06-15T11:43:47ZPaolo G. GiarrussoiEval (eauto) "corrupts" goalWhile I ran into !269, I also ended up learning that `iEval (eauto)` can "corrupt" the goal by calling `iStartProof` again:
```
1 subgoal
Σ : gFunctors
H : heapG Σ
c1, c2 : val
A1, A2, B1, B2 : lty Σ
v1, v2 : val
w2, w1 : ...While I ran into !269, I also ended up learning that `iEval (eauto)` can "corrupt" the goal by calling `iStartProof` again:
```
1 subgoal
Σ : gFunctors
H : heapG Σ
c1, c2 : val
A1, A2, B1, B2 : lty Σ
v1, v2 : val
w2, w1 : language.val heap_lang
============================
"HwB2" : B2 w2
"HwB1" : B1 w1
--------------------------------------∗
⌜--------------------------------------∗
(B1 * B2)%lty (w1, w2)%V
⌝
```
(from https://gitlab.mpi-sws.org/Blaisorblade/examples/commit/e9851f6#16adf89a84c96614a153a2ca8db8a92215d85db3_244_297).
Minimized version:
```
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
Lemma foo {Σ}: True ⊢ True : iProp Σ.
Proof.
iIntros.
iEval (info_eauto).
Show.
(*Equal to: *)
(* iEval (iStartProof; iPureIntro). *)
```
gives:
```
1 subgoal
Σ : gFunctors
a : True
============================
--------------------------------------∗
⌜?P⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/221Coqdocs should link to std++ coqdocs2019-06-06T11:39:37ZRalf Jungjung@mpi-sws.orgCoqdocs should link to std++ coqdocsWhen using std++ types, like in https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.gmap.html, we should make them link to the std++ docs. I think this involves setting the `--external` flag correctly.When using std++ types, like in https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.gmap.html, we should make them link to the std++ docs. I think this involves setting the `--external` flag correctly.Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/42Authoritative with fraction2019-06-06T11:07:12ZRalf Jungjung@mpi-sws.orgAuthoritative with fractionThe authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to...The authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to be brought together to change it. I just realized that this could be supported by a fairly small change in the authoritative CMRA, namely to replace `Ex(M)` by `Frac * Ag(M)`:
```
Auth(M) := { (x, a) \in (Frac * Ag(M))^? * M | ...}
```
The interface would then change to allow a fraction in the `●` notation (and once we have an infrastructure for "assertions that can be split at a fraction", it could be registered there). What do you think?
Cc @janno @robbertkrebbers @jjourdanRobbert KrebbersRobbert Krebbers