## Stream: new members

### Topic: norm_num/ ring doesn't solve this?

#### Vaibhav Karve (May 02 2020 at 19:53):

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 (May 02 2020 at 19:56):

wait a second, try rewriting succ_eq_add_one maybe

#### Patrick Massot (May 02 2020 at 19:56):

rw ← nat.add_one, ring,

#### Patrick Massot (May 02 2020 at 19:57):

The problem is nat.succ everywhere

#### Steffan (May 02 2020 at 19:57):

by rw succ_eq_add_one; ring done

#### Patrick Massot (May 02 2020 at 19:58):

Mine is shorter :stuck_out_tongue_wink:

#### Steffan (May 02 2020 at 19:58):

ring doesn't like succ for some reason

#### Kevin Buzzard (May 02 2020 at 19:58):

because succ is not a thing for general rings

#### Steffan (May 02 2020 at 19:59):

Mine is shorter :stuck_out_tongue_wink:

hey we're not golfing :wink:

#### Kevin Buzzard (May 02 2020 at 20:00):

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

Same here

#### Vaibhav Karve (May 02 2020 at 20:02):

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 (May 02 2020 at 20:04):

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

#### Vaibhav Karve (May 02 2020 at 20:07):

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

#### Patrick Massot (May 02 2020 at 20:08):

Because that's the definition

#### Vaibhav Karve (May 02 2020 at 20:08):

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 (May 02 2020 at 20:13):

It's not rings job to do rewrites.

#### Kevin Buzzard (May 02 2020 at 20:15):

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 (May 02 2020 at 20:15):

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

#### Vaibhav Karve (May 02 2020 at 20:16):

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

#### Kevin Buzzard (May 02 2020 at 20:17):

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 (May 02 2020 at 20:17):

import tactic

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


#### Jalex Stark (May 02 2020 at 20:20):

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

Eg you can be me

#### Kevin Buzzard (May 02 2020 at 21:23):

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

Last updated: May 14 2021 at 23:14 UTC