Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-22T16:31:07Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/273Iris shadows ssreflect new syntax2019-11-22T16:31:07ZPaolo G. GiarrussoIris shadows ssreflect new syntaxIris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
In 8.10.1 ssreflect introduced syntax using `[^` and `[^~`, but they're shadowed by iris's big_op notations....Iris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
In 8.10.1 ssreflect introduced syntax using `[^` and `[^~`, but they're shadowed by iris's big_op notations.
Here's a mininal example. Block introductions are pointless here — but useful for big datatypes.
```coq
From iris.algebra Require Import base.
Lemma foo (n : nat) : n = n.
elim: n => [^ s]. (* Works *)
Restart.
elim: n => [^~ s]. (* Works *)
Abort.
From iris.proofmode Require Import tactics.
Locate "[^". (* big_op notations *).
Lemma foo (n : nat) : n = n.
(* Parse error for each of the following commands: *)
elim: n => [^~ s].
elim: n => [^ s].
(* Each gives:
Syntax error: [tactic:ssripats_ne] expected after '=>' (in [tactic:ssrintros_ne]).
*)
```
Iris version: dev.2019-11-02.2.ea809ed4.https://gitlab.mpi-sws.org/iris/iris/-/issues/329Iris Website Reform2020-09-29T15:48:56ZRalf Jungjung@mpi-sws.orgIris Website ReformWe had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* W...We had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* We'd like to split the website into sub-pages, as the list of papers is getting too long.
* We'd like to have the website repo public for contributors. I think it would make sense to have it in the Iris organization here on MPI's GitLab.
* In terms of content, the concern that triggered this discussion was along the lines of "(some) people think Iris is just for academic/toy/ML-like languages". We should probably put the fact that Iris is very flexible front and center, maybe by picking a few papers to display on the front page that use Iris for various models of real-world definitely-not-toy languages (RustBelt for Rust, runST for Haskell, DOT for Scala, "Non-Determinism in C Expressions" for C, Goose for Go, and once that paper exists RefinedC for C).
* We could also highlight the different kinds of properties people verify in Iris (type system soundness, refinement, verification of concurrent algorithms, non-interference, ...).
I expect I will take the lead on setting up the infrastructure for wiring up GitLab with Jekyll and GH pages, and @robbertkrebbers offered to take the lead on the content side of things.https://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/335iris.sty incompatible with acmart2020-07-15T12:25:40ZRalf Jungjung@mpi-sws.orgiris.sty incompatible with acmartThe `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the ...The `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the existing `\nequiv` is, or else change the name of our macro.https://gitlab.mpi-sws.org/iris/iris/-/issues/419Iron slowdown investigation2021-06-17T07:20:40ZRalf Jungjung@mpi-sws.orgIron slowdown investigationIron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iri...Iron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iris from `dev.2021-03-06.3.b0708b01` to `dev.2021-06-03.0.2959900d`. I am not sure if we can do anything about that, but it would be good to at least figure out which changes caused the slowdown (though it looks like there at several, so this might be "death by a thousand cuts").https://gitlab.mpi-sws.org/iris/iris/-/issues/168iSpecialize on implications behaves inconsistently2019-11-01T13:35:17ZRalf Jungjung@mpi-sws.orgiSpecialize on implications behaves inconsistentlyIn a goal like
```
"HP" : ■ P
--------------------------------------□
"HPQ" : ■ P → Q
--------------------------------------∗
Q
```
doing `iSpecialize ("HPQ" with "HP")` behaves as expected, but `iSpecialize ("HPQ" with "[]")` ...In a goal like
```
"HP" : ■ P
--------------------------------------□
"HPQ" : ■ P → Q
--------------------------------------∗
Q
```
doing `iSpecialize ("HPQ" with "HP")` behaves as expected, but `iSpecialize ("HPQ" with "[]")` fails saying
```
iSpecialize: (■ P → Q)%I not an implication/wand.
```
Here's a testcase:
```coq
Lemma test_plain_impl `{BiPlainly PROP} P Q :
(■ P → (■ P → Q) -∗ Q)%I.
Proof.
iIntros "#HP HPQ".
Fail iSpecialize ("HPQ" with "[]").
Fail iApply "HPQ".
iSpecialize ("HPQ" with "HP"). done.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/424Laterable cleanup2021-07-15T07:49:33ZRalf Jungjung@mpi-sws.orgLaterable cleanuphttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `late...https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `laterable_alt`).
* [ ] Rename `make_laterable` to follow our modality naming scheme... `laterably`?
* [ ] Resolve TC backtracking issue around `persistent_laterable`
* [ ] `iMod` for `make_laterable` elimination?https://gitlab.mpi-sws.org/iris/iris/-/issues/418library inG instances should be local2021-06-02T14:46:21ZRalf Jungjung@mpi-sws.orglibrary inG instances should be localCurrently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.Currently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.https://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-10-20T09:21:24ZPaolo G. GiarrussoMake `contractive_proper` into a lemma, or control other instances that make it costly.Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://...Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?https://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/428Make `iDestruct` work on `▷ ∃` if goal is except_0/update2021-07-22T13:02:40ZRobbert KrebbersMake `iDestruct` work on `▷ ∃` if goal is except_0/updateBIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
I...BIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
Instead, you get an except-0 (`◇`) modality, which can be eliminated if the goal is, for example, an update modality.
This trick is not commonly known, so it would be great if the proof mode's `iDestruct` tactic could use `bi.later_exist_except_0` automatically instead of just failing when the domain `A` is not inhabited.
This is what happens now:
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import updates.
Lemma test `{BiFUpd PROP} {A} (Φ : A → PROP) (Q : PROP) E :
▷ (∃ x, Φ x) ={E}=∗ Q.
Proof.
iIntros "H".
(* Goal:
"H" : ▷ (∃ x : A, Φ x)
--------------------------------------∗
|={E}=> Q *)
(* Tactic failure: iExistDestruct: cannot destruct (▷ (∃ x : A, Φ x))%I. *)
Fail iDestruct "H" as (x) "H".
(* Works *)
iMod (bi.later_exist_except_0 with "H") as (x) "H".
```
I tried to implement what I proposed in this MR some day, but I could not find a satisfactory generalization of the `IntoExist` class. After all, that class then needs to take the goal into account to eliminate the ◇ modality.
An alternative, we could use the `pm_error` infrastructure from #413 (which still needs to be ported to `IntoExists`) to give an error that points the user to `bi.later_exist_except_0` in case the domain `A` is not inhabited.https://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/205Make notation for pure and plainly affine2021-07-18T09:46:52ZRalf Jungjung@mpi-sws.orgMake notation for pure and plainly affineI think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/379Make sealing consistent and document it2020-11-10T13:15:28ZRalf Jungjung@mpi-sws.orgMake sealing consistent and document itWe should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to ...We should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to the eta-expanded term. This immediately implies that sealing should be done outside of sections.
* Add an `unseal` tactic, either as `Local Ltac` or in a module to avoid polluting the global namespace.
* There is no need to make sealed definitions `Typeclasses Opaque`.
- no eta, ergo no sections
- unseal tactic
- no TC opaque
For example, here is how sealing of a logic-level RA wrapper could look like:
```
Definition mnat_own_auth_def `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (mnat_auth_auth q n).
Definition mnat_own_auth_aux : seal (@mnat_own_auth_def). Proof. by eexists. Qed.
Definition mnat_own_auth := mnat_own_auth_aux.(unseal).
Definition mnat_own_auth_eq : @mnat_own_auth = @mnat_own_auth_def := mnat_own_auth_aux.(seal_eq).
Arguments mnat_own_auth {Σ _} γ q n.
Definition mnat_own_lb_def `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (mnat_auth_frag n).
Definition mnat_own_lb_aux : seal (@mnat_own_lb_def). Proof. by eexists. Qed.
Definition mnat_own_lb := mnat_own_lb_aux.(unseal).
Definition mnat_own_lb_eq : @mnat_own_lb = @mnat_own_lb_def := mnat_own_lb_aux.(seal_eq).
Arguments mnat_own_lb {Σ _} γ n.
Local Ltac unseal := rewrite
?mnat_own_auth_eq /mnat_own_auth_def
?mnat_own_lb_eq /mnat_own_lb_def.
```
When there are operational typeclasses involved, the `_eq` lemma should also account for those to avoid having to rewrite twice:
```
Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Arguments monPred_bupd {_}.
Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
```https://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/381Make sure we have Hint Mode for every typeclass2021-06-17T13:19:41ZRalf Jungjung@mpi-sws.orgMake sure we have Hint Mode for every typeclassWe should have `Hint Mode` for all our `Class`es. We could detect this with some kind of shell script that greps for `Class`, extracts the name, and then greps for `Hint Mode`.
Currently known missing `Mode`s:
* [ ] `IntoVal`
* [ ] `Wp`...We should have `Hint Mode` for all our `Class`es. We could detect this with some kind of shell script that greps for `Class`, extracts the name, and then greps for `Hint Mode`.
Currently known missing `Mode`s:
* [ ] `IntoVal`
* [ ] `Wp`
* [ ] `Twp`https://gitlab.mpi-sws.org/iris/iris/-/issues/392Masks in step-taking fupd notation2020-12-10T13:37:03ZRalf Jungjung@mpi-sws.orgMasks in step-taking fupd notationEarlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gi...Earlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/338Missing unseal tactic for siProp2020-08-30T07:04:36ZPaolo G. GiarrussoMissing unseal tactic for siProp
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_...
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl.
(* Should be siProp.unseal. *)
Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.
```
The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.https://gitlab.mpi-sws.org/iris/iris/-/issues/410Modality for `Timeless`2021-04-19T07:51:21ZRalf Jungjung@mpi-sws.orgModality for `Timeless`We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ ...We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/426Notation `≼@{A}` is missing2021-07-07T11:02:38ZRobbert KrebbersNotation `≼@{A}` is missingWe are probably missing such notations for more relations. It would be good to do a sweep.We are probably missing such notations for more relations. It would be good to do a sweep.