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.

Equations

• One or more equations did not get rendered due to their size.

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 ^ to •.

Equations

• One or more equations did not get rendered due to their size.

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 using the function findRelevantArg, 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.

If a declaration is not tagged, 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 argument. 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.

Equations

• One or more equations did not get rendered due to their size.

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 := β).

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

A hint for where to find the translated declaration (existing or self)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

An attribute that stores all the declarations that deal with numeric literals on variable types.

Numeral literals occur in expressions without type information, so in order to decide whether 1 needs to be changed to 0, the context around the numeral is relevant. Most numerals will be in an OfNat.ofNat application, though tactics can add numeral literals inside arbitrary functions. By default we assume that we do not change numerals, unless it is in a function application with the translate_change_numeral attribute.

@[translate_change_numeral n₁ ...] should be added to all functions that take one or more numerals as argument that should be changed if shouldTranslate succeeds on the first argument, i.e. when the numeral is only translated if the first argument is a variable (or consists of variables). The arguments n₁ ... are the positions of the numeral arguments (starting counting from 1).

Equations

• One or more equations did not get rendered due to their size.

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.changeNumeralAttr : Lean.NameMapExtension (List ℕ)

An attribute that stores all the declarations that deal with numeric literals on variable types.

Numeral literals occur in expressions without type information, so in order to decide whether 1 needs to be changed to 0, the context around the numeral is relevant. Most numerals will be in an OfNat.ofNat application, though tactics can add numeral literals inside arbitrary functions. By default we assume that we do not change numerals, unless it is in a function application with the translate_change_numeral attribute.

@[translate_change_numeral n₁ ...] should be added to all functions that take one or more numerals as argument that should be changed if shouldTranslate succeeds on the first argument, i.e. when the numeral is only translated if the first argument is a variable (or consists of variables). The arguments n₁ ... are the positions of the numeral arguments (starting counting from 1).

structure Mathlib.Tactic.Translate.ArgInfo : Type

ArgInfo stores information about how a constant should be translated.

• reorder : List (List ℕ)

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

• 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.

• argInfoAttr : Lean.NameMapExtension ArgInfo

  argInfoAttr stores the declarations that need some extra information to be translated.

• dontTranslateAttr : Lean.NameMapExtension Unit

  The global dont_translate attribute specifies that operations on the given type should not be translated. This can be either for types that are translated, such as MonoidAlgebra -> AddMonoidAlgebra, or for fixed types, such as Fin n/ZMod n.

  Note: The name generation is not aware that the operations on this type should not be translated, so you generally have to specify a name manually, if some part should not be translated.

• translations : Lean.NameMapExtension Lean.Name

  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 Lean.Name

Get the translation for the given name.

Equations

• Mathlib.Tactic.Translate.findTranslation? env t = (Lean.SimplePersistentEnvExtension.getState t.translations env).find?

def Mathlib.Tactic.Translate.findPrefixTranslation (env : Lean.Environment) (nm : Lean.Name) (t : TranslateData) : Lean.Name

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.ArgInfo.reverse (i : ArgInfo) : ArgInfo

Compute the ArgInfo for the reverse translation. The reorder permutation is inverted. In practice, relevantArg does not overlap with reorder for dual translations, so we don't bother applying the permutation to relevantArg.

Equations

• i.reverse = { reorder := List.map (fun (x : List ℕ) => x.reverse) i.reorder, relevantArg := i.relevantArg }

def Mathlib.Tactic.Translate.insertTranslation (t : TranslateData) (src tgt : Lean.Name) (argInfo : ArgInfo) (failIfExists : Bool := true) : Lean.CoreM Unit

Add a name translation to the translations map and add the argInfo information to src. If the translation attribute is dual, also add the reverse translation.

Equations

• One or more equations did not get rendered due to their size.

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 : List (List ℕ)

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

• relevantArg? : Option ℕ

  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. It can also be used to give a hint to shouldTranslate, such as in attribute [to_additive self] Unit. If self := true, we should also have existing := true.

instance Mathlib.Tactic.Translate.instReprConfig : Repr Config

Equations

• Mathlib.Tactic.Translate.instReprConfig = { reprPrec := Mathlib.Tactic.Translate.instReprConfig.repr }

def Mathlib.Tactic.Translate.instReprConfig.repr : Config → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

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

Eta expands e at most n times.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.expand (t : TranslateData) (e : Lean.Expr) : Lean.MetaM Lean.Expr

