inductive Ordering : Type

The result of a comparison according to a total order.

The relationship between the compared items may be:

• Ordering.lt: less than
• Ordering.eq: equal
• Ordering.gt: greater than

• lt : Ordering

  Less than.

• eq : Ordering

  Equal.

• gt : Ordering

  Greater than.

instance instInhabitedOrdering : Inhabited Ordering

Equations

• instInhabitedOrdering = { default := instInhabitedOrdering.default }

def instInhabitedOrdering.default : Ordering

Equations

• instInhabitedOrdering.default = Ordering.lt

instance instDecidableEqOrdering : DecidableEq Ordering

Equations

• instDecidableEqOrdering x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instReprOrdering : Repr Ordering

Equations

• instReprOrdering = { reprPrec := instReprOrdering.repr }

def instReprOrdering.repr : Ordering → Nat → Std.Format

Equations

• instReprOrdering.repr Ordering.lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ordering.lt")).group prec✝
• instReprOrdering.repr Ordering.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ordering.eq")).group prec✝
• instReprOrdering.repr Ordering.gt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ordering.gt")).group prec✝

@[inline]

def Ordering.swap : Ordering → Ordering

Swaps less-than and greater-than ordering results.

Examples:

• Ordering.lt.swap = Ordering.gt
• Ordering.eq.swap = Ordering.eq
• Ordering.gt.swap = Ordering.lt

Equations

• Ordering.lt.swap = Ordering.gt
• Ordering.eq.swap = Ordering.eq
• Ordering.gt.swap = Ordering.lt

@[macro_inline]

def Ordering.then (a b : Ordering) : Ordering

If a and b are Ordering, then a.then b returns a unless it is .eq, in which case it returns b. Additionally, it has “short-circuiting” behavior similar to boolean &&: if a is not .eq then the expression for b is not evaluated.

This is a useful primitive for constructing lexicographic comparator functions. The deriving Ord syntax on a structure uses the Ord instance to compare each field in order, combining the results equivalently to Ordering.then.

Use compareLex to lexicographically combine two comparison functions.

Examples:

structure Person where
  name : String
  age : Nat

-- Sort people first by name (in ascending order), and people with the same name by age (in
-- descending order)
instance : Ord Person where
  compare a b := (compare a.name b.name).then (compare b.age a.age)

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Dana", 50⟩

Ordering.gt

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 50⟩

Ordering.gt

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 20⟩

Ordering.lt

Equations

• Ordering.eq.then b = b
• a.then b = a

noncomputable def Ordering.then' (a b : Ordering) : Ordering

Version of Ordering.then' for proof by reflection.

Equations

• a.then' b = Ordering.rec a b a a

@[inline]

def Ordering.isEq : Ordering → Bool

Checks whether the ordering is eq.

Equations

• Ordering.eq.isEq = true
• x✝.isEq = false

@[inline]

def Ordering.isNe : Ordering → Bool

Checks whether the ordering is not eq.

Equations

• Ordering.eq.isNe = false
• x✝.isNe = true

@[inline]

def Ordering.isLE : Ordering → Bool

Checks whether the ordering is lt or eq.

Equations

• Ordering.gt.isLE = false
• x✝.isLE = true

@[inline]

def Ordering.isLT : Ordering → Bool

Checks whether the ordering is lt.

Equations

• Ordering.lt.isLT = true
• x✝.isLT = false

@[inline]

def Ordering.isGT : Ordering → Bool

Checks whether the ordering is gt.

Equations

• Ordering.gt.isGT = true
• x✝.isGT = false

@[inline]

def Ordering.isGE : Ordering → Bool

Checks whether the ordering is gt or eq.

Equations

• Ordering.lt.isGE = false
• x✝.isGE = true

theorem Ordering.forall {p : Ordering → Prop} : (∀ (o : Ordering), p o) ↔ p lt ∧ p eq ∧ p gt

theorem Ordering.exists {p : Ordering → Prop} : (∃ (o : Ordering), p o) ↔ p lt ∨ p eq ∨ p gt

