Explanation of Lawful Equality.

LawfulEquality.lean

import Batteries.Data.RBMap.Basic

open Batteries

-- `Ordering` is used instead of mainstream languages' approach with (-1, 0, 1) and consits of:
-- lt - less than (-1)
-- eq - equals (0)
-- gt - greater than (1)

-- This one sparks joy.
def compareIntGood (x y : Int) : Ordering :=
  if x < y then .lt
  else if x = y then .eq
  else .gt

-- This one does not spark joy.
def compareIntBad (x y : Int) : Ordering :=
  if x < y then .gt
  else if x = y then .lt
  else .eq

def xs : List (Int × String) :=
  [ (3, "drei")
  , (9, "neun")
  , (4, "vier")
  , (8, "acht")
  , (6, "sechs")
  ]

-- Here we pass the comparators:
def xsGood : RBMap Int String compareIntGood := RBMap.ofList xs compareIntGood
def xsBad : RBMap Int String compareIntBad := RBMap.ofList xs compareIntBad

#eval xsGood.find? 3 -- some "drei"
#eval xsBad.find? 3 -- none

def RBMapLawful (α β : Type) [LE α] [LT α] [BEq α] [Ord α] [LawfulOrd α] := RBMap α β compare

def xsBest : RBMapLawful Int String := RBMap.ofList xs compareIntGood

#eval xsBest.find? 3 -- some "drei"

/-
type mismatch
  RBMap.ofList xs compareIntBad
has type
  RBMap Int String compareIntBad : Type
but is expected to have type
  RBMapLawful Int String : Type
-/
def xsWorst : RBMapLawful Int String := RBMap.ofList xs compareIntBad