Discardable camera improvements
I think the variant of
dfrac that I implemented with !531 (merged) can be generalized to a "discardable-anything":
Inductive discardable (A: cmraT) := | DOwn : A → dfrac | DDiscarded : dfrac | DBoth : A → dfrac.
with validity something like
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.^^
After !531 (merged), 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 !486 (merged). We can probably rephrase all the existing lemmas in terms of that single constructor, and @robbertkrebbers agrees that that would make a better interface.