The translation attribute.

Implementation of the translation attribute. This is used for @[to_additive] and @[to_dual]. See the docstring of to_additive for more information

def Mathlib.Tactic.Translate.attrOption : Lean.ParserDescr

(attr := ...) applies the given attributes to the original and the translated declaration. In the case of to_additive, we may want to apply it multiple times, (such as in a ^ n -> n • a -> n +ᵥ a). In this case, you should use the syntax to_additive (attr := some_other_attr, to_additive), which will apply some_other_attr to all three generated declarations.

def Mathlib.Tactic.Translate.reorderOption : Lean.ParserDescr

(reorder := ...) reorders the arguments/hypotheses in the generated declaration. It uses cycle notation. For example (reorder := α β, 5 6) swaps the arguments α and β with each other and the fifth and the sixth argument, and (reorder := 3 4 5) will move the fifth argument before the third argument. This is used in to_dual to swap the arguments in ≤, < and ⟶. It is also used in to_additive to translate from a ^ n to n • a.

If the translated declaration already exists (i.e. when using existing or self), this is inferred automatically using the function guessReorder.

def Mathlib.Tactic.Translate.relevantArgOption : Lean.ParserDescr

the (relevant_arg := ...) option tells which argument to look at to determine whether to translate this constant. This is inferred automatically, but it can also be overwritten using this syntax.

If there are multiple possible arguments, we typically tag the first one. If this argument contains a fixed type, this declaration will not be translated. See the Heuristics section of the to_additive doc-string for more details.

When it cannot be inferred automatically, it is presumed that the first argument is relevant.

Use (relevant_arg := _) to indicate that there is no relevant argument.

Implementation note: we only allow exactly 1 relevant argument, even though some declarations (like Prod.instGroup) have multiple relevant arguments. The reason is that whether we translate a declaration is an all-or-nothing decision, and we will not be able to translate declarations that (e.g.) talk about multiplication on ℕ × α anyway.

def Mathlib.Tactic.Translate.dontTranslateOption : Lean.ParserDescr

(dont_translate := ...) takes a list of type variables (separated by spaces) that should not be considered for translation. For example in

lemma foo {α β : Type} [Group α] [Group β] (a : α) (b : β) : a * a⁻¹ = 1 ↔ b * b⁻¹ = 1

we can choose to only translate α by writing to_additive (dont_translate := β).

def Mathlib.Tactic.Translate.bracketedOption : Lean.ParserDescr

def Mathlib.Tactic.Translate.translationHint : Lean.ParserDescr

A hint about the translated declaration

• existing indicates that the translated form of the declaration is a pre-existing declaration. This is useful when the value cannot be translated, either because of a limitation in the translation heuristics, or because the value/proof is genuinely different.

• self indicates that the declaration translates to itself, up to some reordering of arguments. If no arguments are reordered then the attribute is redundant, which the translateRedundant linter will warn about.

• none indicates that the translated declaration should not get a user-facing name, instead being named like an auxiliary declaration. This is particularly useful for to_dual when using the reassoc attribute, because the dual of a right associated term is left associated, but we only want user-facing lemmas with right associated terms.

def Mathlib.Tactic.Translate.attrArgs : Lean.ParserDescr

opaque Mathlib.Tactic.Translate.linter.existingAttributeWarning : Lean.Option Bool

Linter, mostly used by translate attributes, that checks that the source declaration doesn't have certain attributes

opaque Mathlib.Tactic.Translate.linter.translateGenerateName : Lean.Option Bool

Linter used by translate attributes that checks if the given declaration name is equal to the automatically generated name

opaque Mathlib.Tactic.Translate.linter.translateExisting : Lean.Option Bool

Linter to check whether the user correctly specified that the translated declaration already exists

opaque Mathlib.Tactic.Translate.linter.translateReorder : Lean.Option Bool

Linter used by translate attributes that checks if the given reorder is equal to the automatically generated name

opaque Mathlib.Tactic.Translate.linter.translateRelevantArg : Lean.Option Bool

Linter used by translate attributes that checks if the relevant_arg is automatically generated.

opaque Mathlib.Tactic.Translate.linter.translateOverwrite : Lean.Option Bool

