Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-04-07T15:39:37Zhttps://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.https://gitlab.mpi-sws.org/iris/iris/-/issues/279Editor bindings for Emacs and m17n are inconsistent2020-02-11T08:40:22ZTej Chajedtchajed@mit.eduEditor bindings for Emacs and m17n are inconsistentThe list of bindings for Emacs in [editor.md](docs/editor.md) is missing a bunch of useful bindings for superscripts/subscripts and a rule for ö (for typing Löb) that are in the config for m17n. We should make both lists consistent by ta...The list of bindings for Emacs in [editor.md](docs/editor.md) is missing a bunch of useful bindings for superscripts/subscripts and a rule for ö (for typing Löb) that are in the config for m17n. We should make both lists consistent by taking the union of the bindings.https://gitlab.mpi-sws.org/iris/iris/-/issues/274Regression after !329 on recursive proofs2019-12-02T14:10:16ZPaolo G. GiarrussoRegression after !329 on recursive proofsHere's a self-contained testcase:
```coq
From iris.proofmode Require Import tactics.
Section testcase.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Fixpoint test_fixpoint (n : nat) {struct n} : emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
...Here's a self-contained testcase:
```coq
From iris.proofmode Require Import tactics.
Section testcase.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Fixpoint test_fixpoint (n : nat) {struct n} : emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
Proof.
case: n => [|n] /=.
- iIntros "_ !%". reflexivity.
- iIntros "_".
(* Works *)
(* by iDestruct (test_fixpoint n with "[//]") as %->. *)
(* Fails *)
by iDestruct (test_fixpoint with "[//]") as %->.
Qed.
```
This testcase is silly, but recursive proofs for mutually recursive lemmas can make sense, especially when the proof uses a custom induction scheme that is only used once: proving it by hand has advantages, especially for automation, but can create more boilerplate than a recursive proof.
I tried out a suggestion from @robbertkrebbers, got it to work and will send a MR shortly, but I expect the result should be achieved otherwise.https://gitlab.mpi-sws.org/iris/iris/-/issues/270non-Unicode Iris notations2020-04-07T13:59:09ZRalf Jungjung@mpi-sws.orgnon-Unicode Iris notationsSome people askedd about a non-Unicode variant of our notation. @jihgfee @gmalecha have such a file I think, maybe we could contribute that upstream?Some people askedd about a non-Unicode variant of our notation. @jihgfee @gmalecha have such a file I think, maybe we could contribute that upstream?https://gitlab.mpi-sws.org/iris/iris/-/issues/269Editor config should explain how to configure CoqIDE 8.10 unicode input2020-02-10T15:44:56ZTej Chajedtchajed@mit.eduEditor config should explain how to configure CoqIDE 8.10 unicode inputCoqIDE 8.10 has a new feature for inputting unicode symbols with LaTeX-to-unicode conversion (triggered by typing shift-space). It's possible to configure the supported bindings (see https://coq.github.io/doc/master/refman/practical-tool...CoqIDE 8.10 has a new feature for inputting unicode symbols with LaTeX-to-unicode conversion (triggered by typing shift-space). It's possible to configure the supported bindings (see https://coq.github.io/doc/master/refman/practical-tools/coqide.html#coqide-unicode), so [editor.md](docs/editor.md) should give a configuration file with the Iris LaTeX bindings.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/263IPM/MoSeL nested disjunction syntax2019-11-01T13:02:01ZDan FruminIPM/MoSeL nested disjunction syntaxWould it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.Would it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.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/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.