perf(reassoc, to_app, elementwise): don't pass the same proof to the kernel again (#30650)

In `reassoc`, `to_app`, `elementwise`, the proof of the original lemma was being used to prove the modified lemma. This is silly, because the modified lemma can be proved using the original lemma directly. Hence, this PR modifies `addRelatedDecl` to include this optimization.

Previously, `addRelatedDecl` would pass around both the type and the value of the original declaration. This was necessary, because the inferred type of the value might not be identical to the type it is given. Now this is not necessary anymore, because the type of the constant is exactly the type that it is given, so the type can always be obtained with `inferType`.

Author: JovanGerb

Mathlib/Tactic/CategoryTheory/Elementwise.lean

@@ -82,11 +82,11 @@ for the first universe parameter to `HasForget`.
 The `simpSides` option controls whether to simplify both sides of the equality, for simpNF
 purposes.
 -/
-def elementwiseExpr (src : Name) (type pf : Expr) (simpSides := true) :
+def elementwiseExpr (src : Name) (pf : Expr) (simpSides := true) :
     MetaM (Expr × Option (Level × Level)) := do
-  let type := (← instantiateMVars type).cleanupAnnotations
+  let type := (← instantiateMVars (← inferType pf)).cleanupAnnotations
   forallTelescope type fun fvars type' => do
