From 2f4156e1918b1bb532f463d6838dd7e1d5715b22 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 22 Dec 2024 16:53:08 +0000 Subject: [PATCH] feat(to_additive): option to not translate operations on a type (#19297) * Also some cleanup in the `ToAdditive/Frontend` file (please review the first 3 commits separately), only the second commit actually changes the functionality of `to_additive`. The main cleanups: move doc-strings to the syntax declarations, remove the module doc which was just duplicating the `to_additive`-doc, and let a few internal functions depend on `Environment` instead of multiple other arguments. * In #19687 this is done for `Monoid.End` (in a separate PR, since that requires some library fixes). --- Mathlib/Tactic/ToAdditive/Frontend.lean | 457 +++++++----------------- MathlibTest/toAdditive.lean | 28 +- 2 files changed, 154 insertions(+), 331 deletions(-) diff --git a/Mathlib/Tactic/ToAdditive/Frontend.lean b/Mathlib/Tactic/ToAdditive/Frontend.lean index 6ff136a85b869..7d4f031891763 100644 --- a/Mathlib/Tactic/ToAdditive/Frontend.lean +++ b/Mathlib/Tactic/ToAdditive/Frontend.lean @@ -23,7 +23,84 @@ import Mathlib.Tactic.Simps.Basic /-! # The `@[to_additive]` attribute. -The attribute `to_additive` can be used to automatically transport theorems +Implementation of the `to_additive` attribute. +See the docstring of `ToAdditive.to_additive` for more information +-/ + +open Lean Meta Elab Command Std + +namespace ToAdditive + +/-- An attribute that tells `@[to_additive]` that certain arguments of this definition are not +involved when using `@[to_additive]`. +This helps the heuristic of `@[to_additive]` by also transforming definitions if `ℕ` or another +fixed type occurs as one of these arguments. -/ +syntax (name := to_additive_ignore_args) "to_additive_ignore_args" (ppSpace num)* : attr + +/-- An attribute that is automatically added to declarations tagged with `@[to_additive]`, +if needed. + +This attribute tells which argument is the type where this declaration uses the multiplicative +structure. If there are multiple argument, we typically tag the first one. +If this argument contains a fixed type, this declaration will note be additivized. +See the Heuristics section of `to_additive.attr` for more details. + +If a declaration is not tagged, it is presumed that the first argument is relevant. +`@[to_additive]` uses the function `to_additive.first_multiplicative_arg` to automatically tag +declarations. It is ok to update it manually if the automatic tagging made an error. + +Implementation note: we only allow exactly 1 relevant argument, even though some declarations +(like `prod.group`) have multiple arguments with a multiplicative structure on it. +The reason is that whether we additivize a declaration is an all-or-nothing decision, and if +we will not be able to additivize declarations that (e.g.) talk about multiplication on `ℕ × α` +anyway. + +Warning: interactions between this and the `(reorder := ...)` argument are not well-tested. -/ +syntax (name := to_additive_relevant_arg) "to_additive_relevant_arg " num : attr + +/-- An attribute that stores all the declarations that needs their arguments reordered when +applying `@[to_additive]`. It is applied automatically by the `(reorder := ...)` syntax of +`to_additive`, and should not usually be added manually. -/ +syntax (name := to_additive_reorder) "to_additive_reorder " (num+),+ : attr + +/-- 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 `to_additive_change_numeral` attribute. + +`@[to_additive_change_numeral n₁ ...]` should be added to all functions that take one or more +numerals as argument that should be changed if `additiveTest` 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). -/ +syntax (name := to_additive_change_numeral) "to_additive_change_numeral" (ppSpace num)* : attr + +/-- The `to_additive_dont_translate` attribute, used to specify types that should be translated by +`to_additive`, but its operations should remain multiplicative. + +Usage notes: +* Apply this together with the `to_additive` attribute. +* The name generation of `to_additive` is not aware that the operations on this type should not be + translated, so you generally have to specify the name itself, if the name should remain + multiplicative. +-/ +syntax (name := to_additive_dont_translate) "to_additive_dont_translate" : attr + +/-- An `attr := ...` option for `to_additive`. -/ +syntax toAdditiveAttrOption := &"attr" " := " Parser.Term.attrInstance,* +/-- A `reorder := ...` option for `to_additive`. -/ +syntax toAdditiveReorderOption := &"reorder" " := " (num+),+ +/-- Options to `to_additive`. -/ +syntax toAdditiveParenthesizedOption := "(" toAdditiveAttrOption <|> toAdditiveReorderOption ")" +/-- Options to `to_additive`. -/ +syntax toAdditiveOption := toAdditiveParenthesizedOption <|> &"existing" +/-- Remaining arguments of `to_additive`. -/ +syntax toAdditiveRest := (ppSpace toAdditiveOption)* (ppSpace ident)? (ppSpace str)? + +/-- The attribute `to_additive` can be used to automatically transport theorems and definitions (but not inductive types and structures) from a multiplicative theory to an additive theory. @@ -117,6 +194,7 @@ There are some exceptions to this heuristic: * Identifiers that have the `@[to_additive]` attribute are ignored. For example, multiplication in `↥Semigroup` is replaced by addition in `↥AddSemigroup`. + You can turn this behavior off by *also* adding the `@[to_additive_dont_translate]` attribute. * If an identifier `d` has attribute `@[to_additive_relevant_arg n]` then the argument in position `n` is checked for a fixed type, instead of checking the first argument. `@[to_additive]` will automatically add the attribute `@[to_additive_relevant_arg n]` to a @@ -230,34 +308,10 @@ In this case `to_additive` adds all structure fields to its mapping. new name as is. As a safety check, in the first case `to_additive` double checks -that the new name differs from the original one. - --/ - -open Lean Meta Elab Command Std - -/-- The `to_additive_ignore_args` attribute. -/ -syntax (name := to_additive_ignore_args) "to_additive_ignore_args" (ppSpace num)* : attr -/-- The `to_additive_relevant_arg` attribute. -/ -syntax (name := to_additive_relevant_arg) "to_additive_relevant_arg " num : attr -/-- The `to_additive_reorder` attribute. -/ -syntax (name := to_additive_reorder) "to_additive_reorder " (num+),+ : attr -/-- The `to_additive_change_numeral` attribute. -/ -syntax (name := to_additive_change_numeral) "to_additive_change_numeral" (ppSpace num)* : attr -/-- An `attr := ...` option for `to_additive`. -/ -syntax toAdditiveAttrOption := &"attr" " := " Parser.Term.attrInstance,* -/-- A `reorder := ...` option for `to_additive`. -/ -syntax toAdditiveReorderOption := &"reorder" " := " (num+),+ -/-- Options to `to_additive`. -/ -syntax toAdditiveParenthesizedOption := "(" toAdditiveAttrOption <|> toAdditiveReorderOption ")" -/-- Options to `to_additive`. -/ -syntax toAdditiveOption := toAdditiveParenthesizedOption <|> &"existing" -/-- Remaining arguments of `to_additive`. -/ -syntax toAdditiveRest := (ppSpace toAdditiveOption)* (ppSpace ident)? (ppSpace str)? -/-- The `to_additive` attribute. -/ +that the new name differs from the original one. -/ syntax (name := to_additive) "to_additive" "?"? toAdditiveRest : attr -/-- The `to_additive` attribute. -/ +@[inherit_doc to_additive] macro "to_additive?" rest:toAdditiveRest : attr => `(attr| to_additive ? $rest) /-- A set of strings of names that end in a capital letter. @@ -274,15 +328,14 @@ def endCapitalNames : Lean.RBMap String (List String) compare := -- endCapitalNamesOfList ["LE", "LT", "WF", "CoeTC", "CoeT", "CoeHTCT"] .ofList [("LE", [""]), ("LT", [""]), ("WF", [""]), ("Coe", ["TC", "T", "HTCT"])] -/-- -This function takes a String and splits it into separate parts based on the following +open String in +/-- This function takes a String and splits it into separate parts based on the following (naming conventions)[https://github.com/leanprover-community/mathlib4/wiki#naming-convention]. E.g. `#eval "InvHMulLEConjugate₂SMul_ne_top".splitCase` yields -`["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]`. --/ -partial def String.splitCase (s : String) (i₀ : Pos := 0) (r : List String := []) : List String := -Id.run do +`["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]`. -/ +partial def _root_.String.splitCase (s : String) (i₀ : Pos := 0) (r : List String := []) : + List String := Id.run do -- We test if we need to split between `i₀` and `i₁`. let i₁ := s.next i₀ if s.atEnd i₁ then @@ -305,8 +358,6 @@ Id.run do return splitCase (s.extract i₁ s.endPos) 0 <| (s.extract 0 i₁)::r return splitCase s i₁ r -namespace ToAdditive - initialize registerTraceClass `to_additive initialize registerTraceClass `to_additive_detail @@ -336,12 +387,7 @@ register_option linter.toAdditiveExisting : Bool := { the additive declaration already exists" } -/-- -An attribute that tells `@[to_additive]` that certain arguments of this definition are not -involved when using `@[to_additive]`. -This helps the heuristic of `@[to_additive]` by also transforming definitions if `ℕ` or another -fixed type occurs as one of these arguments. --/ +@[inherit_doc to_additive_ignore_args] initialize ignoreArgsAttr : NameMapExtension (List Nat) ← registerNameMapAttribute { name := `to_additive_ignore_args @@ -353,11 +399,7 @@ initialize ignoreArgsAttr : NameMapExtension (List Nat) ← | _ => throwUnsupportedSyntax return ids.toList } -/-- -An attribute that stores all the declarations that needs their arguments reordered when -applying `@[to_additive]`. It is applied automatically by the `(reorder := ...)` syntax of -`to_additive`, and should not usually be added manually. --/ +@[inherit_doc to_additive_reorder] initialize reorderAttr : NameMapExtension (List <| List Nat) ← registerNameMapAttribute { name := `to_additive_reorder @@ -375,26 +417,7 @@ initialize reorderAttr : NameMapExtension (List <| List Nat) ← pure <| reorders.toList.map (·.toList.map (·.raw.isNatLit?.get! - 1)) | _, _ => throwUnsupportedSyntax } -/-- -An attribute that is automatically added to declarations tagged with `@[to_additive]`, if needed. - -This attribute tells which argument is the type where this declaration uses the multiplicative -structure. If there are multiple argument, we typically tag the first one. -If this argument contains a fixed type, this declaration will note be additivized. -See the Heuristics section of `to_additive.attr` for more details. - -If a declaration is not tagged, it is presumed that the first argument is relevant. -`@[to_additive]` uses the function `to_additive.first_multiplicative_arg` to automatically tag -declarations. It is ok to update it manually if the automatic tagging made an error. - -Implementation note: we only allow exactly 1 relevant argument, even though some declarations -(like `prod.group`) have multiple arguments with a multiplicative structure on it. -The reason is that whether we additivize a declaration is an all-or-nothing decision, and if -we will not be able to additivize declarations that (e.g.) talk about multiplication on `ℕ × α` -anyway. - -Warning: interactions between this and the `(reorder := ...)` argument are not well-tested. --/ +@[inherit_doc to_additive_relevant_arg] initialize relevantArgAttr : NameMapExtension Nat ← registerNameMapAttribute { name := `to_additive_relevant_arg @@ -404,21 +427,17 @@ initialize relevantArgAttr : NameMapExtension Nat ← | _, `(attr| to_additive_relevant_arg $id) => pure <| id.1.isNatLit?.get!.pred | _, _ => throwUnsupportedSyntax } -/-- -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 `to_additive_change_numeral` attribute. +@[inherit_doc to_additive_dont_translate] +initialize dontTranslateAttr : NameMapExtension Unit ← + registerNameMapAttribute { + name := `to_additive_dont_translate + descr := "Auxiliary attribute for `to_additive` stating \ + that the operations on this type should not be translated." + add := fun + | _, `(attr| to_additive_dont_translate) => return + | _, _ => throwUnsupportedSyntax } -`@[to_additive_change_numeral n₁ ...]` should be added to all functions that take one or more -numerals as argument that should be changed if `additiveTest` 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). --/ +@[inherit_doc to_additive_change_numeral] initialize changeNumeralAttr : NameMapExtension (List Nat) ← registerNameMapAttribute { name := `to_additive_change_numeral @@ -476,19 +495,20 @@ structure Config : Type where deriving Repr /-- Implementation function for `additiveTest`. - We cache previous applications of the function, using an expression cache using ptr equality - to avoid visiting the same subexpression many times. Note that we only need to cache the - expressions without taking the value of `inApp` into account, since `inApp` only matters when - the expression is a constant. However, for this reason we have to make sure that we never - cache constant expressions, so that's why the `if`s in the implementation are in this order. - - Note that this function is still called many times by `applyReplacementFun` - and we're not remembering the cache between these calls. -/ -unsafe def additiveTestUnsafe (findTranslation? : Name → Option Name) - (ignore : Name → Option (List ℕ)) (e : Expr) : Option Name := +Failure means that in that subexpression there is no constant that blocks `e` from being translated. +We cache previous applications of the function, using an expression cache using ptr equality +to avoid visiting the same subexpression many times. Note that we only need to cache the +expressions without taking the value of `inApp` into account, since `inApp` only matters when +the expression is a constant. However, for this reason we have to make sure that we never +cache constant expressions, so that's why the `if`s in the implementation are in this order. + +Note that this function is still called many times by `applyReplacementFun` +and we're not remembering the cache between these calls. -/ +unsafe def additiveTestUnsafe (env : Environment) (e : Expr) : Option Name := let rec visit (e : Expr) (inApp := false) : OptionT (StateM (PtrSet Expr)) Name := do if e.isConst then - if inApp || (findTranslation? e.constName).isSome then + if (dontTranslateAttr.find? env e.constName).isNone && + (inApp || (findTranslation? env e.constName).isSome) then failure else return e.constName @@ -501,7 +521,7 @@ unsafe def additiveTestUnsafe (findTranslation? : Name → Option Name) -- make sure that we don't treat `(fun x => α) (n + 1)` as a type that depends on `Nat` guard !x.isConstantApplication if let some n := e.getAppFn.constName? then - if let some l := ignore n then + if let some l := ignoreArgsAttr.find? env n then if e.getAppNumArgs + 1 ∈ l then failure visit a @@ -513,18 +533,15 @@ unsafe def additiveTestUnsafe (findTranslation? : Name → Option Name) | _ => failure Id.run <| (visit e).run' mkPtrSet -/-- -`additiveTest e` tests whether the expression `e` contains a constant +/-- `additiveTest 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 in `@[to_additive]` for deciding which subexpressions to transform: we only transform -constants if `additiveTest` applied to their first argument returns `true`. +constants if `additiveTest` 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`. --/ -def additiveTest (findTranslation? : Name → Option Name) - (ignore : Name → Option (List ℕ)) (e : Expr) : Option Name := - unsafe additiveTestUnsafe findTranslation? ignore e +We ignore all arguments specified by the `ignore` `NameMap`. -/ +def additiveTest (env : Environment) (e : Expr) : Option Name := + unsafe additiveTestUnsafe env e /-- Swap the first two elements of a list -/ def _root_.List.swapFirstTwo {α : Type _} : List α → List α @@ -549,24 +566,18 @@ 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]`. -/ -def applyReplacementFun (e : Expr) : MetaM Expr := do - let env ← getEnv +def applyReplacementFun (e : Expr) : MetaM Expr := + return aux (← getEnv) (← getBoolOption `trace.to_additive_detail) e +where /-- Implementation of `applyReplacementFun`. -/ + aux (env : Environment) (trace : Bool) : Expr → Expr := let reorderFn : Name → List (List ℕ) := fun nm ↦ (reorderAttr.find? env nm |>.getD []) let relevantArg : Name → ℕ := fun nm ↦ (relevantArgAttr.find? env nm).getD 0 - return aux - (findTranslation? <| ← getEnv) reorderFn (ignoreArgsAttr.find? env) - (changeNumeralAttr.find? env) relevantArg (← getBoolOption `trace.to_additive_detail) e -where /-- Implementation of `applyReplacementFun`. -/ - aux (findTranslation? : Name → Option Name) - (reorderFn : Name → List (List ℕ)) (ignore : Name → Option (List ℕ)) - (changeNumeral? : Name → Option (List Nat)) (relevantArg : Name → ℕ) (trace : Bool) : - Expr → Expr := Lean.Expr.replaceRec fun r e ↦ Id.run do if trace then dbg_trace s!"replacing at {e}" match e with | .const n₀ ls₀ => do - let n₁ := n₀.mapPrefix findTranslation? + let n₁ := n₀.mapPrefix <| findTranslation? env let ls₁ : List Level := if 0 ∈ (reorderFn n₀).flatten then ls₀.swapFirstTwo else ls₀ if trace then if n₀ != n₁ then @@ -589,7 +600,8 @@ where /-- Implementation of `applyReplacementFun`. -/ let relevantArgId := relevantArg nm let gfAdditive := if relevantArgId < gAllArgs.size && gf.isConst then - if let some fxd := additiveTest findTranslation? ignore gAllArgs[relevantArgId]! then + if let some fxd := + additiveTest env gAllArgs[relevantArgId]! then Id.run <| do if trace then dbg_trace s!"The application of {nm} contains the fixed type \ @@ -602,14 +614,14 @@ where /-- Implementation of `applyReplacementFun`. -/ /- Test if arguments should be reordered. -/ let reorder := reorderFn nm if !reorder.isEmpty && relevantArgId < gAllArgs.size && - (additiveTest findTranslation? ignore gAllArgs[relevantArgId]!).isNone then + (additiveTest env gAllArgs[relevantArgId]!).isNone then gAllArgs := gAllArgs.permute! reorder if trace then dbg_trace s!"reordering the arguments of {nm} using the cyclic permutations {reorder}" /- Do not replace numerals in specific types. -/ let firstArg := gAllArgs[0]! - if let some changedArgNrs := changeNumeral? nm then - if additiveTest findTranslation? ignore firstArg |>.isNone then + if let some changedArgNrs := changeNumeralAttr.find? env nm then + if additiveTest env firstArg |>.isNone then if trace then dbg_trace s!"applyReplacementFun: We change the numerals in this expression. \ However, we will still recurse into all the non-numeral arguments." @@ -626,7 +638,7 @@ where /-- Implementation of `applyReplacementFun`. -/ pure (← r gf, ← gAllArgs.mapM r) return some <| mkAppN gfAdditive gAllArgsAdditive | .proj n₀ idx e => do - let n₁ := n₀.mapPrefix findTranslation? + let n₁ := n₀.mapPrefix <| findTranslation? env if trace then dbg_trace s!"applyReplacementFun: in projection {e}.{idx} of type {n₀}, \ replace type with {n₁}" @@ -1301,217 +1313,6 @@ partial def addToAdditiveAttr (src : Name) (cfg : Config) (kind := AttributeKind end -/-- -The attribute `to_additive` can be used to automatically transport theorems -and definitions (but not inductive types and structures) from a multiplicative -theory to an additive theory. - -To use this attribute, just write: - -``` -@[to_additive] -theorem mul_comm' {α} [CommSemigroup α] (x y : α) : x * y = y * x := mul_comm x y -``` - -This code will generate a theorem named `add_comm'`. It is also -possible to manually specify the name of the new declaration: - -``` -@[to_additive add_foo] -theorem foo := 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 additive version should be passed explicitly to -`to_additive`. - -``` -/-- Multiplication is commutative -/ -@[to_additive "Addition is commutative"] -theorem mul_comm' {α} [CommSemigroup α] (x y : α) : x * y = y * x := CommSemigroup.mul_comm -``` - -The transport tries to do the right thing in most cases using several -heuristics described below. However, in some cases it fails, and -requires manual intervention. - -Use the `(reorder := ...)` syntax to reorder the arguments in the generated additive 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. This is mostly useful to translate declarations using -`Pow` to those using `SMul`. - -Use the `(attr := ...)` syntax to apply attributes to both the multiplicative and the additive -version: - -``` -@[to_additive (attr := simp)] lemma mul_one' {G : Type*} [Group G] (x : G) : x * 1 = x := mul_one x -``` - -For `simps` this also ensures that some generated lemmas are added to the additive dictionary. -`@[to_additive (attr := to_additive)]` is a special case, where the `to_additive` -attribute is added to the generated lemma only, to additivize it again. -This is useful for lemmas about `Pow` to generate both lemmas about `SMul` and `VAdd`. Example: -``` -@[to_additive (attr := to_additive VAdd_lemma, simp) SMul_lemma] -lemma Pow_lemma ... := -``` -In the above example, the `simp` is added to all 3 lemmas. All other options to `to_additive` -(like the generated name or `(reorder := ...)`) are not passed down, -and can be given manually to each individual `to_additive` call. - -## Implementation notes - -The transport process generally works by taking all the names of -identifiers appearing in the name, type, and body of a declaration and -creating a new declaration by mapping those names to additive versions -using a simple string-based dictionary and also using all declarations -that have previously been labeled with `to_additive`. - -In the `mul_comm'` example above, `to_additive` maps: -* `mul_comm'` to `add_comm'`, -* `CommSemigroup` to `AddCommSemigroup`, -* `x * y` to `x + y` and `y * x` to `y + x`, and -* `CommSemigroup.mul_comm'` to `AddCommSemigroup.add_comm'`. - -### Heuristics - -`to_additive` uses heuristics to determine whether a particular identifier has to be -mapped to its additive version. The basic heuristic is - -* Only map an identifier to its additive version if its first argument doesn't - contain any unapplied identifiers. - -Examples: -* `@Mul.mul Nat n m` (i.e. `(n * m : Nat)`) will not change to `+`, since its - first argument is `Nat`, an identifier not applied to any arguments. -* `@Mul.mul (α × β) x y` will change to `+`. It's first argument contains only the identifier - `Prod`, but this is applied to arguments, `α` and `β`. -* `@Mul.mul (α × Int) x y` will not change to `+`, since its first argument contains `Int`. - -The reasoning behind the heuristic is that the first argument is the type which is "additivized", -and this usually doesn't make sense if this is on a fixed type. - -There are some exceptions to this heuristic: - -* Identifiers that have the `@[to_additive]` attribute are ignored. - For example, multiplication in `↥Semigroup` is replaced by addition in `↥AddSemigroup`. -* If an identifier `d` has attribute `@[to_additive_relevant_arg n]` then the argument - in position `n` is checked for a fixed type, instead of checking the first argument. - `@[to_additive]` will automatically add the attribute `@[to_additive_relevant_arg n]` to a - declaration when the first argument has no multiplicative type-class, but argument `n` does. -* If an identifier has attribute `@[to_additive_ignore_args n1 n2 ...]` then all the arguments in - positions `n1`, `n2`, ... will not be checked for unapplied identifiers (start counting from 1). - For example, `ContMDiffMap` has attribute `@[to_additive_ignore_args 21]`, which means - that its 21st argument `(n : WithTop ℕ)` can contain `ℕ` - (usually in the form `Top.top ℕ ...`) and still be additivized. - So `@Mul.mul (C^∞⟮I, N; I', G⟯) _ f g` will be additivized. - -### Troubleshooting - -If `@[to_additive]` fails because the additive declaration raises a type mismatch, there are -various things you can try. -The first thing to do is to figure out what `@[to_additive]` did wrong by looking at the type -mismatch error. - -* Option 1: The most common case is that it didn't additivize a declaration that should be - additivized. This happened because the heuristic applied, and the first argument contains a - fixed type, like `ℕ` or `ℝ`. However, the heuristic misfires on some other declarations. - Solutions: - * First figure out what the fixed type is in the first argument of the declaration that didn't - get additivized. Note that this fixed type can occur in implicit arguments. If manually finding - it is hard, you can run `set_option trace.to_additive_detail true` and search the output for the - fragment "contains the fixed type" to find what the fixed type is. - * If the fixed type has an additive counterpart (like `↥Semigroup`), give it the `@[to_additive]` - attribute. - * If the fixed type has nothing to do with algebraic operations (like `TopCat`), add the attribute - `@[to_additive existing Foo]` to the fixed type `Foo`. - * If the fixed type occurs inside the `k`-th argument of a declaration `d`, and the - `k`-th argument is not connected to the multiplicative structure on `d`, consider adding - attribute `[to_additive_ignore_args k]` to `d`. - Example: `ContMDiffMap` ignores the argument `(n : WithTop ℕ)` -* Option 2: It additivized a declaration `d` that should remain multiplicative. Solution: - * Make sure the first argument of `d` is a type with a multiplicative structure. If not, can you - reorder the (implicit) arguments of `d` so that the first argument becomes a type with a - multiplicative structure (and not some indexing type)? - The reason is that `@[to_additive]` doesn't additivize declarations if their first argument - contains fixed types like `ℕ` or `ℝ`. See section Heuristics. - If the first argument is not the argument with a multiplicative type-class, `@[to_additive]` - should have automatically added the attribute `@[to_additive_relevant_arg]` to the declaration. - You can test this by running the following (where `d` is the full name of the declaration): - ``` - open Lean in run_cmd logInfo m!"{ToAdditive.relevantArgAttr.find? (← getEnv) `d}" - ``` - The expected output is `n` where the `n`-th (0-indexed) argument of `d` is a type (family) - with a multiplicative structure on it. `none` means `0`. - If you get a different output (or a failure), you could add the attribute - `@[to_additive_relevant_arg n]` manually, where `n` is an (1-indexed) argument with a - multiplicative structure. -* Option 3: Arguments / universe levels are incorrectly ordered in the additive version. - This likely only happens when the multiplicative declaration involves `pow`/`^`. Solutions: - * Ensure that the order of arguments of all relevant declarations are the same for the - multiplicative and additive version. This might mean that arguments have an "unnatural" order - (e.g. `Monoid.npow n x` corresponds to `x ^ n`, but it is convenient that `Monoid.npow` has this - argument order, since it matches `AddMonoid.nsmul n x`. - * If this is not possible, add `(reorder := ...)` argument to `to_additive`. - -If neither of these solutions work, and `to_additive` is unable to automatically generate the -additive version of a declaration, manually write and prove the additive version. -Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to -`multiplicative G`. -Afterwards, apply the attribute manually: - -``` -attribute [to_additive foo_add_bar] foo_bar -``` - -This will allow future uses of `to_additive` to recognize that -`foo_bar` should be replaced with `foo_add_bar`. - -### Handling of hidden definitions - -Before transporting the “main” declaration `src`, `to_additive` first -scans its type and value for names starting with `src`, and transports -them. This includes auxiliary definitions like `src._match_1`, -`src._proof_1`. - -In addition to transporting the “main” declaration, `to_additive` transports -its equational lemmas and tags them as equational lemmas for the new declaration. - -### Structure fields and constructors - -If `src` is a structure, then the additive version has to be already written manually. -In this case `to_additive` adds all structure fields to its mapping. - -### Name generation - -* If `@[to_additive]` is called without a `name` argument, then the - new name is autogenerated. First, it takes the longest prefix of - the source name that is already known to `to_additive`, and replaces - this prefix with its additive counterpart. Second, it takes the last - part of the name (i.e., after the last dot), and replaces common - name parts (“mul”, “one”, “inv”, “prod”) with their additive versions. - -* [todo] Namespaces can be transformed using `map_namespace`. For example: - ``` - run_cmd to_additive.map_namespace `QuotientGroup `QuotientAddGroup - ``` - - Later uses of `to_additive` on declarations in the `QuotientGroup` - namespace will be created in the `QuotientAddGroup` namespaces. - -* If `@[to_additive]` is called with a `name` argument `new_name` - /without a dot/, then `to_additive` updates the prefix as described - above, then replaces the last part of the name with `new_name`. - -* If `@[to_additive]` is called with a `name` argument - `NewNamespace.new_name` /with a dot/, then `to_additive` uses this - new name as is. - -As a safety check, in the first case `to_additive` double checks -that the new name differs from the original one. - --/ initialize registerBuiltinAttribute { name := `to_additive descr := "Transport multiplicative to additive" @@ -1521,5 +1322,3 @@ initialize registerBuiltinAttribute { } end ToAdditive - -set_option linter.style.longFile 1700 diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean index 777f544504921..91b979c8d8095 100644 --- a/MathlibTest/toAdditive.lean +++ b/MathlibTest/toAdditive.lean @@ -192,7 +192,8 @@ def fixedNumeralTest {α} [One α] := def fixedNumeralTest2 {α} [One α] := @OfNat.ofNat ((fun _ => ℕ) (1 : α)) 1 (@One.toOfNat1 ((fun _ => ℕ) (1 : α)) _) -/-! Test the namespace bug (https://github.com/leanprover-community/mathlib4/pull/8733). This code should *not* generate a lemma +/-! Test the namespace bug (https://github.com/leanprover-community/mathlib4/pull/8733). +This code should *not* generate a lemma `add_some_def.in_namespace`. -/ def some_def.in_namespace : Bool := false @@ -206,7 +207,8 @@ instance : One (myFin n) := ⟨(1 : ℕ)⟩ @[to_additive bar] def myFin.foo : myFin (n+1) := 1 -/-- We can pattern-match with `1`, which creates a term with a pure nat literal. See https://github.com/leanprover-community/mathlib4/pull/2046 -/ +/-- We can pattern-match with `1`, which creates a term with a pure nat literal. +See https://github.com/leanprover-community/mathlib4/pull/2046 -/ @[to_additive] def mul_foo {α} [Monoid α] (a : α) : ℕ → α | 0 => 1 @@ -337,6 +339,28 @@ run_cmd do unless !(q((fun x => x) 3) : Q(Nat)).isConstantApplication do throwError "3" unless (q((fun _ => 5) 3) : Q(Nat)).isConstantApplication do throwError "4" +@[to_additive, to_additive_dont_translate] +def MonoidEnd : Type := Unit + +run_cmd do + let stx ← `(Semigroup MonoidEnd) + liftTermElabM do + let e ← Term.elabTerm stx none + guard <| additiveTest (← getEnv) e == some `Test.MonoidEnd + + +@[to_additive instSemiGroupAddMonoidEnd] +instance : Semigroup MonoidEnd where + mul _ _ := () + mul_assoc _ _ _ := rfl + +@[to_additive] +lemma monoidEnd_lemma (x y z : MonoidEnd) : x * (y * z) = (x * y) * z := mul_assoc .. |>.symm + +/-- info: Test.addMonoidEnd_lemma (x y z : AddMonoidEnd) : x * (y * z) = x * y * z -/ +#guard_msgs in +#check addMonoidEnd_lemma + /-! Some arbitrary tests to check whether additive names are guessed correctly. -/