Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-08-13T16:01:57Zhttps://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/253Constructing CMRAs by giving isomorphism to CMRAs2020-11-06T14:41:47ZPaolo G. GiarrussoConstructing CMRAs by giving isomorphism to CMRAsIris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).Iris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).https://gitlab.mpi-sws.org/iris/iris/-/issues/86CoPset finite decomposition into singletons2017-05-19T15:20:29ZHai DangCoPset finite decomposition into singletonsI'm working with a proof that requires unlimited tokens, which leads me to use the disjoint union `CoPset` cmra.
In a specific subproof I need to split a finite set `X : gset positive` of tokens into singletons:
`own γ (CoPset $ of_gs...I'm working with a proof that requires unlimited tokens, which leads me to use the disjoint union `CoPset` cmra.
In a specific subproof I need to split a finite set `X : gset positive` of tokens into singletons:
`own γ (CoPset $ of_gset X) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]}) `
With `big_opS_commute1` I can get
`own γ ([⋅ set] i ∈ X, CoPset $ of_gset {[i]}) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]})`
And then I only need to show that
`CoPset $ of_gset X ≡ [⋅ set] i ∈ X, CoPset $ of_gset {[i]}`,
which currently there seems to be no easy way to solve.
Is there an induction principle for gset's, or any way to solve this?https://gitlab.mpi-sws.org/iris/iris/-/issues/34Coq induction support in proof mode2016-09-30T10:31:09ZJacques-Henri JourdanCoq induction support in proof modeThere is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.There is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/194coq-speed: Measure using performance counters2018-06-22T22:02:37ZRalf Jungjung@mpi-sws.orgcoq-speed: Measure using performance counters@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?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/351Decouple framing and IntoSep2022-01-17T02:16:40ZRalf Jungjung@mpi-sws.orgDecouple framing and IntoSepCurrently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disab...Currently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disabled some `IntoSep` instances in Perennial for this reason.
It might make sense to have a separate IntoSep for framing that is more optimized for performance and, for example, does not try to exploit fractional things.
This is somewhat similar to https://gitlab.mpi-sws.org/iris/iris/-/issues/186.
To avoid making a mess, probably we should figure out https://gitlab.mpi-sws.org/iris/iris/-/issues/139 first.https://gitlab.mpi-sws.org/iris/iris/-/issues/10Defining RAs with a partial composition operation2016-01-18T16:38:58ZRalf Jungjung@mpi-sws.orgDefining RAs with a partial composition operationRight now, if your RA has a partial composition operation and you'd like to make a case distinction on something that's not decidable, you have to use some rather hideous trick. For example, in the case of STSs, composition is defined on...Right now, if your RA has a partial composition operation and you'd like to make a case distinction on something that's not decidable, you have to use some rather hideous trick. For example, in the case of STSs, composition is defined only if the intersection of the state sets is non-empty. To define this in Coq, the STS monoid actually carries around a `valid: Prop` piece of "data", and equality of monoid elements is defined as a quotient, equalizing all invalid elements. @robbertkrebbers convinced me this also comes up for some other monoid, I believe it was the fractions - but actually, I can't tell any more why this should come up there. Robbert, could you remind me?
It may be a good idea to axiomatize a class of "DRAs" (disjoint RAs), that have, instead of a validity predicate, a binary *disjointness* predicate. Composition would still have to be total, but commutativity (and potentially associativity) would only have to hold if the involved elements are disjoint. We could then have a functor from RAs to DRAs, using above construction with the `valid: Prop` and the quotient. This way, people could define such monoids much easier, but we wouldn't have to suffer the pain of using DRAs in the model. (Which would be really annoying; every time we use commutativity, we'd have to prove disjointness.)https://gitlab.mpi-sws.org/iris/iris/-/issues/387Deprecate unqualified "Instance"2020-12-19T17:43:58ZRalf Jungjung@mpi-sws.orgDeprecate unqualified "Instance"With https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/594 (and potentially some follow-up changes), all `Hint` in Iris will be qualified with `Local` or `Global`. I think we should do the same with `Instance`.
@tchajed is there a w...With https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/594 (and potentially some follow-up changes), all `Hint` in Iris will be qualified with `Local` or `Global`. I think we should do the same with `Instance`.
@tchajed is there a way to adjust your script to do that, or will we have to ask the Coq devs for an (opt-in) deprecation warning for `Instance` first, similar to the `Hint` warning that your script is based on?https://gitlab.mpi-sws.org/iris/iris/-/issues/64Destruct patterns: Support -> and <- (at least) for pure Coq equalities, and ...2017-10-27T13:17:57ZRalf Jungjung@mpi-sws.orgDestruct patterns: Support -> and <- (at least) for pure Coq equalities, and maybe injection patternsIn lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; i...In lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %[= ->]`, i.e., there is an additional injection applied. Any way we could also get that in the proof mode? Maybe even using the "injective" typeclass so that it doesn't have to be the constructor of an inductive type (however, of course it'd also have to support all constructors, so it can't rely just on that typeclass).Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/92Discussion: Better(?) Logically-Atomic Triples2018-07-13T15:54:13ZJannoDiscussion: Better(?) Logically-Atomic TriplesHey everyone,
I am doing some groundwork on logical atomicity for weak memory and I got annoyed by the "current" definition of atomic triples:
1. The quantification over the "real" precondition P seems unnecessary.
2. The box around the...Hey everyone,
I am doing some groundwork on logical atomicity for weak memory and I got annoyed by the "current" definition of atomic triples:
1. The quantification over the "real" precondition P seems unnecessary.
2. The box around the shift is an artifact of working directly with (persistent) triples.
This is the reference definition of atomic triple (taken from @zhangz's iris-atomic@13900169bafb6b6ef1d091236dba493eaa25cc95):
```coq
∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
α x ∗
((α x ={Ei, Eo}=∗ P) ∧
(∀ v, β x v ={Ei, Eo}=∗ Q v))
) -∗ {{ P }} e @ ⊤ {{ Q }}.
```
I propose the following change:
```coq
atomic_shift Eo Ei α β Φ :=
|={Eo,Ei}=> ∃ x : A,
α x ∗
((α x ={Ei,Eo}=∗ ▷ atomic_shift Eo Ei α β Φ) ∧
∀ y, β x y ={Ei,Eo}=∗ Φ y).
atomic_wp Eo Ei α β := ∀ Φ, atomic_shift Eo Ei α β Φ -∗ WP e @ Eo { Φ }
```
It should be easy enough to derive a notion of logically-atomic triples (as opposed to weakestpre) the same way we derive normal triples.
I did some initial testing by porting iris-atomic/atomic_incr.v to this definition. Apart from some inconveniences regarding boxes in the client (orthogonal to logically-atomic triples; just a proof setup problem), the proof of the spec and the client remain mostly the same. One additional (albeit entirely trivial) Löb induction had to be introduced in the client to prove the atomic shift. The spec proof already had a Löb induction and so will almost any other proof of that kind I think.
You can see the changes to the proof here: janno/iris-atomic@06d9dc7d. The definition is here: janno/iris-atomic@ba66f8bd.
Before I continue to work with this new definition in my own development I would like to gather feedback. What does everyone think of it?
I am specifically worried about examples that somehow manage to run out of steps and thus cannot get rid of the `▷` modality. I can't imagine what those would look like but they might exist. Additionally, the added complexity of requiring `iLöb` in client proofs may be considered a substantial disadvantage of this definition by some.
P.S.: This is orthogonal to (and thus hopefully compatible with) the work on using telescopes to represent an arbitrary number of binders in atomic triples. I made some progress on that, too. But it's not done.https://gitlab.mpi-sws.org/iris/iris/-/issues/113Do not run `simpl` on user-visible goals2017-12-02T00:07:12ZRalf Jungjung@mpi-sws.orgDo not run `simpl` on user-visible goalsThe proof mode, and in particular the `wp_*` tactics, currently sometimes run `simpl` on the user's goal. That can be annoying if `simpl` misbehaves. Ideally, we should avoid running `simpl` on user goals.The proof mode, and in particular the `wp_*` tactics, currently sometimes run `simpl` on the user's goal. That can be annoying if `simpl` misbehaves. Ideally, we should avoid running `simpl` on user goals.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/28docs: the universe $\cal U$ is used without definition2016-08-16T17:40:06ZJeehoon Kangjeehoon.kang@kaist.ac.krdocs: the universe $\cal U$ is used without definitionHere: https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/model.tex#L155
Without saying that $\cal U$ is the universe (in whatever sense), the sentence seems confusing to me..Here: https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/model.tex#L155
Without saying that $\cal U$ is the universe (in whatever sense), the sentence seems confusing to me..https://gitlab.mpi-sws.org/iris/iris/-/issues/192Document `iRewrite -...` in `ProofMode.md`2019-01-11T10:13:31ZDan FruminDocument `iRewrite -...` in `ProofMode.md`I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```https://gitlab.mpi-sws.org/iris/iris/-/issues/131Document heap-lang `wp_` tactics2019-02-18T12:39:37ZRobbert KrebbersDocument heap-lang `wp_` tacticsRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/311Document side-effects of importing Iris2020-09-29T16:33:55ZRalf Jungjung@mpi-sws.orgDocument side-effects of importing IrisIris should have something [like std++ has](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects) where we document its global, Coq-level side-effects.Iris should have something [like std++ has](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects) where we document its global, Coq-level side-effects.https://gitlab.mpi-sws.org/iris/iris/-/issues/133Document unicode input method in README2018-12-19T16:20:38ZRobbert KrebbersDocument unicode input method in README* [x] @jung do it for emacs
* [x] @robbertkrebbers do it for CoqIDE* [x] @jung do it for emacs
* [x] @robbertkrebbers do it for CoqIDERobbert KrebbersRobbert Krebbershttps://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/318Drop support for Coq 8.9?2020-08-24T08:47:06ZRalf Jungjung@mpi-sws.orgDrop support for Coq 8.9?Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`...Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`)
* `change_no_check` (to stop using deprecated `convert_concl_no_check`)
* `Declare Scope` (to fix deprecated use of undeclared scopes)
Is there more?https://gitlab.mpi-sws.org/iris/iris/-/issues/388Dropping support for Coq 8.102020-12-16T12:17:28ZTej Chajedtchajed@mit.eduDropping support for Coq 8.10At some point we should drop support for Coq 8.10.
The benefits are:
- Ltac2 is available starting with Coq 8.11. This would let us integrate https://gitlab.mpi-sws.org/iris/string-ident into Iris and support the `"%H"` intro pattern wi...At some point we should drop support for Coq 8.10.
The benefits are:
- Ltac2 is available starting with Coq 8.11. This would let us integrate https://gitlab.mpi-sws.org/iris/string-ident into Iris and support the `"%H"` intro pattern without any additional work from the user.
- Custom entries [had some bugs](https://github.com/coq/coq/pull/11530) that seem to block their use in !554; in Coq 8.11 and forward we can give good notation for dfracs.
We should probably release Iris 3.4 before dropping support. Before that out of the current MRs I think !572 is the most important, to avoid releasing the mnat library and then immediately renaming it.