nat.pow and ring

Stream: maths

[Kevin Buzzard]

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]

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

[Andrew Ashworth]

[deleted - incorrect information]

[Kevin Buzzard]

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]

Is life that easy?

[Andrew Ashworth]

[deleted - incorrect information]

[Andrew Ashworth]

[deleted - incorrect information]

[Mario Carneiro]

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]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

The ring tactic is already very useful but it has bugs

[Johan Commelin]

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.