Instance packages and factories for them

Instance packages are classes with the sole purpose to bundle together multiple smaller classes. They should not be used as hypotheses, but they make it more convenient to define multiple instances at once.

class Std.PreorderPackage (α : Type u) extends LE α, LT α, BEq α, Std.LawfulOrderLT α, Std.LawfulOrderBEq α, Std.IsPreorder α : Type u

This class entails LE α, LT α and BEq α instances as well as proofs that these operations represent the same preorder structure on α.

• le : α → α → Prop
• lt : α → α → Prop
• beq : α → α → Bool
• lt_iff (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• beq_iff_le_and_ge (a b : α) : (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• decidableLE : DecidableLE α
• decidableLT : DecidableLT α

instance Std.instDecidableLE {α : Type u_1} [PreorderPackage α] : DecidableLE α

instance Std.instDecidableLT {α : Type u_1} [PreorderPackage α] : DecidableLT α

def Std.FactoryInstances.beqOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : BEq α

instance Std.FactoryInstances.instLawfulOrderBEqOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : LawfulOrderBEq α

def Std.FactoryInstances.decidableLTOfLE {α : Type u} [LE α] {x✝ : LT α} [DecidableLE α] [LawfulOrderLT α] : DecidableLT α

If LT can be characterized in terms of a decidable LE, then LT is decidable either.

structure Std.Packages.PreorderOfLEArgs (α : Type u) : Type u

This structure contains all the data needed to create a PreorderPackage α instance. Its fields are automatically provided if possible. For the detailed rules how the fields are inferred, see PreorderPackage.ofLE.

• le : LE α
• decidableLE : DecidableLE α
• lt : let this := self.le; LT α
• beq : let this := self.le; let this := self.decidableLE; BEq α
• lt_iff : let this := self.le; let this_1 := self.lt; ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• decidableLT : let this := self.le; let this := self.decidableLE; let this := self.lt; have this_1 := ⋯; DecidableLT α
• beq_iff_le_and_ge : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.beq; ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl : let this := self.le; ∀ (a : α), a ≤ a
• le_trans : let this := self.le; ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c

def Std.PreorderPackage.ofLE (α : Type u) (args : Packages.PreorderOfLEArgs α := by exact { }) : PreorderPackage α

Use this factory to conveniently define a preorder on a type α and all the associated operations and instances given an LE α instance.

Creates a PreorderPackage α instance. Such an instance entails LE α, LT α and BEq α instances as well as an IsPreorder α instance and LawfulOrder* instances proving the compatibility of the operations with the preorder.

In the presence of LE α, DecidableLE α, Refl (· ≤ ·) and Trans (· ≤ ·) (· ≤ ·) (· ≤ ·) instances, no arguments are required and the factory can be used as in this example:

public instance : PreorderPackage X := .ofLE X

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly provide some arguments:

public instance : PreorderPackage X := .ofLE X {
  le_refl := sorry
  le_trans := sorry }

It is also possible to do all of this by hand, without resorting to PreorderPackage. This can be useful if, say, one wants to avoid specifying an LT α instance, which is not possible with PreorderPackage.

How the arguments are filled

Lean tries to fill all of the fields of the args : Packages.PreorderOfLEArgs α parameter automatically. If it fails, it is necessary to provide some of the fields manually.

• For the data-carrying typeclasses LE, LT and BEq, existing instances are always preferred. If no existing instances can be synthesized, it is attempted to derive an instance from the LE instance.
• Some proof obligations can be filled automatically if the data-carrying typeclasses have been derived from the LE instance. For example: If the beq field is omitted and no BEq α instance can be synthesized, it is derived from the LE α instance. In this case, beq_iff_le_and_ge can be omitted because Lean can infer that BEq α and LE α are compatible.
• Other proof obligations, namely le_refl and le_trans, can be omitted if Refl and Trans instances can be synthesized.

class Std.PartialOrderPackage (α : Type u) extends Std.PreorderPackage α, Std.IsPartialOrder α : Type u

This class entails LE α, LT α and BEq α instances as well as proofs that these operations represent the same partial order structure on α.

• le : α → α → Prop
• lt : α → α → Prop
• beq : α → α → Bool
• lt_iff (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• beq_iff_le_and_ge (a b : α) : (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• decidableLE : DecidableLE α
• decidableLT : DecidableLT α
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b

structure Std.Packages.PartialOrderOfLEArgs (α : Type u) extends Std.Packages.PreorderOfLEArgs α : Type u

This structure contains all the data needed to create a PartialOrderPakckage α instance. Its fields are automatically provided if possible. For the detailed rules how the fields are inferred, see PartialOrderPackage.ofLE.

• le : LE α
• decidableLE : DecidableLE α
• lt : let this := self.le; LT α
• beq : let this := self.le; let this := self.decidableLE; BEq α
• lt_iff : let this := self.le; let this_1 := self.lt; ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• decidableLT : let this := self.le; let this := self.decidableLE; let this := self.lt; have this_1 := ⋯; DecidableLT α
• beq_iff_le_and_ge : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.beq; ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl : let this := self.le; ∀ (a : α), a ≤ a
• le_trans : let this := self.le; ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• le_antisymm : let this := self.le; ∀ (a b : α), a ≤ b → b ≤ a → a = b

def Std.PartialOrderPackage.ofLE (α : Type u) (args : Packages.PartialOrderOfLEArgs α := by exact { }) : PartialOrderPackage α

def Std.FactoryInstances.instOrdOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : Ord α

instance Std.FactoryInstances.instLawfulOrderOrdOfDecidableLE {α : Type u} [LE α] [DecidableLE α] [Total fun (x1 x2 : α) => x1 ≤ x2] : LawfulOrderOrd α

class Std.LinearPreorderPackage (α : Type u) extends Std.PreorderPackage α, Ord α, Std.LawfulOrderOrd α, Std.IsLinearPreorder α : Type u

This class entails LE α, LT α, BEq α and Ord α instances as well as proofs that these operations represent the same linear preorder structure on α.

• le : α → α → Prop
• lt : α → α → Prop
• beq : α → α → Bool
• lt_iff (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• beq_iff_le_and_ge (a b : α) : (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• decidableLE : DecidableLE α
• decidableLT : DecidableLT α
• compare : α → α → Ordering
• isLE_compare (a b : α) : (compare a b).isLE = true ↔ a ≤ b
• isGE_compare (a b : α) : (compare a b).isGE = true ↔ b ≤ a
• le_total (a b : α) : a ≤ b ∨ b ≤ a

structure Std.Packages.LinearPreorderOfLEArgs (α : Type u) extends Std.Packages.PreorderOfLEArgs α : Type u

This structure contains all the data needed to create a LinearPreorderPackage α instance. Its fields are automatically provided if possible. For the detailed rules how the fields are inferred, see LinearPreorderPackage.ofLE.

• le : LE α
• decidableLE : DecidableLE α
• lt : let this := self.le; LT α
• beq : let this := self.le; let this := self.decidableLE; BEq α
• lt_iff : let this := self.le; let this_1 := self.lt; ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• decidableLT : let this := self.le; let this := self.decidableLE; let this := self.lt; have this_1 := ⋯; DecidableLT α
• beq_iff_le_and_ge : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.beq; ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl : let this := self.le; ∀ (a : α), a ≤ a
• le_trans : let this := self.le; ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• ord : let this := self.le; let this := self.decidableLE; Ord α
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• isLE_compare : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.ord; ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b
• isGE_compare : let this := self.le; let this_1 := self.decidableLE; have this_2 := ⋯; let this_3 := self.ord; ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a

def Std.LinearPreorderPackage.ofLE (α : Type u) (args : Packages.LinearPreorderOfLEArgs α := by exact { }) : LinearPreorderPackage α

Use this factory to conveniently define a linear preorder on a type α and all the associated operations and instances given an LE α instance.

Creates a LinearPreorderPackage α instance. Such an instance entails LE α, LT α, BEq α and Ord α instances as well as an IsLinearPreorder α instance and LawfulOrder* instances proving the compatibility of the operations with the linear preorder.

In the presence of LE α, DecidableLE α, Total (· ≤ ·) and Trans (· ≤ ·) (· ≤ ·) (· ≤ ·) instances, no arguments are required and the factory can be used as in this example:

public instance : LinearPreorderPackage X := .ofLE X

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly provide some arguments:

public instance : LinearPreorderPackage X := .ofLE X {
  le_total := sorry
  le_trans := sorry }

It is also possible to do all of this by hand, without resorting to LinearPreorderPackage. This can be useful if, say, one wants to avoid specifying an LT α instance, which is not possible with LinearPreorderPackage.

How the arguments are filled

Lean tries to fill all of the fields of the args : Packages.LinearPreorderOfLEArgs α parameter automatically. If it fails, it is necessary to provide some of the fields manually.

• For the data-carrying typeclasses LE, LT, BEq and Ord, existing instances are always preferred. If no existing instances can be synthesized, it is attempted to derive an instance from the LE instance.
• Some proof obligations can be filled automatically if the data-carrying typeclasses have been derived from the LE instance. For example: If the beq field is omitted and no BEq α instance can be synthesized, it is derived from the LE α instance. In this case, beq_iff_le_and_ge can be omitted because Lean can infer that BEq α and LE α are compatible.
• Other proof obligations, namely le_total and le_trans, can be omitted if Total and Trans instances can be synthesized.

class Std.LinearOrderPackage (α : Type u) extends Std.LinearPreorderPackage α, Std.PartialOrderPackage α, Min α, Max α, Std.LawfulOrderMin α, Std.LawfulOrderMax α, Std.IsLinearOrder α : Type u

This class entails LE α, LT α, BEq α, Ord α, Min α and Max α instances as well as proofs that these operations represent the same linear order structure on α.

• le : α → α → Prop
• lt : α → α → Prop
• beq : α → α → Bool
• lt_iff (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• beq_iff_le_and_ge (a b : α) : (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• decidableLE : DecidableLE α
• decidableLT : DecidableLT α
• compare : α → α → Ordering
• isLE_compare (a b : α) : (compare a b).isLE = true ↔ a ≤ b
• isGE_compare (a b : α) : (compare a b).isGE = true ↔ b ≤ a
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• min_eq_or (a b : α) : min a b = a ∨ min a b = b
• le_min_iff (a b c : α) : a ≤ min b c ↔ a ≤ b ∧ a ≤ c
• max_eq_or (a b : α) : max a b = a ∨ max a b = b
• max_le_iff (a b c : α) : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

structure Std.Packages.LinearOrderOfLEArgs (α : Type u) extends Std.Packages.LinearPreorderOfLEArgs α, Std.Packages.PartialOrderOfLEArgs α : Type u

This structure contains all the data needed to create a LinearOrderPackage α instance. Its fields are automatically provided if possible. For the detailed rules how the fields are inferred, see LinearOrderPackage.ofLE.

• le : LE α
• decidableLE : DecidableLE α
• lt : let this := self.le; LT α
• beq : let this := self.le; let this := self.decidableLE; BEq α
• lt_iff : let this := self.le; let this_1 := self.lt; ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• decidableLT : let this := self.le; let this := self.decidableLE; let this := self.lt; have this_1 := ⋯; DecidableLT α
• beq_iff_le_and_ge : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.beq; ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a
• le_refl : let this := self.le; ∀ (a : α), a ≤ a
• le_trans : let this := self.le; ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• ord : let this := self.le; let this := self.decidableLE; Ord α
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• isLE_compare : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.ord; ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b
• isGE_compare : let this := self.le; let this_1 := self.decidableLE; have this_2 := ⋯; let this_3 := self.ord; ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a
• le_antisymm : let this := self.le; ∀ (a b : α), a ≤ b → b ≤ a → a = b
• min : let this := self.le; let this := self.decidableLE; Min α
• max : let this := self.le; let this := self.decidableLE; Max α
• min_eq : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.min; ∀ (a b : α), Min.min a b = if a ≤ b then a else b
• max_eq : let this := self.le; let this_1 := self.decidableLE; let this_2 := self.max; ∀ (a b : α), Max.max a b = if b ≤ a then a else b

def Std.LinearOrderPackage.ofLE (α : Type u) (args : Packages.LinearOrderOfLEArgs α := by exact { }) : LinearOrderPackage α

Use this factory to conveniently define a linear order on a type α and all the associated operations and instances given an LE α instance.

Creates a LinearOrderPackage α instance. Such an instance entails LE α, LT α, BEq α, Ord α, Min α and Max α instances as well as an IsLinearOrder α instance and LawfulOrder* instances proving the compatibility of the operations with the linear order.

In the presence of LE α, DecidableLE α, Total (· ≤ ·), Trans (· ≤ ·) (· ≤ ·) (· ≤ ·) and Antisymm (· ≤ ·) instances, no arguments are required and the factory can be used as in this example:

public instance : LinearOrderPackage X := .ofLE X

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly provide some arguments:

public instance : LinearOrderPackage X := .ofLE X {
  le_total := sorry
  le_trans := sorry
  le_antisymm := sorry }

It is also possible to do all of this by hand, without resorting to LinearOrderPackage. This can be useful if, say, one wants to avoid specifying an LT α instance, which is not possible with LinearOrderPackage.

How the arguments are filled

Lean tries to fill all of the fields of the args : Packages.LinearOrderOfLEArgs α parameter automatically. If it fails, it is necessary to provide some of the fields manually.

• For the data-carrying typeclasses LE, LT, BEq, Ord, Min and Max, existing instances are always preferred. If no existing instances can be synthesized, it is attempted to derive an instance from the LE instance.
• Some proof obligations can be filled automatically if the data-carrying typeclasses have been derived from the LE instance. For example: If the beq field is omitted and no BEq α instance can be synthesized, it is derived from the LE α instance. In this case, beq_iff_le_and_ge can be omitted because Lean can infer that BEq α and LE α are compatible.
• Other proof obligations, namely le_total, le_trans and le_antisymm, can be omitted if Total, Trans and Antisymm instances can be synthesized.

theorem Std.OrientedCmp.of_gt_iff_lt {α : Type u} {cmp : α → α → Ordering} (h : ∀ (a b : α), cmp a b = Ordering.gt ↔ cmp b a = Ordering.lt) : OrientedCmp cmp

structure Std.Packages.LinearPreorderOfOrdArgs (α : Type u) : Type u

This structure contains all the data needed to create a LinearPreorderPackage α instance. Its fields are automatically provided if possible. For the detailed rules how the fields are inferred, see LinearPreorderPackage.ofOrd.

• ord : Ord α
• transOrd : TransOrd α
• le : let this := self.ord; LE α
• lawfulOrderOrd : let this := self.ord; let this_1 := ⋯; let this_2 := self.le; LawfulOrderOrd α
• decidableLE : let this := self.ord; let this := self.le; have this_1 := ⋯; DecidableLE α
• lt : let this := self.ord; LT α
• lt_iff : let this := self.ord; let this_1 := self.le; have this_2 := ⋯; let this_3 := self.lt; ∀ (a b : α), a < b ↔ compare a b = Ordering.lt
• decidableLT : let this := self.ord; let this := self.lt; let this_1 := self.le; have this_2 := ⋯; have this_3 := ⋯; DecidableLT α
• beq : let this := self.ord; BEq α
• beq_iff : let this := self.ord; let this_1 := self.le; have this_2 := ⋯; let this_3 := self.beq; ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq

def Std.LinearPreorderPackage.ofOrd (α : Type u) (args : Packages.LinearPreorderOfOrdArgs α := by exact { }) : LinearPreorderPackage α

Use this factory to conveniently define a linear preorder on a type α and all the associated operations and instances given an Ord α instance.

Creates a LinearPreorderPackage α instance. Such an instance entails LE α, LT α, BEq α and Ord α instances as well as an IsLinearPreorder α instance and LawfulOrder* instances proving the compatibility of the operations with the linear preorder.

In the presence of Ord α and TransOrd α instances, no arguments are required and the factory can be used as in this example:

public instance : LinearPreorderPackage X := .ofOrd X

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly provide some arguments:

public instance : LinearPreorderPackage X := .ofOrd X {
  ord := sorry
  transOrd := sorry }

It is also possible to do all of this by hand, without resorting to LinearPreorderPackage. This can be useful if, say, one wants to avoid specifying an LT α instance, which is not possible with LinearPreorderPackage.

How the arguments are filled

Lean tries to fill all of the fields of the args : Packages.LinearPreorderOfOrdArgs α parameter automatically. If it fails, it is necessary to provide some of the fields manually.

• For the data-carrying typeclasses LE, LT, BEq and Ord, existing instances are always preferred. If no existing instances can be synthesized, it is attempted to derive an instance from the Ord instance.
• Some proof obligations can be filled automatically if the data-carrying typeclasses have been derived from the Ord instance. For example: If the beq field is omitted and no BEq α instance can be synthesized, it is derived from the Ord α instance. In this case, beq_iff can be omitted because Lean can infer that BEq α and Ord α are compatible.
• Other proof obligations, for example transOrd, can be omitted if a matching instance can be synthesized.

def Std.FactoryInstances.instMinOfOrd {α : Type u} [Ord α] : Min α

def Std.FactoryInstances.instMaxOfOrd {α : Type u} [Ord α] : Max α

instance Std.FactoryInstances.instLawfulOrderLeftLeaningMinOfOrd {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] : LawfulOrderLeftLeaningMin α

instance Std.FactoryInstances.instLawfulOrderLeftLeaningMaxOfOrd {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] : LawfulOrderLeftLeaningMax α

structure Std.Packages.LinearOrderOfOrdArgs (α : Type u) extends Std.Packages.LinearPreorderOfOrdArgs α : Type u

This structure contains all the data needed to create a LinearOrderPackage α instance. Its fields are automatically provided if possible. For the detailed rules how the fields are inferred, see LinearOrderPackage.ofOrd.

• ord : Ord α
• transOrd : TransOrd α
• le : let this := self.ord; LE α
• lawfulOrderOrd : let this := self.ord; let this_1 := ⋯; let this_2 := self.le; LawfulOrderOrd α
• decidableLE : let this := self.ord; let this := self.le; have this_1 := ⋯; DecidableLE α
• lt : let this := self.ord; LT α
• lt_iff : let this := self.ord; let this_1 := self.le; have this_2 := ⋯; let this_3 := self.lt; ∀ (a b : α), a < b ↔ compare a b = Ordering.lt
• decidableLT : let this := self.ord; let this := self.lt; let this_1 := self.le; have this_2 := ⋯; have this_3 := ⋯; DecidableLT α
• beq : let this := self.ord; BEq α
• beq_iff : let this := self.ord; let this_1 := self.le; have this_2 := ⋯; let this_3 := self.beq; ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq
• eq_of_compare : let this := self.ord; let this_1 := self.le; ∀ (a b : α), compare a b = Ordering.eq → a = b
• min : let this := self.ord; Min α
• max : let this := self.ord; Max α
• min_eq : let this := self.ord; let this_1 := self.le; let this_2 := self.min; have this_3 := ⋯; ∀ (a b : α), Min.min a b = if (compare a b).isLE = true then a else b
• max_eq : let this := self.ord; let this_1 := self.le; let this_2 := self.max; have this_3 := ⋯; ∀ (a b : α), Max.max a b = if (compare a b).isGE = true then a else b

def Std.LinearOrderPackage.ofOrd (α : Type u) (args : Packages.LinearOrderOfOrdArgs α := by exact { }) : LinearOrderPackage α

Use this factory to conveniently define a linear order on a type α and all the associated operations and instances given an Ord α instance.

Creates a LinearOrderPackage α instance. Such an instance entails LE α, LT α, BEq α, Ord α, Min α and Max α instances as well as an IsLinearOrder α instance and LawfulOrder* instances proving the compatibility of the operations with the linear order.

In the presence of Ord α, TransOrd α and LawfulEqOrd α instances, no arguments are required and the factory can be used as in this example:

public instance : LinearOrderPackage X := .ofLE X

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly provide some arguments:

public instance : LinearOrderPackage X := .ofLE X {
  transOrd := sorry
  eq_of_compare := sorry }

It is also possible to do all of this by hand, without resorting to LinearOrderPackage. This can be useful if, say, one wants to avoid specifying an LT α instance, which is not possible with LinearOrderPackage.

How the arguments are filled

Lean tries to fill all of the fields of the args : Packages.LinearOrderOfLEArgs α parameter automatically. If it fails, it is necessary to provide some of the fields manually.

• For the data-carrying typeclasses LE, LT, BEq, Ord, Min and Max, existing instances are always preferred. If no existing instances can be synthesized, it is attempted to derive an instance from the Ord instance.
• Some proof obligations can be filled automatically if the data-carrying typeclasses have been derived from the Ord instance. For example: If the beq field is omitted and no BEq α instance can be synthesized, it is derived from the LE α instance. In this case, beq_iff can be omitted because Lean can infer that BEq α and Ord α are compatible.
• Other proof obligations, such as transOrd, can be omitted if matching instances can be synthesized.