Draft: Improve validity information received from `iCombine`ing `own`s

Draft MR for addressing #251 and #460. This is basically !771 (closed), but rebuilt on top of the CombineSepAs and CombineSepGives typeclasses from !872 (merged).

In the following environment:

"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)

executing iCombine "Hγ1 Hγ2" as "Hγ" gives %[Hq HE] will now replace "Hγ1" and "Hγ2" with a new hypothesis "Hγ" : own γ (q1 + q2, GSet (E1 ∪ E2)) and two pure hypotheses: Hq : q1 + q2 ≤ 1 and HE : E1 ## E2. In the following environment:

"Hγ1" : own γ (◯ (Some (q1, GSet E1)))
"Hγ2" : own γ (● (Some (q2, GSet E2)))

executing iCombine "Hγ1 Hγ2" gives %H should give you a new pure hypotheses H : q1 ≤ q2 ∧ E1 ⊆ E2 ∧ ((q1 < q2) ∨ (q1 ≡ q2 ∧ E1 ≡ E2)).

It works by adding three typeclasses, IsValidOp, IsValidGives and IsIncluded, which try to determine an iProp that simplifies ✓ or ≼. Since we are looking for an iProp, not a pure proposition, this approach also works for higher-order ghost state.

Engineering questions:

• The current approach does not simplify equivalences. If directly using rewrites in introduction patterns, this may cause slowdowns. Currently an explicit %leibniz_equiv on the equality is needed for faster rewrites. Fixing this would require an additional typeclass or some such for doing the simplification beforehand. For now, Robbert and I propose to leave this as such, and instead improve the IntoPure instance.

Style/MR questions:

• Does not yet have instances for all CMRA building blocks provided in iris/algebra, but at least supports the ones used inside the iris repository, and some others I have used in the past. How complete should this be?
• I needed some additional lemmas to simplify internal validity of e.g. viewR. Should these be upstreamed in a separate MR? They might not very nicely mesh with Robberts siProp, since they lift the view_rel to the logic, which only works for uPred currently.

TODO:

• Documentation is missing
• Tests are still missing
• List CMRA building blocks for which support is missing
• I added additional IsOp instances for gset, gmultiset and gmap, need to wait for MR !1004.
• I added some lemmas about IdFree at the logic level, need to wait for MR !1005 (merged).
• I added additional MakeOr instances for simplifying e.g. False ∨ P, need to wait for MR !940 (merged).
• I am using ∗-∗ in IsIncluded to make sure I'm not dropping information. I sometimes make use of the transitivity of this, need to wait for MR !941 (merged).
• I needed some additional lemmas to simplify internal validity of e.g. dfracR and authR, need to wait for MR !942 (merged).
• Improve the IntoPure instance for leibniz equivalences in a separate MR, need to wait for MR !966 (merged).
• Add ≼ on the BI level, need to wait for !944 (merged).
• Remove reservation_map support for now.

Feedback is most welcome!