Skip to content
GitLab

Define `Proper` for `dom` and enable `iRewrite` on goals involving `dom`

Merged Robbert Krebbers requested to merge robbert/iRewrite_dom into master

This MR enables rewrite with a step-indexed equality on maps in a goal involving dom. For example:

Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
  m1 ≡ m2 ⊢@{PROP}
  ⌜ dom (gset nat) m1 = dom (gset nat) m2 ⌝.
Proof. iIntros "H". by iRewrite "H". Qed.

Note that the Proper instance is a bit different from the one I suggested at Mattermost. The version in this MR does not involve the OFE for gset, and is more consistent withthe Proper instances for e.g., is_Some.