Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-07-23T09:30:47Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/429Enable the use of the proofmode for proving big-op lemmas2021-07-23T09:30:47ZRalf Jungjung@mpi-sws.orgEnable the use of the proofmode for proving big-op lemmasThere are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find some way to stratify this, so that only some core set of lemmas needs to be shown without the proofmode, and the rest can use the proofmode.There are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find some way to stratify this, so that only some core set of lemmas needs to be shown without the proofmode, and the rest can use the proofmode.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/428Make `iDestruct` work on `▷ ∃` if goal is except_0/update2021-07-22T13:02:40ZRobbert KrebbersMake `iDestruct` work on `▷ ∃` if goal is except_0/updateBIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
Instead, you get an except-0 (`◇`) modality, which can be eliminated if the goal is, for example, an update modality.
This trick is not commonly known, so it would be great if the proof mode's `iDestruct` tactic could use `bi.later_exist_except_0` automatically instead of just failing when the domain `A` is not inhabited.
This is what happens now:
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import updates.
Lemma test `{BiFUpd PROP} {A} (Φ : A → PROP) (Q : PROP) E :
▷ (∃ x, Φ x) ={E}=∗ Q.
Proof.
iIntros "H".
(* Goal:
"H" : ▷ (∃ x : A, Φ x)
--------------------------------------∗
|={E}=> Q *)
(* Tactic failure: iExistDestruct: cannot destruct (▷ (∃ x : A, Φ x))%I. *)
Fail iDestruct "H" as (x) "H".
(* Works *)
iMod (bi.later_exist_except_0 with "H") as (x) "H".
```
I tried to implement what I proposed in this MR some day, but I could not find a satisfactory generalization of the `IntoExist` class. After all, that class then needs to take the goal into account to eliminate the ◇ modality.
An alternative, we could use the `pm_error` infrastructure from #413 (which still needs to be ported to `IntoExists`) to give an error that points the user to `bi.later_exist_except_0` in case the domain `A` is not inhabited.BIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
Instead, you get an except-0 (`◇`) modality, which can be eliminated if the goal is, for example, an update modality.
This trick is not commonly known, so it would be great if the proof mode's `iDestruct` tactic could use `bi.later_exist_except_0` automatically instead of just failing when the domain `A` is not inhabited.
This is what happens now:
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import updates.
Lemma test `{BiFUpd PROP} {A} (Φ : A → PROP) (Q : PROP) E :
▷ (∃ x, Φ x) ={E}=∗ Q.
Proof.
iIntros "H".
(* Goal:
"H" : ▷ (∃ x : A, Φ x)
--------------------------------------∗
|={E}=> Q *)
(* Tactic failure: iExistDestruct: cannot destruct (▷ (∃ x : A, Φ x))%I. *)
Fail iDestruct "H" as (x) "H".
(* Works *)
iMod (bi.later_exist_except_0 with "H") as (x) "H".
```
I tried to implement what I proposed in this MR some day, but I could not find a satisfactory generalization of the `IntoExist` class. After all, that class then needs to take the goal into account to eliminate the ◇ modality.
An alternative, we could use the `pm_error` infrastructure from #413 (which still needs to be ported to `IntoExists`) to give an error that points the user to `bi.later_exist_except_0` in case the domain `A` is not inhabited.https://gitlab.mpi-sws.org/iris/iris/-/issues/427Upstreaming big_op lemmas2021-07-16T09:37:22ZMichael SammlerUpstreaming big_op lemmasRefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
length l1 = length l2 →
([∗ list] k↦x ∈ l1, Φ k x) -∗
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen); destruct l2 => //=; simpl in *.
iDestruct "Hl" as "[Hx1 Hl]". iSplitL "Hx1". by iApply "Himpl".
iApply ("IH" $! (Φ ∘ S) (Ψ ∘ S) l2 _ with "[] Hl").
iIntros "!>" (k y1 y2 ?) "Hl2 /= ?".
by iApply ("Himpl" with "[] [Hl2]").
Unshelve. lia.
Qed.
End sep_list.
Lemma big_sepL2_impl' {A B C D} (Φ : _ → _ → _ → PROP) (Ψ : _ → _ → _ → _) (l1 : list A) (l2 : list B) (l1' : list C) (l2' : list D) `{!BiAffine PROP} :
length l1 = length l1' → length l2 = length l2' →
([∗ list] k↦x;y ∈ l1; l2, Φ k x y) -∗
□ (∀ k x1 x2 y1 y2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ ⌜l1' !! k = Some y1⌝ -∗ ⌜l2' !! k = Some y2⌝ -∗ Φ k x1 x2 -∗ Ψ k y1 y2) -∗
[∗ list] k↦x;y ∈ l1';l2', Ψ k x y.
Proof.
iIntros (Hlen1 Hlen2) "Hl #Himpl".
rewrite !big_sepL2_alt. iDestruct "Hl" as (Hl1) "Hl".
iSplit. { iPureIntro. congruence. }
iApply (big_sepL_impl' with "Hl"). { rewrite !zip_with_length. lia. }
iIntros "!>" (k [x1 x2] [y1 y2]).
rewrite !lookup_zip_with_Some.
iDestruct 1 as %(?&?&?&?).
iDestruct 1 as %(?&?&?&?). simplify_eq. destruct_and!.
by iApply "Himpl".
Qed.
```
How can one prove these lemmas in a way that they can be upstreamed?RefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
length l1 = length l2 →
([∗ list] k↦x ∈ l1, Φ k x) -∗
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen); destruct l2 => //=; simpl in *.
iDestruct "Hl" as "[Hx1 Hl]". iSplitL "Hx1". by iApply "Himpl".
iApply ("IH" $! (Φ ∘ S) (Ψ ∘ S) l2 _ with "[] Hl").
iIntros "!>" (k y1 y2 ?) "Hl2 /= ?".
by iApply ("Himpl" with "[] [Hl2]").
Unshelve. lia.
Qed.
End sep_list.
Lemma big_sepL2_impl' {A B C D} (Φ : _ → _ → _ → PROP) (Ψ : _ → _ → _ → _) (l1 : list A) (l2 : list B) (l1' : list C) (l2' : list D) `{!BiAffine PROP} :
length l1 = length l1' → length l2 = length l2' →
([∗ list] k↦x;y ∈ l1; l2, Φ k x y) -∗
□ (∀ k x1 x2 y1 y2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ ⌜l1' !! k = Some y1⌝ -∗ ⌜l2' !! k = Some y2⌝ -∗ Φ k x1 x2 -∗ Ψ k y1 y2) -∗
[∗ list] k↦x;y ∈ l1';l2', Ψ k x y.
Proof.
iIntros (Hlen1 Hlen2) "Hl #Himpl".
rewrite !big_sepL2_alt. iDestruct "Hl" as (Hl1) "Hl".
iSplit. { iPureIntro. congruence. }
iApply (big_sepL_impl' with "Hl"). { rewrite !zip_with_length. lia. }
iIntros "!>" (k [x1 x2] [y1 y2]).
rewrite !lookup_zip_with_Some.
iDestruct 1 as %(?&?&?&?).
iDestruct 1 as %(?&?&?&?). simplify_eq. destruct_and!.
by iApply "Himpl".
Qed.
```
How can one prove these lemmas in a way that they can be upstreamed?https://gitlab.mpi-sws.org/iris/iris/-/issues/426Notation `≼@{A}` is missing2021-07-07T11:02:38ZRobbert KrebbersNotation `≼@{A}` is missingWe are probably missing such notations for more relations. It would be good to do a sweep.We are probably missing such notations for more relations. It would be good to do a sweep.https://gitlab.mpi-sws.org/iris/iris/-/issues/425Splitting (some of) the laws for persistence into a separate class.2021-06-17T18:42:42ZDan FruminSplitting (some of) the laws for persistence into a separate class.I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persistence modality that can be equipped onto an arbitrary BI.
For later, the BI interface includes the operation itself in the signature, and states a bunch of laws that are satisfied by a degenerate instance of the later modality, and the law that is _not_ satisfied by the degenerate version is in a separate class `BiLöb`.
Would something like that be possible for the persistence modality?
For example, the laws `bi_mixin_persistently_absorbing` and `bi_mixin_persistently_and_sep_elim` could be moved into a separate typeclass; then the remaining laws could be satisfied by the identity function.I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persistence modality that can be equipped onto an arbitrary BI.
For later, the BI interface includes the operation itself in the signature, and states a bunch of laws that are satisfied by a degenerate instance of the later modality, and the law that is _not_ satisfied by the degenerate version is in a separate class `BiLöb`.
Would something like that be possible for the persistence modality?
For example, the laws `bi_mixin_persistently_absorbing` and `bi_mixin_persistently_and_sep_elim` could be moved into a separate typeclass; then the remaining laws could be satisfied by the identity function.https://gitlab.mpi-sws.org/iris/iris/-/issues/424Laterable cleanup2021-07-15T07:49:33ZRalf Jungjung@mpi-sws.orgLaterable cleanuphttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `laterable_alt`).
* [ ] Rename `make_laterable` to follow our modality naming scheme... `laterably`?
* [ ] Resolve TC backtracking issue around `persistent_laterable`
* [ ] `iMod` for `make_laterable` elimination?https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `laterable_alt`).
* [ ] Rename `make_laterable` to follow our modality naming scheme... `laterably`?
* [ ] Resolve TC backtracking issue around `persistent_laterable`
* [ ] `iMod` for `make_laterable` elimination?https://gitlab.mpi-sws.org/iris/iris/-/issues/423⌜...⌝ uses bad scopes2021-06-18T22:07:47ZRalf Jungjung@mpi-sws.org⌜...⌝ uses bad scopes`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
```
This leads to `+` being interpreted as a type.
I think we should remove `%type` here. Not sure about `%stdpp`.`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
```
This leads to `+` being interpreted as a type.
I think we should remove `%type` here. Not sure about `%stdpp`.https://gitlab.mpi-sws.org/iris/iris/-/issues/422`iApply` does not use `FromAssumption` for goal matching2021-06-14T13:46:08ZRobbert Krebbers`iApply` does not use `FromAssumption` for goal matching```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
(P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
```
When using `iApply` in combination with the `with` clause, it will first `iSpecialize` and then use `iApply`, which in these examples turns to the degenerate case of `iExact`. The `iExact` tactic uses `FromAssumption` to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).
When using `iApply` without the `with` clause, it will launch a search using `IntoWand` where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.
The problem is the instance:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
Here, `Q` should match exactly. I tried strengtening it to:
```coq
Global Instance into_wand_wand p q P Q P' Q' :
FromAssumption q P P' →
FromAssumption (p && q) Q' Q →
IntoWand p q (P' -∗ Q') P Q.
```
However, that causes other problems: in some cases the above instance will be triggered instead of instances like `into_wand_bupd_args` causing the following to go wrong:
```coq
Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
(P -∗ Q) -∗ |==> Q.
Proof.
iIntros "H".
iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)
```
This issue came up in practice Simuliris.```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
(P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
```
When using `iApply` in combination with the `with` clause, it will first `iSpecialize` and then use `iApply`, which in these examples turns to the degenerate case of `iExact`. The `iExact` tactic uses `FromAssumption` to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).
When using `iApply` without the `with` clause, it will launch a search using `IntoWand` where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.
The problem is the instance:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
Here, `Q` should match exactly. I tried strengtening it to:
```coq
Global Instance into_wand_wand p q P Q P' Q' :
FromAssumption q P P' →
FromAssumption (p && q) Q' Q →
IntoWand p q (P' -∗ Q') P Q.
```
However, that causes other problems: in some cases the above instance will be triggered instead of instances like `into_wand_bupd_args` causing the following to go wrong:
```coq
Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
(P -∗ Q) -∗ |==> Q.
Proof.
iIntros "H".
iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)
```
This issue came up in practice Simuliris.https://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2021-06-30T17:27:28ZRalf Jungjung@mpi-sws.orgUse siProp more in building the uPred (and BI) interfacesuPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.uPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/419Iron slowdown investigation2021-06-17T07:20:40ZRalf Jungjung@mpi-sws.orgIron slowdown investigationIron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iris from `dev.2021-03-06.3.b0708b01` to `dev.2021-06-03.0.2959900d`. I am not sure if we can do anything about that, but it would be good to at least figure out which changes caused the slowdown (though it looks like there at several, so this might be "death by a thousand cuts").Iron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iris from `dev.2021-03-06.3.b0708b01` to `dev.2021-06-03.0.2959900d`. I am not sure if we can do anything about that, but it would be good to at least figure out which changes caused the slowdown (though it looks like there at several, so this might be "death by a thousand cuts").https://gitlab.mpi-sws.org/iris/iris/-/issues/418library inG instances should be local2021-06-02T14:46:21ZRalf Jungjung@mpi-sws.orglibrary inG instances should be localCurrently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.Currently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.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 { 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.
```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/416big_sep lemmas fail to apply when goal is not eta-expanded2021-05-26T11:31:56ZRalf Jungjung@mpi-sws.orgbig_sep lemmas fail to apply when goal is not eta-expandedI just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failure: iApply: cannot apply
(([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, ?Goal k y1 y2)
∗-∗ ?Goal ?Goal2 ?Goal3 ?Goal4
∗ ([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, if decide (k = ?Goal2) then emp else ?Goal k y1 y2))%I. *)
iApply (big_sepL2_delete Φ).
(* This works. *)
```
For some reason Coq needs to be manually given `Φ` here. That should not be the case.
The only difference between the lemma statement and the goal is an eta-expansion of `Φ`.I just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failure: iApply: cannot apply
(([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, ?Goal k y1 y2)
∗-∗ ?Goal ?Goal2 ?Goal3 ?Goal4
∗ ([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, if decide (k = ?Goal2) then emp else ?Goal k y1 y2))%I. *)
iApply (big_sepL2_delete Φ).
(* This works. *)
```
For some reason Coq needs to be manually given `Φ` here. That should not be the case.
The only difference between the lemma statement and the goal is an eta-expansion of `Φ`.https://gitlab.mpi-sws.org/iris/iris/-/issues/415Tracking issue for append-only list RA2021-06-17T18:41:07ZRalf Jungjung@mpi-sws.orgTracking issue for append-only list RAThis is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Do we really want notation for the mono_list algebra elements? The main "pro" reasin here is that `dfrac` otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation
and add them on-demand.
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use.
* Do a solid review of the API surface.This is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Do we really want notation for the mono_list algebra elements? The main "pro" reasin here is that `dfrac` otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation
and add them on-demand.
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/414Tracking issue for monotone RA2021-05-07T08:49:48ZRalf Jungjung@mpi-sws.orgTracking issue for monotone RAThis is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* How should the RA be called? `monotone` is a very general term, it would be good to find something more specific. Currently it is called `mra` which is short but cryptic. `principal` should then likely become `mra_principal` and all lemmas be prefixed with `mra` as well.
* Do a solid review of the API surface.
Cc @amintimany @robbertkrebbersThis is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* How should the RA be called? `monotone` is a very general term, it would be good to find something more specific. Currently it is called `mra` which is short but cryptic. `principal` should then likely become `mra_principal` and all lemmas be prefixed with `mra` as well.
* Do a solid review of the API surface.
Cc @amintimany @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/413Better errors when tactic fails to automatically resolve some side-condition2021-07-22T12:54:29ZRalf Jungjung@mpi-sws.orgBetter errors when tactic fails to automatically resolve some side-condition@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-condition; we could introduce something like
```
Definition pm_error (s : string) := False
```
and add instances with `error "foo"` as their side-condition; together with some support in `iSolveSideCondition` this could be used to then show better, instance-specific error messages when `iMod` fails.
2. We could add a new typeclass like `ElimModalError` that is used to compute an error message when `ElimModal` failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-condition; we could introduce something like
```
Definition pm_error (s : string) := False
```
and add instances with `error "foo"` as their side-condition; together with some support in `iSolveSideCondition` this could be used to then show better, instance-specific error messages when `iMod` fails.
2. We could add a new typeclass like `ElimModalError` that is used to compute an error message when `ElimModal` failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.https://gitlab.mpi-sws.org/iris/iris/-/issues/412Use dfrac everywhere2021-04-23T12:47:13ZRalf Jungjung@mpi-sws.orgUse dfrac everywhere`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [ ] `algebra.lib.gmap_view`
* [ ] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [ ] `algebra.lib.gmap_view`
* [ ] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.https://gitlab.mpi-sws.org/iris/iris/-/issues/411Taking ∃ out of ▷ without Inhabited, more easily2021-04-29T09:25:44ZYusuke MatsushitaTaking ∃ out of ▷ without Inhabited, more easilyIn Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If we use the lemma `later_exist_except_0` instead, we get `▷ Φ x` without having `Inhabited A`, under the `◇` modality.
In Iris we are often under the `◇` modality because the update modality `|=>` contains `◇`.
I hope the operation of taking `∃x` out of `▷` without `Inhabited` becomes easier to use.
One possibility is to let Iris Proof Mode apply `later_exist_except_0` when the goal is under the `◇` modality.In Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If we use the lemma `later_exist_except_0` instead, we get `▷ Φ x` without having `Inhabited A`, under the `◇` modality.
In Iris we are often under the `◇` modality because the update modality `|=>` contains `◇`.
I hope the operation of taking `∃x` out of `▷` without `Inhabited` becomes easier to use.
One possibility is to let Iris Proof Mode apply `later_exist_except_0` when the goal is under the `◇` modality.https://gitlab.mpi-sws.org/iris/iris/-/issues/410Modality for `Timeless`2021-04-19T07:51:21ZRalf Jungjung@mpi-sws.orgModality for `Timeless`We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/407Tracking issue for list RA2021-03-17T11:50:01ZRalf Jungjung@mpi-sws.orgTracking issue for list RAThis is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.This is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.