Zulip Chat Archive

Stream: new members

Topic: simp and nats


view this post on Zulip Christopher Upshaw (Mar 22 2019 at 20:11):

So it used to be that you could use simp and unfold to simplify expresions like "succ n + (succ m * 2) ^ 2" then type classes made it so you had to use unfold to get it to work, and now it just seems immposible and you have to use exposed lemmas, which seems really ..tedious? low level? Am I missing something like "omega" in coq?

view this post on Zulip Andrew Ashworth (Mar 22 2019 at 20:22):

Nah. You could get lucky and see if linarith will close your goal. Otherwise, port of Presburger arithmetic solver welcome.

view this post on Zulip Chris Hughes (Mar 22 2019 at 20:26):

I don't think omega would handle this, because it involves multiplication.

When you say "simplify", what would you like the simplified expression to look like?

view this post on Zulip Chris Hughes (Mar 22 2019 at 20:26):

ring may well help

view this post on Zulip Alexander Bentkamp (Mar 22 2019 at 20:27):

Is this the omega that @Seul Baek has been working on?

view this post on Zulip Andrew Ashworth (Mar 22 2019 at 20:27):

omega will unfold small multiplications up to some small number, like 10 * n = n + n + n + n + n + ...

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 20:27):

Whatever the OP wants to do, surely ring will do it.

view this post on Zulip Andrew Ashworth (Mar 22 2019 at 20:28):

oh, right. you could add https://github.com/skbaek/omega to your leanpkg and see if it works

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 20:41):

import tactic.ring
open nat

example (m n : ) : succ n + (succ m * 2) ^ 2 = n + 4 * m ^ 2 + 8 * m + 5 :=
by simp [succ_eq_add_one]; ring

ring apparently won't deal with succ m so we have to change it to m + 1 first

view this post on Zulip Christopher Upshaw (Mar 22 2019 at 23:14):

Thanks!

view this post on Zulip Christopher Upshaw (Mar 22 2019 at 23:18):

How does one use ring? It doesn't seem to ever work.

view this post on Zulip Mario Carneiro (Mar 22 2019 at 23:24):

If you are proving an equality involving * and + and - and powers then ring works

view this post on Zulip Mario Carneiro (Mar 22 2019 at 23:25):

if there is stuff like nat.succ or other domain specific things then you have to get rid of them first

view this post on Zulip Simon Hudon (Mar 23 2019 at 04:04):

I think we could afford to add support specifically for nat.succ because it comes up so often.

view this post on Zulip Kevin Buzzard (Mar 23 2019 at 09:21):

Ring proves equalities. https://xenaproject.wordpress.com/2018/06/13/ab3/


Last updated: May 16 2021 at 21:11 UTC