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.
A typeclass for comparison functions cmp for which cmp a a = .eq for all a.
Comparison is reflexive.
Instances
@[reducible, inline]
A typeclasses for ordered types for which compare a a = .eq for all a.
Equations
Instances For
@[simp]
A typeclass for functions α → α → Ordering which are oriented: flipping the arguments amounts
to applying Ordering.swap to the return value.
Swapping the arguments to
cmpswaps the outcome.
Instances
@[reducible, inline]
A typeclass for types with an oriented comparison function: flipping the arguments amounts to
applying Ordering.swap to the return value.
Equations
Instances For
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
theorem
Std.OrientedCmp.gt_iff_lt
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{a b : α}
:
theorem
Std.OrientedCmp.isGT_eq_isLT
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{a b : α}
:
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_eq_isLE
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{a b : α}
:
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 : α}
:
theorem
Std.OrientedCmp.not_isGE_of_gt
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{a b : α}
:
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 : α}
:
theorem
Std.OrientedCmp.gt_of_not_isGE
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{a b : α}
:
theorem
Std.OrientedCmp.isLE_antisymm
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{a b : α}
(h₁ : (cmp a b).isLE = true)
(h₂ : (cmp b a).isLE = true)
:
theorem
Std.OrientedCmp.isGE_antisymm
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{a b : α}
(h₁ : (cmp a b).isGE = true)
(h₂ : (cmp b a).isGE = true)
:
A typeclass for functions α → α → Ordering which are transitive.
Transitivity of
cmp, expressed viaOrdering.isLE.
Instances
@[reducible, inline]
A typeclass for types with a transitive ordering function.
Equations
Instances For
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
theorem
Std.TransCmp.congr_left
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{a b c : α}
(hab : cmp a b = Ordering.eq)
:
theorem
Std.TransCmp.congr_right
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{a b c : α}
(hbc : cmp b c = Ordering.eq)
:
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 (==).
- eq_of_compare {a b : α} : cmp a b = Ordering.eq → a = b
If two values compare equal, then they are logically equal.
Instances
@[reducible, inline]
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.eq → a = b
instance
Std.LawfulEqCmp.opposite
{α : Type u}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
[LawfulEqCmp cmp]
:
LawfulEqCmp fun (a b : α) => cmp b a
theorem
Std.LawfulEqCmp.compare_eq_iff_eq
{α : Type u}
{cmp : α → α → Ordering}
[LawfulEqCmp cmp]
{a b : α}
:
theorem
Std.LawfulEqCmp.compare_beq_iff_eq
{α : Type u}
{cmp : α → α → Ordering}
[LawfulEqCmp cmp]
{a b : α}
:
@[simp]
The corresponding lemma for LawfulEqCmp is LawfulEqCmp.compare_eq_iff_eq
@[simp]
The corresponding lemma for LawfulEqCmp is LawfulEqCmp.compare_beq_iff_eq
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 (=).
If two values compare equal, then they are boolean equal.
Instances
theorem
Std.LawfulBEqCmp.not_compare_eq_iff_beq_eq_false
{α : Type u}
[BEq α]
{cmp : α → α → Ordering}
[LawfulBEqCmp cmp]
{a b : α}
:
theorem
Std.LawfulBEqCmp.compare_beq_eq_beq
{α : Type u}
[BEq α]
{cmp : α → α → Ordering}
[LawfulBEqCmp cmp]
{a b : α}
:
theorem
Std.LawfulBEqCmp.isEq_compare_eq_beq
{α : Type u}
[BEq α]
{cmp : α → α → Ordering}
[LawfulBEqCmp cmp]
{a b : α}
:
@[reducible, inline]
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 : α}
:
theorem
Std.LawfulBEqOrd.compare_beq_eq_beq
{α : Type u}
{x✝ : Ord α}
{x✝¹ : BEq α}
[LawfulBEqOrd α]
{a b : α}
:
theorem
Std.LawfulBEqOrd.isEq_compare_eq_beq
{α : Type u}
{x✝ : Ord α}
{x✝¹ : BEq α}
[LawfulBEqOrd α]
{a b : α}
:
instance
Std.instLawfulBEqCmpOfLawfulEqCmpOfLawfulBEq
{α : Type u}
[BEq α]
{cmp : α → α → Ordering}
[LawfulEqCmp cmp]
[LawfulBEq α]
:
LawfulBEqCmp cmp
theorem
Std.LawfulBEqCmp.reflBEq
{α : Type u}
[BEq α]
{cmp : α → α → Ordering}
[inst : LawfulBEqCmp cmp]
[ReflCmp cmp]
:
ReflBEq α
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]
:
instance
Std.LawfulBEqCmp.lawfulBEqCmp
{α : Type u}
[BEq α]
{cmp : α → α → Ordering}
[inst : LawfulBEqCmp cmp]
[LawfulBEq α]
:
LawfulEqCmp cmp
instance
Std.LawfulBEqCmp.opposite
{α : Type u}
[BEq α]
{cmp : α → α → Ordering}
[OrientedCmp cmp]
[LawfulBEqCmp cmp]
:
LawfulBEqCmp fun (a b : α) => cmp b a
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.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.instOrientedCmpCompareOnOfOrientedOrd
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Ord β]
[OrientedOrd β]
:
OrientedCmp (compareOn f)
instance
Std.instOrientedOrdProd
{α : Type u_1}
{β : Type u_2}
[Ord α]
[Ord β]
[OrientedOrd α]
[OrientedOrd β]
:
OrientedOrd (α × β)
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]
:
instance
List.instLawfulBEqCmpCompareLex
{α : Type u_1}
{cmp : α → α → Ordering}
[BEq α]
[Std.LawfulBEqCmp cmp]
:
instance
List.instOrientedCmpCompareLex
{α : Type u_1}
{cmp : α → α → Ordering}
[Std.OrientedCmp cmp]
:
instance
List.instTransCmpCompareLex
{α : Type u_1}
{cmp : α → α → Ordering}
[Std.TransCmp cmp]
:
Std.TransCmp (List.compareLex cmp)
instance
List.instLawfulBEqOrd
{α : Type u_1}
[Ord α]
[BEq α]
[Std.LawfulBEqOrd α]
:
Std.LawfulBEqOrd (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]
:
instance
Array.instLawfulBEqCmpCompareLex
{α : Type u_1}
{cmp : α → α → Ordering}
[BEq α]
[Std.LawfulBEqCmp cmp]
:
instance
Array.instOrientedCmpCompareLex
{α : Type u_1}
{cmp : α → α → Ordering}
[Std.OrientedCmp cmp]
:
instance
Array.instTransCmpCompareLex
{α : Type u_1}
{cmp : α → α → Ordering}
[Std.TransCmp cmp]
:
Std.TransCmp (Array.compareLex cmp)
instance
Array.instLawfulEqOrd
{α : Type u_1}
[Ord α]
[Std.LawfulEqOrd α]
:
Std.LawfulEqOrd (Array α)
instance
Array.instOrientedOrd
{α : Type u_1}
[Ord α]
[Std.OrientedOrd α]
:
Std.OrientedOrd (Array α)