instance Ordering.instDecidableForallOfDecidablePred {p : Ordering → Prop} [DecidablePred p] : Decidable (∀ (o : Ordering), p o)

Equations

• Ordering.instDecidableForallOfDecidablePred = decidable_of_decidable_of_iff ⋯

instance Ordering.instDecidableExistsOfDecidablePred {p : Ordering → Prop} [DecidablePred p] : Decidable (∃ (o : Ordering), p o)

Equations

• Ordering.instDecidableExistsOfDecidablePred = decidable_of_decidable_of_iff ⋯

@[simp]

theorem Ordering.isLT_lt : lt.isLT = true

@[simp]

theorem Ordering.isLE_lt : lt.isLE = true

@[simp]

theorem Ordering.isEq_lt : lt.isEq = false

@[simp]

theorem Ordering.isNe_lt : lt.isNe = true

@[simp]

theorem Ordering.isGE_lt : lt.isGE = false

@[simp]

theorem Ordering.isGT_lt : lt.isGT = false

@[simp]

theorem Ordering.isLT_eq : eq.isLT = false

@[simp]

theorem Ordering.isLE_eq : eq.isLE = true

@[simp]

theorem Ordering.isEq_eq : eq.isEq = true

@[simp]

theorem Ordering.isNe_eq : eq.isNe = false

@[simp]

theorem Ordering.isGE_eq : eq.isGE = true

@[simp]

theorem Ordering.isGT_eq : eq.isGT = false

@[simp]

theorem Ordering.isLT_gt : gt.isLT = false

@[simp]

theorem Ordering.isLE_gt : gt.isLE = false

@[simp]

theorem Ordering.isEq_gt : gt.isEq = false

@[simp]

theorem Ordering.isNe_gt : gt.isNe = true

@[simp]

theorem Ordering.isGE_gt : gt.isGE = true

@[simp]

theorem Ordering.isGT_gt : gt.isGT = true

@[simp]

theorem Ordering.lt_beq_eq : (lt == eq) = false

@[simp]

theorem Ordering.lt_beq_gt : (lt == gt) = false

@[simp]

theorem Ordering.eq_beq_lt : (eq == lt) = false

@[simp]

theorem Ordering.eq_beq_gt : (eq == gt) = false

@[simp]

theorem Ordering.gt_beq_lt : (gt == lt) = false

@[simp]

theorem Ordering.gt_beq_eq : (gt == eq) = false

@[simp]

theorem Ordering.swap_lt : lt.swap = gt

@[simp]

theorem Ordering.swap_eq : eq.swap = eq

@[simp]

theorem Ordering.swap_gt : gt.swap = lt

theorem Ordering.eq_eq_of_isLE_of_isLE_swap {o : Ordering} : o.isLE = true → o.swap.isLE = true → o = eq

theorem Ordering.eq_eq_of_isGE_of_isGE_swap {o : Ordering} : o.isGE = true → o.swap.isGE = true → o = eq

theorem Ordering.eq_eq_of_isLE_of_isGE {o : Ordering} : o.isLE = true → o.isGE = true → o = eq

theorem Ordering.eq_eq_iff_isLE_and_isGE {o : Ordering} : o = eq ↔ o.isLE = true ∧ o.isGE = true

theorem Ordering.eq_swap_iff_eq_eq {o : Ordering} : o = o.swap ↔ o = eq

theorem Ordering.eq_eq_of_eq_swap {o : Ordering} : o = o.swap → o = eq

@[simp]

theorem Ordering.isLE_eq_false {o : Ordering} : o.isLE = false ↔ o = gt

@[simp]

theorem Ordering.isGE_eq_false {o : Ordering} : o.isGE = false ↔ o = lt

@[simp]

theorem Ordering.isNe_eq_false {o : Ordering} : o.isNe = false ↔ o = eq

@[simp]

theorem Ordering.isEq_eq_false {o : Ordering} : o.isEq = false ↔ ¬o = eq

@[simp]

