[Merged by Bors] - feat: arith_mult: an aesop tactic for proving IsMultiplicative statements
#9310
Conversation
FLDutchmann
added
awaiting-review
t-meta
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
FLDutchmann
added
awaiting-review
awaiting-CI
and removed
awaiting-author
There was a problem hiding this comment.
I like the way this tactic can be implemented quite easily using aesop! Although I do have a big question: wouldn't it better to use the new fun_prop system: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60fun_prop.60.20new.20tactic.20for.20Differentiable.2C.20Continuous.2C.20.2E.2E.2E
Mathlib/Tactic/Multiplicativity.lean
Outdated
| `multiplicativity` solves goals of the form `IsMultiplicative f` for `f : ArithmeticFunction R` | ||
| by applying lemmas tagged with the user attribute `multiplicativity`. -/ | ||
| macro (name := multiplicativity) "multiplicativity" c:Aesop.tactic_clause* : tactic => |
There was a problem hiding this comment.
The name sounds quite general compared to the actual scope: "multiplicative" has lots of uses like "multiplicative actions", and the Multiplicative type synonym. So maybe a more complicated name like arith_multiplicative?
There was a problem hiding this comment.
fun_prop is designed for proposition for which you have *_id, *_const, *_comp, *_apply and *_pi theorems(or subset of them). I do not see them for IsMultiplicative so I don't think it is applicable in this case.
There was a problem hiding this comment.
Sorry for the late reply - since this was still tagged awaiting-author I was expecting you might have more to say/do here.
I see why fun_prop wouldn't be appropriate for this tactic then. So the design looks good and I just have a question about the name.
Note that the tactic syntax multiplicative is not namespaced:
example : Nat.ArithmeticFunction.IsMultiplicative Nat.ArithmeticFunction.moebius := by multiplicativity
works without opening any namespace. So I really do think that a more specific name should be used.
There was a problem hiding this comment.
Sorry for the delay on my part. I agree with changing the name. How about arith_mult? multiplicativity is frankly a bit of a mouthful.
And I also think aesop is probably a little suboptimal regarding performance and code extraction, but for a tactic that won't be very widely used, it should be fine. (that is to say I am pretty excited about fun_prop, and I'm a little sad it can't be used here)
There's also a merge conflict at the moment, so I'll merge master and rename.
Vierkantor
added
awaiting-author
FLDutchmann
changed the title
multiplicativity: an aesop tactic for proving IsMultiplicative statementsarith_mult: an aesop tactic for proving IsMultiplicative statements
FLDutchmann
added
awaiting-review
awaiting-CI
and removed
awaiting-author
|
✌️ FLDutchmann can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
bors r+ |
…statements (#9310) Add a tactic that proves multiplicativity of arithmetic functions using Aesop by applying structural lemmas, akin to the `continuity` and `measurability` tactics. Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
arith_mult: an aesop tactic for proving IsMultiplicative statementsarith_mult: an aesop tactic for proving IsMultiplicative statements
…statements (#9310) Add a tactic that proves multiplicativity of arithmetic functions using Aesop by applying structural lemmas, akin to the `continuity` and `measurability` tactics. Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>
…statements (#9310) Add a tactic that proves multiplicativity of arithmetic functions using Aesop by applying structural lemmas, akin to the `continuity` and `measurability` tactics. Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>
…statements (#9310) Add a tactic that proves multiplicativity of arithmetic functions using Aesop by applying structural lemmas, akin to the `continuity` and `measurability` tactics. Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>
…statements (#9310) Add a tactic that proves multiplicativity of arithmetic functions using Aesop by applying structural lemmas, akin to the `continuity` and `measurability` tactics. Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>
…statements (#9310) Add a tactic that proves multiplicativity of arithmetic functions using Aesop by applying structural lemmas, akin to the `continuity` and `measurability` tactics. Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>
Add a tactic that proves multiplicativity of arithmetic functions using Aesop by applying structural lemmas, akin to the
continuityandmeasurabilitytactics.