From dfbe9387054e2972449de7bf346059d3609529fa Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Fri, 29 Nov 2024 02:12:39 -0500 Subject: [PATCH 1/8] fix: dependency syntax for a reservoir+git lakefile.toml (#1067) --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index e20b87c09f..36d46eee4d 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ Or add the following to your `lakefile.toml`: [[require]] name = "batteries" scope = "leanprover-community" -version = "main" +rev = "main" ``` Additionally, please make sure that you're using the version of Lean that the current version of `batteries` expects. The easiest way to do this is to copy the [`lean-toolchain`](./lean-toolchain) file from this repository to your project. Once you've added the dependency declaration, the command `lake update` checks out the current version of `batteries` and writes it the Lake manifest file. Don't run this command again unless you're prepared to potentially also update your Lean compiler version, as it will retrieve the latest version of dependencies and add them to the manifest. From 5de63200cb5bb3460e09225874a6e2fe6ca9da5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Fri, 29 Nov 2024 08:31:03 -0500 Subject: [PATCH 2/8] chore: bump toolchain to v4.14.0-rc3 (#1068) --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 0bef727630..6d9e70f733 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc1 +leanprover/lean4:v4.14.0-rc3 From f46c0445cc86ad2bc973edf8c5b2bd88bd91913b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Fri, 29 Nov 2024 09:41:07 -0500 Subject: [PATCH 3/8] chore: update docs-release action (#1069) --- .github/workflows/docs-release.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/docs-release.yml b/.github/workflows/docs-release.yml index 2926a31340..2c8a5c57f6 100644 --- a/.github/workflows/docs-release.yml +++ b/.github/workflows/docs-release.yml @@ -40,6 +40,8 @@ jobs: - name: Release Docs uses: softprops/action-gh-release@v2 with: + prerelease: ${{ contains(github.ref, 'rc') }} + make_latest: ${{ !contains(github.ref, 'rc') }} files: | docs/docs-${{ github.ref_name }}.tar.gz docs/docs-${{ github.ref_name }}.zip From 8d6c853f11a5172efa0e96b9f2be1a83d861cdd9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 11:10:16 +1100 Subject: [PATCH 4/8] chore: bump toolchain to v4.14.0 (#1070) --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 6d9e70f733..1e70935f69 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc3 +leanprover/lean4:v4.14.0 From 7805acf1864ba1a2e359f86a8f092ccf1438ad83 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 13:52:46 +1100 Subject: [PATCH 5/8] chore: move to v4.15.0-rc1, and merge bump/v4.15.0 branch (#1073) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: Mario Carneiro Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Joachim Breitner Co-authored-by: Kyle Miller Co-authored-by: Matthew Ballard Co-authored-by: Henrik Böving --- Batteries.lean | 1 - Batteries/Classes/SatisfiesM.lean | 6 - Batteries/Data/Array/Basic.lean | 49 +---- Batteries/Data/Array/Lemmas.lean | 308 ++++++++++++--------------- Batteries/Data/Array/Merge.lean | 2 +- Batteries/Data/Array/Monadic.lean | 2 +- Batteries/Data/Array/OfFn.lean | 4 - Batteries/Data/Array/Pairwise.lean | 2 +- Batteries/Data/BinaryHeap.lean | 12 +- Batteries/Data/ByteArray.lean | 8 +- Batteries/Data/Fin/Basic.lean | 54 ----- Batteries/Data/Fin/Lemmas.lean | 136 ------------ Batteries/Data/HashMap/Basic.lean | 7 +- Batteries/Data/List/Basic.lean | 37 +--- Batteries/Data/List/FinRange.lean | 34 --- Batteries/Data/List/Lemmas.lean | 20 -- Batteries/Data/List/OfFn.lean | 34 --- Batteries/Data/MLList/Basic.lean | 2 +- Batteries/Data/String/Lemmas.lean | 2 +- Batteries/Data/UInt.lean | 90 -------- Batteries/Data/UnionFind/Basic.lean | 130 ++++++----- Batteries/Data/UnionFind/Lemmas.lean | 2 +- Batteries/Data/Vector/Basic.lean | 278 +----------------------- Batteries/Data/Vector/Lemmas.lean | 105 ++++----- Batteries/Lean/Meta/Simp.lean | 8 +- Batteries/Lean/NameMap.lean | 40 ---- Batteries/Tactic/Instances.lean | 2 +- Batteries/Tactic/Lint/Frontend.lean | 7 +- Batteries/Tactic/Lint/Simp.lean | 6 +- Batteries/Tactic/Trans.lean | 9 +- Batteries/Util/Cache.lean | 5 +- BatteriesTest/alias.lean | 16 +- BatteriesTest/array.lean | 8 +- BatteriesTest/help_cmd.lean | 7 +- BatteriesTest/lint_simpNF.lean | 13 ++ BatteriesTest/show_term.lean | 2 +- lean-toolchain | 2 +- 37 files changed, 321 insertions(+), 1129 deletions(-) delete mode 100644 Batteries/Lean/NameMap.lean diff --git a/Batteries.lean b/Batteries.lean index b645334bf4..6c24d239bc 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -55,7 +55,6 @@ import Batteries.Lean.Meta.SavedState import Batteries.Lean.Meta.Simp import Batteries.Lean.Meta.UnusedNames import Batteries.Lean.MonadBacktrack -import Batteries.Lean.NameMap import Batteries.Lean.NameMapAttribute import Batteries.Lean.PersistentHashMap import Batteries.Lean.PersistentHashSet diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean index 9b34cf475b..a89dad3dfd 100644 --- a/Batteries/Classes/SatisfiesM.lean +++ b/Batteries/Classes/SatisfiesM.lean @@ -248,9 +248,6 @@ instance : MonadSatisfying (Except ε) where | .error e => .error e val_eq {α p x?} h := by cases x? <;> simp --- This will be redundant after nightly-2024-11-08. -attribute [ext] ReaderT.ext - instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where satisfying {α p x} h := have h' := SatisfiesM_ReaderT_eq.mp h @@ -264,9 +261,6 @@ instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) := inferInstanceAs <| MonadSatisfying (ReaderT _ _) --- This will be redundant after nightly-2024-11-08. -attribute [ext] StateT.ext - instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m) where satisfying {α p x} h := have h' := SatisfiesM_StateT_eq.mp h diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean index 3f05693926..9164b1219e 100644 --- a/Batteries/Data/Array/Basic.lean +++ b/Batteries/Data/Array/Basic.lean @@ -46,7 +46,7 @@ considered. protected def minD [ord : Ord α] (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α := if h: start < xs.size ∧ start < stop then - xs.minWith (xs.get ⟨start, h.left⟩) (start + 1) stop + xs.minWith xs[start] (start + 1) stop else d @@ -60,7 +60,7 @@ considered. protected def min? [ord : Ord α] (xs : Array α) (start := 0) (stop := xs.size) : Option α := if h : start < xs.size ∧ start < stop then - some $ xs.minD (xs.get ⟨start, h.left⟩) start stop + some $ xs.minD xs[start] start stop else none @@ -135,48 +135,13 @@ A proof by `get_elem_tactic` is provided as a default argument for `h`. This will perform the update destructively provided that `a` has a reference count of 1 when called. -/ abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α := - a.set ⟨i, h⟩ x + a.set i x -/-- -`swapN a i j hi hj` swaps two `Nat` indexed entries in an `Array α`. -Uses `get_elem_tactic` to supply a proof that the indices are in range. -`hi` and `hj` are both given a default argument `by get_elem_tactic`. -This will perform the update destructively provided that `a` has a reference count of 1 when called. --/ -abbrev swapN (a : Array α) (i j : Nat) - (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α := - Array.swap a ⟨i,hi⟩ ⟨j, hj⟩ - -/-- -`swapAtN a i h x` swaps the entry with index `i : Nat` in the vector for a new entry `x`. -The old entry is returned alongwith the modified vector. -Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible. --/ -abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : - α × Array α := swapAt a ⟨i,h⟩ x +@[deprecated (since := "2024-11-24")] alias swapN := swap -/-- -`eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`. -`h : i < a.size` has a default argument `by get_elem_tactic` which tries to supply a proof -that the index is valid. -This function takes worst case O(n) time because it has to backshift all elements at positions -greater than i. --/ -abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α := - a.feraseIdx ⟨i, h⟩ - -/-- -Remove the element at a given index from an array, panics if index is out of bounds. --/ -def eraseIdx! (a : Array α) (i : Nat) : Array α := - if h : i < a.size then - a.feraseIdx ⟨i, h⟩ - else - have : Inhabited (Array α) := ⟨a⟩ - panic! s!"index {i} out of bounds" +@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt -/-- `finRange n` is the array of all elements of `Fin n` in order. -/ -protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i +@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx end Array @@ -204,7 +169,7 @@ subarray, or `none` if the subarray is empty. def popHead? (as : Subarray α) : Option (α × Subarray α) := if h : as.start < as.stop then - let head := as.array.get ⟨as.start, Nat.lt_of_lt_of_le h as.stop_le_array_size⟩ + let head := as.array[as.start]'(Nat.lt_of_lt_of_le h as.stop_le_array_size) let tail := { as with start := as.start + 1 diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean index 7022ef1cc2..9bfa7c43d0 100644 --- a/Batteries/Data/Array/Lemmas.lean +++ b/Batteries/Data/Array/Lemmas.lean @@ -23,65 +23,9 @@ theorem forIn_eq_forIn_toList [Monad m] /-! ### zipWith / zip -/ -theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) : - (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by - let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size → - (zipWithAux f as bs i cs).toList = - cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by - intro i cs hia hib - unfold zipWithAux - by_cases h : i = as.size ∨ i = bs.size - case pos => - have : ¬(i < as.size) ∨ ¬(i < bs.size) := by - cases h <;> simp_all only [Nat.not_lt, Nat.le_refl, true_or, or_true] - -- Cleaned up aesop output below - simp_all only [Nat.not_lt] - cases h <;> [(cases this); (cases this)] - · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length, - List.zipWith_nil_left, List.append_nil] - · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length, - List.zipWith_nil_left, List.append_nil] - · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length, - List.zipWith_nil_right, List.append_nil] - split <;> simp_all only [Nat.not_lt] - · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length, - List.zipWith_nil_right, List.append_nil] - split <;> simp_all only [Nat.not_lt] - case neg => - rw [not_or] at h - have has : i < as.size := Nat.lt_of_le_of_ne hia h.1 - have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2 - simp only [has, hbs, dite_true] - rw [loop (i+1) _ has hbs, Array.push_toList] - have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl - let i_as : Fin as.toList.length := ⟨i, has⟩ - let i_bs : Fin bs.toList.length := ⟨i, hbs⟩ - rw [h₁, List.append_assoc] - congr - rw [← List.zipWith_append (h := by simp), getElem_eq_getElem_toList, - getElem_eq_getElem_toList] - show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList) - ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) = - List.zipWith f (List.drop i as.toList) (List.drop i bs.toList) - simp only [length_toList, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem] - simp [zipWith, loop 0 #[] (by simp) (by simp)] @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith -@[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : - (as.zipWith bs f).size = min as.size bs.size := by - rw [size_eq_length_toList, toList_zipWith, List.length_zipWith] - -theorem toList_zip (as : Array α) (bs : Array β) : - (as.zip bs).toList = as.toList.zip bs.toList := - toList_zipWith Prod.mk as bs -@[deprecated (since := "2024-09-09")] alias data_zip := toList_zip -@[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip - -@[simp] theorem size_zip (as : Array α) (bs : Array β) : - (as.zip bs).size = min as.size bs.size := - as.size_zipWith bs Prod.mk - /-! ### filter -/ theorem size_filter_le (p : α → Bool) (l : Array α) : @@ -120,12 +64,9 @@ where @[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} : (l.erase a).toList = l.toList.erase a -@[simp] theorem eraseIdx!_eq_eraseIdx (a : Array α) (i : Nat) : - a.eraseIdx! i = a.eraseIdx i := rfl - -@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) : - (a.eraseIdx i).size = if i < a.size then a.size-1 else a.size := by - simp only [eraseIdx]; split; simp; rfl +@[simp] theorem size_eraseIdxIfInBounds (a : Array α) (i : Nat) : + (a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size := by + simp only [eraseIdxIfInBounds]; split; simp; rfl /-! ### set -/ @@ -133,128 +74,143 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp /-! ### map -/ -theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by - rw [mapM, mapM.map]; rfl - -theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f - /-! ### mem -/ theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp -/-! ### append -/ - -alias append_empty := append_nil - -alias empty_append := nil_append - /-! ### insertAt -/ -private theorem size_insertAt_loop (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) : - (insertAt.loop as i bs j).size = bs.size := by - unfold insertAt.loop +@[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) : + (insertIdx.loop i as j).size = as.size := by + unfold insertIdx.loop split - · rw [size_insertAt_loop, size_swap] + · rw [size_insertIdx_loop, size_swap] · rfl -@[simp] theorem size_insertAt (as : Array α) (i : Fin (as.size+1)) (v : α) : - (as.insertAt i v).size = as.size + 1 := by - rw [insertAt, size_insertAt_loop, size_push] - -private theorem get_insertAt_loop_lt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) - (k) (hk : k < (insertAt.loop as i bs j).size) (h : k < i) : - (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by - unfold insertAt.loop - split - · have h1 : k ≠ j - 1 := by omega - have h2 : k ≠ j := by omega - rw [get_insertAt_loop_lt, getElem_swap, if_neg h1, if_neg h2] - exact h +@[simp] theorem size_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) : + (as.insertIdx i v).size = as.size + 1 := by + rw [insertIdx, size_insertIdx_loop, size_push] + +@[deprecated size_insertIdx (since := "2024-11-20")] alias size_insertAt := size_insertIdx + +theorem getElem_insertIdx_loop_lt {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h} + (w : k < i) : + (insertIdx.loop i as j)[k] = as[k]'(by simpa using h) := by + unfold insertIdx.loop + split <;> rename_i h₁ + · simp only + rw [getElem_insertIdx_loop_lt w] + rw [getElem_swap] + split <;> rename_i h₂ + · simp_all + omega + · split <;> rename_i h₃ + · omega + · simp_all · rfl -private theorem get_insertAt_loop_gt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) - (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : j < k) : - (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by - unfold insertAt.loop - split - · have h1 : k ≠ j - 1 := by omega - have h2 : k ≠ j := by omega - rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_neg h2] - exact Nat.lt_of_le_of_lt (Nat.pred_le _) hgt - · rfl - -private theorem get_insertAt_loop_eq (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) - (k) (hk : k < (insertAt.loop as i bs j).size) (heq : i = k) (h : i.val ≤ j.val) : - (insertAt.loop as i bs j)[k] = bs[j] := by - unfold insertAt.loop - split - · next h => - rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_swap, if_pos rfl] - exact heq - exact Nat.le_pred_of_lt h - · congr; omega - -private theorem get_insertAt_loop_gt_le (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) - (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : i < k) (hle : k ≤ j) : - (insertAt.loop as i bs j)[k] = bs[k-1] := by - unfold insertAt.loop - split - · next h => - if h0 : k = j then - cases h0 - have h1 : j.val ≠ j - 1 := by omega - rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_pos rfl]; rfl - exact Nat.pred_lt_of_lt hgt - else - have h1 : k - 1 ≠ j - 1 := by omega - have h2 : k - 1 ≠ j := by omega - rw [get_insertAt_loop_gt_le, getElem_swap, if_neg h1, if_neg h2] - apply Nat.le_of_lt_add_one - rw [Nat.sub_one_add_one] - exact Nat.lt_of_le_of_ne hle h0 - exact Nat.not_eq_zero_of_lt h - exact hgt - · next h => - absurd h - exact Nat.lt_of_lt_of_le hgt hle - -theorem getElem_insertAt_lt (as : Array α) (i : Fin (as.size+1)) (v : α) - (k) (hlt : k < i.val) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} : - (as.insertAt i v)[k] = as[k] := by - simp only [insertAt] - rw [get_insertAt_loop_lt, getElem_push, dif_pos hk'] - exact hlt - -theorem getElem_insertAt_gt (as : Array α) (i : Fin (as.size+1)) (v : α) - (k) (hgt : k > i.val) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} : - (as.insertAt i v)[k] = as[k - 1] := by - simp only [insertAt] - rw [get_insertAt_loop_gt_le, getElem_push, dif_pos hk'] - exact hgt - rw [size_insertAt] at hk - exact Nat.le_of_lt_succ hk - -theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α) - (k) (heq : i.val = k) {hk : k < (as.insertAt i v).size} : - (as.insertAt i v)[k] = v := by - simp only [insertAt] - rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq] - exact heq - exact Nat.le_of_lt_succ i.is_lt - -/-! ### ofFn -/ - -@[simp] theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by - apply List.ext_getElem <;> simp - -/-! ### finRange -/ - -@[simp] theorem size_finRange (n) : (Array.finRange n).size = n := by - simp [Array.finRange] - -@[simp] theorem getElem_finRange (n i) (h : i < (Array.finRange n).size) : - (Array.finRange n)[i] = ⟨i, size_finRange n ▸ h⟩ := by - simp [Array.finRange] - -@[simp] theorem toList_finRange (n) : (Array.finRange n).toList = List.finRange n := by - simp [Array.finRange, List.finRange] +theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {h} : + (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]'(by simpa using h) := by + unfold insertIdx.loop + split <;> rename_i h₁ + · simp at h₁ + have : j - 1 < j := by omega + rw [getElem_insertIdx_loop_eq] + rw [getElem_swap] + simp + split <;> rename_i h₂ + · rw [if_pos (by omega)] + · omega + · simp at h₁ + by_cases h' : i = j + · simp [h'] + · have t : ¬ i ≤ j := by omega + simp [t] + +theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} + {k : Nat} {h} (w : i < k) : + (insertIdx.loop i as ⟨j, hj⟩)[k] = + if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by + unfold insertIdx.loop + split <;> rename_i h₁ + · simp only + simp only at h₁ + have : j - 1 < j := by omega + rw [getElem_insertIdx_loop_gt w] + rw [getElem_swap] + split <;> rename_i h₂ + · rw [if_neg (by omega), if_neg (by omega)] + have t : k ≤ j := by omega + simp [t] + · rw [getElem_swap] + rw [if_neg (by omega)] + split <;> rename_i h₃ + · simp [h₃] + · have t : ¬ k ≤ j := by omega + simp [t] + · simp only at h₁ + have t : ¬ k ≤ j := by omega + simp [t] + +theorem getElem_insertIdx_loop {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {k : Nat} {h} : + (insertIdx.loop i as ⟨j, hj⟩)[k] = + if h₁ : k < i then + as[k]'(by simpa using h) + else + if h₂ : k = i then + if i ≤ j then as[j] else as[i]'(by simpa [h₂] using h) + else + if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by + split <;> rename_i h₁ + · rw [getElem_insertIdx_loop_lt h₁] + · split <;> rename_i h₂ + · subst h₂ + rw [getElem_insertIdx_loop_eq] + · rw [getElem_insertIdx_loop_gt (by omega)] + +theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) + (k) (h' : k < (as.insertIdx i v).size) : + (as.insertIdx i v)[k] = + if h₁ : k < i then + as[k]'(by omega) + else + if h₂ : k = i then + v + else + as[k - 1]'(by simp at h'; omega) := by + unfold insertIdx + rw [getElem_insertIdx_loop] + simp only [size_insertIdx] at h' + replace h' : k ≤ as.size := by omega + simp only [getElem_push, h, ↓reduceIte, Nat.lt_irrefl, ↓reduceDIte, h', dite_eq_ite] + split <;> rename_i h₁ + · rw [dif_pos (by omega)] + · split <;> rename_i h₂ + · simp [h₂] + · split <;> rename_i h₃ + · rfl + · omega + +theorem getElem_insertIdx_lt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) + (k) (h' : k < (as.insertIdx i v).size) (h : k < i) : + (as.insertIdx i v)[k] = as[k] := by + simp [getElem_insertIdx, h] + +@[deprecated getElem_insertIdx_lt (since := "2024-11-20")] alias getElem_insertAt_lt := +getElem_insertIdx_lt + +theorem getElem_insertIdx_eq (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) : + (as.insertIdx i v)[i]'(by simp; omega) = v := by + simp [getElem_insertIdx, h] + +@[deprecated getElem_insertIdx_eq (since := "2024-11-20")] alias getElem_insertAt_eq := +getElem_insertIdx_eq + +theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) + (k) (h' : k < (as.insertIdx i v).size) (h : i < k) : + (as.insertIdx i v)[k] = as[k-1]'(by simp at h'; omega) := by + rw [getElem_insertIdx] + rw [dif_neg (by omega), dif_neg (by omega)] + +@[deprecated getElem_insertIdx_gt (since := "2024-11-20")] alias getElem_insertAt_gt := +getElem_insertIdx_gt diff --git a/Batteries/Data/Array/Merge.lean b/Batteries/Data/Array/Merge.lean index 70034111ad..7f26fd0c3f 100644 --- a/Batteries/Data/Array/Merge.lean +++ b/Batteries/Data/Array/Merge.lean @@ -83,7 +83,7 @@ set_option linter.unusedVariables.funArgs false in `f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ`. -/ def mergeAdjacentDups [eq : BEq α] (f : α → α → α) (xs : Array α) : Array α := - if h : 0 < xs.size then go (mkEmpty xs.size) 1 (xs.get ⟨0, h⟩) else xs + if h : 0 < xs.size then go (mkEmpty xs.size) 1 xs[0] else xs where /-- Auxiliary definition for `mergeAdjacentDups`. -/ go (acc : Array α) (i : Nat) (hd : α) := diff --git a/Batteries/Data/Array/Monadic.lean b/Batteries/Data/Array/Monadic.lean index 934111e131..ba297a9f70 100644 --- a/Batteries/Data/Array/Monadic.lean +++ b/Batteries/Data/Array/Monadic.lean @@ -153,7 +153,7 @@ theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Nat (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) : SatisfiesM (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i]) - (Array.mapIdxM as f) := + (as.mapIdxM f) := SatisfiesM_mapFinIdxM as (fun i => f i) motive h0 p hs theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α → m α) : diff --git a/Batteries/Data/Array/OfFn.lean b/Batteries/Data/Array/OfFn.lean index e02be7cba1..5233fd1f96 100644 --- a/Batteries/Data/Array/OfFn.lean +++ b/Batteries/Data/Array/OfFn.lean @@ -11,8 +11,4 @@ namespace Array /-! ### ofFn -/ -@[simp] -theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by - apply ext_getElem <;> simp - end Array diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean index 82ace9609f..498c070540 100644 --- a/Batteries/Data/Array/Pairwise.lean +++ b/Batteries/Data/Array/Pairwise.lean @@ -20,7 +20,7 @@ that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔ - ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by + ∀ (i j : Fin as.size), i < j → R (as.get i i.2) (as.get j j.2) := by unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList] theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔ diff --git a/Batteries/Data/BinaryHeap.lean b/Batteries/Data/BinaryHeap.lean index 29a273a9d0..4795be8352 100644 --- a/Batteries/Data/BinaryHeap.lean +++ b/Batteries/Data/BinaryHeap.lean @@ -67,9 +67,9 @@ def heapifyUp (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) : match i with | ⟨0, _⟩ => a | ⟨i'+1, hi⟩ => - let j := ⟨i'/2, by get_elem_tactic⟩ + let j := i'/2 if lt a[j] a[i] then - heapifyUp lt (a.swap i j) j + heapifyUp lt (a.swap i j) ⟨j, by get_elem_tactic⟩ else a /-- `O(1)`. Build a new empty heap. -/ @@ -88,7 +88,7 @@ def size (self : BinaryHeap α lt) : Nat := self.1.size def vector (self : BinaryHeap α lt) : Vector α self.size := ⟨self.1, rfl⟩ /-- `O(1)`. Get an element in the heap by index. -/ -def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i +def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1[i]'(i.2) /-- `O(log n)`. Insert an element into a `BinaryHeap`, preserving the max-heap property. -/ def insert (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where @@ -107,7 +107,7 @@ def popMax (self : BinaryHeap α lt) : BinaryHeap α lt := if h0 : self.size = 0 then self else have hs : self.size - 1 < self.size := Nat.pred_lt h0 have h0 : 0 < self.size := Nat.zero_lt_of_ne_zero h0 - let v := self.vector.swap ⟨_, h0⟩ ⟨_, hs⟩ |>.pop + let v := self.vector.swap _ _ h0 hs |>.pop if h : 0 < self.size - 1 then ⟨heapifyDown lt v ⟨0, h⟩ |>.toArray⟩ else @@ -136,7 +136,7 @@ def insertExtractMax (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt | none => (x, self) | some m => if lt x m then - let v := self.vector.set ⟨0, size_pos_of_max e⟩ x + let v := self.vector.set 0 x (size_pos_of_max e) (m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩) else (x, self) @@ -145,7 +145,7 @@ def replaceMax (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α l match e : self.max with | none => (none, ⟨self.vector.push x |>.toArray⟩) | some m => - let v := self.vector.set ⟨0, size_pos_of_max e⟩ x + let v := self.vector.set 0 x (size_pos_of_max e) (some m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩) /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/ diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean index 6a95a241aa..86a495e2df 100644 --- a/Batteries/Data/ByteArray.lean +++ b/Batteries/Data/ByteArray.lean @@ -15,7 +15,7 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data /-! ### uget/uset -/ @[simp] theorem uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) : - a.uset i v h = a.set ⟨i.toNat, h⟩ v := rfl + a.uset i v h = a.set i.toNat v := rfl /-! ### empty -/ @@ -45,7 +45,7 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) : /-! ### set -/ @[simp] theorem data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) : - (a.set i v).data = a.data.set i v := rfl + (a.set i v).data = a.data.set i v i.isLt := rfl @[deprecated (since := "2024-08-13")] alias set_data := data_set @[simp] theorem size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) : @@ -60,7 +60,7 @@ theorem get_set_ne (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size Array.get_set_ne (h:=h) .. theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) : - (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := + (a.set i v).set i v' = a.set i v' := ByteArray.ext <| Array.set_set .. /-! ### copySlice -/ @@ -132,7 +132,7 @@ def ofFn (f : Fin n → UInt8) : ByteArray where simp [get, Fin.cast] @[simp] theorem getElem_ofFn (f : Fin n → UInt8) (i) (h : i < (ofFn f).size) : - (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn .. + (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn f ⟨i, h⟩ private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where go (i : Nat) (acc : ByteArray) : ByteArray := diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index f1357f50b0..f63e38ab37 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -17,57 +17,3 @@ alias enum := Array.finRange @[deprecated (since := "2024-11-15")] alias list := List.finRange - -/-- -Folds a monadic function over `Fin n` from left to right: -``` -Fin.foldlM n f x₀ = do - let x₁ ← f x₀ 0 - let x₂ ← f x₁ 1 - ... - let xₙ ← f xₙ₋₁ (n-1) - pure xₙ -``` --/ -@[inline] def foldlM [Monad m] (n) (f : α → Fin n → m α) (init : α) : m α := loop init 0 where - /-- - Inner loop for `Fin.foldlM`. - ``` - Fin.foldlM.loop n f xᵢ i = do - let xᵢ₊₁ ← f xᵢ i - ... - let xₙ ← f xₙ₋₁ (n-1) - pure xₙ - ``` - -/ - loop (x : α) (i : Nat) : m α := do - if h : i < n then f x ⟨i, h⟩ >>= (loop · (i+1)) else pure x - termination_by n - i - -/-- -Folds a monadic function over `Fin n` from right to left: -``` -Fin.foldrM n f xₙ = do - let xₙ₋₁ ← f (n-1) xₙ - let xₙ₋₂ ← f (n-2) xₙ₋₁ - ... - let x₀ ← f 0 x₁ - pure x₀ -``` --/ -@[inline] def foldrM [Monad m] (n) (f : Fin n → α → m α) (init : α) : m α := - loop ⟨n, Nat.le_refl n⟩ init where - /-- - Inner loop for `Fin.foldrM`. - ``` - Fin.foldrM.loop n f i xᵢ = do - let xᵢ₋₁ ← f (i-1) xᵢ - ... - let x₁ ← f 1 x₂ - let x₀ ← f 0 x₁ - pure x₀ - ``` - -/ - loop : {i // i ≤ n} → α → m α - | ⟨0, _⟩, x => pure x - | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩ diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 90a574cf2c..ddc7bbf1cf 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -13,139 +13,3 @@ attribute [norm_cast] val_last /-! ### clamp -/ @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl - -/-! ### foldlM -/ - -theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) : - foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by - rw [foldlM.loop, dif_pos h] - -theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x := by - rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)] - -theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) : - foldlM.loop (n+1) f x i = f x ⟨i, h⟩ >>= (foldlM.loop n (fun x j => f x j.succ) . i) := by - if h' : i < n then - rw [foldlM_loop_lt _ _ h] - congr; funext - rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl - else - cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [foldlM_loop_lt] - congr; funext - rw [foldlM_loop_eq, foldlM_loop_eq] -termination_by n - i - -@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x := - foldlM_loop_eq .. - -theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) : - foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop .. - -/-! ### foldrM -/ - -theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) : - foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by - rw [foldrM.loop] - -theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) : - foldrM.loop n f ⟨i+1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, Nat.le_of_lt h⟩ := by - rw [foldrM.loop] - -theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) : - foldrM.loop (n+1) f ⟨i+1, h⟩ x = - foldrM.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x >>= f 0 := by - induction i generalizing x with - | zero => - rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind] - conv => rhs; rw [←bind_pure (f 0 x)] - congr; funext; exact foldrM_loop_zero .. - | succ i ih => - rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc] - congr; funext; exact ih .. - -@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x := - foldrM_loop_zero .. - -theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) : - foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop .. - -/-! ### foldl -/ - -theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) : - foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by - rw [foldl.loop, dif_pos h] - -theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by - rw [foldl.loop, dif_neg (Nat.lt_irrefl _)] - -theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : i < n+1) : - foldl.loop (n+1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i := by - if h' : i < n then - rw [foldl_loop_lt _ _ h] - rw [foldl_loop_lt _ _ h', foldl_loop]; rfl - else - cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [foldl_loop_lt] - rw [foldl_loop_eq, foldl_loop_eq] - -@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := - foldl_loop_eq .. - -theorem foldl_succ (f : α → Fin (n+1) → α) (x) : - foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) := - foldl_loop .. - -theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) : - foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by - rw [foldl_succ] - induction n generalizing x with - | zero => simp [foldl_succ, Fin.last] - | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc] - -theorem foldl_eq_foldlM (f : α → Fin n → α) (x) : - foldl n f x = foldlM (m:=Id) n f x := by - induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *] - -/-! ### foldr -/ - -theorem foldr_loop_zero (f : Fin n → α → α) (x) : - foldr.loop n f ⟨0, Nat.zero_le _⟩ x = x := by - rw [foldr.loop] - -theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) : - foldr.loop n f ⟨i+1, h⟩ x = foldr.loop n f ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x) := by - rw [foldr.loop] - -theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) : - foldr.loop (n+1) f ⟨i+1, h⟩ x = - f 0 (foldr.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x) := by - induction i generalizing x <;> simp [foldr_loop_zero, foldr_loop_succ, *] - -@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x := - foldr_loop_zero .. - -theorem foldr_succ (f : Fin (n+1) → α → α) (x) : - foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop .. - -theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) : - foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by - induction n generalizing x with - | zero => simp [foldr_succ, Fin.last] - | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc] - -theorem foldr_eq_foldrM (f : Fin n → α → α) (x) : - foldr n f x = foldrM (m:=Id) n f x := by - induction n <;> simp [foldr_succ, foldrM_succ, *] - -theorem foldl_rev (f : Fin n → α → α) (x) : - foldl n (fun x i => f i.rev x) x = foldr n f x := by - induction n generalizing x with - | zero => simp - | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ] - -theorem foldr_rev (f : α → Fin n → α) (x) : - foldr n (fun i x => f x i.rev) x = foldl n f x := by - induction n generalizing x with - | zero => simp - | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ] diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean index de029c4276..0d1b2b1fe1 100644 --- a/Batteries/Data/HashMap/Basic.lean +++ b/Batteries/Data/HashMap/Basic.lean @@ -40,7 +40,7 @@ Note: this is marked `noncomputable` because it is only intended for specificati noncomputable def size (data : Buckets α β) : Nat := (data.1.toList.map (·.toList.length)).sum @[simp] theorem update_size (self : Buckets α β) (i d h) : - (self.update i d h).1.size = self.1.size := Array.size_uset .. + (self.update i d h).1.size = self.1.size := Array.size_uset _ _ _ h /-- Map a function over the values in the map. -/ @[specialize] def mapVal (f : α → β → γ) (self : Buckets α β) : Buckets α γ := @@ -143,11 +143,10 @@ where destroying `source` in the process. -/ go (i : Nat) (source : Array (AssocList α β)) (target : Buckets α β) : Buckets α β := if h : i < source.size then - let idx : Fin source.size := ⟨i, h⟩ - let es := source.get idx + let es := source[i] -- We remove `es` from `source` to make sure we can reuse its memory cells -- when performing es.foldl - let source := source.set idx .nil + let source := source.set i .nil let target := es.foldl reinsertAux target go (i+1) source target else target diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index 8dbcabb4a8..1404315159 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -159,32 +159,8 @@ Split a list at every occurrence of a separator element. The separators are not | [x], acc => acc.toListAppend [f x] | x :: xs, acc => go xs (acc.push x) -/-- -`insertIdx n a l` inserts `a` into the list `l` after the first `n` elements of `l` -``` -insertIdx 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4] -``` --/ -def insertIdx (n : Nat) (a : α) : List α → List α := - modifyTailIdx (cons a) n - @[deprecated (since := "2024-10-21")] alias insertNth := insertIdx -/-- Tail-recursive version of `insertIdx`. -/ -@[inline] def insertIdxTR (n : Nat) (a : α) (l : List α) : List α := go n l #[] where - /-- Auxiliary for `insertIdxTR`: `insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l`. -/ - go : Nat → List α → Array α → List α - | 0, l, acc => acc.toListAppend (a :: l) - | _, [], acc => acc.toList - | n+1, a :: l, acc => go n l (acc.push a) - -theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l - | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx] - | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l] - -@[csimp] theorem insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR := by - funext α f n l; simp [insertIdxTR, insertIdxTR_go_eq] - theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a := by cases l <;> rfl /-- @@ -487,7 +463,7 @@ theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L = cases e : L.any isEmpty <;> simp [sections_eq_nil_of_isEmpty, *] clear e; induction L with | nil => rfl | cons l L IH => ?_ simp [IH, sectionsTR.go] - rw [Array.foldl_eq_foldl_toList, Array.foldl_toList_eq_flatMap]; rfl + rw [← Array.foldl_toList, Array.foldl_toList_eq_flatMap]; rfl intros; apply Array.foldl_toList_eq_map /-- @@ -544,14 +520,6 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) : rw [Array.foldl_toList_eq_flatMap]; rfl intros; apply Array.foldl_toList_eq_map -/-- -`ofFn f` with `f : fin n → α` returns the list whose ith element is `f i` -``` -ofFn f = [f 0, f 1, ... , f (n - 1)] -``` --/ -def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) [] - /-- `ofFnNthVal f i` returns `some (f i)` if `i < n` and `none` otherwise. -/ def ofFnNthVal {n} (f : Fin n → α) (i : Nat) : Option α := if h : i < n then some (f ⟨i, h⟩) else none @@ -1096,6 +1064,3 @@ where | a :: as, acc => match (a :: as).dropPrefix? i with | none => go as (a :: acc) | some s => (acc.reverse, s) - -/-- `finRange n` lists all elements of `Fin n` in order -/ -def finRange (n : Nat) : List (Fin n) := ofFn fun i => i diff --git a/Batteries/Data/List/FinRange.lean b/Batteries/Data/List/FinRange.lean index 432e3133af..dd6b13724d 100644 --- a/Batteries/Data/List/FinRange.lean +++ b/Batteries/Data/List/FinRange.lean @@ -7,54 +7,20 @@ import Batteries.Data.List.OfFn namespace List -@[simp] theorem length_finRange (n) : (List.finRange n).length = n := by - simp [List.finRange] - @[deprecated (since := "2024-11-19")] alias length_list := length_finRange -@[simp] theorem getElem_finRange (i : Nat) (h : i < (List.finRange n).length) : - (finRange n)[i] = Fin.cast (length_finRange n) ⟨i, h⟩ := by - simp [List.finRange] - @[deprecated (since := "2024-11-19")] alias getElem_list := getElem_finRange -@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn] - @[deprecated (since := "2024-11-19")] alias list_zero := finRange_zero -theorem finRange_succ (n) : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by - apply List.ext_getElem; simp; intro i; cases i <;> simp - @[deprecated (since := "2024-11-19")] alias list_succ := finRange_succ -theorem finRange_succ_last (n) : - finRange (n+1) = (finRange n).map Fin.castSucc ++ [Fin.last n] := by - apply List.ext_getElem - · simp - · intros - simp only [List.finRange, List.getElem_ofFn, getElem_append, length_map, length_ofFn, - getElem_map, Fin.castSucc_mk, getElem_singleton] - split - · rfl - · next h => exact Fin.eq_last_of_not_lt h - @[deprecated (since := "2024-11-19")] alias list_succ_last := finRange_succ_last -theorem finRange_reverse (n) : (finRange n).reverse = (finRange n).map Fin.rev := by - induction n with - | zero => simp - | succ n ih => - conv => lhs; rw [finRange_succ_last] - conv => rhs; rw [finRange_succ] - rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse, - map_cons, ih, map_map, map_map] - congr; funext - simp [Fin.rev_succ] - @[deprecated (since := "2024-11-19")] alias list_reverse := finRange_reverse diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 840940dbaf..1e02d90c98 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -15,26 +15,6 @@ namespace List @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl -/-! ### == -/ - -@[simp] theorem beq_nil_iff [BEq α] {l : List α} : (l == []) = l.isEmpty := by - cases l <;> rfl - -@[simp] theorem nil_beq_iff [BEq α] {l : List α} : ([] == l) = l.isEmpty := by - cases l <;> rfl - -@[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} : - (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl - -theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length := - match l₁, l₂ with - | [], [] => rfl - | [], _ :: _ => by simp [beq_nil_iff] at h - | _ :: _, [] => by simp [nil_beq_iff] at h - | a :: l₁, b :: l₂ => by - simp at h - simpa using length_eq_of_beq h.2 - /-! ### next? -/ @[simp] theorem next?_nil : @next? α [] = none := rfl diff --git a/Batteries/Data/List/OfFn.lean b/Batteries/Data/List/OfFn.lean index 93214cc99b..c66846e61a 100644 --- a/Batteries/Data/List/OfFn.lean +++ b/Batteries/Data/List/OfFn.lean @@ -12,38 +12,4 @@ import Batteries.Data.Fin.Lemmas namespace List -@[simp] -theorem length_ofFn (f : Fin n → α) : (ofFn f).length = n := by - simp only [ofFn] - induction n with - | zero => simp - | succ n ih => simp [Fin.foldr_succ, ih] - -@[simp] -protected theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length) : - (ofFn f)[i] = f ⟨i, by simp_all⟩ := by - simp only [ofFn] - induction n generalizing i with - | zero => simp at h - | succ n ih => - match i with - | 0 => simp [Fin.foldr_succ] - | i+1 => - simp only [Fin.foldr_succ] - apply ih - simp_all - -@[simp] -protected theorem getElem?_ofFn (f : Fin n → α) (i) : (ofFn f)[i]? = ofFnNthVal f i := - if h : i < (ofFn f).length - then by - rw [getElem?_eq_getElem h, List.getElem_ofFn] - · simp only [length_ofFn] at h; simp [ofFnNthVal, h] - else by - rw [ofFnNthVal, dif_neg] <;> - simpa using h - -@[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by - ext <;> simp - end List diff --git a/Batteries/Data/MLList/Basic.lean b/Batteries/Data/MLList/Basic.lean index 1ed6d7e256..8ab11c3d80 100644 --- a/Batteries/Data/MLList/Basic.lean +++ b/Batteries/Data/MLList/Basic.lean @@ -334,7 +334,7 @@ partial def fin (n : Nat) : MLList m (Fin n) := go 0 where partial def ofArray {α : Type} (L : Array α) : MLList m α := go 0 where /-- Implementation of `MLList.ofArray`. -/ go (i : Nat) : MLList m α := - if h : i < L.size then cons (L.get ⟨i, h⟩) (thunk fun _ => go (i+1)) else nil + if h : i < L.size then cons L[i] (thunk fun _ => go (i+1)) else nil /-- Group the elements of a lazy list into chunks of a given size. If the lazy list is finite, the last chunk may be smaller (possibly even length 0). -/ diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean index 431591ebc1..642029cdd1 100644 --- a/Batteries/Data/String/Lemmas.lean +++ b/Batteries/Data/String/Lemmas.lean @@ -573,7 +573,7 @@ theorem extract (h₁ : ValidFor l (m ++ r) it₁) (h₂ : ValidFor (m.reverse + it₁.extract it₂ = ⟨m⟩ := by cases h₁.out; cases h₂.out simp only [Iterator.extract, List.reverseAux_eq, List.reverse_append, List.reverse_reverse, - List.append_assoc, ne_eq, not_true_eq_false, decide_False, utf8Len_append, utf8Len_reverse, + List.append_assoc, ne_eq, not_true_eq_false, decide_false, utf8Len_append, utf8Len_reverse, gt_iff_lt, pos_lt_eq, Nat.not_lt.2 (Nat.le_add_left ..), Bool.or_self, Bool.false_eq_true, ↓reduceIte] simpa [Nat.add_comm] using extract_of_valid l.reverse m r diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index 3f9b495629..007a57d75d 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -10,11 +10,6 @@ import Batteries.Classes.Order @[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -@[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl - -@[simp] theorem UInt8.toNat_ofNat (n) : - (no_index (OfNat.ofNat n) : UInt8).toNat = n % UInt8.size := rfl - theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt @[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl @@ -23,19 +18,6 @@ theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt @[simp] theorem UInt8.toUInt64_toNat (x : UInt8) : x.toUInt64.toNat = x.toNat := rfl -theorem UInt8.toNat_add (x y : UInt8) : (x + y).toNat = (x.toNat + y.toNat) % UInt8.size := rfl - -theorem UInt8.toNat_sub (x y : UInt8) : - (x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size := rfl - -theorem UInt8.toNat_mul (x y : UInt8) : (x * y).toNat = (x.toNat * y.toNat) % UInt8.size := rfl - -theorem UInt8.le_antisymm_iff {x y : UInt8} : x = y ↔ x ≤ y ∧ y ≤ x := - UInt8.ext_iff.trans Nat.le_antisymm_iff - -theorem UInt8.le_antisymm {x y : UInt8} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := - UInt8.le_antisymm_iff.2 ⟨h1, h2⟩ - instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt8.le_antisymm @@ -44,11 +26,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -@[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl - -@[simp] theorem UInt16.toNat_ofNat (n) : - (no_index (OfNat.ofNat n) : UInt16).toNat = n % UInt16.size := rfl - theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt @[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl @@ -57,19 +34,6 @@ theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt @[simp] theorem UInt16.toUInt64_toNat (x : UInt16) : x.toUInt64.toNat = x.toNat := rfl -theorem UInt16.toNat_add (x y : UInt16) : (x + y).toNat = (x.toNat + y.toNat) % UInt16.size := rfl - -theorem UInt16.toNat_sub (x y : UInt16) : - (x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size := rfl - -theorem UInt16.toNat_mul (x y : UInt16) : (x * y).toNat = (x.toNat * y.toNat) % UInt16.size := rfl - -theorem UInt16.le_antisymm_iff {x y : UInt16} : x = y ↔ x ≤ y ∧ y ≤ x := - UInt16.ext_iff.trans Nat.le_antisymm_iff - -theorem UInt16.le_antisymm {x y : UInt16} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := - UInt16.le_antisymm_iff.2 ⟨h1, h2⟩ - instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt16.le_antisymm @@ -78,11 +42,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -@[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl - -@[simp] theorem UInt32.toNat_ofNat (n) : - (no_index (OfNat.ofNat n) : UInt32).toNat = n % UInt32.size := rfl - theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt @[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl @@ -91,19 +50,6 @@ theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt @[simp] theorem UInt32.toUInt64_toNat (x : UInt32) : x.toUInt64.toNat = x.toNat := rfl -theorem UInt32.toNat_add (x y : UInt32) : (x + y).toNat = (x.toNat + y.toNat) % UInt32.size := rfl - -theorem UInt32.toNat_sub (x y : UInt32) : - (x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size := rfl - -theorem UInt32.toNat_mul (x y : UInt32) : (x * y).toNat = (x.toNat * y.toNat) % UInt32.size := rfl - -theorem UInt32.le_antisymm_iff {x y : UInt32} : x = y ↔ x ≤ y ∧ y ≤ x := - UInt32.ext_iff.trans Nat.le_antisymm_iff - -theorem UInt32.le_antisymm {x y : UInt32} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := - UInt32.le_antisymm_iff.2 ⟨h1, h2⟩ - instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt32.le_antisymm @@ -112,11 +58,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -@[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl - -@[simp] theorem UInt64.toNat_ofNat (n) : - (no_index (OfNat.ofNat n) : UInt64).toNat = n % UInt64.size := rfl - theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt @[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl @@ -125,19 +66,6 @@ theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt @[simp] theorem UInt64.toUInt32_toNat (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl -theorem UInt64.toNat_add (x y : UInt64) : (x + y).toNat = (x.toNat + y.toNat) % UInt64.size := rfl - -theorem UInt64.toNat_sub (x y : UInt64) : - (x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size := rfl - -theorem UInt64.toNat_mul (x y : UInt64) : (x * y).toNat = (x.toNat * y.toNat) % UInt64.size := rfl - -theorem UInt64.le_antisymm_iff {x y : UInt64} : x = y ↔ x ≤ y ∧ y ≤ x := - UInt64.ext_iff.trans Nat.le_antisymm_iff - -theorem UInt64.le_antisymm {x y : UInt64} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := - UInt64.le_antisymm_iff.2 ⟨h1, h2⟩ - instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt64.le_antisymm @@ -146,11 +74,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -@[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl - -@[simp] theorem USize.toNat_ofNat (n) : - (no_index (OfNat.ofNat n) : USize).toNat = n % USize.size := rfl - theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by rw [USize.size] @@ -172,18 +95,5 @@ theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by @[simp] theorem UInt32.toUSize_toNat (x : UInt32) : x.toUSize.toNat = x.toNat := rfl -theorem USize.toNat_add (x y : USize) : (x + y).toNat = (x.toNat + y.toNat) % USize.size := rfl - -theorem USize.toNat_sub (x y : USize) : - (x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size := rfl - -theorem USize.toNat_mul (x y : USize) : (x * y).toNat = (x.toNat * y.toNat) % USize.size := rfl - -theorem USize.le_antisymm_iff {x y : USize} : x = y ↔ x ≤ y ∧ y ≤ x := - USize.ext_iff.trans Nat.le_antisymm_iff - -theorem USize.le_antisymm {x y : USize} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := - USize.le_antisymm_iff.2 ⟨h1, h2⟩ - instance : Batteries.LawfulOrd USize := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt USize.le_antisymm diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean index c48bb5bda1..3328834ec2 100644 --- a/Batteries/Data/UnionFind/Basic.lean +++ b/Batteries/Data/UnionFind/Basic.lean @@ -25,39 +25,35 @@ namespace UnionFind /-- Parent of a union-find node, defaults to self when the node is a root -/ def parentD (arr : Array UFNode) (i : Nat) : Nat := - if h : i < arr.size then (arr.get ⟨i, h⟩).parent else i + if h : i < arr.size then arr[i].parent else i /-- Rank of a union-find node, defaults to 0 when the node is a root -/ def rankD (arr : Array UFNode) (i : Nat) : Nat := - if h : i < arr.size then (arr.get ⟨i, h⟩).rank else 0 + if h : i < arr.size then arr[i].rank else 0 -theorem parentD_eq {arr : Array UFNode} {i} : parentD arr i.1 = (arr.get i).parent := dif_pos _ +theorem parentD_eq {arr : Array UFNode} {i} (h) : + parentD arr i = arr[i].parent := dif_pos _ -theorem parentD_eq' {arr : Array UFNode} {i} (h) : - parentD arr i = (arr.get ⟨i, h⟩).parent := dif_pos _ - -theorem rankD_eq {arr : Array UFNode} {i} : rankD arr i.1 = (arr.get i).rank := dif_pos _ - -theorem rankD_eq' {arr : Array UFNode} {i} (h) : rankD arr i = (arr.get ⟨i, h⟩).rank := dif_pos _ +theorem rankD_eq {arr : Array UFNode} {i} (h) : rankD arr i = arr[i].rank := dif_pos _ theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·) theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size := Decidable.not_imp_comm.1 parentD_of_not_lt -theorem parentD_set {arr : Array UFNode} {x v i} : - parentD (arr.set x v) i = if x.1 = i then v.parent else parentD arr i := by +theorem parentD_set {arr : Array UFNode} {x v i h} : + parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD] split · split <;> simp_all - · split <;> [(subst i; cases ‹¬_› x.2); rfl] + · split <;> [(subst i; cases ‹¬_› h); rfl] -theorem rankD_set {arr : Array UFNode} {x v i} : - rankD (arr.set x v) i = if x.1 = i then v.rank else rankD arr i := by +theorem rankD_set {arr : Array UFNode} {x v i h} : + rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD] split · split <;> simp_all - · split <;> [(subst i; cases ‹¬_› x.2); rfl] + · split <;> [(subst i; cases ‹¬_› h); rfl] end UnionFind @@ -126,9 +122,8 @@ instance : EmptyCollection UnionFind := ⟨.empty⟩ /-- Parent of union-find node -/ abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i -theorem parent'_lt (self : UnionFind) (i : Fin self.size) : - (self.arr.get i).parent < self.size := by - simp only [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList] +theorem parent'_lt (self : UnionFind) (i : Nat) (h) : self.arr[i].parent < self.size := by + simp [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList, h] theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by simp only [parentD]; split <;> simp only [*, parent'_lt] @@ -139,20 +134,19 @@ abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i → self.rank i < self.rank (self.parent i) := by simpa only [rank] using self.rankD_lt -theorem rank'_lt (self : UnionFind) (i : Fin self.size) : (self.arr.get i).parent ≠ i → - self.rank i < self.rank (self.arr.get i).parent := by +theorem rank'_lt (self : UnionFind) (i h) : self.arr[i].parent ≠ i → + self.rank i < self.rank (self.arr[i]).parent := by simpa only [← parentD_eq] using self.rankD_lt /-- Maximum rank of nodes in a union-find structure -/ noncomputable def rankMax (self : UnionFind) := self.arr.foldr (max ·.rank) 0 + 1 -theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) : - (self.arr.get i).rank < self.rankMax := by +theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank < self.rankMax := by let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..) - simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList] - exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2) + simp only [Array.get_eq_getElem, rankMax, ← Array.foldr_toList] + exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem _) theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) : rankD self.arr i < self.rankMax := by @@ -175,17 +169,17 @@ def push (self : UnionFind) : UnionFind where arr := self.arr.push ⟨self.arr.size, 0⟩ parentD_lt {i} := by simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem] - split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt _); exact id] + split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt ..); exact id] rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt /-- Root of a union-find node. -/ def root (self : UnionFind) (x : Fin self.size) : Fin self.size := - let y := (self.arr.get x).parent + let y := self.arr[x.1].parent if h : y = x then x else - have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h) - self.root ⟨y, self.parent'_lt x⟩ + have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ h) + self.root ⟨y, self.parent'_lt x _⟩ termination_by self.rankMax - self.rank x @[inherit_doc root] @@ -202,9 +196,9 @@ def rootD (self : UnionFind) (x : Nat) : Nat := @[nolint unusedHavesSuffices] theorem parent_root (self : UnionFind) (x : Fin self.size) : - (self.arr.get (self.root x)).parent = self.root x := by + (self.arr[(self.root x).1]).parent = self.root x := by rw [root]; split <;> [assumption; skip] - have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›) + have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›) apply parent_root termination_by self.rankMax - self.rank x @@ -231,7 +225,7 @@ theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x < @[nolint unusedHavesSuffices] theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩ - rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl] + rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq ‹_›] at h)]; rfl] theorem rootD_rootD {self : UnionFind} {x : Nat} : self.rootD (self.rootD x) = self.rootD x := rootD_eq_self.2 (parent_rootD ..) @@ -271,12 +265,12 @@ structure FindAux (n : Nat) where /-- Auxiliary function for find operation -/ def findAux (self : UnionFind) (x : Fin self.size) : FindAux self.size := - let y := (self.arr.get x).parent + let y := self.arr[x.1].parent if h : y = x then ⟨self.arr, x, rfl⟩ else - have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h) - let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt x⟩ + have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ h) + let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt _ x.2⟩ ⟨arr₁.modify x fun s => { s with parent := root }, root, by simp [H]⟩ termination_by self.rankMax - self.rank x @@ -286,16 +280,16 @@ theorem findAux_root {self : UnionFind} {x : Fin self.size} : rw [findAux, root] simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite] split <;> simp only - have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›) + have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›) exact findAux_root termination_by self.rankMax - self.rank x @[nolint unusedHavesSuffices] theorem findAux_s {self : UnionFind} {x : Fin self.size} : - (findAux self x).s = if (self.arr.get x).parent = x then self.arr else - (self.findAux ⟨_, self.parent'_lt x⟩).s.modify x fun s => + (findAux self x).s = if self.arr[x.1].parent = x then self.arr else + (self.findAux ⟨_, self.parent'_lt x x.2⟩).s.modify x fun s => { s with parent := self.rootD x } := by - rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _] + rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x x.2⟩).root from _] · rw [findAux]; split <;> rfl · rw [← rootD_parent, parent, parentD_eq] simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root] @@ -307,10 +301,11 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} : rankD (findAux self x).s i = self.rank i := by if h : i < self.size then rw [findAux_s]; split <;> [rfl; skip] - have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›) + have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›) have := lt_of_parentD (by rwa [parentD_eq]) - rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify] - split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem] + rw [rankD_eq (by simp [FindAux.size_eq, h]), Array.getElem_modify] + split <;> + simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem] else simp only [rankD, Array.data_length, Array.get_eq_getElem, rank] rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h] @@ -319,13 +314,13 @@ termination_by self.rankMax - self.rank x set_option linter.deprecated false in theorem parentD_findAux {self : UnionFind} {x : Fin self.size} : parentD (findAux self x).s i = - if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt x⟩).s i := by + if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i := by rw [findAux_s]; split <;> [split; skip] · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem] · rw [findAux_s]; simp [*, -Array.get_eq_getElem] · next h => rw [parentD]; split <;> rename_i h' - · rw [Array.get_modify (by simpa using h')] + · rw [Array.getElem_modify (by simpa using h')] simp only [Array.data_length, @eq_comm _ i] split <;> simp [← parentD_eq, -Array.get_eq_getElem] · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')] @@ -334,47 +329,48 @@ theorem parentD_findAux {self : UnionFind} {x : Fin self.size} : theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} : parentD (findAux self x).s (self.rootD x) = self.rootD x := by rw [parentD_findAux]; split <;> [rfl; rename_i h] - rw [rootD_eq_self, parent, parentD_eq] at h - have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›) - rw [← rootD_parent, parent, parentD_eq] - exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt x⟩) + rw [rootD_eq_self, parent, parentD_eq x.2] at h + have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›) + rw [← rootD_parent, parent, parentD_eq x.2] + exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt _ x.2⟩) termination_by self.rankMax - self.rank x theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) : parentD (findAux self x).s i < self.size := by - if h' : (self.arr.get x).parent = x then + if h' : self.arr[x.1].parent = x then rw [findAux_s, if_pos h']; apply self.parentD_lt h else rw [parentD_findAux] split · simp [rootD_lt] - · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›) + · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›) apply parentD_findAux_lt h termination_by self.rankMax - self.rank x theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) : parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨ parentD (findAux self x).s i = self.parent i := by - if h' : (self.arr.get x).parent = x then + if h' : self.arr[x.1].parent = x then rw [findAux_s, if_pos h']; exact .inr rfl else rw [parentD_findAux] split · simp [*] - · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›) - exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by - simp only [h, ← parentD_eq, rootD_parent, Array.length_toList] + · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›) + refine (parentD_findAux_or self ⟨_, self.parent'_lt _ x.2⟩ i) + |>.imp_left (.imp_right fun h => ?_) + simp only [h, ← parentD_eq, rootD_parent, Array.length_toList] termination_by self.rankMax - self.rank x theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} : parentD (findAux self x).s i ≠ i → self.rank i < self.rank (parentD (findAux self x).s i) := by - if h' : (self.arr.get x).parent = x then + if h' : self.arr[x.1].parent = x then rw [findAux_s, if_pos h']; apply self.rank_lt else rw [parentD_findAux]; split <;> rename_i h <;> intro h' · subst i; rwa [lt_rank_root, Ne, ← rootD_eq_self] - · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›) + · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›) apply lt_rankD_findAux h' termination_by self.rankMax - self.rank x @@ -447,46 +443,46 @@ def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode := if x.1 = y then self else - let nx := self.get x - let ny := self.get y + let nx := self[x.1] + let ny := self[y.1] if ny.rank < nx.rank then self.set y {ny with parent := x} else let arr₁ := self.set x {nx with parent := y} if nx.rank = ny.rank then - arr₁.set ⟨y, by simp [arr₁]⟩ {ny with rank := ny.rank + 1} + arr₁.set y {ny with rank := ny.rank + 1} (by simp [arr₁]) else arr₁ theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size} - (hroot : (arr.get x).rank < (arr.get y).rank ∨ (arr.get y).parent = y) - (H : (arr.get x).rank ≤ (arr.get y).rank) {i : Nat} + (hroot : arr[x.1].rank < arr[y.1].rank ∨ arr[y.1].parent = y) + (H : arr[x.1].rank ≤ arr[y.1].rank) {i : Nat} (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i) (hR : ∀ {i}, rankD arr' i = - if y.1 = i ∧ (arr.get x).rank = (arr.get y).rank then - (arr.get y).rank + 1 + if y.1 = i ∧ arr[x.1].rank = arr[y.1].rank then + arr[y.1].rank + 1 else rankD arr i) : ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;> split <;> rename_i h₂ <;> intro h · simp [h₂] at h - · simp only [rankD_eq, Array.get_eq_getElem] + · simp only [rankD_eq, x.2, y.2, Array.get_eq_getElem] split <;> rename_i h₃ · rw [← h₃]; apply Nat.lt_succ_self · exact Nat.lt_of_le_of_ne H h₃ · cases h₂.1 simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot - simp only [hroot, parentD_eq, not_true_eq_false] at h + simp only [hroot, parentD_eq y.2, not_true_eq_false] at h · have := rankD_lt h split <;> rename_i h₃ · rw [← rankD_eq, h₃.1]; exact Nat.lt_succ_of_lt this · exact this theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size} - (h : (arr.get x).rank < (arr.get y).rank) {i : Nat} + (h : arr[x.1].rank < arr[y.1].rank) {i : Nat} (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) : - let arr' := arr.set x ⟨y, (arr.get x).rank⟩ + let arr' := arr.set x ⟨y, arr[x].rank⟩ parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) := setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem]) @@ -505,7 +501,7 @@ def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) : · exact self.parentD_lt h · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h] · rw [parentD_set]; split - · exact self.parent'_lt _ + · exact self.parent'_lt .. · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h] · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h] rankD_lt := by diff --git a/Batteries/Data/UnionFind/Lemmas.lean b/Batteries/Data/UnionFind/Lemmas.lean index 9a7b0dac58..f070a6d4f1 100644 --- a/Batteries/Data/UnionFind/Lemmas.lean +++ b/Batteries/Data/UnionFind/Lemmas.lean @@ -43,7 +43,7 @@ theorem parentD_linkAux {self} {x y : Fin self.size} : if x.1 = y then parentD self i else - if (self.get y).rank < (self.get x).rank then + if self[y.1].rank < self[x.1].rank then if y = i then x else parentD self i else if x = i then y else parentD self i := by diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean index 0273c93c18..7b2581c852 100644 --- a/Batteries/Data/Vector/Basic.lean +++ b/Batteries/Data/Vector/Basic.lean @@ -17,290 +17,30 @@ import Batteries.Tactic.PrintPrefix `Vector α n` is a thin wrapper around `Array α` for arrays of fixed size `n`. -/ -namespace Batteries - -/-- `Vector α n` is an `Array α` with size `n`. -/ -structure Vector (α : Type u) (n : Nat) extends Array α where - /-- Array size. -/ - size_toArray : toArray.size = n -deriving Repr, DecidableEq - -attribute [simp] Vector.size_toArray - namespace Vector @[deprecated (since := "2024-10-15")] alias size_eq := size_toArray -/-- Syntax for `Vector α n` -/ -syntax "#v[" withoutPosition(sepBy(term, ", ")) "]" : term - -open Lean in -macro_rules - | `(#v[ $elems,* ]) => `(Vector.mk (n := $(quote elems.getElems.size)) #[$elems,*] rfl) - -/-- Custom eliminator for `Vector α n` through `Array α` -/ -@[elab_as_elim] -def elimAsArray {motive : Vector α n → Sort u} - (mk : ∀ (a : Array α) (ha : a.size = n), motive ⟨a, ha⟩) : - (v : Vector α n) → motive v - | ⟨a, ha⟩ => mk a ha - -/-- Custom eliminator for `Vector α n` through `List α` -/ -@[elab_as_elim] -def elimAsList {motive : Vector α n → Sort u} - (mk : ∀ (a : List α) (ha : a.length = n), motive ⟨⟨a⟩, ha⟩) : - (v : Vector α n) → motive v - | ⟨⟨a⟩, ha⟩ => mk a ha - -/-- The empty vector. -/ -@[inline] def empty : Vector α 0 := ⟨.empty, rfl⟩ - -/-- Make an empty vector with pre-allocated capacity. -/ -@[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩ - -/-- Makes a vector of size `n` with all cells containing `v`. -/ -@[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩ - -/-- Returns a vector of size `1` with element `v`. -/ -@[inline] def singleton (v : α) : Vector α 1 := ⟨#[v], rfl⟩ - -instance [Inhabited α] : Inhabited (Vector α n) where - default := mkVector n default - -/-- Get an element of a vector using a `Fin` index. -/ -@[inline] def get (v : Vector α n) (i : Fin n) : α := - v.toArray.get (i.cast v.size_toArray.symm) - -/-- Get an element of a vector using a `USize` index and a proof that the index is within bounds. -/ -@[inline] def uget (v : Vector α n) (i : USize) (h : i.toNat < n) : α := - v.toArray.uget i (v.size_toArray.symm ▸ h) - -instance : GetElem (Vector α n) Nat α fun _ i => i < n where - getElem x i h := get x ⟨i, h⟩ - -/-- -Get an element of a vector using a `Nat` index. Returns the given default value if the index is out -of bounds. --/ -@[inline] def getD (v : Vector α n) (i : Nat) (default : α) : α := v.toArray.getD i default - -/-- The last element of a vector. Panics if the vector is empty. -/ -@[inline] def back! [Inhabited α] (v : Vector α n) : α := v.toArray.back! - -/-- The last element of a vector, or `none` if the array is empty. -/ -@[inline] def back? (v : Vector α n) : Option α := v.toArray.back? - -/-- The last element of a non-empty vector. -/ -@[inline] def back [NeZero n] (v : Vector α n) : α := - -- TODO: change to just `v[n]` - have : Inhabited α := ⟨v[0]'(Nat.pos_of_neZero n)⟩ - v.back! - -/-- The first element of a non-empty vector. -/ -@[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n) - -/-- Push an element `x` to the end of a vector. -/ -@[inline] def push (x : α) (v : Vector α n) : Vector α (n + 1) := - ⟨v.toArray.push x, by simp⟩ - -/-- Remove the last element of a vector. -/ -@[inline] def pop (v : Vector α n) : Vector α (n - 1) := - ⟨Array.pop v.toArray, by simp⟩ - -/-- -Set an element in a vector using a `Fin` index. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def set (v : Vector α n) (i : Fin n) (x : α) : Vector α n := - ⟨v.toArray.set (i.cast v.size_toArray.symm) x, by simp⟩ - -/-- -Set an element in a vector using a `Nat` index. By default, the `get_elem_tactic` is used to -synthesize a proof that the index is within bounds. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def setN (v : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic) : - Vector α n := ⟨v.toArray.setN i x (by simp_all), by simp⟩ - -/-- -Set an element in a vector using a `Nat` index. Returns the vector unchanged if the index is out of -bounds. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def setD (v : Vector α n) (i : Nat) (x : α) : Vector α n := - ⟨v.toArray.setD i x, by simp⟩ - -/-- -Set an element in a vector using a `Nat` index. Panics if the index is out of bounds. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def set! (v : Vector α n) (i : Nat) (x : α) : Vector α n := - ⟨v.toArray.set! i x, by simp⟩ - -/-- Append two vectors. -/ -@[inline] def append (v : Vector α n) (w : Vector α m) : Vector α (n + m) := - ⟨v.toArray ++ w.toArray, by simp⟩ - -instance : HAppend (Vector α n) (Vector α m) (Vector α (n + m)) where - hAppend := append - -/-- Creates a vector from another with a provably equal length. -/ -@[inline] protected def cast (h : n = m) (v : Vector α n) : Vector α m := - ⟨v.toArray, by simp [*]⟩ - -/-- -Extracts the slice of a vector from indices `start` to `stop` (exclusive). If `start ≥ stop`, the -result is empty. If `stop` is greater than the size of the vector, the size is used instead. --/ -@[inline] def extract (v : Vector α n) (start stop : Nat) : Vector α (min stop n - start) := - ⟨v.toArray.extract start stop, by simp⟩ - -/-- Maps elements of a vector using the function `f`. -/ -@[inline] def map (f : α → β) (v : Vector α n) : Vector β n := - ⟨v.toArray.map f, by simp⟩ - -/-- Maps corresponding elements of two vectors of equal size using the function `f`. -/ -@[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n := - ⟨Array.zipWith a.toArray b.toArray f, by simp⟩ - -/-- The vector of length `n` whose `i`-th element is `f i`. -/ -@[inline] def ofFn (f : Fin n → α) : Vector α n := - ⟨Array.ofFn f, by simp⟩ - -/-- -Swap two elements of a vector using `Fin` indices. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def swap (v : Vector α n) (i j : Fin n) : Vector α n := - ⟨v.toArray.swap (Fin.cast v.size_toArray.symm i) (Fin.cast v.size_toArray.symm j), by simp⟩ - -/-- -Swap two elements of a vector using `Nat` indices. By default, the `get_elem_tactic` is used to -synthesize proofs that the indices are within bounds. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def swapN (v : Vector α n) (i j : Nat) - (hi : i < n := by get_elem_tactic) (hj : j < n := by get_elem_tactic) : Vector α n := - ⟨v.toArray.swapN i j (by simp_all) (by simp_all), by simp⟩ - -/-- -Swap two elements of a vector using `Nat` indices. Panics if either index is out of bounds. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def swap! (v : Vector α n) (i j : Nat) : Vector α n := - ⟨v.toArray.swap! i j, by simp⟩ - -/-- -Swaps an element of a vector with a given value using a `Fin` index. The original value is returned -along with the updated vector. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def swapAt (v : Vector α n) (i : Fin n) (x : α) : α × Vector α n := - let a := v.toArray.swapAt (Fin.cast v.size_toArray.symm i) x - ⟨a.fst, a.snd, by simp [a]⟩ - -/-- -Swaps an element of a vector with a given value using a `Nat` index. By default, the -`get_elem_tactic` is used to synthesise a proof that the index is within bounds. The original value -is returned along with the updated vector. - -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def swapAtN (v : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic) : - α × Vector α n := - let a := v.toArray.swapAtN i x (by simp_all) - ⟨a.fst, a.snd, by simp [a]⟩ +@[deprecated (since := "2024-11-25")] alias setN := set -/-- -Swaps an element of a vector with a given value using a `Nat` index. Panics if the index is out of -bounds. The original value is returned along with the updated vector. +@[deprecated (since := "2024-11-25")] alias setD := setIfInBounds -This will perform the update destructively provided that the vector has a reference count of 1. --/ -@[inline] def swapAt! (v : Vector α n) (i : Nat) (x : α) : α × Vector α n := - let a := v.toArray.swapAt! i x - ⟨a.fst, a.snd, by simp [a]⟩ +@[deprecated (since := "2024-11-24")] alias swapN := swap -/-- The vector `#v[0,1,2,...,n-1]`. -/ -@[inline] def range (n : Nat) : Vector Nat n := ⟨Array.range n, by simp⟩ +@[deprecated (since := "2024-11-24")] alias swap! := swapIfInBounds -/-- -Extract the first `m` elements of a vector. If `m` is greater than or equal to the size of the -vector then the vector is returned unchanged. --/ -@[inline] def take (v : Vector α n) (m : Nat) : Vector α (min m n) := - ⟨v.toArray.take m, by simp⟩ +@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt @[deprecated (since := "2024-10-22")] alias shrink := take -/-- -Deletes the first `m` elements of a vector. If `m` is greater than or equal to the size of the -vector then the empty vector is returned. --/ -@[inline] def drop (v : Vector α n) (m : Nat) : Vector α (n - m) := - ⟨v.toArray.extract m v.size, by simp⟩ - -/-- -Compares two vectors of the same size using a given boolean relation `r`. `isEqv v w r` returns -`true` if and only if `r v[i] w[i]` is true for all indices `i`. --/ -@[inline] def isEqv (v w : Vector α n) (r : α → α → Bool) : Bool := - Array.isEqvAux v.toArray w.toArray (by simp) r n (by simp) +@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx -instance [BEq α] : BEq (Vector α n) where - beq a b := isEqv a b (· == ·) +/-- Use `#v[]` instead. -/ +@[deprecated "Use `#v[]`." (since := "2024-11-27")] +def empty (α : Type u) : Vector α 0 := #v[] proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n) -/-- Reverse the elements of a vector. -/ -@[inline] def reverse (v : Vector α n) : Vector α n := - ⟨v.toArray.reverse, by simp⟩ - -/-- Delete an element of a vector using a `Fin` index. -/ -@[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) := - ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩ - -/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/ -@[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) := - if _ : i < n then - ⟨v.toArray.eraseIdx i, by simp [*]⟩ - else - have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩ - panic! "index out of bounds" - -/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/ -@[inline] def tail (v : Vector α n) : Vector α (n-1) := - if _ : 0 < n then - ⟨v.toArray.eraseIdx 0, by simp [*]⟩ - else - v.cast (by omega) - -/-- -Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to -synthesise a proof that the index is within bounds. --/ -@[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) : - Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩ - -/-- -Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the -no element of the index matches the given value. --/ -@[inline] def indexOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) := - (v.toArray.indexOf? x).map (Fin.cast v.size_toArray) - -/-- Returns `true` when `v` is a prefix of the vector `w`. -/ -@[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool := - v.toArray.isPrefixOf w.toArray - /-- Returns `true` when all elements of the vector are pairwise distinct using `==` for comparison. -/ diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean index 9a14c4a548..3cbcd854f2 100644 --- a/Batteries/Data/Vector/Lemmas.lean +++ b/Batteries/Data/Vector/Lemmas.lean @@ -10,8 +10,6 @@ import Batteries.Data.List.Lemmas import Batteries.Data.Array.Lemmas import Batteries.Tactic.Lint.Simp -namespace Batteries - namespace Vector theorem toArray_injective : ∀ {v w : Vector α n}, v.toArray = w.toArray → v = w @@ -45,13 +43,13 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a @[simp] theorem drop_mk (a : Array α) (h : a.size = n) (m) : (Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl +@[simp] theorem eraseIdx_mk (a : Array α) (h : a.size = n) (i) (h') : + (Vector.mk a h).eraseIdx i h' = Vector.mk (a.eraseIdx i) (by simp [h]) := rfl + @[simp] theorem eraseIdx!_mk (a : Array α) (h : a.size = n) (i) (hi : i < n) : - (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx! i) (by simp [h, hi]) := by + (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx i) (by simp [h, hi]) := by simp [Vector.eraseIdx!, hi] -@[simp] theorem feraseIdx_mk (a : Array α) (h : a.size = n) (i) : - (Vector.mk a h).feraseIdx i = Vector.mk (a.feraseIdx (i.cast h.symm)) (by simp [h]) := rfl - @[simp] theorem extract_mk (a : Array α) (h : a.size = n) (start stop) : (Vector.mk a h).extract start stop = Vector.mk (a.extract start stop) (by simp [h]) := rfl @@ -59,7 +57,7 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a (Vector.mk a h)[i] = a[i] := rfl @[simp] theorem get_mk (a : Array α) (h : a.size = n) (i) : - (Vector.mk a h).get i = a.get (i.cast h.symm) := rfl + (Vector.mk a h).get i = a[i] := rfl @[simp] theorem getD_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).getD i x = a.getD i x := rfl @@ -89,38 +87,35 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a @[simp] theorem reverse_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).reverse = Vector.mk a.reverse (by simp [h]) := rfl -@[simp] theorem set_mk (a : Array α) (h : a.size = n) (i x) : - (Vector.mk a h).set i x = Vector.mk (a.set (i.cast h.symm) x) (by simp [h]) := rfl +@[simp] theorem set_mk (a : Array α) (h : a.size = n) (i x w) : + (Vector.mk a h).set i x = Vector.mk (a.set i x) (by simp [h]) := rfl @[simp] theorem set!_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).set! i x = Vector.mk (a.set! i x) (by simp [h]) := rfl -@[simp] theorem setD_mk (a : Array α) (h : a.size = n) (i x) : - (Vector.mk a h).setD i x = Vector.mk (a.setD i x) (by simp [h]) := rfl +@[simp] theorem setIfInBounds_mk (a : Array α) (h : a.size = n) (i x) : + (Vector.mk a h).setIfInBounds i x = Vector.mk (a.setIfInBounds i x) (by simp [h]) := rfl -@[simp] theorem setN_mk (a : Array α) (h : a.size = n) (i x) (hi : i < n) : - (Vector.mk a h).setN i x = Vector.mk (a.setN i x) (by simp [h]) := rfl +@[deprecated (since := "2024-11-25")] alias setN_mk := set_mk -@[simp] theorem swap_mk (a : Array α) (h : a.size = n) (i j) : - (Vector.mk a h).swap i j = Vector.mk (a.swap (i.cast h.symm) (j.cast h.symm)) (by simp [h]) := +@[simp] theorem swap_mk (a : Array α) (h : a.size = n) (i j) (hi hj) : + (Vector.mk a h).swap i j = Vector.mk (a.swap i j) (by simp [h]) := rfl -@[simp] theorem swap!_mk (a : Array α) (h : a.size = n) (i j) : - (Vector.mk a h).swap! i j = Vector.mk (a.swap! i j) (by simp [h]) := rfl +@[simp] theorem swapIfInBounds_mk (a : Array α) (h : a.size = n) (i j) : + (Vector.mk a h).swapIfInBounds i j = Vector.mk (a.swapIfInBounds i j) (by simp [h]) := rfl -@[simp] theorem swapN_mk (a : Array α) (h : a.size = n) (i j) (hi : i < n) (hj : j < n) : - (Vector.mk a h).swapN i j = Vector.mk (a.swapN i j) (by simp [h]) := rfl +@[deprecated (since := "2024-11-25")] alias swapN_mk := swap_mk -@[simp] theorem swapAt_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt i x = - ((a.swapAt (i.cast h.symm) x).fst, Vector.mk (a.swapAt (i.cast h.symm) x).snd (by simp [h])) := +@[simp] theorem swapAt_mk (a : Array α) (h : a.size = n) (i x) (hi) : + (Vector.mk a h).swapAt i x = + ((a.swapAt i x).fst, Vector.mk (a.swapAt i x).snd (by simp [h])) := rfl @[simp] theorem swapAt!_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt! i x = ((a.swapAt! i x).fst, Vector.mk (a.swapAt! i x).snd (by simp [h])) := rfl -@[simp] theorem swapAtN_mk (a : Array α) (h : a.size = n) (i x) (hi : i < n) : - (Vector.mk a h).swapAtN i x = - ((a.swapAtN i x).fst, Vector.mk (a.swapAtN i x).snd (by simp [h])) := rfl +@[deprecated (since := "2024-11-25")] alias swapAtN_mk := swapAt_mk @[simp] theorem take_mk (a : Array α) (h : a.size = n) (m) : (Vector.mk a h).take m = Vector.mk (a.take m) (by simp [h]) := rfl @@ -141,20 +136,17 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a @[simp] theorem toArray_drop (a : Vector α n) (m) : (a.drop m).toArray = a.toArray.extract m a.size := rfl -@[simp] theorem toArray_empty : (Vector.empty (α := α)).toArray = #[] := rfl +@[simp] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl @[simp] theorem toArray_mkEmpty (cap) : (Vector.mkEmpty (α := α) cap).toArray = Array.mkEmpty cap := rfl +@[simp] theorem toArray_eraseIdx (a : Vector α n) (i) (h) : + (a.eraseIdx i h).toArray = a.toArray.eraseIdx i (by simp [h]) := rfl + @[simp] theorem toArray_eraseIdx! (a : Vector α n) (i) (hi : i < n) : (a.eraseIdx! i).toArray = a.toArray.eraseIdx! i := by - cases a; simp [hi] - -@[simp] theorem toArray_eraseIdxN (a : Vector α n) (i) (hi : i < n) : - (a.eraseIdxN i).toArray = a.toArray.eraseIdxN i (by simp [hi]) := rfl - -@[simp] theorem toArray_feraseIdx (a : Vector α n) (i) : - (a.feraseIdx i).toArray = a.toArray.feraseIdx (i.cast a.size_toArray.symm) := rfl + cases a; simp_all [Array.eraseIdx!] @[simp] theorem toArray_extract (a : Vector α n) (start stop) : (a.extract start stop).toArray = a.toArray.extract start stop := rfl @@ -172,42 +164,39 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a @[simp] theorem toArray_reverse (a : Vector α n) : a.reverse.toArray = a.toArray.reverse := rfl -@[simp] theorem toArray_set (a : Vector α n) (i x) : - (a.set i x).toArray = a.toArray.set (i.cast a.size_toArray.symm) x := rfl +@[simp] theorem toArray_set (a : Vector α n) (i x h) : + (a.set i x).toArray = a.toArray.set i x (by simpa using h):= rfl @[simp] theorem toArray_set! (a : Vector α n) (i x) : (a.set! i x).toArray = a.toArray.set! i x := rfl -@[simp] theorem toArray_setD (a : Vector α n) (i x) : - (a.setD i x).toArray = a.toArray.setD i x := rfl +@[simp] theorem toArray_setIfInBounds (a : Vector α n) (i x) : + (a.setIfInBounds i x).toArray = a.toArray.setIfInBounds i x := rfl -@[simp] theorem toArray_setN (a : Vector α n) (i x) (hi : i < n) : - (a.setN i x).toArray = a.toArray.setN i x (by simp [hi]) := rfl +@[deprecated (since := "2024-11-25")] alias toArray_setD := toArray_setIfInBounds +@[deprecated (since := "2024-11-25")] alias toArray_setN := toArray_set @[simp] theorem toArray_singleton (x : α) : (Vector.singleton x).toArray = #[x] := rfl -@[simp] theorem toArray_swap (a : Vector α n) (i j) : (a.swap i j).toArray = - a.toArray.swap (i.cast a.size_toArray.symm) (j.cast a.size_toArray.symm) := rfl +@[simp] theorem toArray_swap (a : Vector α n) (i j) (hi hj) : (a.swap i j).toArray = + a.toArray.swap i j (by simp [hi, hj]) (by simp [hi, hj]) := rfl -@[simp] theorem toArray_swap! (a : Vector α n) (i j) : - (a.swap! i j).toArray = a.toArray.swap! i j := rfl +@[simp] theorem toArray_swapIfInBounds (a : Vector α n) (i j) : + (a.swapIfInBounds i j).toArray = a.toArray.swapIfInBounds i j := rfl -@[simp] theorem toArray_swapN (a : Vector α n) (i j) (hi : i < n) (hj : j < n) : - (a.swapN i j).toArray = a.toArray.swapN i j (by simp [hi]) (by simp [hj]) := rfl +@[deprecated (since := "2024-11-25")] alias toArray_swap! := toArray_swapIfInBounds +@[deprecated (since := "2024-11-25")] alias toArray_swapN := toArray_swap -@[simp] theorem toArray_swapAt (a : Vector α n) (i x) : +@[simp] theorem toArray_swapAt (a : Vector α n) (i x h) : ((a.swapAt i x).fst, (a.swapAt i x).snd.toArray) = - ((a.toArray.swapAt (i.cast a.size_toArray.symm) x).fst, - (a.toArray.swapAt (i.cast a.size_toArray.symm) x).snd) := rfl + ((a.toArray.swapAt i x (by simpa using h)).fst, + (a.toArray.swapAt i x (by simpa using h)).snd) := rfl @[simp] theorem toArray_swapAt! (a : Vector α n) (i x) : ((a.swapAt! i x).fst, (a.swapAt! i x).snd.toArray) = ((a.toArray.swapAt! i x).fst, (a.toArray.swapAt! i x).snd) := rfl -@[simp] theorem toArray_swapAtN (a : Vector α n) (i x) (hi : i < n) : - ((a.swapAtN i x).fst, (a.swapAtN i x).snd.toArray) = - ((a.toArray.swapAtN i x (by simp [hi])).fst, - (a.toArray.swapAtN i x (by simp [hi])).snd) := rfl +@[deprecated (since := "2024-11-25")] alias toArray_swapAtN := toArray_swapAt @[simp] theorem toArray_take (a : Vector α n) (m) : (a.take m).toArray = a.toArray.take m := rfl @@ -256,22 +245,22 @@ defeq issues in the implicit size argument. /-! ### empty lemmas -/ -@[simp] theorem map_empty (f : α → β) : map f empty = empty := by - apply toArray_injective; simp +theorem map_empty (f : α → β) : map f #v[] = #v[] := by + simp -protected theorem eq_empty (v : Vector α 0) : v = empty := by +protected theorem eq_empty (v : Vector α 0) : v = #v[] := by apply toArray_injective apply Array.eq_empty_of_size_eq_zero v.2 /-! ### Decidable quantifiers. -/ theorem forall_zero_iff {P : Vector α 0 → Prop} : - (∀ v, P v) ↔ P .empty := by + (∀ v, P v) ↔ P #v[] := by constructor · intro h apply h · intro h v - obtain (rfl : v = .empty) := (by ext i h; simp at h) + obtain (rfl : v = #v[]) := (by ext i h; simp at h) apply h theorem forall_cons_iff {P : Vector α (n + 1) → Prop} : @@ -285,7 +274,7 @@ theorem forall_cons_iff {P : Vector α (n + 1) → Prop} : apply h instance instDecidableForallVectorZero (P : Vector α 0 → Prop) : - ∀ [Decidable (P .empty)], Decidable (∀ v, P v) + ∀ [Decidable (P #v[])], Decidable (∀ v, P v) | .isTrue h => .isTrue fun ⟨v, s⟩ => by obtain (rfl : v = .empty) := (by ext i h₁ h₂; exact s; cases h₂) exact h @@ -295,7 +284,7 @@ instance instDecidableForallVectorSucc (P : Vector α (n+1) → Prop) [Decidable (∀ (x : α) (v : Vector α n), P (v.push x))] : Decidable (∀ v, P v) := decidable_of_iff' (∀ x (v : Vector α n), P (v.push x)) forall_cons_iff -instance instDecidableExistsVectorZero (P : Vector α 0 → Prop) [Decidable (P .empty)] : +instance instDecidableExistsVectorZero (P : Vector α 0 → Prop) [Decidable (P #v[])] : Decidable (∃ v, P v) := decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not diff --git a/Batteries/Lean/Meta/Simp.lean b/Batteries/Lean/Meta/Simp.lean index 7ea81e87fa..085472c934 100644 --- a/Batteries/Lean/Meta/Simp.lean +++ b/Batteries/Lean/Meta/Simp.lean @@ -55,10 +55,8 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo pure simpTheorems let simprocs ← if simpOnly then pure {} else Simp.getSimprocs let congrTheorems ← Meta.getSimpCongrTheorems - let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) { - config := (← elabSimpConfig stx[1] (kind := kind)) - simpTheorems := #[simpTheorems], congrTheorems - } + let ctx ← Simp.mkContext (← elabSimpConfig stx[1] (kind := kind)) #[simpTheorems] congrTheorems + let r ← elabSimpArgs stx[4] (simprocs := #[simprocs]) ctx eraseLocal kind if !r.starArg || ignoreStarArg then return { r with dischargeWrapper } else @@ -73,7 +71,7 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo for h in hs do unless simpTheorems.isErased (.fvar h) do simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr - let ctx := { ctx with simpTheorems } + let ctx := ctx.setSimpTheorems simpTheorems return { ctx, simprocs, dischargeWrapper } diff --git a/Batteries/Lean/NameMap.lean b/Batteries/Lean/NameMap.lean deleted file mode 100644 index 0c6d341925..0000000000 --- a/Batteries/Lean/NameMap.lean +++ /dev/null @@ -1,40 +0,0 @@ -/- -Copyright (c) 2023 Jon Eugster. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jon Eugster --/ -import Lean.Data.NameMap - -/-! -# Additional functions on `Lean.NameMap`. - -We provide `NameMap.filter` and `NameMap.filterMap`. --/ - -namespace Lean.NameMap - -/-- -`filter f m` returns the `NameMap` consisting of all -"`key`/`val`"-pairs in `m` where `f key val` returns `true`. --/ -def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α := - m.fold process {} -where - /-- see `Lean.NameMap.filter` -/ - process (r : NameMap α) (n : Name) (i : α) := - if f n i then r.insert n i else r - -/-- -`filterMap f m` allows to filter a `NameMap` and simultaneously modify the filtered values. - -It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`. -The resulting entries with non-`none` value are collected to form the output `NameMap`. --/ -def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := - m.fold process {} -where - /-- see `Lean.NameMap.filterMap` -/ - process (r : NameMap β) (n : Name) (i : α) := - match f n i with - | none => r - | some b => r.insert n b diff --git a/Batteries/Tactic/Instances.lean b/Batteries/Tactic/Instances.lean index b243c4f153..7e7ea30d8f 100644 --- a/Batteries/Tactic/Instances.lean +++ b/Batteries/Tactic/Instances.lean @@ -35,7 +35,7 @@ elab (name := instancesCmd) tk:"#instances " stx:term : command => runTermElabM let some className ← isClass? type | throwErrorAt stx "type class instance expected{indentExpr type}" let globalInstances ← getGlobalInstancesIndex - let result ← globalInstances.getUnify type tcDtConfig + let result ← globalInstances.getUnify type let erasedInstances ← getErasedInstances let mut msgs := #[] for e in result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority do diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean index cb0369db5f..7f39e6759c 100644 --- a/Batteries/Tactic/Lint/Frontend.lean +++ b/Batteries/Tactic/Lint/Frontend.lean @@ -53,7 +53,7 @@ sanity check, lint, cleanup, command, tactic -/ namespace Batteries.Tactic.Lint -open Lean +open Lean Elab Command /-- Verbosity for the linter output. -/ inductive LintVerbosity @@ -89,9 +89,6 @@ def getChecks (slow : Bool) (runOnly : Option (List Name)) (runAlways : Option ( result := result.binInsert (·.name.lt ·.name) linter pure result --- Note: we have to use the same context as `runTermElabM` here so that the `simpNF` --- linter works the same as the `simp` tactic itself. See #671 -open private mkMetaContext from Lean.Elab.Command in /-- Runs all the specified linters on all the specified declarations in parallel, producing a list of results. @@ -107,7 +104,7 @@ def lintCore (decls : Array Name) (linters : Array NamedLinter) : (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do BaseIO.asTask do match ← withCurrHeartbeats (linter.test decl) - |>.run' mkMetaContext + |>.run' mkMetaContext -- We use the context used by `Command.liftTermElabM` |>.run' {options, fileName := "", fileMap := default} {env} |>.toBaseIO with | Except.ok msg? => pure msg? diff --git a/Batteries/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean index c6c0ad8828..3e83431dcc 100644 --- a/Batteries/Tactic/Lint/Simp.lean +++ b/Batteries/Tactic/Lint/Simp.lean @@ -108,7 +108,7 @@ see note [simp-normal form] for tips how to debug this. https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form" test := fun declName => do unless ← isSimpTheorem declName do return none - let ctx := { ← Simp.Context.mkDefault with config.decide := false } + let ctx ← Simp.Context.mkDefault checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do let isRfl ← isRflTheorem declName let ({ expr := lhs', proof? := prf1, .. }, prf1Stats) ← @@ -228,7 +228,7 @@ private def Expr.eqOrIff? : Expr → Option (Expr × Expr) noErrorsFound := "No commutativity lemma is marked simp." errorsFound := "COMMUTATIVITY LEMMA IS SIMP. Some commutativity lemmas are simp lemmas:" - test := fun declName => withReducible do + test := fun declName => withSimpGlobalConfig do withReducible do unless ← isSimpTheorem declName do return none let ty := (← getConstInfo declName).type forallTelescopeReducing ty fun _ ty' => do @@ -239,7 +239,7 @@ Some commutativity lemmas are simp lemmas:" unless ← isDefEq rhs lhs' do return none unless ← withNewMCtxDepth (isDefEq rhs lhs') do return none -- make sure that the discrimination tree will actually find this match (see #69) - if (← (← DiscrTree.empty.insert rhs () simpDtConfig).getMatch lhs' simpDtConfig).isEmpty then + if (← (← DiscrTree.empty.insert rhs ()).getMatch lhs').isEmpty then return none -- ensure that the second application makes progress: if ← isDefEq lhs' rhs' then return none diff --git a/Batteries/Tactic/Trans.lean b/Batteries/Tactic/Trans.lean index 7070c843ac..903796bc5d 100644 --- a/Batteries/Tactic/Trans.lean +++ b/Batteries/Tactic/Trans.lean @@ -24,9 +24,6 @@ open Lean Meta Elab initialize registerTraceClass `Tactic.trans -/-- Discrimation tree settings for the `trans` extension. -/ -def transExt.config : WhnfCoreConfig := {} - /-- Environment extension storing transitivity lemmas -/ initialize transExt : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ← @@ -49,7 +46,7 @@ initialize registerBuiltinAttribute { let some xyHyp := xs.pop.back? | fail let .app (.app _ _) _ ← inferType yzHyp | fail let .app (.app _ _) _ ← inferType xyHyp | fail - let key ← withReducible <| DiscrTree.mkPath rel transExt.config + let key ← withReducible <| DiscrTree.mkPath rel transExt.add (decl, key) kind } @@ -162,7 +159,7 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do let s ← saveState trace[Tactic.trans]"trying homogeneous case" let lemmas := - (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push ``Trans.simple + (← (transExt.getState (← getEnv)).getUnify rel).push ``Trans.simple for lem in lemmas do trace[Tactic.trans]"trying lemma {lem}" try @@ -182,7 +179,7 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do trace[Tactic.trans]"trying heterogeneous case" let t'? ← t?.mapM (elabTermWithHoles · none (← getMainTag)) let s ← saveState - for lem in (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push + for lem in (← (transExt.getState (← getEnv)).getUnify rel).push ``HEq.trans |>.push ``Trans.trans do try liftMetaTactic fun g => do diff --git a/Batteries/Util/Cache.lean b/Batteries/Util/Cache.lean index 866325df5a..de6beb846b 100644 --- a/Batteries/Util/Cache.lean +++ b/Batteries/Util/Cache.lean @@ -132,9 +132,6 @@ the second will store declarations from imports (and will hopefully be "read-onl -/ @[reducible] def DiscrTreeCache (α : Type) : Type := DeclCache (DiscrTree α × DiscrTree α) -/-- Discrimination tree settings for the `DiscrTreeCache`. -/ -def DiscrTreeCache.config : WhnfCoreConfig := {} - /-- Build a `DiscrTreeCache`, from a function that returns a collection of keys and values for each declaration. @@ -170,4 +167,4 @@ def DiscrTreeCache.getMatch (c : DiscrTreeCache α) (e : Expr) : MetaM (Array α let (locals, imports) ← c.get -- `DiscrTree.getMatch` returns results in batches, with more specific lemmas coming later. -- Hence we reverse this list, so we try out more specific lemmas earlier. - return (← locals.getMatch e config).reverse ++ (← imports.getMatch e config).reverse + return (← locals.getMatch e).reverse ++ (← imports.getMatch e).reverse diff --git a/BatteriesTest/alias.lean b/BatteriesTest/alias.lean index aa6fdfc720..4babc46b5e 100644 --- a/BatteriesTest/alias.lean +++ b/BatteriesTest/alias.lean @@ -11,16 +11,16 @@ theorem foo : 1 + 1 = 2 := rfl /-- doc string for `alias foo` -/ alias foo1 := foo -@[deprecated] alias foo2 := foo -@[deprecated foo2] alias _root_.B.foo3 := foo +@[deprecated (since := "2038-01-20")] alias foo2 := foo +@[deprecated foo2 (since := "2038-01-20")] alias _root_.B.foo3 := foo @[deprecated foo2 "it was never a good idea anyway" (since := "last thursday")] alias foo4 := foo example : 1 + 1 = 2 := foo1 -/-- warning: `A.foo2` has been deprecated, use `A.foo` instead -/ +/-- warning: `A.foo2` has been deprecated: use `A.foo` instead -/ #guard_msgs in example : 1 + 1 = 2 := foo2 -/-- warning: `B.foo3` has been deprecated, use `A.foo2` instead -/ +/-- warning: `B.foo3` has been deprecated: use `A.foo2` instead -/ #guard_msgs in example : 1 + 1 = 2 := B.foo3 -/-- warning: it was never a good idea anyway -/ +/-- warning: `A.foo4` has been deprecated: it was never a good idea anyway -/ #guard_msgs in example : 1 + 1 = 2 := foo4 /-- doc string for bar -/ @@ -87,7 +87,7 @@ unsafe alias barbaz3 := id /- iff version -/ -@[deprecated] alias ⟨mpId, mprId⟩ := Iff.rfl +@[deprecated (since := "2038-01-20")] alias ⟨mpId, mprId⟩ := Iff.rfl /-- info: A.mpId {a : Prop} : a → a -/ #guard_msgs in #check mpId @@ -95,9 +95,9 @@ unsafe alias barbaz3 := id #guard_msgs in #check mprId /-- -warning: `A.mpId` has been deprecated, use `Iff.rfl` instead +warning: `A.mpId` has been deprecated: use `Iff.rfl` instead --- -warning: `A.mprId` has been deprecated, use `Iff.rfl` instead +warning: `A.mprId` has been deprecated: use `Iff.rfl` instead -/ #guard_msgs in example := And.intro @mpId @mprId diff --git a/BatteriesTest/array.lean b/BatteriesTest/array.lean index 89f784293e..e94478ddb6 100644 --- a/BatteriesTest/array.lean +++ b/BatteriesTest/array.lean @@ -9,14 +9,14 @@ variable (v d : α) variable (g : i < (a.set! i v).size) variable (j_lt : j < (a.set! i v).size) -#check_simp (a.set! i v).get ⟨i, g⟩ ~> v -#check_simp (a.set! i v).get! i ~> (a.setD i v)[i]! +#check_simp (a.set! i v).get i g ~> v +#check_simp (a.set! i v).get! i ~> (a.setIfInBounds i v)[i]! #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d #check_simp (a.set! i v)[i] ~> v -- Checks with different index values. -#check_simp (a.set! i v)[j]'j_lt ~> (a.setD i v)[j]'_ -#check_simp (a.setD i v)[j]'j_lt !~> +#check_simp (a.set! i v)[j]'j_lt ~> (a.setIfInBounds i v)[j]'_ +#check_simp (a.setIfInBounds i v)[j]'j_lt !~> -- This doesn't work currently. -- It will be address in the comprehensive overhaul of array lemmas. diff --git a/BatteriesTest/help_cmd.lean b/BatteriesTest/help_cmd.lean index 23e3698b6d..f76f95c8c9 100644 --- a/BatteriesTest/help_cmd.lean +++ b/BatteriesTest/help_cmd.lean @@ -148,13 +148,12 @@ error: no syntax categories start with foobarbaz #help cats foobarbaz /-- -info: -category prec [Lean.Parser.Category.prec] +info: category prec [Lean.Parser.Category.prec] `prec` is a builtin syntax category for precedences. A precedence is a value that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is - parsed as `1 + (2 * 3)` because `*` has a higher pr0ecedence than `+`. + parsed as `1 + (2 * 3)` because `*` has a higher precedence than `+`. Higher numbers denote higher precedence. - In addition to literals like `37`, there are some special named priorities: + In addition to literals like `37`, there are some special named precedence levels: * `arg` for the precedence of function arguments * `max` for the highest precedence used in term parsers (not actually the maximum possible value) * `lead` for the precedence of terms not supposed to be used as arguments diff --git a/BatteriesTest/lint_simpNF.lean b/BatteriesTest/lint_simpNF.lean index c9c8f9d307..771e47c65a 100644 --- a/BatteriesTest/lint_simpNF.lean +++ b/BatteriesTest/lint_simpNF.lean @@ -38,4 +38,17 @@ theorem foo_eq_ite (n : Nat) : foo n = if n = n then n else 0 := by end Equiv +namespace List + +private axiom test_sorry : ∀ {α}, α + +@[simp] +theorem ofFn_getElem_eq_map {β : Type _} (l : List α) (f : α → β) : + ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := test_sorry + +example {β : Type _} (l : List α) (f : α → β) : + ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := by simp only [ofFn_getElem_eq_map] + +end List + #lint- only simpNF diff --git a/BatteriesTest/show_term.lean b/BatteriesTest/show_term.lean index 7288c369e9..1986fc06ee 100644 --- a/BatteriesTest/show_term.lean +++ b/BatteriesTest/show_term.lean @@ -11,7 +11,7 @@ Authors: Kim Morrison exact n exact 37 -/-- info: Try this: refine (?fst, ?snd) -/ +/-- info: Try this: refine (?_, ?_) -/ #guard_msgs in example : Nat × Nat := by show_term constructor repeat exact 42 diff --git a/lean-toolchain b/lean-toolchain index 1e70935f69..cf25a9816f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.15.0-rc1 From c07c8e232f87929fd228f0dabd5c6a0519a8c20f Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 2 Dec 2024 09:06:32 +0000 Subject: [PATCH 6/8] chore: bump to nightly-2024-12-02 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index cf25a9816f..58c3128c9a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 +leanprover/lean4:nightly-2024-12-02 From ea60bbab96985d5c5ea5b33399ed5d90fd8f3d62 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 3 Dec 2024 09:06:13 +0000 Subject: [PATCH 7/8] chore: bump to nightly-2024-12-03 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 58c3128c9a..e83d31caf9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-02 +leanprover/lean4:nightly-2024-12-03 From b07115b2b95a4765be565fb489e9786d1b53a931 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 3 Dec 2024 20:17:04 +1100 Subject: [PATCH 8/8] fix tests --- Batteries.lean | 1 - Batteries/Tactic/Where.lean | 83 ------------------------------------- BatteriesTest/where.lean | 7 +++- 3 files changed, 5 insertions(+), 86 deletions(-) delete mode 100644 Batteries/Tactic/Where.lean diff --git a/Batteries.lean b/Batteries.lean index 6c24d239bc..f39cd3f6d6 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -93,7 +93,6 @@ import Batteries.Tactic.ShowUnused import Batteries.Tactic.SqueezeScope import Batteries.Tactic.Trans import Batteries.Tactic.Unreachable -import Batteries.Tactic.Where import Batteries.Util.Cache import Batteries.Util.ExtendedBinder import Batteries.Util.LibraryNote diff --git a/Batteries/Tactic/Where.lean b/Batteries/Tactic/Where.lean deleted file mode 100644 index 3ef51a46c9..0000000000 --- a/Batteries/Tactic/Where.lean +++ /dev/null @@ -1,83 +0,0 @@ -/- -Copyright (c) 2023 Kyle Miller. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kyle Miller --/ -import Lean.Elab.Command - -/-! # `#where` command - -The `#where` command prints information about the current location, including the namespace, -active `open`, `universe`, and `variable` commands, and any options set with `set_option`. --/ - -open Lean Elab Command - -namespace Batteries.Tactic.Where - -private def describeOpenDecls (ds : List OpenDecl) : MessageData := Id.run do - let mut lines := #[] - let mut simple := #[] - let flush (lines simple : Array MessageData) : Array MessageData × Array MessageData := - if simple.isEmpty then - (lines, simple) - else - (lines.push ("open " ++ MessageData.joinSep simple.toList " "), #[]) - for d in ds do - match d with - | .explicit id decl => - (lines, simple) := flush lines simple - lines := lines.push m!"open {id} → {decl}" - | .simple ns ex => - if ex == [] then - simple := simple.push ns - else - (lines, simple) := flush lines simple - let ex' := ex.map toMessageData - lines := lines.push m!"open {ns} hiding {MessageData.joinSep ex' ", "}" - (lines, _) := flush lines simple - return MessageData.joinSep lines.toList "\n" - -private def describeOptions (opts : Options) : CommandElabM (Option MessageData) := do - let mut lines := #[] - let decls ← getOptionDecls - for (name, val) in opts do - match decls.find? name with - | some decl => - if val != decl.defValue then - lines := lines.push m!"set_option {name} {val}" - | none => - lines := lines.push m!"-- set_option {name} {val} -- unknown" - if lines.isEmpty then - return none - else - return MessageData.joinSep lines.toList "\n" - -/-- `#where` gives a description of the global scope at this point in the module. -This includes the namespace, `open` namespaces, `universe` and `variable` commands, -and options set with `set_option`. -/ -elab "#where" : command => do - let scope ← getScope - let mut msg : Array MessageData := #[] - -- Noncomputable - if scope.isNoncomputable then - msg := msg.push m!"noncomputable section" - -- Namespace - if !scope.currNamespace.isAnonymous then - msg := msg.push m!"namespace {scope.currNamespace}" - -- Open namespaces - if !scope.openDecls.isEmpty then - msg := msg.push <| describeOpenDecls scope.openDecls.reverse - -- Universe levels - if !scope.levelNames.isEmpty then - let levels := scope.levelNames.reverse.map toMessageData - msg := msg.push <| "universe " ++ MessageData.joinSep levels " " - -- Variables - if !scope.varDecls.isEmpty then - msg := msg.push <| ← `(command| variable $scope.varDecls*) - -- Options - if let some m ← describeOptions scope.opts then - msg := msg.push m - if msg.isEmpty then - msg := #[m!"-- In root namespace with initial scope"] - logInfo <| m!"{MessageData.joinSep msg.toList "\n\n"}" diff --git a/BatteriesTest/where.lean b/BatteriesTest/where.lean index a88f1ed8e5..eb715d6ad6 100644 --- a/BatteriesTest/where.lean +++ b/BatteriesTest/where.lean @@ -1,4 +1,7 @@ -import Batteries.Tactic.Where +-- None of these imports are really necessary, except to create namespace mentioned below. +import Lean.Elab.Term +import Lean.Elab.Command +import Batteries.Data.UnionFind.Basic -- Return to pristine state set_option linter.missingDocs false @@ -68,6 +71,6 @@ open Array renaming map -> listMap info: open Lean Lean.Meta open Lean.Elab hiding TermElabM open Lean.Elab.Command Batteries -open listMap → Array.map +open Array renaming map → listMap -/ #guard_msgs in #where