Documentation

Std.Classes.Ord

Type classes related to Ord #

This file provides several typeclasses encode properties of an Ord instance. For each typeclass, there is also a variant that does not depend on an Ord instance and takes an explicit comparison function cmp : α → α → Ordering instead.

class Std.ReflCmp {α : Type u} (cmp : ααOrdering) :

A typeclass for comparison functions cmp for which cmp a a = .eq for all a.

  • compare_self {a : α} : cmp a a = Ordering.eq

    Comparison is reflexive.

Instances
    @[reducible, inline]
    abbrev Std.ReflOrd (α : Type u) [Ord α] :

    A typeclasses for ordered types for which compare a a = .eq for all a.

    Equations
    Instances For
      @[simp]
      theorem Std.ReflOrd.compare_self {α : Type u} [Ord α] [ReflOrd α] {a : α} :
      theorem Std.ReflCmp.isLE_rfl {α : Type u_1} {cmp : ααOrdering} [ReflCmp cmp] {a : α} :
      (cmp a a).isLE = true
      @[simp]
      theorem Std.ReflOrd.isLE_rfl {α : Type u_1} [Ord α] [ReflOrd α] {a : α} :
      class Std.OrientedCmp {α : Type u} (cmp : ααOrdering) :

      A typeclass for functions α → α → Ordering which are oriented: flipping the arguments amounts to applying Ordering.swap to the return value.

      • eq_swap {a b : α} : cmp a b = (cmp b a).swap

        Swapping the arguments to cmp swaps the outcome.

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

        A typeclass for types with an oriented comparison function: flipping the arguments amounts to applying Ordering.swap to the return value.

        Equations
        Instances For
          theorem Std.OrientedOrd.eq_swap {α : Type u} [Ord α] [OrientedOrd α] {a b : α} :
          compare a b = (compare b a).swap
          instance Std.instReflCmpOfOrientedCmp {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] :
          instance Std.OrientedCmp.opposite {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] :
          OrientedCmp fun (a b : α) => cmp b a
          theorem Std.OrientedCmp.gt_iff_lt {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.gt cmp b a = Ordering.lt
          theorem Std.OrientedCmp.lt_of_gt {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.gtcmp b a = Ordering.lt
          theorem Std.OrientedCmp.gt_of_lt {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.ltcmp b a = Ordering.gt
          theorem Std.OrientedCmp.isGE_iff_isLE {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          (cmp a b).isGE = true (cmp b a).isLE = true
          theorem Std.OrientedCmp.isLE_of_isGE {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          (cmp b a).isGE = true(cmp a b).isLE = true
          theorem Std.OrientedCmp.isGE_of_isLE {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          (cmp b a).isLE = true(cmp a b).isGE = true
          theorem Std.OrientedCmp.eq_comm {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.eq cmp b a = Ordering.eq
          theorem Std.OrientedCmp.eq_symm {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.eqcmp b a = Ordering.eq
          theorem Std.OrientedCmp.not_isLE_of_lt {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.lt¬(cmp b a).isLE = true
          theorem Std.OrientedCmp.not_isGE_of_gt {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.gt¬(cmp b a).isGE = true
          theorem Std.OrientedCmp.not_lt_of_isLE {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          (cmp a b).isLE = truecmp b a Ordering.lt
          theorem Std.OrientedCmp.not_gt_of_isGE {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          (cmp a b).isGE = truecmp b a Ordering.gt
          theorem Std.OrientedCmp.not_lt_of_lt {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.ltcmp b a Ordering.lt
          theorem Std.OrientedCmp.not_gt_of_gt {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          cmp a b = Ordering.gtcmp b a Ordering.gt
          theorem Std.OrientedCmp.lt_of_not_isLE {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          ¬(cmp a b).isLE = truecmp b a = Ordering.lt
          theorem Std.OrientedCmp.gt_of_not_isGE {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] {a b : α} :
          ¬(cmp a b).isGE = truecmp b a = Ordering.gt
          class Std.TransCmp {α : Type u} (cmp : ααOrdering) extends Std.OrientedCmp cmp :

          A typeclass for functions α → α → Ordering which are transitive.

          Instances
            @[reducible, inline]
            abbrev Std.TransOrd (α : Type u) [Ord α] :

            A typeclass for types with a transitive ordering function.

            Equations
            Instances For
              theorem Std.TransOrd.isLE_trans {α : Type u} [Ord α] [TransOrd α] {a b c : α} :
              (compare a b).isLE = true(compare b c).isLE = true(compare a c).isLE = true
              theorem Std.TransCmp.isGE_trans {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (h₁ : (cmp a b).isGE = true) (h₂ : (cmp b c).isGE = true) :
              (cmp a c).isGE = true
              theorem Std.TransOrd.isGE_trans {α : Type u} [Ord α] [TransOrd α] {a b c : α} :
              (compare a b).isGE = true(compare b c).isGE = true(compare a c).isGE = true
              instance Std.TransCmp.opposite {α : Type u} {cmp : ααOrdering} [TransCmp cmp] :
              TransCmp fun (a b : α) => cmp b a
              instance Std.TransOrd.opposite {α : Type u} [Ord α] [TransOrd α] :
              theorem Std.TransCmp.lt_of_lt_of_eq {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.lt) (hbc : cmp b c = Ordering.eq) :
              cmp a c = Ordering.lt
              theorem Std.TransCmp.lt_of_eq_of_lt {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) (hbc : cmp b c = Ordering.lt) :
              cmp a c = Ordering.lt
              theorem Std.TransCmp.gt_of_eq_of_gt {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) (hbc : cmp b c = Ordering.gt) :
              cmp a c = Ordering.gt
              theorem Std.TransCmp.gt_of_gt_of_eq {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : cmp b c = Ordering.eq) :
              cmp a c = Ordering.gt
              theorem Std.TransCmp.lt_trans {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.lt) (hbc : cmp b c = Ordering.lt) :
              cmp a c = Ordering.lt
              theorem Std.TransCmp.gt_trans {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : cmp b c = Ordering.gt) :
              cmp a c = Ordering.gt
              theorem Std.TransCmp.lt_of_lt_of_isLE {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.lt) (hbc : (cmp b c).isLE = true) :
              cmp a c = Ordering.lt
              theorem Std.TransCmp.lt_of_isLE_of_lt {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : (cmp a b).isLE = true) (hbc : cmp b c = Ordering.lt) :
              cmp a c = Ordering.lt
              theorem Std.TransCmp.gt_of_gt_of_isGE {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : (cmp b c).isGE = true) :
              cmp a c = Ordering.gt
              theorem Std.TransCmp.gt_of_gt_of_gt {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : cmp b c = Ordering.gt) :
              cmp a c = Ordering.gt
              theorem Std.TransCmp.gt_of_isGE_of_gt {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : (cmp a b).isGE = true) (hbc : cmp b c = Ordering.gt) :
              cmp a c = Ordering.gt
              theorem Std.TransCmp.isLE_antisymm {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b : α} (h₁ : (cmp a b).isLE = true) (h₂ : (cmp b a).isLE = true) :
              cmp a b = Ordering.eq
              theorem Std.TransCmp.isGE_antisymm {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b : α} (h₁ : (cmp a b).isGE = true) (h₂ : (cmp b a).isGE = true) :
              cmp a b = Ordering.eq
              theorem Std.TransCmp.eq_trans {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) (hbc : cmp b c = Ordering.eq) :
              cmp a c = Ordering.eq
              theorem Std.TransCmp.congr_left {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) :
              cmp a c = cmp b c
              theorem Std.TransCmp.congr_right {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {a b c : α} (hbc : cmp b c = Ordering.eq) :
              cmp a b = cmp a c
              class Std.LawfulEqCmp {α : Type u} (cmp : ααOrdering) extends Std.ReflCmp cmp :

              A typeclass for comparison functions satisfying cmp a b = .eq if and only if the logical equality a = b holds.

              This typeclass distinguishes itself from LawfulBEqCmp by using logical equality (=) instead of boolean equality (==).

              Instances
                @[reducible, inline]
                abbrev Std.LawfulEqOrd (α : Type u) [Ord α] :

                A typeclass for types with a comparison function that satisfies compare a b = .eq if and only if the logical equality a = b holds.

                This typeclass distinguishes itself from LawfulBEqOrd by using logical equality (=) instead of boolean equality (==).

                Equations
                Instances For
                  theorem Std.LawfulEqOrd.eq_of_compare {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} :
                  compare a b = Ordering.eqa = b
                  instance Std.LawfulEqCmp.opposite {α : Type u} {cmp : ααOrdering} [OrientedCmp cmp] [LawfulEqCmp cmp] :
                  LawfulEqCmp fun (a b : α) => cmp b a
                  @[simp]
                  theorem Std.compare_eq_iff_eq {α : Type u} {cmp : ααOrdering} [LawfulEqCmp cmp] {a b : α} :
                  cmp a b = Ordering.eq a = b
                  @[simp]
                  theorem Std.compare_beq_iff_eq {α : Type u} {cmp : ααOrdering} [LawfulEqCmp cmp] {a b : α} :
                  (cmp a b == Ordering.eq) = true a = b
                  class Std.LawfulBEqCmp {α : Type u} [BEq α] (cmp : ααOrdering) :

                  A typeclass for comparison functions satisfying cmp a b = .eq if and only if the boolean equality a == b holds.

                  This typeclass distinguishes itself from LawfulEqCmp by using boolean equality (==) instead of logical equality (=).

                  • compare_eq_iff_beq {a b : α} : cmp a b = Ordering.eq (a == b) = true

                    If two values compare equal, then they are logically equal.

                  Instances
                    theorem Std.LawfulBEqCmp.not_compare_eq_iff_beq_eq_false {α : Type u} [BEq α] {cmp : ααOrdering} [LawfulBEqCmp cmp] {a b : α} :
                    ¬cmp a b = Ordering.eq (a == b) = false
                    @[reducible, inline]
                    abbrev Std.LawfulBEqOrd (α : Type u) [BEq α] [Ord α] :

                    A typeclass for types with a comparison function that satisfies compare a b = .eq if and only if the boolean equality a == b holds.

                    This typeclass distinguishes itself from LawfulEqOrd by using boolean equality (==) instead of logical equality (=).

                    Equations
                    Instances For
                      theorem Std.LawfulBEqOrd.compare_eq_iff_beq {α : Type u} {x✝ : Ord α} {x✝¹ : BEq α} [LawfulBEqOrd α] {a b : α} :
                      theorem Std.LawfulBEqOrd.not_compare_eq_iff_beq_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Ord α} [LawfulBEqOrd α] {a b : α} :
                      instance Std.instLawfulBEqCmpOfLawfulEqCmpOfLawfulBEq {α : Type u} [BEq α] {cmp : ααOrdering} [LawfulEqCmp cmp] [LawfulBEq α] :
                      theorem Std.LawfulBEqCmp.equivBEq {α : Type u} [BEq α] {cmp : ααOrdering} [inst : LawfulBEqCmp cmp] [TransCmp cmp] :
                      instance Std.LawfulBEqOrd.equivBEq {α : Type u} [BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] :
                      theorem Std.LawfulBEqCmp.lawfulBEq {α : Type u} [BEq α] {cmp : ααOrdering} [inst : LawfulBEqCmp cmp] [LawfulEqCmp cmp] :
                      instance Std.LawfulBEqCmp.lawfulBEqCmp {α : Type u} [BEq α] {cmp : ααOrdering} [inst : LawfulBEqCmp cmp] [LawfulBEq α] :
                      instance Std.LawfulBEqCmp.opposite {α : Type u} [BEq α] {cmp : ααOrdering} [OrientedCmp cmp] [LawfulBEqCmp cmp] :
                      LawfulBEqCmp fun (a b : α) => cmp b a
                      def Std.Internal.beqOfOrd {α : Type u} [Ord α] :
                      BEq α

                      Internal funcion to derive a BEq instance from an Ord instance in order to connect the verification machinery for tree maps to the verification machinery for hash maps.

                      Equations
                      Instances For
                        instance Std.Internal.instLawfulBEqOrd {α : Type u} {x✝ : Ord α} :
                        theorem Std.Internal.beq_eq {α : Type u} [Ord α] {a b : α} :
                        ((a == b) = true) = (compare a b = Ordering.eq)
                        theorem Std.Internal.beq_iff {α : Type u} [Ord α] {a b : α} :
                        theorem Std.Internal.eq_beqOfOrd_of_lawfulBEqOrd {α : Type u} [Ord α] (inst : BEq α) [instLawful : LawfulBEqOrd α] :
                        inst = beqOfOrd
                        theorem Std.TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff {α : Type u} [LT α] [DecidableLT α] [DecidableEq α] (lt_trans : ∀ {a b c : α}, a < bb < ca < c) (h : ∀ (x y : α), x < y ¬y < x x y) :
                        TransCmp fun (x y : α) => compareOfLessAndEq x y
                        theorem Std.TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (antisymm : ∀ {x y : α}, x yy xx = y) (trans : ∀ {x y z : α}, x yy zx z) (total : ∀ (x y : α), x y y x) (not_le : ∀ {x y : α}, ¬x y y < x) :
                        TransCmp fun (x y : α) => compareOfLessAndEq x y
                        instance Std.Option.instReflOrdOption {α : Type u_1} [Ord α] [ReflOrd α] :
                        instance Std.instReflCmpCompareLex {α : Type u_1} {cmp₁ cmp₂ : ααOrdering} [ReflCmp cmp₁] [ReflCmp cmp₂] :
                        ReflCmp (compareLex cmp₁ cmp₂)
                        instance Std.instOrientedCmpCompareLex {α : Type u_1} {cmp₁ cmp₂ : ααOrdering} [OrientedCmp cmp₁] [OrientedCmp cmp₂] :
                        OrientedCmp (compareLex cmp₁ cmp₂)
                        instance Std.instTransCmpCompareLex {α : Type u_1} {cmp₁ cmp₂ : ααOrdering} [TransCmp cmp₁] [TransCmp cmp₂] :
                        TransCmp (compareLex cmp₁ cmp₂)
                        instance Std.instReflCmpCompareOnOfReflOrd {α : Type u_1} {β : Type u_2} {f : αβ} [Ord β] [ReflOrd β] :
                        instance Std.instOrientedCmpCompareOnOfOrientedOrd {α : Type u_1} {β : Type u_2} {f : αβ} [Ord β] [OrientedOrd β] :
                        instance Std.instTransCmpCompareOnOfTransOrd {α : Type u_1} {β : Type u_2} {f : αβ} [Ord β] [TransOrd β] :
                        instance Std.instReflOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [ReflOrd α] [ReflOrd β] :
                        ReflOrd (α × β)
                        instance Std.instOrientedOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] :
                        OrientedOrd (α × β)
                        instance Std.instTransOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [TransOrd α] [TransOrd β] :
                        TransOrd (α × β)
                        instance Std.instLawfulEqOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [LawfulEqOrd α] [LawfulEqOrd β] :
                        LawfulEqOrd (α × β)
                        instance List.instReflCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.ReflCmp cmp] :
                        instance List.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [BEq α] [Std.LawfulBEqCmp cmp] :
                        instance List.instTransCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.TransCmp cmp] :
                        instance List.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] :
                        instance List.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] :
                        instance Array.instReflCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.ReflCmp cmp] :
                        instance Array.instTransCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.TransCmp cmp] :
                        instance Array.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] :
                        instance Array.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] :
                        instance Vector.instReflCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.ReflCmp cmp] {n : Nat} :
                        instance Vector.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.LawfulEqCmp cmp] {n : Nat} :
                        instance Vector.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [BEq α] [Std.LawfulBEqCmp cmp] {n : Nat} :
                        instance Vector.instOrientedCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.OrientedCmp cmp] {n : Nat} :
                        instance Vector.instTransCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.TransCmp cmp] {n : Nat} :
                        instance Vector.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] {n : Nat} :
                        instance Vector.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] {n : Nat} :
                        instance Vector.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] {n : Nat} :
                        instance Vector.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] {n : Nat} :
                        instance Vector.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] {n : Nat} :