theorem Ordering.swap_eq_gt {o : Ordering} : o.swap = gt ↔ o = lt

@[simp]

theorem Ordering.swap_eq_lt {o : Ordering} : o.swap = lt ↔ o = gt

@[simp]

theorem Ordering.swap_eq_eq {o : Ordering} : o.swap = eq ↔ o = eq

@[simp]

theorem Ordering.isLT_swap {o : Ordering} : o.swap.isLT = o.isGT

@[simp]

theorem Ordering.isLE_swap {o : Ordering} : o.swap.isLE = o.isGE

@[simp]

theorem Ordering.isEq_swap {o : Ordering} : o.swap.isEq = o.isEq

@[simp]

theorem Ordering.isNe_swap {o : Ordering} : o.swap.isNe = o.isNe

@[simp]

theorem Ordering.isGE_swap {o : Ordering} : o.swap.isGE = o.isLE

@[simp]

theorem Ordering.isGT_swap {o : Ordering} : o.swap.isGT = o.isLT

theorem Ordering.isLE_of_eq_lt {o : Ordering} : o = lt → o.isLE = true

theorem Ordering.isLE_of_eq_eq {o : Ordering} : o = eq → o.isLE = true

theorem Ordering.isGE_of_eq_gt {o : Ordering} : o = gt → o.isGE = true

theorem Ordering.isGE_of_eq_eq {o : Ordering} : o = eq → o.isGE = true

theorem Ordering.ne_eq_of_eq_lt {o : Ordering} : o = lt → o ≠ eq

theorem Ordering.ne_eq_of_eq_gt {o : Ordering} : o = gt → o ≠ eq

@[simp]

theorem Ordering.isLT_iff_eq_lt {o : Ordering} : o.isLT = true ↔ o = lt

@[simp]

theorem Ordering.isGT_iff_eq_gt {o : Ordering} : o.isGT = true ↔ o = gt

@[simp]

theorem Ordering.isEq_iff_eq_eq {o : Ordering} : o.isEq = true ↔ o = eq

@[simp]

theorem Ordering.isNe_iff_ne_eq {o : Ordering} : o.isNe = true ↔ ¬o = eq

theorem Ordering.isLE_iff_ne_gt {o : Ordering} : o.isLE = true ↔ ¬o = gt

theorem Ordering.isGE_iff_ne_lt {o : Ordering} : o.isGE = true ↔ ¬o = lt

theorem Ordering.isLE_iff_eq_lt_or_eq_eq {o : Ordering} : o.isLE = true ↔ o = lt ∨ o = eq

theorem Ordering.isGE_iff_eq_gt_or_eq_eq {o : Ordering} : o.isGE = true ↔ o = gt ∨ o = eq

theorem Ordering.isLT_eq_beq_lt {o : Ordering} : o.isLT = (o == lt)

theorem Ordering.isLE_eq_not_beq_gt {o : Ordering} : o.isLE = !o == gt

theorem Ordering.isLE_eq_isLT_or_isEq {o : Ordering} : o.isLE = (o.isLT || o.isEq)

theorem Ordering.isGT_eq_beq_gt {o : Ordering} : o.isGT = (o == gt)

theorem Ordering.isGE_eq_not_beq_lt {o : Ordering} : o.isGE = !o == lt

theorem Ordering.isGE_eq_isGT_or_isEq {o : Ordering} : o.isGE = (o.isGT || o.isEq)

theorem Ordering.isEq_eq_beq_eq {o : Ordering} : o.isEq = (o == eq)

theorem Ordering.isNe_eq_not_beq_eq {o : Ordering} : o.isNe = !o == eq

theorem Ordering.isNe_eq_isLT_or_isGT {o : Ordering} : o.isNe = (o.isLT || o.isGT)

@[simp]

theorem Ordering.not_isLT_eq_isGE {o : Ordering} : (!o.isLT) = o.isGE

@[simp]

theorem Ordering.not_isLE_eq_isGT {o : Ordering} : (!o.isLE) = o.isGT

