Documentation

Batteries.Classes.Order

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

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

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

      TransCmp cmp asserts that cmp induces a transitive relation.

      Instances
        theorem Batteries.TransCmp.le_trans {α : Sort u_1} {cmp : ααOrdering} [self : Batteries.TransCmp cmp] {x : α} {y : α} {z : α} :
        cmp x y Ordering.gtcmp y z Ordering.gtcmp x z Ordering.gt

        The comparator operation is transitive.

        theorem Batteries.TransCmp.ge_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y Ordering.ltcmp y z Ordering.ltcmp x_1 z Ordering.lt
        theorem Batteries.TransCmp.lt_asymm :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.ltcmp y x_1 Ordering.lt
        theorem Batteries.TransCmp.gt_asymm :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.gtcmp y x_1 Ordering.gt
        theorem Batteries.TransCmp.le_lt_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y Ordering.gtcmp y z = Ordering.ltcmp x_1 z = Ordering.lt
        theorem Batteries.TransCmp.lt_le_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.ltcmp y z Ordering.gtcmp x_1 z = Ordering.lt
        theorem Batteries.TransCmp.lt_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.ltcmp y z = Ordering.ltcmp x_1 z = Ordering.lt
        theorem Batteries.TransCmp.gt_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.gtcmp y z = Ordering.gtcmp x_1 z = Ordering.gt
        theorem Batteries.TransCmp.cmp_congr_left :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.eqcmp x_1 z = cmp y z
        theorem Batteries.TransCmp.cmp_congr_left' :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.eqcmp x_1 = cmp y
        theorem Batteries.TransCmp.cmp_congr_right :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Batteries.TransCmp cmp] {y z x : x}, cmp y z = Ordering.eqcmp x y = cmp x 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) :

        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.

        Instances
          theorem Batteries.BEqCmp.cmp_iff_beq {α : Type u_1} :
          ∀ {inst : 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 :

          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_lt {α : Type u_1} :
            ∀ {inst : 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 :

            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_le {α : Type u_1} :
              ∀ {inst : 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 :

              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
                Instances For
                  @[reducible, inline]
                  abbrev Batteries.TransOrd (α : Type u_1) [Ord α] :

                  TransOrd α asserts that the Ord instance satisfies TransCmp.

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

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

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

                      LTOrd α asserts that the Ord instance satisfies LTCmp.

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

                        LEOrd α asserts that the Ord instance satisfies LECmp.

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

                          LawfulOrd α asserts that the Ord instance satisfies LawfulCmp.

                          Equations
                          Instances For
                            theorem Batteries.compareOfLessAndEq_eq_lt {α : Type u_1} {x : α} {y : α} [LT α] [Decidable (x < y)] [DecidableEq α] :
                            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) :
                            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 < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < yy x) (le_antisymm : ∀ {x y : α}, x yy xx = 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 < yy < zx < z) (lt_antisymm : ∀ {x y : α}, ¬x < y¬y < xx = 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 < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < yy x) (le_antisymm : ∀ {x y : α}, x yy xx = 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 < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < y y x) (le_antisymm : ∀ {x y : α}, x yy xx = 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 < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < y y x) (le_antisymm : ∀ {x y : α}, x yy xx = 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
                            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
                            • =
                            Equations
                            • =
                            instance Batteries.instTransCmpCompareOnOfTransOrd {β : Type u_1} {α : Sort u_2} [Ord β] [Batteries.TransOrd β] (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.TransOrd.instLexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [Batteries.TransOrd α] [Batteries.TransOrd β] :

                            Local instance for TransOrd lexOrd.

                            Local instance for OrientedOrd ord.opposite.

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

                            Local instance for TransOrd ord.opposite.

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

                            Local instance for OrientedOrd (ord.on f).

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

                            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 β] :

                            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 β] :

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

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

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

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

                            Equations
                            • =
                            @[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] :
                              Equations
                              • =
                              instance Ordering.instTransCmpByKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [Batteries.TransCmp cmp] :
                              Equations
                              • =