Lake.Util.Compare

source

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'

Instances

source

theorem Lake.EqOfCmp.eq_of_cmp {α : Type u} {cmp : α → α → Ordering} [self : Lake.EqOfCmp α cmp] {a : α} {a' : α} :

cmp a a' = Ordering.eq → a = a'

source

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

Instances

source

@[simp]

theorem Lake.LawfulCmpEq.cmp_rfl {α : Type u} {cmp : α → α → Ordering} [self : Lake.LawfulCmpEq α cmp] {a : α} :

cmp a a = Ordering.eq

source

@[simp]

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

cmp a a' = Ordering.eq ↔ a = a'

source

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'

Instances

source

theorem Lake.EqOfCmpWrt.eq_of_cmp_wrt {α : Type u} {β : Type v} {f : α → β} {cmp : α → α → Ordering} [self : Lake.EqOfCmpWrt α f cmp] {a : α} {a' : α} :

cmp a a' = Ordering.eq → f a = f a'

source

instance Lake.instEqOfCmpWrt {α : Type u_1} {cmp : α → α → Ordering} :

Lake.EqOfCmpWrt α (fun (x : α) => α) cmp

Equations

Lake.instEqOfCmpWrt = { eq_of_cmp_wrt := ⋯ }

source

instance Lake.instEqOfCmpWrtOfEqOfCmp {α : Type u_1} {cmp : α → α → Ordering} :

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

Equations

Lake.instEqOfCmpWrtOfEqOfCmp = { eq_of_cmp_wrt := ⋯ }

source

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

Lake.EqOfCmp α cmp

Equations

Lake.instEqOfCmpOfEqOfCmpWrt = { eq_of_cmp := ⋯ }

source

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

a = a'

source

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

compareOfLessAndEq a a = Ordering.eq

source

instance Lake.instLawfulCmpEqNatCompare :

Lake.LawfulCmpEq Nat compare

Equations

Lake.instLawfulCmpEqNatCompare = Lake.LawfulCmpEq.mk @Lake.instLawfulCmpEqNatCompare.proof_2

source

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

n = n'

source

instance Lake.instLawfulCmpEqFinCompare {n : Nat} :

Lake.LawfulCmpEq (Fin n) compare

Equations

Lake.instLawfulCmpEqFinCompare = Lake.LawfulCmpEq.mk ⋯

source

instance Lake.instLawfulCmpEqUInt64Compare :

Lake.LawfulCmpEq UInt64 compare

Equations

Lake.instLawfulCmpEqUInt64Compare = Lake.LawfulCmpEq.mk @Lake.instLawfulCmpEqUInt64Compare.proof_2

source

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

¬a < a

source

@[simp]

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

¬s < s

source

instance Lake.instLawfulCmpEqStringCompare :

Lake.LawfulCmpEq String compare

Equations

Lake.instLawfulCmpEqStringCompare = Lake.LawfulCmpEq.mk @Lake.instLawfulCmpEqStringCompare.proof_2

source

@[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

Instances For

source

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

Lake.EqOfCmp (Option α) (Lake.Option.compareWith cmp)

Equations

Lake.instEqOfCmpOptionCompareWith = { eq_of_cmp := ⋯ }

source

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

Lake.LawfulCmpEq (Option α) (Lake.Option.compareWith cmp)

Equations

Lake.instLawfulCmpEqOptionCompareWith = Lake.LawfulCmpEq.mk ⋯

source

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

Instances For

source

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 := ⋯ }

source

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

Lake.instLawfulCmpEqProdCompareWith = Lake.LawfulCmpEq.mk ⋯