Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-07-13T08:51:27Zhttps://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/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/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/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/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/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/139Better names and documentation for proof mode typeclasses2020-11-23T02:33:06ZRalf Jungjung@mpi-sws.orgBetter names and documentation for proof mode typeclassesI think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs...I think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs, what are the outputs, what's it supposed to do?
Don't expect people know what the `Hint Mode` sigils mean, I certainly don't. ;)
I am thinking of something like
```coq
(* Input: `P`; Outputs: `Q1`, `Q2`.
Strengthen `P` into a disjunction. Used for `iLeft`, `iRight`. *)
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
(* Input: `P`; Outputs: `Q1`, `Q2`.
Weaken `P` into a disjunction. Used for disjunction elimination patterns. *)
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P ⊢ Q1 ∨ Q2.
```
For classes like `ElimModal` or `AddModal`, I have a hard time figuring out what they mean because they are stated in an extremely general way.https://gitlab.mpi-sws.org/iris/iris/-/issues/138wp_apply/Texan triple improvements2021-11-19T19:15:17ZRalf Jungjung@mpi-sws.orgwp_apply/Texan triple improvements* [ ] `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* [ ] `wp_apply` could automatically try to prove that the expression is not a value, and then apply some varia...* [ ] `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* [ ] `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [ ] [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* [ ] When proving a triple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
* [ ] What about some support for introducing the postcondition into the context (avoiding a manual `iIntros` all the time)?
Blocked by #130https://gitlab.mpi-sws.org/iris/iris/-/issues/137Iris-internal solve_proper2019-11-01T12:51:26ZRalf Jungjung@mpi-sws.orgIris-internal solve_properWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRustWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRusthttps://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/135Use [notypeclasses refine] for all proofmode tactics2020-11-11T12:36:56ZRobbert KrebbersUse [notypeclasses refine] for all proofmode tacticsAs done ad-hoc for two tactics in 5249f4c488c0847f229b4d9e38f89145775933be to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.As done ad-hoc for two tactics in 5249f4c488c0847f229b4d9e38f89145775933be to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.https://gitlab.mpi-sws.org/iris/iris/-/issues/134Document language interface2019-11-01T13:08:15ZRobbert KrebbersDocument language interfaceIt would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related doc...It would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related documentation, also including the current `ProofMode.md`. We could also LaTeX-ify all Coq documentation, and add it to the already existing theoretical documentation.https://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 Krebbers