fix(translate): don't unfold aux lemmas, but translate them (leanprover-community#33603)

`to_additive` has some troublesome interactions with the module system, because it sometimes relies on unfolding theorems whose value is not exported. This PR fixes that by never unfolding these theorems, and instead creating their translation the first time they appear.

This will help remove some instances of `import all` and instances of `proofsInPublic`.

The only theorems that we still unfold are the auxiliary theorems created by `simp`. These have very small proofs, and these proofs are always exported, so it is fine to unfold them.

Author: JovanGerb

Mathlib/Lean/Name.lean

@@ -58,14 +58,3 @@ def Lean.Name.decapitalize (n : Name) : Name :=
   n.modifyBase fun
     | .str p s => .str p s.decapitalize
     | n       => n
-
-/-- Whether the lemma has a name of the form produced by `Lean.Meta.mkAuxLemma`. -/
-def Lean.Name.isAuxLemma (n : Name) : Bool :=
-  match n with
-  -- `mkAuxLemma` generally allows for arbitrary prefixes but these are the ones produced by core.
-  | .str _ s => "_proof_".isPrefixOf s || "_simp_".isPrefixOf s
-  | _ => false
-
-/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. -/
-def Lean.Meta.unfoldAuxLemmas (e : Expr) : MetaM Expr := do
-  deltaExpand e Lean.Name.isAuxLemma

Mathlib/MeasureTheory/Function/LpSpace/DomAct/Continuous.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
 public import Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
 public import Mathlib.Topology.Algebra.Constructions.DomMulAct
-import all Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic  -- for `to_additive` to unfold proof
 
 /-!
 # Continuity of the action of `Mᵈᵐᵃ` on `MeasureSpace.Lp E p μ`

Mathlib/Tactic/Translate/Core.lean