Linter used by translate attributes that checks if the attribute was already applied

opaque Mathlib.Tactic.Translate.linter.translateRedundant : Lean.Option Bool

Linter used by translate attributes that checks if the attribute is redundant

@[reducible, inline]

abbrev Mathlib.Tactic.Translate.Reorder : Type

Reorder represents a permutation of arguments in a translation. It is specified with the (reorder := ...) notation using a disjoint cycle representation.

inductive Mathlib.Tactic.Translate.RelevantArg : Type

RelevantArg represents an optional argument that should be checked to determine whether or not to translate the given constant.

• noArg : RelevantArg

  No argument needs to be checked. This is specified with (relevant_arg := _).

• arg (n : ℕ) : RelevantArg

  Argument n needs to be checked. This is specified with (relevant_arg := n).

instance Mathlib.Tactic.Translate.instBEqRelevantArg : BEq RelevantArg

def Mathlib.Tactic.Translate.instBEqRelevantArg.beq : RelevantArg → RelevantArg → Bool

def Mathlib.Tactic.Translate.instInhabitedRelevantArg.default : RelevantArg

instance Mathlib.Tactic.Translate.instInhabitedRelevantArg : Inhabited RelevantArg

instance Mathlib.Tactic.Translate.instToMessageDataRelevantArg : Lean.ToMessageData RelevantArg

structure Mathlib.Tactic.Translate.TranslationInfo : Type

TranslationInfo stores the information of how to translate a constant.

• translation : Lean.Name

  The name that we are translating to.

• reorder : Reorder

  The arguments that should be reordered when translating, using disjoint cycle notation.

• relevantArg : RelevantArg

  The argument used to determine whether this constant should be translated.

structure Mathlib.Tactic.Translate.TranslateData : Type

TranslateData is a structure that holds all data required for a translation attribute.

• ignoreArgsAttr : Lean.NameMapExtension (List ℕ)

  An attribute that tells that certain arguments of this definition are not involved when translating. This helps the translation heuristic by also transforming definitions if ℕ or another fixed type occurs as one of these arguments.

• doTranslateAttr : Lean.NameMapExtension Bool

  The global do_translate/dont_translate attributes specify whether operations on a given type should be translated. dont_translate can be used for types that are translated, such as MonoidAlgebra -> AddMonoidAlgebra, or for fixed types, such as Fin n/ZMod n. do_translate is for types without arguments, like Unit and Empty, where the structure on it can be translated.

  Note: The name generation is not aware of dont_translate, so if some part of a lemma is not translated thanks to this, you generally have to specify the translated name manually.

• unfoldBoundaries? : Option UnfoldBoundary.UnfoldBoundaryExt

  The insert_cast/insert_cast_fun attributes create an abstraction boundary for the tagged constant when translating it. For example, Set.Icc, Monotone, DecidableLT, WCovBy are all morally self-dual, but their definition is not self-dual. So, in order to allow these constants to be self-dual, we need to not unfold their definition in the proof term that we translate.

• translations : Lean.NameMapExtension TranslationInfo

  translations stores all of the constants that have been tagged with this attribute, and maps them to their translation.

• attrName : Lean.Name

  The name of the attribute, for example to_additive or to_dual.

• changeNumeral : Bool

  If changeNumeral := true, then try to translate the number 1 to 0.

• isDual : Bool

  When isDual := true, every translation A → B will also give a translation B → A.

• guessNameData : GuessName.GuessNameData

  The data that is required to guess the name of a translation.

def Mathlib.Tactic.Translate.findTranslation? (env : Lean.Environment) (t : TranslateData) : Lean.Name → Option TranslationInfo

Get the translation for the given name.

def Mathlib.Tactic.Translate.findTranslationName? (env : Lean.Environment) (t : TranslateData) (n : Lean.Name) : Option Lean.Name

Get the translation name for the given name.

def Mathlib.Tactic.Translate.findPrefixTranslation? (n : Lean.Name) (t : TranslateData) : Lean.CoreM (Option TranslationInfo)

Get the translation for the given name, falling back to translating a prefix of the name if the full name can't be translated. This allows translating automatically generated declarations such as IsRegular.casesOn. We make sure that the new constant is realized.