@[simp]

theorem Ordering.not_isGT_eq_isLE {o : Ordering} : (!o.isGT) = o.isLE

@[simp]

theorem Ordering.not_isGE_eq_isLT {o : Ordering} : (!o.isGE) = o.isLT

@[simp]

theorem Ordering.not_isNe_eq_isEq {o : Ordering} : (!o.isNe) = o.isEq

theorem Ordering.not_isEq_eq_isNe {o : Ordering} : (!o.isEq) = o.isNe

theorem Ordering.ne_lt_iff_isGE {o : Ordering} : ¬o = lt ↔ o.isGE = true

theorem Ordering.ne_gt_iff_isLE {o : Ordering} : ¬o = gt ↔ o.isLE = true

@[simp]

theorem Ordering.swap_swap {o : Ordering} : o.swap.swap = o

@[simp]

theorem Ordering.swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂

theorem Ordering.swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap

theorem Ordering.then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt

theorem Ordering.then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt

@[simp]

theorem Ordering.then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq

theorem Ordering.isLT_then {o₁ o₂ : Ordering} : (o₁.then o₂).isLT = (o₁.isLT || o₁.isEq && o₂.isLT)

theorem Ordering.isEq_then {o₁ o₂ : Ordering} : (o₁.then o₂).isEq = (o₁.isEq && o₂.isEq)

theorem Ordering.isNe_then {o₁ o₂ : Ordering} : (o₁.then o₂).isNe = (o₁.isNe || o₂.isNe)

theorem Ordering.isGT_then {o₁ o₂ : Ordering} : (o₁.then o₂).isGT = (o₁.isGT || o₁.isEq && o₂.isGT)

@[simp]

theorem Ordering.lt_then {o : Ordering} : lt.then o = lt

@[simp]

theorem Ordering.gt_then {o : Ordering} : gt.then o = gt

@[simp]

theorem Ordering.eq_then {o : Ordering} : eq.then o = o

@[simp]

theorem Ordering.then_eq {o : Ordering} : o.then eq = o

@[simp]

theorem Ordering.then_self {o : Ordering} : o.then o = o

theorem Ordering.then_assoc (o₁ o₂ o₃ : Ordering) : (o₁.then o₂).then o₃ = o₁.then (o₂.then o₃)

theorem Ordering.isLE_then_iff_or {o₁ o₂ : Ordering} : (o₁.then o₂).isLE = true ↔ o₁ = lt ∨ o₁ = eq ∧ o₂.isLE = true

theorem Ordering.isLE_then_iff_and {o₁ o₂ : Ordering} : (o₁.then o₂).isLE = true ↔ o₁.isLE = true ∧ (o₁ = lt ∨ o₂.isLE = true)

theorem Ordering.isLE_left_of_isLE_then {o₁ o₂ : Ordering} : (o₁.then o₂).isLE = true → o₁.isLE = true

theorem Ordering.isGE_left_of_isGE_then {o₁ o₂ : Ordering} : (o₁.then o₂).isGE = true → o₁.isGE = true

instance Ordering.instAssociativeThen : Std.Associative «then»

instance Ordering.instIdempotentOpThen : Std.IdempotentOp «then»

instance Ordering.instLawfulIdentityThenEq : Std.LawfulIdentity «then» eq

theorem Ordering.then'_eq_then (a b : Ordering) : a.then' b = a.then b

@[inline]

