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.

changed title from Make _iff and _alter lemmas for invariants consistent, and add such a lemma for locks to Make _iff and _alter lemmas for invariants consistent, and add {+_iff+} lemma for locks

changed the description

resolved all threads

LGTM.

@iris-users this is a breaking change for cinv_iff, inv_alter, inv_iff, na_inv_iff.

@robbertkrebbers maybe the changelog should list explicitly (for grepping purposes) which lemmas actually change here.

added 12 commits

• 6a8975fc...ae0b5798 - 8 commits from branch master
• 92eaf4f9 - Prove that `is_lock` is contractive.
• df8e3df5 - Make `_iff` and `_alter` lemmas for invariants consistent.
• 13b6713d - Add rule `is_lock_iff` for locks.
• 31d5df29 - CHANGELOG.

Compare with previous version

resolved all threads

@robbertkrebbers maybe the changelog should list explicitly (for grepping purposes) which lemmas actually change here.

Done.

Ah inv_alter did not change actually.

LGTM, feel free to merge.

mentioned in commit 0ccaa796

merged