chore: adaptations for nightly-2024-08-08 (#910)

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Wojciech Nawrocki <[email protected]> Co-authored-by: L <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Kyle Miller <[email protected]>
leanprover-community · Aug 8, 2024 · 2fae043 · 2fae043
1 parent dc167d2
commit 2fae043
Show file tree

Hide file tree

Showing 13 changed files with 25 additions and 23 deletions.
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
@@ -11,6 +11,11 @@ import Batteries.Util.ProofWanted
 
 namespace Array
 
+theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
+    (arr.modify x f).get ⟨i, by simp [h]⟩ =
+    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+  simp [getElem_modify h]
+
 theorem forIn_eq_data_forIn [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.data b f := by

diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
@@ -224,7 +224,7 @@ private theorem pairwise_replaceF [BEq α] [PartialEquivBEq α]
   | cons a l ih =>
     simp only [List.pairwise_cons, List.replaceF] at H ⊢
     generalize e : cond .. = z; unfold cond at e; revert e
-    split <;> (intro h; subst h; simp)
+    split <;> (intro h; subst h; simp only [List.pairwise_cons])
     · next e => exact ⟨(H.1 · · ∘ PartialEquivBEq.trans e), H.2⟩
     · next e =>
       refine ⟨fun a h => ?_, ih H.2⟩

diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
@@ -307,7 +307,8 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     rw [findAux_s]; split <;> [rfl; skip]
     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 (by rwa [FindAux.size_eq])]
+    rw [rankD_eq' (by simp [FindAux.size_eq, h])]
+    rw [Array.get_modify (by rwa [FindAux.size_eq])]
     split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
   else
     simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]

diff --git a/Batteries/Lean/AttributeExtra.lean b/Batteries/Lean/AttributeExtra.lean
@@ -8,6 +8,8 @@ open Lean
 
 namespace Lean
 
+open Std
+
 /--
 `TagAttributeExtra` works around a limitation of `TagAttribute`, which is that definitions
 must be tagged in the same file that declares the definition.
@@ -94,7 +96,7 @@ or `none` if `decl` is not tagged.
 -/
 def getParam? [Inhabited α] (attr : ParametricAttributeExtra α)
     (env : Environment) (decl : Name) : Option α :=
-  attr.attr.getParam? env decl <|> attr.base.find? decl
+  attr.attr.getParam? env decl <|> attr.base[decl]?
 
 /-- Applies attribute `attr` to declaration `decl`, given a value for the parameter. -/
 def setParam (attr : ParametricAttributeExtra α)

diff --git a/Batteries/Lean/HashSet.lean b/Batteries/Lean/HashSet.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Lean.Data.HashSet
+import Std.Data.HashSet
 
-namespace Lean.HashSet
+namespace Std.HashSet
 
 variable [BEq α] [Hashable α]
 
@@ -66,10 +66,3 @@ def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
 @[inline]
 protected def ofArray [BEq α] [Hashable α] (as : Array α) : HashSet α :=
   HashSet.empty.insertMany as
-
-/--
-`O(n)`. Obtain a `HashSet` from a list.
--/
-@[inline]
-protected def ofList [BEq α] [Hashable α] (as : List α) : HashSet α :=
-  HashSet.empty.insertMany as
diff --git a/Batteries/Lean/Meta/Inaccessible.lean b/Batteries/Lean/Meta/Inaccessible.lean
@@ -5,7 +5,7 @@ Authors: Jannis Limperg
 -/
 import Lean.Meta.InferType
 
-open Lean Lean.Meta
+open Lean Lean.Meta Std
 
 /--
 Obtain the inaccessible fvars from the given local context. An fvar is

diff --git a/Batteries/Linter/UnnecessarySeqFocus.lean b/Batteries/Linter/UnnecessarySeqFocus.lean
@@ -8,7 +8,7 @@ import Lean.Linter.Util
 import Batteries.Lean.AttributeExtra
 
 namespace Batteries.Linter
-open Lean Elab Command Linter
+open Lean Elab Command Linter Std
 
 /--
 Enables the 'unnecessary `<;>`' linter. This will warn whenever the `<;>` tactic combinator
@@ -120,7 +120,7 @@ partial def markUsedTactics : InfoTree → M ω Unit
   | .node i c => do
     if let .ofTacticInfo i := i then
       if let some r := i.stx.getRange? true then
-      if let some entry := (← get).find? r then
+      if let some entry := (← get)[r]? then
       if i.stx.getKind == ``Parser.Tactic.«tactic_<;>_» then
         let isBad := do
           unless i.goalsBefore.length == 1 || !multigoalAttr.hasTag env i.stx[0].getKind do

diff --git a/Batteries/Linter/UnreachableTactic.lean b/Batteries/Linter/UnreachableTactic.lean
@@ -8,7 +8,7 @@ import Lean.Linter.Util
 import Batteries.Tactic.Unreachable
 
 namespace Batteries.Linter
-open Lean Elab Command Linter
+open Lean Elab Command Linter Std
 
 /--
 Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed.

diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean
@@ -126,7 +126,7 @@ def sortResults (results : HashMap Name α) : CoreM <| Array (Name × α) := do
   for (n, _) in results.toArray do
     if let some range ← findDeclarationRanges? n then
       key := key.insert n <| range.range.pos.line
-  pure $ results.toArray.qsort fun (a, _) (b, _) => key.findD a 0 < key.findD b 0
+  pure $ results.toArray.qsort fun (a, _) (b, _) => key.getD a 0 < key.getD b 0
 
 /-- Formats a linter warning as `#check` command with comment. -/
 def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Bool := false)
