# 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 eachother. Currently, this requires writing `attribute [to_dual existing le_add] add_le`.

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

Instances For

source
def Mathlib.Tactic.ToDual.to_dual_relevant_arg :
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.

To indicate that there is no relevant argument, set it to a number that is out of bounds, i.e. larger than the number of arguments, e.g. `(relevant_arg := 100)`.

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.

Instances For

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

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.

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)

Instances For

source
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 := 1 2, 5 6)` swaps the first two arguments 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 to tag `LE.le` with `(reorder := 3 4)`, so that `a ≤ b` gets transformed into `b ≤ a`.

Use the `to_dual self` syntax to use the lemma as its own dual. This is often combined with the `(reorder := ...)` syntax, because a lemma is usually dual to itself only up to some reordering of its arguments.

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.

Instances For

source
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 := 1 2, 5 6)` swaps the first two arguments 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 to tag `LE.le` with `(reorder := 3 4)`, so that `a ≤ b` gets transformed into `b ≤ a`.

Use the `to_dual self` syntax to use the lemma as its own dual. This is often combined with the `(reorder := ...)` syntax, because a lemma is usually dual to itself only up to some reordering of its arguments.

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.

Instances For

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

source
opaque Mathlib.Tactic.ToDual.reorderAttr :
Lean.NameMapExtension (List (List ℕ))

An extension that stores all the declarations that need their arguments reordered when applying `@[to_dual]`. It is applied using the `to_dual (reorder := ...)` syntax.

source
opaque Mathlib.Tactic.ToDual.relevantArgAttr :
Lean.NameMapExtension ℕ

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.

To indicate that there is no relevant argument, set it to a number that is out of bounds, i.e. larger than the number of arguments, e.g. `(relevant_arg := 100)`.

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.

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

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

Maps names to their dual counterparts.

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

Instances For

source
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 []

Instances For

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

Instances For