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

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

• Array.instReflCmpCompareLex
• Array.instReflOrd
• List.instReflCmpCompareLex
• List.instReflOrd
• Std.Option.instReflOrdOption
• Std.instReflCmpCompareLex
• Std.instReflCmpCompareOnOfReflOrd
• Std.instReflCmpOfOrientedCmp
• Std.instReflOrdProd
• Vector.instReflCmpCompareLex
• Vector.instReflOrd

@[reducible, inline]

abbrev Std.ReflOrd (α : Type u) [Ord α] : Prop

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

Equations

• Std.ReflOrd α = Std.ReflCmp compare

@[simp]

theorem Std.ReflOrd.compare_self {α : Type u} [Ord α] [ReflOrd α] {a : α} : compare a a = Ordering.eq

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 : α} : (compare a a).isLE = true

class Std.OrientedCmp {α : Type u} (cmp : α → α → Ordering) : Prop

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

• Array.instOrientedCmpCompareLex
• Array.instOrientedOrd
• List.instOrientedCmpCompareLex
• List.instOrientedOrd
• Std.Fin.instOrientedOrdFin
• Std.Option.instOrientedOrdOption
• Std.OrientedCmp.opposite
• Std.OrientedOrd.opposite
• Std.Time.Internal.Bounded.instOrientedOrd
• Std.Time.Internal.instOrientedOrdUnitVal
• Std.Time.instOrientedOrdHourMarker
• Std.Time.instOrientedOrdValidDate
• Std.instOrientedCmpCompareLex
• Std.instOrientedCmpCompareOnOfOrientedOrd
• Std.instOrientedOrdProd
• Vector.instOrientedCmpCompareLex
• Vector.instOrientedOrd

@[reducible, inline]

abbrev Std.OrientedOrd (α : Type u) [Ord α] : Prop

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

Equations

• Std.OrientedOrd α = Std.OrientedCmp compare

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] : ReflCmp cmp

instance Std.OrientedCmp.opposite {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] : OrientedCmp fun (a b : α) => cmp b a

instance Std.OrientedOrd.opposite {α : Type u} [Ord α] [OrientedOrd α] : OrientedOrd α

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.gt → cmp b a = Ordering.lt

theorem Std.OrientedCmp.gt_of_lt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.lt → cmp 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.eq → cmp 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 = true → cmp b a ≠ Ordering.lt

theorem Std.OrientedCmp.not_gt_of_isGE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp a b).isGE = true → cmp b a ≠ Ordering.gt

theorem Std.OrientedCmp.not_lt_of_lt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.lt → cmp b a ≠ Ordering.lt

theorem Std.OrientedCmp.not_gt_of_gt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.gt → cmp b a ≠ Ordering.gt

theorem Std.OrientedCmp.lt_of_not_isLE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : ¬(cmp a b).isLE = true → cmp b a = Ordering.lt

theorem Std.OrientedCmp.gt_of_not_isGE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : ¬(cmp a b).isGE = true → cmp b a = Ordering.gt

class Std.TransCmp {α : Type u} (cmp : α → α → Ordering) extends Std.OrientedCmp cmp : Prop

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

