chore: adaptations for nightly-2024-11-18 (#1053)

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>

Batteries/Data/Array/Lemmas.lean

@@ -93,12 +93,6 @@ theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 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) :

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

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?

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
+    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

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

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

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-14
+leanprover/lean4:nightly-2024-11-18