Skip to content

Various setoids lemmas for maps, lists, and option

Robbert Krebbers requested to merge robbert/setoid into master

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


  • Add Proper instances for union, union_with, intersection_with, and difference_with.
  • Rename equiv_NoneNone_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.


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


  • Add map_filter_proper
  • Rename map_equiv_emptymap_empty_equiv_eq.
  • Add ≡-inversion lemmas insert_equiv_eq, delete_equiv_eq, map_union_equiv_eq, etc.
Edited by Robbert Krebbers

Merge request reports