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_equivon 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/.