Ordering

@[simp]

theorem Ordering.swap_swap {o : Ordering} : o.swap.swap = o

@[simp]

theorem Ordering.swap_inj {o₁ : Ordering} {o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂

theorem Ordering.swap_then (o₁ : Ordering) (o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap

theorem Ordering.then_eq_lt {o₁ : Ordering} {o₂ : Ordering} : o₁.then o₂ = Ordering.lt ↔ o₁ = Ordering.lt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.lt

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

theorem Ordering.then_eq_gt {o₁ : Ordering} {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.

theorem Batteries.TotalBLE.total {α : Sort u_1} {le : α → α → Bool} [self : Batteries.TotalBLE le] {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.symm {α : Sort u_1} {cmp : α → α → Ordering} [self : Batteries.OrientedCmp cmp] (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 : α} [inst : 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 : α} [inst : 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 : α} [inst : Batteries.OrientedCmp cmp], cmp x y = Ordering.eq ↔ cmp y x = Ordering.eq

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

class Batteries.TransCmp {α : Sort u_1} (cmp : α → α → Ordering) extends Batteries.OrientedCmp : 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.le_trans {α : Sort u_1} {cmp : α → α → Ordering} [self : Batteries.TransCmp cmp] {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} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y ≠ Ordering.lt → cmp y z ≠ Ordering.lt → cmp x_1 z ≠ Ordering.lt

theorem Batteries.TransCmp.lt_asymm : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.lt → cmp y x_1 ≠ Ordering.lt

theorem Batteries.TransCmp.gt_asymm : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.gt → cmp y x_1 ≠ Ordering.gt

theorem Batteries.TransCmp.le_lt_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y ≠ Ordering.gt → cmp y z = Ordering.lt → cmp x_1 z = Ordering.lt

theorem Batteries.TransCmp.lt_le_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.lt → cmp y z ≠ Ordering.gt → cmp x_1 z = Ordering.lt

theorem Batteries.TransCmp.lt_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.lt → cmp y z = Ordering.lt → cmp x_1 z = Ordering.lt

theorem Batteries.TransCmp.gt_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.gt → cmp y z = Ordering.gt → cmp x_1 z = Ordering.gt

theorem Batteries.TransCmp.cmp_congr_left : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.eq → cmp x_1 z = cmp y z

theorem Batteries.TransCmp.cmp_congr_left' : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.eq → cmp x_1 = cmp y

theorem Batteries.TransCmp.cmp_congr_right : ∀ {x : Sort u_1} {cmp : x → x → Ordering} {y z x_1 : x} [inst : Batteries.TransCmp cmp], cmp y z = Ordering.eq → cmp x_1 y = cmp x_1 z

instance Batteries.instOrientedCmpFlipOrdering : ∀ {α : Sort u_1} {cmp : α → α → Ordering} [inst : Batteries.OrientedCmp cmp], Batteries.OrientedCmp (flip cmp)

Equations

• ⋯ = ⋯

instance Batteries.instTransCmpFlipOrdering : ∀ {α : Sort u_1} {cmp : α → α → Ordering} [inst : Batteries.TransCmp cmp], Batteries.TransCmp (flip cmp)

Equations

• ⋯ = ⋯

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_beq {α : Type u_1} [BEq α] {cmp : α → α → Ordering} [self : Batteries.BEqCmp cmp] {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 : 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_lt {α : Type u_1} [LT α] {cmp : α → α → Ordering} [self : Batteries.LTCmp cmp] {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 : 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_le {α : Type u_1} [LE α] {cmp : α → α → Ordering} [self : Batteries.LECmp cmp] {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 , Batteries.BEqCmp : 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 x y = .lt holds iff x < y is true.

• cmp_iff_le : ∀ {x y : α}, cmp x y ≠ Ordering.gt ↔ x ≤ y

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

@[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 (x x_1 : α) => compareOfLessAndEq x x_1

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 (x x_1 : α) => compareOfLessAndEq x x_1

theorem Batteries.BEqCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] [BEq α] [LawfulBEq α] (lt_irrefl : ∀ (x : α), ¬x < x) : Batteries.BEqCmp fun (x x_1 : α) => compareOfLessAndEq x x_1

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 (x x_1 : α) => compareOfLessAndEq x x_1

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 (x x_1 : α) => compareOfLessAndEq x x_1

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 (x x_1 : α) => compareOfLessAndEq x x_1

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 (x x_1 : α) => compareOfLessAndEq x x_1

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Batteries.instTransCmpCompareOnOfTransOrd {β : Type u_1} {α : Sort u_2} [Ord β] [Batteries.TransOrd β] (f : α → β) : Batteries.TransCmp (compareOn f)

Equations

• ⋯ = ⋯

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₂ : Ord α) [Batteries.OrientedOrd α] [Batteries.OrientedOrd α] : Batteries.OrientedOrd α

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

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

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

instance Batteries.instLawfulOrdNat : Batteries.LawfulOrd Nat

Equations

• Batteries.instLawfulOrdNat = ⋯

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

Equations

• ⋯ = ⋯

instance Batteries.instLawfulOrdBool : Batteries.LawfulOrd Bool

Equations

• Batteries.instLawfulOrdBool = ⋯

instance Batteries.instLawfulOrdInt : Batteries.LawfulOrd Int

Equations

• Batteries.instLawfulOrdInt = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