## Stream: maths

### Topic: nat.pow and ring

#### Kevin Buzzard (Jun 09 2018 at 01:19):

import tactic.ring

example (d : ℕ) : d ^ 2 + (2 * d + 1) = (d + 1) ^ 2 :=
begin
unfold has_pow.pow monoid.pow nat.pow,
ring
end


#### Kevin Buzzard (Jun 09 2018 at 01:19):

Could I have done that in one line with ring? [using some options or something]

#### Andrew Ashworth (Jun 09 2018 at 01:45):

[deleted - incorrect information]

#### Kevin Buzzard (Jun 09 2018 at 01:52):

So I could make an even cooler ring tactic by writing a tactic which tries to do those unfolds and then applies ring?

#### Kevin Buzzard (Jun 09 2018 at 01:52):

Is life that easy?

#### Andrew Ashworth (Jun 09 2018 at 01:58):

[deleted - incorrect information]

#### Andrew Ashworth (Jun 09 2018 at 01:59):

[deleted - incorrect information]

#### Mario Carneiro (Jun 09 2018 at 05:24):

ring should handle powers... it automatically handles ring like operations that make sense as polynomial expressions, although it can't handle x^n for nonconstant n

#### Mario Carneiro (Jun 09 2018 at 05:26):

in particular it has optimizations for sparse polynomials like x^100 + x, which requires interpreting ^

#### Andrew Ashworth (Jun 09 2018 at 06:25):

that's pretty sweet! I didn't expect that you'd put that much effort into the tactic. thanks for writing it!

#### Kevin Buzzard (Jun 09 2018 at 10:41):

Yes thanks very much indeed for writing it. It is an essential part of the "mathematician's interface" to Lean. Writing it was I'm sure nontrivial but at the end of the day, as I know I've said before, if a mathematician can't prove things like the example above with one or two lines then they will never take to Lean.

#### Kevin Buzzard (Jun 09 2018 at 10:42):

Just to be clear -- in the example above ring falls without the initial unfolding

#### Patrick Massot (Jun 09 2018 at 10:43):

The ring tactic is already very useful but it has bugs

#### Johan Commelin (Jun 09 2018 at 14:51):

How hard would it be to state a theorem about the ring tactic, and prove that the implementation is compliant? Then we are sure we won't have bugs. But I guess that the meta stuff makes this complicated.

Last updated: May 18 2021 at 08:14 UTC