From 24cafcd65dabf3ddc4f4573372932352deb2c38a Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 19 Aug 2025 15:43:29 +0200 Subject: [PATCH] feat: package factories for order typeclasses (#9797) This PR provides the means to quickly provide all the order instances associated with some high-level order structure (preorder, partial order, linear preorder, linear order). This can be done via the factory functions `PreorderPackage.ofLE`, `PartialOrderPackage.ofLE`, `LinearPreorderPackage.ofLE` and `LinearOrderPackage.ofLE`. --- src/Init/Data/Order.lean | 2 +- src/Init/Data/Order/Classes.lean | 14 + src/Init/Data/Order/Lemmas.lean | 41 ++ src/Init/Data/Order/LemmasExtra.lean | 10 + src/Init/Data/Order/PackageFactories.lean | 552 ++++++++++++++++++++++ tests/lean/run/info_trees.lean | 2 +- tests/lean/run/order.lean | 87 ++++ 7 files changed, 706 insertions(+), 2 deletions(-) create mode 100644 src/Init/Data/Order/PackageFactories.lean create mode 100644 tests/lean/run/order.lean diff --git a/src/Init/Data/Order.lean b/src/Init/Data/Order.lean index db5e82ae67..07ef84a7c6 100644 --- a/src/Init/Data/Order.lean +++ b/src/Init/Data/Order.lean @@ -13,4 +13,4 @@ public import Init.Data.Order.Lemmas public import Init.Data.Order.LemmasExtra public import Init.Data.Order.Factories public import Init.Data.Order.FactoriesExtra -public import Init.Data.Subtype.Order +public import Init.Data.Order.PackageFactories diff --git a/src/Init/Data/Order/Classes.lean b/src/Init/Data/Order/Classes.lean index 967f3f6f4f..43f4678ebc 100644 --- a/src/Init/Data/Order/Classes.lean +++ b/src/Init/Data/Order/Classes.lean @@ -138,6 +138,13 @@ the other. -/ public class LawfulOrderMin (α : Type u) [Min α] [LE α] extends MinEqOr α, LawfulOrderInf α +/-- +This typeclass states that `min a b = if a ≤ b then a else b` (for any `DecidableLE α` instance). +-/ +public class LawfulOrderLeftLeaningMin (α : Type u) [Min α] [LE α] where + min_eq_left : ∀ a b : α, a ≤ b → min a b = a + min_eq_right : ∀ a b : α, ¬ a ≤ b → min a b = b + end Min section Max @@ -175,6 +182,13 @@ the other. -/ public class LawfulOrderMax (α : Type u) [Max α] [LE α] extends MaxEqOr α, LawfulOrderSup α +/-- +This typeclass states that `max a b = if b ≤ a then a else b` (for any `DecidableLE α` instance). +-/ +public class LawfulOrderLeftLeaningMax (α : Type u) [Max α] [LE α] where + max_eq_left : ∀ a b : α, b ≤ a → max a b = a + max_eq_right : ∀ a b : α, ¬ b ≤ a → max a b = b + end Max end Std diff --git a/src/Init/Data/Order/Lemmas.lean b/src/Init/Data/Order/Lemmas.lean index 8d97b7d163..a609f72f08 100644 --- a/src/Init/Data/Order/Lemmas.lean +++ b/src/Init/Data/Order/Lemmas.lean @@ -70,6 +70,11 @@ public theorem le_total {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)] a ≤ b ∨ b ≤ a := Std.Total.total a b +public theorem le_of_not_ge {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)] {a b : α} : + ¬ b ≤ a → a ≤ b := by + intro h + simpa [h] using Std.Total.total a b (r := (· ≤ ·)) + end LE section LT @@ -272,6 +277,31 @@ public instance {α : Type u} [LE α] [Min α] [IsLinearOrder α] [LawfulOrderMi Std.Associative (min : α → α → α) where assoc a b c := by apply le_antisymm <;> simp [min_le, le_min_iff, le_refl] +public theorem min_eq_if {α : Type u} [LE α] [DecidableLE α] {_ : Min α} + [LawfulOrderLeftLeaningMin α] {a b : α} : + min a b = if a ≤ b then a else b := by + split <;> rename_i h + · simp [LawfulOrderLeftLeaningMin.min_eq_left _ _ h] + · simp [LawfulOrderLeftLeaningMin.min_eq_right _ _ h] + +public theorem max_eq_if {α : Type u} [LE α] [DecidableLE α] {_ : Max α} + [LawfulOrderLeftLeaningMax α] {a b : α} : + max a b = if b ≤ a then a else b := by + split <;> rename_i h + · simp [LawfulOrderLeftLeaningMax.max_eq_left _ _ h] + · simp [LawfulOrderLeftLeaningMax.max_eq_right _ _ h] + +public instance {α : Type u} [LE α] [Min α] [IsLinearOrder α] [LawfulOrderInf α] : + LawfulOrderLeftLeaningMin α where + min_eq_left a b hab := by + apply le_antisymm + · apply min_le_left + · simp [le_min_iff, le_refl, hab] + min_eq_right a b hab := by + apply le_antisymm + · apply min_le_right + · simp [le_min_iff, le_refl, le_of_not_ge hab] + end Min section Max @@ -356,6 +386,17 @@ public instance {α : Type u} [LE α] [Max α] [IsLinearOrder α] [LawfulOrderMa simp only [max_le_iff] simp [le_max, le_refl] +public instance {α : Type u} [LE α] [Max α] [IsLinearOrder α] [LawfulOrderSup α] : + LawfulOrderLeftLeaningMax α where + max_eq_left a b hab := by + apply le_antisymm + · simp [max_le_iff, le_refl, hab] + · apply left_le_max + max_eq_right a b hab := by + apply le_antisymm + · simp [max_le_iff, le_refl, le_of_not_ge hab] + · apply right_le_max + end Max end Std diff --git a/src/Init/Data/Order/LemmasExtra.lean b/src/Init/Data/Order/LemmasExtra.lean index db45264d8c..bdf26732c4 100644 --- a/src/Init/Data/Order/LemmasExtra.lean +++ b/src/Init/Data/Order/LemmasExtra.lean @@ -145,6 +145,16 @@ public instance LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [L toLawfulOrderSup := .of_ord α compare_max_isLE_iff max_eq_or := max_eq_or +public theorem min_eq_if_isLE_compare {α : Type u} [Ord α] [LE α] {_ : Min α} + [LawfulOrderOrd α] [LawfulOrderLeftLeaningMin α] {a b : α} : + min a b = if (compare a b).isLE then a else b := by + open Classical in simp [min_eq_if, isLE_compare] + +public theorem max_eq_if_isGE_compare {α : Type u} [Ord α] [LE α] {_ : Max α} + [LawfulOrderOrd α] [LawfulOrderLeftLeaningMax α] + {a b : α} : max a b = if (compare a b).isGE then a else b := by + open Classical in simp [max_eq_if, isGE_compare] + end Std namespace Classical.Order diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean new file mode 100644 index 0000000000..1c5c228baf --- /dev/null +++ b/src/Init/Data/Order/PackageFactories.lean @@ -0,0 +1,552 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Init.Data.Order.FactoriesExtra +public import Init.Data.Order.LemmasExtra + +namespace Std + +/-! +## 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. +-/ + +section Preorder + +/-- +This class entails `LE α`, `LT α` and `BEq α` instances as well as proofs that these operations +represent the same preorder structure on `α`. +-/ +public class PreorderPackage (α : Type u) extends + LE α, LT α, BEq α, LawfulOrderLT α, LawfulOrderBEq α, IsPreorder α where + decidableLE : DecidableLE α + decidableLT : DecidableLT α + +public instance [PreorderPackage α] : DecidableLE α := PreorderPackage.decidableLE +public instance [PreorderPackage α] : DecidableLT α := PreorderPackage.decidableLT + +namespace FactoryInstances + +public scoped instance beqOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : + BEq α where + beq a b := a ≤ b ∧ b ≤ a + +public instance instLawfulOrderBEqOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : + LawfulOrderBEq α where + beq_iff_le_and_ge := by simp [BEq.beq] + +/-- If `LT` can be characterized in terms of a decidable `LE`, then `LT` is decidable either. -/ +@[expose] +public def decidableLTOfLE {α : Type u} [LE α] {_ : LT α} [DecidableLE α] [LawfulOrderLT α] : + DecidableLT α := + fun a b => + haveI := iff_iff_eq.mp <| LawfulOrderLT.lt_iff a b + if h : a ≤ b ∧ ¬ b ≤ a then .isTrue (this ▸ h) else .isFalse (this ▸ h) + +end FactoryInstances + +/-- +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`. +-/ +public structure Packages.PreorderOfLEArgs (α : Type u) where + le : LE α := by infer_instance + decidableLE : DecidableLE α := by infer_instance + lt : + let := le + LT α := by + extract_lets + first + | infer_instance + | exact Classical.Order.instLT + beq : + let := le; let := decidableLE + BEq α := by + extract_lets + first + | infer_instance + | exact FactoryInstances.beqOfDecidableLE + lt_iff : + let := le; let := lt + ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a := by + extract_lets + first + | exact LawfulOrderLT.lt_iff + | fail "Failed to automatically prove that the `LE` and `LT` instances are compatible. \ + Please ensure that a `LawfulOrderLT` instance can be synthesized or \ + manually provide the field `lt_iff`." + decidableLT : + let := le; let := decidableLE; let := lt; haveI := lt_iff + have := lt_iff + DecidableLT α := by + extract_lets + haveI := @LawfulOrderLT.mk (lt_iff := by assumption) .. + first + | infer_instance + | exact FactoryInstances.decidableLTOfLE + | fail "Failed to automatically derive that `LT` is decidable. \ + Please ensure that a `DecidableLT` instance can be synthesized or \ + manually provide the field `decidableLT`." + beq_iff_le_and_ge : + let := le; let := decidableLE; let := beq + ∀ a b : α, a == b ↔ a ≤ b ∧ b ≤ a := by + extract_lets + first + | exact LawfulOrderBEq.beq_iff_le_and_ge + | fail "Failed to automatically prove that the `LE` and `BEq` instances are compatible. \ + Please ensure that a `LawfulOrderBEq` instance can be synthesized or \ + manually provide the field `beq_iff_le_and_ge`." + le_refl : + let := le + ∀ a : α, a ≤ a := by + extract_lets + first + | exact Std.Refl.refl (r := (· ≤ ·)) + | fail "Failed to automatically prove that the `LE` instance is reflexive. \ + Please ensure that a `Refl` instance can be synthesized or \ + manually provide the field `le_refl`." + le_trans : + let := le + ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c := by + extract_lets + first + | exact fun _ _ _ hab hbc => Trans.trans (r := (· ≤ ·)) (s := (· ≤ ·)) (t := (· ≤ ·)) hab hbc + | fail "Failed to automatically prove that the `LE` instance is transitive. \ + Please ensure that a `Trans` instance can be synthesized or \ + manually provide the field `le_trans`." + +/-- +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: + +```lean +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: + +```lean +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. +-/ +@[expose] +public def PreorderPackage.ofLE (α : Type u) + (args : Packages.PreorderOfLEArgs α := by exact {}) : PreorderPackage α where + toLE := args.le + decidableLE := args.decidableLE + toLT := args.lt + toBEq := args.beq + toLawfulOrderLT := @LawfulOrderLT.mk (lt_iff := args.lt_iff) + decidableLT := args.decidableLT + toLawfulOrderBEq := @LawfulOrderBEq.mk (beq_iff_le_and_ge := args.beq_iff_le_and_ge) + le_refl := args.le_refl + le_trans := args.le_trans + +end Preorder + +section PartialOrder + +/-- +This class entails `LE α`, `LT α` and `BEq α` instances as well as proofs that these operations +represent the same partial order structure on `α`. +-/ +public class PartialOrderPackage (α : Type u) extends + PreorderPackage α, IsPartialOrder α + +/-- +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`. +-/ +public structure Packages.PartialOrderOfLEArgs (α : Type u) extends Packages.PreorderOfLEArgs α where + le_antisymm : + let := le + ∀ a b : α, a ≤ b → b ≤ a → a = b := by + extract_lets + first + | exact Antisymm.antisymm + | fail "Failed to automatically prove that the `LE` instance is antisymmetric. \ + Please ensure that a `Antisymm` instance can be synthesized or \ + manually provide the field `le_antisymm`." + +/- +Use this factory to conveniently define a partial order on a type `α` and all the associated +operations and instances given an `LE α` instance. + +Creates a `PartialOrderPackage α` instance. Such an instance entails `LE α`, `LT α` and +`BEq α` instances as well as an `IsPartialOrder α` instance and `LawfulOrder*` instances proving the +compatibility of the operations with the preorder. + +In the presence of `LE α`, `DecidableLE α`, `Refl (· ≤ ·)`, `Trans (· ≤ ·) (· ≤ ·) (· ≤ ·)` +and `Antisymm (· ≤ ·)` instances, no arguments are required and the factory can be used as in this +example: + +```lean +public instance : PartialOrderPackage X := .ofLE X +``` + +If not all of these instances are available via typeclass synthesis, it is necessary to explicitly +provide some arguments: + +```lean +public instance : PartialOrderPackage X := .ofLE X { + le_refl := sorry + le_trans := sorry + le_antisymm := sorry } +``` + +It is also possible to do all of this by hand, without resorting to `PartialOrderPackage`. This can +be useful if, say, one wants to avoid specifying an `LT α` instance, which is not possible with +`PartialOrderPackage`. + +**How the arguments are filled** + +Lean tries to fill all of the fields of the `args : Packages.PartialOrderOfLEArgs α` 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`, `le_trans` and `le_antisymm`, can be omitted if `Refl`, + `Trans` and `Antisymm` instances can be synthesized. +-/ +@[expose] +public def PartialOrderPackage.ofLE (α : Type u) + (args : Packages.PartialOrderOfLEArgs α := by exact {}) : PartialOrderPackage α where + toPreorderPackage := .ofLE α args.toPreorderOfLEArgs + le_antisymm := args.le_antisymm + +end PartialOrder + +namespace FactoryInstances + +public scoped instance instOrdOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : + Ord α where + compare a b := if a ≤ b then if b ≤ a then .eq else .lt else .gt + +theorem isLE_compare {α : Type u} [LE α] [DecidableLE α] {a b : α} : + (compare a b).isLE ↔ a ≤ b := by + simp only [compare] + split + · split <;> simp_all + · simp_all + +theorem isGE_compare {α : Type u} [LE α] [DecidableLE α] + (le_total : ∀ a b : α, a ≤ b ∨ b ≤ a) {a b : α} : + (compare a b).isGE ↔ b ≤ a := by + simp only [compare] + split + · split <;> simp_all + · specialize le_total a b + simp_all + +public instance instLawfulOrderOrdOfDecidableLE {α : Type u} [LE α] [DecidableLE α] + [Total (α := α) (· ≤ ·)] : + LawfulOrderOrd α where + isLE_compare _ _ := by exact isLE_compare + isGE_compare _ _ := by exact isGE_compare (le_total := Total.total) + +end FactoryInstances + +/-- +This class entails `LE α`, `LT α`, `BEq α` and `Ord α` instances as well as proofs that these +operations represent the same linear preorder structure on `α`. +-/ +public class LinearPreorderPackage (α : Type u) extends + PreorderPackage α, Ord α, LawfulOrderOrd α, IsLinearPreorder α + +/-- +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`. +-/ +public structure Packages.LinearPreorderOfLEArgs (α : Type u) extends + PreorderOfLEArgs α where + ord : + let := le; let := decidableLE + Ord α := by + extract_lets + first + | infer_instance + | exact FactoryInstances.instOrdOfDecidableLE + le_total : + ∀ a b : α, a ≤ b ∨ b ≤ a := by + first + | exact Total.total + | fail "Failed to automatically prove that the `LE` instance is total. \ + Please ensure that a `Total` instance can be synthesized or \ + manually provide the field `le_total`." + le_refl a := (by simpa using le_total a a) + isLE_compare : + let := le; let := decidableLE; let := ord + ∀ a b : α, (compare a b).isLE ↔ a ≤ b := by + extract_lets + first + | exact LawfulOrderOrd.isLE_compare + | fail "Failed to automatically prove that `(compare a b).isLE` is equivalent to `a ≤ b`. \ + Please ensure that a `LawfulOrderOrd` instance can be synthesized or \ + manually provide the field `isLE_compare`." + isGE_compare : + let := le; let := decidableLE; have := le_total; let := ord + ∀ a b : α, (compare a b).isGE ↔ b ≤ a := by + extract_lets + first + | exact LawfulOrderOrd.isGE_compare + | fail "Failed to automatically prove that `(compare a b).isGE` is equivalent to `b ≤ a`. \ + Please ensure that a `LawfulOrderOrd` instance can be synthesized or \ + manually provide the field `isGE_compare`." + +/-- +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: + +```lean +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: + +```lean +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. +-/ +@[expose] +public def LinearPreorderPackage.ofLE (α : Type u) + (args : Packages.LinearPreorderOfLEArgs α := by exact {}) : LinearPreorderPackage α where + toPreorderPackage := .ofLE α args.toPreorderOfLEArgs + toOrd := letI := args.le; args.ord + le_total := args.le_total + isLE_compare := args.isLE_compare + isGE_compare := args.isGE_compare + +namespace FactoryInstances + +public scoped instance instMinOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : Min α where + min a b := if a ≤ b then a else b + +public scoped instance instMaxOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : Max α where + max a b := if b ≤ a then a else b + +public instance instLawfulOrderLeftLeaningMinOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : + LawfulOrderLeftLeaningMin α where + min_eq_left a b := by simp +contextual [min] + min_eq_right a b := by simp +contextual [min] + +public instance instLawfulOrderLeftLeaningMaxOfDecidableLE {α : Type u} [LE α] [DecidableLE α] : + LawfulOrderLeftLeaningMax α where + max_eq_left a b := by simp +contextual [max] + max_eq_right a b := by simp +contextual [max] + +end FactoryInstances + +/-- +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 `α`. +-/ +public class LinearOrderPackage (α : Type u) extends + LinearPreorderPackage α, PartialOrderPackage α, Min α, Max α, + LawfulOrderMin α, LawfulOrderMax α, IsLinearOrder α + +/-- +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`. +-/ +public structure Packages.LinearOrderOfLEArgs (α : Type u) extends + LinearPreorderOfLEArgs α, PartialOrderOfLEArgs α where + min : + let := le; let := decidableLE + Min α := by + extract_lets + first + | infer_instance + | exact FactoryInstances.instMinOfDecidableLE + max : + let := le; let := decidableLE + Max α := by + extract_lets + first + | infer_instance + | exact FactoryInstances.instMaxOfDecidableLE + min_eq : + let := le; let := decidableLE; let := min + ∀ a b : α, Min.min a b = if a ≤ b then a else b := by + extract_lets + first + | exact fun a b => Std.min_eq_if (a := a) (b := b) + | fail "Failed to automatically prove that `min` is left-leaning. \ + Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \ + manually provide the field `min_eq`." + max_eq : + let := le; let := decidableLE; let := max + ∀ a b : α, Max.max a b = if b ≤ a then a else b := by + extract_lets + first + | exact fun a b => Std.max_eq_if (a := a) (b := b) + | fail "Failed to automatically prove that `max` is left-leaning. \ + Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \ + manually provide the field `max_eq`." + +public theorem IsLinearPreorder.lawfulOrderMin_of_min_eq {α : Type u} [LE α] + [DecidableLE α] [Min α] [IsLinearPreorder α] + (min_eq : ∀ a b : α, min a b = if a ≤ b then a else b) : + LawfulOrderMin α where + min_eq_or a b := by + rw [min_eq] + split <;> simp + le_min_iff a b c := by + simp only [min_eq] + split <;> rename_i hbc + · simp only [iff_self_and] + exact fun hab => le_trans hab hbc + · simp only [iff_and_self] + exact fun hac => le_trans hac (by simpa [hbc] using Std.le_total (a := b) (b := c)) + +public theorem IsLinearPreorder.lawfulOrderMax_of_max_eq {α : Type u} [LE α] + [DecidableLE α] [Max α] [IsLinearPreorder α] + (max_eq : ∀ a b : α, max a b = if b ≤ a then a else b) : + LawfulOrderMax α where + max_eq_or a b := by + rw [max_eq] + split <;> simp + max_le_iff a b c := by + simp only [max_eq] + split <;> rename_i hab + · simp only [iff_self_and] + exact fun hbc => le_trans hab hbc + · simp only [iff_and_self] + exact fun hac => le_trans (by simpa [hab] using Std.le_total (a := a) (b := b)) hac + +/-- +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: + +```lean +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: + +```lean +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. +-/ +@[expose] +public def LinearOrderPackage.ofLE (α : Type u) + (args : Packages.LinearOrderOfLEArgs α := by exact {}) : LinearOrderPackage α where + toLinearPreorderPackage := .ofLE α args.toLinearPreorderOfLEArgs + le_antisymm := (PartialOrderPackage.ofLE α args.toPartialOrderOfLEArgs).le_antisymm + toMin := args.min + toMax := args.max + toLawfulOrderMin := + letI := LinearPreorderPackage.ofLE α args.toLinearPreorderOfLEArgs + letI := args.decidableLE; letI := args.min + IsLinearPreorder.lawfulOrderMin_of_min_eq args.min_eq + toLawfulOrderMax := + letI := LinearPreorderPackage.ofLE α args.toLinearPreorderOfLEArgs + letI := args.decidableLE; letI := args.max + IsLinearPreorder.lawfulOrderMax_of_max_eq args.max_eq + +end Std diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean index 4cf35da961..ef1d9c8278 100644 --- a/tests/lean/run/info_trees.lean +++ b/tests/lean/run/info_trees.lean @@ -61,7 +61,7 @@ info: • [Command] @ ⟨83, 0⟩-⟨83, 40⟩ @ Lean.Elab.Command.elabDeclarati ⊢ 0 ≤ n after no goals • [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp - • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.36 @ ⟨1, 0⟩†-⟨1, 0⟩† + • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.37 @ ⟨1, 0⟩†-⟨1, 0⟩† • [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩† • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent • [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩† diff --git a/tests/lean/run/order.lean b/tests/lean/run/order.lean new file mode 100644 index 0000000000..33bc1fb2f3 --- /dev/null +++ b/tests/lean/run/order.lean @@ -0,0 +1,87 @@ + +import Init.Data.Order.PackageFactories + +open Std + +variable {α : Type u} + +opaque X : Type := Unit + +namespace X + +#guard_msgs(error, drop warning) in +opaque instLE : LE X := sorry +attribute [scoped instance] instLE + +#guard_msgs(error, drop warning) in +@[scoped instance] opaque instDecidableLE : DecidableLE X := sorry + +#guard_msgs(error, drop warning) in +@[instance] opaque instTotal : Total (α := X) (· ≤ ·) := sorry + +#guard_msgs(error, drop warning) in +@[instance] opaque instAntisymm : Antisymm (α := X) (· ≤ ·) := sorry + +#guard_msgs(error, drop warning) in +@[instance] opaque instTrans : Trans (α := X) (· ≤ ·) (· ≤ ·) (· ≤ ·) := sorry + +namespace Package + +scoped instance packageOfLE : LinearOrderPackage X := .ofLE X + +example : instLE = (inferInstanceAs (PreorderPackage X)).toLE := rfl +example : IsLinearOrder X := inferInstance +example : LawfulOrderLT X := inferInstance +example : LawfulOrderOrd X := inferInstance +example : LawfulOrderMin X := inferInstance +example : LawfulOrderMax X := inferInstance +example : LawfulOrderLeftLeaningMin X := inferInstance +example : LawfulOrderLeftLeaningMax X := inferInstance + +end Package + +end X + +section + +def packageWithoutSynthesizableInstances : LinearOrderPackage X := .ofLE X { + le := X.instLE + decidableLE := X.instDecidableLE } + +end + +section + +attribute [local instance] X.Package.packageOfLE + +def packageWithoutSynthesizableInstances' : LinearOrderPackage X := .ofLE X { + le := X.instLE + decidableLE := X.instDecidableLE +} + +end + +/-- +error: could not synthesize default value for field 'lt_iff' of 'Std.Packages.PreorderOfLEArgs' using tactics +--- +error: Failed to automatically prove that the `LE` and `LT` instances are compatible. Please ensure that a `LawfulOrderLT` instance can be synthesized or manually provide the field `lt_iff`. +α : Type u +inst✝² : LE α +inst✝¹ : DecidableLE α +inst✝ : LT α +this✝¹ : LE α := inferInstance +this✝ : LT α := inferInstance +⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a +-/ +#guard_msgs in +def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : PreorderPackage α := .ofLE α { + le_refl := sorry + le_trans := sorry +} + +def packageOfLEOfLT2 [LE α] [DecidableLE α] [LT α] (h : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) : + PreorderPackage α := .ofLE α { + lt_iff := h + le_refl := sorry + le_trans := sorry +}