simp and nats

Stream: new members

[Christopher Upshaw]

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]

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

[Chris Hughes]

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]

ring may well help

[Alexander Bentkamp]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Christopher Upshaw]

Thanks!

[Christopher Upshaw]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Kevin Buzzard]

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