Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-10-29T13:32:07Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/218Remove duplicate abstraction2018-10-29T13:32:07ZGhost UserRemove duplicate abstractionIn https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/proofmode/class_instances_bi.v#L13, with respect to the following three `Global Instance` declarations.
`PROP` is already abstracted as a section variable, and the extra gen...In https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/proofmode/class_instances_bi.v#L13, with respect to the following three `Global Instance` declarations.
`PROP` is already abstracted as a section variable, and the extra generality is not used.
Removing `{PROP : bi}` here is needed for compatibility with coq/coq#8820.https://gitlab.mpi-sws.org/iris/iris/-/issues/215Explore getting rid of implication2019-11-01T11:07:41ZRalf Jungjung@mpi-sws.orgExplore getting rid of implicationIt seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. ...It seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. We could remove implication from the MoSeL interface and see what happens.
For Iris itself I mostly expect this to work, but the general linear case might make this harder. Or not.https://gitlab.mpi-sws.org/iris/iris/-/issues/214Werid bug with `env_notations` and stdpp's `destruct_and!` tactic.2018-10-12T08:53:03ZDan FruminWerid bug with `env_notations` and stdpp's `destruct_and!` tactic.The following code snippet doesn't work, and `destruct_and!` fails:
```ocaml
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
Section test.
Variable A : Type.
Variable wf : A -> bool.
Lemma tes...The following code snippet doesn't work, and `destruct_and!` fails:
```ocaml
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
Section test.
Variable A : Type.
Variable wf : A -> bool.
Lemma test x y :
(wf x && wf y) → (wf y && wf x).
Proof.
intros.
destruct_and!.
Abort.
End test.
```
- If you remove the `env_notations` import than it works fine.
- If you place the `env_notations` import inside the proof script it also works.
- If you inline the `destruct_and?` tactic it also works.
(using coq 8.8.1, HEAD iris and coq-stdpp)https://gitlab.mpi-sws.org/iris/iris/-/issues/213Moving hypotheses from the intuitionistic to the spatial context2020-02-18T22:04:14ZRobbert KrebbersMoving hypotheses from the intuitionistic to the spatial contextRight now, there appears to be no decent way to move hypotheses from the intuitionistic context to the spatial context.
I thought this should never be needed, but I was proved wrong. As @jtassaro shows in (https://gitlab.mpi-sws.org/FP/...Right now, there appears to be no decent way to move hypotheses from the intuitionistic context to the spatial context.
I thought this should never be needed, but I was proved wrong. As @jtassaro shows in (https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/171/diffs#d026f8137ab7b7e373742e0df76ccf325011a5cf_53_89), this is sometimes needed before doing an induction.
I suppose we could make a tactic for this (and a corresponding introduction pattern like `-# pat`), but I'm not sure I like that very much. Also, in the case of a generic BI, there is probably the choice of having an `<affine>` modality or not.
As an alternative, if we believe this only ever occurs when doing induction, we could extend the syntax of the `forall` argument of `iInduction` to allow moving hypotheses from the intuitionistic to the spatial context.https://gitlab.mpi-sws.org/iris/iris/-/issues/211Masks are coPsets in the Coq development, not arbitrary subsets of natural nu...2020-03-18T15:29:30ZJoseph TassarottiMasks are coPsets in the Coq development, not arbitrary subsets of natural numbersThe appendix suggests that masks for updates and weakest preconditions may be arbitrary sets (it does not say so explicitly when defining fancy updates, but on p. 29 the camera used for "enabled" invariants is said to be P(N)). However, ...The appendix suggests that masks for updates and weakest preconditions may be arbitrary sets (it does not say so explicitly when defining fancy updates, but on p. 29 the camera used for "enabled" invariants is said to be P(N)). However, in the Coq code, the representation used for masks is `coPset`. @robbertkrebbers says that `coPsets` are used so that the representation has extensional equality, but that in principle the constructions all could work with arbitrary sets.
It seems like either the discussion in the appendix should be changed to `coPset` as well (in order to stick to the claim that everything is verified), or an explanatory note should be given. Unfortunately, it is not so easy to concisely describe `coPsets`: they contain all finite and cofinite sets, and are closed under various set operations. However, as @jung points out, the namespace "suffix" construction is not so clearly derivable just from the closure properties.https://gitlab.mpi-sws.org/iris/iris/-/issues/209Iris 3.1.0 is compatible with Coq 8.8.1 and coq-mathcomp-ssreflect 1.7.02018-08-29T10:49:18ZJannoIris 3.1.0 is compatible with Coq 8.8.1 and coq-mathcomp-ssreflect 1.7.0The `opam` file currently claims otherwise because these versions of Coq and ssreflect didn't exist when it was written. The only changes necessary are to adapt the `opam` entries for these two packages by increasing their respective upp...The `opam` file currently claims otherwise because these versions of Coq and ssreflect didn't exist when it was written. The only changes necessary are to adapt the `opam` entries for these two packages by increasing their respective upper bound's minor version by 1. I have tested this locally and have not encountered any issues.https://gitlab.mpi-sws.org/iris/iris/-/issues/208Import Coq.Strings.Ascii before using ascii notations2018-08-24T16:40:02ZGhost UserImport Coq.Strings.Ascii before using ascii notationsI don't know how to fork a repo on gitlab (the button is grayed out), and I don't know how to make a merge request here from a branch on github, so I'm creating an issue instead for merging https://github.com/JasonGross/iris-coq/commit/5...I don't know how to fork a repo on gitlab (the button is grayed out), and I don't know how to make a merge request here from a branch on github, so I'm creating an issue instead for merging https://github.com/JasonGross/iris-coq/commit/57743dd702b4c09b6e8d7cd171c0d7852d1da39a / https://github.com/JasonGross/iris-coq/compare/fix-for-8064
Import prim token notations before using them
This is required for compatibility with
coq/coq#8064, where prim token notations no longer
follow `Require`, but instead follow `Import`.
c.f. coq/coq#8064 (comment)
All changes were made via
https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-pyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/207Rule "Res-Alloc" in documentation is stronger than the Coq version2019-03-06T09:54:29ZJoseph TassarottiRule "Res-Alloc" in documentation is stronger than the Coq versionIn the rule "Res-alloc" on page 26 of the documentation (see https://plv.mpi-sws.org/iris/appendix-3.1.pdf, or https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/ghost-state.tex#L211) the set for the new ghost name is allowed to be ...In the rule "Res-alloc" on page 26 of the documentation (see https://plv.mpi-sws.org/iris/appendix-3.1.pdf, or https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/ghost-state.tex#L211) the set for the new ghost name is allowed to be an arbitrary infinite set.
However, what's proved here (https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/base_logic/lib/own.v#L116) in the Coq code is a little bit weaker -- you only get that the new name must be in the complement of a finite set.
The stronger rule should be true though. As @robbertkrebbers points out, basically one first needs to port something like `gset_disj_alloc_updateP_strong` to `gmap`, and then the stronger result follows.https://gitlab.mpi-sws.org/iris/iris/-/issues/206Missing error message with `iDestruct ... as "#..."`2019-01-23T09:20:00ZRalf Jungjung@mpi-sws.orgMissing error message with `iDestruct ... as "#..."`Testcase:
```coq
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".
```
Prints
```
No matching clauses for match.
```
That's never an acceptable ...Testcase:
```coq
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".
```
Prints
```
No matching clauses for match.
```
That's never an acceptable error message, obviously.https://gitlab.mpi-sws.org/iris/iris/-/issues/204Support `iInduction .. using ...`2018-08-29T09:48:58ZRobbert KrebbersSupport `iInduction .. using ...`Like `induction ... using ...`; so one can more easily use custom induction principle like `map_ind`.
Requested by @dfruminLike `induction ... using ...`; so one can more easily use custom induction principle like `map_ind`.
Requested by @dfruminRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/201Improve "... not found" error messages2019-01-11T09:44:12ZRalf Jungjung@mpi-sws.orgImprove "... not found" error messagesCurrently, the message says `(INamed "HQ") not found.`. Can we improve that to `"HQ" not found.`?Currently, the message says `(INamed "HQ") not found.`. Can we improve that to `"HQ" not found.`?https://gitlab.mpi-sws.org/iris/iris/-/issues/200Framing: Make* classes lead to suboptimal results2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgFraming: Make* classes lead to suboptimal resultsFraming uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_la...Framing uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_later_rel (P : PROP) :
▷ P -∗ (▷ (P ∧ P)).
Proof. iIntros "?". iFrame.
(* Now the goal is [▷ emp] *)
```
I would expect the goal to become `emp` (and hence `iFrame` closing the goal), and indeed that would be sound (`emp` implies `▷ emp`) but it doesn't happen.https://gitlab.mpi-sws.org/iris/iris/-/issues/199iSplitL no longer checks if assumptions are spatial2018-06-10T20:13:10ZRalf Jungjung@mpi-sws.orgiSplitL no longer checks if assumptions are spatialThe following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```The following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/198iAlways fails without a proper error message2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgiAlways fails without a proper error messageThe following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last ca...The following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last call failed.
No matching clauses for match.
```
It should either give a proper error or empty the spatial context.https://gitlab.mpi-sws.org/iris/iris/-/issues/197iFrame sometimes needs to be called twice2018-06-14T11:41:14ZRalf Jungjung@mpi-sws.orgiFrame sometimes needs to be called twiceConsider the following proof (written in the context of `tests/proofmode_monpred.v`):
```
Program Definition monPred_id (R : monPred) : monPred :=
MonPred (λ V, R V) _.
Next Obligation. intros ? ???. eauto. Qed.
Lemma test_iFr...Consider the following proof (written in the context of `tests/proofmode_monpred.v`):
```
Program Definition monPred_id (R : monPred) : monPred :=
MonPred (λ V, R V) _.
Next Obligation. intros ? ???. eauto. Qed.
Lemma test_iFrame_monPred_id (P Q R : monPred) i :
(P i) ∗ (Q i) ∗ (R i) -∗ (P ∗ Q ∗ monPred_id R) i.
Proof.
iIntros "(? & ? & ?)". iFrame. iFrame.
Qed.
```
Notice that I need to call `iFrame` twice. That should not be necessary.
This lead to a bunch of additional rewrites being introduced when fixing the fallout from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/154 because the `[$]` specialization pattern stopped working (it does `iFrame` just once, it seems).https://gitlab.mpi-sws.org/iris/iris/-/issues/195Always qualify Instance with Local or Global2021-01-07T13:58:38ZRalf Jungjung@mpi-sws.orgAlways qualify Instance with Local or GlobalSince you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? Fo...Since you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? For the same reason that we should always use qualifiers, `sed` cannot know whether we are inside a section.
I can do the `sed`, but I'm not sure how to do the review if any of these should be `Local`. Also, let's do this after merging some MRs because this will cause plenty of conflicts.https://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/193Remove or fix `base_logic/deprecated.v`2018-07-13T08:51:26ZRobbert KrebbersRemove or fix `base_logic/deprecated.v`It currently contains:
```
(*
FIXME
...
*)
```It currently contains:
```
(*
FIXME
...
*)
```Generalized Proofmode Mergerhttps://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/191Printing of the sequence operator `;;`2018-06-13T10:08:33ZMarianna RapoportPrinting of the sequence operator `;;`The [first](https://gitlab.mpi-sws.org/FP/iris-examples/blob/f9bee86a91025f7d727a1765a2d9ad98fbd10c9f/theories/lecture_notes/coq_intro_example_1.v) Coq example that comes with the Iris [lecture notes]() shows how to prove a lemma with th...The [first](https://gitlab.mpi-sws.org/FP/iris-examples/blob/f9bee86a91025f7d727a1765a2d9ad98fbd10c9f/theories/lecture_notes/coq_intro_example_1.v) Coq example that comes with the Iris [lecture notes]() shows how to prove a lemma with the following proof goal:
`{{{ ℓ ↦ #n }}} (incr ℓ) ||| (incr ℓ) ;; !#ℓ {{{m, RET #m; ⌜n ≤ m⌝ }}}`
However, in the interactive proof mode, the goal is displayed as
`{{{ ℓ ↦ #n }}} (Lam <> ! #ℓ) (incr ℓ ||| incr ℓ) {{{ (m : Z), RET #m; ⌜n ≤ m⌝}}}`
I.e. Coq automatically desugars the `;;` notation.