def Mathlib.Tactic.Translate.insertTranslation (t : TranslateData) (src tgt : Lean.Name) (reorder : Reorder) (relevantArg : RelevantArg) (ref : Lean.Syntax) : Lean.CoreM Unit

Add a translation to the translations map. If the translation attribute is dual, also add the reverse translation.

structure Mathlib.Tactic.Translate.Config : Type

Config is the type of the arguments that can be provided to to_additive.

• trace : Bool

  View the trace of the translation procedure. Equivalent to set_option trace.translate true.

• tgt : Lean.Name

  The given name of the target.

• doc : Option String

  An optional doc string.

• allowAutoName : Bool

  If allowAutoName is false (default) then we check whether the given name can be auto-generated.

• reorder? : Option Reorder

  The arguments that should be reordered when translating, using cycle notation.

• relevantArg? : Option RelevantArg

  The argument used to determine whether this constant should be translated.

• attrs : Array Lean.Syntax

  The attributes which we want to give to the original and translated declaration. For simps this will also add generated lemmas to the translation dictionary.

• dontTranslate : List ℕ

  A list of positions of type variables that should not be translated.

• ref : Lean.Syntax

  The Syntax element corresponding to the translation attribute, which we need for adding definition ranges, and for logging messages.

• existing : Bool

  An optional flag stating that the translated declaration already exists. If this flag is wrong about whether the translated declaration exists, we raise a linter error. Note: the linter will never raise an error for inductive types and structures.

• self : Bool

  An optional flag stating that the target of the translation is the target itself. This can be used to reorder arguments, such as in attribute [to_dual self (reorder := 3 4)] LE.le. If self := true, we should also have existing := true.

• none : Bool

  An optional flag for not giving the new declaration a user-facing name. This is achieved by appending e.g. _to_dual_1 to the name of the original declaration.

def Mathlib.Tactic.Translate.etaExpandN (n : ℕ) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Eta expands e exactly n times.

@[reducible, inline]

abbrev Mathlib.Tactic.Translate.ReplacementM (α : Type) : Type

Monad used by applyReplacementFun.

• The reader stores the free variables on which nothing should be translated.
• The state stores the free variables on which something has been translated.
• The cache caches the results on subexpressions.

def Mathlib.Tactic.Translate.ReplacementM.run {α : Type} (dontTranslate allFVars : Array Lean.FVarId) (x : ReplacementM α) : Lean.MetaM (α × Option ℕ)

Run a ReplacementM computation, returning the result and the value of relevant_arg that corresponds to this translation.

@[implemented_by _private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.shouldTranslateUnsafe]

opaque Mathlib.Tactic.Translate.shouldTranslate (env : Lean.Environment) (t : TranslateData) (e : Lean.Expr) : ReplacementM (Option Lean.Expr)

shouldTranslate e tests whether the expression e contains a constant that is not applied to any arguments and that doesn't have a translation itself. This is used for deciding which subexpressions to translate: we only translate constants if shouldTranslate applied to their relevant argument returns true. This means we will replace expression applied to e.g. α or α × β, but not when applied to e.g. ℕ or ℝ × α. We ignore all arguments specified by the ignore NameMap.

def Mathlib.Tactic.Translate.List.swapFirstTwo {α : Type u_1} : List α → List α

Swap the first two elements of a list

def Mathlib.Tactic.Translate.applyReplacementFun (t : TranslateData) (e : Lean.Expr) : ReplacementM Lean.Expr

applyReplacementFun e replaces the expression e with its translation. It translates each identifier (inductive type, defined function etc) in an expression, unless

• The identifier occurs in an application with relevantArg argument arg; and
• shouldTranslate arg is false.

It will also reorder arguments of certain functions, using the stored reorder.

def Mathlib.Tactic.Translate.renameBinderNames (t : TranslateData) (src : Lean.Expr) : Lean.Expr

Rename binder names in pi type.

def Mathlib.Tactic.Translate.reorderForall (reorder : Reorder) (src : Lean.Expr) : Lean.MetaM Lean.Expr

Reorder pi-binders. See doc of reorderAttr for the interpretation of the argument

def Mathlib.Tactic.Translate.reorderLambda (reorder : Reorder) (src : Lean.Expr) : Lean.MetaM Lean.Expr