@@ -531,16 +531,6 @@ def applyReplacementLambda (t : TranslateData) (dontTranslate : List Nat) (e : E
   else
     applyReplacementFun t e #[]
 
-/-- Unfold auxlemmas in the type and value. -/
-def declUnfoldAuxLemmas (decl : ConstantInfo) : MetaM ConstantInfo := do
-  let mut decl := decl
-  decl := decl.updateType <| ← unfoldAuxLemmas decl.type
-  if let some v := decl.value? (allowOpaque := true) then
-    trace[translate] "value before unfold:{indentExpr v}"
-    decl := decl.updateValue <| ← unfoldAuxLemmas v
-    trace[translate] "value after unfold:{indentExpr decl.value!}"
-  return decl
-
 /-- Run applyReplacementFun on the given `srcDecl` to make a new declaration with name `tgt` -/
 def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
     (reorder : List (List Nat)) (dont : List Nat) : MetaM ConstantInfo := do
@@ -578,48 +568,49 @@ def findRelevantArg (t : TranslateData) (nm : Name) : CoreM Nat := MetaM.run' do
     trace[translate_detail] "findRelevantArg: {arg}"
     return arg.getD 0
 
-/-- Abstracts the nested proofs in the value of `decl` if it is a def.
-This follows the behaviour of `Elab.abstractNestedProofs`. -/
-def declAbstractNestedProofs (decl : ConstantInfo) : MetaM ConstantInfo := do
-  let .defnInfo info := decl | return decl
-  let value ← withDeclNameForAuxNaming decl.name do Meta.abstractNestedProofs info.value
-  return .defnInfo { info with value }
+/-- Unfold `simp` auxlemmas in the type and value.
+The reason why we can't just translate them is that they are generated by the `@[simp]` attribute,
+so it would require a change in the implementation of `@[simp]` to add these translateions.
+Additionally, these lemmas have very short proofs, so unfolding them is not costly. -/
+def declUnfoldSimpAuxLemmas (decl : ConstantInfo) : MetaM ConstantInfo := do
+  let unfold (e : Expr) := deltaExpand e fun
+    | .str _ s => "_simp_".isPrefixOf s
+    | _ => false
+  let mut decl := decl
+  decl := decl.updateType <| ← unfold decl.type
+  if let some v := decl.value? (allowOpaque := true) then
+    trace[translate] "value before unfold:{indentExpr v}"
+    decl := decl.updateValue <| ← unfold v
+    trace[translate] "value after unfold:{indentExpr decl.value!}"
+  return decl
 
-/-- Find the target name of `pre` and all created auxiliary declarations. -/
-def findTargetName (env : Environment) (t : TranslateData) (src pre tgt_pre : Name) : CoreM Name :=
+/-- Find the target name of `src`, which is assumed to have been selected by `findAuxDecls`. -/
+def findTargetName (env : Environment) (t : TranslateData) (src pre tgt_pre : Name) :
+    CoreM Name := do
   /- This covers auxiliary declarations like `match_i` and `proof_i`. -/
-  if let some post := pre.isPrefixOf? src then
-    return tgt_pre ++ post
-  else if src.hasMacroScopes then
-    -- This branch should come before the next one because an aux def may be both private and macro
-    -- scoped - but really the next branch shouldn't just assume all private defs are eqns??
+  if let some post := (privateToUserName pre).isPrefixOf? (privateToUserName src) then
+    let tgt := tgt_pre ++ post
+    return if isPrivateName src then mkPrivateName env tgt else tgt
+  if src.hasMacroScopes then
     mkFreshUserName src.eraseMacroScopes
-  /- This covers equation lemmas (for other declarations). -/
-  else if let some post := privateToUserName? src then
-    match findTranslation? env t post.getPrefix with
-    -- this is an equation lemma for a declaration without a translation. We will skip this.
-    | none => return src
-    -- this is an equation lemma for a declaration with a translation. We will translate this.
-    -- Note: if this errors we could do this instead by calling `getEqnsFor?`
-    | some addName => return src.updatePrefix <| mkPrivateName env addName
   else
-    throwError "internal @[{t.attrName}] error."
-
-/-- Returns a `NameSet` of all auxiliary constants in `e` that might have been generated
-when adding `pre` to the environment.
-Examples include `pre.match_5` and
-`_private.Mathlib.MyFile.someOtherNamespace.someOtherDeclaration._eq_2`.
-The last two examples may or may not have been generated by this declaration.
-The last example may or may not be the equation lemma of a declaration with a translation attribute.
-We will only translate it if it has a translation attribute.
-
-Note that this function would return `proof_nnn` aux lemmas if
-we hadn't unfolded them in `declUnfoldAuxLemmas`.
+    withDeclNameForAuxNaming src do mkAuxDeclName (Name.mkSimple s!"_{t.attrName.toString}")
+
+/-- Returns a `NameSet` of auxiliary constants in `decl` that might have been generated
+when adding `pre` to the environment, and which hence might need to be translated.
+Examples include `pre.match_5`, `pre._proof_2`, `someOtherDeclaration._proof_2` and `wrapped✝`.
+The reason why we have to include `_proof_i` lemmas from other declarations is that there is a
+cache of such proofs, and previous such auxiliary proofs are reused when possible.
+These auxiliary declarations may be private or not, independent of whether `pre` is private.
+`wrapped✝` is generated by `irreducible_def`, and it has macro scopes.
 -/
-def findAuxDecls (e : Expr) (pre : Name) : NameSet :=
-  e.foldConsts ∅ fun n l ↦
-    if (privateToUserName n).getPrefix == privateToUserName pre || n.hasMacroScopes then
-      l.insert n
+def findAuxDecls (decl : ConstantInfo) (pre : Name) : CoreM (Array Name) := do
+  let env ← withoutExporting getEnv
+  return (Expr.app decl.type (decl.value! (allowOpaque := true))).foldConsts #[] fun n l ↦
+    if (env.find? n).any (·.hasValue (allowOpaque := true)) &&
+      ((match n with | .str _ s => "_proof_".isPrefixOf s | _ => false) ||
+      (privateToUserName n).getPrefix == privateToUserName pre || n.hasMacroScopes) then
+      l.push n
     else
       l
 
@@ -631,7 +622,7 @@ occurring in `src` using the `translations` dictionary.
 `pre` is the declaration that got the translation attribute and `tgt_pre` is the target of this
 declaration. -/
 partial def transformDeclRec (t : TranslateData) (ref : Syntax) (pre tgt_pre src : Name)
-    (reorder : List (List Nat) := []) (dontTranslate : List Nat := []) : CoreM Unit := do
+    (dontTranslate : List Nat) (reorder : List (List Nat) := []) : CoreM Unit := do
   let env ← getEnv
   trace[translate_detail] "visiting {src}"
   -- if we have already translated this declaration, we do nothing.
@@ -655,27 +646,28 @@ partial def transformDeclRec (t : TranslateData) (ref : Syntax) (pre tgt_pre src
     return
   let srcDecl ← withoutExporting do getConstInfo src
   -- we first unfold all auxlemmas, since they are not always able to be translated on their own
-  let srcDecl ← withoutExporting do MetaM.run' do declUnfoldAuxLemmas srcDecl
+  let srcDecl ← withoutExporting do MetaM.run' do declUnfoldSimpAuxLemmas srcDecl
   -- we then transform all auxiliary declarations generated when elaborating `pre`
-  for n in findAuxDecls srcDecl.type pre do
-    transformDeclRec t ref pre tgt_pre n
-  if let some value := srcDecl.value? (allowOpaque := true) then
-    for n in findAuxDecls value pre do
-      transformDeclRec t ref pre tgt_pre n
+  for n in ← findAuxDecls srcDecl pre do
+    transformDeclRec t ref pre tgt_pre n dontTranslate
   -- expose target body when source body is exposed
   withExporting (isExporting := (← getEnv).setExporting true |>.find? src |>.any (·.hasValue)) do
   -- if the auxiliary declaration doesn't have prefix `pre`, then we have to add this declaration
   -- to the translation dictionary, since otherwise we cannot translate the name.
   let relevantArg ← findRelevantArg t src
   if !pre.isPrefixOf src || src != pre && relevantArg != 0 then
     insertTranslation t src tgt { relevantArg }
+  -- We still lack a heuristic that automatically infers the `dontTranslate`,
+  -- so for now we do a best guess based on argument names.
+  let dontTranslate ← if dontTranslate.isEmpty then pure [] else
+    if src == pre then pure dontTranslate else
+      let namesPre := (← getConstInfo pre).type.getForallBinderNames
+      let namesSrc := (← getConstInfo src).type.getForallBinderNames
+      pure <| dontTranslate.filterMap (namesPre[·]? >>= namesSrc.idxOf?)
   -- now transform the source declaration
   let trgDecl ← MetaM.run' <| updateDecl t tgt srcDecl reorder dontTranslate
-  let some value := trgDecl.value? (allowOpaque := true)
-    | throwError "Expected {tgt} to have a value."
+  let value := trgDecl.value! (allowOpaque := true)
   trace[translate] "generating\n{tgt} : {trgDecl.type} :=\n  {value}"
-  -- "Refold" all the aux lemmas that we unfolded.
-  let trgDecl ← MetaM.run' <| declAbstractNestedProofs trgDecl
   /- If `src` is explicitly marked as `noncomputable`, then add the new decl as a declaration but
   do not compile it, and mark is as noncomputable. Otherwise, only log errors in compiling if `src`
   has executable code.
@@ -1194,7 +1186,7 @@ partial def addTranslationAttr (t : TranslateData) (src : Name) (cfg : Config)
     proceedFields t src tgt argInfo
   else
     -- tgt doesn't exist, so let's make it
-    transformDeclRec t cfg.ref src tgt src argInfo.reorder cfg.dontTranslate
+    transformDeclRec t cfg.ref src tgt src cfg.dontTranslate argInfo.reorder
   let nestedNames ← copyMetaData t cfg src tgt argInfo
   -- add pop-up information when mousing over the given translated name
   -- (the information will be over the attribute if no translated name is given)

MathlibTest/ToDual.lean

@@ -2,6 +2,8 @@ import Mathlib.Order.Defs.PartialOrder
 import Mathlib.Order.Notation
 import Mathlib.Tactic.ToAdditive
 
+variable {α : Type} [PartialOrder α] (a b c : α)
+
 -- test that we can translate between structures, reordering the arguments of the fields
 class SemilatticeInf (α : Type) extends PartialOrder α, Min α where
   le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c
@@ -39,8 +41,7 @@ in the application
 -/
 #guard_msgs in
 @[to_dual]
-instance {α : Type} [PartialOrder α] [Min α]
-    (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where
+instance [Min α] (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where
   le_inf
 
 
@@ -53,7 +54,7 @@ Note: This linter can be disabled with `set_option linter.translateReorder false
 -/
 #guard_msgs in
 @[to_dual self (reorder := a b)]
-theorem le_imp_le {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id
+theorem le_imp_le : a ≤ b → a ≤ b := id
 
 -- The comparison on `reorder`s can see that `a b` is the same as `b a`:
 /--
@@ -64,7 +65,7 @@ Note: This linter can be disabled with `set_option linter.translateReorder false
 -/
 #guard_msgs in
 @[to_dual self (reorder := b a)]
-theorem le_imp_le' {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id
+theorem le_imp_le' : a ≤ b → a ≤ b := id
 
 -- It is possible to overwrite the autogenerated `reorder`:
 /--
@@ -75,7 +76,7 @@ but 'le_imp_le''' has type
 -/
 #guard_msgs in
 @[to_dual self (reorder := 2 3)]
-theorem le_imp_le'' {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id
+theorem le_imp_le'' : a ≤ b → a ≤ b := id
 
 -- We can even overwrite it with the empty `reorder`:
 /--
@@ -86,7 +87,7 @@ but 'le_imp_le'''' has type
 -/
 #guard_msgs in
 @[to_dual self (reorder := )]
-theorem le_imp_le''' {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id
+theorem le_imp_le''' : a ≤ b → a ≤ b := id
 
 -- Test a larger permutation:
 
@@ -104,11 +105,11 @@ Maybe we should have a new command `@[to_dual_translate]`, analogous to `@[to_du
 instead of using `@[to_dual self]` for those cases.
 -/
 @[to_dual self]
-theorem not_lt_self {α : Type} [PartialOrder α] (a : α) : ¬ a < a := lt_irrefl a
+theorem not_lt_self : ¬ a < a := lt_irrefl a
 
 -- Test that we do not translate numerals like we do in `@[to_additive]`
 @[to_dual self]
-theorem one_le_one {α : Type} [One α] [Preorder α] : (1 : α) ≤ 1 := le_rfl
+theorem one_le_one [One α] : (1 : α) ≤ 1 := le_rfl
 
 -- Test the name generated by `to_dual none`
 @[to_dual none]
@@ -117,3 +118,22 @@ theorem bot_eq_top {α : Type} [Bot α] [Top α] : (⊤ : α) = ⊥ → (⊤ : 
 /-- info: bot_eq_top._to_dual_1 {α : Type} [Top α] [Bot α] : ⊥ = ⊤ → ⊥ = ⊤ -/
 #guard_msgs in
 #check bot_eq_top._to_dual_1
+
+/- Test the translation of auxLemmas.
+`_proof_i` lemmas are translated, but `_simp_i` lemmas are unfolded. -/
+@[to_dual lt_le_trans]
+theorem le_lt_trans (h₁ : a ≤ b) (h₂ : b < c) : a < c := by
+  grind
+
+theorem le_refl': ∀ a : α, a ≤ a := by
+  simp
+
+/--
+info: fun {α} [PartialOrder α] a b c h₁ h₂ => lt_le_trans._proof_1_1 a b c h₁ h₂
+---
+info: fun {α} [PartialOrder α] => of_eq_true (Eq.trans (forall_congr fun a => le_refl._simp_1 a) (implies_true α))
+-/
+#guard_msgs in
+run_meta
+  Lean.logInfo (← Lean.getConstInfo ``lt_le_trans).value!
+  Lean.logInfo (← Lean.getConstInfo ``le_refl').value!

MathlibTest/toAdditive.lean

@@ -231,7 +231,7 @@ def mul_foo {α} [Monoid α] (a : α) : ℕ → α
 
 -- cannot apply `@[to_additive]` to `some_def` if `some_def.in_namespace` doesn't have the attribute
 run_cmd liftCoreM <| successIfFail <|
-  transformDeclRec ToAdditive.data (← getRef) `Test.some_def `Test.add_some_def `Test.some_def
+  transformDeclRec ToAdditive.data (← getRef) `Test.some_def `Test.add_some_def `Test.some_def []
 
 
 attribute [to_additive some_other_name] some_def.in_namespace