• eq_swap {a b : α} : cmp a b = (cmp b a).swap
• isLE_trans {a b c : α} : (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true

  Transitivity of cmp, expressed via Ordering.isLE.

Instances

• Array.instTransCmpCompareLex
• Array.instTransOrd
• List.instTransCmpCompareLex
• List.instTransOrd
• Std.BitVec.instTransOrdBitVec
• Std.Bool.instTransOrdBool
• Std.Char.instTransOrdChar
• Std.Fin.instTransOrdFin
• Std.ISize.instTransOrdISize
• Std.Int.instTransOrdInt
• Std.Int16.instTransOrdInt16
• Std.Int32.instTransOrdInt32
• Std.Int64.instTransOrdInt64
• Std.Int8.instTransOrdInt8
• Std.Nat.instTransOrdNat
• Std.Option.instTransOrdOption
• Std.String.instTransOrdString
• Std.Time.Day.Ordinal.instTransOrdOfYear
• Std.Time.Day.instTransOrdOffset
• Std.Time.Day.instTransOrdOrdinal
• Std.Time.Hour.instTransOrdOffset
• Std.Time.Hour.instTransOrdOrdinal
• Std.Time.Internal.Bounded.instTransOrd
• Std.Time.Internal.instTransOrdUnitVal
• Std.Time.Millisecond.instTransOrdOffset
• Std.Time.Millisecond.instTransOrdOrdinal
• Std.Time.Minute.instTransOrdOffset
• Std.Time.Minute.instTransOrdOrdinal
• Std.Time.Month.instTransOrdOffset
• Std.Time.Month.instTransOrdOrdinal
• Std.Time.Month.instTransOrdQuarter
• Std.Time.Nanosecond.Ordinal.instTransOrdOfDay
• Std.Time.Nanosecond.instTransOrdOffset
• Std.Time.Nanosecond.instTransOrdOrdinal
• Std.Time.Nanosecond.instTransOrdSpan
• Std.Time.Second.instTransOrdOffset
• Std.Time.Second.instTransOrdOrdinal
• Std.Time.TimeZone.instTransOrdOffset
• Std.Time.Week.Ordinal.instTransOrdOfMonth
• Std.Time.Week.instTransOrdOffset
• Std.Time.Week.instTransOrdOrdinal
• Std.Time.Weekday.instTransOrd
• Std.Time.Weekday.instTransOrdOrdinal
• Std.Time.Year.instTransOrdOffset
• Std.Time.instTransOrdDateTime
• Std.Time.instTransOrdDuration
• Std.Time.instTransOrdHourMarker
• Std.Time.instTransOrdPlainDate
• Std.Time.instTransOrdPlainDateTime
• Std.Time.instTransOrdPlainTime
• Std.Time.instTransOrdTimestamp
• Std.Time.instTransOrdValidDate
• Std.TransCmp.opposite
• Std.TransOrd.opposite
• Std.UInt16.instTransOrdUInt16
• Std.UInt32.instTransOrdUInt32
• Std.UInt64.instTransOrdUInt64
• Std.UInt8.instTransOrdUInt8
• Std.USize.instTransOrdUSize
• Std.instTransCmpCompareLex
• Std.instTransCmpCompareOnOfTransOrd
• Std.instTransOrdProd
• Vector.instTransCmpCompareLex
• Vector.instTransOrd

@[reducible, inline]

abbrev Std.TransOrd (α : Type u) [Ord α] : Prop

A typeclass for types with a transitive ordering function.

Equations

• Std.TransOrd α = Std.TransCmp compare

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 α] : 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 : Prop

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

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

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

Instances

