norm_num/ ring doesn't solve this?

Stream: new members

[Vaibhav Karve]

What is the easiest way to resolve goals of the form:

example (n : ℕ) : (n + 1) * n + 2 * nat.succ n = (nat.succ n + 1) * nat.succ n :=
    sorry

So far I have tried simp, ring, omega and norm_num. None of them work. I am looking for a tactic that will resolve all statements of this type.

[Steffan]

wait a second, try rewriting succ_eq_add_one maybe

[Patrick Massot]

rw ← nat.add_one, ring,

[Patrick Massot]

The problem is nat.succ everywhere

[Steffan]

by rw succ_eq_add_one; ring done

[Patrick Massot]

Mine is shorter :stuck_out_tongue_wink:

[Steffan]

ring doesn't like succ for some reason

[Kevin Buzzard]

because succ is not a thing for general rings

[Steffan]

Mine is shorter :stuck_out_tongue_wink:

hey we're not golfing :wink:

[Kevin Buzzard]

I'm only golfing when my solution turns out to be shorter :-)

[Patrick Massot]

Same here

[Vaibhav Karve]

Thanks! Both these solutions work.

When defining new functions, I tend to write n + 1 for readability. But then simp often introduces a bunch of nat.succ into my goal and context states. Is it then best to avoid n + 1 in my definitions to begin with?

[Steffan]

@Kevin Buzzard I think "nat.succ_eq_add_one" is a bit clearer than \l nat.add_one :)

[Vaibhav Karve]

Why does refl solve n + 1 = nat.succ n? :confused:

[Patrick Massot]

Because that's the definition

[Vaibhav Karve]

I mean to ask, if it is something so simple that refl can make this rewrite then naively I would think that ring can do that rewrite too?

[Kevin Buzzard]

It's not rings job to do rewrites.

[Kevin Buzzard]

Tactics have clear domains where they work, and ring's job is to prove equalities which are true in arbitrary rings, not to guess which rewrites the user wants to do first.

[Jalex Stark]

If every tactic calls every other tactic then you never prove anything, or at least not in say 20 seconds

[Vaibhav Karve]

Thanks. I should start looking more carefully into what tactics (can/can't) do instead of treating them like a black box.

[Kevin Buzzard]

ring will prove theorems about nat.succ n because it will treat it as an atom. There might be cases when you want to treat something like it as an atom, rather than applying some rewrite.

[Kevin Buzzard]

import tactic

example (n : ℕ) : (nat.succ n)^2 = (nat.succ n) * nat.succ n :=
by ring

[Jalex Stark]

to be fair, you can learn a lot about which goals a tactic can solve while not understanding anything about its implementation

[Kevin Buzzard]

Eg you can be me

[Kevin Buzzard]

I read the documentation but I wouldn't touch the meta code