From d96b7a7d98a3bd7468302cfbd438629c09e50efe Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 29 Sep 2024 16:23:24 +1000 Subject: [PATCH] chore: rename List.maximum? to max? (#5518) More consistent with other API. --- src/Init/Data/List/Basic.lean | 26 ++--- src/Init/Data/List/Impl.lean | 2 +- src/Init/Data/List/Lemmas.lean | 2 +- src/Init/Data/List/MinMax.lean | 113 +++++++++++++--------- src/Init/Data/List/Nat/Basic.lean | 75 +++++++------- src/Lean/Elab/Tactic/Omega/MinNatAbs.lean | 24 ++--- src/Lean/Server/InfoUtils.lean | 4 +- src/Std/Sat/CNF/RelabelFin.lean | 14 +-- tests/lean/run/list_simp.lean | 16 +-- 9 files changed, 153 insertions(+), 123 deletions(-) diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 07b598891829..7bd1a9d4eabf 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -43,7 +43,7 @@ The operations are organized as follow: * Logic: `any`, `all`, `or`, and `and`. * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`. * Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`. -* Minima and maxima: `minimum?` and `maximum?`. +* Minima and maxima: `min?` and `max?`. * Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`, `removeAll` (currently these functions are mostly only used in meta code, @@ -1464,30 +1464,34 @@ def enum : List α → List (Nat × α) := enumFrom 0 /-! ## Minima and maxima -/ -/-! ### minimum? -/ +/-! ### min? -/ /-- Returns the smallest element of the list, if it is not empty. -* `[].minimum? = none` -* `[4].minimum? = some 4` -* `[1, 4, 2, 10, 6].minimum? = some 1` +* `[].min? = none` +* `[4].min? = some 4` +* `[1, 4, 2, 10, 6].min? = some 1` -/ -def minimum? [Min α] : List α → Option α +def min? [Min α] : List α → Option α | [] => none | a::as => some <| as.foldl min a -/-! ### maximum? -/ +@[inherit_doc min?, deprecated min? (since := "2024-09-29")] abbrev minimum? := @min? + +/-! ### max? -/ /-- Returns the largest element of the list, if it is not empty. -* `[].maximum? = none` -* `[4].maximum? = some 4` -* `[1, 4, 2, 10, 6].maximum? = some 10` +* `[].max? = none` +* `[4].max? = some 4` +* `[1, 4, 2, 10, 6].max? = some 10` -/ -def maximum? [Max α] : List α → Option α +def max? [Max α] : List α → Option α | [] => none | a::as => some <| as.foldl max a +@[inherit_doc max?, deprecated max? (since := "2024-09-29")] abbrev maximum? := @max? + /-! ## Other list operations The functions are currently mostly used in meta code, diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index c07ac71c8cec..79dca13384ea 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -31,7 +31,7 @@ The following operations are still missing `@[csimp]` replacements: The following operations are not recursive to begin with (or are defined in terms of recursive primitives): `isEmpty`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft`, `rotateRight`, `insert`, `zip`, `enum`, -`minimum?`, `maximum?`, and `removeAll`. +`min?`, `max?`, and `removeAll`. The following operations were already given `@[csimp]` replacements in `Init/Data/List/Basic.lean`: `length`, `map`, `filter`, `replicate`, `leftPad`, `unzip`, `range'`, `iota`, `intersperse`. diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index b746491e18ae..ed6e283b5755 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -55,7 +55,7 @@ See also * `Init.Data.List.Erase` for lemmas about `List.eraseP` and `List.erase`. * `Init.Data.List.Find` for lemmas about `List.find?`, `List.findSome?`, `List.findIdx`, `List.findIdx?`, and `List.indexOf` -* `Init.Data.List.MinMax` for lemmas about `List.minimum?` and `List.maximum?`. +* `Init.Data.List.MinMax` for lemmas about `List.min?` and `List.max?`. * `Init.Data.List.Pairwise` for lemmas about `List.Pairwise` and `List.Nodup`. * `Init.Data.List.Sublist` for lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`. diff --git a/src/Init/Data/List/MinMax.lean b/src/Init/Data/List/MinMax.lean index b7432cb709fc..08c37a1c4fec 100644 --- a/src/Init/Data/List/MinMax.lean +++ b/src/Init/Data/List/MinMax.lean @@ -7,7 +7,7 @@ prelude import Init.Data.List.Lemmas /-! -# Lemmas about `List.minimum?` and `List.maximum?. +# Lemmas about `List.min?` and `List.max?. -/ namespace List @@ -16,24 +16,24 @@ open Nat /-! ## Minima and maxima -/ -/-! ### minimum? -/ +/-! ### min? -/ -@[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl +@[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl --- We don't put `@[simp]` on `minimum?_cons`, +-- We don't put `@[simp]` on `min?_cons`, -- because the definition in terms of `foldl` is not useful for proofs. -theorem minimum?_cons [Min α] {xs : List α} : (x :: xs).minimum? = foldl min x xs := rfl +theorem min?_cons [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl -@[simp] theorem minimum?_eq_none_iff {xs : List α} [Min α] : xs.minimum? = none ↔ xs = [] := by - cases xs <;> simp [minimum?] +@[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = [] := by + cases xs <;> simp [min?] -theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) : - {xs : List α} → xs.minimum? = some a → a ∈ xs := by +theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) : + {xs : List α} → xs.min? = some a → a ∈ xs := by intro xs match xs with | nil => simp | x :: xs => - simp only [minimum?_cons, Option.some.injEq, List.mem_cons] + simp only [min?_cons, Option.some.injEq, List.mem_cons] intro eq induction xs generalizing x with | nil => @@ -49,12 +49,12 @@ theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`. -theorem le_minimum?_iff [Min α] [LE α] +theorem le_min?_iff [Min α] [LE α] (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) : - {xs : List α} → xs.minimum? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b + {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b | nil => by simp | cons x xs => by - rw [minimum?] + rw [min?] intro eq y simp only [Option.some.injEq] at eq induction xs generalizing x with @@ -67,46 +67,46 @@ theorem le_minimum?_iff [Min α] [LE α] -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`, -- and `le_min_iff`. -theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)] +theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)] (le_refl : ∀ a : α, a ≤ a) (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : - xs.minimum? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by - refine ⟨fun h => ⟨minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩ + xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by + refine ⟨fun h => ⟨min?_mem min_eq_or h, (le_min?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩ intro ⟨h₁, h₂⟩ cases xs with | nil => simp at h₁ | cons x xs => exact congrArg some <| anti.1 - ((le_minimum?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁) - (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl)) + ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁) + (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl)) -theorem minimum?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) : - (replicate n a).minimum? = if n = 0 then none else some a := by +theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) : + (replicate n a).min? = if n = 0 then none else some a := by induction n with | zero => rfl - | succ n ih => cases n <;> simp_all [replicate_succ, minimum?_cons] + | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons] -@[simp] theorem minimum?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) : - (replicate n a).minimum? = some a := by - simp [minimum?_replicate, Nat.ne_of_gt h, w] +@[simp] theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) : + (replicate n a).min? = some a := by + simp [min?_replicate, Nat.ne_of_gt h, w] -/-! ### maximum? -/ +/-! ### max? -/ -@[simp] theorem maximum?_nil [Max α] : ([] : List α).maximum? = none := rfl +@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl --- We don't put `@[simp]` on `maximum?_cons`, +-- We don't put `@[simp]` on `max?_cons`, -- because the definition in terms of `foldl` is not useful for proofs. -theorem maximum?_cons [Max α] {xs : List α} : (x :: xs).maximum? = foldl max x xs := rfl +theorem max?_cons [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl -@[simp] theorem maximum?_eq_none_iff {xs : List α} [Max α] : xs.maximum? = none ↔ xs = [] := by - cases xs <;> simp [maximum?] +@[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = [] := by + cases xs <;> simp [max?] -theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) : - {xs : List α} → xs.maximum? = some a → a ∈ xs +theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) : + {xs : List α} → xs.max? = some a → a ∈ xs | nil => by simp | cons x xs => by - rw [maximum?]; rintro ⟨⟩ + rw [max?]; rintro ⟨⟩ induction xs generalizing x with simp at * | cons y xs ih => rcases ih (max x y) with h | h <;> simp [h] @@ -114,40 +114,57 @@ theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`. -theorem maximum?_le_iff [Max α] [LE α] +theorem max?_le_iff [Max α] [LE α] (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) : - {xs : List α} → xs.maximum? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x + {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x | nil => by simp | cons x xs => by - rw [maximum?]; rintro ⟨⟩ y + rw [max?]; rintro ⟨⟩ y induction xs generalizing x with | nil => simp | cons y xs ih => simp [ih, max_le_iff, and_assoc] -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`, -- and `le_min_iff`. -theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)] +theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)] (le_refl : ∀ a : α, a ≤ a) (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} : - xs.maximum? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by - refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩ + xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by + refine ⟨fun h => ⟨max?_mem max_eq_or h, (max?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩ intro ⟨h₁, h₂⟩ cases xs with | nil => simp at h₁ | cons x xs => exact congrArg some <| anti.1 - (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl)) - ((maximum?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁) + (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl)) + ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁) -theorem maximum?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) : - (replicate n a).maximum? = if n = 0 then none else some a := by +theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) : + (replicate n a).max? = if n = 0 then none else some a := by induction n with | zero => rfl - | succ n ih => cases n <;> simp_all [replicate_succ, maximum?_cons] - -@[simp] theorem maximum?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) : - (replicate n a).maximum? = some a := by - simp [maximum?_replicate, Nat.ne_of_gt h, w] + | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons] + +@[simp] theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) : + (replicate n a).max? = some a := by + simp [max?_replicate, Nat.ne_of_gt h, w] + +@[deprecated min?_nil (since := "2024-09-29")] abbrev minimum?_nil := @min?_nil +@[deprecated min?_cons (since := "2024-09-29")] abbrev minimum?_cons := @min?_cons +@[deprecated min?_eq_none_iff (since := "2024-09-29")] abbrev mininmum?_eq_none_iff := @min?_eq_none_iff +@[deprecated min?_mem (since := "2024-09-29")] abbrev minimum?_mem := @min?_mem +@[deprecated le_min?_iff (since := "2024-09-29")] abbrev le_minimum?_iff := @le_min?_iff +@[deprecated min?_eq_some_iff (since := "2024-09-29")] abbrev minimum?_eq_some_iff := @min?_eq_some_iff +@[deprecated min?_replicate (since := "2024-09-29")] abbrev minimum?_replicate := @min?_replicate +@[deprecated min?_replicate_of_pos (since := "2024-09-29")] abbrev minimum?_replicate_of_pos := @min?_replicate_of_pos +@[deprecated max?_nil (since := "2024-09-29")] abbrev maximum?_nil := @max?_nil +@[deprecated max?_cons (since := "2024-09-29")] abbrev maximum?_cons := @max?_cons +@[deprecated max?_eq_none_iff (since := "2024-09-29")] abbrev maximum?_eq_none_iff := @max?_eq_none_iff +@[deprecated max?_mem (since := "2024-09-29")] abbrev maximum?_mem := @max?_mem +@[deprecated max?_le_iff (since := "2024-09-29")] abbrev maximum?_le_iff := @max?_le_iff +@[deprecated max?_eq_some_iff (since := "2024-09-29")] abbrev maximum?_eq_some_iff := @max?_eq_some_iff +@[deprecated max?_replicate (since := "2024-09-29")] abbrev maximum?_replicate := @max?_replicate +@[deprecated max?_replicate_of_pos (since := "2024-09-29")] abbrev maximum?_replicate_of_pos := @max?_replicate_of_pos end List diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 4abd0d98d379..fa760d499c18 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -86,26 +86,26 @@ theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ obtain ⟨h', -⟩ := getElem?_eq_some_iff.1 h exact ⟨h', h⟩ -/-! ### minimum? -/ +/-! ### min? -/ --- A specialization of `minimum?_eq_some_iff` to Nat. -theorem minimum?_eq_some_iff' {xs : List Nat} : - xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := - minimum?_eq_some_iff +-- A specialization of `min?_eq_some_iff` to Nat. +theorem min?_eq_some_iff' {xs : List Nat} : + xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := + min?_eq_some_iff (le_refl := Nat.le_refl) - (min_eq_or := fun _ _ => by omega) - (le_min_iff := fun _ _ _ => by omega) + (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp) + (le_min_iff := fun _ _ _ => Nat.le_min) -- This could be generalized, -- but will first require further work on order typeclasses in the core repository. -theorem minimum?_cons' {a : Nat} {l : List Nat} : - (a :: l).minimum? = some (match l.minimum? with +theorem min?_cons' {a : Nat} {l : List Nat} : + (a :: l).min? = some (match l.min? with | none => a | some m => min a m) := by - rw [minimum?_eq_some_iff'] + rw [min?_eq_some_iff'] split <;> rename_i h m · simp_all - · rw [minimum?_eq_some_iff'] at m + · rw [min?_eq_some_iff'] at m obtain ⟨m, le⟩ := m rw [Nat.min_def] constructor @@ -122,11 +122,11 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} : theorem foldl_min {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)] {l : List α} {a : α} : - l.foldl (init := a) min = min a (l.minimum?.getD a) := by + l.foldl (init := a) min = min a (l.min?.getD a) := by cases l with | nil => simp [Std.IdempotentOp.idempotent] | cons b l => - simp only [minimum?] + simp only [min?] induction l generalizing a b with | nil => simp | cons c l ih => simp [ih, Std.Associative.assoc] @@ -134,7 +134,7 @@ theorem foldl_min theorem foldl_min_right {α β : Type _} [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)] {l : List α} {b : β} {f : α → β} : - (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by + (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).min?.getD b) := by rw [← foldl_map, foldl_min] theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by @@ -148,12 +148,12 @@ theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) : l.foldl (init := a) min ≤ b := Nat.le_trans (foldl_min_le) h -theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : - l.minimum?.getD k ≤ a := by +theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : + l.min?.getD k ≤ a := by cases l with | nil => simp at h | cons b l => - simp [minimum?_cons] + simp [min?_cons] simp at h rcases h with (rfl | h) · exact foldl_min_le @@ -166,26 +166,26 @@ theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : · exact foldl_min_min_of_le (Nat.min_le_right _ _) · exact ih _ h -/-! ### maximum? -/ +/-! ### max? -/ --- A specialization of `maximum?_eq_some_iff` to Nat. -theorem maximum?_eq_some_iff' {xs : List Nat} : - xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) := - maximum?_eq_some_iff +-- A specialization of `max?_eq_some_iff` to Nat. +theorem max?_eq_some_iff' {xs : List Nat} : + xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) := + max?_eq_some_iff (le_refl := Nat.le_refl) - (max_eq_or := fun _ _ => by omega) - (max_le_iff := fun _ _ _ => by omega) + (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp) + (max_le_iff := fun _ _ _ => Nat.max_le) -- This could be generalized, -- but will first require further work on order typeclasses in the core repository. -theorem maximum?_cons' {a : Nat} {l : List Nat} : - (a :: l).maximum? = some (match l.maximum? with +theorem max?_cons' {a : Nat} {l : List Nat} : + (a :: l).max? = some (match l.max? with | none => a | some m => max a m) := by - rw [maximum?_eq_some_iff'] + rw [max?_eq_some_iff'] split <;> rename_i h m · simp_all - · rw [maximum?_eq_some_iff'] at m + · rw [max?_eq_some_iff'] at m obtain ⟨m, le⟩ := m rw [Nat.max_def] constructor @@ -202,11 +202,11 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} : theorem foldl_max {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)] {l : List α} {a : α} : - l.foldl (init := a) max = max a (l.maximum?.getD a) := by + l.foldl (init := a) max = max a (l.max?.getD a) := by cases l with | nil => simp [Std.IdempotentOp.idempotent] | cons b l => - simp only [maximum?] + simp only [max?] induction l generalizing a b with | nil => simp | cons c l ih => simp [ih, Std.Associative.assoc] @@ -214,7 +214,7 @@ theorem foldl_max theorem foldl_max_right {α β : Type _} [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)] {l : List α} {b : β} {f : α → β} : - (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by + (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).max?.getD b) := by rw [← foldl_map, foldl_max] theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by @@ -228,12 +228,12 @@ theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) : a ≤ l.foldl (init := b) max := Nat.le_trans h (le_foldl_max) -theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : - a ≤ l.maximum?.getD k := by +theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : + a ≤ l.max?.getD k := by cases l with | nil => simp at h | cons b l => - simp [maximum?_cons] + simp [max?_cons] simp at h rcases h with (rfl | h) · exact le_foldl_max @@ -246,4 +246,11 @@ theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : · exact le_foldl_max_of_le (Nat.le_max_right b a) · exact ih _ h +@[deprecated min?_eq_some_iff' (since := "2024-09-29")] abbrev minimum?_eq_some_iff' := @min?_eq_some_iff' +@[deprecated min?_cons' (since := "2024-09-29")] abbrev minimum?_cons' := @min?_cons' +@[deprecated min?_getD_le_of_mem (since := "2024-09-29")] abbrev minimum?_getD_le_of_mem := @min?_getD_le_of_mem +@[deprecated max?_eq_some_iff' (since := "2024-09-29")] abbrev maximum?_eq_some_iff' := @max?_eq_some_iff' +@[deprecated max?_cons' (since := "2024-09-29")] abbrev maximum?_cons' := @max?_cons' +@[deprecated le_max?_getD_of_mem (since := "2024-09-29")] abbrev le_maximum?_getD_of_mem := @le_max?_getD_of_mem + end List diff --git a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean index 1b41587538ec..f55330fe03a8 100644 --- a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean +++ b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean @@ -29,12 +29,14 @@ The minimum non-zero entry in a list of natural numbers, or zero if all entries We completely characterize the function via `nonzeroMinimum_eq_zero_iff` and `nonzeroMinimum_eq_nonzero_iff` below. -/ -def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.minimum? |>.getD 0 +def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.min? |>.getD 0 -- A specialization of `minimum?_eq_some_iff` to Nat. -theorem minimum?_eq_some_iff' {xs : List Nat} : - xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := - minimum?_eq_some_iff +-- This is a duplicate `min?_eq_some_iff'` proved in `Init.Data.List.Nat.Basic`, +-- and could be deduplicated but the import hierarchy is awkward. +theorem min?_eq_some_iff'' {xs : List Nat} : + xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := + min?_eq_some_iff (le_refl := Nat.le_refl) (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp) (le_min_iff := fun _ _ _ => Nat.le_min) @@ -42,27 +44,27 @@ theorem minimum?_eq_some_iff' {xs : List Nat} : open Classical in @[simp] theorem nonzeroMinimum_eq_zero_iff {xs : List Nat} : xs.nonzeroMinimum = 0 ↔ ∀ x ∈ xs, x = 0 := by - simp [nonzeroMinimum, Option.getD_eq_iff, minimum?_eq_none_iff, minimum?_eq_some_iff', + simp [nonzeroMinimum, Option.getD_eq_iff, min?_eq_none_iff, min?_eq_some_iff'', filter_eq_nil_iff, mem_filter] theorem nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum ≠ 0) : xs.nonzeroMinimum ∈ xs := by dsimp [nonzeroMinimum] at * - generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m at * + generalize h : (xs.filter (· ≠ 0) |>.min?) = m at * match m, w with - | some (m+1), _ => simp_all [minimum?_eq_some_iff', mem_filter] + | some (m+1), _ => simp_all [min?_eq_some_iff'', mem_filter] theorem nonzeroMinimum_pos {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : 0 < xs.nonzeroMinimum := Nat.pos_iff_ne_zero.mpr fun w => h (nonzeroMinimum_eq_zero_iff.mp w _ m) theorem nonzeroMinimum_le {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : xs.nonzeroMinimum ≤ a := by - have : (xs.filter (· ≠ 0) |>.minimum?) = some xs.nonzeroMinimum := by + have : (xs.filter (· ≠ 0) |>.min?) = some xs.nonzeroMinimum := by have w := nonzeroMinimum_pos m h dsimp [nonzeroMinimum] at * - generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m? at * + generalize h : (xs.filter (· ≠ 0) |>.min?) = m? at * match m?, w with | some m?, _ => rfl - rw [minimum?_eq_some_iff'] at this + rw [min?_eq_some_iff''] at this apply this.2 simp [List.mem_filter] exact ⟨m, h⟩ @@ -142,4 +144,4 @@ theorem minNatAbs_eq_nonzero_iff (xs : List Int) (w : z ≠ 0) : @[simp] theorem minNatAbs_nil : ([] : List Int).minNatAbs = 0 := rfl /-- The maximum absolute value in a list of integers. -/ -def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.maximum? |>.getD 0 +def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.max? |>.getD 0 diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 361c37d39ca0..8a850b1ac12f 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -237,7 +237,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in let _ := @lexOrd let _ := @leOfOrd.{0} let _ := @maxOfLe - results.map (·.1) |>.maximum? + results.map (·.1) |>.max? let res? := results.find? (·.1 == maxPrio?) |>.map (·.2) if let some i := res? then if let .ofTermInfo ti := i.info then @@ -380,7 +380,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String priority := if hoverPos.byteIdx == tailPos.byteIdx + trailSize then 0 else 1 }] return gs - let maxPrio? := gs.map (·.priority) |>.maximum? + let maxPrio? := gs.map (·.priority) |>.max? gs.filter (some ·.priority == maxPrio?) where hasNestedTactic (pos tailPos) : InfoTree → Bool diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 8c40b7ae1b91..7790e45ba366 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -15,12 +15,12 @@ namespace CNF /-- Obtain the literal with the largest identifier in `c`. -/ -def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.maximum? +def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.max? theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) : ∀ lit, Mem lit c → lit ≤ maxLit := by intro lit hlit - simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp, + simp only [maxLiteral, List.max?_eq_some_iff', List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h simp only [Mem] at hlit rcases h with ⟨_, hbar⟩ @@ -35,25 +35,25 @@ theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) : cases h <;> rename_i h all_goals have h1 := List.ne_nil_of_mem h - have h2 := not_congr <| @List.maximum?_eq_none_iff _ (c.map (·.1)) _ + have h2 := not_congr <| @List.max?_eq_none_iff _ (c.map (·.1)) _ simp [← Option.ne_none_iff_exists', h1, h2, maxLiteral] theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) : ∀ lit, ¬Mem lit c := by intro lit hlit - simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil_iff] at h + simp only [maxLiteral, List.max?_eq_none_iff, List.map_eq_nil_iff] at h simp only [h, not_mem_nil] at hlit /-- Obtain the literal with the largest identifier in `f`. -/ def maxLiteral (f : CNF Nat) : Option Nat := - List.filterMap Clause.maxLiteral f |>.maximum? + List.filterMap Clause.maxLiteral f |>.max? theorem of_maxLiteral_eq_some' (f : CNF Nat) (h : f.maxLiteral = some maxLit) : ∀ clause, clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit := by intro clause hclause1 hclause2 - simp [maxLiteral, List.maximum?_eq_some_iff'] at h + simp [maxLiteral, List.max?_eq_some_iff'] at h rcases h with ⟨_, hclause3⟩ apply hclause3 localMax clause hclause1 hclause2 @@ -70,7 +70,7 @@ theorem of_maxLiteral_eq_some (f : CNF Nat) (h : f.maxLiteral = some maxLit) : theorem of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) : ∀ lit, ¬Mem lit f := by intro lit hlit - simp only [maxLiteral, List.maximum?_eq_none_iff] at h + simp only [maxLiteral, List.max?_eq_none_iff] at h dsimp [Mem] at hlit rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩ have := Clause.of_maxLiteral_eq_none clause (List.forall_none_of_filterMap_eq_nil h clause hclause1) lit diff --git a/tests/lean/run/list_simp.lean b/tests/lean/run/list_simp.lean index e62eb854d155..6fd985face4c 100644 --- a/tests/lean/run/list_simp.lean +++ b/tests/lean/run/list_simp.lean @@ -336,21 +336,21 @@ variable (h : n ≤ m) in -- unzip #check_simp unzip (replicate n (x, y)) ~> (replicate n x, replicate n y) --- minimum? +-- min? -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma -#check_simp (replicate (n+1) 7).minimum? ~> some 7 +#check_simp (replicate (n+1) 7).min? ~> some 7 variable (h : 0 < n) in -#check_tactic (replicate n 7).minimum? ~> some 7 by simp [h] +#check_tactic (replicate n 7).min? ~> some 7 by simp [h] --- maximum? +-- max? -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma -#check_simp (replicate (n+1) 7).maximum? ~> some 7 +#check_simp (replicate (n+1) 7).max? ~> some 7 variable (h : 0 < n) in -#check_tactic (replicate n 7).maximum? ~> some 7 by simp [h] +#check_tactic (replicate n 7).max? ~> some 7 by simp [h] end @@ -456,9 +456,9 @@ end Pairwise /-! ### enumFrom -/ -/-! ### minimum? -/ +/-! ### min? -/ -/-! ### maximum? -/ +/-! ### max? -/ /-! ## Monadic operations -/