Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-02-27T11:21:27Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/230"Generalizable All Variables" considered harmful2019-02-27T11:21:27ZRalf Jungjung@mpi-sws.org"Generalizable All Variables" considered harmfulOver the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and ...Over the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and then consider the following preamble:
```
Section something_about_sprop.
Conext `{authG Σ (exR spropC)}.
```
Can you spot what's wrong with this? Well, we just assumed that SProp is discrete, which it is not. Ouch.
From my experiments, we can avoid over-eager generalization by adding a `!`. I have not found conclusive documentation for `!`, but it seems the least we should do is (a) add `!` basically everywhere, and (b) treat the *absence* of `!` as a big fat warning bell during code review. The latter will be hard.
But really, while `Generalizable All Variables` is very useful for some things (like the general fin map libraries in std++), I think for most code the benefits are slim. I have [ported a few files](https://gitlab.mpi-sws.org/iris/iris/commit/f5bceb45532b5c9dff9124589b93eccee722be8f) to `Generalizable No Variables`, and the additional declarations required are negligible IMO. So I think what we should aim for (but that might take a while) is for std++ to no longer set `Generalizable All Variables` (to avoid inflicting this subtle issue onto unsuspecting users), and to locally set that flag in the (few) files that really benefit.
Or maybe I am overreacting, and things are not that bad. But the thought of accidentally assuming things I don't want to assume makes me nervous. What do you think?https://gitlab.mpi-sws.org/iris/iris/-/issues/229Odd Behavior for Substitution2020-03-12T21:08:39ZDaniel GratzerOdd Behavior for SubstitutionHello,
Simon noticed a somewhat odd occurrence with substitution today. Apparently values are no longer required to be closed (?) but defining a value which is open seems to break substitution in a confusing way?
```
Definition tryset ...Hello,
Simon noticed a somewhat odd occurrence with substitution today. Apparently values are no longer required to be closed (?) but defining a value which is open seems to break substitution in a confusing way?
```
Definition tryset : val :=
λ: "n",
CAS "x" NONE (SOME "n").
Definition check : val :=
λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
NONE => #()
| SOME "n" =>
match: !"x" with
NONE => assert: #false
| SOME "m" => assert: "n" = "m"
end
end.
Definition mk_oneshot : val := λ: <>,
let: "x" := ref NONE in (tryset, check).
```
With this example program we have separated out `tryset` and `check` even though they both depend on `"x"`. However, when proving some properties about `mk_oneshot` substituting `"x"` for a new location `#l` does not replace `"x` in either.
This behavior is demonstrated by the attached file: [oneshot.v](/uploads/cc01dea007082db718057bb66ad87c88/oneshot.v). Am I missing something obvious here?https://gitlab.mpi-sws.org/iris/iris/-/issues/226Typeclass interference does not work for Timeless (□ P)2019-02-12T20:55:26ZMichael SammlerTypeclass interference does not work for Timeless (□ P)In the following code I would expect the first `apply _` to work. Instead `affinely_timeless` has to be applied explicitly before `apply _` works.
```
Instance timeless (P : iProp Σ) `{!Timeless P} : Timeless (□ (P)).
Proof.
F...In the following code I would expect the first `apply _` to work. Instead `affinely_timeless` has to be applied explicitly before `apply _` works.
```
Instance timeless (P : iProp Σ) `{!Timeless P} : Timeless (□ (P)).
Proof.
Fail apply _.
eapply affinely_timeless; by apply _. (* this goes through *)
Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/225`is_closed_expr` is stronger than stability under `subst`2019-01-06T17:04:41ZDan Frumin`is_closed_expr` is stronger than stability under `subst`I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
How...I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
However, `is_closed_expr (of_val v) = is_closed_val v` (<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/metatheory.v#L22>) which is not always true.
That means, IIUC, that there are expressions that are not closed, but which are idempotent under the substitution.https://gitlab.mpi-sws.org/iris/iris/-/issues/223Module `iris.algebra.big_op` exports unqualified `foo`2018-12-20T21:06:52ZPaolo G. GiarrussoModule `iris.algebra.big_op` exports unqualified `foo`Minor issue — `iris.algebra.big_op` uses `foo` for the name of an instance. A more unique name might be better.
```
From iris.program_logic Require Import ectx_lifting.
About foo.
foo : ∀ (A : Type) (R : relation A), RewriteRelation R
...Minor issue — `iris.algebra.big_op` uses `foo` for the name of an instance. A more unique name might be better.
```
From iris.program_logic Require Import ectx_lifting.
About foo.
foo : ∀ (A : Type) (R : relation A), RewriteRelation R
Argument A is implicit and maximally inserted
Argument scopes are [type_scope _]
foo is transparent
Expands to: Constant iris.algebra.big_op.foo
```https://gitlab.mpi-sws.org/iris/iris/-/issues/222Can't iSpecialize/iDestruct with (("A" with "B") with "C")2018-12-03T07:17:44ZPaolo G. GiarrussoCan't iSpecialize/iDestruct with (("A" with "B") with "C")`iSpecialize (("HLT" with "Hg") with "HL").` fails with
```
Error:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_c...`iSpecialize (("HLT" with "Hg") with "HL").` fails with
```
Error:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)", last call failed.
Tactic failure: iSpecialize: ("HLT" with "Hg") should be a hypothesis, use iPoseProof instead.
```
While that's technically true, it seems unfortunate, and forces me to call two tactics for the job. I end up writing
`iSpecialize ("HLT" with "Hg"); iDestruct ("HLT" with "HL") as "#HLT1"; auto.`
instead of `iDestruct (("HLT" with "Hg") with "HL") as "#HLT1"; auto.`, which fails with
```
Error:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)", "iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", "iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" and "<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call
failed.
No applicable tactic.
```
FWIW here's my context. Things are persistent as I'm not yet using mutable state (only persistent ghost state).
```
1 subgoal (ID 3041)
Σ : gFunctors
HdotG : dotG Σ
Γ : list ty
T, L, U : ty
γ : gname
ρ : vls
l : label
v : vl
============================
"Hv" : γ ⤇ (λ ρ0 : leibnizC vls, ⟦ T ⟧ ρ0)
"Hg" : ⟦ Γ ⟧* ρ
"HLU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ⟦ L ⟧ ρ0 v0 → ⟦ U ⟧ ρ0 v0
"HTU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ T ⟧ ρ0 v0 → ▷ ⟦ U ⟧ ρ0 v0
"HLT" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ L ⟧ ρ0 v0 → ▷ ⟦ T ⟧ ρ0 v0
"HL" : ▷ ⟦ L ⟧ ρ v
--------------------------------------□
▷ □ ⟦ T ⟧ ρ v
```https://gitlab.mpi-sws.org/iris/iris/-/issues/221Coqdocs should link to std++ coqdocs2019-06-06T11:39:37ZRalf Jungjung@mpi-sws.orgCoqdocs should link to std++ coqdocsWhen using std++ types, like in https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.gmap.html, we should make them link to the std++ docs. I think this involves setting the `--external` flag correctly.When using std++ types, like in https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.gmap.html, we should make them link to the std++ docs. I think this involves setting the `--external` flag correctly.Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/220wp_cas_suc fails with total weakest precondition2018-11-30T09:38:10ZAleš Bizjakales@alesb.comwp_cas_suc fails with total weakest preconditionAs the title mentions wp_cas_suc fails with total weakest precondition. The reason seems to be that the well-formedness assumption on what is stored at the location is not discharged correctly since I can make it go through with
``wp_app...As the title mentions wp_cas_suc fails with total weakest precondition. The reason seems to be that the well-formedness assumption on what is stored at the location is not discharged correctly since I can make it go through with
``wp_apply (twp_cas_suc with "Hpt"); [by left | ].`` instead of wp_cas_suc.
See the [attached file](/uploads/9ef9df2e283a15d2ec19539d09934b55/example.v) for a complete example.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/219What are arrows in the category of CMRAs?2018-11-28T10:31:46ZJacques-Henri JourdanWhat are arrows in the category of CMRAs?In `cmra.v`, we define `CmraMorphism`, and use it int the notion of rFunctor:
```coq
Structure rFunctor := RFunctor {
rFunctor_car : ofeT → ofeT → cmraT;
rFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1...In `cmra.v`, we define `CmraMorphism`, and use it int the notion of rFunctor:
```coq
Structure rFunctor := RFunctor {
rFunctor_car : ofeT → ofeT → cmraT;
rFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
rFunctor_ne A1 A2 B1 B2 :
NonExpansive (@rFunctor_map A1 A2 B1 B2);
rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
rFunctor_compose {A1 A2 A3 B1 B2 B3}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (rFunctor_map fg)
}.
```
However, in the manual we say:
> The category $\CMRAs$ consists of cameras as objects, and monotone functions as arrows.
My question is: Which is right?https://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.`?