From 8c79f5be06cbde71a707dc1d67a88671f3423e42 Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Wed, 25 Sep 2024 02:37:41 +0800 Subject: [PATCH 1/2] chore: use implicit arguments in iff lemmas also `(rfl : a = a)` => `rfl` --- Batteries/Logic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean index 03c82eb5ac..9d7d14a70d 100644 --- a/Batteries/Logic.lean +++ b/Batteries/Logic.lean @@ -79,25 +79,25 @@ theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' := ⟨heq_of_cast_eq _, fun h => by cases h; rfl⟩ theorem eqRec_eq_cast {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _} - (x : motive a (rfl : a = a)) {a' : α} (e : a = a') : + (x : motive a rfl) {a' : α} (e : a = a') : @Eq.rec α a motive x a' e = cast (e ▸ rfl) x := by subst e; rfl --Porting note: new theorem. More general version of `eqRec_heq` theorem eqRec_heq_self {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _} - (x : motive a (rfl : a = a)) {a' : α} (e : a = a') : + (x : motive a rfl) {a' : α} (e : a = a') : HEq (@Eq.rec α a motive x a' e) x := by subst e; rfl @[simp] theorem eqRec_heq_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _} - (x : motive a (rfl : a = a)) {a' : α} (e : a = a') {β : Sort _} (y : β) : + {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} : HEq (@Eq.rec α a motive x a' e) y ↔ HEq x y := by subst e; rfl @[simp] theorem heq_eqRec_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _} - (x : motive a (rfl : a = a)) {a' : α} (e : a = a') {β : Sort _} (y : β) : + {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} : HEq y (@Eq.rec α a motive x a' e) ↔ HEq y x := by subst e; rfl From ef2bc763ed3204680501d8f7da2b9f96bd89299d Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sat, 28 Sep 2024 12:35:51 -0400 Subject: [PATCH 2/2] chore: merge main and trigger Mathlib check --- .github/workflows/build.yml | 2 +- .github/workflows/test_mathlib.yml | 97 ++++++++++++++++++++++++++++ Batteries/CodeAction/Attr.lean | 2 +- Batteries/CodeAction/Basic.lean | 2 +- Batteries/CodeAction/Deprecated.lean | 4 +- Batteries/CodeAction/Misc.lean | 2 +- Batteries/Data/Array.lean | 1 + Batteries/Data/Array/Lemmas.lean | 57 +++++++++++++++- Batteries/Data/Array/OfFn.lean | 23 +++++++ Batteries/Data/Fin/Lemmas.lean | 4 +- Batteries/Data/HashMap/WF.lean | 4 +- Batteries/Data/List.lean | 1 + Batteries/Data/List/Basic.lean | 23 +------ Batteries/Data/List/Lemmas.lean | 72 +++++++++++++++++++++ Batteries/Data/List/OfFn.lean | 49 ++++++++++++++ Batteries/Tactic/Alias.lean | 2 +- Batteries/Tactic/Lint/Basic.lean | 2 +- Batteries/Tactic/Lint/Frontend.lean | 22 +++---- Batteries/Tactic/Lint/Misc.lean | 4 +- Batteries/Tactic/Lint/Simp.lean | 4 +- Batteries/Tactic/Lint/TypeClass.lean | 2 +- lakefile.lean | 7 +- scripts/runLinter.lean | 4 +- test/lintTC.lean | 2 +- test/lintsimp.lean | 2 +- 25 files changed, 334 insertions(+), 60 deletions(-) create mode 100644 .github/workflows/test_mathlib.yml create mode 100644 Batteries/Data/Array/OfFn.lean create mode 100644 Batteries/Data/List/OfFn.lean diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 15d72c6876..61af30e96e 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -20,7 +20,7 @@ jobs: name: build, test, and lint batteries uses: leanprover/lean-action@v1 with: - build-args: '-Kwerror' + build-args: '--wfail' - name: Check that all files are imported run: lake env lean scripts/check_imports.lean diff --git a/.github/workflows/test_mathlib.yml b/.github/workflows/test_mathlib.yml new file mode 100644 index 0000000000..15062cb521 --- /dev/null +++ b/.github/workflows/test_mathlib.yml @@ -0,0 +1,97 @@ +# Test Mathlib against a Batteries PR + +name: Test Mathlib + +on: + workflow_run: + workflows: [ci] + types: [completed] + +jobs: + on-success: + runs-on: ubuntu-latest + if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover-community/batteries' + steps: + - name: Retrieve information about the original workflow + uses: potiuk/get-workflow-origin@v1_1 + id: workflow-info + with: + token: ${{ secrets.GITHUB_TOKEN }} + sourceRunId: ${{ github.event.workflow_run.id }} + + - name: Checkout mathlib4 repository + if: steps.workflow-info.outputs.pullRequestNumber != '' + uses: actions/checkout@v4 + with: + repository: leanprover-community/mathlib4 + token: ${{ secrets.MATHLIB4_BOT }} + ref: master + fetch-depth: 0 + + - name: install elan + run: | + set -o pipefail + curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y --default-toolchain none + echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" + + - name: Retrieve PR information + if: steps.workflow-info.outputs.pullRequestNumber != '' + id: pr-info + uses: actions/github-script@v6 + env: + PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }} + with: + script: | + const prNumber = process.env.PR_NUMBER; + const { data: pr } = await github.rest.pulls.get({ + owner: context.repo.owner, + repo: context.repo.repo, + pull_number: prNumber + }); + core.exportVariable('HEAD_REPO', pr.head.repo.full_name); + core.exportVariable('HEAD_BRANCH', pr.head.ref); + + - name: Check if tag exists + if: steps.workflow-info.outputs.pullRequestNumber != '' + id: check_mathlib_tag + env: + PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }} + HEAD_REPO: ${{ env.HEAD_REPO }} + HEAD_BRANCH: ${{ env.HEAD_BRANCH }} + run: | + git config user.name "leanprover-community-mathlib4-bot" + git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" + + echo "PR info: $HEAD_REPO $HEAD_BRANCH" + + BASE=master + echo "Using base tag: $BASE" + + EXISTS="$(git ls-remote --heads origin batteries-pr-testing-$PR_NUMBER | wc -l)" + echo "Branch exists: $EXISTS" + if [ "$EXISTS" = "0" ]; then + echo "Branch does not exist, creating it." + git switch -c batteries-pr-testing-$PR_NUMBER "$BASE" + + # Use the fork and branch name to modify the lakefile.lean + sed -i "s,require \"leanprover-community\" / \"batteries\" @ git \".\+\",require \"leanprover-community\" / \"batteries\" from git \"https://github.com/$HEAD_REPO\" @ \"$HEAD_BRANCH\",g" lakefile.lean + + lake update batteries + git add lakefile.lean lake-manifest.json + git commit -m "Update Batteries branch for testing https://github.com/leanprover-community/batteries/pull/$PR_NUMBER" + else + echo "Branch already exists, merging $BASE and bumping Batteries." + git switch batteries-pr-testing-$PR_NUMBER + git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories + lake update batteries + git add lake-manifest.json + git commit --allow-empty -m "Trigger CI for https://github.com/leanprover-community/batteries/pull/$PR_NUMBER" + fi + + - name: Push changes + if: steps.workflow-info.outputs.pullRequestNumber != '' + env: + PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }} + run: | + git push origin batteries-pr-testing-$PR_NUMBER diff --git a/Batteries/CodeAction/Attr.lean b/Batteries/CodeAction/Attr.lean index 79802d6932..308c4c7ad3 100644 --- a/Batteries/CodeAction/Attr.lean +++ b/Batteries/CodeAction/Attr.lean @@ -14,7 +14,7 @@ import Lean.Server.CodeActions.Basic * Attribute `@[tactic_code_action]` collects code actions which will be called on each occurrence of a tactic. -/ -namespace Std.CodeAction +namespace Batteries.CodeAction open Lean Elab Server Lsp RequestM Snapshots diff --git a/Batteries/CodeAction/Basic.lean b/Batteries/CodeAction/Basic.lean index 378f6aa00d..120de7eb05 100644 --- a/Batteries/CodeAction/Basic.lean +++ b/Batteries/CodeAction/Basic.lean @@ -19,7 +19,7 @@ on each occurrence of a hole (`_`, `?_` or `sorry`). attempt to use this code action provider when browsing the `Batteries.CodeAction.Hole.Attr` file itself.) -/ -namespace Std.CodeAction +namespace Batteries.CodeAction open Lean Elab Server RequestM CodeAction diff --git a/Batteries/CodeAction/Deprecated.lean b/Batteries/CodeAction/Deprecated.lean index 33d1d75243..30745d161d 100644 --- a/Batteries/CodeAction/Deprecated.lean +++ b/Batteries/CodeAction/Deprecated.lean @@ -14,7 +14,9 @@ This is an opt-in mechanism for making machine-applicable `@[deprecated]` defini whenever the deprecation lint also fires, allowing the user to replace the usage of the deprecated constant. -/ -namespace Std + +namespace Batteries + open Lean Elab Server Lsp RequestM CodeAction /-- An environment extension for identifying `@[deprecated]` definitions which can be auto-fixed -/ diff --git a/Batteries/CodeAction/Misc.lean b/Batteries/CodeAction/Misc.lean index 0bea77ff55..4ad0a8099d 100644 --- a/Batteries/CodeAction/Misc.lean +++ b/Batteries/CodeAction/Misc.lean @@ -15,7 +15,7 @@ import Lean.Server.CodeActions.Provider This declares some basic tactic code actions, using the `@[tactic_code_action]` API. -/ -namespace Std.CodeAction +namespace Batteries.CodeAction open Lean Meta Elab Server RequestM CodeAction diff --git a/Batteries/Data/Array.lean b/Batteries/Data/Array.lean index 4d41e75755..1f500b700a 100644 --- a/Batteries/Data/Array.lean +++ b/Batteries/Data/Array.lean @@ -4,4 +4,5 @@ import Batteries.Data.Array.Lemmas import Batteries.Data.Array.Match import Batteries.Data.Array.Merge import Batteries.Data.Array.Monadic +import Batteries.Data.Array.OfFn import Batteries.Data.Array.Pairwise diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean index 02293aa349..d384a334ab 100644 --- a/Batteries/Data/Array/Lemmas.lean +++ b/Batteries/Data/Array/Lemmas.lean @@ -115,9 +115,64 @@ theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L · rintro ⟨s, h₁, h₂⟩ refine ⟨s.data, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩ +/-! ### indexOf? -/ + +theorem indexOf?_data [BEq α] {a : α} {l : Array α} : + l.data.indexOf? a = (l.indexOf? a).map Fin.val := by + simpa using aux l 0 +where + aux (l : Array α) (i : Nat) : + ((l.data.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by + rw [indexOfAux] + if h : i < l.size then + rw [List.drop_eq_getElem_cons h, ←getElem_eq_data_getElem, List.indexOf?_cons] + if h' : l[i] == a then + simp [h, h'] + else + simp [h, h', ←aux l (i+1), Function.comp_def, ←Nat.add_assoc, Nat.add_right_comm] + else + have h' : l.size ≤ i := Nat.le_of_not_lt h + simp [h, List.drop_of_length_le h', List.indexOf?] + termination_by l.size - i + /-! ### erase -/ -@[simp] proof_wanted data_erase [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a +theorem eraseIdx_data_swap {l : Array α} (i : Nat) (lt : i + 1 < size l) : + (l.swap ⟨i+1, lt⟩ ⟨i, Nat.lt_of_succ_lt lt⟩).data.eraseIdx (i+1) = l.data.eraseIdx i := by + let ⟨xs⟩ := l + induction i generalizing xs <;> let x₀::x₁::xs := xs + case zero => simp [swap, get] + case succ i ih _ => + have lt' := Nat.lt_of_succ_lt_succ lt + have : (swap ⟨x₀::x₁::xs⟩ ⟨i.succ + 1, lt⟩ ⟨i.succ, Nat.lt_of_succ_lt lt⟩).data + = x₀::(swap ⟨x₁::xs⟩ ⟨i + 1, lt'⟩ ⟨i, Nat.lt_of_succ_lt lt'⟩).data := by + simp [swap_def, getElem_eq_data_getElem] + simp [this, ih] + +@[simp] theorem data_feraseIdx {l : Array α} (i : Fin l.size) : + (l.feraseIdx i).data = l.data.eraseIdx i := by + induction l, i using feraseIdx.induct with + | @case1 a i lt a' i' ih => + rw [feraseIdx] + simp [lt, ih, a', eraseIdx_data_swap i lt] + | case2 a i lt => + have : i + 1 ≥ a.size := Nat.ge_of_not_lt lt + have last : i + 1 = a.size := Nat.le_antisymm i.is_lt this + simp [feraseIdx, lt, List.dropLast_eq_eraseIdx last] + +@[simp] theorem data_erase [BEq α] (l : Array α) (a : α) : (l.erase a).data = l.data.erase a := by + match h : indexOf? l a with + | none => + simp only [erase, h] + apply Eq.symm + rw [List.erase_eq_self_iff_forall_bne, ←List.indexOf?_eq_none_iff, indexOf?_data, + h, Option.map_none'] + | some i => + simp only [erase, h] + rw [data_feraseIdx, ←List.eraseIdx_indexOf_eq_erase] + congr + rw [List.indexOf_eq_indexOf?, indexOf?_data] + simp [h] /-! ### shrink -/ diff --git a/Batteries/Data/Array/OfFn.lean b/Batteries/Data/Array/OfFn.lean new file mode 100644 index 0000000000..a5d3bc78bc --- /dev/null +++ b/Batteries/Data/Array/OfFn.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Batteries.Data.List.OfFn + +open List + +namespace Array + +/-! ### ofFn -/ + +@[simp] +theorem data_ofFn (f : Fin n → α) : (ofFn f).data = List.ofFn f := by + ext1 + simp only [getElem?_eq, data_length, size_ofFn, length_ofFn, getElem_ofFn] + split + · rw [← getElem_eq_data_getElem] + simp + · rfl + +end Array diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index bc1eb0d2c9..5ddde152de 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -40,14 +40,14 @@ theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by rw [list_succ] induction n with - | zero => rfl + | zero => simp [last] | succ n ih => rw [list_succ, List.map_cons castSucc, ih] simp [Function.comp_def, succ_castSucc] theorem list_reverse (n) : (list n).reverse = (list n).map rev := by induction n with - | zero => rfl + | zero => simp [last] | succ n ih => conv => lhs; rw [list_succ_last] conv => rhs; rw [list_succ] diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean index 9f69994638..258723a89b 100644 --- a/Batteries/Data/HashMap/WF.lean +++ b/Batteries/Data/HashMap/WF.lean @@ -94,12 +94,14 @@ where .sum (source.data.map (·.toList.length)) + target.size := by unfold expand.go; split · next H => - refine (go (i+1) _ _ fun j hj => ?a).trans ?b <;> simp + refine (go (i+1) _ _ fun j hj => ?a).trans ?b · case a => + simp only [Array.data_length, Array.data_set] simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]; split · cases source.data[j]? <;> rfl · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H)) · case b => + simp only [Array.data_length, Array.data_set, Array.get_eq_getElem, AssocList.foldl_eq] refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; eq ▸ ?_ rw [h₁] simp only [Buckets.size_eq, List.map_append, List.map_cons, AssocList.toList, diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean index 998160b904..f93f90a6c2 100644 --- a/Batteries/Data/List.lean +++ b/Batteries/Data/List.lean @@ -3,5 +3,6 @@ import Batteries.Data.List.Count import Batteries.Data.List.EraseIdx import Batteries.Data.List.Init.Lemmas import Batteries.Data.List.Lemmas +import Batteries.Data.List.OfFn import Batteries.Data.List.Pairwise import Batteries.Data.List.Perm diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index 963920017c..c2d76ed0e6 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -601,28 +601,7 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) : ofFn f = [f 0, f 1, ... , f (n - 1)] ``` -/ -def ofFn {n} (f : Fin n → α) : List α := go n 0 rfl where - /-- Auxiliary for `List.ofFn`. `ofFn.go f i j _ = [f j, ..., f (n - 1)]`. -/ - -- This used to be defined via `Array.ofFn` but mathlib relies on reducing it, - -- so we use a structurally recursive definition here. - go : (i j : Nat) → (h : i + j = n) → List α - | 0, _, _ => [] - | i+1, j, h => f ⟨j, by omega⟩ :: go i (j+1) (Nat.add_right_comm .. ▸ h :) - -/-- Tail-recursive version of `ofFn`. -/ -@[inline] def ofFnTR {n} (f : Fin n → α) : List α := go n (Nat.le_refl _) [] where - /-- Auxiliary for `List.ofFnTR`. `ofFnTR.go f i _ acc = f 0 :: ... :: f (i - 1) :: acc`. -/ - go : (i : Nat) → (h : i ≤ n) → List α → List α - | 0, _, acc => acc - | i+1, h, acc => go i (Nat.le_of_lt h) (f ⟨i, h⟩ :: acc) - -@[csimp] theorem ofFn_eq_ofFnTR : @ofFn = @ofFnTR := by - funext α n f; simp [ofFnTR] - let rec go (i j h h') : ofFnTR.go f j h' (ofFn.go f i j h) = ofFn f := by - unfold ofFnTR.go; split - · subst h; rfl - · next l j h' => exact go (i+1) j ((Nat.succ_add ..).trans h) (Nat.le_of_lt h') - exact (go 0 n (Nat.zero_add _) (Nat.le_refl _)).symm +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 α := diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index a68d820a52..5df9338026 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -17,11 +17,45 @@ open Nat @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by simp [Array.mem_def] +/-! ### toArray-/ + +@[simp] theorem size_toArrayAux (l : List α) (r : Array α) : + (l.toArrayAux r).size = r.size + l.length := by + induction l generalizing r with + | nil => simp [toArrayAux] + | cons a l ih => + simp [ih, List.toArrayAux] + omega + +@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : + (Array.mk xs)[i] = xs[i] := rfl + +@[simp] theorem getElem_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) : + l.toArray[i] = l[i]'(by simpa using h) := by + rw [Array.getElem_eq_data_getElem] + simp + /-! ### next? -/ @[simp] theorem next?_nil : @next? α [] = none := rfl @[simp] theorem next?_cons (a l) : @next? α (a :: l) = some (a, l) := rfl +/-! ### dropLast -/ + +theorem dropLast_eq_eraseIdx {xs : List α} {i : Nat} (last_idx : i + 1 = xs.length) : + xs.dropLast = List.eraseIdx xs i := by + induction i generalizing xs with + | zero => + let [x] := xs + rfl + | succ n ih => + let x::xs := xs + simp at last_idx + rw [dropLast, eraseIdx] + congr + exact ih last_idx + exact fun _ => nomatch xs + /-! ### get? -/ @[deprecated getElem_eq_iff (since := "2024-06-12")] @@ -210,6 +244,23 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) : @[deprecated (since := "2024-04-22")] alias sublist.erase := Sublist.erase +theorem erase_eq_self_iff_forall_bne [BEq α] (a : α) (xs : List α) : + xs.erase a = xs ↔ ∀ (x : α), x ∈ xs → ¬x == a := by + rw [erase_eq_eraseP', eraseP_eq_self_iff] + +/-! ### findIdx? -/ + +theorem findIdx_eq_findIdx? (p : α → Bool) (l : List α) : + l.findIdx p = (match l.findIdx? p with | some i => i | none => l.length) := by + induction l with + | nil => rfl + | cons x xs ih => + rw [findIdx_cons, findIdx?_cons] + if h : p x then + simp [h] + else + cases h' : findIdx? p xs <;> simp [h, h', ih] + /-! ### replaceF -/ theorem replaceF_nil : [].replaceF p = [] := rfl @@ -553,6 +604,14 @@ theorem indexesOf_cons [BEq α] : (x :: xs : List α).indexesOf y = bif x == y then 0 :: (xs.indexesOf y).map (· + 1) else (xs.indexesOf y).map (· + 1) := by simp [indexesOf, findIdxs_cons] +@[simp] theorem eraseIdx_indexOf_eq_erase [BEq α] (a : α) (l : List α) : + l.eraseIdx (l.indexOf a) = l.erase a := by + induction l with + | nil => rfl + | cons x xs ih => + rw [List.erase, indexOf_cons] + cases x == a <;> simp [ih] + theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) : xs.indexOf x ∈ xs.indexesOf x := by induction xs with @@ -567,6 +626,19 @@ theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ specialize ih m simpa +@[simp] theorem indexOf?_nil [BEq α] : ([] : List α).indexOf? x = none := rfl +theorem indexOf?_cons [BEq α] : + (x :: xs : List α).indexOf? y = if x == y then some 0 else (xs.indexOf? y).map Nat.succ := by + simp [indexOf?] + +theorem indexOf?_eq_none_iff [BEq α] {a : α} {l : List α} : + l.indexOf? a = none ↔ ∀ x ∈ l, ¬x == a := by + simp [indexOf?, findIdx?_eq_none_iff] + +theorem indexOf_eq_indexOf? [BEq α] (a : α) (l : List α) : + l.indexOf a = (match l.indexOf? a with | some i => i | none => l.length) := by + simp [indexOf, indexOf?, findIdx_eq_findIdx?] + /-! ### insertP -/ theorem insertP_loop (a : α) (l r : List α) : diff --git a/Batteries/Data/List/OfFn.lean b/Batteries/Data/List/OfFn.lean new file mode 100644 index 0000000000..93214cc99b --- /dev/null +++ b/Batteries/Data/List/OfFn.lean @@ -0,0 +1,49 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Batteries.Data.List.Lemmas +import Batteries.Data.Fin.Lemmas + +/-! +# Theorems about `List.ofFn` +-/ + +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/Tactic/Alias.lean b/Batteries/Tactic/Alias.lean index 07b91dc76e..471dfd883a 100644 --- a/Batteries/Tactic/Alias.lean +++ b/Batteries/Tactic/Alias.lean @@ -19,7 +19,7 @@ an iff theorem. namespace Batteries.Tactic.Alias -open Lean Elab Parser.Command Std +open Lean Elab Parser.Command /-- An alias can be in one of three forms -/ inductive AliasInfo where diff --git a/Batteries/Tactic/Lint/Basic.lean b/Batteries/Tactic/Lint/Basic.lean index 948bab5456..a0fceb7fa2 100644 --- a/Batteries/Tactic/Lint/Basic.lean +++ b/Batteries/Tactic/Lint/Basic.lean @@ -9,7 +9,7 @@ import Lean.Elab.Exception open Lean Meta -namespace Std.Tactic.Lint +namespace Batteries.Tactic.Lint /-! # Basic linter types and attributes diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean index 27ff3bf3b2..cb0369db5f 100644 --- a/Batteries/Tactic/Lint/Frontend.lean +++ b/Batteries/Tactic/Lint/Frontend.lean @@ -39,7 +39,7 @@ You can append `only name1 name2 ...` to any command to run a subset of linters, You can add custom linters by defining a term of type `Linter` with the `@[env_linter]` attribute. -A linter defined with the name `Std.Tactic.Lint.myNewCheck` can be run with `#lint myNewCheck` +A linter defined with the name `Batteries.Tactic.Lint.myNewCheck` can be run with `#lint myNewCheck` or `#lint only myNewCheck`. If you add the attribute `@[env_linter disabled]` to `linter.myNewCheck` it will be registered, but not run by default. @@ -52,8 +52,8 @@ omits it from only the specified linter checks. sanity check, lint, cleanup, command, tactic -/ -namespace Std.Tactic.Lint -open Lean Std +namespace Batteries.Tactic.Lint +open Lean /-- Verbosity for the linter output. -/ inductive LintVerbosity @@ -97,7 +97,7 @@ Runs all the specified linters on all the specified declarations in parallel, producing a list of results. -/ def lintCore (decls : Array Name) (linters : Array NamedLinter) : - CoreM (Array (NamedLinter × HashMap Name MessageData)) := do + CoreM (Array (NamedLinter × Std.HashMap Name MessageData)) := do let env ← getEnv let options ← getOptions -- TODO: sanitize options? @@ -114,15 +114,15 @@ def lintCore (decls : Array Name) (linters : Array NamedLinter) : | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}" tasks.mapM fun (linter, decls) => do - let mut msgs : HashMap Name MessageData := {} + let mut msgs : Std.HashMap Name MessageData := {} for (declName, msg?) in decls do if let some msg := msg?.get then msgs := msgs.insert declName msg pure (linter, msgs) /-- Sorts a map with declaration keys as names by line number. -/ -def sortResults (results : HashMap Name α) : CoreM <| Array (Name × α) := do - let mut key : HashMap Name Nat := {} +def sortResults (results : Std.HashMap Name α) : CoreM <| Array (Name × α) := do + let mut key : Std.HashMap Name Nat := {} for (n, _) in results.toArray do if let some range ← findDeclarationRanges? n then key := key.insert n <| range.range.pos.line @@ -140,7 +140,7 @@ def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Boo addMessageContextPartial m!"#check {← mkConstWithLevelParams declName} /- {warning} -/" /-- Formats a map of linter warnings using `print_warning`, sorted by line number. -/ -def printWarnings (results : HashMap Name MessageData) (filePath : System.FilePath := default) +def printWarnings (results : Std.HashMap Name MessageData) (filePath : System.FilePath := default) (useErrorFormat : Bool := false) : CoreM MessageData := do (MessageData.joinSep ·.toList Format.line) <$> (← sortResults results).mapM fun (declName, warning) => @@ -150,10 +150,10 @@ def printWarnings (results : HashMap Name MessageData) (filePath : System.FilePa Formats a map of linter warnings grouped by filename with `-- filename` comments. The first `drop_fn_chars` characters are stripped from the filename. -/ -def groupedByFilename (results : HashMap Name MessageData) (useErrorFormat : Bool := false) : +def groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) : CoreM MessageData := do let sp ← if useErrorFormat then initSrcSearchPath ["."] else pure {} - let grouped : HashMap Name (System.FilePath × HashMap Name MessageData) ← + let grouped : Std.HashMap Name (System.FilePath × Std.HashMap Name MessageData) ← results.foldM (init := {}) fun grouped declName msg => do let mod ← findModuleOf? declName let mod := mod.getD (← getEnv).mainModule @@ -174,7 +174,7 @@ def groupedByFilename (results : HashMap Name MessageData) (useErrorFormat : Boo Formats the linter results as Lean code with comments and `#check` commands. -/ def formatLinterResults - (results : Array (NamedLinter × HashMap Name MessageData)) + (results : Array (NamedLinter × Std.HashMap Name MessageData)) (decls : Array Name) (groupByFilename : Bool) (whereDesc : String) (runSlowLinters : Bool) diff --git a/Batteries/Tactic/Lint/Misc.lean b/Batteries/Tactic/Lint/Misc.lean index a0aa8bc884..075c139aea 100644 --- a/Batteries/Tactic/Lint/Misc.lean +++ b/Batteries/Tactic/Lint/Misc.lean @@ -14,7 +14,7 @@ import Batteries.Tactic.Lint.Basic open Lean Meta Std -namespace Std.Tactic.Lint +namespace Batteries.Tactic.Lint /-! # Various linters @@ -143,7 +143,7 @@ In pseudo-mathematical form, this returns `{{p : parameter | p ∈ u} | (u : lev FIXME: We use `Array Name` instead of `HashSet Name`, since `HashSet` does not have an equality instance. It will ignore `nm₀.proof_i` declarations. -/ -private def univParamsGrouped (e : Expr) (nm₀ : Name) : HashSet (Array Name) := +private def univParamsGrouped (e : Expr) (nm₀ : Name) : Std.HashSet (Array Name) := runST fun σ => do let res ← ST.mkRef (σ := σ) {} e.forEach fun diff --git a/Batteries/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean index 9196e4ab74..c6c0ad8828 100644 --- a/Batteries/Tactic/Lint/Simp.lean +++ b/Batteries/Tactic/Lint/Simp.lean @@ -9,7 +9,7 @@ import Batteries.Tactic.OpenPrivate import Batteries.Util.LibraryNote open Lean Meta -namespace Std.Tactic.Lint +namespace Batteries.Tactic.Lint /-! # Linter for simplification lemmas @@ -86,8 +86,6 @@ where | Trie.node vs children => children.foldl (init := arr ++ vs) fun arr (_, child) => trieElements arr child -open Std - /-- Add message `msg` to any errors thrown inside `k`. -/ def decorateError (msg : MessageData) (k : MetaM α) : MetaM α := do try k catch e => throw (.error e.getRef m!"{msg}\n{e.toMessageData}") diff --git a/Batteries/Tactic/Lint/TypeClass.lean b/Batteries/Tactic/Lint/TypeClass.lean index e6cf632f87..a025777d18 100644 --- a/Batteries/Tactic/Lint/TypeClass.lean +++ b/Batteries/Tactic/Lint/TypeClass.lean @@ -6,7 +6,7 @@ Authors: Gabriel Ebner import Lean.Meta.Instances import Batteries.Tactic.Lint.Basic -namespace Std.Tactic.Lint +namespace Batteries.Tactic.Lint open Lean Meta /-- diff --git a/lakefile.lean b/lakefile.lean index e55e8b2639..7c287c4c95 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,13 +2,8 @@ import Lake open Lake DSL -macro "opt_arg?" x:ident v:term : term => `(if get_config? $x |>.isSome then $v else default) - package batteries where - moreLeanArgs := opt_arg? werror #["-DwarningAsError=true"] - leanOptions := - #[⟨`linter.missingDocs, true⟩] ++ - opt_arg? disable_new_compiler #[⟨`compiler.enableNew, false⟩] + leanOptions := #[⟨`linter.missingDocs, true⟩] @[default_target] lean_lib Batteries diff --git a/scripts/runLinter.lean b/scripts/runLinter.lean index 3fab25f834..89976f0e47 100644 --- a/scripts/runLinter.lean +++ b/scripts/runLinter.lean @@ -2,7 +2,7 @@ import Lean.Util.SearchPath import Batteries.Tactic.Lint import Batteries.Data.Array.Basic -open Lean Core Elab Command Std.Tactic.Lint +open Lean Core Elab Command Batteries.Tactic.Lint open System (FilePath) /-- The list of `nolints` pulled from the `nolints.json` file -/ @@ -15,7 +15,7 @@ def readJsonFile (α) [FromJson α] (path : System.FilePath) : IO α := do /-- Serialize the given value `a : α` to the file as JSON. -/ def writeJsonFile [ToJson α] (path : System.FilePath) (a : α) : IO Unit := - IO.FS.writeFile path <| toJson a |>.pretty + IO.FS.writeFile path <| toJson a |>.pretty.push '\n' /-- Usage: `runLinter [--update] [Batteries.Data.Nat.Basic]` diff --git a/test/lintTC.lean b/test/lintTC.lean index 1f0ade6987..2a5f6f2640 100644 --- a/test/lintTC.lean +++ b/test/lintTC.lean @@ -1,7 +1,7 @@ import Batteries.Tactic.Lint.TypeClass import Lean.Elab.Command -open Std.Tactic.Lint +open Batteries.Tactic.Lint namespace A diff --git a/test/lintsimp.lean b/test/lintsimp.lean index 0950578665..ad2a589247 100644 --- a/test/lintsimp.lean +++ b/test/lintsimp.lean @@ -1,6 +1,6 @@ import Batteries.Tactic.Lint -open Std.Tactic.Lint +open Batteries.Tactic.Lint set_option linter.missingDocs false def f : Nat := 0