From fc304d95c06cb4668a5c2ecbbe3cb05fcc5e6fd8 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 21 Oct 2022 12:17:59 -0700 Subject: [PATCH] feat: Min/Max typeclasses --- src/Init/Data/Float.lean | 4 +++ src/Init/Data/Int/Basic.lean | 4 +++ src/Init/Data/List/Basic.lean | 4 +-- src/Init/Data/Nat/Basic.lean | 15 ++++++--- src/Init/Data/UInt.lean | 8 +++++ src/Init/Prelude.lean | 38 +++++++++++++++------- src/lake | 2 +- tests/lean/run/1025.lean | 8 +++-- tests/lean/run/909.lean | 2 ++ tests/lean/run/ac_rfl.lean | 60 +++++++++++++++++++++++------------ 10 files changed, 104 insertions(+), 41 deletions(-) diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index ee44c8ec53..d45a565bb6 100644 --- a/src/Init/Data/Float.lean +++ b/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`. -/ diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 0a12ff799e..c5e16e8122 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/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 diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 6af96a1e5b..100c545be0 100644 --- a/src/Init/Data/List/Basic.lean +++ b/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 diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index ac5ff5584e..cb71e54e96 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/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 -/ diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean index 232f291f77..be66dede76 100644 --- a/src/Init/Data/UInt.lean +++ b/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 diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 9f73068659..32d3b709bb 100644 --- a/src/Init/Prelude.lean +++ b/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 diff --git a/src/lake b/src/lake index c4a1e54353..7264961e9f 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit c4a1e543537d293c35b9a4604f6285ed5fad4bf5 +Subproject commit 7264961e9fe62d217586a24c96c76cc160f008b6 diff --git a/tests/lean/run/1025.lean b/tests/lean/run/1025.lean index 238cdce884..74d5023bce 100644 --- a/tests/lean/run/1025.lean +++ b/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 diff --git a/tests/lean/run/909.lean b/tests/lean/run/909.lean index 64c4220de2..f2955ed52c 100644 --- a/tests/lean/run/909.lean +++ b/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) := diff --git a/tests/lean/run/ac_rfl.lean b/tests/lean/run/ac_rfl.lean index 6e57a5e9cd..86dc762d30 100644 --- a/tests/lean/run/ac_rfl.lean +++ 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 :=