Make `_iff` and `_alter` lemmas for invariants consistent, and add `_iff` lemma for locks
_iff lemma and contractive instance for
is_lock were missing. This MR adds these.
_alter lemmas for invariants had their arguments in inconsistent order. This MR makes them consistent with e.g.,
wp_wand. For example,
inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q.