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

          Checks whether the ordering is not eq.

          Equations
          Instances For
            @[inline]

            Checks whether the ordering is lt or eq.

            Equations
            Instances For
              @[inline]

              Checks whether the ordering is lt.

              Equations
              Instances For
                @[inline]

                Checks whether the ordering is gt.

                Equations
                Instances For
                  @[inline]

                  Checks whether the ordering is gt or eq.

                  Equations
                  Instances For
                    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
                    Instances For
                      @[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
                      Instances For
                        @[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
                              @[specialize #[]]
                              def List.compareLex {α : Type u_1} (cmp : ααOrdering) :
                              List αList αOrdering
                              Equations
                              Instances For
                                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 α} :
                                @[specialize #[]]
                                def Array.compareLex {α : Type u_1} (cmp : ααOrdering) (a₁ a₂ : Array α) :
                                Equations
                                Instances For
                                  @[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.
                                  Instances For
                                    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
                                    def Vector.compareLex {α : Type u_1} {n : Nat} (cmp : ααOrdering) (a b : Vector α n) :
                                    Equations
                                    Instances For
                                      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
                                      Instances For
                                        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
                                        Instances For
                                          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
                                          Instances For
                                            @[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
                                            Instances For
                                              @[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
                                              Instances For
                                                @[reducible, inline]
                                                abbrev Ord.toLT {α : Type u_1} (ord : Ord α) :
                                                LT α

                                                Constructs an LT instance from an Ord instance.

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

                                                  Constructs an LE instance from an Ord instance.

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