Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-06-18T11:20:17Zhttps://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/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/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/314Argument to bi_pure should have argument at type_scope?2021-06-16T21:14:34ZGregory MalechaArgument to bi_pure should have argument at type_scope?The argument of `bi_pure` is marked as `stdpp` scope, which seems odd since it is a `Prop`? This works since all notations inside of stdpp have stdpp_scope, but it isn't nicely compatible with non stdpp notations.
If you already have a ...The argument of `bi_pure` is marked as `stdpp` scope, which seems odd since it is a `Prop`? This works since all notations inside of stdpp have stdpp_scope, but it isn't nicely compatible with non stdpp notations.
If you already have a `Open Scope stdpp_scope` in your file, you should already get access to notations in stdpp scope.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/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/310Choose syntax and implement destructuring existentials with pure components, ...2021-03-24T12:42:23ZPaolo G. GiarrussoChoose syntax and implement destructuring existentials with pure components, following !400It'd be nice to support something like `iDestruct "H" as "∃[%x HP]"` on `"H": ∃ x, P` (where the `∃[ipat ipat]` syntax is a strawman), mapping that introduction pattern to `iExistsDestruct`. The killer feature is support for nested exist...It'd be nice to support something like `iDestruct "H" as "∃[%x HP]"` on `"H": ∃ x, P` (where the `∃[ipat ipat]` syntax is a strawman), mapping that introduction pattern to `iExistsDestruct`. The killer feature is support for nested existentials, which require multiple iDestruct calls today.
In discussion on [!400](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/400#note_45911), I and @tchajed considered supporting that with pattern `[%x HP]`, but that pattern is already mapped to `iAndDestruct`, and unlike in Coq the two methods are very different.
Steps:
1. [ ] bikeshed a syntax
2. [ ] any other discussion on the specification, if needed
3. [ ] implement this.https://gitlab.mpi-sws.org/iris/iris/-/issues/307`iIntros "%"` no longer works with universal quantification2020-04-07T15:39:37ZRalf Jungjung@mpi-sws.org`iIntros "%"` no longer works with universal quantificationThis test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebber...This test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebbers @tchajedhttps://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 @gmalechahttps://gitlab.mpi-sws.org/iris/iris/-/issues/301`iExists` ignores `Opaque`2020-03-30T11:52:39ZPaolo G. Giarrusso`iExists` ignores `Opaque`Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Defi...Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Definition foo : iProp Σ := ∃ (x : nat), x ≡ 0.
End foo.
Opaque foo.
Lemma bar Σ : ⊢ foo Σ .
Proof.
by iExists 0. Restart.
iStartProof.
eapply coq_tactics.tac_exist.
Fail apply (class_instances_bi.from_exist_exist _).
(* The Hint Extern from !372: *)
notypeclasses refine (class_instances_bi.from_exist_exist _).
(* apply: (class_instances_bi.from_exist_exist _). (* Also works *) *)
by eexists 0.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/299`leibnizO` finds convoluted proof for definitions2020-03-12T21:15:28ZRobbert Krebbers`leibnizO` finds convoluted proof for definitions```coq
Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)
``````coq
Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/293Add `array_copy` function in HeapLang2020-02-25T14:20:49ZRobbert KrebbersAdd `array_copy` function in HeapLangThis would be pretty useful.This would be pretty useful.https://gitlab.mpi-sws.org/iris/iris/-/issues/288iExists fails if goal after the existential quantifier is an evar2020-12-10T12:07:25ZMichael SammleriExists fails if goal after the existential quantifier is an evarIris version: dev.2019-11-22.2.a979391c
`iExists` fails if you have a goal of the form
```
∃ _, ?P
```
Here is a test case which illustrates the problem:
```
Lemma test Σ:
(∃ P, ∃ (_ : True), P : iProp Σ)%I.
Proof.
iExists _.
(*...Iris version: dev.2019-11-22.2.a979391c
`iExists` fails if you have a goal of the form
```
∃ _, ?P
```
Here is a test case which illustrates the problem:
```
Lemma test Σ:
(∃ P, ∃ (_ : True), P : iProp Σ)%I.
Proof.
iExists _.
(* Here iExists fails *)
Fail iExists _.
(* Solving the existential quantifier manually *)
eapply coq_tactics.tac_exist.
(* Using apply fails *)
Fail apply @class_instances_bi.from_exist_exist.
(* But apply: works *)
apply: @class_instances_bi.from_exist_exist. simpl.
eexists _.
Abort.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/285Remove eta-expansions from sealed definitions2020-08-30T09:53:12ZRalf Jungjung@mpi-sws.orgRemove eta-expansions from sealed definitionsAs discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/352#note_42913), we plan to remove all eta-expansions from sealed definitions. That makes the unfolding `rewrite` more widely applicable.As discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/352#note_42913), we plan to remove all eta-expansions from sealed definitions. That makes the unfolding `rewrite` more widely applicable.https://gitlab.mpi-sws.org/iris/iris/-/issues/284fupd_proper is too weak2020-01-06T18:24:52ZAbhishek Anandfupd_proper is too weakhttps://gitlab.mpi-sws.org/iris/iris/blob/627984129ca88df5a6c89fca3b64cfa146d582c3/theories/bi/updates.v#L216
The type should be
```coq
Global Instance fupd_proper:
forall (PROP : sbi) (H : BiFUpd PROP),
Proper (equiv ==> equiv ==...https://gitlab.mpi-sws.org/iris/iris/blob/627984129ca88df5a6c89fca3b64cfa146d582c3/theories/bi/updates.v#L216
The type should be
```coq
Global Instance fupd_proper:
forall (PROP : sbi) (H : BiFUpd PROP),
Proper (equiv ==> equiv ==> equiv ==> equiv) (@fupd (sbi_car PROP) _).
Proof using.
Admitted.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/283big_sepM2_fmap and friends only work for nat keys2019-12-20T15:28:54ZMichael Sammlerbig_sepM2_fmap and friends only work for nat keysIris version: dev.2019-11-22.2.a979391c
`big_sepM2_fmap`, `big_sepM2_fmap_l` and `big_sepM2_fmap_r` only work for maps with `nat` keys, but I don't see a fundamental reason for this. The problem is that they use `(Φ : nat → A' → B' → PR...Iris version: dev.2019-11-22.2.a979391c
`big_sepM2_fmap`, `big_sepM2_fmap_l` and `big_sepM2_fmap_r` only work for maps with `nat` keys, but I don't see a fundamental reason for this. The problem is that they use `(Φ : nat → A' → B' → PROP)` instead of `(Φ : K → A' → B' → PROP)`. Let me know if I should open a PR which fixes this.https://gitlab.mpi-sws.org/iris/iris/-/issues/282Undesired simplification behaviour of big_sepM22020-02-05T19:04:27ZMichael SammlerUndesired simplification behaviour of big_sepM2Iris version: dev.2019-11-22.2.a979391c
`simpl` unfolds the definition of `big_sepM2` which makes it basically unusable.
Example:
```coq
From iris.program_logic Require Import weakestpre.
Example big_sepM2_simpl Σ (xs ys : gmap nat na...Iris version: dev.2019-11-22.2.a979391c
`simpl` unfolds the definition of `big_sepM2` which makes it basically unusable.
Example:
```coq
From iris.program_logic Require Import weakestpre.
Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => uPred_and ⌜∀ k : nat, is_Some (xs !! k) ↔ is_Some (ys !! k)⌝
([∗ map] xy ∈ map_zip xs ys, ⌜xy.1 = xy.2⌝%I) *)
```
I am currently using the following workaround (`big_sepM2` does not seem to have an `Arguments` command at the moment):
```coq
Arguments big_sepM2 {PROP K _ _ A B} _ !_ !_ /.
Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => ([∗ map] x;y ∈ xs;ys, ⌜x = y⌝)%I *)
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/281proof_mode.md documentation has a broken link2019-12-19T19:14:39ZJules Jacobsproof_mode.md documentation has a broken linkproofmode.md's link to the heaplang tactics file is broken.
Also, the example of iIntros seems to show deprecated !# instead of !>, and Hx instead of x.proofmode.md's link to the heaplang tactics file is broken.
Also, the example of iIntros seems to show deprecated !# instead of !>, and Hx instead of x.