Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-09-10T17:45:28Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/342Missing {u,}rFunctors and conversions2020-09-10T17:45:28ZPaolo G. GiarrussoMissing {u,}rFunctors and conversionsSome missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable throu...Some missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable through the above conversion, and @jung suggests that's an oversight; OTOH, that alerted me to a bug; I only needed it because I tried writing `GFunctor (gmapRF ...)`, which does not seem useful
- `listRF` does not exist (which I noticed while grepping)https://gitlab.mpi-sws.org/iris/iris/-/issues/341Coecisting fractional and persistent read-only ownership2020-08-25T09:34:48ZRalf Jungjung@mpi-sws.orgCoecisting fractional and persistent read-only ownershipAs part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Ri...As part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Right now, our encoding through `frac * agree T + agree T` (or equivalently `(frac + ()) * agree T`) requires ownership of the full fraction for that move.
I think such a construction is possible, but it requires https://gitlab.mpi-sws.org/iris/iris/-/issues/257. Then we could relate an authoritative map to a fragment that's more like `option (frac * agree T) * option (agree T)`, and ensure that the second `option` is `None` unless the sum of all fraction fragments is less than 1.https://gitlab.mpi-sws.org/iris/iris/-/issues/340Polymorphic equality for HeapLang2020-08-22T19:06:03ZDan FruminPolymorphic equality for HeapLangIt would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.It would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.https://gitlab.mpi-sws.org/iris/iris/-/issues/339Add "reservation map" CMRA2020-09-09T12:29:51ZRalf Jungjung@mpi-sws.orgAdd "reservation map" CMRAFor the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an i...For the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?https://gitlab.mpi-sws.org/iris/iris/-/issues/338Missing unseal tactic for siProp2020-08-30T07:04:36ZPaolo G. GiarrussoMissing unseal tactic for siProp
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_...
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl.
(* Should be siProp.unseal. *)
Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.
```
The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.https://gitlab.mpi-sws.org/iris/iris/-/issues/337Weird automatically generated names2020-08-12T16:46:47ZRobbert KrebbersWeird automatically generated namesAfter @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatic...After @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatically generated hypothesis `x`.
```
1 subgoal
PROP : bi
x : True
______________________________________(1/1)
_ : ⌜0 = 0⌝
--------------------------------------□
True
```
I don't understand where the name `x` comes from, but it's very annoying. The `∃ _ : ..., ...` pattern is often used for `inG`, and the `inG` being called `x` is very annoying. It prevents one from using `x` for other variables.
Obviously, in this case I could use `iDestruct foo as (name_for_my_inG) "?"`, but I really don't want to name that hypothesis.https://gitlab.mpi-sws.org/iris/iris/-/issues/336Use user-supplied names in iIntros (?)2020-08-12T16:46:47ZTej Chajedtchajed@gmail.comUse user-supplied names in iIntros (?)Similar to !479, the proof mode should preserve user names in binders in `iIntros (?)`.
This depends on !479 since there's some common infrastructure for representing and threading identifiers through typeclasses.Similar to !479, the proof mode should preserve user names in binders in `iIntros (?)`.
This depends on !479 since there's some common infrastructure for representing and threading identifiers through typeclasses.https://gitlab.mpi-sws.org/iris/iris/-/issues/335iris.sty incompatible with acmart2020-07-15T12:25:40ZRalf Jungjung@mpi-sws.orgiris.sty incompatible with acmartThe `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the ...The `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the existing `\nequiv` is, or else change the name of our macro.https://gitlab.mpi-sws.org/iris/iris/-/issues/334Expand test coverage of proofmode2021-12-16T22:21:12ZTej Chajedtchajed@gmail.comExpand test coverage of proofmodeThe proof mode tests don't cover the following:
- [x] `iRename`
- [x] `iTypeOf`
- [x] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris...The proof mode tests don't cover the following:
- [x] `iRename`
- [x] `iTypeOf`
- [x] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris-coq/-/tree/bytes-ident) branch.https://gitlab.mpi-sws.org/iris/iris/-/issues/331simpl breaks error checking of `iNext (S i)`2020-07-14T08:21:09ZPaolo G. Giarrussosimpl breaks error checking of `iNext (S i)`I'd expect `iNext (S i)` to introduce exactly `S i` later, and fail otherwise. However, after e.g. `simpl` turns `▷^(S i) P` into `▷ ▷^i P`, that will sometimes introduce _one_ later, as shown below.
```coq
From iris.proofmode Require I...I'd expect `iNext (S i)` to introduce exactly `S i` later, and fail otherwise. However, after e.g. `simpl` turns `▷^(S i) P` into `▷ ▷^i P`, that will sometimes introduce _one_ later, as shown below.
```coq
From iris.proofmode Require Import tactics.
Lemma foo i {PROP} P : P ⊢@{PROP} ▷^(S i) P.
Proof.
iIntros "H".
Fail iNext 2.
iNext (S i).
Fail iNext i.
Fail iNext.
iExact "H".
Restart.
iIntros "H /=".
Fail iNext 2.
iNext (S i).
iNext i. (* !!! *)
Abort.
```
### Iris version
```
$ opam show coq-iris -f version
dev.2020-05-24.2.af5e50e7
```
with Coq 8.11.1.https://gitlab.mpi-sws.org/iris/iris/-/issues/330Consider adding `iEnough` variants of `iAssert` ?2020-06-26T07:35:15ZPaolo G. GiarrussoConsider adding `iEnough` variants of `iAssert` ?Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first ...Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first last.
```
The point is just readability, and adding all the overloads is probably not worth it, but maybe this would change with an Ltac2 proofmode?https://gitlab.mpi-sws.org/iris/iris/-/issues/328Add RA for auth of a heap2020-10-12T15:45:22ZRalf Jungjung@mpi-sws.orgAdd RA for auth of a heap`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in I...`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in Iris. ;)
The only open question for me is, what is `Y`? (`X` is any countable type.)
* We probably should have fractions, so that would be `Y := frac * agree T`. Even if you don't need fractions, just making it always "1" should not be hard to use (we should just make sure to have a lemma that from owning the "1" fraction twice, derives `False`).
* @tchajed mentioned they also need something with agreement in a few places. So we could either also have a version with `Y := agree T`, or we could do the strictly more powerful thing (subsuming both of the above) and do `Y := (frac * agree T) + agree T`. I *think* with the right surface-level definitions, this is actually not harder to use than either of the two more specialized heaps.https://gitlab.mpi-sws.org/iris/iris/-/issues/325iSpecialize with "[% //]" does not report an error if done fails2020-06-26T10:51:38ZTej Chajedtchajed@gmail.comiSpecialize with "[% //]" does not report an error if done failsiSpecialize on `SPureGoal true` does not report an error message.
```coq
From iris Require Import proofmode.tactics.
Theorem test {PROP: bi} (P: PROP) :
(⌜False⌝ -∗ P) -∗
P.
Proof.
iIntros "Hwand".
iSpecializePat_go "Hwand" [sp...iSpecialize on `SPureGoal true` does not report an error message.
```coq
From iris Require Import proofmode.tactics.
Theorem test {PROP: bi} (P: PROP) :
(⌜False⌝ -∗ P) -∗
P.
Proof.
iIntros "Hwand".
iSpecializePat_go "Hwand" [spec_patterns.SPureGoal true] (* with "[% //]" *).
Abort.
```
The reason is that this match is failing: https://gitlab.mpi-sws.org/iris/iris/-/blob/11f9d567c2a8b1f52d00e562d5cc39262463cf9e/theories/proofmode/ltac_tactics.v#L849. It should have another case that prints the normal Coq goal rather than the IPM goal.https://gitlab.mpi-sws.org/iris/iris/-/issues/324Add "nat+min" RA2020-06-18T11:20:17ZRalf Jungjung@mpi-sws.orgAdd "nat+min" RAWe have an RA `mnat` for `nat` with "max" as composition. But we don't have one with "min". It would probably make sense to add that.
But how should we name things? `mnat` isn't great as `m` could be min or max...We have an RA `mnat` for `nat` with "max" as composition. But we don't have one with "min". It would probably make sense to add that.
But how should we name things? `mnat` isn't great as `m` could be min or max...https://gitlab.mpi-sws.org/iris/iris/-/issues/322Operator precedence in heap lang is wrong2020-05-28T13:50:42ZDmitry KhalanskiyOperator precedence in heap lang is wrongThe Iris version is dev.2020-05-18.2.fdda97e8.
Given the definition
```
Definition v: expr := #true || #false = #false.
```
I expect it to read the same as in most other languages: "Either `true` is true or `false` is equal to `false`"....The Iris version is dev.2020-05-18.2.fdda97e8.
Given the definition
```
Definition v: expr := #true || #false = #false.
```
I expect it to read the same as in most other languages: "Either `true` is true or `false` is equal to `false`". However, `Print v` shows:
```
v = ((if: #true then #true else #false) = #false)%E
: expr
```
In other words, `||` has higher precedence than comparisons. I'm not familiar with how exactly notations in Coq are specified, but, looking at `notation.v`, it seems that precedence for common operators is not specified explicitly but is instead inherited from other notations that are known to Coq, and in vanilla Coq `=` has low precedence, given its role.https://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-10-20T09:21:24ZPaolo G. GiarrussoMake `contractive_proper` into a lemma, or control other instances that make it costly.Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://...Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?https://gitlab.mpi-sws.org/iris/iris/-/issues/320λne should use %I for body — or add a variant using `%I`.2020-07-14T08:20:05ZPaolo G. Giarrussoλne should use %I for body — or add a variant using `%I`.For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
...For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
```
Similarly, needing both `λne` and `%I` is annoying, what about:
```coq
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
```
I'd even consider placing that annotation in `λne` itself – `algebra.ofe` could import `bi.notation`; but many non-expansive functions aren't predicates :-).Paolo G. GiarrussoPaolo G. Giarrussohttps://gitlab.mpi-sws.org/iris/iris/-/issues/319Fix "omega is deprecated" warnings by switching to lia2020-05-16T17:14:49ZTej Chajedtchajed@gmail.comFix "omega is deprecated" warnings by switching to liaOn Coq v8.12+alpha there are a few new warnings from uses of `omega`, which should be replaced with `lia`. This might be a little annoying to make compatible with Coq v8.9, since `lia` has gotten progressively more powerful.On Coq v8.12+alpha there are a few new warnings from uses of `omega`, which should be replaced with `lia`. This might be a little annoying to make compatible with Coq v8.9, since `lia` has gotten progressively more powerful.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/316Explore use of `#[local]`/`Local` definitions2020-10-02T11:44:42ZRalf Jungjung@mpi-sws.orgExplore use of `#[local]`/`Local` definitionsI recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions...I recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.
As a random example for such definitions, [consider these](https://gitlab.mpi-sws.org/iris/iris/-/blob/701b533c8be530a69e605ee5443a089146d5701f/theories/base_logic/lib/gen_heap.v#L136-164).
`Local Definition` is supported in Coq 8.9 (and maybe older) so we can start using it any time.