GitLab

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.