• Array.instLawfulEqCmpCompareLex
• Array.instLawfulEqOrd
• List.instLawfulEqCmpCompareLex
• List.instLawfulEqOrd
• Std.BitVec.instLawfulEqOrdBitVec
• Std.Bool.instLawfulEqOrdBool
• Std.Char.instLawfulEqOrdChar
• Std.Fin.instLawfulEqOrdFin
• Std.ISize.instLawfulEqOrdISize
• Std.Int.instLawfulEqOrdInt
• Std.Int16.instLawfulEqOrdInt16
• Std.Int32.instLawfulEqOrdInt32
• Std.Int64.instLawfulEqOrdInt64
• Std.Int8.instLawfulEqOrdInt8
• Std.LawfulBEqCmp.lawfulBEqCmp
• Std.LawfulEqCmp.opposite
• Std.LawfulEqOrd.opposite
• Std.Nat.instLawfulEqOrdNat
• Std.Option.instLawfulEqOrdOption
• Std.String.instLawfulEqOrdString
• Std.Time.Day.Ordinal.instLawfulEqOrdOfYear
• Std.Time.Day.instLawfulEqOrdOffset
• Std.Time.Day.instLawfulEqOrdOrdinal
• Std.Time.Hour.instLawfulEqOrdOffset
• Std.Time.Hour.instLawfulEqOrdOrdinal
• Std.Time.Internal.Bounded.instLawfulEqOrd
• Std.Time.Internal.instLawfulEqOrdUnitVal
• Std.Time.Millisecond.instLawfulEqOrdOffset
• Std.Time.Millisecond.instLawfulEqOrdOrdinal
• Std.Time.Minute.instLawfulEqOrdOffset
• Std.Time.Minute.instLawfulEqOrdOrdinal
• Std.Time.Month.instLawfulEqOrdOffset
• Std.Time.Month.instLawfulEqOrdOrdinal
• Std.Time.Month.instLawfulEqOrdQuarter
• Std.Time.Nanosecond.Ordinal.instLawfulEqOrdOfDay
• Std.Time.Nanosecond.instLawfulEqOrdOffset
• Std.Time.Nanosecond.instLawfulEqOrdOrdinal
• Std.Time.Nanosecond.instLawfulEqOrdSpan
• Std.Time.Second.instLawfulEqOrdOffset
• Std.Time.Second.instLawfulEqOrdOrdinal
• Std.Time.TimeZone.instLawfulEqOrdOffset
• Std.Time.Week.Ordinal.instLawfulEqOrdOfMonth
• Std.Time.Week.instLawfulEqOrdOffset
• Std.Time.Week.instLawfulEqOrdOrdinal
• Std.Time.Weekday.instLawfulEqOrd
• Std.Time.Weekday.instLawfulEqOrdOrdinal
• Std.Time.Year.instLawfulEqOrdOffset
• Std.Time.instLawfulEqOrdDuration
• Std.Time.instLawfulEqOrdHourMarker
• Std.Time.instLawfulEqOrdPlainDate
• Std.Time.instLawfulEqOrdPlainDateTime
• Std.Time.instLawfulEqOrdPlainTime
• Std.Time.instLawfulEqOrdTimestamp
• Std.Time.instLawfulEqOrdValidDate
• Std.UInt16.instLawfulEqOrdUInt16
• Std.UInt32.instLawfulEqOrdUInt32
• Std.UInt64.instLawfulEqOrdUInt64
• Std.UInt8.instLawfulEqOrdUInt8
• Std.USize.instLawfulEqOrdUSize
• Std.instLawfulEqOrdProd
• Vector.instLawfulEqCmpCompareLex
• Vector.instLawfulEqOrd

@[reducible, inline]

abbrev Std.LawfulEqOrd (α : Type u) [Ord α] : Prop

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

• Std.LawfulEqOrd α = Std.LawfulEqCmp compare

theorem Std.LawfulEqOrd.eq_of_compare {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} : compare a b = Ordering.eq → a = b

instance Std.LawfulEqCmp.opposite {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] [LawfulEqCmp cmp] : LawfulEqCmp fun (a b : α) => cmp b a

instance Std.LawfulEqOrd.opposite {α : Type u} [Ord α] [OrientedOrd α] [LawfulEqOrd α] : LawfulEqOrd α

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

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

• Array.instLawfulBEqCmpCompareLex
• Array.instLawfulBEqOrd
• List.instLawfulBEqCmpCompareLex
• List.instLawfulBEqOrd
• Std.Internal.instLawfulBEqOrd
• Std.LawfulBEqCmp.opposite
• Std.LawfulBEqOrd.opposite
• Std.Option.instLawfulBEqOrdOption
• Std.Time.instLawfulBEqOrdDateTime
• Std.instLawfulBEqCmpOfLawfulEqCmpOfLawfulBEq
• Vector.instLawfulBEqCmpCompareLex
• Vector.instLawfulBEqOrd

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 α] : Prop

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

• Std.LawfulBEqOrd α = Std.LawfulBEqCmp compare

theorem Std.LawfulBEqOrd.compare_eq_iff_beq {α : Type u} {x✝ : Ord α} {x✝¹ : BEq α} [LawfulBEqOrd α] {a b : α} : compare a b = Ordering.eq ↔ (a == b) = true

theorem Std.LawfulBEqOrd.not_compare_eq_iff_beq_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Ord α} [LawfulBEqOrd α] {a b : α} : ¬compare a b = Ordering.eq ↔ (a == b) = false

instance Std.instLawfulBEqCmpOfLawfulEqCmpOfLawfulBEq {α : Type u} [BEq α] {cmp : α → α → Ordering} [LawfulEqCmp cmp] [LawfulBEq α] : LawfulBEqCmp cmp

