Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-01-22T17:22:52Zhttps://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 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 Mergerhttps://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/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/117Make some of the `wp_` tactics language independent2019-11-01T13:23:45ZRobbert KrebbersMake some of the `wp_` tactics language independentA large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.A large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.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 Krebbers