Reorder lambda-binders. See doc of reorderAttr for the interpretation of the argument

def Mathlib.Tactic.Translate.applyReplacementForall (t : TranslateData) (dontTranslate : List ℕ) (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Option RelevantArg)

Run applyReplacementFun on an expression ∀ x₁ .. xₙ, e, making sure not to translate type-classes on xᵢ if i is in dontTranslate.

def Mathlib.Tactic.Translate.applyReplacementLambda (t : TranslateData) (dontTranslate : List ℕ) (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Option RelevantArg)

Run applyReplacementFun on an expression fun x₁ .. xₙ ↦ e, making sure not to translate type-classes on xᵢ if i is in dontTranslate.

def Mathlib.Tactic.Translate.updateDecl (t : TranslateData) (tgt : Lean.Name) (srcDecl : Lean.ConstantInfo) (reorder : Reorder) (dont : List ℕ) (unfoldBoundaries? : Option UnfoldBoundary.UnfoldBoundaries) : Lean.MetaM (Lean.ConstantInfo × Option RelevantArg)

Run applyReplacementFun on the given srcDecl to make a new declaration with name tgt.

def Mathlib.Tactic.Translate.updateAndAddDecl (t : TranslateData) (tgt : Lean.Name) (srcDecl : Lean.ConstantInfo) (reorder : Reorder) (dont : List ℕ) : Lean.MetaM (Lean.ConstantInfo × Option RelevantArg)

Translate the source declaration and then run addDecl. If the kernel throws an error, try to emit a better error message.

For efficiency in to_dual, we first run updateDecl without any UnfoldBoundaries, and only if that fails do we try to include them. The reason is that in the most common case, to_dual succeeds without needing to insert unfold boundaries, and figuring out whether to insert them can be quite expensive.

def Mathlib.Tactic.Translate.declUnfoldSimpAuxLemmas (decl : Lean.ConstantInfo) : Lean.MetaM Lean.ConstantInfo

Unfold simp and gcongr 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 Mathlib.Tactic.Translate.findTargetName (env : Lean.Environment) (t : TranslateData) (src rootSrc rootTgt : Lean.Name) : Lean.CoreM Lean.Name

Find the target name of src, which is assumed to have been selected by findAuxDecls.

def Mathlib.Tactic.Translate.findAuxDecls (decl : Lean.ConstantInfo) (pre : Lean.Name) : Lean.CoreM (Array Lean.Name)

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 Mathlib.Tactic.Translate.getRelevantArg (t : TranslateData) (cfg : Config) (relevantArg? : Option RelevantArg) (src : Lean.Name) : Lean.CoreM RelevantArg

Return the relevant_arg option based on the computed relevantArg? and the given cfg.relevantArg?.

partial def Mathlib.Tactic.Translate.transformDeclRec (t : TranslateData) (cfg : Config) (rootSrc rootTgt src : Lean.Name) (reorder : Reorder := []) : Lean.CoreM Unit

Translate the declaration src and recursively all declarations pre._proof_i occurring in src using the translations dictionary.

replace_all, trace, ignore and reorder are configuration options.

pre is the declaration that got the translation attribute and tgt_pre is the target of this declaration.

def Mathlib.Tactic.Translate.copyInstanceAttribute (src tgt : Lean.Name) : Lean.CoreM Unit

Copy the instance attribute in a to_additive

[todo] it seems not to work when the to_additive is added as an attribute later.

def Mathlib.Tactic.Translate.warnAttrCore (stx : Lean.Syntax) (f : Lean.Environment → Lean.Name → Bool) (thisAttr attrName src tgt : Lean.Name) : Lean.CoreM Unit

Warn the user when the declaration has an attribute.

def Mathlib.Tactic.Translate.warnAttr {α β : Type} [Inhabited β] (stx : Lean.Syntax) (attr : Lean.SimpleScopedEnvExtension α β) (f : β → Lean.Name → Bool) (thisAttr attrName src tgt : Lean.Name) : Lean.CoreM Unit

Warn the user when the declaration has a simple scoped attribute.