-    mkHomElementwise type' (← mkExpectedTypeHint (mkAppN pf fvars) type') fun eqPf instConcr? => do
+    mkHomElementwise type' (mkAppN pf fvars) fun eqPf instConcr? => do
       -- First simplify using elementwise-specific lemmas
       let mut eqPf' ← simpType (simpOnlyNames elementwiseThms (config := { decide := false })) eqPf
       if (← inferType eqPf') == .const ``True [] then
@@ -213,8 +213,8 @@ initialize registerBuiltinAttribute {
   | `(attr| elementwise $[nosimp%$nosimp?]? $[(attr := $stx?,*)]?) => MetaM.run' do
     if (kind != AttributeKind.global) then
       throwError "`elementwise` can only be used as a global attribute"
-    addRelatedDecl src "_apply" ref stx? fun type value levels => do
-      let (newValue, level?) ← elementwiseExpr src type value (simpSides := nosimp?.isNone)
+    addRelatedDecl src "_apply" ref stx? fun value levels => do
+      let (newValue, level?) ← elementwiseExpr src value (simpSides := nosimp?.isNone)
       let newLevels ← if let some (levelW, levelUF) := level? then do
         let w := mkUnusedName levels `w
         let uF := mkUnusedName levels `uF
@@ -252,7 +252,7 @@ normal form. `elementwise_of%` does not do this.
 -/
 elab "elementwise_of% " t:term : term => do
   let e ← Term.elabTerm t none
-  let (pf, _) ← elementwiseExpr .anonymous (← inferType e) e (simpSides := false)
+  let (pf, _) ← elementwiseExpr .anonymous e (simpSides := false)
   return pf
 
 -- TODO: elementwise tactic

Mathlib/Tactic/CategoryTheory/Reassoc.lean

@@ -102,14 +102,12 @@ def registerReassocExpr (f : Expr → MetaM (Expr × Array MVarId)) : IO Unit :=
   reassocImplRef.modify (·.push f)
 
 /--
-Reassociates the morphisms in `type?` using the registered handlers,
+Reassociates the morphisms in the type of `pf` using the registered handlers,
 using `reassocExprHom` as the default.
-If `type?` is not given, it is assumed to be the type of `pf`.
 
 Returns the proof of the lemma along with instance metavariables that need synthesis.
 -/
-def reassocExpr (pf : Expr) (type? : Option Expr) : MetaM (Expr × Array MVarId) := do
-  let pf ← if let some type := type? then mkExpectedTypeHint pf type else pure pf
+def reassocExpr (pf : Expr) : MetaM (Expr × Array MVarId) := do
   forallTelescopeReducing (← inferType pf) fun xs _ => do
     let pf := mkAppN pf xs
     let handlers ← reassocImplRef.get
@@ -120,8 +118,8 @@ def reassocExpr (pf : Expr) (type? : Option Expr) : MetaM (Expr × Array MVarId)
 /--
 Version of `reassocExpr` for the `TermElabM` monad. Handles instance metavariables automatically.
 -/
-def reassocExpr' (pf : Expr) (type? : Option Expr) : TermElabM Expr := do
-  let (e, insts) ← reassocExpr pf type?
+def reassocExpr' (pf : Expr) : TermElabM Expr := do
+  let (e, insts) ← reassocExpr pf
   for inst in insts do
     inst.withContext do
       unless ← Term.synthesizeInstMVarCore inst do
@@ -136,9 +134,9 @@ initialize registerBuiltinAttribute {
   | `(attr| reassoc $[(attr := $stx?,*)]?) => MetaM.run' do
     if (kind != AttributeKind.global) then
       throwError "`reassoc` can only be used as a global attribute"
-    addRelatedDecl src "_assoc" ref stx? fun type value levels => do
+    addRelatedDecl src "_assoc" ref stx? fun value levels => do
       Term.TermElabM.run' <| Term.withSynthesize do
-        let pf ← reassocExpr' value type
+        let pf ← reassocExpr' value
         pure (pf, levels)
   | _ => throwUnsupportedSyntax }
 
@@ -152,6 +150,6 @@ This also works for equations between isomorphisms, provided that
 -/
 elab "reassoc_of% " t:term : term => do
   let e ← Term.withSynthesizeLight <| Term.elabTerm t none
-  reassocExpr' e none
+  reassocExpr' e
 
 end CategoryTheory

Mathlib/Tactic/CategoryTheory/ToApp.lean

@@ -122,9 +122,8 @@ initialize registerBuiltinAttribute {
   | `(attr| to_app $[(attr := $stx?,*)]?) => MetaM.run' do
     if (kind != AttributeKind.global) then
       throwError "`to_app` can only be used as a global attribute"
-    addRelatedDecl src "_app" ref stx? fun type value levels => do
+    addRelatedDecl src "_app" ref stx? fun value levels => do
       let levelMVars ← levels.mapM fun _ => mkFreshLevelMVar
-      let value ← mkExpectedTypeHint value type
       let value := value.instantiateLevelParams levels levelMVars
       let newValue ← toAppExpr (← toCatExpr value)
       let r := (← getMCtx).levelMVarToParam (fun _ => false) (fun _ => false) newValue

Mathlib/Util/AddRelatedDecl.lean

@@ -30,8 +30,8 @@ Arguments:
 * `src : Name` is the existing declaration that we are modifying.
 * `suffix : String` will be appended to `src` to form the name of the new declaration.
 * `ref : Syntax` is the syntax where the user requested the related declaration.
-* `construct type value levels : MetaM (Expr × List Name)`
-  given the type, value, and universe variables of the original declaration,
+* `construct value levels : MetaM (Expr × List Name)`
+  given an `Expr.const` referring to the original declaration, and its universe variables,
   should construct the value of the new declaration,
   along with the names of its universe variables.
 * `attrs` is the attributes that should be applied to both the new and the original declaration,
@@ -42,14 +42,15 @@ Arguments:
 -/
 def addRelatedDecl (src : Name) (suffix : String) (ref : Syntax)
     (attrs? : Option (Syntax.TSepArray `Lean.Parser.Term.attrInstance ","))
-    (construct : Expr → Expr → List Name → MetaM (Expr × List Name)) :
+    (construct : Expr → List Name → MetaM (Expr × List Name)) :
     MetaM Unit := do
   let tgt := match src with
     | Name.str n s => Name.mkStr n <| s ++ suffix
     | x => x
   addDeclarationRangesFromSyntax tgt (← getRef) ref
   let info ← getConstInfo src
-  let (newValue, newLevels) ← construct info.type info.value! info.levelParams
+  let value := .const src (info.levelParams.map mkLevelParam)
+  let (newValue, newLevels) ← construct value info.levelParams
   let newValue ← instantiateMVars newValue
   let newType ← instantiateMVars (← inferType newValue)
   match info with