Skip to content

Improve iCombine to allow a 'gives' clause for validity properties

Ike Mulder requested to merge snyke7/iris:ike/better-combine into master

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.

Merge request reports