def Mathlib.Tactic.Translate.warnParametricAttr {β : Type} [Inhabited β] (stx : Lean.Syntax) (attr : Lean.ParametricAttribute β) (thisAttr attrName src tgt : Lean.Name) : Lean.CoreM Unit

Warn the user when the declaration has a parametric attribute.

def Mathlib.Tactic.Translate.translateLemmas {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m] (t : TranslateData) (names : Array Lean.Name) (reorder : Reorder) (relevantArg : RelevantArg) (desc : String) (ref : Lean.Syntax) (runAttr : Lean.Name → m (Array Lean.Name)) : m Unit

translateLemmas names argInfo desc t runs t on all elements of names and adds translations between the generated lemmas (the output of t). names must be non-empty.

def Mathlib.Tactic.Translate.targetName (t : TranslateData) (cfg : Config) (src : Lean.Name) : Lean.CoreM Lean.Name

Return the provided target name or autogenerate one if one was not provided.

def Mathlib.Tactic.Translate.guessReorder (src tgt : Lean.Expr) : Reorder

Try to determine the value of the (reorder := ...) option that would be needed to translate type e₁ to type e₂. If there is no good guess, default to []. The heuristic that we use is to compare the conclusions of e₁ and e₂, and to observe which variables are swapped.

def Mathlib.Tactic.Translate.checkExistingType (t : TranslateData) (src tgt : Lean.Name) (cfg : Config) : Lean.MetaM (Reorder × RelevantArg)

Verify that the type of srcDecl translates to that of tgtDecl. Also try to autogenerate the reorder option for this translation.

def Mathlib.Tactic.Translate.proceedFieldsAux (t : TranslateData) (src tgt : Lean.Name) (reorder : Reorder) (relevantArg : RelevantArg) (ref : Lean.Syntax) (f : Lean.Name → Array Lean.Name) : Lean.CoreM Unit

if f src = #[a_1, ..., a_n] and f tgt = #[b_1, ... b_n] then proceedFieldsAux src tgt f will insert translations from a_i to b_i.

def Mathlib.Tactic.Translate.proceedFields (t : TranslateData) (src tgt : Lean.Name) (reorder : Reorder) (relevantArg : RelevantArg) (ref : Lean.Syntax) : Lean.CoreM Unit

Add the structure fields of src to the translations dictionary so that they will be translated correctly.

def Mathlib.Tactic.Translate.elabArgStx (declName : Lean.Name) (argNames : Array Lean.Name) (args : Array Lean.Expr) (stx : Lean.TSyntax [`ident, `num]) : Lean.MetaM ℕ

Elaborate syntax that refers to an argument of the declaration. This is either a 1-indexed number, or a name from argNames. args is only used to add hover information to stx, and declName is only used for the error message.

def Mathlib.Tactic.Translate.elabTranslationAttr (declName : Lean.Name) (stx : Lean.Syntax) : Lean.CoreM Config

Elaboration of the configuration options for a translation attribute. It is assumed that

• stx[0] is the attribute (e.g. to_additive)
• stx[1] is the optional tracing ?
• stx[2] is the remaining attrArgs

TODO: Currently, we don't deduce any dont_translate arguments based on the type of declName. In the future we would like that the presence of MonoidAlgebra k G will automatically flag k as a type to not be translated.

partial def Mathlib.Tactic.Translate.applyAttributes (t : TranslateData) (cfg : Config) (src tgt : Lean.Name) (reorder : Reorder) (relevantArg : RelevantArg) : Lean.Elab.TermElabM (Array Lean.Name)

Apply attributes to the original and translated declarations.

partial def Mathlib.Tactic.Translate.copyMetaData (t : TranslateData) (cfg : Config) (src : Lean.Name) : Lean.CoreM (Array Lean.Name)

Copies equation lemmas and attributes from src to tgt

partial def Mathlib.Tactic.Translate.addTranslationAttr (t : TranslateData) (src : Lean.Name) (cfg : Config) (kind : Lean.AttributeKind := Lean.AttributeKind.global) : Lean.AttrM (Array Lean.Name)

addTranslationAttr src cfg adds a translation attribute to src with configuration cfg. See the attribute implementation for more details. It returns an array with names of translated declarations (usually 1, but more if there are nested to_additive calls).