e.expand eta-expands all expressions that have as head a constant n in reorder. They are expanded until they are applied to one more argument than the maximum in reorder.find n. It also expands all kernel projections that have as head a constant n in reorder.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.shouldTranslate (env : Lean.Environment) (t : TranslateData) (e : Lean.Expr) (dontTranslate : Array Lean.FVarId := #[]) : Option (Lean.Name ⊕ Lean.FVarId)

shouldTranslate e tests whether the expression e contains a constant nm that is not applied to any arguments, and such that translations.find?[nm] = none. 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.

Equations

• Mathlib.Tactic.Translate.shouldTranslate env t e dontTranslate = Mathlib.Tactic.Translate.shouldTranslate.unsafe_impl_3✝ env t e dontTranslate

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

Swap the first two elements of a list

Equations

• Mathlib.Tactic.Translate.List.swapFirstTwo [] = []
• Mathlib.Tactic.Translate.List.swapFirstTwo [x_1] = [x_1]
• Mathlib.Tactic.Translate.List.swapFirstTwo (x_1 :: y :: l) = y :: x_1 :: l

def Mathlib.Tactic.Translate.changeNumeral : Lean.Expr → Lean.Expr

Change the numeral nat_lit 1 to the numeral nat_lit 0. Leave all other expressions unchanged.

Equations

• Mathlib.Tactic.Translate.changeNumeral (Lean.Expr.lit (Lean.Literal.natVal 1)) = Lean.mkRawNatLit 0
• Mathlib.Tactic.Translate.changeNumeral x✝ = x✝

def Mathlib.Tactic.Translate.applyReplacementFun (t : TranslateData) (e : Lean.Expr) (dontTranslate : Array Lean.FVarId := #[]) : Lean.MetaM Lean.Expr

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

• The identifier occurs in an application with first argument arg; and
• test arg is false. However, if f is in the dictionary relevant, then the argument relevant.find f is tested, instead of the first argument.

It will also reorder arguments of certain functions, using reorderFn: e.g. g x₁ x₂ x₃ ... xₙ becomes g x₂ x₁ x₃ ... xₙ if reorderFn g = some [1].

Equations

• One or more equations did not get rendered due to their size.

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

Rename binder names in pi type.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Unfold auxlemmas in the type and value.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.updateDecl (t : TranslateData) (tgt : Lean.Name) (srcDecl : Lean.ConstantInfo) (reorder : List (List ℕ)) (dont : List ℕ) : Lean.MetaM Lean.ConstantInfo

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

Equations

• One or more equations did not get rendered due to their size.

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

Abstracts the nested proofs in the value of decl if it is a def.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.findTargetName (env : Lean.Environment) (t : TranslateData) (src pre tgt_pre : Lean.Name) : Lean.CoreM Lean.Name

Find the target name of pre and all created auxiliary declarations.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.findAuxDecls (e : Lean.Expr) (pre : Lean.Name) : Lean.NameSet

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.

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.Translate.transformDeclAux (t : TranslateData) (cfg : Config) (pre tgt_pre : Lean.Name) : Lean.Name → Lean.CoreM Unit

Transform the declaration src and all declarations pre._proof_i occurring in src using the transforms 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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.translateLemmas {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m] (t : TranslateData) (names : Array Lean.Name) (argInfo : ArgInfo) (desc : String) (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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.findRelevantArg (t : TranslateData) (nm : Lean.Name) : Lean.MetaM ℕ

Find the argument of nm that appears in the first translatable (type-class) argument. Returns 1 if there are no types with a translatable class as arguments. E.g. Prod.instGroup returns 1, and Pi.instOne returns 2. Note: we only consider the relevant argument ((relevant_arg := ...)) of each type-class. E.g. [Pow A N] is a translatable type-class on A, not on N.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.proceedFieldsAux (t : TranslateData) (src tgt : Lean.Name) (argInfo : ArgInfo) (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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.proceedFields (t : TranslateData) (src tgt : Lean.Name) (argInfo : ArgInfo) : Lean.CoreM Unit

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.Translate.applyAttributes (t : TranslateData) (stx : Lean.Syntax) (rawAttrs : Array Lean.Syntax) (src tgt : Lean.Name) (argInfo : ArgInfo) : 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 tgt : Lean.Name) (argInfo : ArgInfo) : Lean.CoreM (Array Lean.Name)

Copies equation lemmas and attributes from src to tgt

partial def Mathlib.Tactic.Translate.transformDecl (t : TranslateData) (cfg : Config) (src tgt : Lean.Name) (argInfo : ArgInfo := { }) : Lean.CoreM (Array Lean.Name)

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and the body using the translations dictionary.

def Mathlib.Tactic.Translate.checkExistingType (t : TranslateData) (src tgt : Lean.Name) (reorder : List (List ℕ)) (dont : List ℕ) : Lean.MetaM Unit

Verify that the type of given srcDecl translates to that of tgtDecl.

Equations

• One or more equations did not get rendered due to their size.

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).