theorem Std.LawfulBEqCmp.equivBEq {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [TransCmp cmp] : EquivBEq α

instance Std.LawfulBEqOrd.equivBEq {α : Type u} [BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] : EquivBEq α

theorem Std.LawfulBEqCmp.lawfulBEq {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [LawfulEqCmp cmp] : LawfulBEq α

instance Std.LawfulBEqOrd.lawfulBEq {α : Type u} [BEq α] [Ord α] [LawfulBEqOrd α] [LawfulEqOrd α] : LawfulBEq α

instance Std.LawfulBEqCmp.lawfulBEqCmp {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp

theorem Std.LawfulBEqOrd.lawfulBEqOrd {α : Type u} [BEq α] [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α

instance Std.LawfulBEqCmp.opposite {α : Type u} [BEq α] {cmp : α → α → Ordering} [OrientedCmp cmp] [LawfulBEqCmp cmp] : LawfulBEqCmp fun (a b : α) => cmp b a

instance Std.LawfulBEqOrd.opposite {α : Type u} [BEq α] [Ord α] [OrientedOrd α] [LawfulBEqOrd α] : LawfulBEqOrd α

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

• Std.Internal.beqOfOrd = { beq := fun (a b : α) => decide (compare a b = Ordering.eq) }

instance Std.Internal.instLawfulBEqOrd {α : Type u} {x✝ : Ord α} : LawfulBEqOrd α

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 : α} : (a == b) = true ↔ compare a b = Ordering.eq

theorem Std.Internal.eq_beqOfOrd_of_lawfulBEqOrd {α : Type u} [Ord α] (inst : BEq α) [instLawful : LawfulBEqOrd α] : inst = beqOfOrd

theorem Std.Internal.equivBEq_of_transOrd {α : Type u} [Ord α] [TransOrd α] : EquivBEq α

theorem Std.Internal.lawfulBEq_of_lawfulEqOrd {α : Type u} [Ord α] [LawfulEqOrd α] : LawfulBEq α

theorem Std.TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff {α : Type u} [LT α] [DecidableLT α] [DecidableEq α] (lt_trans : ∀ {a b c : α}, a < b → b < c → a < 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 ≤ y → y ≤ x → x = y) (trans : ∀ {x y z : α}, x ≤ y → y ≤ z → x ≤ 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.Bool.instTransOrdBool : TransOrd Bool

instance Std.Bool.instLawfulEqOrdBool : LawfulEqOrd Bool

instance Std.Nat.instTransOrdNat : TransOrd Nat

instance Std.Nat.instLawfulEqOrdNat : LawfulEqOrd Nat

instance Std.Int.instTransOrdInt : TransOrd Int

instance Std.Int.instLawfulEqOrdInt : LawfulEqOrd Int

instance Std.Fin.instOrientedOrdFin (n : Nat) : OrientedOrd (Fin n)

instance Std.Fin.instTransOrdFin (n : Nat) : TransOrd (Fin n)

instance Std.Fin.instLawfulEqOrdFin (n : Nat) : LawfulEqOrd (Fin n)

instance Std.String.instTransOrdString : TransOrd String

instance Std.String.instLawfulEqOrdString : LawfulEqOrd String

instance Std.Char.instTransOrdChar : TransOrd Char

instance Std.Char.instLawfulEqOrdChar : LawfulEqOrd Char

instance Std.UInt8.instTransOrdUInt8 : TransOrd UInt8

instance Std.UInt8.instLawfulEqOrdUInt8 : LawfulEqOrd UInt8

instance Std.UInt16.instTransOrdUInt16 : TransOrd UInt16

instance Std.UInt16.instLawfulEqOrdUInt16 : LawfulEqOrd UInt16

instance Std.UInt32.instTransOrdUInt32 : TransOrd UInt32

instance Std.UInt32.instLawfulEqOrdUInt32 : LawfulEqOrd UInt32

instance Std.UInt64.instTransOrdUInt64 : TransOrd UInt64

instance Std.UInt64.instLawfulEqOrdUInt64 : LawfulEqOrd UInt64

instance Std.USize.instTransOrdUSize : TransOrd USize

instance Std.USize.instLawfulEqOrdUSize : LawfulEqOrd USize

instance Std.Int8.instTransOrdInt8 : TransOrd Int8

instance Std.Int8.instLawfulEqOrdInt8 : LawfulEqOrd Int8

instance Std.Int16.instTransOrdInt16 : TransOrd Int16

instance Std.Int16.instLawfulEqOrdInt16 : LawfulEqOrd Int16

instance Std.Int32.instTransOrdInt32 : TransOrd Int32

instance Std.Int32.instLawfulEqOrdInt32 : LawfulEqOrd Int32

instance Std.Int64.instTransOrdInt64 : TransOrd Int64

instance Std.Int64.instLawfulEqOrdInt64 : LawfulEqOrd Int64

instance Std.ISize.instTransOrdISize : TransOrd ISize

instance Std.ISize.instLawfulEqOrdISize : LawfulEqOrd ISize

instance Std.BitVec.instTransOrdBitVec {n : Nat} : TransOrd (BitVec n)

instance Std.BitVec.instLawfulEqOrdBitVec {n : Nat} : LawfulEqOrd (BitVec n)

instance Std.Option.instOrientedOrdOption {α : Type u_1} [Ord α] [OrientedOrd α] : OrientedOrd (Option α)

instance Std.Option.instTransOrdOption {α : Type u_1} [Ord α] [TransOrd α] : TransOrd (Option α)

instance Std.Option.instReflOrdOption {α : Type u_1} [Ord α] [ReflOrd α] : ReflOrd (Option α)

instance Std.Option.instLawfulEqOrdOption {α : Type u_1} [Ord α] [LawfulEqOrd α] : LawfulEqOrd (Option α)

instance Std.Option.instLawfulBEqOrdOption {α : Type u_1} [Ord α] [BEq α] [LawfulBEqOrd α] : LawfulBEqOrd (Option α)

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 β] : ReflCmp (compareOn f)

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

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

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] : Std.ReflCmp (List.compareLex cmp)

instance List.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] : Std.LawfulEqCmp (List.compareLex cmp)

instance List.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [BEq α] [Std.LawfulBEqCmp cmp] : Std.LawfulBEqCmp (List.compareLex cmp)

instance List.instOrientedCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] : Std.OrientedCmp (List.compareLex cmp)

