Draft: Add simplification machinery for ✓ and ≼.

This merge request partially addresses issue #251 .

Concretely, this merge request adds an iCombineOwn tactic. In the following environment:

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

executing iCombineOwn "Hγ1 Hγ2" as "Hγ" gives %[Hq HE] should 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.

The "as" clause is optional. This is especially useful when you want to combine validity information for a ● and a ◯. In the following environment:

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

executing iCombineOwn "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.

Some current issues:

• Does not simplify equivalences. If directly using rewrites in introduction patterns, may cause slowdowns. Currently an explicit %leibniz_equiv on the equality is needed for faster rewrites.
• Some lemmas I used on validity and equivalence of views are still lying around in an awkward place.
• Documentation is missing
• 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.

Feedback is most welcome! I wasn't really sure where to place some of this stuff, so it currently resides in iris/base_logic/.