# 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.

Edited by Robbert Krebbers