Documentation

Mathlib.Tactic.Translate.ToDual

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:

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.

    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.
    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
      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.argInfoAttr :
            Lean.NameMapExtension Translate.ArgInfo

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

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