add pair_equiv

When having H: (a1, b1) ≡ (a2, b2), it's actually rather annoying to rewrite an a1 in the goal:

destruct H as [H _]; simpl in H; rewrite H

This is because destructing H yields (a1, b1).1 ≡ (a2, b2).1.

So a lemma like this could be useful, then we should be able to do apply pair_equiv in H as [-> _].

This looks like a useful lemma. Some comments:

• We should also have a version for eq (in std++) and dist (in Iris).
• For the first, there is pair_equal_spec : (a1, b1) = (a2, b2) ↔ a1 = a2 ∧ b1 = b2 in stdlib. I don't particularly like that name since it does not involve eq so does not scale to dist and equiv. We might as well make a copy for eq in std++.

Where would that eq veresion go?

added 1 commit

• b63074db - add pair_eq

Compare with previous version

resolved all threads

mentioned in merge request iris!961 (merged)

LGTM. Feel free to merge if you agree with my comment.

resolved all threads

added 1 commit

• 08d238fd - repeat ourselves

Compare with previous version

enabled an automatic merge when the pipeline for 08d238fd succeeds

merged

mentioned in commit 14322a17