Zulip Chat Archive

Stream: new members

Topic: norm_num/ ring doesn't solve this?


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

view this post on Zulip Steffan (May 02 2020 at 19:56):

wait a second, try rewriting succ_eq_add_one maybe

view this post on Zulip Patrick Massot (May 02 2020 at 19:56):

rw ← nat.add_one, ring,

view this post on Zulip Patrick Massot (May 02 2020 at 19:57):

The problem is nat.succ everywhere

view this post on Zulip Steffan (May 02 2020 at 19:57):

by rw succ_eq_add_one; ring done

view this post on Zulip Patrick Massot (May 02 2020 at 19:58):

Mine is shorter :stuck_out_tongue_wink:

view this post on Zulip Steffan (May 02 2020 at 19:58):

ring doesn't like succ for some reason

view this post on Zulip Kevin Buzzard (May 02 2020 at 19:58):

because succ is not a thing for general rings

view this post on Zulip Steffan (May 02 2020 at 19:59):

Mine is shorter :stuck_out_tongue_wink:

hey we're not golfing :wink:

view this post on Zulip Kevin Buzzard (May 02 2020 at 20:00):

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

view this post on Zulip Patrick Massot (May 02 2020 at 20:00):

Same here

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

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

view this post on Zulip Vaibhav Karve (May 02 2020 at 20:07):

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

view this post on Zulip Patrick Massot (May 02 2020 at 20:08):

Because that's the definition

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

view this post on Zulip Kevin Buzzard (May 02 2020 at 20:13):

It's not rings job to do rewrites.

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

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

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

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

view this post on Zulip Kevin Buzzard (May 02 2020 at 20:17):

import tactic

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

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

view this post on Zulip Kevin Buzzard (May 02 2020 at 21:22):

Eg you can be me

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