Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-03-30T09:38:01Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/300vs doesn't use FUpd2020-03-30T09:38:01ZGregory Malechavs doesn't use FUpdIs there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `m...Is there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `monPred x (iProp _)` even though all of the other notation (that are conceptually very simple) do work at `monPred`.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/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/297Persistent (and other BI class) instances missing for telescopes2020-03-05T18:44:04ZRobbert KrebbersPersistent (and other BI class) instances missing for telescopeshttps://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/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/290Possible redesign of handling of persistent/intuitionistic propositions in in...2020-02-11T17:35:16ZRalf Jungjung@mpi-sws.orgPossible redesign of handling of persistent/intuitionistic propositions in intro patternsAt https://gitlab.mpi-sws.org/iris/iris/merge_requests/370#note_43784 we had some discussion about possible re-designs of the handling of persistent/intuitionistic propositions (when `#` is needed and when not) with the goal of being mor...At https://gitlab.mpi-sws.org/iris/iris/merge_requests/370#note_43784 we had some discussion about possible re-designs of the handling of persistent/intuitionistic propositions (when `#` is needed and when not) with the goal of being more consistent. That was put on hold for now due to being too much work and likely also breaking many things; the issue here tracks possibly doing at least some of that in the future if we want to improve the situation around the `#` pattern (and its opt-out version, whatever that will be).https://gitlab.mpi-sws.org/iris/iris/-/issues/289Documentation for installation on Windows2020-02-06T16:07:24ZRalf Jungjung@mpi-sws.orgDocumentation for installation on WindowsWe have very few Windows users, but every now and then the question comes up and we are rather clueless about what is the best way to use Iris on Windows. It would be good to document some best practices. (This is a sister issue to https...We have very few Windows users, but every now and then the question comes up and we are rather clueless about what is the best way to use Iris on Windows. It would be good to document some best practices. (This is a sister issue to https://gitlab.mpi-sws.org/iris/iris/issues/280.)
Cc @codyroux @quarkbeast @blaisorbladehttps://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/287iApply strips some modalities, but not monotonically2020-02-01T13:06:32ZPaolo G. GiarrussoiApply strips some modalities, but not monotonicallyHere's a minimized inconsistent behavior and a possible fix via an instance. I suspect *that* instance is missing by design, but I can't tell what the design is, even tho I can read `Hint Mode` — see #139.
(I also realize that such insta...Here's a minimized inconsistent behavior and a possible fix via an instance. I suspect *that* instance is missing by design, but I can't tell what the design is, even tho I can read `Hint Mode` — see #139.
(I also realize that such instances must appear for either all or none of the monotonic modalities).
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import bi.
Import bi.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
(* Here [iApply] works. *)
Lemma foo0 P : □ P -∗ P.
Proof. iIntros "H". iApply "H". Qed.
(* But here it fails! *)
Lemma foo1 P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". Fail iApply "H". iNext. iApply "H". Qed.
(* Here's a possible fix, but I'm unsure whether it respects the interplay of
FromAssumption, KnownLFromAssumption and KnownRFromAssumption,
as it is not fully documented.
Should I add this for both KnownLFromAssumption and KnownRFromAssumption? *)
Global Instance from_assumption_later_later p P Q :
FromAssumption p P Q → FromAssumption p (▷ P) (▷ Q)%I.
Proof.
rewrite /KnownRFromAssumption /FromAssumption
later_intuitionistically_if_2 => ->. exact: later_mono.
Qed.
Lemma foo P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". iApply "H". Qed.
End sbi_instances.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/286Address the STS encodings lack of usefulness2020-01-30T21:32:04ZJonas KastbergAddress the STS encodings lack of usefulnessThe current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "ve...The current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".
Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out.
Going forward we should do either of the following:
- Include a disclaimer discouraging people from using them
- Remove the encoding from the repository
- Update the implementation to be more user-friendly
I suggest doing either of the first two short-term and then possibly look into the third long-term.
It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.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/280Documentation for installation on OS X2020-02-06T16:07:27ZJules JacobsDocumentation for installation on OS XPerhaps there could be an Install.md that describes the installation process to install Coq, Iris, and an IDE for Coq on OS X (and other platforms). Not everything works well on OS X. CoqIDE is extremely slow, for instance, and the main ...Perhaps there could be an Install.md that describes the installation process to install Coq, Iris, and an IDE for Coq on OS X (and other platforms). Not everything works well on OS X. CoqIDE is extremely slow, for instance, and the main Coq extension for VS code does not work well, and OS X has an old version of Make that fails sometimes. VS Code + the maximedenes.vscoq for Coq + oijaz.unicode-latex for unicode input works reasonably well. What I eventually did was something like:
```
/usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
brew update
brew install make
brew install opam
opam init
eval $(opam env)
opam install coq
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-iris
brew install visual-studio-code
code --install-extension maximedenes.vscoq
code --install-extension oijaz.unicode-latex
```
A complete recipe like that might save new people a lot of time.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/278Write `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendl...2019-12-12T22:47:43ZRalf Jungjung@mpi-sws.orgWrite `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendly waySee [this discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/340#note_42362): `wp_apply` only works poorly for array accesses currently due to `Z` vs `nat` conflicts. We should find a way to do better.
Equipping `wp_load` w...See [this discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/340#note_42362): `wp_apply` only works poorly for array accesses currently due to `Z` vs `nat` conflicts. We should find a way to do better.
Equipping `wp_load` with support for array accesses is certainly a good idea, but I think we should also figure out a way to write such lemmas in a more apply-friendly style that can be used by other lemmas without having to write a tactic for each of them.https://gitlab.mpi-sws.org/iris/iris/-/issues/277Find a way to reduce usage of O/R/U suffixes2019-12-02T12:56:11ZRalf Jungjung@mpi-sws.orgFind a way to reduce usage of O/R/U suffixesIt is very annoying to have to remember those O/R/U suffices for our algebra instances. This comes up mostly when defining `inG`. It would be good to find a way to avoid having to remember and use them.
@robbertkrebbers proposed some sc...It is very annoying to have to remember those O/R/U suffices for our algebra instances. This comes up mostly when defining `inG`. It would be good to find a way to avoid having to remember and use them.
@robbertkrebbers proposed some scheme similar to the already existing `ofe_mixin_of`.