Mathlib.Data.Ordering.Basic

instReprOrdering_mathlib instance

: Repr✝ (@Ordering✝)

Full source

Repr for Ordering

Pretty-Printing Representation for Ordering Type

Informal description

The type `Ordering` (with values `lt`, `eq`, and `gt`) has a canonical representation for pretty-printing.

Ordering.Compares definition

[LT α] : Ordering → α → α → Prop

Full source

/-- `Compares o a b` means that `a` and `b` have the ordering relation `o` between them, assuming
that the relation `a < b` is defined. -/
def Compares [LT α] : Ordering → α → α → Prop
  | lt, a, b => a < b
  | eq, a, b => a = b
  | gt, a, b => a > b

Order comparison predicate

Informal description

Given a type $\alpha$ with a less-than relation $<$, the predicate $\text{Compares}\,o\,a\,b$ states that elements $a$ and $b$ in $\alpha$ are related by the ordering $o$, where $o$ can be: - $\text{lt}$ (less than), meaning $a < b$, - $\text{eq}$ (equal), meaning $a = b$, - $\text{gt}$ (greater than), meaning $a > b$.

Ordering.compares_lt theorem

[LT α] (a b : α) : Compares lt a b = (a < b)

Full source

@[simp] lemma compares_lt [LT α] (a b : α) : Compares lt a b = (a < b) := rfl

Equivalence of "Less Than" Comparison and Strict Ordering

Informal description

For any type $\alpha$ with a less-than relation $<$, the predicate $\text{Compares}\,\text{lt}\,a\,b$ holds if and only if $a < b$.

Ordering.compares_eq theorem

[LT α] (a b : α) : Compares eq a b = (a = b)

Full source

@[simp] lemma compares_eq [LT α] (a b : α) : Compares eq a b = (a = b) := rfl

Equivalence of Equality Comparison and Equality Relation

Informal description

For any type $\alpha$ with a less-than relation $<$, the comparison predicate $\text{Compares}$ with ordering $\text{eq}$ applied to elements $a$ and $b$ in $\alpha$ is equivalent to the equality $a = b$.

Ordering.compares_gt theorem

[LT α] (a b : α) : Compares gt a b = (a > b)

Full source

@[simp] lemma compares_gt [LT α] (a b : α) : Compares gt a b = (a > b) := rfl

Greater-than Comparison via Ordering Predicate

Informal description

For any type $\alpha$ with a less-than relation $<$, and for any elements $a, b \in \alpha$, the predicate $\text{Compares}\, \text{gt}\, a\, b$ holds if and only if $a > b$ (i.e., $b < a$).

Ordering.dthen definition

: (o : Ordering) → (o = .eq → Ordering) → Ordering

Full source

/-- `o₁.dthen fun h => o₂(h)` is like `o₁.then o₂` but `o₂` is allowed to depend on
`h : o₁ = .eq`. -/
@[macro_inline] def dthen :
    (o : Ordering) → (o = .eq → Ordering) → Ordering
  | .eq, f => f rfl
  | o, _ => o

Dependent then operation for orderings

Informal description

Given an ordering `o` and a function `f` that takes a proof that `o = Ordering.eq` and returns another ordering, `dthen` evaluates to `f` applied to the proof of `o = Ordering.eq` if `o` is indeed `Ordering.eq`, and otherwise returns `o` unchanged. This is a dependent version of the `then` operation on orderings.

cmpUsing definition

{α : Type u} (lt : α → α → Prop) [DecidableRel lt] (a b : α) : Ordering

Full source

/--
Lift a decidable relation to an `Ordering`,
assuming that incomparable terms are `Ordering.eq`.
-/
def cmpUsing {α : Type u} (lt : α → α → Prop) [DecidableRel lt] (a b : α) : Ordering :=
  if lt a b then Ordering.lt else if lt b a then Ordering.gt else Ordering.eq

Comparison using a decidable relation

Informal description

Given a type $\alpha$ with a decidable relation `lt`, the function `cmpUsing` compares two elements $a$ and $b$ of $\alpha$ and returns an `Ordering` value: `Ordering.lt` if $a < b$, `Ordering.gt` if $b < a$, and `Ordering.eq` otherwise (i.e., when $a$ and $b$ are incomparable or equal under `lt`).

cmp definition

{α : Type u} [LT α] [DecidableLT α] (a b : α) : Ordering

Full source

/--
Construct an `Ordering` from a type with a decidable `LT` instance,
assuming that incomparable terms are `Ordering.eq`.
-/
def cmp {α : Type u} [LT α] [DecidableLT α] (a b : α) : Ordering :=
  cmpUsing (· < ·) a b

Comparison function for decidable less-than relation

Informal description

Given a type $\alpha$ with a decidable less-than relation `<`, the function `cmp` compares two elements $a$ and $b$ of $\alpha$ and returns an `Ordering` value: `Ordering.lt` if $a < b$, `Ordering.gt` if $b < a$, and `Ordering.eq` otherwise (i.e., when $a$ and $b$ are incomparable or equal under `<`).