Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T12:48:48Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/254Reliance on `Export` bug2019-11-01T12:48:48ZMaxime DénèsReliance on `Export` bugDear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is...Dear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is an easy way to observe the problem on Coq master: take `algebra.ufrac_auth`, and change the first line:
```coq
From iris.algebra Require Export auth frac.
```
into:
```coq
From iris.algebra Require Export auth.
From iris.algebra Require Export frac.
```
it will make the proof of `ufrac_auth_agreeN` fail because a view starts applying in the wrong direction...
Could you provide some guidance on how to make the file pass with the two separate `Export`s? It will probably make it compatible with the fix of the bug I mentioned above.
Thanks!https://gitlab.mpi-sws.org/iris/iris/-/issues/87Remove "dev" from list of compatible coq versions?2017-04-19T16:05:33ZJannoRemove "dev" from list of compatible coq versions?Iris currently lists "dev" as a compatible coq version. I have not tried to find out if it actually is compatible, since ssreflect currently does not compile against coq-dev. @jjourdan and I discussed this issue and we came to the conclu...Iris currently lists "dev" as a compatible coq version. I have not tried to find out if it actually is compatible, since ssreflect currently does not compile against coq-dev. @jjourdan and I discussed this issue and we came to the conclusion that "dev" should be removed and possibly replaced with a comment explaining to add it again when compiling against coq-dev. What does everyone else think?
This issue came up because the inclusion of "dev" breaks `make build-dep` in our gps development. Opam thinks coq-dev is a compatible with both ssreflect (their fault) and Iris (our fault).https://gitlab.mpi-sws.org/iris/iris/-/issues/121Remove `bi_persistently_exist_1` and `bi_plainly_exist_1` from the BI axioms2018-03-19T11:01:03ZJacques-Henri JourdanRemove `bi_persistently_exist_1` and `bi_plainly_exist_1` from the BI axiomsThey possibly not hold for linear logics.They possibly not hold for linear logics.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/368Remove `inv` lemmas for agree/auth/view/etc and add `_L` variants to the ↔ lemma2020-11-04T09:54:59ZRobbert KrebbersRemove `inv` lemmas for agree/auth/view/etc and add `_L` variants to the ↔ lemmaSee the discussion here https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/551#note_58488See the discussion here https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/551#note_58488https://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/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/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/122Rename `AffineBI` and `PositiveBI`2017-12-04T18:34:10ZRobbert KrebbersRename `AffineBI` and `PositiveBI`These should be named `BiAffine` and `BiPositive` to follow the naming scheme we use elsewhere, e.g. for `OfeDiscrete` and `Cmra...`.These should be named `BiAffine` and `BiPositive` to follow the naming scheme we use elsewhere, e.g. for `OfeDiscrete` and `Cmra...`.https://gitlab.mpi-sws.org/iris/iris/-/issues/119Rename bi_later → sbi_later2017-12-04T21:22:48ZRobbert KrebbersRename bi_later → sbi_laterBy @jjourdan: is there a reason why `bi_later` is not called `sbi_later`? Likewise for except_0By @jjourdan: is there a reason why `bi_later` is not called `sbi_later`? Likewise for except_0https://gitlab.mpi-sws.org/iris/iris/-/issues/35Renaming things2016-11-09T12:42:38ZRalf Jungjung@mpi-sws.orgRenaming thingsThere are some names some of us are not happy with. This issue is just meant to track the latest status in these discussions.
* `◇`: After a lot of discussion about `except_last` vs. `except_now`, we agreed that depending on whether y...There are some names some of us are not happy with. This issue is just meant to track the latest status in these discussions.
* `◇`: After a lot of discussion about `except_last` vs. `except_now`, we agreed that depending on whether you look at the adequacy theorem or the state at some point of the proof, either may make sense. We all agreed that `except_0` would be acceptable.
* `≡`: I still plan to rename this from `uPred_eq` to `uPred_internal_eq`.
* The lowest-level view shift... my latest suggestion was
```
|=u=> Q update modality
|={E1,E2}=> Q view modality
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
or
```
|=s=> Q state update (modality)
|={E1,E2}=> Q view update (modality)
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
I couldn't find JH's last proposal. Robbert expressed that he liked Derek's:
```
|=p=> Q primitive shift
|={E1,E2}=> Q primitive view shift
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
However, my concern here is that it becomes hard to say that we want a
"primitive non-view shift". Also, the "primitive view shift" is not
primitive...
* Filenames:
```
base_logic/upred [just the definition, metric space, functors]
base_logic/primitive [primitive connectives and proofs in the model]
base_logic/base_logic or base_logic/logic [upred + primitive + derived connectives/rules]
```Iris 3.0https://gitlab.mpi-sws.org/iris/iris/-/issues/175Replace booleans in proofmode typeclasses by a more informative type2019-11-01T12:51:13ZRalf Jungjung@mpi-sws.orgReplace booleans in proofmode typeclasses by a more informative typeWe have booleans in some of the proofmode typeclasses, which makes them pretty hard to read. We should use more informative types.
Right now, we seem to use booleans several times for the conditional intuitionistic modality, once for c...We have booleans in some of the proofmode typeclasses, which makes them pretty hard to read. We should use more informative types.
Right now, we seem to use booleans several times for the conditional intuitionistic modality, once for conditional affinity, and once for something completely different in `IntoLaterN`.https://gitlab.mpi-sws.org/iris/iris/-/issues/216Replace most occurences of `.. || ..` by `first [..|..]`2021-02-02T16:14:57ZRobbert KrebbersReplace most occurences of `.. || ..` by `first [..|..]`Today I found out, as described [in the Coq documentation](https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#left-biased-branching), that the behavior of `e1 || e2` in Ltac is not what I expected. It will execute `e2` no...Today I found out, as described [in the Coq documentation](https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#left-biased-branching), that the behavior of `e1 || e2` in Ltac is not what I expected. It will execute `e2` not just when `e1` fails, but also when it does not make any progress.
This problem came up when debugging an issue reported by YoungJu Song on Mattermost. He noticed that the `wp_bind` tactic does not work when one tries to bind the top-level term. The code of `wp_bind` contains:
```coq
reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
|| fail "wp_bind: cannot find" efoc "in" e
```
`wp_bind_core` is special casing the context `[]`, and then performs just an `idtac` instead of actually using the bind rule for WP.https://gitlab.mpi-sws.org/iris/iris/-/issues/385reshape_expr does not recognize `fill`2020-12-05T08:58:01ZRalf Jungjung@mpi-sws.orgreshape_expr does not recognize `fill`There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-e...There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-enabling that instance locally in ReLoC, C and Actris.https://gitlab.mpi-sws.org/iris/iris/-/issues/417Revert !118: Use ∃ instead of SIgma for extension axiom2021-06-01T09:05:54ZRobbert KrebbersRevert !118: Use ∃ instead of SIgma for extension axiomI am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet ...I am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet { multiset_car : list A }.
```
And define `dist` and `(≡)` to be modulo permutations. For permutations I use https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.SetoidPermutation.html
Unfortunately, this does not work: the extension axiom of cameras does not seem provable.
```coq
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
```
The problem is that I need to construct `z1` and `z2` as a sigma type, not an ordinary exist. But the type of permutations is a `Prop`, so I cannot do this.
Here's the whole code I have so far:
```coq
From Coq Require Import SetoidPermutation.
From iris.algebra Require Export cmra.
Lemma PermutationA_mono {A} (R1 R2 : relation A) xs1 xs2 :
(∀ x1 x2, R1 x1 x2 → R2 x1 x2) →
PermutationA R1 xs1 xs2 → PermutationA R2 xs1 xs2.
Proof. induction 2; econstructor; by eauto. Qed.
Record multiset A := MultiSet { multiset_car : list A }.
Arguments MultiSet {_} _.
Arguments multiset_car {_} _.
Section multiset.
Context {A : ofe}.
Implicit Types x y : A.
Implicit Types X Y : multiset A.
Local Instance multiset_equiv_instance : Equiv (multiset A) := λ X1 X2,
∀ n, PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_dist_instance : Dist (multiset A) := λ n X1 X2,
PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_valid_instance : Valid (multiset A) := λ _, True.
Local Instance multiset_validN_instance : ValidN (multiset A) := λ _ _, True.
Local Instance multiset_unit_instance : Unit (multiset A) := MultiSet [].
Local Instance multiset_op_instance : Op (multiset A) := λ X1 X2,
MultiSet (multiset_car X1 ++ multiset_car X2).
Local Instance multiset_pcore_instance : PCore (multiset A) := λ X, Some ε.
Global Instance multiset_singleton : Singleton A (multiset A) := λ x,
MultiSet [x].
Lemma multiset_ofe_mixin : OfeMixin (multiset A).
Proof.
split; rewrite /equiv /dist /multiset_equiv_instance /multiset_dist_instance /=.
- done.
- intros n. split.
+ by intros X.
+ intros X1 X2 ?. done.
+ intros X1 X2 X3 ??. by etrans.
- intros n X1 X2. apply PermutationA_mono, dist_S.
Qed.
Canonical Structure multisetO := Ofe (multiset A) multiset_ofe_mixin.
Global Instance multiset_ofe_discrete : OfeDiscrete A → OfeDiscrete multisetO.
Proof.
intros HA [xs1] [xs2] Hxs n. revert Hxs. apply PermutationA_mono.
by intros x1 x2 ->%(discrete _).
Qed.
Lemma multiset_cmra_mixin : CmraMixin (multiset A).
Proof.
apply cmra_total_mixin; try by eauto.
- intros X n Y1 Y2 HY. by apply (PermutationA_app _).
- by intros n X1 X2.
- intros X1 X2 X3. admit. (* boring case *)
- intros X1 X2 n. apply (PermutationA_app_comm _).
- by intros X n.
- intros X1 X2 _. exists ε. by intros n.
- intros n [xs] [ys1] [ys2] _. rewrite /equiv /dist /op
/multiset_equiv_instance /multiset_dist_instance /multiset_op_instance /=.
(* Stuck here. The witness [PermutationA (dist n) xs (ys1 ++ ys2)] basically
says how the elements in [xs] are distributed over [ys1] and [ys2].
Intuitively, it says element 0 of [xs] goes to position [i0] in
[ys1 ++ ys2], element 1 of [xs] goes to position [i1] in ys1 ++ ys2 and so
on. *)
(* I would like to use the lemma [PermutationA_decompose], but that does
not work since it gives an [∃]. *)
(* I tried to prove it by induction on the list instead, but that seems
pointless. At some point I need to invert on the [PermutationA] witness,
which is not possible. *)
induction ys1 as [|y1 ys1 IH]; intros Hxs; simpl in *.
{ by exists (MultiSet []), (MultiSet xs). }
admit.
Admitted.
Canonical Structure multisetR := Cmra (multiset A) multiset_cmra_mixin.
Lemma multiset_ucmra_mixin : UcmraMixin (multiset A).
Proof. split; [done | | done]. by intros X n. Qed.
Canonical Structure multisetUR := Ucmra (multiset A) multiset_ucmra_mixin.
Global Instance multiset_cancelable X : Cancelable X.
Proof. Admitted.
Global Instance multiset_singleton_ne : NonExpansive (singleton (B:=multiset A)).
Proof. intros n x1 x2. by repeat constructor. Qed.
Global Instance multiset_singleton_proper :
Proper ((≡) ==> (≡)) (singleton (B:=multiset A)).
Proof. apply (ne_proper _). Qed.
Global Instance multiset_singleton_dist_inj n :
Inj (dist n) (dist n) (singleton (B:=multiset A)).
Proof. intros x1 x2. Admitted.
Global Instance multiset_singleton_inj :
Inj (≡) (≡) (singleton (B:=multiset A)).
Proof.
intros x1 x2 Hx. apply equiv_dist=> n. apply (inj singleton). by rewrite Hx.
Qed.
End multiset.
Global Arguments multisetO : clear implicits.
Global Arguments multisetR : clear implicits.
Global Arguments multisetUR : clear implicits.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/107Reverting to old (stronger) definition of atomicity2017-10-29T14:58:25ZAmin TimanyReverting to old (stronger) definition of atomicityIn Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` is *stuck*.
The old definition was: ```e``` is a...In Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` is *stuck*.
The old definition was: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` *is a value*.
These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike ```WP``` do not guarantee safety, e.g., ```IC``` (if convergent predicates).Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/41Rewrite unexpectedly failing (Nested below |-, *, \later, -*)2016-10-28T09:07:53ZRalf Jungjung@mpi-sws.orgRewrite unexpectedly failing (Nested below |-, *, \later, -*)The rewrite at <https://gitlab.mpi-sws.org/FP/iris-coq/blob/ralf/broken-rewrite/heap_lang/lifting.v#L66> is unexpectedly failing.
The goal is of the shape
```
▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v)
```
and I am ...The rewrite at <https://gitlab.mpi-sws.org/FP/iris-coq/blob/ralf/broken-rewrite/heap_lang/lifting.v#L66> is unexpectedly failing.
The goal is of the shape
```
▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v)
```
and I am trying to rewrite backwards with `P ⊢ |={E}=> P` to remove the fancy update (behind the linear view shift notation).
Cc @robbertkrebbers could you have a look at this?Robbert KrebbersRobbert Krebbershttps://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/37saved_prop for predicate2016-10-05T23:07:43ZGhost Usersaved_prop for predicateI have a `Q: val -> iProp`, now I want to save predicate `Q` just like the saved proposition. How to do that?I have a `Q: val -> iProp`, now I want to save predicate `Q` just like the saved proposition. How to do that?https://gitlab.mpi-sws.org/iris/iris/-/issues/203Seal off local and frame-preserving update2019-11-01T12:50:04ZRalf Jungjung@mpi-sws.orgSeal off local and frame-preserving updateThat might solve `apply` diverging all the time.That might solve `apply` diverging all the time.https://gitlab.mpi-sws.org/iris/iris/-/issues/344Set Default Goal Selector2020-11-10T19:12:02ZRalf Jungjung@mpi-sws.orgSet Default Goal SelectorAs a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.As a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.