Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-07-13T08:51:26Zhttps://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/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/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/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/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/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/131Document heap-lang `wp_` tactics2019-02-18T12:39:37ZRobbert KrebbersDocument heap-lang `wp_` tacticsRobbert 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/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/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/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/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/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/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/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/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/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/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/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/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?