Improve iCombine to derive validity properties of ghost state automatically

It would be great if iCombine was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if iCombine takes an extra (optional) gives clause, which provides extra persistent facts (if those exist).

For example, consider the following environment:

"H1" : l ↦{#q1} v1
"H2" : l ↦{#q2} v2

executing iCombine "H1 H2" as "H" gives %[Hq Hv] should replace "H1" and "H2" with "H": l ↦{#(q1 + q2)} v1 and introduces two new pure hypotheses Hq : q1 + q2 ≤ 1 and Hv : v1 = v2.

The roadmap for implementing this would be split into two merge requests:

1. Change FromSep to only be used for iSplit{L,R}, change iCombine to rely on two new typeclasses CombineSepAs and CombineSepGives.
   These would be defined as CombineSepAs P1 P2 P := P1 ∗ P2 ⊢ P where P1 P2 are input, P output
   and CombineSepGives P1 P2 := P1 ∗ P2 ⊢ <pers> R where P1 P2 are input, R output.
   This MR would provide some instances for stuff in base_logic.lib, mapsto.
   The new syntax would be iCombine "Hs" [as "H"] [gives "P"], where either the as clause or the gives clause must be present.
   • If as "H" is present, all hypotheses "Hs" will be replaced by "H", which can be an introduction pattern.
     If not present, all "Hs" are kept as is
   • If gives "P" is present, additionally learn persistent fact "P", which can be an introduction pattern. Also supports %? introduction if this fact is pure.
   • If more than two hypotheses are provided in "Hs", repeatedly run CombineSep with the accumulated results
   • There will be an additional boolean indicating whether CombineSepAs used the default instance.
2. Give general instance for own (= MR !771 (closed), addresses #251)

This is a summary of a discussion by @jung, @robbertkrebbers, @snyke7 and @gmalecha at the Iris Workshop. Let me know if I forgot something.