@@ -158,7 +158,7 @@ def groupedByFilename (results : HashMap Name MessageData) (useErrorFormat : Boo
       let mod ← findModuleOf? declName
       let mod := mod.getD (← getEnv).mainModule
       grouped.insert mod <$>
-        match grouped.find? mod with
+        match grouped[mod]? with
         | some (fp, msgs) => pure (fp, msgs.insert declName msg)
         | none => do
           let fp ← if useErrorFormat then
@@ -217,7 +217,7 @@ def getDeclsInPackage (pkg : Name) : CoreM (Array Name) := do
   let mut decls ← getDeclsInCurrModule
   let modules := env.header.moduleNames.map (pkg.isPrefixOf ·)
   return env.constants.map₁.fold (init := decls) fun decls declName _ =>
-    if modules[env.const2ModIdx[declName].get! (α := Nat)]! then
+    if modules[env.const2ModIdx[declName]?.get! (α := Nat)]! then
       decls.push declName
     else decls
 

diff --git a/Batteries/Tactic/Lint/Misc.lean b/Batteries/Tactic/Lint/Misc.lean
@@ -12,7 +12,7 @@ import Lean.Util.Recognizers
 import Lean.DocString
 import Batteries.Tactic.Lint.Basic
 
-open Lean Meta
+open Lean Meta Std
 
 namespace Std.Tactic.Lint
 
@@ -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) : Lean.HashSet (Array Name) :=
+private def univParamsGrouped (e : Expr) (nm₀ : Name) : HashSet (Array Name) :=
   runST fun σ => do
     let res ← ST.mkRef (σ := σ) {}
     e.forEach fun

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc1
+leanprover/lean4:nightly-2024-08-08
diff --git a/scripts/check_imports.lean b/scripts/check_imports.lean
@@ -70,7 +70,7 @@ def writeImportModule (path : FilePath) (imports : Array Name) : IO Unit := do
 /-- Check for imports and return true if warnings issued. -/
 def checkMissingImports (modName : Name) (modData : ModuleData) (reqImports : Array Name) :
     LogIO Bool := do
-  let names : HashSet Name := HashSet.ofArray (modData.imports.map (·.module))
+  let names : Std.HashSet Name := Std.HashSet.ofArray (modData.imports.map (·.module))
   let mut warned := false
   for req in reqImports do
     if !names.contains req then

diff --git a/test/where.lean b/test/where.lean
@@ -2,6 +2,7 @@ import Batteries.Tactic.Where
 
 -- Return to pristine state
 set_option linter.missingDocs false
+set_option internal.minimalSnapshots false
 
 /-- info: -- In root namespace with initial scope -/
 #guard_msgs in #where