Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-08-05T14:57:38Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/422`iApply` does not use `FromAssumption` for goal matching2021-08-05T14:57:38ZRobbert Krebbers`iApply` does not use `FromAssumption` for goal matching```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} ...```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
(P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
```
When using `iApply` in combination with the `with` clause, it will first `iSpecialize` and then use `iApply`, which in these examples turns to the degenerate case of `iExact`. The `iExact` tactic uses `FromAssumption` to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).
When using `iApply` without the `with` clause, it will launch a search using `IntoWand` where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.
The problem is the instance:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
Here, `Q` should match exactly. I tried strengtening it to:
```coq
Global Instance into_wand_wand p q P Q P' Q' :
FromAssumption q P P' →
FromAssumption (p && q) Q' Q →
IntoWand p q (P' -∗ Q') P Q.
```
However, that causes other problems: in some cases the above instance will be triggered instead of instances like `into_wand_bupd_args` causing the following to go wrong:
```coq
Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
(P -∗ Q) -∗ |==> Q.
Proof.
iIntros "H".
iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)
```
This issue came up in practice Simuliris.https://gitlab.mpi-sws.org/iris/iris/-/issues/423⌜...⌝ uses bad scopes2021-06-18T22:07:47ZRalf Jungjung@mpi-sws.org⌜...⌝ uses bad scopes`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
...`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
```
This leads to `+` being interpreted as a type.
I think we should remove `%type` here. Not sure about `%stdpp`.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/425Splitting (some of) the laws for persistence into a separate class.2023-07-25T15:46:59ZDan FruminSplitting (some of) the laws for persistence into a separate class.I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persiste...I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persistence modality that can be equipped onto an arbitrary BI.
For later, the BI interface includes the operation itself in the signature, and states a bunch of laws that are satisfied by a degenerate instance of the later modality, and the law that is _not_ satisfied by the degenerate version is in a separate class `BiLöb`.
Would something like that be possible for the persistence modality?
For example, the laws `bi_mixin_persistently_absorbing` and `bi_mixin_persistently_and_sep_elim` could be moved into a separate typeclass; then the remaining laws could be satisfied by the identity function.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.https://gitlab.mpi-sws.org/iris/iris/-/issues/427Upstreaming big_op lemmas2021-07-16T09:37:22ZMichael SammlerUpstreaming big_op lemmasRefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
len...RefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
length l1 = length l2 →
([∗ list] k↦x ∈ l1, Φ k x) -∗
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen); destruct l2 => //=; simpl in *.
iDestruct "Hl" as "[Hx1 Hl]". iSplitL "Hx1". by iApply "Himpl".
iApply ("IH" $! (Φ ∘ S) (Ψ ∘ S) l2 _ with "[] Hl").
iIntros "!>" (k y1 y2 ?) "Hl2 /= ?".
by iApply ("Himpl" with "[] [Hl2]").
Unshelve. lia.
Qed.
End sep_list.
Lemma big_sepL2_impl' {A B C D} (Φ : _ → _ → _ → PROP) (Ψ : _ → _ → _ → _) (l1 : list A) (l2 : list B) (l1' : list C) (l2' : list D) `{!BiAffine PROP} :
length l1 = length l1' → length l2 = length l2' →
([∗ list] k↦x;y ∈ l1; l2, Φ k x y) -∗
□ (∀ k x1 x2 y1 y2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ ⌜l1' !! k = Some y1⌝ -∗ ⌜l2' !! k = Some y2⌝ -∗ Φ k x1 x2 -∗ Ψ k y1 y2) -∗
[∗ list] k↦x;y ∈ l1';l2', Ψ k x y.
Proof.
iIntros (Hlen1 Hlen2) "Hl #Himpl".
rewrite !big_sepL2_alt. iDestruct "Hl" as (Hl1) "Hl".
iSplit. { iPureIntro. congruence. }
iApply (big_sepL_impl' with "Hl"). { rewrite !zip_with_length. lia. }
iIntros "!>" (k [x1 x2] [y1 y2]).
rewrite !lookup_zip_with_Some.
iDestruct 1 as %(?&?&?&?).
iDestruct 1 as %(?&?&?&?). simplify_eq. destruct_and!.
by iApply "Himpl".
Qed.
```
How can one prove these lemmas in a way that they can be upstreamed?https://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/429Enable the use of the proofmode for proving big-op lemmas2021-07-28T12:28:45ZRalf Jungjung@mpi-sws.orgEnable the use of the proofmode for proving big-op lemmasThere are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find s...There are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find some way to stratify this, so that only some core set of lemmas needs to be shown without the proofmode, and the rest can use the proofmode.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/430iInduction does not work well for induction principles involving `Forall`2022-02-11T10:28:24ZRalf Jungjung@mpi-sws.orgiInduction does not work well for induction principles involving `Forall`Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind...Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind`, where `expr_ind` is a custom induction principle that uses `Forall` to handle nested lists.
Here's a self-contained testcase:
```coq
Inductive tree (T : Type) := Tree : list (tree T) → tree T.
Arguments Tree {T}.
Lemma tree_ind' T (P : tree T → Prop) :
(∀ l, Forall P l → P (Tree l)) →
∀ t, P t.
Proof.
intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
induction l as [|t l IH].
{ constructor. }
constructor; last apply IH.
apply REC.
Qed.
Lemma test_iInduction_Forall (t : tree nat) (P : PROP) : ⊢ P.
Proof. iInduction t as [] "IH" using tree_ind'.
```
This shows a goal
```
PROP : bi
l : list (tree nat)
P : PROP
============================
"IH" : <pers> ?P
--------------------------------------□
P
```
An `unshelve` shows that the `IntoIH` simply was not resolved, which seems like a bug in its own right -- `iInduction` should fail in that case.
In fact this testcase is interesting in the sense that even adding the instance from Simuliris (even after getting rid of the `BiAffine` assumption) does not help:
```coq
Section tactics.
Import iris.bi.bi.
Import iris.proofmode.base environments classes modality_instances.
Import bi.
Import env_notations.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
Import coq_tactics.
Local Instance into_ih_Forall {A} (φ : A → Prop) (l : list A) Δ Φ :
(∀ x, x ∈ l → IntoIH (φ x) Δ (Φ x)) → IntoIH (Forall φ l) Δ (∀ x, ⌜x ∈ l⌝ → Φ x) | 2.
Proof.
rewrite /IntoIH Forall_forall => HΔ Hf. apply forall_intro=> x.
iIntros "Henv %Hl". iApply (HΔ with "Henv"); eauto.
Qed.
End tactics.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/431Add generalized implication lemma for sets, etc.2021-07-29T07:29:12ZSimon Friis VindumAdd generalized implication lemma for sets, etc.!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X...!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X1 X2 :
([∗ set] x ∈ X1, Φ k x) -∗
□ (∀ (x : X),
⌜x ∈ X2⌝ →
((⌜x ∈ X1⌝ ∧ Φ x) ∨ <affinely> ⌜x ¬∈ X1⌝) -∗
Ψ x) -∗
([∗ set] y ∈ X2, Ψ y) ∗
([∗ set] x ∈ X1∖X2, Φ x).
```https://gitlab.mpi-sws.org/iris/iris/-/issues/432iApply "auto frame": bad error message2021-09-06T06:47:59ZRalf Jungjung@mpi-sws.orgiApply "auto frame": bad error messageThe following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable t...The following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable tactic.
```
There is a `fail "iSpecialize: premise cannot be solved by framing"` in the tactic code but that does not seem to work.https://gitlab.mpi-sws.org/iris/iris/-/issues/433Tracking issue for HeapLang improvements2021-09-26T00:23:01ZTej Chajedtchajed@gmail.comTracking issue for HeapLang improvementsWe (primarily @robbertkrebbers, @jung, @tchajed, @arthuraa) have a few ideas for improving HeapLang as a language to write programs in. One way to improve HeapLang is by adding libraries, and another way is to add primitives to the langu...We (primarily @robbertkrebbers, @jung, @tchajed, @arthuraa) have a few ideas for improving HeapLang as a language to write programs in. One way to improve HeapLang is by adding libraries, and another way is to add primitives to the language.
Libraries are nice because they don't break backwards compatibility, don't make metatheory harder, and are easy to incrementally develop, test, and improve. There are already libraries floating around, so this effort would be mainly developing good specifications and ergonomics, then distributing the libraries so people can start using them.
# Library support
Some libraries we would like to support include:
- n-ary products and sums, either on the heap or as pure values
- lists and maps, either on the heap or as pure values
Here are a few concrete tasks to get started:
- [ ] Implement pattern matching for products. It would look something like `let: ("a", "b") := "p" in ...` and would bind `"a"` and `"b"` to `Fst "p"` and `Snd "p"`. This is interesting because it's the simplest example we could come up with of a derived construct with binders.
- [ ] Experiment with a nice sum pattern matching library, desugaring to `match:` but with support for a list of variants.
- [ ] Implement a generic list matching library, for list values.
- [ ] Implement a heap linked-list library. Give it a spec in terms of `list val` and then a derived spec that takes `list_rep {A:Type} (l:list A) (Φ: A -> iProp) (v:val)`, relating the list reference `v` to a Gallina list via a representation predicate for each element.
- [ ] Implement a map library along the same lines as the heap linked-list library, using a `gmap val val` and a representation predicate.
# Language improvements
One simplification to the language's representation is to consolidate constructors. The best illustration of this is [simp_lang](https://github.com/tchajed/iris-simp-lang/blob/9ae960be92d23fcf2c96fc8108d3c70c0b790db6/src/lang.v#L75-L77) which already does this; for example, `Fst`, `Snd`, `InjL`, and `InjR` are all consolidated into a single `UnOp op` constructor with a Gallina inductive `op` to identify which operation it is. One resulting simplification is that these all share the same evaluation contexts.
We could have primitive algebraic data types. This has the strong downside of requiring metatheory like logical relations to handle them in some way, whereas right now they only need cases for binary sums and products, with a simple pattern matching construct for sums that takes two lambdas. n-ary pattern matching on sums takes an arbitrary number of lambdas, which is complicated.
Adding a type discriminator would allow a generic, polymorphic equality operator. For metatheory like logical relations, most likely most users would just forbid type discrimination (eg, by not including it in the type system or logical relation), partly because it breaks abstraction.https://gitlab.mpi-sws.org/iris/iris/-/issues/434Diverging `iFrame` with predicate evar2021-10-01T18:46:05ZRalf Jungjung@mpi-sws.orgDiverging `iFrame` with predicate evarThis is a minimized version of a diverging `iFrame` I found in Perennial:
```
Lemma test_iFrame_pred_evar (P Q : PROP) :
P -∗ ∃ (Φ : nat → PROP), ((∃ n, id (Φ n)) ∨ Q).
Proof. iIntros "HP". iExists _. iFrame "HP".
```
The goal at the t...This is a minimized version of a diverging `iFrame` I found in Perennial:
```
Lemma test_iFrame_pred_evar (P Q : PROP) :
P -∗ ∃ (Φ : nat → PROP), ((∃ n, id (Φ n)) ∨ Q).
Proof. iIntros "HP". iExists _. iFrame "HP".
```
The goal at the time of framing is
```
"HP" : P
--------------------------------------∗
(∃ n : nat, id (?Goal n)) ∨ Q
```
All these components seem necessary: when I remove the disjunction, the exisential, or the `id`, the divergence goes away.
In the trace, I can see that it is phantasizing a bigMS into existence, but I do not know why:
```
Debug: 1.1-1.1-1.1-1.1-1.12: simple apply @frame_instances.frame_big_sepMS_disj_union on
(Frame false P (id (?Goal a)) (?Ψ a)), 1 subgoal(s)
Debug:
1.1-1.1-1.1-1.1-1.12-1 : (Frame false P (([∗ mset] y ∈ ?X1, ?Φ y) ∗ ([∗ mset] y ∈ ?X2, ?Φ y)) (?Ψ a))
```
I think one part of the problem is that the extra `id` means that `(id (?Goal a))` does not start with an evar, so the `!` is circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/435Please create a tag for Coq 8.14 in Coq Platform 2021.112021-11-14T18:33:05ZMichael SoegtropPlease create a tag for Coq 8.14 in Coq Platform 2021.11The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of di...The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.4.0) does not work with Coq 8.14+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
ee6a36b3e803ebec465bf44bb5bcbf9b19fe6b62 on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag, or communicate us any existing tag that works with Coq branch v8.14, preferably before November 15, 2021?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
The working branch of Coq Platform, which already supports Coq version 8.14+rc1, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/139https://gitlab.mpi-sws.org/iris/iris/-/issues/436opam package description is not helpful2021-10-26T21:59:09ZMichael Soegtropopam package description is not helpfulThe package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_l...The package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
```
The description should more elaborate on the question what this can be used for.
See (https://coq.inria.fr/opam/released/packages/coq-iris/coq-iris.3.4.0/opam)
See (https://coq.inria.fr/opam/released/packages/coq-iris-heap-lang/coq-iris-heap-lang.3.4.0/opam)
Please note that (afaik) it is no issue to change the description of opam packages without creating a new version.https://gitlab.mpi-sws.org/iris/iris/-/issues/437Typo in documentation2021-10-26T19:12:53ZAlexandre MoineTypo in documentationHi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two l...Hi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two lines. This seems to be the only occurrencehttps://gitlab.mpi-sws.org/iris/iris/-/issues/438Use HB.lock(-like) sealing2023-11-10T15:51:29ZRalf Jungjung@mpi-sws.orgUse HB.lock(-like) sealinghierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a dif...hierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a difference in practice.
Quoting from https://github.com/math-comp/hierarchy-builder/wiki/Locking:
```
HB.lock Definition new_concept := 999999.
Lemma test x : new_concept ^ x ^ new_concept = x ^ new_concept ^ new_concept.
Proof.
Time Fail reflexivity. (* takes 0s *)
rewrite new_concept.unlock.
Time Fail reflexivity. (* takes 7s, the original body is restored *)
Abort.
```
This is exactly the kind of locking API I always wanted: just adding a keyword in front of the `Definition`, done. This would make it a no-brainer to seal basically every `iProp` that our reusable libraries export.
TODO:
- Check if this actually works in Iris
- Decide if we want to do this, and how -- are we okay with a dependency on hierarchy-builder?https://gitlab.mpi-sws.org/iris/iris/-/issues/439Tracking issue for append-only list RA2022-01-21T21:41:49ZRalf Jungjung@mpi-sws.orgTracking issue for append-only list RAThis is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
The a...This is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
The algebra part of this has been merged; what remains is the base_logic wrapper.
## Open issues
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use. This is discussed in more generality at https://gitlab.mpi-sws.org/iris/iris/-/issues/412.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/441Upstream later credits2022-10-14T16:34:37ZRalf Jungjung@mpi-sws.orgUpstream later credits@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I k...@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I keep forgetting what exactly are the `fupd` laws that we would lose by doing this, so maybe we can put that here. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/442Potentially add Frame instances for all our Fractional instances2022-01-17T02:02:14ZRalf Jungjung@mpi-sws.orgPotentially add Frame instances for all our Fractional instancesIn https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
...In https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
```
This is useful since it matches on the head symbol of the framed expression, which is a lot more efficient than `frame_fractional`.
However, we have more `Fractional` instances in the codebase, which for now do not support framing any more:
* `Fractional (λ q, mono_nat_auth_own γ q n)`
* `Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L)`
* `Fractional (λ q, k ↪[γ]{#q} v)` (for `ghost_map`)
* `Fractional (λ q, ghost_map_auth γ q m)`
* `Fractional (λ q, ghost_var γ q a)`
* `Fractional (cinv_own γ)`
If the need comes up, we should add them back. Also, if it was easier to add them (e.g. with some kind of macro), there'd be less hesitation to add these instances everywhere.