Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2023-10-24T12:28:27Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/545Better error when trying mask-changing iMod on non-atomic WP goal2023-10-24T12:28:27ZRalf Jungjung@mpi-sws.orgBetter error when trying mask-changing iMod on non-atomic WP goalCurrently when you run `iMod` on a mask-changing fupd and the goal is a WP with an expression that cannot be proven atomic, we open a subgoal that asks the user to prove atomicity. In many cases, this subgoal will be unprovable. Also in ...Currently when you run `iMod` on a mask-changing fupd and the goal is a WP with an expression that cannot be proven atomic, we open a subgoal that asks the user to prove atomicity. In many cases, this subgoal will be unprovable. Also in many cases, the user will be surprised by why this shows up now but didn't show up in the tutorial when they opened an invariant.
I think instead of falling back to asking the user to prove the goal, we should fall back to showing an error message, such as with the `pm_error` infrastructure. The message should then give the user some useful hints for what to do.https://gitlab.mpi-sws.org/iris/iris/-/issues/413Better errors when tactic fails to automatically resolve some side-condition2021-07-22T12:54:29ZRalf Jungjung@mpi-sws.orgBetter errors when tactic fails to automatically resolve some side-condition@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-conditio...@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-condition; we could introduce something like
```
Definition pm_error (s : string) := False
```
and add instances with `error "foo"` as their side-condition; together with some support in `iSolveSideCondition` this could be used to then show better, instance-specific error messages when `iMod` fails.
2. We could add a new typeclass like `ElimModalError` that is used to compute an error message when `ElimModal` failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.https://gitlab.mpi-sws.org/iris/iris/-/issues/139Better names and documentation for proof mode typeclasses2020-11-23T02:33:06ZRalf Jungjung@mpi-sws.orgBetter names and documentation for proof mode typeclassesI think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs...I think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs, what are the outputs, what's it supposed to do?
Don't expect people know what the `Hint Mode` sigils mean, I certainly don't. ;)
I am thinking of something like
```coq
(* Input: `P`; Outputs: `Q1`, `Q2`.
Strengthen `P` into a disjunction. Used for `iLeft`, `iRight`. *)
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
(* Input: `P`; Outputs: `Q1`, `Q2`.
Weaken `P` into a disjunction. Used for disjunction elimination patterns. *)
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P ⊢ Q1 ∨ Q2.
```
For classes like `ElimModal` or `AddModal`, I have a hard time figuring out what they mean because they are stated in an extremely general way.https://gitlab.mpi-sws.org/iris/iris/-/issues/416big_sep lemmas fail to apply when goal is not eta-expanded2021-05-26T11:31:56ZRalf Jungjung@mpi-sws.orgbig_sep lemmas fail to apply when goal is not eta-expandedI just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failu...I just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failure: iApply: cannot apply
(([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, ?Goal k y1 y2)
∗-∗ ?Goal ?Goal2 ?Goal3 ?Goal4
∗ ([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, if decide (k = ?Goal2) then emp else ?Goal k y1 y2))%I. *)
iApply (big_sepL2_delete Φ).
(* This works. *)
```
For some reason Coq needs to be manually given `Φ` here. That should not be the case.
The only difference between the lemma statement and the goal is an eta-expansion of `Φ`.https://gitlab.mpi-sws.org/iris/iris/-/issues/500Boolean parameters to `MaybeFrame` and other proofmode classes are hard to read2022-12-07T10:39:07ZIke MulderBoolean parameters to `MaybeFrame` and other proofmode classes are hard to readThe `MaybeFrame` class used by the `iFrame` tactic is defined as follows:
```
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been...The `MaybeFrame` class used by the `iFrame` tactic is defined as follows:
```
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : □?p R ∗ Q ⊢ P.
```
However, as noted in !872, this `progress` argument becomes quite hard to read in instances like
`TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.`
A suggestion was to use a custom two-constructor inductive, something like
`Inductive progress_indicator := DidSomething | DidNothing.`.
Operations like `&&` and `||` would then need to be added for this inductive as well.
(@robbertkrebbers mentioned the `MaybeFrame` instances might be removed someday, so that the `MaybeFrame` class would become obsolete. That would also fix this problem.)https://gitlab.mpi-sws.org/iris/iris/-/issues/29Bring back Logically Atomic Triples (Coq + docs)2019-11-01T13:09:17ZJeehoon Kangjeehoon.kang@kaist.ac.krBring back Logically Atomic Triples (Coq + docs)* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendi...* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
- Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.
---
@jung wrote
The POPL 2015 appendix has been split into two parts:
* The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/
* The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)
What, specifically, are you missing from the POPL 2015 appendix?
https://gitlab.mpi-sws.org/iris/iris/-/issues/357Cancelable locks2020-10-21T11:00:44ZRobbert KrebbersCancelable locksIt would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R...It would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R }} free lk {{ R }}`
2. A rule `is_lock lk 1 R ==∗ ▷ R ∗ (▷ R' ==∗ is_lock lk 1 R')` that allows a "strong update" of the payload of the lock.
Now that we have the discardable fractional permissions, we could use those to get back the ordinary lock-spec by picking the fraction to be `DfracDiscarded`.
To implement this, we probably first want to generalize cancelable invariants, by a.) adding a discardable fraction b.) adding a rule for changing the proposition in case one owns the entire fraction.
Questions:
- For locks, do we want to equip `is_lock` with a fraction, or do we want to add a token `lock_own` (which would be timeless).
- If we equip `is_lock` with a fraction, we won't break backwards compatibility that much. One just needs to add `DfracDiscarded` everywhere. If we have a token for the fraction, backwards compatibility is a bigger issue. We could of course define `is_lock ... := new_is_lock ... ∗ lock_own DfracDiscarded` or something like that.
Any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/496Cannot iApply lemma with let-binder and bi_emp_valid2022-11-23T18:37:35ZRalf Jungjung@mpi-sws.orgCannot iApply lemma with let-binder and bi_emp_validThe following script fails:
```
Lemma test_iPoseProof_let2 P Q :
(let R := True%I in ⊢ R ∗ P -∗ Q) →
P ⊢ Q.
Proof.
iIntros (help) "HP".
iPoseProof (help with "[$HP]") as "?". done.
Qed.
```
It says (notation printing due to this ...The following script fails:
```
Lemma test_iPoseProof_let2 P Q :
(let R := True%I in ⊢ R ∗ P -∗ Q) →
P ⊢ Q.
Proof.
iIntros (help) "HP".
iPoseProof (help with "[$HP]") as "?". done.
Qed.
```
It says (notation printing due to this being in !791)
```
Error: Tactic failure: iPoseProof: (let R := True%I in R ∗ P -∗ Q) not a BI assertion.
```
If I move the ⊢ between `R ∗ P` and `Q`, it works, so this is related to bi_entails vs bi_emp_valid somehow.https://gitlab.mpi-sws.org/iris/iris/-/issues/303Canonical structures have major performance impact2022-08-12T14:48:02ZRobbert KrebbersCanonical structures have major performance impactAs I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and ...As I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and `bi` canonical structures.
- [37.40% overall on lambdarust-weak](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=masters%2Fweak_mem&var-commit1=bcc7c0be5ba2def0989d727c97d94a8492b9e40b&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi_weak&var-commit2=4ea92744abcd644f385696c398206a20a2cab7cf&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 72.22%.
- [23.28% overall on Iron](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iron&var-branch1=master&var-commit1=4dcc142742d846037be4cd94678ff8759465e6c1&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=37f90dd22db3ca477377d16ae72d761cb617412c&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 38.13%.
- [3.8% overall on Iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=9b2ad256fbf948933cdbf6c313eb244fd2439bf3&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=294ef2ef2df5478db81065f6cd5edc1d831419a1&var-config2=build-coq.8.11.0&var-group=().*&var-metric=instructions), with improvements for individual files up to 13.16%.
- [5.2% overall on lamdarust master](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=bea9f4a02efe48a38894fe1286add7ab25a2d2de&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 10.18%.
These differences are major, especially for the projects that use BI formers (monPred in lambdarust-weak and fracPred in Iron)! So it looks like there is really something we should investigate.https://gitlab.mpi-sws.org/iris/iris/-/issues/389Citation guide2020-12-08T17:17:32ZTej Chajedtchajed@gmail.comCitation guideThe docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.The docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.https://gitlab.mpi-sws.org/iris/iris/-/issues/341Coecisting fractional and persistent read-only ownership2020-08-25T09:34:48ZRalf Jungjung@mpi-sws.orgCoecisting fractional and persistent read-only ownershipAs part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Ri...As part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Right now, our encoding through `frac * agree T + agree T` (or equivalently `(frac + ()) * agree T`) requires ownership of the full fraction for that move.
I think such a construction is possible, but it requires https://gitlab.mpi-sws.org/iris/iris/-/issues/257. Then we could relate an authoritative map to a fragment that's more like `option (frac * agree T) * option (agree T)`, and ensure that the second `option` is `None` unless the sum of all fraction fragments is less than 1.https://gitlab.mpi-sws.org/iris/iris/-/issues/330Consider adding `iEnough` variants of `iAssert` ?2020-06-26T07:35:15ZPaolo G. GiarrussoConsider adding `iEnough` variants of `iAssert` ?Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first ...Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first last.
```
The point is just readability, and adding all the overloads is probably not worth it, but maybe this would change with an Ltac2 proofmode?https://gitlab.mpi-sws.org/iris/iris/-/issues/552Consider merging "examples" into this repository2023-11-20T13:53:20ZRalf Jungjung@mpi-sws.orgConsider merging "examples" into this repositoryWe now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one reposito...We now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one repository less that Robbert and me have to port changes to.
- People trying to fix Coq CI have one repository less to worry about.
Downsides:
- `make` will require Autosubst to fully work
- `make` in Iris will take quite a bit longer
- CI will take longer before a package is published in opam
I don't have a very strong opinion on this. Very rarely I make changes that break something in iris/examples in subtle ways and debugging that would be much easier in a mono repo. But most of the time the overhead from having two repositories is not so bad, and it's nice that people don't have to install Autosubst to make `make` work.https://gitlab.mpi-sws.org/iris/iris/-/issues/499Consistent error messages for internal IPM failures2023-04-12T14:51:54ZIke MulderConsistent error messages for internal IPM failuresThere are a couple of places where an IPM tactic could theoretically fail in strange cases.
The treatment of such cases is not consistent.
When defining a tactic in `ltac_tactics`, sideconditions of a lemma from `coq_tactics` that sho...There are a couple of places where an IPM tactic could theoretically fail in strange cases.
The treatment of such cases is not consistent.
When defining a tactic in `ltac_tactics`, sideconditions of a lemma from `coq_tactics` that should be always be solvable by a single tactic `tac`:
- are sometimes just handled with `tac`
- are sometimes handled as `tac || fail "some error message which might make clear that this should not happen"`
Some examples are in [iInduction](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/ltac_tactics.v#L2307), [iLöb](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/ltac_tactics.v#L2702) and [iPoseProofCoreLem](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/ltac_tactics.v#L869).
As discussed [here](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/872#note_86860), it would be nice if such cases were handled consistently.
A possible fix might look as follows:
```
Ltac iInternalFailMsg :=
idtac "Iris encountered an internal error! This is very bad!";
idtac "Please report a bug at https://gitlab.mpi-sws.org/iris/iris/-/issues ".
Ltac iExampleTac.
let H := constr:(I) in
iInternalFailMsg; fail "iTest: Something with" H "is off"
```
prepending `iInternalFailMsg` to all such `fail` statements.https://gitlab.mpi-sws.org/iris/iris/-/issues/276Create example user library and document library best practices2021-04-24T10:13:54ZRobbert KrebbersCreate example user library and document library best practicesDuring a discussion at MPI with @jung @haidang @lepigre @msammler, we figured it may be a good idea to make a sample file to demonstrate the various conventions in Iris.
Possible aspects the file could cover:
+ Section structure, defin...During a discussion at MPI with @jung @haidang @lepigre @msammler, we figured it may be a good idea to make a sample file to demonstrate the various conventions in Iris.
Possible aspects the file could cover:
+ Section structure, definitions outside of sections
+ Sealing
+ `Params`
+ `Typeclasses Opaque` versus `tc_opaque`
+ `inG` and `Σ`s
+ `Implicit Types`
+ Indenting, use of bullets, use of braces
+ Styles of WP and Texan Triple lemmas, e.g. use of binders, value pairshttps://gitlab.mpi-sws.org/iris/iris/-/issues/163Dealing with nested modalities in `iModIntro`2020-06-29T10:38:08ZRobbert KrebbersDealing with nested modalities in `iModIntro`We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 →...We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
```
This instance allows introduction of e.g. updates below `monPred_at`.
When we add a `FromModal` instance for `monPred_at P i`, we end up with ambiguity when introducing `monPred_at (|==> P) i`: should `|==>` or `monPred_at` be introduced?
Concretely, we should:
- [ ] Add a `FromModal` instance for `monPred_at`
- [ ] Get the priorities of that instance and e.g. the above `from_modal_monPred_at` right
- [x] Do the same for `embed`https://gitlab.mpi-sws.org/iris/iris/-/issues/224Define persistence otherwise (and get rid of core)2021-06-13T09:56:24ZRalf Jungjung@mpi-sws.orgDefine persistence otherwise (and get rid of core)As a preparatory step towards defining the persistence modality inside the logic (if reasonably possible), we could try to change the model of persistence in Iris to no longer use the core (and get rid of the core). As long as persisten...As a preparatory step towards defining the persistence modality inside the logic (if reasonably possible), we could try to change the model of persistence in Iris to no longer use the core (and get rid of the core). As long as persistence is the only connective defined using the core, it is impossible to define an equivalent connective inside the logic, so this is interesting both to simplify the RA axioms (and even more so the axioms for ordered RAs), and to work towards maybe eventually defining persistence inside the logic.
Cc @robbertkrebbers @jjourdan @jtassarohttps://gitlab.mpi-sws.org/iris/iris/-/issues/528Depend on Coq-elpi2023-08-02T09:51:46ZRobbert KrebbersDepend on Coq-elpiCoq-elpi might bring various benefits to Iris:
- We can use its [locker](https://github.com/LPCIC/coq-elpi/tree/master/apps/locker) to replace our sealing mechanism. As noticed in #527, locker might be more efficient, and it also reduce...Coq-elpi might bring various benefits to Iris:
- We can use its [locker](https://github.com/LPCIC/coq-elpi/tree/master/apps/locker) to replace our sealing mechanism. As noticed in #527, locker might be more efficient, and it also reduces the amount of boilerplate.
- We can use Elpi to create "deriving" like mechanisms, for example, for the infamous `inG` and `Σ` definitions.
- In the future we can investigate if we can use Elpi to implement parts of the Iris Proof mode more efficiently.
Coq-elpi is available in opam, and seems pretty stable. What do we think of letting Iris depend on Coq-elpi?https://gitlab.mpi-sws.org/iris/iris/-/issues/304Direction of _op lemmas is inconsistent with _(p)core, _valid, _included2021-12-06T20:17:41ZRalf Jungjung@mpi-sws.orgDirection of _op lemmas is inconsistent with _(p)core, _valid, _includedSee the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔...See the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
```
However, most of our `_op` lemmas push the named operation "out":
```coq
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
```
Moreover, even with one "group" of lemmas, not all are consistent: `singleton_op`, `discrete_fun_singleton_op`, `list_singleton_op` push "in", while `cmra_morphism_(p)core` push "out" (and there might be more).
At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the `_op` lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/303, so this starts to look like we are just going back and forth...https://gitlab.mpi-sws.org/iris/iris/-/issues/354Discardable camera improvements2020-10-09T13:50:33ZRalf Jungjung@mpi-sws.orgDiscardable camera improvements## Generalization
I think the variant of `dfrac` that I implemented with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531 can be generalized to a "discardable-anything":
```coq
Inductive discardable (A: cmraT) :=
| DOwn : A →...## Generalization
I think the variant of `dfrac` that I implemented with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531 can be generalized to a "discardable-anything":
```coq
Inductive discardable (A: cmraT) :=
| DOwn : A → dfrac
| DDiscarded : dfrac
| DBoth : A → dfrac.
```
with validity something like
```coq
Instance discardable_valid (A: cmraT) : Valid (discardable A) := λ x,
match x with
| DOwn q => ✓ q
| DDiscarded => True
| DBoth q => exists p, ✓ (q ⋅ p)
end%Qc.
```
I think this should work... what I am not sure about is if this is useful.^^
## old [discarded](https://gitlab.mpi-sws.org/iris/iris/-/issues/354#note_57686) idea: `option Qp`
After https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531, the public interface of `dfrac` can basically be described via a smart constructor that takes `option Qp` -- in fact I am adding such a notation in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486. We can probably rephrase all the existing lemmas in terms of that single constructor, and @robbertkrebbers agrees that that would make a better interface.
Cc @simonfv @tchajed