Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-11-08T18:15:18Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/273Iris shadows ssreflect new syntax2022-11-08T18:15:18ZPaolo G. GiarrussoIris shadows ssreflect new syntaxIris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
Since Coq 8.10.1 ssreflect introduced syntax using `[^` and `[^~`, but they're shadowed by iris's big_op not...Iris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
Since Coq 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.
Example (EDIT: updated for modern Iris).
```coq
(* https://gitlab.mpi-sws.org/iris/iris/-/issues/273 *)
From iris.prelude Require Import prelude.
Lemma foo (n : nat) : n = n.
elim: n => [^ s]. (* Works *)
Restart.
elim: n => [^~ s]. (* Works *)
Abort.
Locate "[^". (* big_op notations *)
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 .. 4.0.0https://gitlab.mpi-sws.org/iris/iris/-/issues/262`big_op*_forall` that relate traversals over different structures2020-01-21T18:50:28ZDmitry Khalanskiy`big_op*_forall` that relate traversals over different structuresMost lemmas that relate several `big_op` statements only concern themselves with the case when the iteration is performed on the same data. However, at times, even if the structures are actually different, the values combined by `o` are,...Most lemmas that relate several `big_op` statements only concern themselves with the case when the iteration is performed on the same data. However, at times, even if the structures are actually different, the values combined by `o` are, in fact, the same.
So, I think that `big_op*_forall` can be usefully generalized.
Here is my attempt at generalizing `big_opL_forall`:
```
Theorem big_opL_forall' {M: ofeT} {o: M -> M -> M} {H': Monoid o} {A B: Type}
R f g (l: list A) (l': list B):
Reflexive R ->
Proper (R ==> R ==> R) o ->
length l = length l' ->
(forall k y y', l !! k = Some y -> l' !! k = Some y' -> R (f k y) (g k y')) ->
R ([^o list] k ↦ y ∈ l, f k y) ([^o list] k ↦ y ∈ l', g k y).
Proof.
intros ??. revert l' f g. induction l as [|x l IH]=> l' f g HLen HHyp //=.
all: destruct l'; inversion HLen; eauto.
simpl. f_equiv; eauto.
Qed.
```
A client of this theorem that I actually needed:
```
Lemma big_opL_irrelevant_element (M: ofeT) (o: M -> M -> M) (H': Monoid o)
{A: Type} n (P: nat -> M) (l: list A):
([^o list] i ↦ _ ∈ l, P (n+i)%nat)%I =
([^o list] i ∈ seq n (length l), P i%nat)%I.
Proof.
assert (length l = length (seq n (length l))) as HSeqLen
by (rewrite seq_length; auto).
apply big_opL_forall'; try apply _. done.
intros ? ? ? _ HElem.
assert (k < length l)%nat as HKLt.
{ rewrite HSeqLen. apply lookup_lt_is_Some. by eexists. }
apply nth_lookup_Some with (d:=O) in HElem.
rewrite seq_nth in HElem; subst; done.
Qed.
```
Without `big_forall'`, I couldn't come up with such a straightforward proof and ended up with this unpleasantness:
```
Lemma big_opL_irrelevant_element (M: ofeT) (o: M -> M -> M) (H': Monoid o)
{A: Type} n (P: nat -> M) (l: list A):
([^o list] i ↦ _ ∈ l, P (n+i)%nat)%I =
([^o list] i ∈ seq n (length l), P i%nat)%I.
Proof.
move: n. induction l; simpl. done.
move=> n. rewrite -plus_n_O.
specialize (IHl (S n)).
rewrite -IHl /= (big_opL_forall _ _ (fun i _ => P (S (n + i))%nat)) //.
intros. by rewrite plus_n_Sm.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/251Simplification machinery for RA operations2023-05-25T11:45:26ZRalf Jungjung@mpi-sws.orgSimplification machinery for RA operationsOne repeating point of frustration and confusion for new people learning Iris is how to deal with validity, composition, inclusion and updates of RAs that are composed by layering our combinators. Basically you need to peel off these co...One repeating point of frustration and confusion for new people learning Iris is how to deal with validity, composition, inclusion and updates of RAs that are composed by layering our combinators. Basically you need to peel off these combinators layer-by-layer and find the right lemmas each time, which can be very tricky, and even for an experienced Iris user this frequently takes way more time than it should. Things get worse because Coq's unification is often not able to apply these lemmas.
So @simonspies and @lepigre suggested we should have some (typeclass-based?) simplification machinery for these operations. Something that is able to e.g. turn `✓ (● Excl' n ⋅ ◯ Excl' m)` into `n = m`, or `{[l := x]} ≼ f <$> σ` into `exists y, σ !! l = Some y /\ f y ≼ x` (and then if `f = to_agree` and `x = to_agree v` maybe even into `σ !! l = v`).https://gitlab.mpi-sws.org/iris/iris/-/issues/244Add a general lattice RA to Iris2020-12-10T16:56:05ZRalf Jungjung@mpi-sws.orgAdd a general lattice RA to IrisHistories as monotonically growing lists are something that comes up every now and then, and it can be quite annoying to formalize. I believe we have something like that already in GPFSL, based on a general framework of (semi-) lattices....Histories as monotonically growing lists are something that comes up every now and then, and it can be quite annoying to formalize. I believe we have something like that already in GPFSL, based on a general framework of (semi-) lattices. We should have that RA in Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/243Avoid type-level aliases for overloading of canonical structures2019-11-01T13:05:35ZRobbert KrebbersAvoid type-level aliases for overloading of canonical structuresIn https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a...In https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a canonical structure for a type... Why cannot we define `ufrac` as something like: `Record ufrac := uf_qp { qp_uf : Qp }.`? Sure, this will require some boilerplate for projecting and boxing fractions, but hoping that such hack will keep a stable behaviors seems rather optimistic!
This applies to `ufrac` (introduced in !195) and `mnat` (introduced a long time ago).https://gitlab.mpi-sws.org/iris/iris/-/issues/235Documentation for the algebra folder2019-11-01T11:10:11ZRobbert KrebbersDocumentation for the algebra folderIt would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical...It would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical structures are used.https://gitlab.mpi-sws.org/iris/iris/-/issues/227Provide a convenient way to define non-recursive ghost state2020-12-07T10:18:54ZRalf Jungjung@mpi-sws.orgProvide a convenient way to define non-recursive ghost stateIt is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definitio...It is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
```
To make things worse, if you forget the `lockΣ`, your proof will still work. You might just have assumed false, accidentally.
Can we do better than that, at least for the simple and common case of non-recursive ghost state?https://gitlab.mpi-sws.org/iris/iris/-/issues/210Generic subset construction for RAs2020-09-08T20:33:39ZRalf Jungjung@mpi-sws.orgGeneric subset construction for RAsIn auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
...In auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
Related to https://gitlab.mpi-sws.org/FP/iris-coq/issues/42 (which also wants to touch `auth`).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.