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₂ = Ordering.lt ↔ o₁ = Ordering.lt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.lt

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

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

class Batteries.TotalBLE {α : Sort u_1} (le : α → α → Bool) : Prop

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.

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

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.

theorem Batteries.OrientedCmp.cmp_eq_gt {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} [Batteries.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 : α✝} [Batteries.OrientedCmp cmp] : cmp x y ≠ Ordering.gt ↔ cmp y x ≠ Ordering.lt

theorem Batteries.OrientedCmp.cmp_eq_eq_symm {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} [Batteries.OrientedCmp cmp] : cmp x y = Ordering.eq ↔ cmp y x = Ordering.eq

theorem Batteries.OrientedCmp.cmp_refl {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x : α✝} [Batteries.OrientedCmp cmp] : cmp x x = Ordering.eq

class Batteries.TransCmp {α : Sort u_1} (cmp : α → α → Ordering) extends Batteries.OrientedCmp cmp : Prop

TransCmp cmp asserts that cmp induces a transitive relation.

• symm : ∀ (x y : α), (cmp x y).swap = cmp y x
• le_trans : ∀ {x y z : α}, cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt

  The comparator operation is transitive.

theorem Batteries.TransCmp.ge_trans {x✝ : Sort u_1} {cmp : x✝ → x✝ → Ordering} [Batteries.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.lt_asymm {x✝ : Sort u_1} {cmp : x✝ → x✝ → Ordering} [Batteries.TransCmp cmp] {x y : x✝} (h : cmp x y = Ordering.lt) : cmp y x ≠ Ordering.lt

theorem Batteries.TransCmp.gt_asymm {x✝ : Sort u_1} {cmp : x✝ → x✝ → Ordering} [Batteries.TransCmp cmp] {x y : x✝} (h : cmp x y = Ordering.gt) : cmp y x ≠ Ordering.gt

theorem Batteries.TransCmp.le_lt_trans {x✝ : Sort u_1} {cmp : x✝ → x✝ → Ordering} [Batteries.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} [Batteries.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} [Batteries.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} [Batteries.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} [Batteries.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} [Batteries.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} [Batteries.TransCmp cmp] {y z x : x✝} (yz : cmp y z = Ordering.eq) : cmp x y = cmp x z

theorem Batteries.instOrientedCmpFlipOrdering {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [inst : Batteries.OrientedCmp cmp] : Batteries.OrientedCmp (flip cmp)

theorem Batteries.instTransCmpFlipOrdering {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [inst : Batteries.TransCmp cmp] : Batteries.TransCmp (flip cmp)

class Batteries.BEqCmp {α : Type u_1} [BEq α] (cmp : α → α → Ordering) : Prop

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

• cmp_iff_beq : ∀ {x y : α}, cmp x y = Ordering.eq ↔ (x == y) = true

  cmp x y = .eq holds iff x == y is true.

theorem Batteries.BEqCmp.cmp_iff_eq {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [BEq α] [LawfulBEq α] [Batteries.BEqCmp cmp] : cmp x y = Ordering.eq ↔ x = y

class Batteries.LTCmp {α : Type u_1} [LT α] (cmp : α → α → Ordering) extends Batteries.OrientedCmp cmp : Prop

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.

theorem Batteries.LTCmp.cmp_iff_gt {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [LT α] [Batteries.LTCmp cmp] : cmp x y = Ordering.gt ↔ y < x

class Batteries.LECmp {α : Type u_1} [LE α] (cmp : α → α → Ordering) extends Batteries.OrientedCmp cmp : Prop

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.

theorem Batteries.LECmp.cmp_iff_ge {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [LE α] [Batteries.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 : Prop

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).

• symm : ∀ (x y : α), (cmp x y).swap = cmp y x
• le_trans : ∀ {x y z : α}, cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt
• cmp_iff_beq : ∀ {x y : α}, cmp x y = Ordering.eq ↔ (x == y) = true
• cmp_iff_lt : ∀ {x y : α}, cmp x y = Ordering.lt ↔ x < y
• cmp_iff_le : ∀ {x y : α}, cmp x y ≠ Ordering.gt ↔ x ≤ y

@[reducible, inline]

abbrev Batteries.OrientedOrd (α : Type u_1) [Ord α] : Prop

OrientedOrd α asserts that the Ord instance satisfies OrientedCmp.

Equations

• Batteries.OrientedOrd α = Batteries.OrientedCmp compare

@[reducible, inline]

abbrev Batteries.TransOrd (α : Type u_1) [Ord α] : Prop

TransOrd α asserts that the Ord instance satisfies TransCmp.

Equations

• Batteries.TransOrd α = Batteries.TransCmp compare

@[reducible, inline]

abbrev Batteries.BEqOrd (α : Type u_1) [BEq α] [Ord α] : Prop

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

Equations

• Batteries.BEqOrd α = Batteries.BEqCmp compare

@[reducible, inline]

abbrev Batteries.LTOrd (α : Type u_1) [LT α] [Ord α] : Prop

LTOrd α asserts that the Ord instance satisfies LTCmp.

Equations

• Batteries.LTOrd α = Batteries.LTCmp compare

@[reducible, inline]

abbrev Batteries.LEOrd (α : Type u_1) [LE α] [Ord α] : Prop

LEOrd α asserts that the Ord instance satisfies LECmp.

Equations

• Batteries.LEOrd α = Batteries.LECmp compare

@[reducible, inline]

abbrev Batteries.LawfulOrd (α : Type u_1) [LE α] [LT α] [BEq α] [Ord α] : Prop

LawfulOrd α asserts that the Ord instance satisfies LawfulCmp.

Equations

• Batteries.LawfulOrd α = Batteries.LawfulCmp compare

theorem Batteries.compareOfLessAndEq_eq_lt {α : Type u_1} {x y : α} [LT α] [Decidable (x < y)] [DecidableEq α] : compareOfLessAndEq x y = Ordering.lt ↔ x < y

theorem Batteries.TransCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z) (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y) : Batteries.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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y → y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) : Batteries.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) : Batteries.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 < y → y < z → x < z) (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y) : Batteries.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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y → y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) : Batteries.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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) : Batteries.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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) : Batteries.LawfulCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2

