Improve iCombine to allow a 'gives' clause for validity properties
This MR takes the first step towards fixing #460.
It extends the iCombine
tactic with an (optional) gives
clause, which can be used to obtain extra validity information. For example:
Lemma mapsto_combine_2 l v1 q1 v2 q2 :
l ↦{#q1} v1 -∗ l ↦{#q2} v2 -∗ l ↦{#(q1 + q2)} v1 ∗ ⌜q1 + q2 ≤ 1⌝%Qp ∗ ⌜v1 = v2⌝.
Proof. iIntros "H1 H2". by iCombine "H1 H2" as "$" gives %[? ->]. Qed.
Behind the scenes, it changes iCombine
to no longer rely on FromSep
, but on new typeclasses CombineSepAs
and CombineSepGives
.
These compute the simplified hypothesis gotten with as
or gives
, respectively.
iCombine
can now also be used with just a gives
clause.
This allows for some slightly shorter proofs:
instead of iDestruct (own_valid_2 with "H1 H2") as %?
or iDestruct (mapsto_valid_2 with "H1 H2") as %?
, one can now use iCombine "H1 H2" gives %?
in both cases.