Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-10-20T09:21:24Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-10-20T09:21:24ZPaolo G. GiarrussoMake `contractive_proper` into a lemma, or control other instances that make it costly.Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://...Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?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/316Explore use of `#[local]`/`Local` definitions2020-10-02T11:44:42ZRalf Jungjung@mpi-sws.orgExplore use of `#[local]`/`Local` definitionsI recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions...I recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.
As a random example for such definitions, [consider these](https://gitlab.mpi-sws.org/iris/iris/-/blob/701b533c8be530a69e605ee5443a089146d5701f/theories/base_logic/lib/gen_heap.v#L136-164).
`Local Definition` is supported in Coq 8.9 (and maybe older) so we can start using it any time.https://gitlab.mpi-sws.org/iris/iris/-/issues/312Fix setoid rewriting for function application in Iris2021-07-25T11:37:33ZPaolo G. GiarrussoFix setoid rewriting for function application in IrisSome of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fi...Some of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fix by reading rewrite's error message, and I adapted this to Iris:
```coq
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
```
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.https://gitlab.mpi-sws.org/iris/iris/-/issues/304Direction of _op lemmas is inconsistent with _(p)core, _valid, _included2021-12-06T20:17:41ZRalf Jungjung@mpi-sws.orgDirection of _op lemmas is inconsistent with _(p)core, _valid, _includedSee the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔...See the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
```
However, most of our `_op` lemmas push the named operation "out":
```coq
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
```
Moreover, even with one "group" of lemmas, not all are consistent: `singleton_op`, `discrete_fun_singleton_op`, `list_singleton_op` push "in", while `cmra_morphism_(p)core` push "out" (and there might be more).
At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the `_op` lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/303, so this starts to look like we are just going back and forth...https://gitlab.mpi-sws.org/iris/iris/-/issues/303Canonical structures have major performance impact2020-05-11T18:22:36ZRobbert KrebbersCanonical structures have major performance impactAs I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and ...As I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and `bi` canonical structures.
- [37.40% overall on lambdarust-weak](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=masters%2Fweak_mem&var-commit1=bcc7c0be5ba2def0989d727c97d94a8492b9e40b&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi_weak&var-commit2=4ea92744abcd644f385696c398206a20a2cab7cf&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 72.22%.
- [23.28% overall on Iron](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iron&var-branch1=master&var-commit1=4dcc142742d846037be4cd94678ff8759465e6c1&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=37f90dd22db3ca477377d16ae72d761cb617412c&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 38.13%.
- [3.8% overall on Iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=9b2ad256fbf948933cdbf6c313eb244fd2439bf3&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=294ef2ef2df5478db81065f6cd5edc1d831419a1&var-config2=build-coq.8.11.0&var-group=().*&var-metric=instructions), with improvements for individual files up to 13.16%.
- [5.2% overall on lamdarust master](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=bea9f4a02efe48a38894fe1286add7ab25a2d2de&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 10.18%.
These differences are major, especially for the projects that use BI formers (monPred in lambdarust-weak and fracPred in Iron)! So it looks like there is really something we should investigate.https://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/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/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/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/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`.https://gitlab.mpi-sws.org/iris/iris/-/issues/275use implicit arguments for lemmas in coq_tactics.v2019-11-22T16:30:29ZPaolo G. Giarrussouse implicit arguments for lemmas in coq_tactics.v- [ ] The following [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/338#note_42171) from !338 should be addressed:
> > I was tempted to use implicit arguments instead of (some of) these underscores to make the `refi...- [ ] The following [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/338#note_42171) from !338 should be addressed:
> > I was tempted to use implicit arguments instead of (some of) these underscores to make the `refine` more readable... does that cause problems? [@Blaisorblade]
> I have been thinking about this many times. However, we should not just do it locally here, but should do it globally for all proof mode tactics. First let's get #135 fixed and then do what you suggest. [@robbertkrebbers]https://gitlab.mpi-sws.org/iris/iris/-/issues/273Iris shadows ssreflect new syntax2019-11-22T16:31:07ZPaolo G. GiarrussoIris shadows ssreflect new syntaxIris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
In 8.10.1 ssreflect introduced syntax using `[^` and `[^~`, but they're shadowed by iris's big_op notations....Iris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
In 8.10.1 ssreflect introduced syntax using `[^` and `[^~`, but they're shadowed by iris's big_op notations.
Here's a mininal example. Block introductions are pointless here — but useful for big datatypes.
```coq
From iris.algebra Require Import base.
Lemma foo (n : nat) : n = n.
elim: n => [^ s]. (* Works *)
Restart.
elim: n => [^~ s]. (* Works *)
Abort.
From iris.proofmode Require Import tactics.
Locate "[^". (* big_op notations *).
Lemma foo (n : nat) : n = n.
(* Parse error for each of the following commands: *)
elim: n => [^~ s].
elim: n => [^ s].
(* Each gives:
Syntax error: [tactic:ssripats_ne] expected after '=>' (in [tactic:ssrintros_ne]).
*)
```
Iris version: dev.2019-11-02.2.ea809ed4.https://gitlab.mpi-sws.org/iris/iris/-/issues/272Fix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8...2020-02-12T10:10:51ZRobbert KrebbersFix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8.9.0This issue is to track the status of the performance regression in Coq 8.10.1.
* [Compare Timing for std++](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=stdpp&var-branch1=master&var-commit1=9e267150f49e87f4c...This issue is to track the status of the performance regression in Coq 8.10.1.
* [Compare Timing for std++](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=stdpp&var-branch1=master&var-commit1=9e267150f49e87f4c9e15e61e5e48a2c57acf8d6&var-config1=coq-8.9.0&var-branch2=master&var-commit2=3a0c0ae002a0b51c0ab25586c6ed2fd43173aef8&var-config2=coq-8.10.1&var-group=(.*)&var-metric=instructions)
* [Compare Timing for iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=891124d61509345967eec12e004eda252f76342a&var-config1=coq-8.9.0&var-branch2=master&var-commit2=e46457b2a05b94c4815ec08d9e9f4506c52e0e42&var-config2=coq-8.10.1&var-group=(.*)&var-metric=instructions)
A possible cause: https://github.com/coq/coq/issues/11063https://gitlab.mpi-sws.org/iris/iris/-/issues/268`iInv`: support tokens that are "framed" around the accessor2020-03-18T15:01:32ZDan Frumin`iInv`: support tokens that are "framed" around the accessorI have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" ...I have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" "Hcl"
```
This also prevents me from using the `(x1 x2) "..."` introduction pattern. E.g. instead of
```
iInv N with "Hp" as (x) "[H1 H2]" "Hcl"
```
one has to write
```
iInv N with "Hp" as "[H Hp]" "Hcl";
iDestruct "H" as (x) "[H1 H2]"
```
It is not immediately obvious how to modify the tactics, because in general the `selpat` in `iInv N with selpat` can be an arbitrary selection pattern and not just one identifier.https://gitlab.mpi-sws.org/iris/iris/-/issues/267Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.2019-11-01T13:07:58ZDan FruminInconsistent order of arguments for `inv_alloc` and `cinv_alloc`.```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_a...```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_alloc` first takes the namespace and then the mask, but `cinv_alloc` first takes the mask and the the namespace.https://gitlab.mpi-sws.org/iris/iris/-/issues/264Investigate use of "Filtered Unification"2019-11-01T13:02:29ZRalf Jungjung@mpi-sws.orgInvestigate use of "Filtered Unification"When I talked with Matthieu at ICFP about our unification problems, he told me to look at "filtered unification" and thought it might help. The docs are at https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.typeclasses-filte...When I talked with Matthieu at ICFP about our unification problems, he told me to look at "filtered unification" and thought it might help. The docs are at https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.typeclasses-filtered-unification.
So, let's look at that at some point. ;)