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.

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

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.

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

instance Std.instReflCmpOfOrientedCmp {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] : ReflCmp cmp

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.

@[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.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.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_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.

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

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

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

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 α

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

theorem Std.Internal.beq_eq {α : Type u} [Ord α] {a b : α} : (a == b) = (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 α