Converting Std order typeclasses into Mathlib ones

This file provides factories for creating Mathlib order typeclasses (PartialOrder, LinearOrder) from Std ones.

When all instances are present, the factories may be used without arguments:

instance : LinearOrder X := .ofStd X

Otherwise, it may be necessary to provide some instances manually:

instance : LinearOrder X := .ofStd X
  { lawfulOrderOrd := sorry }

When existing instances of typeclasses exist, they will be preferred; otherwise, they will be generated automatically.

Implementation notes

This module's job is to take a bunch of autoparams filled in with all the ways we could synthesize order typeclasses from Std and bundle them into a Mathlib order typeclass. We also need inheritance of sets of autoparams, because PartialOrder.ofStd takes all the autoparams of Preorder.ofStd and then some.

To achieve this, each set of autoparams becomes a structure called OfStdArgs (thereby allowing it to extend existing OfStdArgs structures), and the synthesization scripts are in the default field values of this type. For the user, a simple {} will synthesize all fields of the structure with tactics, while individual fields that fail to synthesize may be specified using { field := … }.

The autoparam tactic scripts prioritize existing instances if they exist, to prevent diamonds, and in such cases require extra Prop typeclasses to ensure everyone agrees on the order. Otherwise, those agreement typeclasses can be synthesized with tactics automatically.

Often, we write let := someField in the type of the structure fields, followed by extract_lets in the tactic body. This is done to make sure that someField is an instance that can be found by typeclass search in the tactic body: in the case where someField is generated by some means other than typeclass inference, it does not exist as a local variable otherwise.

structure Preorder.OfStdArgs (α : Type u_1) : Type u_1

Arguments for Preorder.ofStd; see that function for details.

• le : LE α

  The LE instance of the order.

• lt : let this := self.le; LT α

  The LT instance of the order.

• lawfulOrderLT : let this := self.le; let this_1 := self.lt; Std.LawfulOrderLT α

  a < b is equivalent to a ≤ b ∧ ¬b ≤ a.

• isPreorder : let this := self.le; Std.IsPreorder α

  ≤ forms a preorder.

@[implicit_reducible]

def Preorder.ofStd (α : Type u_1) (args : OfStdArgs α := by exact { }) : Preorder α

Create a Preorder from a type satisfying Std.IsPreorder.

If an LE instance exists, either an Std.IsPreorder instance must exist, or there must be an Ord instance together with Std.LawfulOrderOrd and Std.TransOrd instances.

If no LE instance exists, it can be generated from Ord and Std.TransOrd instances.

If an LT instance exists, an Std.LawfulOrderLT instance must exist also; otherwise, a suitable LT instance will be generated.

Equations

• Preorder.ofStd α args = { toLE := args.le, toLT := args.lt, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

structure PartialOrder.OfStdArgs (α : Type u_1) extends Preorder.OfStdArgs α : Type u_1

Arguments for PartialOrder.ofStd; see that function for details.

• le : LE α
• lt : let this := self.le; LT α
• lawfulOrderLT : let this := self.le; let this_1 := self.lt; Std.LawfulOrderLT α
• isPreorder : let this := self.le; Std.IsPreorder α
• isPartialOrder : let this := self.le; Std.IsPartialOrder α

  ≤ forms a partial order.

@[implicit_reducible]

def PartialOrder.ofStd (α : Type u_1) (args : OfStdArgs α := by exact { }) : PartialOrder α

Create a PartialOrder from a type satisfying Std.IsPartialOrder.

If an LE instance exists, either an Std.IsPartialOrder instance must exist, or there must be an Ord instance together with Std.LawfulOrderOrd, Std.LawfulEqOrd, and Std.TransOrd instances.

If no LE instance exists, it can be generated from Ord, Std.LawfulEqOrd, and Std.TransOrd instances.

If an LT instance exists, an Std.LawfulOrderLT instance must exist also; otherwise, a suitable LT instance will be generated.

Equations

• PartialOrder.ofStd α args = { toPreorder := Preorder.ofStd α args.toPreorderArgs, le_antisymm := ⋯ }

theorem Std.LawfulOrderCmp.compareOfLessAndEq (α : Type u_1) [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [DecidableEq α] [DecidableLT α] : LawfulOrderCmp fun (a b : α) => _root_.compareOfLessAndEq a b

structure LinearOrder.OfStdArgs (α : Type u_1) extends PartialOrder.OfStdArgs α : Type u_1

Arguments for LinearOrder.ofStd; see that function for details.

• le : LE α
• lt : let this := self.le; LT α
• lawfulOrderLT : let this := self.le; let this_1 := self.lt; Std.LawfulOrderLT α
• isPreorder : let this := self.le; Std.IsPreorder α
• isPartialOrder : let this := self.le; Std.IsPartialOrder α
• isLinearOrder : let this := self.le; Std.IsLinearOrder α

  ≤ forms a linear order.

• decidableLE : DecidableLE α

  ≤ is decidable.

• decidableEq : let this := self.toPartialOrderArgs; let this := self.decidableLE; DecidableEq α

  = is decidable. This can always be automatically derived from decidableLE.

• decidableLT : let this := self.toPreorderArgs; let this := self.decidableLE; DecidableLT α

  < is decidable. This can always be automatically derived from decidableLE.

• min : let this := self.le; let this := self.decidableLE; Min α

  The Min instance of the order. This can always be automatically derived.

• max : let this := self.le; let this := self.decidableLE; Max α

  The Max instance of the order. This can always be automatically derived.

• lawfulOrderLeftLeaningMin : Std.LawfulOrderLeftLeaningMin α

  min a b is equivalent to if a ≤ b then a else b.

• lawfulOrderLeftLeaningMax : Std.LawfulOrderLeftLeaningMax α

  max a b is equivalent to if b ≤ a then a else b.

• ord : let this := self.lt; let this := self.decidableEq; let this := self.decidableLT; Ord α

  The Ord instance of the order. This can always be automatically derived.

• lawfulOrderOrd : let this := self.le; let this_1 := self.lt; let this_2 := ⋯; let this_3 := ⋯; let this_4 := self.decidableEq; let this_5 := self.decidableLT; Std.LawfulOrderOrd α

  Ord is compatible with ≤.

@[implicit_reducible]

def LinearOrder.ofStd (α : Type u_1) (args : OfStdArgs α := by exact { }) : LinearOrder α

Create a LinearOrder from a type satisfying Std.IsLinearOrder.

If an LE instance exists, either an Std.IsLinearOrder instance must exist, or there must be an Ord instance together with Std.LawfulOrderOrd, Std.LawfulEqOrd, and Std.TransOrd instances.

If no LE instance exists, it can be generated from Ord, Std.LawfulEqOrd, and Std.TransOrd instances.

If an LT instance exists, an Std.LawfulOrderLT instance must exist also; otherwise, a suitable LT instance will be generated.

If a DecidableLE instance exists, it will be used. Otherwise, it can be generated from an Ord instance.

If DecidableEq and DecidableLT instances exist, they will be used. Otherwise, they will be generated from the DecidableLE instance.

If Min and Max instances exist, they will be used, in which case the user must provide Std.LawfulOrderLeftLeaningMin or Std.LawfulOrderLeftLeaningMax respectively. Otherwise, they will be generated.

If an Ord instance exists, it will be used, in which case the user must provide an Std.LawfulOrderOrd instance. Otherwise, it will be generated.

Equations

• One or more equations did not get rendered due to their size.