Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-08-22T19:06:03Zhttps://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/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/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/295Have iApply introduce equalities for subterms that cannot be unified directly2020-08-08T21:57:49ZArmaël GuéneauHave iApply introduce equalities for subterms that cannot be unified directlyThe initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 ...The initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 = z⌝
```
without relying explicitly on the names `x4` and `z`.
I'm not sure what would be the most general form of such a tactic, or what its user interface would be, though. I think it would be nice to have it as an instance of `iApply`, if that's possible. (having it in `iFrame` as well is perhaps possible but risky, for instance in the case of mapsto it should at least be restricted to mapsto with the same syntactic location...).https://gitlab.mpi-sws.org/iris/iris/-/issues/333Iris Library Best Practices2020-08-06T16:37:12ZRalf Jungjung@mpi-sws.orgIris Library Best PracticesWe should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered for...We should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered form. Other aspects are not mentioned; @blaisorblade pointed out that it is non-obvious that specs should not contain `own` but instead wrap those things in their own definitions that depend on `libG` instead of `inG`.https://gitlab.mpi-sws.org/iris/iris/-/issues/315Port HeapLang tactics to more efficient style2020-07-15T19:27:00ZRobbert KrebbersPort HeapLang tactics to more efficient styleThe heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248The heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248https://gitlab.mpi-sws.org/iris/iris/-/issues/306Iris 3.3 release planning2020-07-15T16:05:09ZRalf Jungjung@mpi-sws.orgIris 3.3 release planningWhat needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed s...What needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed script in the CHANGELOG.
* [x] Release a matching std++.
* [x] Write announcement.
* [x] Release opam packages on coq opam registry.
* [x] Send out announcements.Iris 3.3https://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/296Use Coq deprecation attribute to implement deprecations2020-07-15T10:35:39ZTej Chajedtchajed@gmail.comUse Coq deprecation attribute to implement deprecationsNow that Iris only supports Coq 8.9+, we can use the [`#[deprecated]` attribute](https://coq.github.io/doc/master/refman/language/gallina-specification-language.html#coq:attr.deprecated) on any deprecated tactics or definitions. Deprecat...Now that Iris only supports Coq 8.9+, we can use the [`#[deprecated]` attribute](https://coq.github.io/doc/master/refman/language/gallina-specification-language.html#coq:attr.deprecated) on any deprecated tactics or definitions. Deprecation warnings are nice because they can be either suppressed with `-w -deprecated` or turned into an error with `-w +deprecated`.
This immediately applies to:
- `iAlways`
- `algebra/deprecated.v`'s `cofeT` and `dec_agree` (`dec_agree` may need to be wrapped in a notation first)
Iris also has a few dynamic deprecations that Coq currently doesn't support. The IPM can detect these but currently (due to Coq limitations) has no way to raise a user-level deprecation warning.
- The deprecated `!#` intro pattern is parsed as `TIntuitionisticIntro` but then treated the same as `TModalIntro`.
- The `*` specialization pattern is deprecated and triggers a deprecation message using `idtac`.Iris 3.3https://gitlab.mpi-sws.org/iris/iris/-/issues/309Fix name duplication `elem_of_list_singleton` in Iris and std++2020-07-15T09:36:22ZRobbert KrebbersFix name duplication `elem_of_list_singleton` in Iris and std++See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47923See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47923Iris 3.3https://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/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/163Dealing with nested modalities in `iModIntro`2020-06-29T10:38:08ZRobbert KrebbersDealing with nested modalities in `iModIntro`We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 →...We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
```
This instance allows introduction of e.g. updates below `monPred_at`.
When we add a `FromModal` instance for `monPred_at P i`, we end up with ambiguity when introducing `monPred_at (|==> P) i`: should `|==>` or `monPred_at` be introduced?
Concretely, we should:
- [ ] Add a `FromModal` instance for `monPred_at`
- [ ] Get the priorities of that instance and e.g. the above `from_modal_monPred_at` right
- [x] Do the same for `embed`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/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/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/298Guide typeclass search via more specialized typeclasses2020-06-17T16:51:55ZMichael SammlerGuide typeclass search via more specialized typeclassesFind places where a general typeclass (like `SetUnfold` before) can be split into more specialized typeclasses (like `SetUnfoldElemOf`) such that typeclass search is always guided by the head symbol. https://gitlab.mpi-sws.org/iris/stdpp...Find places where a general typeclass (like `SetUnfold` before) can be split into more specialized typeclasses (like `SetUnfoldElemOf`) such that typeclass search is always guided by the head symbol. https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/66 applied this optimization to `SetUnfold`.
cc @robbertkrebbershttps://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/313Add deallocation operation to HeapLang2020-05-25T16:01:10ZRalf Jungjung@mpi-sws.orgAdd deallocation operation to HeapLangIt would be great if HeapLang would also support deallocation, to enable reasoning about programs that perform explicit deallocation. To support the `meta` mechanism we have to ensure that locations never get reused but that seems fine -...It would be great if HeapLang would also support deallocation, to enable reasoning about programs that perform explicit deallocation. To support the `meta` mechanism we have to ensure that locations never get reused but that seems fine -- we do not have ptr-int-casts.
We *do* have ptr equality tests though. I am not sure if we are willing to demand that locations must not have been deallocated yet for them to be comparable -- that makes ptr equality a memory-dependent operation, which is quite the pain. Maybe it is okay to not be super realistic in this regard?https://gitlab.mpi-sws.org/iris/iris/-/issues/302Notation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` broken2020-05-24T12:55:45ZRobbert KrebbersNotation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` brokenSee https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/396#note_46604
Apparently https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/384 did break these notations...
Minimized example. The following works:
```coq
Notation "(⊢@{ P...See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/396#note_46604
Apparently https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/384 did break these notations...
Minimized example. The following works:
```coq
Notation "(⊢@{ PROP } )" := (eq (A:=PROP)) (only parsing).
Definition test PROP := (⊢@{PROP}).
```
But the following doesn't:
```coq
Notation "('⊢@{' PROP } )" := (eq (A:=PROP)) (only parsing).
Definition test PROP := (⊢@{PROP}).
(* Syntax Error: Lexer: Undefined token *)
```
/cc @Blaisorblade @gmalecha