Make `_iff` and `_alter` lemmas for invariants consistent, and add `_iff` lemma for locks

The _iff lemma and contractive instance for is_lock were missing. This MR adds these.

The _iff and _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.