Various setoids lemmas for maps, lists, and option

This MR adds various setoid lemmas.

Primarily: it's often useful to turn a setoid equality into a Leibniz equality. For boring elements like None, nil, and empty we have ma ≡ None ↔ ma = None, l ≡ [] ↔ l = [], and m ≡ ∅ ↔ m = ∅. For other functions, this is a bit more complicated, but there are useful results nonetheless. For example:

Lemma Some_equiv_eq mx y : mx ≡ Some y ↔ ∃ y', mx = Some y' ∧ y' ≡ y.
Lemma app_equiv_eq l k1 k2 :
  l ≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡ k1 ∧ k2' ≡ k2.
Lemma map_union_equiv_eq (m1 m2a m2b : M A) :
  m1 ≡ m2a ∪ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∪ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.

This MR adds such lemmas for all map operations, some lists operations.

For Some we had like 4 variants of the lemma. I removed all of those, and created a new lemma equiv_Some that follows the scheme for the other operations.

---

Concrete changes

Option:

• Add Proper instances for union, union_with, intersection_with, and difference_with.
• Rename equiv_None → None_equiv_eq.
• Replace equiv_Some_inv_l, equiv_Some_inv_r, equiv_Some_inv_l', and equiv_Some_inv_r' by new lemma Some_equiv_eq that follows the pattern of other ≡-inversion lemmas: it uses a ↔ and puts the arguments of ≡ and = in consistent order.

List:

• Add ≡-inversion lemmas nil_equiv_eq, cons_equiv_eq, list_singleton_equiv_eq, and app_equiv_eq.
• Add lemmas Permutation_equiv and equiv_Permutation.

Maps:

• Add map_filter_proper
• Rename map_equiv_empty → map_empty_equiv_eq.
• Add ≡-inversion lemmas insert_equiv_eq, delete_equiv_eq, map_union_equiv_eq, etc.

added 12 commits

• 889f16ac...fc5f75e5 - 4 commits from branch master
• 43ae1a74 - Add lemmas `equiv_nil`, `equiv_cons`, `equiv_list_singleton`, `equiv_app`.
• d6073f3b - Clean up `equiv_Some` lemmas.
• 9ba77da6 - Move setoid lemmas for maps to bottom of file.
• 041e5fcd - Add lemma `map_filter_proper`.
• b1ae9a79 - `Proper`s for `union`, `union_with`, `intersection_with`, `difference_with` on `option`.
• a12e2279 - Inversion lemmas for setoids on maps.
• e0643c8a - Add lemmas `Permutation_equiv` and `equiv_Permutation`.
• 4f1f7778 - CHANGELOG.

Compare with previous version

I added lemmas Permutation_equiv and equiv_Permutation.

I also updated the CHANGELOG (and reorganized it a bit to have a more consistent list of all setoid-related changes).

added 2 commits

• 0ae98cf5 - Add lemmas `Permutation_equiv` and `equiv_Permutation`.
• be44569f - CHANGELOG.

Compare with previous version

added 2 commits

• c9a8da07 - Add lemmas `Permutation_equiv` and `equiv_Permutation`.
• c79d89c3 - CHANGELOG.

Compare with previous version

added 9 commits

• c79d89c3...3722f090 - 2 commits from branch master
• 65a379f3 - Add lemma `map_filter_proper`.
• afdc8633 - `Proper`s for `union`, `union_with`, `intersection_with`, `difference_with` on `option`.
• d6148a30 - Add lemmas `nil_equiv_eq`, `cons_equiv_eq`, `list_singleton_equiv_eq`, `app_equiv_eq`.
• c488cab8 - Rename `equiv_None` → `None_equiv_eq`, add `Some_equiv_eq` to replace prior lemmas.
• a588e72a - Inversion lemmas for setoids on maps.
• 237cfeac - Add lemmas `Permutation_equiv` and `equiv_Permutation`.
• 50b147c6 - CHANGELOG.

Compare with previous version

changed the description

added 1 commit

• 4b564874 - CHANGELOG.

Compare with previous version

added 1 commit

• e0c793be - CHANGELOG.

Compare with previous version

I updated the MR:

• The ≡-inversion lemmas as now consistently called operation_equiv_eq (as discussed with @jung in private)
• The MR description now lists the concrete changes (the CHANGELOG commit also performs some reorganization)

resolved all threads

Thanks a lot for the detailed description! LGTM.

merged

mentioned in commit 3bddee70

@iris-users This MR contains the following breaking changes:

• Rename equiv_None → None_equiv_eq.
• Replace equiv_Some_inv_l, equiv_Some_inv_r, equiv_Some_inv_l', and equiv_Some_inv_r' by new lemma Some_equiv_eq that follows the pattern of other ≡-inversion lemmas: it uses a ↔ and puts the arguments of ≡ and = in consistent order.
• Rename map_equiv_empty → map_empty_equiv_eq.