class Lake.EqOfCmp (α : Type u) (cmp : α → α → Ordering) : Type

Proof that the equality of a compare function corresponds to propositional equality.

• eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'

class Lake.LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends Lake.EqOfCmp : Type

Proof that the equality of a compare function corresponds to propositional equality and vice versa.

• eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'
• cmp_rfl : ∀ {a : α}, cmp a a = Ordering.eq

@[simp]

theorem Lake.cmp_iff_eq {α : Type u_1} {cmp : α → α → Ordering} {a : α} {a' : α} [Lake.LawfulCmpEq α cmp] : cmp a a' = Ordering.eq ↔ a = a'

class Lake.EqOfCmpWrt (α : Type u) {β : Type v} (f : α → β) (cmp : α → α → Ordering) : Type

Proof that the equality of a compare function corresponds to propositional equality with respect to a given function.

• eq_of_cmp_wrt : ∀ {a a' : α}, cmp a a' = Ordering.eq → f a = f a'

instance Lake.instEqOfCmpWrtType {α : Type u_1} {cmp : α → α → Ordering} : Lake.EqOfCmpWrt α (fun (x : α) => α) cmp

Equations

• Lake.instEqOfCmpWrtType = { eq_of_cmp_wrt := (_ : ∀ {a a' : α}, cmp a a' = Ordering.eq → α = α) }

instance Lake.instEqOfCmpWrt {α : Type u_1} {cmp : α → α → Ordering} : {β : Type u_2} → {f : α → β} → [inst : Lake.EqOfCmp α cmp] → Lake.EqOfCmpWrt α f cmp

Equations

• Lake.instEqOfCmpWrt = { eq_of_cmp_wrt := (_ : ∀ {a a' : α}, cmp a a' = Ordering.eq → f a = f a') }

instance Lake.instEqOfCmp {α : Type u_1} {cmp : α → α → Ordering} [Lake.EqOfCmpWrt α (fun (a : α) => a) cmp] : Lake.EqOfCmp α cmp

Equations

• Lake.instEqOfCmp = { eq_of_cmp := (_ : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a') }

theorem Lake.eq_of_compareOfLessAndEq {α : Type u_1} [LT α] [DecidableEq α] {a : α} {a' : α} [Decidable (a < a')] (h : compareOfLessAndEq a a' = Ordering.eq) : a = a'

theorem Lake.compareOfLessAndEq_rfl {α : Type u_1} [LT α] [DecidableEq α] {a : α} [Decidable (a < a)] (lt_irrefl : ¬a < a) : compareOfLessAndEq a a = Ordering.eq

instance Lake.instLawfulCmpEqNatCompareInstOrdNat : Lake.LawfulCmpEq Nat compare

Equations

• Lake.instLawfulCmpEqNatCompareInstOrdNat = Lake.LawfulCmpEq.mk @Lake.instLawfulCmpEqNatCompareInstOrdNat.proof_2

theorem Lake.Fin.eq_of_compare {m : Nat} {n : Fin m} {n' : Fin m} (h : compare n n' = Ordering.eq) : n = n'

instance Lake.instLawfulCmpEqFinCompareInstOrdFin {n : Nat} : Lake.LawfulCmpEq (Fin n) compare

Equations

• Lake.instLawfulCmpEqFinCompareInstOrdFin = Lake.LawfulCmpEq.mk (_ : ∀ {a : Fin n}, compareOfLessAndEq a.val a.val = Ordering.eq)

instance Lake.instLawfulCmpEqUInt64CompareInstOrdUInt64 : Lake.LawfulCmpEq UInt64 compare

Equations

• Lake.instLawfulCmpEqUInt64CompareInstOrdUInt64 = Lake.LawfulCmpEq.mk @Lake.instLawfulCmpEqUInt64CompareInstOrdUInt64.proof_2

theorem Lake.List.lt_irrefl {α : Type u_1} [LT α] (irrefl_α : ∀ (a : α), ¬a < a) (a : List α) : ¬a < a

@[simp]

theorem Lake.String.lt_irrefl (s : String) : ¬s < s

instance Lake.instLawfulCmpEqStringCompareInstOrdString : Lake.LawfulCmpEq String compare

Equations

• Lake.instLawfulCmpEqStringCompareInstOrdString = Lake.LawfulCmpEq.mk @Lake.instLawfulCmpEqStringCompareInstOrdString.proof_2

@[macro_inline]

def Lake.Option.compareWith {α : Type u_1} (cmp : α → α → Ordering) : Option α → Option α → Ordering

Equations

• Lake.Option.compareWith cmp x✝ x = match x✝, x with | none, none => Ordering.eq | none, some val => Ordering.lt | some val, none => Ordering.gt | some x, some y => cmp x y

instance Lake.instEqOfCmpOptionCompareWith {α : Type u_1} {cmp : α → α → Ordering} [Lake.EqOfCmp α cmp] : Lake.EqOfCmp (Option α) (Lake.Option.compareWith cmp)

Equations

• Lake.instEqOfCmpOptionCompareWith = { eq_of_cmp := (_ : ∀ {o o' : Option α}, Lake.Option.compareWith cmp o o' = Ordering.eq → o = o') }

instance Lake.instLawfulCmpEqOptionCompareWith {α : Type u_1} {cmp : α → α → Ordering} [Lake.LawfulCmpEq α cmp] : Lake.LawfulCmpEq (Option α) (Lake.Option.compareWith cmp)

Equations

• Lake.instLawfulCmpEqOptionCompareWith = Lake.LawfulCmpEq.mk (_ : ∀ {o : Option α}, Lake.Option.compareWith cmp o o = Ordering.eq)

def Lake.Prod.compareWith {α : Type u_1} {β : Type u_2} (cmpA : α → α → Ordering) (cmpB : β → β → Ordering) : α × β → α × β → Ordering

Equations

• Lake.Prod.compareWith cmpA cmpB x✝ x = match x✝ with | (a, b) => match x with | (a', b') => match cmpA a a' with | Ordering.eq => cmpB b b' | ord => ord

instance Lake.instEqOfCmpProdCompareWith {α : Type u_1} {cmpA : α → α → Ordering} {β : Type u_2} {cmpB : β → β → Ordering} [Lake.EqOfCmp α cmpA] [Lake.EqOfCmp β cmpB] : Lake.EqOfCmp (α × β) (Lake.Prod.compareWith cmpA cmpB)

Equations

• Lake.instEqOfCmpProdCompareWith = { eq_of_cmp := (_ : ∀ {h : α × β} {a' : α × β}, Lake.Prod.compareWith cmpA cmpB h a' = Ordering.eq → h = a') }

instance Lake.instLawfulCmpEqProdCompareWith {α : Type u_1} {cmpA : α → α → Ordering} {β : Type u_2} {cmpB : β → β → Ordering} [Lake.LawfulCmpEq α cmpA] [Lake.LawfulCmpEq β cmpB] : Lake.LawfulCmpEq (α × β) (Lake.Prod.compareWith cmpA cmpB)

Equations

• One or more equations did not get rendered due to their size.