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`.
This commit is contained in:
Paul Reichert
GitHub
parent
b75fbe7a40
commit
24cafcd65d
7 changed files with 706 additions and 2 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
552
src/Init/Data/Order/PackageFactories.lean
Normal file
552
src/Init/Data/Order/PackageFactories.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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⟩†
|
||||
|
|
|
|||
87
tests/lean/run/order.lean
Normal file
87
tests/lean/run/order.lean
Normal file
|
|
@ -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
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue