Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-04-19T16:05:33Zhttps://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/88More convenient destruct of pure hypotheses2020-04-07T07:01:25ZRalf Jungjung@mpi-sws.orgMore convenient destruct of pure hypothesesIt is currently pretty annoying to destruct things into the pure (Coq) context, because the assertions cannot be named. This should be fixed.
One somewhat hack-ish option would be to do this the ssreflect style. So `iDestruct ... as "...It is currently pretty annoying to destruct things into the pure (Coq) context, because the assertions cannot be named. This should be fixed.
One somewhat hack-ish option would be to do this the ssreflect style. So `iDestruct ... as "[% %]"` would put two things onto the goal stack, and one would follow this tactic by `=>H1 H2` to give them names. This is somewhat non-local, but OTOH it lets us use the full power of ssreflect intro patterns.
Another option would be to somehow solve the "cannot convert string to ident"-problem, and then support patterns of the form `%H`. This will require a plugin to work in Coq 8.6, which makes it really hard to support Windows (as far as I can tell). Also, I suppose currently `%H` is parsed just like `% H`? So there would be a backwards compatibility problem when `%` starts to behave like `#` (i.e., being a modifier on the following name). We could mitigate that by detecting uses of `%H` right now and warning about them (or erroring immediately?).https://gitlab.mpi-sws.org/iris/iris/-/issues/86CoPset finite decomposition into singletons2017-05-19T15:20:29ZHai DangCoPset finite decomposition into singletonsI'm working with a proof that requires unlimited tokens, which leads me to use the disjoint union `CoPset` cmra.
In a specific subproof I need to split a finite set `X : gset positive` of tokens into singletons:
`own γ (CoPset $ of_gs...I'm working with a proof that requires unlimited tokens, which leads me to use the disjoint union `CoPset` cmra.
In a specific subproof I need to split a finite set `X : gset positive` of tokens into singletons:
`own γ (CoPset $ of_gset X) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]}) `
With `big_opS_commute1` I can get
`own γ ([⋅ set] i ∈ X, CoPset $ of_gset {[i]}) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]})`
And then I only need to show that
`CoPset $ of_gset X ≡ [⋅ set] i ∈ X, CoPset $ of_gset {[i]}`,
which currently there seems to be no easy way to solve.
Is there an induction principle for gset's, or any way to solve this?https://gitlab.mpi-sws.org/iris/iris/-/issues/85Proof mode goals in empty context cannot be distinguished from Coq goals2017-05-19T15:20:29ZRobbert KrebbersProof mode goals in empty context cannot be distinguished from Coq goals@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We...@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We could add some special symbol to the proof mode notation with the empty context? Any suggestions?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/84iDestruct on non-existing name yields "no matching clause for match"2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgiDestruct on non-existing name yields "no matching clause for match"Title says it all. Goal state:
```
============================
"Hincl" : type_incl ty1 ty2
"Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
"Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
"Hsincl" :...Title says it all. Goal state:
```
============================
"Hincl" : type_incl ty1 ty2
"Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
"Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
"Hsincl" : ∀ (κ0 : lft) (tid0 : thread_id) (l0 : loc),
ty_shr ty1 κ0 tid0 l0 -∗ ty_shr ty2 κ0 tid0 l0
--------------------------------------□
"Hshr" : ty_shr (rc ty1) κ tid l
--------------------------------------∗
ty_shr (rc ty2) κ tid l
```
Tactic: `iDestruct "Hst" as (??) "H".`
Error: `Error: No matching clauses for match.`https://gitlab.mpi-sws.org/iris/iris/-/issues/80More precise error message on missing hypothesis2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMore precise error message on missing hypothesisCurrently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found ...Currently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found (while actually, only some of them have not been found). It is also not as useful as the error would be if it would name which hypothesis has not been found.
I assume spec patterns have the same issue.https://gitlab.mpi-sws.org/iris/iris/-/issues/79Make iSplit work below existentials?2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMake iSplit work below existentials?I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; f...I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; first done.`. This works because some part of what is below the existential does not depend on the witness.
Now I wonder, would it make sense for `iSplit` to work in this case (giving me ` ⌜#l = #l⌝` and `∃ x : vec val m, ▷ l ↦∗ x` as goals)? The rewrite I did above is not very discoverable, but neither is the `iSplit`. What do you think? @jjourdan @robbertkrebbers
(You may wonder why I have things under the existential that do not depend on the witness. The reason is that lemmas of the form `∃ x y z, P` work much better with the proofmode, because I an do a single `iDestruct ... as (x y z) ...`. If I pushed the existential down, destructing things would become much more annoying.)https://gitlab.mpi-sws.org/iris/iris/-/issues/77Have iNext "pull" laters out from below other operators.2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgHave iNext "pull" laters out from below other operators.Let's say I have a goal of the shape `∃ x, ▷ Q x` (and the type of `x` is inhabited). I also have an assumption below a later. I want to strip the later from the assumption, which is okay because our goal is equivalent to `▷ ∃ x, Q x`. C...Let's say I have a goal of the shape `∃ x, ▷ Q x` (and the type of `x` is inhabited). I also have an assumption below a later. I want to strip the later from the assumption, which is okay because our goal is equivalent to `▷ ∃ x, Q x`. Currently, I have to do `rewrite -uPred.later_exist` for this.
First of all, I am wondering why `iApply uPred.later_exist` doesn't work in this context. Secondly, it'd be nice if `iNext` could also "pull" laters out of the goal if there's not yet a top-level later.https://gitlab.mpi-sws.org/iris/iris/-/issues/76`iDestruct` for big ops2017-05-19T15:20:29ZRobbert Krebbers`iDestruct` for big opsTogether with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ ...Together with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x
we could use `iDestruct "H" as "[H1 H2]"` to turn it into:
H1 : Φ 0 y
H2 : [∗ list] k ↦ x ∈ l, Φ (S k) x
Although this is not particularly difficult to implement (it just requires one to declare suitable `IntoAnd` instances), it gives rise to some potential ambiguity, namely, what is going to happen when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x ∗ Ψ k x
Will it split through the cons, or through the star inside of the predicate in the big op?
Currently, it will split through the ∗ due to the instance `into_and_big_sepL`. Declaring yet another `IntoAnd` instance for the `cons` case is a bad idea, as it will give rise to the ambiguity above, and we end up with tactics that will behave unpredictably.
However, I think that the `cons` instance would be much more useful than the `∗` instance, hence I propose to drop the current `∗` instance, and instead declare instances for `cons` (and possibly `app`, which does not lead to ambiguity).https://gitlab.mpi-sws.org/iris/iris/-/issues/75Build any merge request on the CI2017-05-19T15:20:29ZRobbert KrebbersBuild any merge request on the CICurrently, I have to change the `.gitlab-ci.yml` in the branch corresponding to the merge request. This is a bit cumbersome, because I have to be careful to not merge the commit in which I changed `.gitlab-ci.yml` when merging into maste...Currently, I have to change the `.gitlab-ci.yml` in the branch corresponding to the merge request. This is a bit cumbersome, because I have to be careful to not merge the commit in which I changed `.gitlab-ci.yml` when merging into master.
Would it be possible to automatically build any branch corresponding to an MR on the CI?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/74iNext does not strip off both laters from ▷ P ∗ ▷ Q2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgiNext does not strip off both laters from ▷ P ∗ ▷ QI would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```I would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/73Specialization patterns syntax extensions2017-05-19T15:20:29ZRobbert KrebbersSpecialization patterns syntax extensionsThere have been some requests to add new stuff to specialization patterns:
1. A `//` token for performing `done`. One could then write things like `[$H1 $H2 //]` or `[//]`.
2. Being able to frame in persistent specialization patterns, i...There have been some requests to add new stuff to specialization patterns:
1. A `//` token for performing `done`. One could then write things like `[$H1 $H2 //]` or `[//]`.
2. Being able to frame in persistent specialization patterns, i.e. `[# $H1 $H2]`.
3. A token, say `[$]` to solve the goal by framing, and by keeping all unused hypotheses for the subsequent goals.
However, there are some questions here:
1. I suppose we want to be able to use `//` also for pure and persistent goals. For example `[% //]` and `[# //]`.
2. What is going to happen when we do `[# H1 $H2]`. There are some obvious choices: a.) using a hypothesis without a `$` prefix is forbidden b.) ignore all hypotheses that are not prefixed with a `$` (there is no need to select hypotheses, you get all anyway, since the goal is persistent) c.) prune the context that goal.
3. What to frame? Just the spatial hypotheses, or everything (including the persistent ones)?
Anyone some ideas? I would like to have a syntax that is not too FUBARed.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/72Support `iCombine "H1 H2 ..." as "Hx"`2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgSupport `iCombine "H1 H2 ..." as "Hx"`It'd be nice if `iCombine` supported passing a single string of space-separated hypothesis instead of insisting on two strings, each being a single name. Combining more than two hypothesis would be done by folding.It'd be nice if `iCombine` supported passing a single string of space-separated hypothesis instead of insisting on two strings, each being a single name. Combining more than two hypothesis would be done by folding.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/70`wp_apply` cannot deal with curried lemmas2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.org`wp_apply` cannot deal with curried lemmasThe `wp_apply` tactic was written in a time when all our lemmas were uncurried. It always distributes all the resources of the current context to one of the goals that it creates, not leaving any control to the user. I think we need some...The `wp_apply` tactic was written in a time when all our lemmas were uncurried. It always distributes all the resources of the current context to one of the goals that it creates, not leaving any control to the user. I think we need something like `wp_apply with "<spec pattern>"` to accommodate curried lemmas.
See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/lang/spawn.v#L77> and <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/typing/unsafe/cell.v#L165> for some examples.https://gitlab.mpi-sws.org/iris/iris/-/issues/69Make `done` solve the goal when one of the Iris hypothesis is `False`2017-05-19T15:20:29ZJacques-Henri JourdanMake `done` solve the goal when one of the Iris hypothesis is `False`As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.https://gitlab.mpi-sws.org/iris/iris/-/issues/68iSpecialize should work even if the wand is under a later.2017-05-19T15:20:29ZJacques-Henri JourdaniSpecialize should work even if the wand is under a later.In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/67iAssert does not support destructing existentials2017-05-19T15:20:29ZJacques-Henri JourdaniAssert does not support destructing existentialsIt seems like I cannot use something like:
```
iAssert (∃ a, P a) with "[]" as (a) "H".
```It seems like I cannot use something like:
```
iAssert (∃ a, P a) with "[]" as (a) "H".
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/65Wish: Prelude support for currying (and other operations) on gmap.2017-05-19T15:20:29ZJannoWish: Prelude support for currying (and other operations) on gmap.The following operations would (or could) be quite useful in my planned clean-up of iGPS:
1. Converting `gmap A (gmap B C)` to `gmap (A* B) (C)` and vice versa.
1. Converting `gmap A B` to `gmap A (A * B)` by copying the argument.
1. C...The following operations would (or could) be quite useful in my planned clean-up of iGPS:
1. Converting `gmap A (gmap B C)` to `gmap (A* B) (C)` and vice versa.
1. Converting `gmap A B` to `gmap A (A * B)` by copying the argument.
1. Converting `gmap A B` as a `gset (A * B)` (possibly by simply adding a ElemOf instance and corresponding lemma).
As Robbert already mentioned to me, these things probably should be generalized. I think there is a general map-filter function lurking in there somewhere. One that gives access to both the key and the value and returns and optional results which is used for the new gmap. I might be wrong though.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/63gmultiset.gmultiset_eq_dec applied too eagerly?2017-05-19T15:20:29ZJannogmultiset.gmultiset_eq_dec applied too eagerly?I don't have time to debug this in more detail so I am just going to dump a representative trace here. Without exception, all my diverging type class searches (of which I have a few per hour) eventually look like this one:
[trace.txt](/...I don't have time to debug this in more detail so I am just going to dump a representative trace here. Without exception, all my diverging type class searches (of which I have a few per hour) eventually look like this one:
[trace.txt](/uploads/1fad04b1b2cb32d92e41f976f8853f1f/trace.txt)
(Just in case somebody actually looks at it: the piece of code you can see in line 1 doesn't actually make any sense, I think.)https://gitlab.mpi-sws.org/iris/iris/-/issues/62Specialization (iApply/iMod) often diverges on missing *2017-11-16T09:36:42ZRalf Jungjung@mpi-sws.orgSpecialization (iApply/iMod) often diverges on missing *When specializing a lemma that contains Iris-level universal quantifiers, if I forget to add the `*` to the pattern, the tactic frequently diverges. This is very frustrating as it is not even clear what's wrong, or where the `*` has to b...When specializing a lemma that contains Iris-level universal quantifiers, if I forget to add the `*` to the pattern, the tactic frequently diverges. This is very frustrating as it is not even clear what's wrong, or where the `*` has to be added.
If you want, I can create a minimal example. Right now, one way to see this is to remove the `*` from the `iMod` in `weakestpre.wp_atomic`, line 172.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/61iLöb doesn't work in the empty context.2017-05-19T15:20:29ZJannoiLöb doesn't work in the empty context.As witnessed by the following example.
```
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Se...As witnessed by the following example.
```
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*".
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
Proof.
Fail (iLöb as "IH" forall (e Closed0)).
iAssert (True)%I as "T"; [by admit|].
(iLöb as "IH" forall (e Closed0)).
Abort.
```
I guess with the new unified handling of reverting hypotheses this probably applies to other tactics as well.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/90Strong persistent framing and saved_prop_agree2017-09-12T14:34:23ZRobbert KrebbersStrong persistent framing and saved_prop_agreeProblem reported by @haidang in #71:
> If I have in my persistent context `Hx: saved_prop_own γ x` and `Hy: saved_prop_own γ y`, then `iDestruct (saved_prop_agree with "[$Hx $Hy]") as "Eq"` gives `x = x`. To get the right result, instea...Problem reported by @haidang in #71:
> If I have in my persistent context `Hx: saved_prop_own γ x` and `Hy: saved_prop_own γ y`, then `iDestruct (saved_prop_agree with "[$Hx $Hy]") as "Eq"` gives `x = x`. To get the right result, instead I need to instantiate `saved_prop_agree _ x y`, which is less convenient.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/91Generalizing the Proofmode2018-07-13T08:40:30ZJannoGeneralizing the ProofmodeI am sure I have this request this issue with almost everyone already but let me summarize it here again:
In our iGPS work, we work with monotone (Iris) predicates over a type called views - though the actual type doesn't matter much. We...I am sure I have this request this issue with almost everyone already but let me summarize it here again:
In our iGPS work, we work with monotone (Iris) predicates over a type called views - though the actual type doesn't matter much. We call these predicates vPreds. In spirit, all proofs are done with respect to a "current" view which changes when taking a step – not unlike step indices, I think. However, we currently have to manually upgrade the view of our assumptions to the new view after taking a step to achieve coherence between the goal and the assumptions.
Since I am about to start another development with the same setup I wanted to gather information on how to hide the views from the potential users of our logic. I talked to @jjourdan about this and he suggested a bunch of hacky steps that could potentially make the views disappear. The approach uses a typeclasse to represent the current view of the proof. However, I think we will still suffer from some inherent drawbacks: we have to redefine connectives, the proof mode syntax, and probably many more things. If possible I would prefer a more principled solution.
Here's an incomplete list of pain points with our current setup:
1. Views show up in the proof context.
1. Views show up in the proof script. (We can mostly hide them behind custom tactics and underscores, though.)
1. We define what amounts to an incomplete copy of the uPred scope to get all the logical connectives on vPreds.
1. Because we do not want to redefine every last bit (especially lemmas) of uPred, we sometimes unfold away all the vPred stuff. This results in scope chaos, with annotations %I and %VP everywhere.
1. Once we unfold, refolding is almost impossible.
1. The typeclasses for the proofmode are not always smart enough to see through our definitions and recognize the underlying uPreds. (I think this is largely fixed but I don't quite remember what the exact issue were. They might pop up again in different circumstances)
I think that these issues could be fixed by making the proofmode more general. Maybe it would be parametrized by a BI with the more intricate parts (viewshift stuff?) parametrized by additional assumptions on the BI. Maybe different parts of it would have different parameters. I haven't thought a lot about the specifics. What I think this doesn't immediately fix is the interaction between two different logics like vPred and uPred: How does one make the proofmode aware of the two different levels? Can we get rid of the need to switch between the two logics entirely or should we try to make it possible to switch between them inside proofs?
I would love to hear your feedback on this. Maybe there are other ways of going about this? @robbertkrebbers, I know you thought about this as well. What is the best approach in your view?
/cc @haidanghttps://gitlab.mpi-sws.org/iris/iris/-/issues/92Discussion: Better(?) Logically-Atomic Triples2018-07-13T15:54:13ZJannoDiscussion: Better(?) Logically-Atomic TriplesHey everyone,
I am doing some groundwork on logical atomicity for weak memory and I got annoyed by the "current" definition of atomic triples:
1. The quantification over the "real" precondition P seems unnecessary.
2. The box around the...Hey everyone,
I am doing some groundwork on logical atomicity for weak memory and I got annoyed by the "current" definition of atomic triples:
1. The quantification over the "real" precondition P seems unnecessary.
2. The box around the shift is an artifact of working directly with (persistent) triples.
This is the reference definition of atomic triple (taken from @zhangz's iris-atomic@13900169bafb6b6ef1d091236dba493eaa25cc95):
```coq
∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
α x ∗
((α x ={Ei, Eo}=∗ P) ∧
(∀ v, β x v ={Ei, Eo}=∗ Q v))
) -∗ {{ P }} e @ ⊤ {{ Q }}.
```
I propose the following change:
```coq
atomic_shift Eo Ei α β Φ :=
|={Eo,Ei}=> ∃ x : A,
α x ∗
((α x ={Ei,Eo}=∗ ▷ atomic_shift Eo Ei α β Φ) ∧
∀ y, β x y ={Ei,Eo}=∗ Φ y).
atomic_wp Eo Ei α β := ∀ Φ, atomic_shift Eo Ei α β Φ -∗ WP e @ Eo { Φ }
```
It should be easy enough to derive a notion of logically-atomic triples (as opposed to weakestpre) the same way we derive normal triples.
I did some initial testing by porting iris-atomic/atomic_incr.v to this definition. Apart from some inconveniences regarding boxes in the client (orthogonal to logically-atomic triples; just a proof setup problem), the proof of the spec and the client remain mostly the same. One additional (albeit entirely trivial) Löb induction had to be introduced in the client to prove the atomic shift. The spec proof already had a Löb induction and so will almost any other proof of that kind I think.
You can see the changes to the proof here: janno/iris-atomic@06d9dc7d. The definition is here: janno/iris-atomic@ba66f8bd.
Before I continue to work with this new definition in my own development I would like to gather feedback. What does everyone think of it?
I am specifically worried about examples that somehow manage to run out of steps and thus cannot get rid of the `▷` modality. I can't imagine what those would look like but they might exist. Additionally, the added complexity of requiring `iLöb` in client proofs may be considered a substantial disadvantage of this definition by some.
P.S.: This is orthogonal to (and thus hopefully compatible with) the work on using telescopes to represent an arbitrary number of binders in atomic triples. I made some progress on that, too. But it's not done.https://gitlab.mpi-sws.org/iris/iris/-/issues/93Using wp_ tactics without making every tiny step a function is super slow sol...2019-02-15T10:36:40ZGhost UserUsing wp_ tactics without making every tiny step a function is super slow solely because Coq has to keep proving this Closed obligationWhich would be fine, except that there is no good way right now to prove closed-ness under a binder without knowing string literals for the variable names.
Concrete example:
```coq
Definition big_blob_of_code x :=
(* huge blob of...Which would be fine, except that there is no good way right now to prove closed-ness under a binder without knowing string literals for the variable names.
Concrete example:
```coq
Definition big_blob_of_code x :=
(* huge blob of code here *)%E.
Definition foo: val :=
(λ: [ "x"; "y" ], big_blob_of_code "x" + big_blob_code "y").
```
I don't want big_blob_of_code to be a function (because it isn't in the source code, and I'd like to actually verify foo as written rather than some other thing). However, Coq takes far too long to execute `wp_rec` on my `foo`-like thing, and it only gets worse the more times it is called. It also requires an irritating number of rewrites. There may be some ways around this if you happen to have some closed values somewhere up the stack and use `Notation` for previous ones, with a typeclass instance for `Closed` for those functions, but even that is highly annoying, and proving `Closed` for any of the lower-level functions doesn't really work because of the way `solve_closed` is defined (and according to Janno, probably just can't work at all).
I don't really care what solution this has, just that there is one.https://gitlab.mpi-sws.org/iris/iris/-/issues/94iInv without Hclose2018-07-13T15:55:27ZRalf Jungjung@mpi-sws.orgiInv without HcloseI've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv...I've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv.
Particularly, I suggest that we get rid of the last parameter of iInv (the name of the "Hclose"), and instead have it add that as an obligation to the postcondition. So, if the goal starts out being `WP e {{ v, Q }}`, then when opening `inv N I` it becomes `WP e {{ v, \later I * Q }}`. Similar things happen when the goal is a view shift.
@robbertkrebbers @jjourdan what do you think? How hard would it be to implement this? We'd probably want a new typeclass generalizing things that can be in the goal when doing iInv. I fear that typeclass will be much like the infamous "frame shift assertions"...https://gitlab.mpi-sws.org/iris/iris/-/issues/95Introduce implication if premise is persistent2017-08-24T08:49:51ZRalf Jungjung@mpi-sws.orgIntroduce implication if premise is persistentCurrently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the g...Currently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the goal is `box P -> Q`, introducing should be possible even for a non-empty spatial context.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/96Spurious whitespace in proofmode notations2017-08-24T14:09:21ZRobbert KrebbersSpurious whitespace in proofmode notationsThis is probably a result of !59. For example:
```coq
Lemma test_iIntros_persistent P Q `{!PersistentP Q, !PersistentP R} :
(P → Q → R → P ∗ Q)%I.
Proof. iIntros "H1 H2 #H3".
```
Coq now displays:
```
_______________________________...This is probably a result of !59. For example:
```coq
Lemma test_iIntros_persistent P Q `{!PersistentP Q, !PersistentP R} :
(P → Q → R → P ∗ Q)%I.
Proof. iIntros "H1 H2 #H3".
```
Coq now displays:
```
______________________________________(1/1)
"H3" : R
--------------------------------------□
"H1" : P
"H2" : Q
--------------------------------------∗
P ∗ Q
```
So, as you can see, the printing of each context starts with a spurious whitespace.
I don't know whether this is a Coq bug, or a bug in our notation. @jung any idea?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/97`iIntros.` should always enter proof mode2017-09-27T08:45:18ZRalf Jungjung@mpi-sws.org`iIntros.` should always enter proof mode```
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
``````
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/98`iIntros.` fails to introduce `True`2017-09-27T08:45:17ZRalf Jungjung@mpi-sws.org`iIntros.` fails to introduce `True````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
``````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/99iNext does not strip off later below existential2017-10-02T13:34:05ZRalf Jungjung@mpi-sws.orgiNext does not strip off later below existential```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below con...```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below conjunctions, but not below existentials.https://gitlab.mpi-sws.org/iris/iris/-/issues/100Proof mode notation broken depending on import order2017-11-11T09:19:19ZRalf Jungjung@mpi-sws.orgProof mode notation broken depending on import orderIt is a long-standing issue that sometimes, depending on the order of re-exports and imports, the proof mode notation is broken. I finally decided to minimize this, and you can find the result in the [`ipm-notation-broken` branch](https...It is a long-standing issue that sometimes, depending on the order of re-exports and imports, the proof mode notation is broken. I finally decided to minimize this, and you can find the result in the [`ipm-notation-broken` branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/ipm-notation-broken). I first thought this is a Coq bug, but now I am not so sure anymore: We do have different notations in the same scope that lead to printing being ambiguous.
Namely, we have
```
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
(at level 99, Q at level 200, right associativity) : C_scope.
```
and
```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) ⊢ Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
```
We seem to be relying on a guarantee that if one notation is strictly more specific than another one, it will have higher priority. Does Coq claim to have such a guarantee?
Maybe one possible solution would be to move the proof mode notations into a different scope, and have `iStartProof` introduce that scope (i.e., turn the goal into `(...)%ProofMode`).Iris 3.1Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/101Make Iris run in jsCoq2017-11-30T09:53:53ZRalf Jungjung@mpi-sws.orgMake Iris run in jsCoqCurrent status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert al...Current status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert already mentioned that he wanted to look into that.https://gitlab.mpi-sws.org/iris/iris/-/issues/82Consider adding a "strong" always modality2018-01-31T09:21:27ZRalf Jungjung@mpi-sws.orgConsider adding a "strong" always modalityThe idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default...The idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default should be not to add anything unless we really need it -- and we got pretty far without the strong always.
So what do we have that this would enable? (I am writing "SB" for the strong box below.)
* Propositional extensionality. Not sure how useful that would be though.
* `(|=> SB P) -> SB P`, i.e. basic updates can be removed around the strong box. That seems pretty powerful, but the only application we have so far is to make the adequacy lemma nicer to state (no more "nested laters and basic updates", but just "nested laters").
* It would be possible to have the "core of a proposition" in a clean way, defined as `∀ Q, SB (Q -> □Q) -> SB (P -> Q) → □ Q`. This works because `SB P -> □ Q` is persistent.
@robbertkrebbers I seem to remember you saying that one of the Iris-based papers added the strong box. Why again did they need it?
I am not convinced that the above is enough of a reason to add the box to the core. In particular, I feel like it would be non-trivial to explain to people why we have two box-like modalities.https://gitlab.mpi-sws.org/iris/iris/-/issues/81Let iAlways clear the spatial context2017-10-27T12:33:40ZRalf Jungjung@mpi-sws.orgLet iAlways clear the spatial contextRight now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is simil...Right now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is similar to the difference between `iIntros "!>"` and `iNext` -- the latter may affect the context, the former will not. Furthermore, this is backwards compatible because iAlways will now only succeed in strictly more cases.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/71Framing in Disjunctions2019-11-01T13:20:31ZJannoFraming in Disjunctions@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize t...@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize that such an instance potentially leads to unsolvable goals more often than any of the existing framing instances. So this should probably not be the default behavior of `iFrame`. Nonetheless, the functionality was extremely convenient in some places. Often, disjunctive goals could easily be closed by framing out a bunch of resources and closing the goal with a `by` prefix or a separate `done`. No `iLeft` or `iRight` was needed.
I wonder if Iris could still benefit from such rules by adding a marker in the syntax for `iFrame`, e.g. `iFrame "!H"`, which applies the more reckless disjunction framing rules. The same could be applied for specialization patterns with something like `$!H`.
What do you think?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/66Use a "settings" file for setting options within the project2020-09-10T17:37:08ZRalf Jungjung@mpi-sws.orgUse a "settings" file for setting options within the projectFollowing a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to d...Following a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to discuss is the name of that file... I suggest putting it into the root, i.e. sth. like `theories/options.v`.https://gitlab.mpi-sws.org/iris/iris/-/issues/64Destruct patterns: Support -> and <- (at least) for pure Coq equalities, and ...2017-10-27T13:17:57ZRalf Jungjung@mpi-sws.orgDestruct patterns: Support -> and <- (at least) for pure Coq equalities, and maybe injection patternsIn lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; i...In lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %[= ->]`, i.e., there is an additional injection applied. Any way we could also get that in the proof mode? Maybe even using the "injective" typeclass so that it doesn't have to be the constructor of an inductive type (however, of course it'd also have to support all constructors, so it can't rely just on that typeclass).Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/58Proofmode with Coq binders, and without strings2019-11-01T11:15:16ZRalf Jungjung@mpi-sws.orgProofmode with Coq binders, and without strings@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust sig...@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust significantly. We could also not use strings, which may even help with speed. (Well, strings are not very efficient in Coq -- but I kind of doubt that's out bottleneck currently.)
I'll leave it to Janno to explain the idea, because I would totally screw that up.
I any case, even if we want to go for this, this is a long-term thing... definitely post-3.0, and definitely breaking everybody using Iris horribly (if we don't just keep the string-based stuff around).https://gitlab.mpi-sws.org/iris/iris/-/issues/49Improve support of simplify_option_eq (and simplify_map_eq?) for setoids2017-11-13T18:13:54ZRalf Jungjung@mpi-sws.orgImprove support of simplify_option_eq (and simplify_map_eq?) for setoidsSome testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Some testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/48Unify `iNext` and `iModIntro` (and more?)2018-07-13T15:56:18ZRobbert KrebbersUnify `iNext` and `iModIntro` (and more?)These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I t...These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I think this should not be too difficult.
See also the discussion as part of commit 9ae19ed5.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/42Authoritative with fraction2019-06-06T11:07:12ZRalf Jungjung@mpi-sws.orgAuthoritative with fractionThe authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to...The authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to be brought together to change it. I just realized that this could be supported by a fairly small change in the authoritative CMRA, namely to replace `Ex(M)` by `Frac * Ag(M)`:
```
Auth(M) := { (x, a) \in (Frac * Ag(M))^? * M | ...}
```
The interface would then change to allow a fraction in the `●` notation (and once we have an infrastructure for "assertions that can be split at a fraction", it could be registered there). What do you think?
Cc @janno @robbertkrebbers @jjourdanRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/36STSs: Consider changing the def. of frame-steps2019-11-01T13:16:11ZRalf Jungjung@mpi-sws.orgSTSs: Consider changing the def. of frame-stepsJeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification...Jeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.https://gitlab.mpi-sws.org/iris/iris/-/issues/21iDestruct and iPureIntro2019-11-01T13:14:54ZGhost UseriDestruct and iPureIntroI recently bumped into a scenario like this:
```
H : heapN ⊥ N
o', n' : Z
============================
"~" : heap_ctx
"~1" : inv N
(∃ o n : Z,
(l ↦ (#o, #n) ∧ ■ (o < n))
★ (au...I recently bumped into a scenario like this:
```
H : heapN ⊥ N
o', n' : Z
============================
"~" : heap_ctx
"~1" : inv N
(∃ o n : Z,
(l ↦ (#o, #n) ∧ ■ (o < n))
★ (auth_own γ {[o := ()]} ∨ own γ (Excl ()) ★ R))
"IH" : (locked l R -★ R -★ Φ #()) -★ WP acquire #l {{ v, Φ v }}
--------------------------------------□
"H2" : ■ (o' < n')
--------------------------------------★
■ (o' < n' + 1)
```
To prove this, I have to first `iDestruct "H2" as "%"` to move `o' < n'` to Coq context, then I can `iPureIntro` and do the following proof.
My problem is, will it be good to let `iPureIntro` (or invent something on top of it) to handle the `iDestruct` here for me?
Or even more convenient, it is possible to apply pure theorems directly in this context?
Thanks!https://gitlab.mpi-sws.org/iris/iris/-/issues/13Bring back unsafe triples2018-02-02T19:07:29ZRalf Jungjung@mpi-sws.orgBring back unsafe triplesThey were lost in the transition from Iris 1.1 to Iris 2.0. @swasey needs them.They were lost in the transition from Iris 1.1 to Iris 2.0. @swasey needs them.https://gitlab.mpi-sws.org/iris/iris/-/issues/102`solve_proper` having troubles proving non-expansiveness2017-10-10T11:50:17ZDan Frumin`solve_proper` having troubles proving non-expansivenessIn the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simp...In the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simpl; f_equiv)` to automatically discharge the obligations.
Is there a reason why this simplification is not happening in `solve_proper_core`?
Is it for the performance reasons?
```coq
From iris.heap_lang Require Import lang proofmode tactics notation.
Section linkedlist.
Context `{heapG Σ}.
Program Definition pre_isLinkedList : (valC -n> iProp Σ) -n> (valC -n> iProp Σ) :=
λne P v, (⌜v = InjLV #()⌝
∨ ∃ (h t : val) (l : loc),
⌜v = InjRV (PairV h #l)⌝
∗ l ↦ t
∗ ▷ (P t))%I.
Solve Obligations with solve_proper_core ltac:(fun _ => simpl; f_equiv).
End linkedlist.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/103Find a better name for iMod2017-11-24T15:57:13ZRalf Jungjung@mpi-sws.orgFind a better name for iModWe do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`...We do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`. `iUpd` is my personal favorite. I know that the tactic supports other modalities, but 99,9% of the time it is used to eliminate some form of an update. The name is more informative than `iMod`, and not more wrong.
`iRun` is slightly less informative, but also less wrong: The tactic does bind in a monad, which can be seen as "running the computation".
Cc @robbertkrebbers @jjourdan
EDIT: All right, I stand corrected on the "wrong" part. Sorry for that. It is still uninformative.https://gitlab.mpi-sws.org/iris/iris/-/issues/105Add some theory about the interaction of plainly and fancy updates2017-11-01T23:47:30ZRalf Jungjung@mpi-sws.orgAdd some theory about the interaction of plainly and fancy updates@amintimany has some theory there, we should get the reusable bits upstream.@amintimany has some theory there, we should get the reusable bits upstream.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/106Iris 3.12018-01-09T15:55:25ZRalf Jungjung@mpi-sws.orgIris 3.1In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels o...In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels of `_ ;; _` and `_ <- _ ;; _`
* [ ] Make sure all our CI'd reverse dependencies build with master.Iris 3.1https://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/108iIntros on pure implications stopped working2017-10-28T21:10:55ZRalf Jungjung@mpi-sws.orgiIntros on pure implications stopped workingThe following proof script used to work, but does not any more:
```
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
```
This is probably a regression of the typeclass-based iIntros?The following proof script used to work, but does not any more:
```
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
```
This is probably a regression of the typeclass-based iIntros?Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/109Post-Iris 3.12018-06-05T08:05:48ZRalf Jungjung@mpi-sws.orgPost-Iris 3.1After Iris 3.1 is released:
* [x] Switching timing measurements to the Coq 8.7 build.
* [x] Drop support for Coq 8.6?
* [x] Enable `test_iIntros_pure`.
* [x] Drop opam dependency on ssreflect, use the one embedded in Coq instead.
Are t...After Iris 3.1 is released:
* [x] Switching timing measurements to the Coq 8.7 build.
* [x] Drop support for Coq 8.6?
* [x] Enable `test_iIntros_pure`.
* [x] Drop opam dependency on ssreflect, use the one embedded in Coq instead.
Are there other work-arounds we can remove or new features we want to make use of?https://gitlab.mpi-sws.org/iris/iris/-/issues/110Import OCPL's heap_lang logic?2018-07-13T15:57:18ZDavid SwaseyImport OCPL's heap_lang logic?From !37:
> Please take a look at the heap interface in Fig. 2 of my OCPL paper (off my home page) or, more informatively, at theories/heap_lang/heap.v in the OCPL Coq development. I propose replacing the current heap_lang logic with th...From !37:
> Please take a look at the heap interface in Fig. 2 of my OCPL paper (off my home page) or, more informatively, at theories/heap_lang/heap.v in the OCPL Coq development. I propose replacing the current heap_lang logic with the strictly more expressive OCPL, and adding the OCPL examples to heap_lang/lib and tests/.
Ralf asked if I have a git repo. Yes. I will create a merge request once we settle !37. (OCPL builds on !37.)David SwaseyDavid Swaseyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/111Proof mode only *mostly* works when it is transitively imported, not exported2017-11-20T14:47:41ZRalf Jungjung@mpi-sws.orgProof mode only *mostly* works when it is transitively imported, not exportedI was debugging some very strange behavior with @janno yesterday, which turned out to be the following: In iGPS, imports and exports are somewhat... messy. (To be fair, I feel that's a very common problem with Coq developments. I know n...I was debugging some very strange behavior with @janno yesterday, which turned out to be the following: In iGPS, imports and exports are somewhat... messy. (To be fair, I feel that's a very common problem with Coq developments. I know no best practices.) In particular, there are files that do `From iris.proofmode Require Import tactics`, and then other files import that file. That's enough to get notations, because they are *always* imported, ignoring the usual reexport rules. (Should we report a Coq bug about that? It does not seem necessary.) However, every since @robbertkrebbers recently disabled `Automatic Coercions Imports`, this is *not* enough to get working coercions. So, most tactics worked, but some (e.g. `iCombine`) rely on coercions and did not work.
I think we should do one of two things:
1. Make the entire proofmode work when it is just re-imported, not re-exported.
2. Make `iStartProof` fail when the proof mode is just re-imported, not re-exported.
(1) would be somewhat nicer as it means the proofmode works "more often".Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/112Make invariants and slices closed under equivalence2018-02-08T10:43:12ZRalf Jungjung@mpi-sws.orgMake invariants and slices closed under equivalenceThis has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the followi...This has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the following holds:
```coq
Lemma inv_iff P Q :
later persistently (P <-> Q) -> inv P -> inv Q.
```
I think this may be worth it, *if* it means we can simplify the definition of the lifetime logic a little bit. However, that will only be the case if we manage to also get this law for `slice`, which requires either a separate closure in `slice` (so the one in `inv` does not help), or doing the same kind of closure in `saved_prop_own` (but then, do we also want the equivalent law for `saved_pred_own`?).
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.https://gitlab.mpi-sws.org/iris/iris/-/issues/113Do not run `simpl` on user-visible goals2017-12-02T00:07:12ZRalf Jungjung@mpi-sws.orgDo not run `simpl` on user-visible goalsThe proof mode, and in particular the `wp_*` tactics, currently sometimes run `simpl` on the user's goal. That can be annoying if `simpl` misbehaves. Ideally, we should avoid running `simpl` on user goals.The proof mode, and in particular the `wp_*` tactics, currently sometimes run `simpl` on the user's goal. That can be annoying if `simpl` misbehaves. Ideally, we should avoid running `simpl` on user goals.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/114Possibly confusing naming: auth_own_valid.2019-06-06T11:06:35ZDan FruminPossibly confusing naming: auth_own_valid.I was wondering if anyone else found this a bit confusing.
The lemma `auth_own_valid` refers to two things:
- `base_logic.lib.auth.auth_own_valid` which states that `own γ (◯ a) ⊢ ✓ a`;
- `algebra.auth.auth_own_valid` which (roughly) s...I was wondering if anyone else found this a bit confusing.
The lemma `auth_own_valid` refers to two things:
- `base_logic.lib.auth.auth_own_valid` which states that `own γ (◯ a) ⊢ ✓ a`;
- `algebra.auth.auth_own_valid` which (roughly) states that `✓ (● a, ◯ b) → ✓ b`.
If you need both of those modules, then the order in which you import them is quite significant.
I guess the issue is that `auth_own` refers both to the *proposition of owning* the fragment part of the Auth algebra and to the actual fragment part of the algebra.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/115Test2017-12-08T15:54:33ZRalf Jungjung@mpi-sws.orgTestThis is an issue to test the mattermost integration. Please ignore.This is an issue to test the mattermost integration. Please ignore.https://gitlab.mpi-sws.org/iris/iris/-/issues/116A tactical for applying tactics to individual proof mode hypotheses2018-01-24T15:27:28ZRobbert KrebbersA tactical for applying tactics to individual proof mode hypothesesFor example, so that you can perform a `rewrite` or `simpl` in just one proof mode hypothesis.
Ssreflect also has such a tactical.For example, so that you can perform a `rewrite` or `simpl` in just one proof mode hypothesis.
Ssreflect also has such a tactical.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/118Notation `A -c> B` makes no sense2019-06-18T17:44:46ZRobbert KrebbersNotation `A -c> B` makes no senseThe `c` goes back to the time we solely used COFEs, now that we use OFEs, this notation makes no sense whatsoever.The `c` goes back to the time we solely used COFEs, now that we use OFEs, this notation makes no sense whatsoever.Iris 3.2https://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/120Add atomic fetch-and-add to `heap_lang`2017-12-05T19:39:19ZRobbert KrebbersAdd atomic fetch-and-add to `heap_lang`For the sake of demonstrating Iris, it is often useful to have an atomic fetch-and-add instruction (see for example my TTT talk and Derek's MFPS talk). Of course, we can implement such a thing using a `CAS` loop, but then the proof in Co...For the sake of demonstrating Iris, it is often useful to have an atomic fetch-and-add instruction (see for example my TTT talk and Derek's MFPS talk). Of course, we can implement such a thing using a `CAS` loop, but then the proof in Coq becomes quite different from the proof on paper.
Adding an atomic fetch-and-add instruction to heap_lang should be easy, and it makes sense, since many actual architectures have such an instruction.
What do you think? Are there any other common atomic instructions that we may add too? We could add something like:
```coq
AtomicBinOp (op : bin_op) (e1 : expr) (e2 : expr).
```
But it is a bit weird to use it with `LeOp`, `LtOp` or `EqOp` since those change the type of the location.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/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/126Naming bikeshed: Persistently and affinely-persistently2018-03-22T12:02:29ZRalf Jungjung@mpi-sws.orgNaming bikeshed: Persistently and affinely-persistentlyCurrently, in `gen_proofmode`, the name "persistently" and the typeclass "Persistent" do not match the notation `□`.
I think this is a great name for "the context that behaves like normal intuitionistic logic", so I think ideally we sho...Currently, in `gen_proofmode`, the name "persistently" and the typeclass "Persistent" do not match the notation `□`.
I think this is a great name for "the context that behaves like normal intuitionistic logic", so I think ideally we should call `□` "persistently" here as well, and define `Persistent P := P |- □ P`. This requires finding a new name for the modality that is in the BI interface -- the modality that allows duplication, but does not allow throwing things away. IIRC @jtassaro called this modality "relevant". That doesn't seem like the worst possible name, though "relevantly" sounds a little funny?
To be clear, I suggest keeping the name "persistent" for the `□` and the "persistent context". If we change that name, it would affect affine Iris, and I don't think we want to rename this symbol there *again*.Generalized Proofmode MergerRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/127Proofmode : pure implies and forall2017-12-21T17:32:40ZJacques-Henri JourdanProofmode : pure implies and forallA few weirdities (tested in gen_proofmode, but a few a these are probably a problem in master too):
```coq
Lemma test_forall_nondep (φ : Prop) :
φ → (∀ _ : φ, False : PROP) -∗ False.
Proof.
iIntros (Hφ) "Hφ".
Fail iSpecialize ("Hφ...A few weirdities (tested in gen_proofmode, but a few a these are probably a problem in master too):
```coq
Lemma test_forall_nondep (φ : Prop) :
φ → (∀ _ : φ, False : PROP) -∗ False.
Proof.
iIntros (Hφ) "Hφ".
Fail iSpecialize ("Hφ" with "[%]").
Fail iApply "Hφ".
Fail iSpecialize ("Hφ" $! _).
iSpecialize ("Hφ" $! Hφ); done.
Qed.
Lemma test_pure_impl (φ : Prop) :
φ → (⌜φ⌝ → False : PROP) -∗ False.
Proof.
iIntros (Hφ) "Hφ".
Fail iSpecialize ("Hφ" $! Hφ).
Fail iSpecialize ("Hφ" $! _).
Fail iApply "Hφ".
iSpecialize ("Hφ" with "[%]"); done.
Qed.
Lemma test_forall_nondep_impl2 (φ : Prop) P :
φ → P -∗ (∀ _ :φ, P -∗ False : PROP) -∗ False.
Proof.
iIntros (Hφ) "HP Hφ".
Fail iSpecialize ("Hφ" with "HP").
Abort.
Lemma test_pure_impl2 (φ : Prop) P :
φ → P -∗ (⌜φ⌝ → P -∗ False : PROP) -∗ False.
Proof.
iIntros (Hφ) "HP Hφ".
Fail iSpecialize ("Hφ" with "HP").
Abort.
```
A few remarks:
1. In the case the hypothesis starts with a forall, `iApply ("H" $! _ with "...")` should behave the same as `iApply ("H" with "...")`. Moreover, it is weird that `iApply ("H" with "...")` suddenly generates a new goal. And, I think it is annoying to generated shelved goals. So I think they should both be rejected (as now, no change required for this). In my opinion, same remark for `iSpecialize ("Hφ" $! Hφ)` for `impl2` test cases.
2. If I remember well, we decided at some point that `∀ _ :φ,` and `⌜φ⌝ → ` should behave more or less the same. So `iSpecialize ("Hφ" with "[%]")` and `iSpecialize ("Hφ" $! Hφ)` should both work for both forms.
3. If we want to somehow support `iApply "Hφ".`, we need to infer persistence of the premises when no annotation is given. We can either do that systematically (but then, what about performances), or do that only in the case everything else fails.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/128WP tactics do not `simpl` enough2018-01-11T18:35:57ZRobbert KrebbersWP tactics do not `simpl` enoughSee for example line 133 of `ticket_lock.v`, after calling `wp_cas_fail`:
```coq
|={⊤ ∖ ↑N,⊤}=> WP if: LitV false then (wait_loop #n) (#lo, #ln) else acquire (#lo, #ln) {{ v, ϕ v }}
```
Here, there is an `of_val (LitV false)`, which sh...See for example line 133 of `ticket_lock.v`, after calling `wp_cas_fail`:
```coq
|={⊤ ∖ ↑N,⊤}=> WP if: LitV false then (wait_loop #n) (#lo, #ln) else acquire (#lo, #ln) {{ v, ϕ v }}
```
Here, there is an `of_val (LitV false)`, which should be simplified into `Lit false`, which is then pretty printed properly.
I expect the problem to be related to the fact that the WP in this case is below an update modality, and as such, `simpl` is not used.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/129Support COQBIN2018-01-23T16:16:54ZRalf Jungjung@mpi-sws.orgSupport COQBINI just got the second request to support a COQBIN environment variable, so maybe we should just do that. I imagine something like what [this Makefile](https://github.com/ppedrot/coq-string-ident/blob/master/Makefile) does, so that not se...I just got the second request to support a COQBIN environment variable, so maybe we should just do that. I imagine something like what [this Makefile](https://github.com/ppedrot/coq-string-ident/blob/master/Makefile) does, so that not setting COQBIN follows the PATH.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/131Document heap-lang `wp_` tactics2019-02-18T12:39:37ZRobbert KrebbersDocument heap-lang `wp_` tacticsRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/132Formalize example that impredicative invariants and linearity are incompatible2020-02-07T15:22:45ZRobbert KrebbersFormalize example that impredicative invariants and linearity are incompatibleRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/133Document unicode input method in README2018-12-19T16:20:38ZRobbert KrebbersDocument unicode input method in README* [x] @jung do it for emacs
* [x] @robbertkrebbers do it for CoqIDE* [x] @jung do it for emacs
* [x] @robbertkrebbers do it for CoqIDERobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/136Typeclass search loops in gen_proofmode2018-01-22T17:22:52ZJannoTypeclass search loops in gen_proofmodeThe cycle is
```
simple apply @as_valid' on
simple apply @as_valid_embed on
simple apply @sbi_embed_bi_embed on
simple eapply @as_valid_monPred_at_equiv on
simple apply @as_valid' on
simple eapply @as_valid_monPred_at_wand on
simp...The cycle is
```
simple apply @as_valid' on
simple apply @as_valid_embed on
simple apply @sbi_embed_bi_embed on
simple eapply @as_valid_monPred_at_equiv on
simple apply @as_valid' on
simple eapply @as_valid_monPred_at_wand on
simple apply @as_valid' on
```
and can be witnessed in
https://gitlab.mpi-sws.org/FP/sra-gps/blob/4514e8fdd515772c09e5a5797327651b4e6f49d4/theories/examples/tstack.v#L112Jacques-Henri JourdanJacques-Henri Jourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/140`iIntoValid` failing in an unexpected way2019-12-03T12:34:58ZJacques-Henri Jourdan`iIntoValid` failing in an unexpected waySee e181f737.
I have no idea why these changes are needed to make the test pass. It seems like iIntoValid is failing in an unexpected way.See e181f737.
I have no idea why these changes are needed to make the test pass. It seems like iIntoValid is failing in an unexpected way.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/141Make `iNext` smarter for mixed `▷` and `▷^n`2018-01-27T16:11:56ZRobbert KrebbersMake `iNext` smarter for mixed `▷` and `▷^n`See below:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n : ▷ ▷^n P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
(* Gives
"H" : ▷ ▷^n P
--------------------------------------∗
▷ P
*)
```See below:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n : ▷ ▷^n P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
(* Gives
"H" : ▷ ▷^n P
--------------------------------------∗
▷ P
*)
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/142Handle both `emp` and `True` as context2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgHandle both `emp` and `True` as contextThe generalized proofmode for a linear logic should be able to handle both `True` and `emp` as the context, ideally both in a somewhat canonical way. However, if both spatial and persistent context are empty, that can only be either `em...The generalized proofmode for a linear logic should be able to handle both `True` and `emp` as the context, ideally both in a somewhat canonical way. However, if both spatial and persistent context are empty, that can only be either `emp` or `True`; the other one will need a different representation. Right now, it is `emp`, so the only way to represent `True` is to have it explicitly in the spatial context -- which seems pretty funny. This is related to the problem with plainly and empty contexts (https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/98#note_22868).
In particular, if the goal is `valid P`, what should `iStartProof` do? (And, for that matter, what does it do currently?) The goal is `True |- P`, so the behavior from Iris (having both contexts empty) will not work.
Some options:
* Make "both contexts are empty" mean `True`, arguing that `True` is somehow more fundamental than `emp`. That clarifies what `iStartProof` should do, but now, how should `emp` be represented? Maybe the empty spatial context is `True`, but when non-empty, we just `*` together what we have, so `emp` is represented by some `"H": emp` in the spatial context? That seems like a strange discontinuitiy though. It means if we "use up" the last spatial assertion, we have to synthesize an `emp` into the context -- not very pleasant.
* Somehow "deeply embed" this information. For example, the spatial context could be optional (`option list PROP`); when absent, it interprets to `True`, otherwise to the iterated `*`. This is also awkward in some circumstances, e.g. when the spatial context is currently missing and the goal is `P -* Q` and we do `iIntros` -- now a `True` has to be synthesized into the spatial context. So maybe the better way to "deeply embed" this is to have some boolean indicating whether the context is "precise" or whether there is a `* True` around? Seems really ugly, but this time I cannot come up with a situation where we have to synthesize an assertion.
How is this currently handled in the IPM for Iron?https://gitlab.mpi-sws.org/iris/iris/-/issues/143Gen_proofmode: move internal eq into SBI2018-02-05T15:16:38ZJacques-Henri JourdanGen_proofmode: move internal eq into SBIIf the Bi is not step-indexed, then there is no reason not to use the pure embedding.If the Bi is not step-indexed, then there is no reason not to use the pure embedding.https://gitlab.mpi-sws.org/iris/iris/-/issues/144Turn Coq quantifiers into proofmode quantifiers on `iStartProof`2018-01-30T14:17:25ZRobbert KrebbersTurn Coq quantifiers into proofmode quantifiers on `iStartProof`For example, it should turn the Coq goal `forall x, P ⊢ Q` into a proof mode goal `∀ x, P → Q`. (And likewise for let-bindings).
Since issue came up in d7db5250ad0214ef4be5f634f81fe35caf6ad0d8, which changes the behavior of `iStartProof...For example, it should turn the Coq goal `forall x, P ⊢ Q` into a proof mode goal `∀ x, P → Q`. (And likewise for let-bindings).
Since issue came up in d7db5250ad0214ef4be5f634f81fe35caf6ad0d8, which changes the behavior of `iStartProof PROP`, to just introduce all quantifiers. @jjourdan introduced that because in iGPS they were often doing:
```coq
intros; iStartProof (uPred _); iIntros (V) "..."
```
The proposal in this issue fixes this problem in a nicer way.Jacques-Henri JourdanJacques-Henri Jourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/145Framing should succeed when a disjunct is exactly the framed hypothesis2018-02-08T21:00:00ZRobbert KrebbersFraming should succeed when a disjunct is exactly the framed hypothesisFor example, framing `P` in `(P ∨ Q) ∗ R` should succeed and turn the goal into `R`.
In general, framing of non-persistent hypotheses in just one disjunct of a disjunction leads to information loss, so should fail. However, if framing i...For example, framing `P` in `(P ∨ Q) ∗ R` should succeed and turn the goal into `R`.
In general, framing of non-persistent hypotheses in just one disjunct of a disjunction leads to information loss, so should fail. However, if framing in one disjunct turns it into `True`, framing should succeed.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/146Lemmas about updates should be instantiated by default witht the current BI i...2018-07-13T08:51:27ZJacques-Henri JourdanLemmas about updates should be instantiated by default witht the current BI instead of `iProp`The instances for the `FUpd` and `FUpdFacts` type classes are set in a way that gives the priority to `iProp`? Therefore, when using lemmas about updates in `vProp`, we sometimes have to manually instantiate them with the current BI. Oth...The instances for the `FUpd` and `FUpdFacts` type classes are set in a way that gives the priority to `iProp`? Therefore, when using lemmas about updates in `vProp`, we sometimes have to manually instantiate them with the current BI. Otherwise, the lemmas are instantiated with `iProp` and used through the embedding.
See, for example https://gitlab.mpi-sws.org/FP/sra-gps/blob/gen_proofmode_WIP/theories/examples/circ_buffer.v#L236
The instances for the `AsValid` type class prioritizes the fact of not using the embedding, so we should be able to fix this issue by simply making sure the search for `AsValid` occurs before `FUpd`, but I do not know how to do that.
@robbertkrebbers, any idea?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/147Infrastructure for the `monPred_all` modality2018-07-13T08:51:27ZJacques-Henri JourdanInfrastructure for the `monPred_all` modalityIf everything in the context is objective, then we should be able to introduce the `monPred_all` modality. This should reuse the infrastructure of `iAlways`.
However, I would like to go a bit further: Actually, in the case everything in...If everything in the context is objective, then we should be able to introduce the `monPred_all` modality. This should reuse the infrastructure of `iAlways`.
However, I would like to go a bit further: Actually, in the case everything in the context is objective, and the goal is objective too, we might want to switch to Iris proofmode to get rid of embeddings and all that.https://gitlab.mpi-sws.org/iris/iris/-/issues/148Make `iNext` smarter for mixed `▷` and `▷^(n+m)`2018-02-20T15:29:40ZLéon GondelmanMake `iNext` smarter for mixed `▷` and `▷^(n+m)`Following the (fixed) issue (https://gitlab.mpi-sws.org/FP/iris-coq/issues/141), there is still an error w.r.t. addition in the laterN modality:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n m : ▷ ▷^...Following the (fixed) issue (https://gitlab.mpi-sws.org/FP/iris-coq/issues/141), there is still an error w.r.t. addition in the laterN modality:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n m : ▷ ▷^(n+m) P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
```
```coq
(* Gives
"H" : ▷ ▷^(n + m) P
--------------------------------------∗
▷ P
*)
```
forgetting erroneously to cancel `n` in the premise `"H"`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/149The current axioms of BI imply emp ≡ True2018-02-26T13:43:07ZAleš Bizjakales@alesb.comThe current axioms of BI imply emp ≡ TrueAs the subject states, the current axiomatization of the plainly modality implies emp ≡ True.
In particular, the guilty parties are the axioms `prop_ext` and `plainly_emp_intro`.
I am not sure whose axioms they are, but I hope either @r...As the subject states, the current axiomatization of the plainly modality implies emp ≡ True.
In particular, the guilty parties are the axioms `prop_ext` and `plainly_emp_intro`.
I am not sure whose axioms they are, but I hope either @robbertkrebbers or @jjourdan knows the history.
I believe this must be an error, since otherwise there is no point in having `emp`.
```coq
From iris.bi Require Import interface.
Import bi.
Section bi_emp.
Context {PROP : bi}.
Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
Lemma bar: emp ⊢ (True → emp) ∧ (emp → True).
Proof.
apply and_intro.
- apply impl_intro_r, and_elim_l.
- apply impl_intro_r, pure_intro; exact I.
Qed.
Lemma baz: True ⊢ ((True : PROP) ≡ emp).
Proof.
transitivity (bi_plainly (emp : PROP))%I; first apply plainly_emp_intro.
transitivity (bi_plainly ((True → emp : PROP) ∧ (emp → True))%I).
{ apply plainly_mono, bar. }
apply prop_ext.
Qed.
End bi_emp.
```Generalized Proofmode MergerJacques-Henri JourdanJacques-Henri Jourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/151Naming : Absolute, absolutely, relatively2018-03-04T19:19:42ZJacques-Henri JourdanNaming : Absolute, absolutely, relativelyThis issue is here just to make sure that everyone agrees with the new names and notations (and to choose other ones, as I am sure you will not agree).
So:
- `monPred_all` becomes `monPred_absolutely`, written `∀ᵢ P`
- `monPred_ex` beco...This issue is here just to make sure that everyone agrees with the new names and notations (and to choose other ones, as I am sure you will not agree).
So:
- `monPred_all` becomes `monPred_absolutely`, written `∀ᵢ P`
- `monPred_ex` becomes `monPred_relatively`, written `∃ᵢ P`
- `Objective` becomes `Absolute`
Just to be clear: it took these names because something had to be chosen to make progress, and because there was objections about the previous names. No decision is taken, and anyone should feel free to contest.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/153Exponential slowdown in `iFrame` and the number of laters2018-02-20T00:50:15ZRobbert KrebbersExponential slowdown in `iFrame` and the number of laters```coq
From iris Require Import proofmode.tactics.
Lemma test2 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.141s *) Admitted.
Lemma test4 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R)...```coq
From iris Require Import proofmode.tactics.
Lemma test2 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.141s *) Admitted.
Lemma test4 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.7s *) Admitted.
Lemma test8 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ ▷ ▷ ▷ ▷ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 6.796s *) Admitted.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/154Bring back side-conditionals for `iMod`2018-07-13T08:51:28ZRobbert KrebbersBring back side-conditionals for `iMod`By @jtassaro
> So, in Iris 2.0, if I'm recalling correctly, one only had (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P under the assumption that E2 ⊆ E1 ∪ E3. I guess in the Iris 3.0 this assumption is no longer needed anymore, and so this ...By @jtassaro
> So, in Iris 2.0, if I'm recalling correctly, one only had (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P under the assumption that E2 ⊆ E1 ∪ E3. I guess in the Iris 3.0 this assumption is no longer needed anymore, and so this assumption is not part of the FUpdFacts (and I can't think of a way to jam it into the instance of ElimModal so that iMod will do the right thing). The problem is that the logic from our ESOP 2017 paper is based on Iris 2.0 style so I need this assumption. Any thoughts? Obviously I can just re-define a version of iMod that accounts for this additional hypothesis, but I'm wondering if there's a preferred way.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/155Make `iPureIntro` able to introduce affine pure assertions when the context i...2018-02-15T16:08:05ZJacques-Henri JourdanMake `iPureIntro` able to introduce affine pure assertions when the context is emtpy.The current lemma behind `iPureIntro` is:
```coq
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
```
Could we change it a bit, ...The current lemma behind `iPureIntro` is:
```coq
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
```
Could we change it a bit, so that we ask for `FromPure true Q φ` when the context is empty? That way, we could introduce CFML's affine pure assertions transparently when the context is empty.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/156How to deal with `emp`, `True`, and friends when the BI is ambigious2018-07-13T08:40:32ZRobbert KrebbersHow to deal with `emp`, `True`, and friends when the BI is ambigiousThe following discussion from !115 should be addressed:
We often write `emp : PROP`. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to wr...The following discussion from !115 should be addressed:
We often write `emp : PROP`. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to write `bi_emp (PROP:=PROP)`, which is ugly.
Maybe we should have special notations to force the type arguments of `emp`, `True`, and friends.
I think ssr is also doing something like that. Depending on the outcome of this issue, we should not just address the occurrence in !115, but also fix other occurrences.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/157`done` loops in proofmode2018-03-07T18:16:58ZRobbert Krebbers`done` loops in proofmode```coq
Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.
``````coq
Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.
```Generalized Proofmode MergerRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/158Make clear which arguments of tactics are optional in `ProofMode.md`2020-12-19T17:43:20ZRobbert KrebbersMake clear which arguments of tactics are optional in `ProofMode.md`See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050https://gitlab.mpi-sws.org/iris/iris/-/issues/159Find better name for "emp |- P"2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgFind better name for "emp |- P"Currently, `emp |- P` is called `bi_valid P` and is used as a coercion from `PROP` to `Prop`. This turns out to be the right definition for the coercion (i.e., `(l |-> v -* l |->{0.5} v * l |->{0.5} v)%I` is provable), but the name is d...Currently, `emp |- P` is called `bi_valid P` and is used as a coercion from `PROP` to `Prop`. This turns out to be the right definition for the coercion (i.e., `(l |-> v -* l |->{0.5} v * l |->{0.5} v)%I` is provable), but the name is dubious: Usually, validity is defined as `True |- P`. Let's try to find a better name.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/160Figure out the best place for the plainly modality2018-03-03T16:56:51ZRalf Jungjung@mpi-sws.orgFigure out the best place for the plainly modalityRight now, `plainly` is part of the BI interface, so *every* logic has to have this modality. Given that this modality is not at all needed for the proof mode to function, I think that's a bad choice. We already have some rather arbitra...Right now, `plainly` is part of the BI interface, so *every* logic has to have this modality. Given that this modality is not at all needed for the proof mode to function, I think that's a bad choice. We already have some rather arbitrary-looking axioms for `bi_persistently`; let's try to minimize the amount of "strange modalities" in the interface(s) as much as possible.
The following proposals are on the table:
1. Follow !98 and treat `plainly` like `fupd` and `bupd`: As "standardized extensions" that come with their own separate interface, but once instantiated with proofs of the basic laws are automatically integrated into the proofmode (because a bunch of instances based on this interface already exist).
1. Put `plainly` into `Sbi`.
1. Have a new "IrisLikeLogic", extending `Sbi`, which contains `plainly` as well as the update modalities.
My own comments:
1. This is the most general and, absent technical concerns, "best" solution -- but handling the resulting hierarchie(s) could become annoying. We'd also have to decide which approach to use for these (bundled/unbundled, typeclasses/canonical structures). (I somehow thought @robbertkrebbers was able to solve all hierarchy problems in Coq as that's what you did so far; hearing even you say that this is getting too complicated is quite unsettling to be honest ;)
1. I see no motivation for doing this, it seems rather arbitrary.
1. seems okay to me -- a little sad, but given the state of affairs probably a reasonable compromise for the time being. We have no example of a logic that would benefit from `plainly` that doesn't also have the updates.
Ideally I'd prefer 1., but given that if @robbertkrebbers can't get the hierarchy to work, neither will I -- that makes 3. look appealing enough. ;) I don't like 2. at all.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/161Use `plainly_alt` as an axiom and replace most of the current ones2020-03-18T15:08:43ZJacques-Henri JourdanUse `plainly_alt` as an axiom and replace most of the current onesIn the interface for plainly, we could have `plainly_alt` as an axiom. Here are the reasons this is not a completely absurd idea:
1- Most of the axioms can be removed. Namely, the only ones remaining are:
* `bi_persistently_impl_plainly...In the interface for plainly, we could have `plainly_alt` as an axiom. Here are the reasons this is not a completely absurd idea:
1- Most of the axioms can be removed. Namely, the only ones remaining are:
* `bi_persistently_impl_plainly`, `bi_plainly_impl_plainly` (which I find kind of arbitrary anyway),
* `sbi_mixin_prop_ext` (which is actually one of the few current axioms of `plainly` that actually /says/ something about the BI. So this is expected that it stays.
* The axioms about the updates, but I would say these are rather about the update than about `bi_plainly`
* `sbi_mixin_later_plainly_2`, which somehow I am not able to prove. But perhaps I am missing something.
Note that for some of these axioms (except `bi_plainly_impl_plainly`, `sbi_mixin_prop_ext` and the update axioms), we could
replace "for all plain assertion P" by "for all equality", which make them understandable even without understanding what is plainly.
2- I would say the definition of `plainly_alt` is quite intuitive. Indeed, `P /\ emp = emp` is a way of internally saying `emp |- P`, which exactly means that `P` is valid. So this definition can directly be interpreted as the "internal validity".https://gitlab.mpi-sws.org/iris/iris/-/issues/162Have `iFrame` smartly instantiate existentials2018-03-03T19:06:32ZJacques-Henri JourdanHave `iFrame` smartly instantiate existentialsIn the case the goal is e.g., of the form `P * ?Q`, where `?Q` is an existential, and we want to frame some assertion `R` that does not appear, we may want to instantiate `?Q` with `R * ?Q'`. Therefore, the meta-variable serves as a "buf...In the case the goal is e.g., of the form `P * ?Q`, where `?Q` is an existential, and we want to frame some assertion `R` that does not appear, we may want to instantiate `?Q` with `R * ?Q'`. Therefore, the meta-variable serves as a "buffer" where we put everything which we frame and fail to put anywhere else.
This is usefull in CFML, so I think I will implement this anyway in CFML. The reason it is usefull is that the typical CFML workflow implies working with an evar as a post-condition, which is instantiated by whatever is remaining.
Would you think this might be worth having in the general IPM?https://gitlab.mpi-sws.org/iris/iris/-/issues/164Take a closer look at the interaction of fancy updates and plainly2018-10-31T14:44:29ZRalf Jungjung@mpi-sws.orgTake a closer look at the interaction of fancy updates and plainlyCurrently we have these two laws:
```
fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
later_fupd_plain E (P : PROP) `{!Plain P} :
(▷ |={E}=> ...Currently we have these two laws:
```
fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
later_fupd_plain E (P : PROP) `{!Plain P} :
(▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
```
First, I find it surprising that we need two laws. Second, the first law looks really unwieldy.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/170iFresh should reserve fresh names2018-07-13T08:51:26ZJoseph TassarottiiFresh should reserve fresh namesRight now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
...Right now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
```
let H1 := iFresh in
let H2 := eval vm_compute in (match H1 with
| IAnon x => IAnon (1 + x)
| INamed x => IAnon 1
end) in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
iDestruct "H" as pat.
```
because `iDestruct` will also use `iFresh` and gets a name that conflicts with `H1`.
One solution would be to add a counter to the `envs` record which is incremented each time `iFresh` is called. This would actually also probably make `iFresh` more efficient anyway.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/171Split derived_laws.v2018-03-21T15:05:46ZRalf Jungjung@mpi-sws.orgSplit derived_laws.v`derived_laws.v` is a very-hard-to-navigate monster. Can we find a good way to split it?
One fairly obvious thing to do is to split the `Sbi` stuff into a separate file. Then the `Bi` file will still be huge, probably... what could be a...`derived_laws.v` is a very-hard-to-navigate monster. Can we find a good way to split it?
One fairly obvious thing to do is to split the `Sbi` stuff into a separate file. Then the `Bi` file will still be huge, probably... what could be a good criterion to separate that?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/173Ambiguous reference to eqb in coq_tactics.v2018-03-12T13:17:31ZGhost UserAmbiguous reference to eqb in coq_tactics.vWhile preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theor...While preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theories/proofmode/coq_tactics.v` fails to compile due to 2 unqualified references to `eqb` not been seen as `Bool.eqb` anymore.
This issue can be fixed in a straightforward (and backward-compatible) way : replace the two occurrence of `eqb` in this file (lines 95 and 288) by `Bool.eqb` (or alternatively, add an `Import Bool` at the end of this file's header).
Sorry for not proposing a pull request directly, but apparently I do not have enough permission to fork on your gitlab.
For this fix to be correctly taken in account by our travis testing infrastructure, could you please update the `opam` file of repository `LambdaRust-coq.git` to mention a fixed version of `iris-coq` ? Currently it points to `iris-coq` version `dev.2018-02-23.0`, leading to commit `db735a4558ad`.
Thanks!
Pierre Letouzeyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/174Confusing result by `wp_op`2018-04-22T18:08:36ZRobbert KrebbersConfusing result by `wp_op`As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(W...As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(WP if: #n = v then #true else #false {{ _, True }})%I.
Proof.
wp_op.
```
This gives
```coq
bin_op_eval EqOp #n v = Some ?Goal0
______________________________________(2/2)
--------------------------------------∗
WP if: ?Goal0 then #true else #false {{ _, True }}
```
Pre !97 this used to work because `bin_op_eval` used to match first on the operations and then on the operand. Right now, it first matches on the operands, and only then on the operation.https://gitlab.mpi-sws.org/iris/iris/-/issues/176Reconsider normalizing `/\ emp` into `<affine>`2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgReconsider normalizing `/\ emp` into `<affine>`I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `...I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `emp`, not `True`. So, framing let's say `P` in `P ∗ Q` turns it into `emp ∗ Q`, which then get beautified into `Q`.
> In this case, you are framing `P` in `<pers> Q ∧ P`, which will turn it into `<pers> Q ∧ emp`. This is then beautified into `<affine> <pers> Q`
I think we should not perform this normalization, and just keep it as `<pers> Q /\ emp`.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/177Improve naming of lemmas about modalities2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgImprove naming of lemmas about modalitiesThe following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1...The following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2_{swap,comm}: M1 (M2 P) ⊣⊢ M2 (M1 P)
```
However, @robbertkrebbers noted that we have plenty of lemmas of the last form. Optimizing for conciseness, we could also use
```
M1_{into,impl,entails}_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
```Generalized Proofmode Merger