|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Sabrina Jewson. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Sabrina Jewson |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Order.Defs.LinearOrder |
| 9 | + |
| 10 | +/-! |
| 11 | +# Converting Std order typeclasses into Mathlib ones |
| 12 | +
|
| 13 | +This file provides factories for creating Mathlib order typeclasses (`PartialOrder`, `LinearOrder`) |
| 14 | +from Std ones. |
| 15 | +
|
| 16 | +When all instances are present, the factories may be used without arguments: |
| 17 | +
|
| 18 | +```lean |
| 19 | +instance : LinearOrder X := .ofStd X |
| 20 | +``` |
| 21 | +
|
| 22 | +Otherwise, it may be necessary to provide some instances manually: |
| 23 | +
|
| 24 | +```lean |
| 25 | +instance : LinearOrder X := .ofStd X |
| 26 | + { lawfulOrderOrd := sorry } |
| 27 | +``` |
| 28 | +
|
| 29 | +When existing instances of typeclasses exist, they will be preferred; otherwise, they will be |
| 30 | +generated automatically. |
| 31 | +
|
| 32 | +## Implementation notes |
| 33 | +
|
| 34 | +This module's job is to take a bunch of autoparams filled in with all the ways we could synthesize |
| 35 | +order typeclasses from `Std` and bundle them into a Mathlib order typeclass. We also need |
| 36 | +inheritance of sets of autoparams, because `PartialOrder.ofStd` takes all the autoparams of |
| 37 | +`Preorder.ofStd` and then some. |
| 38 | +
|
| 39 | +To achieve this, each set of autoparams becomes a structure called `OfStdArgs` (thereby allowing it |
| 40 | +to extend existing `OfStdArgs` structures), and the synthesization scripts are in the default field |
| 41 | +values of this type. For the user, a simple `{}` will synthesize all fields of the structure with |
| 42 | +tactics, while individual fields that fail to synthesize may be specified using `{ field := … }`. |
| 43 | +
|
| 44 | +The autoparam tactic scripts prioritize existing instances if they exist, to prevent diamonds, |
| 45 | +and in such cases require extra `Prop` typeclasses to ensure everyone agrees on the order. |
| 46 | +Otherwise, those agreement typeclasses can be synthesized with tactics automatically. |
| 47 | +
|
| 48 | +Often, we write `let := someField` in the type of the structure fields, followed by `extract_lets` |
| 49 | +in the tactic body. This is done to make sure that `someField` is an instance that can be found by |
| 50 | +typeclass search in the tactic body: in the case where `someField` is generated by some means other |
| 51 | +than typeclass inference, it does not exist as a local variable otherwise. |
| 52 | +-/ |
| 53 | + |
| 54 | +public section |
| 55 | + |
| 56 | +/-- Arguments for `Preorder.ofStd`; see that function for details. -/ |
| 57 | +structure Preorder.OfStdArgs (α : Type*) where |
| 58 | + /-- The `LE` instance of the order. -/ |
| 59 | + le : LE α := by |
| 60 | + first |
| 61 | + | infer_instance |
| 62 | + | exact LE.ofOrd _ |
| 63 | + | fail "failed to infer `LE` instance; \ |
| 64 | + make sure you have an `LE` or `Ord` instance" |
| 65 | + /-- The `LT` instance of the order. -/ |
| 66 | + lt : |
| 67 | + let := le |
| 68 | + LT α := by |
| 69 | + extract_lets |
| 70 | + first |
| 71 | + | infer_instance |
| 72 | + | exact ⟨fun a b ↦ a ≤ b ∧ ¬b ≤ a⟩ |
| 73 | + /-- `a < b` is equivalent to `a ≤ b ∧ ¬b ≤ a`. -/ |
| 74 | + lawfulOrderLT : |
| 75 | + let := le; let := lt |
| 76 | + Std.LawfulOrderLT α := by |
| 77 | + extract_lets |
| 78 | + first |
| 79 | + /- Try the case where `LT` is synthesized from `LE` first so the error message points to the |
| 80 | + lack of an instance and not the lack of a definitional equality. -/ |
| 81 | + | exact ⟨fun _ _ ↦ _root_.Iff.rfl⟩ |
| 82 | + | infer_instance |
| 83 | + /-- ≤ forms a preorder. -/ |
| 84 | + isPreorder : |
| 85 | + let := le |
| 86 | + Std.IsPreorder α := by |
| 87 | + extract_lets |
| 88 | + first |
| 89 | + | infer_instance |
| 90 | + | exact _root_.Std.IsLinearPreorder.of_ord.toIsPreorder |
| 91 | + | fail "failed to infer `Std.IsPreorder` instance; \ |
| 92 | + make sure you have an `Std.IsPreorder` instance \ |
| 93 | + or `Std.LawfulOrderOrd` and `Std.TransOrd` instances" |
| 94 | + |
| 95 | +/-- Create a `Preorder` from a type satisfying `Std.IsPreorder`. |
| 96 | +
|
| 97 | +If an `LE` instance exists, either an `Std.IsPreorder` instance must exist, or there must be an |
| 98 | +`Ord` instance together with `Std.LawfulOrderOrd` and `Std.TransOrd` instances. |
| 99 | +
|
| 100 | +If no `LE` instance exists, it can be generated from `Ord` and `Std.TransOrd` instances. |
| 101 | +
|
| 102 | +If an `LT` instance exists, an `Std.LawfulOrderLT` instance must exist also; otherwise, a suitable |
| 103 | +`LT` instance will be generated. -/ |
| 104 | +@[expose, implicit_reducible] |
| 105 | +def Preorder.ofStd (α : Type*) (args : OfStdArgs α := by exact {}) : Preorder α where |
| 106 | + toLE := args.le |
| 107 | + toLT := args.lt |
| 108 | + le_refl := args.isPreorder.le_refl |
| 109 | + le_trans := args.isPreorder.le_trans |
| 110 | + lt_iff_le_not_ge := args.lawfulOrderLT.lt_iff |
| 111 | + |
| 112 | +/-- Arguments for `PartialOrder.ofStd`; see that function for details. -/ |
| 113 | +structure PartialOrder.OfStdArgs (α : Type*) extends toPreorderArgs : Preorder.OfStdArgs α where |
| 114 | + /-- ≤ forms a partial order. -/ |
| 115 | + isPartialOrder : |
| 116 | + let := le |
| 117 | + Std.IsPartialOrder α := by |
| 118 | + extract_lets |
| 119 | + first |
| 120 | + | infer_instance |
| 121 | + | exact _root_.Std.IsLinearOrder.of_ord.toIsPartialOrder |
| 122 | + | fail "failed to infer `Std.IsPartialOrder` instance; \ |
| 123 | + make sure you have an `Std.IsPartialOrder` instance \ |
| 124 | + or `LawfulOrderOrd`, `LawfulEqOrd` and `TransOrd` instances" |
| 125 | + |
| 126 | +/-- Create a `PartialOrder` from a type satisfying `Std.IsPartialOrder`. |
| 127 | +
|
| 128 | +If an `LE` instance exists, either an `Std.IsPartialOrder` instance must exist, or there must be an |
| 129 | +`Ord` instance together with `Std.LawfulOrderOrd`, `Std.LawfulEqOrd`, and `Std.TransOrd` instances. |
| 130 | +
|
| 131 | +If no `LE` instance exists, it can be generated from `Ord`, `Std.LawfulEqOrd`, and `Std.TransOrd` |
| 132 | +instances. |
| 133 | +
|
| 134 | +If an `LT` instance exists, an `Std.LawfulOrderLT` instance must exist also; otherwise, a suitable |
| 135 | +`LT` instance will be generated. -/ |
| 136 | +@[expose, implicit_reducible] |
| 137 | +def PartialOrder.ofStd (α : Type*) (args : OfStdArgs α := by exact {}) : PartialOrder α where |
| 138 | + toPreorder := .ofStd α args.toPreorderArgs |
| 139 | + le_antisymm := args.isPartialOrder.le_antisymm |
| 140 | + |
| 141 | +/- Although Batteries provides that `compareOfLessAndEq` satisfies `LawfulLECmp`, there is |
| 142 | +unfortunately no link between that and `LawfulOrderCmp` even though they are essentially the same |
| 143 | +thing. -/ |
| 144 | +theorem Std.LawfulOrderCmp.compareOfLessAndEq (α : Type*) |
| 145 | + [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [DecidableEq α] [DecidableLT α] : |
| 146 | + LawfulOrderCmp (fun a b : α ↦ compareOfLessAndEq a b) := |
| 147 | + let : Ord α := ⟨fun a b : α ↦ _root_.compareOfLessAndEq a b⟩ |
| 148 | + { isLE_compare _ _ := |
| 149 | + have : DecidableLE α := fun _ _ ↦ Classical.propDecidable _ |
| 150 | + isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ ↦ Std.le_total) |
| 151 | + isGE_compare _ _ := |
| 152 | + have : DecidableLE α := fun _ _ ↦ Classical.propDecidable _ |
| 153 | + isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ ↦ Std.le_total) } |
| 154 | + |
| 155 | +/-- Arguments for `LinearOrder.ofStd`; see that function for details. -/ |
| 156 | +structure LinearOrder.OfStdArgs (α : Type*) extends |
| 157 | + toPartialOrderArgs : PartialOrder.OfStdArgs α where |
| 158 | + /-- ≤ forms a linear order. -/ |
| 159 | + isLinearOrder : |
| 160 | + let := le |
| 161 | + Std.IsLinearOrder α := by |
| 162 | + extract_lets |
| 163 | + first |
| 164 | + | infer_instance |
| 165 | + | exact _root_.Std.IsLinearOrder.of_ord |
| 166 | + | fail "failed to infer `Std.IsLinearOrder` instance; \ |
| 167 | + make sure you have an `Std.IsLinearOrder` instance \ |
| 168 | + or `LawfulOrderOrd`, `LawfulEqOrd` and `TransOrd` instances" |
| 169 | + /-- ≤ is decidable. -/ |
| 170 | + decidableLE : DecidableLE α := by |
| 171 | + first |
| 172 | + | infer_instance |
| 173 | + | exact _root_.DecidableLE.ofOrd _ |
| 174 | + | fail "failed to infer `DecidableLE` instance; \ |
| 175 | + make sure you have a `DecidableLE` instance \ |
| 176 | + or a `LawfulOrderOrd` instance" |
| 177 | + /-- = is decidable. This can always be automatically derived from `decidableLE`. -/ |
| 178 | + decidableEq : |
| 179 | + let := toPartialOrderArgs; let := decidableLE |
| 180 | + DecidableEq α := by |
| 181 | + extract_lets _ toPartialOrderArgs |
| 182 | + first |
| 183 | + | infer_instance |
| 184 | + | exact @_root_.decidableEqOfDecidableLE _ (.ofStd _ toPartialOrderArgs) _ |
| 185 | + /-- < is decidable. This can always be automatically derived from `decidableLE`. -/ |
| 186 | + decidableLT : |
| 187 | + let := toPreorderArgs; let := decidableLE |
| 188 | + DecidableLT α := by |
| 189 | + extract_lets _ toPreorderArgs |
| 190 | + first |
| 191 | + | infer_instance |
| 192 | + | exact @_root_.decidableLTOfDecidableLE _ (.ofStd _ toPreorderArgs) _ |
| 193 | + /-- The `Min` instance of the order. This can always be automatically derived. -/ |
| 194 | + min : |
| 195 | + let := le; let := decidableLE |
| 196 | + Min α := by |
| 197 | + extract_lets |
| 198 | + first |
| 199 | + | infer_instance |
| 200 | + | exact _root_.Min.leftLeaningOfLE _ |
| 201 | + /-- The `Max` instance of the order. This can always be automatically derived. -/ |
| 202 | + max : |
| 203 | + let := le; let := decidableLE |
| 204 | + Max α := by |
| 205 | + extract_lets |
| 206 | + first |
| 207 | + | infer_instance |
| 208 | + | exact _root_.Max.leftLeaningOfLE _ |
| 209 | + /-- `min a b` is equivalent to `if a ≤ b then a else b`. -/ |
| 210 | + lawfulOrderLeftLeaningMin : Std.LawfulOrderLeftLeaningMin α := by infer_instance |
| 211 | + /-- `max a b` is equivalent to `if b ≤ a then a else b`. -/ |
| 212 | + lawfulOrderLeftLeaningMax : Std.LawfulOrderLeftLeaningMax α := by infer_instance |
| 213 | + /-- The `Ord` instance of the order. This can always be automatically derived. -/ |
| 214 | + ord : |
| 215 | + let := lt; let := decidableEq; let := decidableLT |
| 216 | + Ord α := by |
| 217 | + extract_lets |
| 218 | + first |
| 219 | + | infer_instance |
| 220 | + | exact ⟨fun a b ↦ _root_.compareOfLessAndEq a b⟩ |
| 221 | + /-- `Ord` is compatible with ≤. -/ |
| 222 | + lawfulOrderOrd : |
| 223 | + let := le; let := lt; let := lawfulOrderLT; let := isLinearOrder |
| 224 | + let := decidableEq; let := decidableLT |
| 225 | + Std.LawfulOrderOrd α := by |
| 226 | + extract_lets |
| 227 | + first |
| 228 | + /- Try the case where `Ord` is synthesized from `compareOfLessAndEq` first so the error message |
| 229 | + points to the lack of an instance and not the lack of a definitional equality. -/ |
| 230 | + | exact _root_.Std.LawfulOrderCmp.compareOfLessAndEq _ |
| 231 | + | infer_instance |
| 232 | + |
| 233 | +/-- Create a `LinearOrder` from a type satisfying `Std.IsLinearOrder`. |
| 234 | +
|
| 235 | +If an `LE` instance exists, either an `Std.IsLinearOrder` instance must exist, or there must be an |
| 236 | +`Ord` instance together with `Std.LawfulOrderOrd`, `Std.LawfulEqOrd`, and `Std.TransOrd` instances. |
| 237 | +
|
| 238 | +If no `LE` instance exists, it can be generated from `Ord`, `Std.LawfulEqOrd`, and `Std.TransOrd` |
| 239 | +instances. |
| 240 | +
|
| 241 | +If an `LT` instance exists, an `Std.LawfulOrderLT` instance must exist also; otherwise, a suitable |
| 242 | +`LT` instance will be generated. |
| 243 | +
|
| 244 | +If a `DecidableLE` instance exists, it will be used. Otherwise, it can be generated from an `Ord` |
| 245 | +instance. |
| 246 | +
|
| 247 | +If `DecidableEq` and `DecidableLT` instances exist, they will be used. Otherwise, they will be |
| 248 | +generated from the `DecidableLE` instance. |
| 249 | +
|
| 250 | +If `Min` and `Max` instances exist, they will be used, in which case the user must provide |
| 251 | +`Std.LawfulOrderLeftLeaningMin` or `Std.LawfulOrderLeftLeaningMax` respectively. Otherwise, they |
| 252 | +will be generated. |
| 253 | +
|
| 254 | +If an `Ord` instance exists, it will be used, in which case the user must provide an |
| 255 | +`Std.LawfulOrderOrd` instance. Otherwise, it will be generated. -/ |
| 256 | +@[expose, implicit_reducible] |
| 257 | +def LinearOrder.ofStd (α : Type*) (args : OfStdArgs α := by exact {}) : LinearOrder α := |
| 258 | + let := args.le |
| 259 | + let := args.lt |
| 260 | + have := args.lawfulOrderLT |
| 261 | + have := args.isLinearOrder |
| 262 | + let := args.decidableLE |
| 263 | + have := args.lawfulOrderLeftLeaningMin |
| 264 | + have := args.lawfulOrderLeftLeaningMax |
| 265 | + { toPartialOrder := .ofStd _ args.toPartialOrderArgs |
| 266 | + le_total := args.isLinearOrder.le_total |
| 267 | + toDecidableLE := args.decidableLE |
| 268 | + toDecidableEq := args.decidableEq |
| 269 | + toDecidableLT := args.decidableLT |
| 270 | + toMin := args.min |
| 271 | + toMax := args.max |
| 272 | + min_def _ _ := Std.min_eq_if |
| 273 | + max_def a b := by |
| 274 | + rw [Std.max_eq_if] |
| 275 | + split |
| 276 | + · split |
| 277 | + · exact Std.le_antisymm ‹_› ‹_› |
| 278 | + · rfl |
| 279 | + case _ h => rw [if_pos (Std.le_of_lt (Std.not_le.mp h))] |
| 280 | + toOrd := args.ord |
| 281 | + compare_eq_compareOfLessAndEq a b := by |
| 282 | + let := args.ord |
| 283 | + have := args.lawfulOrderOrd |
| 284 | + rw [compareOfLessAndEq] |
| 285 | + split_ifs |
| 286 | + case _ => rwa [Std.compare_eq_lt] |
| 287 | + case _ => rwa [Std.compare_eq_iff_eq] |
| 288 | + case _ h h' => |
| 289 | + exact Std.compare_eq_gt.mpr <| Std.lt_of_le_of_ne (Std.not_lt.mp h) (Ne.symm h') } |
0 commit comments