Discardable camera improvements
Generalization
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.^^
old discarded idea: option Qp
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.