theorem Batteries.LTCmp.eq_compareOfLessAndEq {α : Type u_1} {cmp : α → α → Ordering} [LT α] [DecidableEq α] [BEq α] [LawfulBEq α] [Batteries.BEqCmp cmp] [Batteries.LTCmp cmp] (x y : α) [Decidable (x < y)] : cmp x y = compareOfLessAndEq x y

theorem Batteries.instOrientedCmpCompareLex {α✝ : Sort u_1} {cmp₁ cmp₂ : α✝ → α✝ → Ordering} [inst₁ : Batteries.OrientedCmp cmp₁] [inst₂ : Batteries.OrientedCmp cmp₂] : Batteries.OrientedCmp (compareLex cmp₁ cmp₂)

theorem Batteries.instTransCmpCompareLex {α✝ : Sort u_1} {cmp₁ cmp₂ : α✝ → α✝ → Ordering} [inst₁ : Batteries.TransCmp cmp₁] [inst₂ : Batteries.TransCmp cmp₂] : Batteries.TransCmp (compareLex cmp₁ cmp₂)

theorem Batteries.instOrientedCmpCompareOnOfOrientedOrd {β : Type u_1} {α : Sort u_2} [Ord β] [Batteries.OrientedOrd β] (f : α → β) : Batteries.OrientedCmp (compareOn f)

theorem Batteries.instTransCmpCompareOnOfTransOrd {β : Type u_1} {α : Sort u_2} [Ord β] [Batteries.TransOrd β] (f : α → β) : Batteries.TransCmp (compareOn 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 β] [Batteries.OrientedOrd α] [Batteries.OrientedOrd β] : Batteries.OrientedOrd (α × β)

Local instance for OrientedOrd lexOrd.

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

Local instance for TransOrd lexOrd.

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

Local instance for OrientedOrd ord.opposite.

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

Local instance for TransOrd ord.opposite.

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

Local instance for OrientedOrd (ord.on f).

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

Local instance for TransOrd (ord.on f).

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

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

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

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

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

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

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

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

theorem Batteries.instLawfulOrdNat : Batteries.LawfulOrd Nat

theorem Batteries.instLawfulOrdFin {n : Nat} : Batteries.LawfulOrd (Fin n)

theorem Batteries.instLawfulOrdBool : Batteries.LawfulOrd Bool

theorem Batteries.instLawfulOrdInt : Batteries.LawfulOrd Int

@[inline]

def Ordering.byKey {α : Sort u_1} {β : Sort u_2} (f : α → β) (cmp : β → β → Ordering) (a b : α) : Ordering

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

Equations

• Ordering.byKey f cmp a b = cmp (f a) (f b)

theorem Ordering.instOrientedCmpByKey {α : Sort u_1} {β : Sort u_2} (f : α → β) (cmp : β → β → Ordering) [Batteries.OrientedCmp cmp] : Batteries.OrientedCmp (Ordering.byKey f cmp)

theorem Ordering.instTransCmpByKey {α : Sort u_1} {β : Sort u_2} (f : α → β) (cmp : β → β → Ordering) [Batteries.TransCmp cmp] : Batteries.TransCmp (Ordering.byKey f cmp)