Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-12-03T12:34:58Zhttps://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/130Make iApply "with" specialization lazier2019-11-01T13:46:23ZRobbert KrebbersMake iApply "with" specialization lazierFor example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tr...For example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tries to prove the premises of the lemma by framing, and then tries to match the goal. Since framing is performed first, it instantiates evars in the wrong way. If it would first try to match the goal, and then frame, the evars would already be instantiated when framing is performed.
```coq
From iris.heap_lang Require Import proofmode notation.
Parameter swap : val.
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Section proof.
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof. Admitted.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
Fail wp_apply (swap_spec with "[$]").
wp_apply (swap_spec y z with "[$]").
Admitted.
End proof.
```
It's probably easy to come up with a simpler example, but I ran into this one while preparing the Iris tutorial.
Another example:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```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/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/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/125Make `iClear` work when there is at least one absorbing spatial hypothesis2019-11-01T13:08:25ZRobbert KrebbersMake `iClear` work when there is at least one absorbing spatial hypothesis`iClear "H"` with `H : P` currently works if either the goal is absorbing, or `P` is affine. (The same applies to `iIntros "_"`).
We could add another case: there exists at least one spatial hypothesis that is absorbing.
See also the d...`iClear "H"` with `H : P` currently works if either the goal is absorbing, or `P` is affine. (The same applies to `iIntros "_"`).
We could add another case: there exists at least one spatial hypothesis that is absorbing.
See also the discussion in !98 for a possible use-case.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/124heap_lang: mutable n-ary locations, n-ary products, n-ary sums2021-09-21T14:25:35ZRalf Jungjung@mpi-sws.orgheap_lang: mutable n-ary locations, n-ary products, n-ary sumsThe former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.The former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.https://gitlab.mpi-sws.org/iris/iris/-/issues/123Add a general constructor from an affine BI2019-11-01T13:24:47ZRalf Jungjung@mpi-sws.orgAdd a general constructor from an affine BIIn master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just...In master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just claims them to be `(ADMISSIBLE)` in a comment.
I see two ways to achieve that:
* We could provide a general way to construct a `BiMixin` from a proof of all the laws given in the appendix.
* We could do the more specific thing and first prove the appendix laws for `uPred`, and subsequently not use `unseal` when proving the `BiMixin`.https://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/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 Merger