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/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 Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/114Possibly confusing naming: auth_own_valid.2019-06-06T11:06:35ZDan FruminPossibly confusing naming: auth_own_valid.I was wondering if anyone else found this a bit confusing.
The lemma `auth_own_valid` refers to two things:
- `base_logic.lib.auth.auth_own_valid` which states that `own γ (◯ a) ⊢ ✓ a`;
- `algebra.auth.auth_own_valid` which (roughly) s...I was wondering if anyone else found this a bit confusing.
The lemma `auth_own_valid` refers to two things:
- `base_logic.lib.auth.auth_own_valid` which states that `own γ (◯ a) ⊢ ✓ a`;
- `algebra.auth.auth_own_valid` which (roughly) states that `✓ (● a, ◯ b) → ✓ b`.
If you need both of those modules, then the order in which you import them is quite significant.
I guess the issue is that `auth_own` refers both to the *proposition of owning* the fragment part of the Auth algebra and to the actual fragment part of the algebra.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/238Wish: iSimpl on multiple hypothesis2019-05-22T22:53:15ZDan FruminWish: iSimpl on multiple hypothesis**A wish**: it would be nice if we could run `iSimpl` on several hypothesis: `iSimpl in "H1 H2"`.**A wish**: it would be nice if we could run `iSimpl` on several hypothesis: `iSimpl in "H1 H2"`.https://gitlab.mpi-sws.org/iris/iris/-/issues/232Investigate slowdown caused by gset change2019-04-24T08:26:43ZRalf Jungjung@mpi-sws.orgInvestigate slowdown caused by gset change[This std++ diff](https://gitlab.mpi-sws.org/iris/stdpp/compare/b938e033...e2eb2948) caused an [80% slowdown in `algebra/gset.v`](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558727491&to=1552560733442&var-metric=...[This std++ diff](https://gitlab.mpi-sws.org/iris/stdpp/compare/b938e033...e2eb2948) caused an [80% slowdown in `algebra/gset.v`](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558727491&to=1552560733442&var-metric=instructions&var-project=iris&var-branch=master&var-config=coq-8.9.0&var-group=(.*)). We should find a way to fix that regression, or at least understand what causes it.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/233Can't install on Coq 8.8.12019-03-20T08:40:16ZMaximilian WuttkeCan't install on Coq 8.8.1Hi,
I want to try out Iris, but `opam install coq-iris` yields this this:
```
#=== ERROR while compiling coq-iris.dev.2019-03-14.3.2d1c8352 ================#
# context 2.0.0~beta5 | linux/x86_64 | coq.8.8.1 | git+https://gitlab.mp...Hi,
I want to try out Iris, but `opam install coq-iris` yields this this:
```
#=== ERROR while compiling coq-iris.dev.2019-03-14.3.2d1c8352 ================#
# context 2.0.0~beta5 | linux/x86_64 | coq.8.8.1 | git+https://gitlab.mpi-sws.org/iris/opam.git
# path ~/.opam/coq88/.opam-switch/build/coq-iris.dev.2019-03-14.3.2d1c8352
# command /usr/bin/make -j7
# exit-code 2
# env-file ~/.opam/log/coq-iris-30223-f0f09f.env
# output-file ~/.opam/log/coq-iris-30223-f0f09f.out
### output ###
# [...]
# -Closed under the global context
# +Axioms:
# +iProp_unfold : ∀ Σ : gFunctors, iProp Σ -n> iPreProp Σ
# +iProp_fold_unfold : ∀ (Σ : gFunctors) (P : iProp Σ),
# +iProp_fold (iProp_unfold P) ≡ P
# +iProp_fold : ∀ Σ : gFunctors, iPreProp Σ -n> iProp Σ
# +iPreProp : gFunctors → ofeT
# make[2]: *** [Makefile.coq.local:20: tests/one_shot.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# make[1]: *** [Makefile.coq:318: all] Error 2
# make[1]: Leaving directory '/home/maxi/.opam/coq88/.opam-switch/build/coq-iris.dev.2019-03-14.3.2d1c8352'
# make: *** [Makefile:6: all] Error 2
```
However, these definitions like `iProp_unfold` etc are not axioms (are they?). Is this a known bug of Coq `8.8.1`?
I will try out the newest Coq version, but compilation takes some time...https://gitlab.mpi-sws.org/iris/iris/-/issues/207Rule "Res-Alloc" in documentation is stronger than the Coq version2019-03-06T09:54:29ZJoseph TassarottiRule "Res-Alloc" in documentation is stronger than the Coq versionIn the rule "Res-alloc" on page 26 of the documentation (see https://plv.mpi-sws.org/iris/appendix-3.1.pdf, or https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/ghost-state.tex#L211) the set for the new ghost name is allowed to be ...In the rule "Res-alloc" on page 26 of the documentation (see https://plv.mpi-sws.org/iris/appendix-3.1.pdf, or https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/ghost-state.tex#L211) the set for the new ghost name is allowed to be an arbitrary infinite set.
However, what's proved here (https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/base_logic/lib/own.v#L116) in the Coq code is a little bit weaker -- you only get that the new name must be in the complement of a finite set.
The stronger rule should be true though. As @robbertkrebbers points out, basically one first needs to port something like `gset_disj_alloc_updateP_strong` to `gmap`, and then the stronger result follows.https://gitlab.mpi-sws.org/iris/iris/-/issues/230"Generalizable All Variables" considered harmful2019-02-27T11:21:27ZRalf Jungjung@mpi-sws.org"Generalizable All Variables" considered harmfulOver the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and ...Over the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and then consider the following preamble:
```
Section something_about_sprop.
Conext `{authG Σ (exR spropC)}.
```
Can you spot what's wrong with this? Well, we just assumed that SProp is discrete, which it is not. Ouch.
From my experiments, we can avoid over-eager generalization by adding a `!`. I have not found conclusive documentation for `!`, but it seems the least we should do is (a) add `!` basically everywhere, and (b) treat the *absence* of `!` as a big fat warning bell during code review. The latter will be hard.
But really, while `Generalizable All Variables` is very useful for some things (like the general fin map libraries in std++), I think for most code the benefits are slim. I have [ported a few files](https://gitlab.mpi-sws.org/iris/iris/commit/f5bceb45532b5c9dff9124589b93eccee722be8f) to `Generalizable No Variables`, and the additional declarations required are negligible IMO. So I think what we should aim for (but that might take a while) is for std++ to no longer set `Generalizable All Variables` (to avoid inflicting this subtle issue onto unsuspecting users), and to locally set that flag in the (few) files that really benefit.
Or maybe I am overreacting, and things are not that bad. But the thought of accidentally assuming things I don't want to assume makes me nervous. What do you think?