feat: Min/Max typeclasses

src/Init/Data/Float.lean

@@ -134,6 +134,10 @@ instance : ReprAtom Float  := ⟨⟩
 
 instance : Pow Float Float := ⟨Float.pow⟩
 
+instance : Min Float := minOfLe
+
+instance : Max Float := maxOfLe
+
 /--
 Efficiently computes `x * 2^i`.
 -/

src/Init/Data/Int/Basic.lean

@@ -171,4 +171,8 @@ instance : LawfulBEq Int where
   eq_of_beq h := by simp [BEq.beq] at h; assumption
   rfl := by simp [BEq.beq]
 
+instance : Min Int := minOfLe
+
+instance : Max Int := maxOfLe
+
 end Int

src/Init/Data/List/Basic.lean

@@ -546,11 +546,11 @@ def dropLast {α} : List α → List α
   | nil => rfl
   | cons a as ih => simp [ih]
 
-def maximum? [LT α] [DecidableRel (@LT.lt α _)] : List α → Option α
+def maximum? [Max α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl max a
 
-def minimum? [LE α] [DecidableRel (@LE.le α _)] : List α → Option α
+def minimum? [Min α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 

src/Init/Data/Nat/Basic.lean

@@ -473,11 +473,18 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
 
 /-! # min/max -/
 
-protected def min (n m : Nat) : Nat :=
-  if n ≤ m then n else m
+instance : Min Nat := minOfLe
+
+protected abbrev min (n m : Nat) := min n m
+
+protected theorem min_def {n m : Nat} : min n m = if n ≤ m then n else m := rfl
+
+instance : Max Nat := maxOfLe
+
+protected abbrev max (n m : Nat) := max n m
+
+protected theorem max_def {n m : Nat} : max n m = if n ≤ m then m else n := rfl
 
-protected def max (n m : Nat) : Nat :=
-  if n ≤ m then m else n
 
 /-! # Auxiliary theorems for well-founded recursion -/
 

src/Init/Data/UInt.lean

@@ -73,6 +73,8 @@ def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
 
 instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
 instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
+instance : Max UInt8 := maxOfLe
+instance : Min UInt8 := minOfLe
 
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
@@ -143,6 +145,8 @@ def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
 
 instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
 instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
+instance : Max UInt16 := maxOfLe
+instance : Min UInt16 := minOfLe
 
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
@@ -277,6 +281,8 @@ def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
 
 instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
 instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
+instance : Max UInt64 := maxOfLe
+instance : Min UInt64 := minOfLe
 
 theorem usize_size_gt_zero : USize.size > 0 :=
   Nat.pos_pow_of_pos System.Platform.numBits (Nat.zero_lt_succ _)
@@ -350,6 +356,8 @@ def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
 
 instance (a b : USize) : Decidable (a < b) := USize.decLt a b
 instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
+instance : Max USize := maxOfLe
+instance : Min USize := minOfLe
 
 theorem USize.modn_lt {m : Nat} : ∀ (u : USize), m > 0 → USize.toNat (u % m) < m
   | ⟨u⟩, h => Fin.modn_lt u h

src/Init/Prelude.lean

@@ -1061,19 +1061,31 @@ class LT (α : Type u) where
 /-- `a > b` is an abbreviation for `b < a`. -/
 @[reducible] def GT.gt {α : Type u} [LT α] (a b : α) : Prop := LT.lt b a
 
-/--
-`max a b` is the maximum of `a` and `b`. It is defined simply as
-`if b < a then a else b`, and works as long as `<` is decidable.
--/
-@[inline] def max [LT α] [DecidableRel (@LT.lt α _)] (a b : α) : α :=
-  ite (LT.lt b a) a b
+/-- `Max α` is the typeclass which supports the operation `max x y` where `x y : α`.-/
+class Max (α : Type u) where
+  /-- The maximum operation: `max x y`. -/
+  max : α → α → α
 
-/--
-`min a b` is the minimum of `a` and `b`. It is defined simply as
-`if a ≤ b then a else b`, and works as long as `≤` is decidable.
--/
-@[inline] def min [LE α] [DecidableRel (@LE.le α _)] (a b : α) : α :=
-  ite (LE.le a b) a b
+export Max (max)
+
+/-- Implementation of the `max` operation using `≤`. -/
+-- Marked inline so that `min x y + max x y` can be optimized to a single branch.
+@[inline]
+def maxOfLe [LE α] [DecidableRel (@LE.le α _)] : Max α where
+  max x y := ite (LE.le x y) y x
+
+/-- `Min α` is the typeclass which supports the operation `min x y` where `x y : α`.-/
+class Min (α : Type u) where
+  /-- The minimum operation: `min x y`. -/
+  min : α → α → α
+
+export Min (min)
+
+/-- Implementation of the `min` operation using `≤`. -/
+-- Marked inline so that `min x y + max x y` can be optimized to a single branch.
+@[inline]
+def minOfLe [LE α] [DecidableRel (@LE.le α _)] : Min α where
+  min x y := ite (LE.le x y) x y
 
 /--
 Transitive chaining of proofs, used e.g. by `calc`.
@@ -1888,6 +1900,8 @@ def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
 
 instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
 instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
+instance : Max UInt32 := maxOfLe
+instance : Min UInt32 := minOfLe
 
 /-- The size of type `UInt64`, that is, `2^64 = 18446744073709551616`. -/
 def UInt64.size : Nat := 18446744073709551616

src/lake

@@ -1 +1 @@
-Subproject commit c4a1e543537d293c35b9a4604f6285ed5fad4bf5
+Subproject commit 7264961e9fe62d217586a24c96c76cc160f008b6

tests/lean/run/1025.lean

@@ -2,6 +2,10 @@ inductive Vector (α : Type u): Nat → Type u where
 | nil : Vector α 0
 | cons (head : α) (tail : Vector α n) : Vector α (n+1)
 
+class Order (α : Type u) extends LE α, LT α, Max α where
+  ltDecidable : DecidableRel (@LT.lt α _)
+  max_def x y : max x y = if x < y then x else y
+
 namespace Vector
   def mem (a : α) : Vector α n → Prop
   | nil => False
@@ -11,10 +15,10 @@ namespace Vector
   | nil     => init
   | cons a l => f a (foldr f init l)
 
-  theorem foldr_max [LE β] [LT β] [DecidableRel (· < · : β → β → Prop)] {v: Vector α n} (f : α → β) (init : β)
+  theorem foldr_max [Order β] {v: Vector α n} (f : α → β) (init : β)
     (h: v.mem y):
     f y ≤ v.foldr (λ x acc => max (f x) acc) init := by
-    induction v <;> simp only[foldr,max]
+    induction v <;> simp only[foldr,Order.max_def]
     · admit
     · split <;> admit
 end Vector

tests/lean/run/909.lean

@@ -7,6 +7,8 @@ instance : LE Date := ⟨InvImage (Nat.le) Date.val⟩
 instance bad (a b : Date) : Decidable (a <= b) :=
   if h0 : (a.val <= b.val) then isTrue h0 else isFalse (fun hf => False.elim (h0 hf))
 
+instance : Min Date := minOfLe
+
 /-
 This implementation also fails:
 instance (a b : Date) : Decidable (a <= b) :=

tests/lean/run/ac_rfl.lean

@@ -8,25 +8,49 @@ instance : IsAssociative (α := Nat) HMul.hMul := ⟨Nat.mul_assoc⟩
 instance : IsCommutative (α := Nat) HMul.hMul := ⟨Nat.mul_comm⟩
 instance : IsNeutral HMul.hMul 1 := ⟨Nat.one_mul, Nat.mul_one⟩
 
-theorem max_assoc (n m k : Nat) : max (max n m) k = max n (max m k) := by
-  simp [max]; split <;> split <;> try split <;> try rfl
-  case inl hmn nhkn hkm => exact False.elim $ nhkn $ Nat.lt_trans hkm hmn
-  . rfl
-  case inl nhmn nhkm hkn => apply absurd hkn; simp [Nat.not_lt_eq] at *; exact Nat.le_trans nhmn nhkm
+@[simp] theorem succ_le_succ_iff {x y : Nat} : x.succ ≤ y.succ ↔ x ≤ y :=
+  ⟨Nat.le_of_succ_le_succ, Nat.succ_le_succ⟩
 
-theorem max_comm (n m : Nat) : max n m = max m n := by
-  simp [max]; split <;> split <;> try rfl
-  case inl h₁ h₂ => apply absurd (Nat.lt_trans h₁ h₂); apply Nat.lt_irrefl
-  case inr h₁ h₂ => simp [Nat.not_lt_eq] at *; apply Nat.le_antisymm <;> assumption
+@[simp] theorem add_le_add_right_iff {x y z : Nat} : x + z ≤ y + z ↔ x ≤ y := by
+  induction z <;> simp_all [Nat.add_succ]
 
-theorem max_idem (n : Nat) : max n n = n := by
-  simp [max]
+set_option linter.unusedVariables false in
+theorem le_ext : ∀ {x y : Nat} (h : ∀ z, z ≤ x ↔ z ≤ y), x = y
+  | 0, 0, _ => rfl
+  | x+1, y+1, h => congrArg (· + 1) <| le_ext fun z => have := h (z + 1); by simp_all
+  | 0, y+1, h => have := h 1; by simp_all
+  | x+1, 0, h => have := h 1; by simp_all
 
-theorem Nat.zero_max (n : Nat) : max 0 n = n := by
-  simp [max]; rfl
+theorem le_or_le : ∀ (a b : Nat), a ≤ b ∨ b ≤ a
+  | x+1, y+1 => by simp [le_or_le x y]
+  | 0, 0 | x+1, 0 | 0, y+1 => by simp
 
-theorem Nat.max_zero (n : Nat) : max n 0 = n := by
-  rw [max_comm, Nat.zero_max]
+theorem le_of_not_le {a b : Nat} (h : ¬ a ≤ b) : b ≤ a :=
+  match le_or_le a b with | .inl ab => (h ab).rec | .inr ba => ba
+
+@[simp] theorem le_max_iff {x y z : Nat} : x ≤ max y z ↔ x ≤ y ∨ x ≤ z := by
+  simp only [Nat.max_def]
+  split
+  · exact Iff.intro .inr fun | .inl xy => Nat.le_trans ‹_› ‹_› | .inr xz => ‹_›
+  · exact Iff.intro .inl fun | .inl xy => ‹_› | .inr xz => Nat.le_trans ‹_› (le_of_not_le ‹_›)
+
+theorem or_assoc : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
+  by_cases p <;> by_cases q <;> by_cases r <;> simp_all
+
+theorem or_comm : p ∨ q ↔ q ∨ p := by
+  by_cases p <;> by_cases q <;> simp_all
+
+theorem max_assoc (n m k : Nat) : max (max n m) k = max n (max m k) :=
+  le_ext (by simp [or_assoc])
+
+theorem max_comm (n m : Nat) : max n m = max m n :=
+  le_ext (by simp [or_comm])
+
+theorem max_idem (n : Nat) : max n n = n := le_ext (by simp)
+
+theorem Nat.zero_max (n : Nat) : max 0 n = n := by simp [Nat.max_def]
+
+theorem Nat.max_zero (n : Nat) : max n 0 = n := by rw [max_comm, Nat.zero_max]
 
 instance : IsAssociative (α := Nat) max := ⟨max_assoc⟩
 instance : IsCommutative (α := Nat) max := ⟨max_comm⟩
@@ -39,11 +63,7 @@ instance : IsIdempotent And := ⟨λ p => propext ⟨λ ⟨hp, _⟩ => hp, λ hp
 instance : IsNeutral And True :=
   ⟨λ p => propext ⟨λ ⟨_, hp⟩ => hp, λ hp => ⟨True.intro, hp⟩⟩, λ p => propext ⟨λ ⟨hp, _⟩ => hp, λ hp => ⟨hp, True.intro⟩⟩⟩
 
-theorem or_assoc (p q r : Prop) : ((p ∨ q) ∨ r) = (p ∨ q ∨ r) :=
-  propext ⟨λ hpqr => hpqr.elim (λ hpq => hpq.elim Or.inl $ λ hq => Or.inr $ Or.inl hq) $ λ hr => Or.inr $ Or.inr hr,
-    λ hpqr => hpqr.elim (λ hp => Or.inl $ Or.inl hp) $ λ hqr => hqr.elim (λ hq => Or.inl $ Or.inr hq) Or.inr⟩
-
-instance : IsAssociative Or := ⟨or_assoc⟩
+instance : IsAssociative Or := ⟨by simp [or_assoc]⟩
 instance : IsCommutative Or := ⟨λ p q => propext ⟨λ hpq => hpq.elim Or.inr Or.inl, λ hqp => hqp.elim Or.inr Or.inl⟩⟩
 instance : IsIdempotent Or := ⟨λ p => propext ⟨λ hp => hp.elim id id, Or.inl⟩⟩
 instance : IsNeutral Or False :=