def compareOfLessAndEq {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering

Uses decidable less-than and equality relations to find an Ordering.

In particular, if x < y then the result is Ordering.lt. If x = y then the result is Ordering.eq. Otherwise, it is Ordering.gt.

compareOfLessAndBEq uses BEq instead of DecidableEq.

Equations

• compareOfLessAndEq x y = if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt

@[inline]

def compareOfLessAndBEq {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering

Uses a decidable less-than relation and Boolean equality to find an Ordering.

In particular, if x < y then the result is Ordering.lt. If x == y then the result is Ordering.eq. Otherwise, it is Ordering.gt.

compareOfLessAndEq uses DecidableEq instead of BEq.

Equations

• compareOfLessAndBEq x y = if x < y then Ordering.lt else if (x == y) = true then Ordering.eq else Ordering.gt

@[inline]

def compareLex {α : Sort u_1} {β : Sort u_2} (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering

Compares a and b lexicographically by cmp₁ and cmp₂.

a and b are first compared by cmp₁. If this returns Ordering.eq, a and b are compared by cmp₂ to break the tie.

To lexicographically combine two Orderings, use Ordering.then.

Equations

• compareLex cmp₁ cmp₂ a b = (cmp₁ a b).then (cmp₂ a b)

@[simp]

theorem compareLex_eq_eq {α : Sort u_1} {cmp₁ cmp₂ : α → α → Ordering} {a b : α} : compareLex cmp₁ cmp₂ a b = Ordering.eq ↔ cmp₁ a b = Ordering.eq ∧ cmp₂ a b = Ordering.eq

theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α] (h : ∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) {x y : α} : compareOfLessAndEq x y = (compareOfLessAndEq y x).swap

theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (x y : α) : x < y ↔ ¬y < x ∧ x ≠ y

theorem compareOfLessAndEq_eq_swap {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) {x y : α} : compareOfLessAndEq x y = (compareOfLessAndEq y x).swap

@[simp]

theorem compareOfLessAndEq_eq_lt {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} : compareOfLessAndEq x y = Ordering.lt ↔ x < y

theorem compareOfLessAndEq_eq_eq {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (refl : ∀ (x : α), x ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) {x y : α} : compareOfLessAndEq x y = Ordering.eq ↔ x = y

theorem compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} (h : ∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) : compareOfLessAndEq x y = Ordering.gt ↔ y < x

theorem compareOfLessAndEq_eq_gt {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (x y : α) : compareOfLessAndEq x y = Ordering.gt ↔ y < x

theorem isLE_compareOfLessAndEq {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) {x y : α} : (compareOfLessAndEq x y).isLE = true ↔ x ≤ y

class Ord (α : Type u) : Type u

Ord α provides a computable total order on α, in terms of the compare : α → α → Ordering function.

Typically instances will be transitive, reflexive, and antisymmetric, but this is not enforced by the typeclass.

There is a derive handler, so appending deriving Ord to an inductive type or structure will attempt to create an Ord instance.

• compare : α → α → Ordering

  Compare two elements in α using the comparator contained in an [Ord α] instance.

theorem Ord.ext {α : Type u} {x y : Ord α} (compare : compare = compare) : x = y

theorem Ord.ext_iff {α : Type u} {x y : Ord α} : x = y ↔ compare = compare

@[inline]

def compareOn {β : Type u_1} {α : Sort u_2} [ord : Ord β] (f : α → β) (x y : α) : Ordering

Compares two values by comparing the results of applying a function.

In particular, x is compared to y by comparing f x and f y.

Examples:

• compareOn (·.length) "apple" "banana" = .lt
• compareOn (· % 3) 5 6 = .gt
• compareOn (·.foldl max 0) [1, 2, 3] [3, 2, 1] = .eq

Equations

• compareOn f x y = compare (f x) (f y)

instance instOrdNat : Ord Nat

Equations

• instOrdNat = { compare := fun (x y : Nat) => compareOfLessAndEq x y }

instance instOrdInt : Ord Int

Equations

• instOrdInt = { compare := fun (x y : Int) => compareOfLessAndEq x y }

instance instOrdBool : Ord Bool

Equations

• instOrdBool = { compare := fun (x x_1 : Bool) => match x, x_1 with | false, true => Ordering.lt | true, false => Ordering.gt | x, x_2 => Ordering.eq }

instance instOrdString : Ord String

Equations

• instOrdString = { compare := fun (x y : String) => compareOfLessAndEq x y }

instance instOrdFin (n : Nat) : Ord (Fin n)

Equations

• instOrdFin n = { compare := fun (x y : Fin n) => compare ↑x ↑y }

instance instOrdUInt8 : Ord UInt8

Equations

• instOrdUInt8 = { compare := fun (x y : UInt8) => compareOfLessAndEq x y }

instance instOrdUInt16 : Ord UInt16

Equations

• instOrdUInt16 = { compare := fun (x y : UInt16) => compareOfLessAndEq x y }

instance instOrdUInt32 : Ord UInt32

Equations

• instOrdUInt32 = { compare := fun (x y : UInt32) => compareOfLessAndEq x y }

instance instOrdUInt64 : Ord UInt64

Equations

• instOrdUInt64 = { compare := fun (x y : UInt64) => compareOfLessAndEq x y }

instance instOrdUSize : Ord USize

Equations

• instOrdUSize = { compare := fun (x y : USize) => compareOfLessAndEq x y }

instance instOrdChar : Ord Char

Equations

• instOrdChar = { compare := fun (x y : Char) => compareOfLessAndEq x y }

instance instOrdInt8 : Ord Int8

Equations

• instOrdInt8 = { compare := fun (x y : Int8) => compareOfLessAndEq x y }

instance instOrdInt16 : Ord Int16

Equations

• instOrdInt16 = { compare := fun (x y : Int16) => compareOfLessAndEq x y }

instance instOrdInt32 : Ord Int32

Equations

• instOrdInt32 = { compare := fun (x y : Int32) => compareOfLessAndEq x y }

instance instOrdInt64 : Ord Int64

Equations

• instOrdInt64 = { compare := fun (x y : Int64) => compareOfLessAndEq x y }

instance instOrdISize : Ord ISize

Equations

• instOrdISize = { compare := fun (x y : ISize) => compareOfLessAndEq x y }

instance instOrdBitVec {n : Nat} : Ord (BitVec n)

Equations

• instOrdBitVec = { compare := fun (x y : BitVec n) => compareOfLessAndEq x y }

instance instOrdOption {α : Type u_1} [Ord α] : Ord (Option α)

Equations

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

instance instOrdOrdering : Ord Ordering

Equations

• instOrdOrdering = { compare := compareOn fun (x : Ordering) => x.ctorIdx }

@[specialize #[]]

def List.compareLex {α : Type u_1} (cmp : α → α → Ordering) : List α → List α → Ordering

Equations

• List.compareLex cmp [] [] = Ordering.eq
• List.compareLex cmp [] x✝ = Ordering.lt
• List.compareLex cmp x✝ [] = Ordering.gt
• List.compareLex cmp (x_2 :: xs) (y :: ys) = match cmp x_2 y with | Ordering.lt => Ordering.lt | Ordering.eq => List.compareLex cmp xs ys | Ordering.gt => Ordering.gt

instance List.instOrd {α : Type u_1} [Ord α] : Ord (List α)

Equations

• List.instOrd = { compare := List.compareLex compare }

theorem List.compare_eq_compareLex {α : Type u_1} [Ord α] : compare = List.compareLex compare

theorem List.compareLex_cons_cons {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {xs ys : List α} : List.compareLex cmp (x :: xs) (y :: ys) = (cmp x y).then (List.compareLex cmp xs ys)

@[simp]

theorem List.compare_cons_cons {α : Type u_1} [Ord α] {x y : α} {xs ys : List α} : compare (x :: xs) (y :: ys) = (compare x y).then (compare xs ys)

theorem List.compareLex_nil_cons {α : Type u_1} {cmp : α → α → Ordering} {x : α} {xs : List α} : List.compareLex cmp [] (x :: xs) = Ordering.lt

@[simp]

theorem List.compare_nil_cons {α : Type u_1} [Ord α] {x : α} {xs : List α} : compare [] (x :: xs) = Ordering.lt

theorem List.compareLex_cons_nil {α : Type u_1} {cmp : α → α → Ordering} {x : α} {xs : List α} : List.compareLex cmp (x :: xs) [] = Ordering.gt

@[simp]

theorem List.compare_cons_nil {α : Type u_1} [Ord α] {x : α} {xs : List α} : compare (x :: xs) [] = Ordering.gt

theorem List.compareLex_nil_nil {α : Type u_1} {cmp : α → α → Ordering} : List.compareLex cmp [] [] = Ordering.eq

@[simp]

theorem List.compare_nil_nil {α : Type u_1} [Ord α] : compare [] [] = Ordering.eq

theorem List.isLE_compareLex_nil_left {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} : (List.compareLex cmp [] xs).isLE = true

theorem List.isLE_compare_nil_left {α : Type u_1} [Ord α] {xs : List α} : (compare [] xs).isLE = true

theorem List.isLE_compareLex_nil_right {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} : (List.compareLex cmp xs []).isLE = true ↔ xs = []

@[simp]

theorem List.isLE_compare_nil_right {α : Type u_1} [Ord α] {xs : List α} : (compare xs []).isLE = true ↔ xs = []

theorem List.isGE_compareLex_nil_left {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} : (List.compareLex cmp [] xs).isGE = true ↔ xs = []

@[simp]

theorem List.isGE_compare_nil_left {α : Type u_1} [Ord α] {xs : List α} : (compare [] xs).isGE = true ↔ xs = []

theorem List.isGE_compareLex_nil_right {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} : (List.compareLex cmp xs []).isGE = true

theorem List.isGE_compare_nil_right {α : Type u_1} [Ord α] {xs : List α} : (compare xs []).isGE = true

theorem List.compareLex_nil_left_eq_eq {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} : List.compareLex cmp [] xs = Ordering.eq ↔ xs = []

@[simp]

theorem List.compare_nil_left_eq_eq {α : Type u_1} [Ord α] {xs : List α} : compare [] xs = Ordering.eq ↔ xs = []

theorem List.compareLex_nil_right_eq_eq {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} : List.compareLex cmp xs [] = Ordering.eq ↔ xs = []

@[simp]

theorem List.compare_nil_right_eq_eq {α : Type u_1} [Ord α] {xs : List α} : compare xs [] = Ordering.eq ↔ xs = []

@[specialize #[]]

def Array.compareLex {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) : Ordering

Equations

• Array.compareLex cmp a₁ a₂ = Array.compareLex.go✝ cmp a₁ a₂ 0

instance Array.instOrd {α : Type u_1} [Ord α] : Ord (Array α)

Equations

• Array.instOrd = { compare := Array.compareLex compare }

theorem Array.compare_eq_compareLex {α : Type u_1} [Ord α] : compare = Array.compareLex compare

theorem List.compareLex_eq_compareLex_toArray {α : Type u_1} {cmp : α → α → Ordering} {l₁ l₂ : List α} : List.compareLex cmp l₁ l₂ = Array.compareLex cmp l₁.toArray l₂.toArray

theorem List.compare_eq_compare_toArray {α : Type u_1} [Ord α] {l₁ l₂ : List α} : compare l₁ l₂ = compare l₁.toArray l₂.toArray

theorem Array.compareLex_eq_compareLex_toList {α : Type u_1} {cmp : α → α → Ordering} {a₁ a₂ : Array α} : Array.compareLex cmp a₁ a₂ = List.compareLex cmp a₁.toList a₂.toList

theorem Array.compare_eq_compare_toList {α : Type u_1} [Ord α] {a₁ a₂ : Array α} : compare a₁ a₂ = compare a₁.toList a₂.toList

def Vector.compareLex {α : Type u_1} {n : Nat} (cmp : α → α → Ordering) (a b : Vector α n) : Ordering

Equations

• Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray

instance Vector.instOrd {α : Type u_1} {n : Nat} [Ord α] : Ord (Vector α n)

Equations

• Vector.instOrd = { compare := Vector.compareLex compare }

theorem Vector.compareLex_eq_compareLex_toArray {α : Type u_1} {n : Nat} {cmp : α → α → Ordering} {a b : Vector α n} : Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray

theorem Vector.compareLex_eq_compareLex_toList {α : Type u_1} {n : Nat} {cmp : α → α → Ordering} {a b : Vector α n} : Vector.compareLex cmp a b = List.compareLex cmp a.toList b.toList

theorem Vector.compare_eq_compare_toArray {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} : compare a b = compare a.toArray b.toArray

theorem Vector.compare_eq_compare_toList {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} : compare a b = compare a.toList b.toList

def lexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] : Ord (α × β)

The lexicographic order on pairs.

Equations

• lexOrd = { compare := compareLex (compareOn fun (x : α × β) => x.fst) (compareOn fun (x : α × β) => x.snd) }

def beqOfOrd {α : Type u_1} [Ord α] : BEq α

Constructs an BEq instance from an Ord instance that asserts that the result of compare is Ordering.eq.

Equations

• beqOfOrd = { beq := fun (a b : α) => (compare a b).isEq }

def ltOfOrd {α : Type u_1} [Ord α] : LT α

Constructs an LT instance from an Ord instance that asserts that the result of compare is Ordering.lt.

Equations

• ltOfOrd = { lt := fun (a b : α) => compare a b = Ordering.lt }

@[inline]

instance instDecidableRelLt {α : Type u_1} [Ord α] : DecidableRel LT.lt

Equations

• instDecidableRelLt a b = decidable_of_bool (compare a b).isLT ⋯

def leOfOrd {α : Type u_1} [Ord α] : LE α

Constructs an LT instance from an Ord instance that asserts that the result of compare satisfies Ordering.isLE.

Equations

• leOfOrd = { le := fun (a b : α) => (compare a b).isLE = true }

@[inline]

instance instDecidableRelLe {α : Type u_1} [Ord α] : DecidableRel LE.le

Equations

• instDecidableRelLe x✝¹ x✝ = instDecidableEqBool (compare x✝¹ x✝).isLE true

@[reducible, inline]

abbrev Ord.toBEq {α : Type u_1} (ord : Ord α) : BEq α

Constructs a BEq instance from an Ord instance.

Equations

• ord.toBEq = beqOfOrd

@[reducible, inline]

abbrev Ord.toLT {α : Type u_1} (ord : Ord α) : LT α

Constructs an LT instance from an Ord instance.

Equations

• ord.toLT = ltOfOrd

@[reducible, inline]

abbrev Ord.toLE {α : Type u_1} (ord : Ord α) : LE α

Constructs an LE instance from an Ord instance.

Equations

• ord.toLE = leOfOrd

def Ord.opposite {α : Type u_1} (ord : Ord α) : Ord α

Inverts the order of an Ord instance.

The result is an Ord α instance that returns Ordering.lt when ord would return Ordering.gt and that returns Ordering.gt when ord would return Ordering.lt.

Equations

• ord.opposite = { compare := fun (x y : α) => compare y x }

def Ord.on {β : Type u_1} {α : Type u_2} : Ord β → (f : α → β) → Ord α

Constructs an Ord instance that compares values according to the results of f.

In particular, ord.on f compares x and y by comparing f x and f y according to ord.

The function compareOn can be used to perform this comparison without constructing an intermediate Ord instance.

Equations

• x✝.on f = { compare := compareOn f }

@[reducible, inline]

abbrev Ord.lex {α : Type u_1} {β : Type u_2} : Ord α → Ord β → Ord (α × β)

Constructs the lexicographic order on products α × β from orders for α and β.

Equations

• x✝¹.lex x✝ = lexOrd

def Ord.lex' {α : Type u_1} (ord₁ ord₂ : Ord α) : Ord α

Constructs an Ord instance from two existing instances by combining them lexicographically.

The resulting instance compares elements first by ord₁ and then, if this returns Ordering.eq, by ord₂.

The function compareLex can be used to perform this comparison without constructing an intermediate Ord instance. Ordering.then can be used to lexicographically combine the results of comparisons.

Equations

• ord₁.lex' ord₂ = { compare := compareLex compare compare }