Documentation

Init.Data.Ord

inductive Ordering :

The result of a comparison according to a total order.

The relationship between the compared items may be:

Instances For
Equations
@[inline]

Swaps less-than and greater-than ordering results.

Examples:

Equations
@[macro_inline]

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
Instances For
@[inline]

Checks whether the ordering is eq.

Equations
@[inline]

Checks whether the ordering is not eq.

Equations
@[inline]

Checks whether the ordering is lt or eq.

Equations
@[inline]

Checks whether the ordering is lt.

Equations
@[inline]

Checks whether the ordering is gt.

Equations
@[inline]

Checks whether the ordering is gt or eq.

Equations
theorem Ordering.forall {p : OrderingProp} :
(∀ (o : Ordering), p o) p lt p eq p gt
theorem Ordering.exists {p : OrderingProp} :
( (o : Ordering), p o) p lt p eq p gt
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[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} :
@[simp]
theorem Ordering.gt_then {o : Ordering} :
@[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 = trueo₁.isLE = true
theorem Ordering.isGE_left_of_isGE_then {o₁ o₂ : Ordering} :
(o₁.then o₂).isGE = trueo₁.isGE = true
@[inline]
def compareOfLessAndEq {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] :

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
@[inline]
def compareOfLessAndBEq {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [BEq α] :

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
@[inline]
def compareLex {α : Sort u_1} {β : Sort u_2} (cmp₁ cmp₂ : αβOrdering) (a : α) (b : β) :

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
Instances For
@[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 : α} :
theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x yy xx = 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 yy xx = y) (total : ∀ (x y : α), x y y x) (not_le : ∀ {x y : α}, ¬x y y < x) {x y : α} :
@[simp]
theorem compareOfLessAndEq_eq_lt {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {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 : α} :
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) :
theorem compareOfLessAndEq_eq_gt {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x yy xx = y) (total : ∀ (x y : α), x y y x) (not_le : ∀ {x y : α}, ¬x y y < x) (x y : α) :
theorem isLE_compareOfLessAndEq {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (antisymm : ∀ {x y : α}, x yy xx = y) (not_le : ∀ {x y : α}, ¬x y y < x) (total : ∀ (x y : α), x y y x) {x y : α} :
class Ord (α : 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.

Instances
theorem Ord.ext_iff {α : Type u} {x y : Ord α} :
theorem Ord.ext {α : Type u} {x y : Ord α} (compare : compare = compare) :
x = y
@[inline]
def compareOn {β : Type u_1} {α : Sort u_2} [ord : Ord β] (f : αβ) (x y : α) :

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:

Equations
Instances For
instance instOrdNat :
Equations
instance instOrdInt :
Equations
instance instOrdBool :
Equations
Equations
instance instOrdFin (n : Nat) :
Ord (Fin n)
Equations
Equations
Equations
Equations
Equations
Equations
instance instOrdChar :
Equations
instance instOrdInt8 :
Equations
Equations
Equations
Equations
Equations
instance instOrdBitVec {n : Nat} :
Equations
instance instOrdOption {α : Type u_1} [Ord α] :
Ord (Option α)
Equations
  • One or more equations did not get rendered due to their size.
Equations
instance List.instOrd {α : Type u_1} [Ord α] :
Ord (List α)
Equations
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 α} :
@[simp]
theorem List.compare_nil_cons {α : Type u_1} [Ord α] {x : α} {xs : List α} :
theorem List.compareLex_cons_nil {α : Type u_1} {cmp : ααOrdering} {x : α} {xs : List α} :
@[simp]
theorem List.compare_cons_nil {α : Type u_1} [Ord α] {x : α} {xs : List α} :
theorem List.compareLex_nil_nil {α : Type u_1} {cmp : ααOrdering} :
@[simp]
theorem List.isLE_compareLex_nil_left {α : Type u_1} {cmp : ααOrdering} {xs : List α} :
theorem List.isLE_compare_nil_left {α : Type u_1} [Ord α] {xs : List α} :
theorem List.isLE_compareLex_nil_right {α : Type u_1} {cmp : ααOrdering} {xs : List α} :
@[simp]
theorem List.isLE_compare_nil_right {α : Type u_1} [Ord α] {xs : List α} :
theorem List.isGE_compareLex_nil_left {α : Type u_1} {cmp : ααOrdering} {xs : List α} :
@[simp]
theorem List.isGE_compare_nil_left {α : Type u_1} [Ord α] {xs : List α} :
theorem List.isGE_compareLex_nil_right {α : Type u_1} {cmp : ααOrdering} {xs : List α} :
theorem List.isGE_compare_nil_right {α : Type u_1} [Ord α] {xs : List α} :
theorem List.compareLex_nil_left_eq_eq {α : Type u_1} {cmp : ααOrdering} {xs : List α} :
@[simp]
theorem List.compare_nil_left_eq_eq {α : Type u_1} [Ord α] {xs : List α} :
theorem List.compareLex_nil_right_eq_eq {α : Type u_1} {cmp : ααOrdering} {xs : List α} :
@[simp]
theorem List.compare_nil_right_eq_eq {α : Type u_1} [Ord α] {xs : List α} :
@[irreducible]
def Array.compareLex.go {α : Type u_1} (cmp : ααOrdering) (a₁ a₂ : Array α) (i : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
instance Array.instOrd {α : Type u_1} [Ord α] :
Ord (Array α)
Equations
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
instance Vector.instOrd {α : Type u_1} {n : Nat} [Ord α] :
Ord (Vector α n)
Equations
theorem Vector.compareLex_eq_compareLex_toArray {α : Type u_1} {n : Nat} {cmp : ααOrdering} {a b : Vector α n} :
theorem Vector.compareLex_eq_compareLex_toList {α : Type u_1} {n : Nat} {cmp : ααOrdering} {a b : Vector α n} :
theorem Vector.compare_eq_compare_toArray {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} :
theorem Vector.compare_eq_compare_toList {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} :
def lexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
Ord (α × β)

The lexicographic order on pairs.

Equations
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
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
@[inline]
instance instDecidableRelLt {α : Type u_1} [Ord α] :
Equations
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
@[inline]
instance instDecidableRelLe {α : Type u_1} [Ord α] :
Equations
@[reducible, inline]
abbrev Ord.toBEq {α : Type u_1} (ord : Ord α) :
BEq α

Constructs a BEq instance from an Ord instance.

Equations
@[reducible, inline]
abbrev Ord.toLT {α : Type u_1} (ord : Ord α) :
LT α

Constructs an LT instance from an Ord instance.

Equations
@[reducible, inline]
abbrev Ord.toLE {α : Type u_1} (ord : Ord α) :
LE α

Constructs an LE instance from an Ord instance.

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