instance List.instTransCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] : Std.TransCmp (List.compareLex cmp)

instance List.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] : Std.ReflOrd (List α)

instance List.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] : Std.LawfulEqOrd (List α)

instance List.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (List α)

instance List.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] : Std.OrientedOrd (List α)

instance List.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (List α)

instance Array.instReflCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp] : Std.ReflCmp (Array.compareLex cmp)

instance Array.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] : Std.LawfulEqCmp (Array.compareLex cmp)

instance Array.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [BEq α] [Std.LawfulBEqCmp cmp] : Std.LawfulBEqCmp (Array.compareLex cmp)

instance Array.instOrientedCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] : Std.OrientedCmp (Array.compareLex cmp)

instance Array.instTransCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] : Std.TransCmp (Array.compareLex cmp)

instance Array.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] : Std.ReflOrd (Array α)

instance Array.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] : Std.LawfulEqOrd (Array α)

instance Array.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (Array α)

instance Array.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] : Std.OrientedOrd (Array α)

instance Array.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (Array α)

instance Vector.instReflCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {n : Nat} : Std.ReflCmp (Vector.compareLex cmp)

instance Vector.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] {n : Nat} : Std.LawfulEqCmp (Vector.compareLex cmp)

instance Vector.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [BEq α] [Std.LawfulBEqCmp cmp] {n : Nat} : Std.LawfulBEqCmp (Vector.compareLex cmp)

instance Vector.instOrientedCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {n : Nat} : Std.OrientedCmp (Vector.compareLex cmp)

instance Vector.instTransCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {n : Nat} : Std.TransCmp (Vector.compareLex cmp)

instance Vector.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] {n : Nat} : Std.ReflOrd (Vector α n)

instance Vector.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] {n : Nat} : Std.LawfulEqOrd (Vector α n)

instance Vector.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] {n : Nat} : Std.LawfulBEqOrd (Vector α n)

instance Vector.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] {n : Nat} : Std.OrientedOrd (Vector α n)

instance Vector.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] {n : Nat} : Std.TransOrd (Vector α n)