## Stream: new members

### Topic: simp and nats

#### 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?

#### 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.

#### 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?

#### Chris Hughes (Mar 22 2019 at 20:26):

ring may well help

#### Alexander Bentkamp (Mar 22 2019 at 20:27):

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

#### 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 + ...

#### Kevin Buzzard (Mar 22 2019 at 20:27):

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

#### 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

#### 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

Thanks!

#### Christopher Upshaw (Mar 22 2019 at 23:18):

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

#### Mario Carneiro (Mar 22 2019 at 23:24):

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

#### 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

#### 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.

#### 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