Zulip Chat Archive

Stream: maths

Topic: nat.pow and ring


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 01:19):

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

view this post on Zulip Andrew Ashworth (Jun 09 2018 at 01:45):

[deleted - incorrect information]

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 01:52):

Is life that easy?

view this post on Zulip Andrew Ashworth (Jun 09 2018 at 01:58):

[deleted - incorrect information]

view this post on Zulip Andrew Ashworth (Jun 09 2018 at 01:59):

[deleted - incorrect information]

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 09 2018 at 05:26):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 10:42):

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

view this post on Zulip Patrick Massot (Jun 09 2018 at 10:43):

The ring tactic is already very useful but it has bugs

view this post on Zulip 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