Iris issueshttps://gitlab.mpi-sws.org/iris/iris/issues2019-11-08T17:49:41Zhttps://gitlab.mpi-sws.org/iris/iris/issues/273Iris shadows ssreflect new syntax2019-11-08T17:49:41ZPaolo 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.
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.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...2019-11-07T14:11:33ZRobbertFix 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.
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
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/11063This issue is to track the status of the performance regression in Coq 8.10.1.
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
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/271Follow-up from "Lang lemmas": intuitive explanation of mixin_step_by_val2019-11-06T15:26:39ZRalf Jungjung@mpi-sws.orgFollow-up from "Lang lemmas": intuitive explanation of mixin_step_by_valIn !324 I started a [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/324#note_41125) to find an intuitive explanation of "mixin_step_by_val". I propose this, and I still think it's good:
"Let \[fill K e1\] and \[fill K' e1'\] be two decompositions of the same expression such that \[e1'\] is reducible. Then either \[K\] is a prefix of \[K'\] (so \[e1\] actually contains \[e1'\] as its head redex), or \[e1\] is a value. In other words, there cannot be two entirely unrelated head redexes that actually reduce."
@amintimany had an objection that I did not understand:
> This does not really say anything about there not being redxes!
My response:
> Of course it does? If there are redexes, the contexts are related; thus if there are unrelated contexts, there are no redexes.
@amintimany @robbertkrebbers let's discuss here.In !324 I started a [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/324#note_41125) to find an intuitive explanation of "mixin_step_by_val". I propose this, and I still think it's good:
"Let \[fill K e1\] and \[fill K' e1'\] be two decompositions of the same expression such that \[e1'\] is reducible. Then either \[K\] is a prefix of \[K'\] (so \[e1\] actually contains \[e1'\] as its head redex), or \[e1\] is a value. In other words, there cannot be two entirely unrelated head redexes that actually reduce."
@amintimany had an objection that I did not understand:
> This does not really say anything about there not being redxes!
My response:
> Of course it does? If there are redexes, the contexts are related; thus if there are unrelated contexts, there are no redexes.
@amintimany @robbertkrebbers let's discuss here.https://gitlab.mpi-sws.org/iris/iris/issues/270non-Unicode Iris notations2019-11-05T12:58:27ZRalf Jungjung@mpi-sws.orgnon-Unicode Iris notationsSome people askedd about a non-Unicode variant of our notation. @jihgfee @gmalecha have such a file I think, maybe we could contribute that upstream?Some people askedd about a non-Unicode variant of our notation. @jihgfee @gmalecha have such a file I think, maybe we could contribute that upstream?https://gitlab.mpi-sws.org/iris/iris/issues/269Editor config should explain how to configure CoqIDE 8.10 unicode input2019-11-01T13:03:57ZTej ChajedEditor config should explain how to configure CoqIDE 8.10 unicode inputCoqIDE 8.10 has a new feature for inputting unicode symbols with LaTeX-to-unicode conversion (triggered by typing shift-space). It's possible to configure the supported bindings (see https://coq.github.io/doc/master/refman/practical-tools/coqide.html#coqide-unicode), so [Editor.md](Editor.md) should give a configuration file with the Iris LaTeX bindings.CoqIDE 8.10 has a new feature for inputting unicode symbols with LaTeX-to-unicode conversion (triggered by typing shift-space). It's possible to configure the supported bindings (see https://coq.github.io/doc/master/refman/practical-tools/coqide.html#coqide-unicode), so [Editor.md](Editor.md) should give a configuration file with the Iris LaTeX bindings.https://gitlab.mpi-sws.org/iris/iris/issues/268`iInv` with cancellable invariants and a cinv_own token2019-11-01T13:03:41ZDan Frumin`iInv` with cancellable invariants and a cinv_own tokenI 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.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_alloc` first takes the namespace and then the mask, but `cinv_alloc` first takes the mask and the the namespace.```
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-filtered-unification.
So, let's look at that at some point. ;)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. ;)https://gitlab.mpi-sws.org/iris/iris/issues/262`big_op*_forall` that relate traversals over different structures2019-11-01T14:24:43ZDmitry 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, 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.
```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/261Provide smart `bi` constructor for BIs that are not step-indexed2019-11-01T13:00:45ZRobbertProvide smart `bi` constructor for BIs that are not step-indexedIn that case, we can just define the distance relation on the OFE as:
```coq
P ≡{n}≡ Q := P ⊢ Q ∧ Q ⊢ P
```
And all `Proper` axioms should be admissible.In that case, we can just define the distance relation on the OFE as:
```coq
P ≡{n}≡ Q := P ⊢ Q ∧ Q ⊢ P
```
And all `Proper` axioms should be admissible.https://gitlab.mpi-sws.org/iris/iris/issues/258Stronger `list_core_id`2019-11-01T14:09:45ZDmitry KhalanskiyStronger `list_core_id`Hi!
I needed a stronger version of `list_core_id` that could depend on the structure of a particular list, similarly to `pair_core_id`. I came up with this:
```
Global Instance list_core_id l : (forall x, x ∈ l -> CoreId x) -> CoreId l.
Proof.
intros Hyp. constructor. apply list_equiv_lookup=> i.
rewrite list_lookup_core.
destruct (l !! i) eqn:E.
2: done.
apply Hyp.
eapply elem_of_list_lookup; by eauto.
Qed.
```
It probably could serve as a drop-in replacement for the old one.Hi!
I needed a stronger version of `list_core_id` that could depend on the structure of a particular list, similarly to `pair_core_id`. I came up with this:
```
Global Instance list_core_id l : (forall x, x ∈ l -> CoreId x) -> CoreId l.
Proof.
intros Hyp. constructor. apply list_equiv_lookup=> i.
rewrite list_lookup_core.
destruct (l !! i) eqn:E.
2: done.
apply Hyp.
eapply elem_of_list_lookup; by eauto.
Qed.
```
It probably could serve as a drop-in replacement for the old one.https://gitlab.mpi-sws.org/iris/iris/issues/257Auth as Views2019-11-01T13:55:52ZRalf Jungjung@mpi-sws.orgAuth as ViewsGregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.
This subsumes https://gitlab.mpi-sws.org/iris/iris/merge_requests/91 by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as `to_agree`, of `ExclBot`). So instead of the pattern where we do `exists heap, own (● to_auth heap)`, we could have this `to_auth` in the relation.
An open question is what would happen with all our theory about local updates.
Things to do:
* [ ] Implement a generalized "auth as view" library
* [ ] Implement monotone partial bijections (https://gitlab.mpi-sws.org/iris/iris/merge_requests/91) in terms of that.Gregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.
This subsumes https://gitlab.mpi-sws.org/iris/iris/merge_requests/91 by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as `to_agree`, of `ExclBot`). So instead of the pattern where we do `exists heap, own (● to_auth heap)`, we could have this `to_auth` in the relation.
An open question is what would happen with all our theory about local updates.
Things to do:
* [ ] Implement a generalized "auth as view" library
* [ ] Implement monotone partial bijections (https://gitlab.mpi-sws.org/iris/iris/merge_requests/91) in terms of that.https://gitlab.mpi-sws.org/iris/iris/issues/255Failure to find a proof of persistence2019-11-01T12:59:48ZDmitry KhalanskiyFailure to find a proof of persistenceVersion of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
```
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO))))
```
proof of
```
Persistent (own γ (◯((None, None), Some (to_agree true))))
```
fails with
```
Proof search failed without reaching its limit.
```
if performed with `typeclasses eauto 10`. It similarly doesn't work with `apply _`.
The statement is actually persistent, as shown by Jonas Kastberg:
```
Proof.
apply own_core_persistent.
apply auth_frag_core_id.
apply pair_core_id; typeclasses eauto.
Qed.
```
Minimal (non-)working example: https://pastebin.com/T7zhm9ZuVersion of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
```
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO))))
```
proof of
```
Persistent (own γ (◯((None, None), Some (to_agree true))))
```
fails with
```
Proof search failed without reaching its limit.
```
if performed with `typeclasses eauto 10`. It similarly doesn't work with `apply _`.
The statement is actually persistent, as shown by Jonas Kastberg:
```
Proof.
apply own_core_persistent.
apply auth_frag_core_id.
apply pair_core_id; typeclasses eauto.
Qed.
```
Minimal (non-)working example: https://pastebin.com/T7zhm9Zuhttps://gitlab.mpi-sws.org/iris/iris/issues/253Constructing CMRAs by giving isomorphism to CMRAs2019-11-01T14:21:31ZPaolo G. GiarrussoConstructing CMRAs by giving isomorphism to CMRAsIris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).Iris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).https://gitlab.mpi-sws.org/iris/iris/issues/252"Exponentiation" for separating conjunctions2019-11-01T14:27:39ZDmitry Khalanskiy"Exponentiation" for separating conjunctionsSometimes it makes sense to have a statement about possessing `n` copies of the same resource. For example (in pseudocode), `own γ 1%Qp -∗ (own γ (1/n))^n`. Maybe such an operation should be available in the standard library, along with some useful lemmas about exponentiation?
An example of what exponentiation could be defined as:
```
Fixpoint iPropPow {Σ} (R : iProp Σ) (n : nat) : iProp Σ :=
match n with
| 0 => (True)%I
| S n' => (R ∗ iPropPow R n')%I
end.
```Sometimes it makes sense to have a statement about possessing `n` copies of the same resource. For example (in pseudocode), `own γ 1%Qp -∗ (own γ (1/n))^n`. Maybe such an operation should be available in the standard library, along with some useful lemmas about exponentiation?
An example of what exponentiation could be defined as:
```
Fixpoint iPropPow {Σ} (R : iProp Σ) (n : nat) : iProp Σ :=
match n with
| 0 => (True)%I
| S n' => (R ∗ iPropPow R n')%I
end.
```https://gitlab.mpi-sws.org/iris/iris/issues/251Simplification machinery for RA operations2019-11-01T14:03:49ZRalf 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 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`).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 Iris2019-11-01T14:03:35ZRalf 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. We should have that RA in Iris.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:35ZRobbertAvoid 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 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).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/241"Flattened" introduction patterns for intuitionistic conjunction elimination.2019-11-01T13:07:29ZDan Frumin"Flattened" introduction patterns for intuitionistic conjunction elimination.The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `P ∧ Q ∧ R` by `iDestruct "H" as "(H&_&_)"`, but it doesn't work this way.
```
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Lemma test P Q R : (P ∧ Q ∧ R) -∗ P.
Proof.
iIntros "H".
(* This works fine *)
iDestruct "H" as "(_ & _ & H)".
Undo.
iDestruct "H" as "(_ & H & _)".
Undo.
(* This results in an error *)
Fail iDestruct "H" as "(H & _ & _)".
(* "Proper" way of doing it *)
iDestruct "H" as "(H & _)".
done.
Qed.
```The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `P ∧ Q ∧ R` by `iDestruct "H" as "(H&_&_)"`, but it doesn't work this way.
```
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Lemma test P Q R : (P ∧ Q ∧ R) -∗ P.
Proof.
iIntros "H".
(* This works fine *)
iDestruct "H" as "(_ & _ & H)".
Undo.
iDestruct "H" as "(_ & H & _)".
Undo.
(* This results in an error *)
Fail iDestruct "H" as "(H & _ & _)".
(* "Proper" way of doing it *)
iDestruct "H" as "(H & _)".
done.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/issues/240We have ambiguous coercion paths2019-11-01T14:15:31ZRalf Jungjung@mpi-sws.orgWe have ambiguous coercion pathsWhen compiling with Coq master, we see lots of these:
```
[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass
```
Also see e.g. [this build log](https://gitlab.mpi-sws.org/iris/iris/-/jobs/31380).
Is this a problem? Can we do anything about it?When compiling with Coq master, we see lots of these:
```
[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass
```
Also see e.g. [this build log](https://gitlab.mpi-sws.org/iris/iris/-/jobs/31380).
Is this a problem? Can we do anything about it?