Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-04-19T22:58:30Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/457"-" in selection patterns2022-04-19T22:58:30ZRalf Jungjung@mpi-sws.org"-" in selection patternsIt would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.It would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.https://gitlab.mpi-sws.org/iris/iris/-/issues/252"Exponentiation" for separating conjunctions2019-11-01T14:27:39ZDmitry Khalanskiy"Exponentiation" for separating conjunctionsSometimes it makes sense to have a statement about possessing `n` copies of the same resource. For example (in pseudocode), `own γ 1%Qp -∗ (own γ (1/n))^n`. Maybe such an operation should be available in the standard library, along with ...Sometimes it makes sense to have a statement about possessing `n` copies of the same resource. For example (in pseudocode), `own γ 1%Qp -∗ (own γ (1/n))^n`. Maybe such an operation should be available in the standard library, along with some useful lemmas about exponentiation?
An example of what exponentiation could be defined as:
```
Fixpoint iPropPow {Σ} (R : iProp Σ) (n : nat) : iProp Σ :=
match n with
| 0 => (True)%I
| S n' => (R ∗ iPropPow R n')%I
end.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/228"expression validity" in WP2019-11-01T13:59:44ZJonas Kastberg"expression validity" in WPI propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid i...I propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid in the absence of certain properties on the state. A predicate on expression, that are preserved under step reduction, could be used to differentiate such expressions.
Furthermore, being able to derive certain properties about expressions when opening the weakest precondition might allow for some automation in regards to "pure" reductions that depend on the state while not changing it.
Specific Case:
My Iris instantation is a "language" over processes, where ```pstate := gmap pid (state)``` and ```pexpr := pid * expr```, where ```pid``` is a process identifier.
For modularity I have separate reduction layers, with the top-layer looking up the state of the process in the state map ```step ((p,e), <[p := σh]>σp) -> ((p,e'), <[p := σh']>σp), efs)```.
This means that every single reduction requires the process id of the expression to be in the map, even if it does not change (in case the underlying reduction is pure).
The presence of the necessary mapping is then expressed as a logical fragment, which is required by every single of my weakest precondition rules. Furthermore, I cannot do "Pure" reductions, as conceptualised with the existing ```PureExec``` class.
Proposed Solution:
Update the language instantiation to include a predicate over expressions (here named ```well_formed```), and use it in the weakest precondition.
The predicate should uphold certain properties, such as being preserved under step reduction and contexts.
```
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κ κs n,
state_interp σ1 (κ ++ κs) n ∗ well_formed e1 ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs (length efs + n) ∗
well_formed e2 ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, well_formed ef ∗ wp ⊤ ef fork_post
end%I.
```
Define a lifted ```PureExecState```, which defines expressions that are reducible and "pure" assuming that the state interpretation and well-formedness predicates hold:
```
Record pure_step_state (e1 e2 : expr Λ) := {
pure_exec_val_state : to_val e1 = None;
pure_step_safe_state σ1 κ n : state_interp σ1 κ n -∗ well_formed e1 -∗ ⌜reducible_no_obs e1 σ1⌝;
pure_step_det_state σ1 κ κs e2' σ2 efs n :
state_interp σ1 (κ++κs) n -∗ well_formed e1 -∗ ⌜prim_step e1 σ1 κ e2' σ2 efs⌝ → ⌜κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []⌝
}.
```
An important property of the proposed change is that original Iris instances remain unchanged when given ```True``` as the well_formed predicate.
Points of discussion:
- It has earlier been suggested to introduce closedness of expression in a [similar manner](https://gitlab.mpi-sws.org/iris/iris/merge_requests/58). Note however that the closedness condition on expressions has been phased out of the current iteration of Iris.
- The change would mean that any WP holds trivially true for invalid expressions, which must then suddenly be considered in many places.https://gitlab.mpi-sws.org/iris/iris/-/issues/241"Flattened" introduction patterns for intuitionistic conjunction elimination.2019-11-01T13:07:29ZDan Frumin"Flattened" introduction patterns for intuitionistic conjunction elimination.The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `...The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `P ∧ Q ∧ R` by `iDestruct "H" as "(H&_&_)"`, but it doesn't work this way.
```
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Lemma test P Q R : (P ∧ Q ∧ R) -∗ P.
Proof.
iIntros "H".
(* This works fine *)
iDestruct "H" as "(_ & _ & H)".
Undo.
iDestruct "H" as "(_ & H & _)".
Undo.
(* This results in an error *)
Fail iDestruct "H" as "(H & _ & _)".
(* "Proper" way of doing it *)
iDestruct "H" as "(H & _)".
done.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/347"solve_inG" is very slow for larger RA combinators2021-03-03T13:07:08ZRalf Jungjung@mpi-sws.org"solve_inG" is very slow for larger RA combinatorsIn his Iris fork, @jtassaro has a [rather large RA](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/wsat.v#L43) that completely explodes `solve_inG`. Before https://...In his Iris fork, @jtassaro has a [rather large RA](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/wsat.v#L43) that completely explodes `solve_inG`. Before https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/498, it took around 15s, and then `Qed` took another 15s.
Since !498, they just don't terminate any more. I can make the proof itself go through by adding a `simpl in *` in `solve_inG` (before [this `intros`](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/own.v#L45)), but then `Qed` still takes forever. To make `Qed` work I added some awful hack that seemingly successfully guides Coq towards using the right reduction strategy for `Qed`.
I am not sure what we can do here, besides entirely sealing functors and thus making them non-computational (so we'd have to prove unfolding lemmas about them all, and somehow use them in `solve_inG`).https://gitlab.mpi-sws.org/iris/iris/-/issues/452"wp_apply ... as"2022-04-16T22:06:11ZRalf Jungjung@mpi-sws.org"wp_apply ... as"Applying a typical spec in Iris usually looks something like this:
```
wp_apply (Spec with "...").
{ (* solve precondition *) }
iIntros (x) "H".
```
The `iIntros` can be quite far removed from the `wp_apply`, if proving the precondition ...Applying a typical spec in Iris usually looks something like this:
```
wp_apply (Spec with "...").
{ (* solve precondition *) }
iIntros (x) "H".
```
The `iIntros` can be quite far removed from the `wp_apply`, if proving the precondition takes some work. Also it seems a bit odd to have this separated into two tactics.
@robbertkrebbers I wonder how feasible it would be to support `wp_apply (Spec with "...") as ...`, combining the `iIntros` into the `wp_apply`? I have actually accidentally written this last week and was a bit bummed that it did not work. ;)https://gitlab.mpi-sws.org/iris/iris/-/issues/262`big_op*_forall` that relate traversals over different structures2020-01-21T18:50:28ZDmitry Khalanskiy`big_op*_forall` that relate traversals over different structuresMost lemmas that relate several `big_op` statements only concern themselves with the case when the iteration is performed on the same data. However, at times, even if the structures are actually different, the values combined by `o` are,...Most lemmas that relate several `big_op` statements only concern themselves with the case when the iteration is performed on the same data. However, at times, even if the structures are actually different, the values combined by `o` are, in fact, the same.
So, I think that `big_op*_forall` can be usefully generalized.
Here is my attempt at generalizing `big_opL_forall`:
```
Theorem big_opL_forall' {M: ofeT} {o: M -> M -> M} {H': Monoid o} {A B: Type}
R f g (l: list A) (l': list B):
Reflexive R ->
Proper (R ==> R ==> R) o ->
length l = length l' ->
(forall k y y', l !! k = Some y -> l' !! k = Some y' -> R (f k y) (g k y')) ->
R ([^o list] k ↦ y ∈ l, f k y) ([^o list] k ↦ y ∈ l', g k y).
Proof.
intros ??. revert l' f g. induction l as [|x l IH]=> l' f g HLen HHyp //=.
all: destruct l'; inversion HLen; eauto.
simpl. f_equiv; eauto.
Qed.
```
A client of this theorem that I actually needed:
```
Lemma big_opL_irrelevant_element (M: ofeT) (o: M -> M -> M) (H': Monoid o)
{A: Type} n (P: nat -> M) (l: list A):
([^o list] i ↦ _ ∈ l, P (n+i)%nat)%I =
([^o list] i ∈ seq n (length l), P i%nat)%I.
Proof.
assert (length l = length (seq n (length l))) as HSeqLen
by (rewrite seq_length; auto).
apply big_opL_forall'; try apply _. done.
intros ? ? ? _ HElem.
assert (k < length l)%nat as HKLt.
{ rewrite HSeqLen. apply lookup_lt_is_Some. by eexists. }
apply nth_lookup_Some with (d:=O) in HElem.
rewrite seq_nth in HElem; subst; done.
Qed.
```
Without `big_forall'`, I couldn't come up with such a straightforward proof and ended up with this unpleasantness:
```
Lemma big_opL_irrelevant_element (M: ofeT) (o: M -> M -> M) (H': Monoid o)
{A: Type} n (P: nat -> M) (l: list A):
([^o list] i ↦ _ ∈ l, P (n+i)%nat)%I =
([^o list] i ∈ seq n (length l), P i%nat)%I.
Proof.
move: n. induction l; simpl. done.
move=> n. rewrite -plus_n_O.
specialize (IHl (S n)).
rewrite -IHl /= (big_opL_forall _ _ (fun i _ => P (S (n + i))%nat)) //.
intros. by rewrite plus_n_Sm.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/366`Export` everywhere does not permit consistent shadowing2020-11-05T11:54:13ZRalf Jungjung@mpi-sws.org`Export` everywhere does not permit consistent shadowingWhen using `Export`, even if imports are ordered consistently, there is sometimes no way to obtain consistent shadowing:
```
From stdpp Require base.
Module or.
Export stdpp.base.
Definition or_comm := 10.
End or.
Module and.
Expo...When using `Export`, even if imports are ordered consistently, there is sometimes no way to obtain consistent shadowing:
```
From stdpp Require base.
Module or.
Export stdpp.base.
Definition or_comm := 10.
End or.
Module and.
Export stdpp.base.
Definition and_comm := 11.
End and.
Module A.
Import or and.
Locate or_comm.
(*
Constant stdpp.base.or_comm
Constant Coq.Init.Logic.or_comm (shorter name to refer to it in current context is Logic.or_comm)
Constant Top.or.or_comm (shorter name to refer to it in current context is or.or_comm)
*)
Locate and_comm.
(*
Constant Top.and.and_comm
Constant Coq.Init.Logic.and_comm (shorter name to refer to it in current context is Logic.and_comm)
Constant stdpp.base.and_comm (shorter name to refer to it in current context is base.and_comm)
*)
End A.
```
Here, importing `and` overwrites `or_comm` because of the `stdpp.base` export.
I think the only way to avoid this is to avoid `Export`ing except when the re-exported symbols are conceptually really part of that library (such as `stdpp.prelude`).https://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/268`iInv`: support tokens that are "framed" around the accessor2020-03-18T15:01:32ZDan Frumin`iInv`: support tokens that are "framed" around the accessorI have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" ...I have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" "Hcl"
```
This also prevents me from using the `(x1 x2) "..."` introduction pattern. E.g. instead of
```
iInv N with "Hp" as (x) "[H1 H2]" "Hcl"
```
one has to write
```
iInv N with "Hp" as "[H Hp]" "Hcl";
iDestruct "H" as (x) "[H1 H2]"
```
It is not immediately obvious how to modify the tactics, because in general the `selpat` in `iInv N with selpat` can be an arbitrary selection pattern and not just one identifier.https://gitlab.mpi-sws.org/iris/iris/-/issues/397`iRename` fails with bad error message when not in proof mode2021-02-17T08:48:22ZRobbert Krebbers`iRename` fails with bad error message when not in proof mode```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
wit...```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
with "True".
```
The tactic probably does not call `iStartProof` at the beginning.https://gitlab.mpi-sws.org/iris/iris/-/issues/178`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviors2019-11-01T12:50:05ZJacques-Henri Jourdan`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviorsIn an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.In an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/339Add "reservation map" CMRA2020-09-09T12:29:51ZRalf Jungjung@mpi-sws.orgAdd "reservation map" CMRAFor the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an i...For the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?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/244Add a general lattice RA to Iris2020-12-10T16:56:05ZRalf Jungjung@mpi-sws.orgAdd a general lattice RA to IrisHistories as monotonically growing lists are something that comes up every now and then, and it can be quite annoying to formalize. I believe we have something like that already in GPFSL, based on a general framework of (semi-) lattices....Histories as monotonically growing lists are something that comes up every now and then, and it can be quite annoying to formalize. I believe we have something like that already in GPFSL, based on a general framework of (semi-) lattices. We should have that RA in Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/391Add append-only list RA to Iris2021-05-17T16:32:27ZRalf Jungjung@mpi-sws.orgAdd append-only list RA to IrisAppend-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize l...Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Hai DangHai Danghttps://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/449Add internalised rules for derived resource algebras2022-03-04T00:38:47ZJonas KastbergAdd internalised rules for derived resource algebrasWorking with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in ...Working with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in the model), `auth_both_validN` (in the model, with step-indices), and `auth_both_validI` (in the logic).
Some derived resource algebras are missing their "internalised rules" (those of the logic).
This issue is then to address the lack of these rules.
One example of a resource algebra with missing rules are `mono_list`.
In full, to solve this issue we should:
- Identify all resource algebras with missing internalised rules
- Add the missing rules
- (Settle on a potential pipeline for future algebras to ensure that the rules are included)https://gitlab.mpi-sws.org/iris/iris/-/issues/371Add validI lemmas for discrete RAs2020-11-05T08:41:29ZRalf Jungjung@mpi-sws.orgAdd validI lemmas for discrete RAsOur discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `...Our discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `Prop`-level lemmas. But e.g. when proving equivalences, it can be useful to have a way to rewrite validity into an equivalent logical statement.
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/558 added the lemma for frac, but other RAs are still missing:
* [ ] `gset_disj`
* [ ] `coPset`, `coPset_disj`
* [ ] `sts`
* [ ] `dfrac`https://gitlab.mpi-sws.org/iris/iris/-/issues/286Address the STS encodings lack of usefulness2020-01-30T21:32:04ZJonas KastbergAddress the STS encodings lack of usefulnessThe current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "ve...The current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".
Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out.
Going forward we should do either of the following:
- Include a disclaimer discouraging people from using them
- Remove the encoding from the repository
- Update the implementation to be more user-friendly
I suggest doing either of the first two short-term and then possibly look into the third long-term.
It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.