Documentation

Batteries.Classes.Order

Ordering #

@[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_eq {o₁ o₂ : Ordering} :
o₁.then o₂ = eq o₁ = eq o₂ = eq
theorem Ordering.then_eq_gt {o₁ o₂ : Ordering} :
o₁.then o₂ = gt o₁ = gt o₁ = eq o₂ = gt
class Batteries.TotalBLE {α : Sort u_1} (le : ααBool) :

TotalBLE le asserts that le has a total order, that is, le a b ∨ le b a.

  • total {a b : α} : le a b = true le b a = true

    le is total: either le a b or le b a.

Instances
    class Batteries.OrientedCmp {α : Sort u_1} (cmp : ααOrdering) :

    OrientedCmp cmp asserts that cmp is determined by the relation cmp x y = .lt.

    • symm (x y : α) : (cmp x y).swap = cmp y x

      The comparator operation is symmetric, in the sense that if cmp x y equals .lt then cmp y x = .gt and vice versa.

    Instances
    theorem Batteries.OrientedCmp.cmp_eq_gt {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {x y : α✝} [OrientedCmp cmp] :
    cmp x y = Ordering.gt cmp y x = Ordering.lt
    theorem Batteries.OrientedCmp.cmp_ne_gt {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {x y : α✝} [OrientedCmp cmp] :
    theorem Batteries.OrientedCmp.cmp_eq_eq_symm {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {x y : α✝} [OrientedCmp cmp] :
    cmp x y = Ordering.eq cmp y x = Ordering.eq
    theorem Batteries.OrientedCmp.cmp_refl {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {x : α✝} [OrientedCmp cmp] :
    cmp x x = Ordering.eq
    class Batteries.TransCmp {α : Sort u_1} (cmp : ααOrdering) extends Batteries.OrientedCmp cmp :

    TransCmp cmp asserts that cmp induces a transitive relation.

    Instances
    theorem Batteries.TransCmp.ge_trans {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y z : x✝} (h₁ : cmp x y Ordering.lt) (h₂ : cmp y z Ordering.lt) :
    theorem Batteries.TransCmp.lt_asymm {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y : x✝} (h : cmp x y = Ordering.lt) :
    theorem Batteries.TransCmp.gt_asymm {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y : x✝} (h : cmp x y = Ordering.gt) :
    theorem Batteries.TransCmp.le_lt_trans {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y z : x✝} (h₁ : cmp x y Ordering.gt) (h₂ : cmp y z = Ordering.lt) :
    cmp x z = Ordering.lt
    theorem Batteries.TransCmp.lt_le_trans {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y z : x✝} (h₁ : cmp x y = Ordering.lt) (h₂ : cmp y z Ordering.gt) :
    cmp x z = Ordering.lt
    theorem Batteries.TransCmp.lt_trans {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y z : x✝} (h₁ : cmp x y = Ordering.lt) (h₂ : cmp y z = Ordering.lt) :
    cmp x z = Ordering.lt
    theorem Batteries.TransCmp.gt_trans {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y z : x✝} (h₁ : cmp x y = Ordering.gt) (h₂ : cmp y z = Ordering.gt) :
    cmp x z = Ordering.gt
    theorem Batteries.TransCmp.cmp_congr_left {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y z : x✝} (xy : cmp x y = Ordering.eq) :
    cmp x z = cmp y z
    theorem Batteries.TransCmp.cmp_congr_left' {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {x y : x✝} (xy : cmp x y = Ordering.eq) :
    cmp x = cmp y
    theorem Batteries.TransCmp.cmp_congr_right {x✝ : Sort u_1} {cmp : x✝x✝Ordering} [TransCmp cmp] {y z x : x✝} (yz : cmp y z = Ordering.eq) :
    cmp x y = cmp x z
    instance Batteries.instOrientedCmpFlipOrdering {α✝ : Sort u_1} {cmp : α✝α✝Ordering} [inst : OrientedCmp cmp] :
    instance Batteries.instTransCmpFlipOrdering {α✝ : Sort u_1} {cmp : α✝α✝Ordering} [inst : TransCmp cmp] :
    class Batteries.BEqCmp {α : Type u_1} [BEq α] (cmp : ααOrdering) :

    BEqCmp cmp asserts that cmp x y = .eq and x == y coincide.

    Instances
    theorem Batteries.BEqCmp.cmp_iff_eq {α : Type u_1} {cmp : ααOrdering} {x y : α} [BEq α] [LawfulBEq α] [BEqCmp cmp] :
    cmp x y = Ordering.eq x = y
    class Batteries.LTCmp {α : Type u_1} [LT α] (cmp : ααOrdering) extends Batteries.OrientedCmp cmp :

    LTCmp cmp asserts that cmp x y = .lt and x < y coincide.

    • symm (x y : α) : (cmp x y).swap = cmp y x
    • cmp_iff_lt {x y : α} : cmp x y = Ordering.lt x < y

      cmp x y = .lt holds iff x < y is true.

    Instances
    theorem Batteries.LTCmp.cmp_iff_gt {α : Type u_1} {cmp : ααOrdering} {x y : α} [LT α] [LTCmp cmp] :
    cmp x y = Ordering.gt y < x
    class Batteries.LECmp {α : Type u_1} [LE α] (cmp : ααOrdering) extends Batteries.OrientedCmp cmp :

    LECmp cmp asserts that cmp x y ≠ .gt and x ≤ y coincide.

    • symm (x y : α) : (cmp x y).swap = cmp y x
    • cmp_iff_le {x y : α} : cmp x y Ordering.gt x y

      cmp x y ≠ .gt holds iff x ≤ y is true.

    Instances
    theorem Batteries.LECmp.cmp_iff_ge {α : Type u_1} {cmp : ααOrdering} {x y : α} [LE α] [LECmp cmp] :
    cmp x y Ordering.lt y x
    class Batteries.LawfulCmp {α : Type u_1} [LE α] [LT α] [BEq α] (cmp : ααOrdering) extends Batteries.TransCmp cmp, Batteries.BEqCmp cmp, Batteries.LTCmp cmp, Batteries.LECmp cmp :

    LawfulCmp cmp asserts that the LE, LT, BEq instances are all coherent with each other and with cmp, describing a strict weak order (a linear order except for antisymmetry).

    Instances
    @[reducible, inline]
    abbrev Batteries.OrientedOrd (α : Type u_1) [Ord α] :

    OrientedOrd α asserts that the Ord instance satisfies OrientedCmp.

    Equations
    @[reducible, inline]
    abbrev Batteries.TransOrd (α : Type u_1) [Ord α] :

    TransOrd α asserts that the Ord instance satisfies TransCmp.

    Equations
    @[reducible, inline]
    abbrev Batteries.BEqOrd (α : Type u_1) [BEq α] [Ord α] :

    BEqOrd α asserts that the Ord and BEq instances are coherent via BEqCmp.

    Equations
    @[reducible, inline]
    abbrev Batteries.LTOrd (α : Type u_1) [LT α] [Ord α] :

    LTOrd α asserts that the Ord instance satisfies LTCmp.

    Equations
    @[reducible, inline]
    abbrev Batteries.LEOrd (α : Type u_1) [LE α] [Ord α] :

    LEOrd α asserts that the Ord instance satisfies LECmp.

    Equations
    @[reducible, inline]
    abbrev Batteries.LawfulOrd (α : Type u_1) [LE α] [LT α] [BEq α] [Ord α] :

    LawfulOrd α asserts that the Ord instance satisfies LawfulCmp.

    Equations
    theorem Batteries.TransCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (lt_antisymm : ∀ {x y : α}, ¬x < y¬y < xx = y) :
    TransCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
    theorem Batteries.TransCmp.compareOfLessAndEq_of_le {α : Type u_1} [LT α] [LE α] [DecidableRel LT.lt] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < yy x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
    TransCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
    theorem Batteries.BEqCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] [BEq α] [LawfulBEq α] (lt_irrefl : ∀ (x : α), ¬x < x) :
    BEqCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
    theorem Batteries.LTCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (lt_antisymm : ∀ {x y : α}, ¬x < y¬y < xx = y) :
    LTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
    theorem Batteries.LTCmp.compareOfLessAndEq_of_le {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] [LE α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < yy x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
    LTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
    theorem Batteries.LECmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] [LE α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < y y x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
    LECmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
    theorem Batteries.LawfulCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] [BEq α] [LawfulBEq α] [LE α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < y y x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
    LawfulCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
    theorem Batteries.LTCmp.eq_compareOfLessAndEq {α : Type u_1} {cmp : ααOrdering} [LT α] [DecidableEq α] [BEq α] [LawfulBEq α] [BEqCmp cmp] [LTCmp cmp] (x y : α) [Decidable (x < y)] :
    cmp x y = compareOfLessAndEq x y
    instance Batteries.instOrientedCmpCompareLex {α✝ : Sort u_1} {cmp₁ cmp₂ : α✝α✝Ordering} [inst₁ : OrientedCmp cmp₁] [inst₂ : OrientedCmp cmp₂] :
    OrientedCmp (compareLex cmp₁ cmp₂)
    instance Batteries.instTransCmpCompareLex {α✝ : Sort u_1} {cmp₁ cmp₂ : α✝α✝Ordering} [inst₁ : TransCmp cmp₁] [inst₂ : TransCmp cmp₂] :
    TransCmp (compareLex cmp₁ cmp₂)
    instance Batteries.instOrientedCmpCompareOnOfOrientedOrd {β : Type u_1} {α : Sort u_2} [Ord β] [OrientedOrd β] (f : αβ) :
    instance Batteries.instTransCmpCompareOnOfTransOrd {β : Type u_1} {α : Sort u_2} [Ord β] [TransOrd β] (f : αβ) :
    theorem lexOrd_def {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
    compare = compareLex (compareOn fun (x : α × β) => x.fst) (compareOn fun (x : α × β) => x.snd)
    theorem Batteries.OrientedOrd.instLexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] :
    OrientedOrd (α × β)

    Local instance for OrientedOrd lexOrd.

    theorem Batteries.TransOrd.instLexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [TransOrd α] [TransOrd β] :
    TransOrd (α × β)

    Local instance for TransOrd lexOrd.

    theorem Batteries.OrientedOrd.instOpposite {α : Type u_1} [ord : Ord α] [inst : OrientedOrd α] :

    Local instance for OrientedOrd ord.opposite.

    theorem Batteries.TransOrd.instOpposite {α : Type u_1} [ord : Ord α] [inst : TransOrd α] :

    Local instance for TransOrd ord.opposite.

    theorem Batteries.OrientedOrd.instOn {β : Type u_1} {α : Type u_2} [ord : Ord β] [OrientedOrd β] (f : αβ) :

    Local instance for OrientedOrd (ord.on f).

    theorem Batteries.TransOrd.instOn {β : Type u_1} {α : Type u_2} [ord : Ord β] [TransOrd β] (f : αβ) :

    Local instance for TransOrd (ord.on f).

    theorem Batteries.OrientedOrd.instOrdLex {α : Type u_1} {β : Type u_2} [oα : Ord α] [oβ : Ord β] [OrientedOrd α] [OrientedOrd β] :
    OrientedOrd (α × β)

    Local instance for OrientedOrd (oα.lex oβ).

    theorem Batteries.TransOrd.instOrdLex {α : Type u_1} {β : Type u_2} [oα : Ord α] [oβ : Ord β] [TransOrd α] [TransOrd β] :
    TransOrd (α × β)

    Local instance for TransOrd (oα.lex oβ).

    theorem Batteries.OrientedOrd.instOrdLex' {α : Type u_1} (ord₁ ord₂ : Ord α) [OrientedOrd α] [OrientedOrd α] :

    Local instance for OrientedOrd (oα.lex' oβ).

    theorem Batteries.TransOrd.instOrdLex' {α : Type u_1} (ord₁ ord₂ : Ord α) [TransOrd α] [TransOrd α] :

    Local instance for TransOrd (oα.lex' oβ).

    @[inline]
    def Ordering.byKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) (a b : α) :

    Pull back a comparator by a function f, by applying the comparator to both arguments.

    Equations
    Instances For
    instance Ordering.instOrientedCmpByKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [Batteries.OrientedCmp cmp] :
    instance Ordering.instTransCmpByKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [Batteries.TransCmp cmp] :