The @[to_dual] attribute.

The @[to_dual] attribute is used to translate declarations to their dual equivalent. See the docstrings of to_dual and to_additive for more information.

Known limitations:

• Reordering arguments of arguments is not yet supported. This usually comes up in constructors of structures. e.g. Pow.mk or OrderTop.mk
• When combining to_additive and to_dual, we need to make sure that all translations are added. For example attribute [to_dual (attr := to_additive) le_mul] mul_le should generate le_mul, le_add and add_le, and in particular should realize that le_add and add_le are dual to each other. Currently, this requires writing attribute [to_dual existing le_add] add_le.

def Mathlib.Tactic.ToDual.to_dual_ignore_args : Lean.ParserDescr

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.

Equations

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

def Mathlib.Tactic.ToDual.to_dual_do_translate : Lean.ParserDescr

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.

Equations

• Mathlib.Tactic.ToDual.to_dual_do_translate = Lean.ParserDescr.node `Mathlib.Tactic.ToDual.to_dual_do_translate 1024 (Lean.ParserDescr.nonReservedSymbol "to_dual_do_translate" false)

def Mathlib.Tactic.ToDual.to_dual_dont_translate : Lean.ParserDescr

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.

Equations

• Mathlib.Tactic.ToDual.to_dual_dont_translate = Lean.ParserDescr.node `Mathlib.Tactic.ToDual.to_dual_dont_translate 1024 (Lean.ParserDescr.nonReservedSymbol "to_dual_dont_translate" false)

def Mathlib.Tactic.ToDual.to_dual : Lean.ParserDescr

The attribute to_dual can be used to automatically transport theorems and definitions (but not inductive types and structures) to their dual version. It uses the same implementation as to_additive.

To use this attribute, just write:

@[to_dual]
theorem max_comm' {α} [LinearOrder α] (x y : α) : max x y = max y x := max_comm x y

This code will generate a theorem named min_comm'. It is also possible to manually specify the name of the new declaration:

@[to_dual le_max_left]
lemma min_le_left (a b : α) : min a b ≤ a := sorry

An existing documentation string will not be automatically used, so if the theorem or definition has a doc string, a doc string for the dual version should be passed explicitly to to_dual.

/-- The maximum is commutative. -/
@[to_dual /-- The minimum is commutative. -/]
theorem max_comm' {α} [LinearOrder α] (x y : α) : max x y = max y x := max_comm x y

Use the (reorder := ...) syntax to reorder the arguments compared to the dual declaration. This is specified using 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. For example, this is used when tagging LE.le with to_dual self (reorder := 3 4), so that a ≤ b gets transformed into b ≤ a.

Use the to_dual self syntax to mark the lemma as its own dual. This is needed if the lemma is its own dual, up to a reordering of its arguments. to_dual self (and to_dual existing) tries to autogenerate the (reorder := ...) argument, so it is usually not necessary to give it explicitly.

Use the to_dual existing syntax to use an existing dual declaration, instead of automatically generating it.

Use the (attr := ...) syntax to apply attributes to both the original and the dual version:

@[to_dual (attr := simp)] lemma min_self (a : α) : min a a = a := sorry

Equations

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

def Mathlib.Tactic.ToDual.attrTo_dual?_ : Lean.ParserDescr

The attribute to_dual can be used to automatically transport theorems and definitions (but not inductive types and structures) to their dual version. It uses the same implementation as to_additive.

To use this attribute, just write:

@[to_dual]
theorem max_comm' {α} [LinearOrder α] (x y : α) : max x y = max y x := max_comm x y

This code will generate a theorem named min_comm'. It is also possible to manually specify the name of the new declaration:

@[to_dual le_max_left]
lemma min_le_left (a b : α) : min a b ≤ a := sorry

An existing documentation string will not be automatically used, so if the theorem or definition has a doc string, a doc string for the dual version should be passed explicitly to to_dual.

/-- The maximum is commutative. -/
@[to_dual /-- The minimum is commutative. -/]
theorem max_comm' {α} [LinearOrder α] (x y : α) : max x y = max y x := max_comm x y

Use the (reorder := ...) syntax to reorder the arguments compared to the dual declaration. This is specified using 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. For example, this is used when tagging LE.le with to_dual self (reorder := 3 4), so that a ≤ b gets transformed into b ≤ a.

Use the to_dual self syntax to mark the lemma as its own dual. This is needed if the lemma is its own dual, up to a reordering of its arguments. to_dual self (and to_dual existing) tries to autogenerate the (reorder := ...) argument, so it is usually not necessary to give it explicitly.

Use the to_dual existing syntax to use an existing dual declaration, instead of automatically generating it.

Use the (attr := ...) syntax to apply attributes to both the original and the dual version:

@[to_dual (attr := simp)] lemma min_self (a : α) : min a a = a := sorry

Equations

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

opaque Mathlib.Tactic.ToDual.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.

opaque Mathlib.Tactic.ToDual.argInfoAttr : Lean.NameMapExtension Translate.ArgInfo

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

opaque Mathlib.Tactic.ToDual.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.

opaque Mathlib.Tactic.ToDual.translations : Lean.NameMapExtension Lean.Name

Maps names to their dual counterparts.

def Mathlib.Tactic.ToDual.nameDict : Std.HashMap String (List String)

Dictionary used by guessName to autogenerate names. This only transforms single name components, unlike abbreviationDict.

Note: guessName capitalizes the output according to the capitalization of the input. In order for this to work, the input should always start with a lower case letter, and the output should always start with an upper case letter.

Equations

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

def Mathlib.Tactic.ToDual.abbreviationDict : Std.HashMap String String

We need to fix a few abbreviations after applying nameDict, i.e. replacing ZeroLE by Nonneg. This dictionary contains these fixes. The input should contain entries that is in lowerCamelCase (e.g. ltzero; the initial sequence of capital letters should be lower-cased) and the output should be in UpperCamelCase (e.g. LTZero). When applying the dictionary, we lower-case the output if the input was also given in lower-case.

Equations

• Mathlib.Tactic.ToDual.abbreviationDict = Std.HashMap.ofList [("wellFoundedLT", "WellFoundedGT"), ("wellFoundedGT", "WellFoundedLT")]

def Mathlib.Tactic.ToDual.data : Translate.TranslateData

The bundle of environment extensions for to_dual

Equations

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