Expression translation for the translation attribute.

This file implements the translation of expressions, and all of the infrastructure that is needed for it.

• TranslateData contains the information specific to the translation attribute (to_additive or to_dual)
• shouldTranslate implements the heuristic for whether or not to translate an expression.
• applyReplacementForall/applyReplacementLambda implement the expression translation.

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 : Nat) : RelevantArg

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

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

Equations

• Mathlib.Tactic.Translate.instBEqRelevantArg.beq Mathlib.Tactic.Translate.RelevantArg.noArg Mathlib.Tactic.Translate.RelevantArg.noArg = true
• Mathlib.Tactic.Translate.instBEqRelevantArg.beq (Mathlib.Tactic.Translate.RelevantArg.arg a) (Mathlib.Tactic.Translate.RelevantArg.arg b) = (a == b)
• Mathlib.Tactic.Translate.instBEqRelevantArg.beq x✝¹ x✝ = false

@[instance_reducible]

instance Mathlib.Tactic.Translate.instBEqRelevantArg : BEq RelevantArg

Equations

• Mathlib.Tactic.Translate.instBEqRelevantArg = { beq := Mathlib.Tactic.Translate.instBEqRelevantArg.beq }

@[instance_reducible]

instance Mathlib.Tactic.Translate.instInhabitedRelevantArg : Inhabited RelevantArg

Equations

• Mathlib.Tactic.Translate.instInhabitedRelevantArg = { default := Mathlib.Tactic.Translate.instInhabitedRelevantArg.default }

def Mathlib.Tactic.Translate.RelevantArg.min : RelevantArg → RelevantArg → RelevantArg

Combine two known RelevantArgs by taking the smallest value of the two. Recall that if there are multiple relevant arguments, relevant_arg is set to the smallest one.

Equations

• (Mathlib.Tactic.Translate.RelevantArg.arg x_2).min (Mathlib.Tactic.Translate.RelevantArg.arg y) = Mathlib.Tactic.Translate.RelevantArg.arg (x_2.min y)
• x✝.min Mathlib.Tactic.Translate.RelevantArg.noArg = x✝
• Mathlib.Tactic.Translate.RelevantArg.noArg.min x✝ = x✝

@[instance_reducible]

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

Equations

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

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.

• unfold : Bool

  Whether translation should be unfolded. This is used by to_dual_for.

structure Mathlib.Tactic.Translate.TranslateData : Type

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

• dontTranslateAttr : Lean.NameMapExtension Unit

  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.

• guessNameExt : GuessName.GuessNameExt

  Environment extension used for guessing the translation of a name.

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

Get the translation for the given name.

Equations

• Mathlib.Tactic.Translate.findTranslation? env t = t.translations.find? env

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

Get the translation name for the given name.

Equations

• Mathlib.Tactic.Translate.findTranslationName? env t n = Option.map (fun (x : Mathlib.Tactic.Translate.TranslationInfo) => x.translation) (Mathlib.Tactic.Translate.findTranslation? env t n)

def Mathlib.Tactic.Translate.realizeGlobalConst (c : Lean.Name) : Lean.CoreM Bool

Check if the given constant exists in the environment, also checking for reserved names. This function is based on Lean.realizeGlobalName.

Equations

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

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

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 Nat) (e : Lean.Expr) : Lean.MetaM (Lean.Expr × RelevantArg)

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.