## Stream: general

### Topic: nat equalities

#### Johan Commelin (Jun 13 2019 at 12:06):

i n : ℕ
hi : i ≤ n
⊢ n + 1 = i + (n - i + 1)


Should omega be able to handle these kind of things? (It failed.)
How do I make these goals go away without desperately scrolling through thousands of trivialities in nat.lean?

#### Bryan Gin-ge Chen (Jun 13 2019 at 13:28):

Hmm, it's working for me? web editor

#### Johan Commelin (Jun 13 2019 at 13:30):

Weird... within my huge crowded context it didn't work...

#### Bryan Gin-ge Chen (Jun 13 2019 at 14:21):

I guess for more control you could try:

begin
revert i n hi,
omega manual nat,
end


#### Johan Commelin (Jun 13 2019 at 14:23):

What exactly does that do?

#### Bryan Gin-ge Chen (Jun 13 2019 at 14:24):

I'm not sure of the details exactly but I found info about it here (some of this should probably be copied to the docstring, which is currently empty).

#### Bryan Gin-ge Chen (Jun 13 2019 at 14:26):

I think the idea is that omega actually works on "closed" terms and if the goal isn't one, it has to try to guess which hypotheses to revert. By using manual, you turn off the guessing.

#### Johan Commelin (Jun 13 2019 at 14:37):

@Bryan Gin-ge Chen Brilliant! That worked!

#### Scott Morrison (Jun 13 2019 at 23:07):

Why doesn't omega just revert stuff automatically if the goal is not a closed term?

#### Scott Morrison (Jun 13 2019 at 23:08):

We really shouldn't have to be calling revert manually.

#### Bryan Gin-ge Chen (Jun 13 2019 at 23:24):

It does, but sometimes it gets the reverts wrong.

#### Scott Morrison (Jun 13 2019 at 23:29):

Are these bugs in omega, or an essential difficulty?

#### Mario Carneiro (Jun 13 2019 at 23:30):

I don't see why there would be an essential difficulty

@Seul Baek

#### Scott Morrison (Jun 13 2019 at 23:32):

btw, @Bryan Gin-ge Chen, your web editor link above just gives me an error unknown identifier 'omega'

#### Bryan Gin-ge Chen (Jun 13 2019 at 23:35):

Uh oh, I updated the build of mathlib that it was using a few hours ago. It does seem like something has gone wrong, but I'm seeing:

1:0: error:
ambiguous import, it can be '/library/algebra/group/default.olean' or '/library/algebra/group.olean'
1:0: error:
invalid import: tactic.omega
could not resolve import: tactic.omega


Edit: the problem was the mk_library.py script was picking up .olean files corresponding to renamed / moved .lean files. Should be fixed now.

#### Johan Commelin (Jun 14 2019 at 05:03):

In this case I had a "very complicated" term that depended on n. It was of the form

IH : \for m, m < n, weird_poly1 m = weird_poly2 m


Maybe that tripped up omega?

#### Seul Baek (Jun 15 2019 at 14:40):

@Johan Commelin I think so. Remember that omega handles goals in presburger arithmetic, which has a pretty restricted language. You can have nat/int constants and variables, addition, multiplication with constant, comparisons, plus a bit of syntactic sugar like subtraction which is eliminated during processing. It wouldn't know what to make of weird_poly1 or weird_poly2 if it contains any symbols other than these.

#### Johan Commelin (Jun 15 2019 at 14:48):

Maybe omega could be opportunistic, and clear assumptions that fall outside the language, before reverting assumptions on which the goal depends...

#### Johan Commelin (Jun 15 2019 at 14:48):

But I'm also fine with manual mode.

#### Johan Commelin (Jun 15 2019 at 14:48):

As long as I know how to use it :wink:

#### Seul Baek (Jun 15 2019 at 14:52):

Reviewing the code, I think I know what the problem is. The preprocessor for omega isn't very careful when choosing which hypotheses to revert - it just checks that its domain (e.g. int or nat) matches the domain of the goal. So it's possible that an hypothesis has the right domain but is not actually in the language of presburger arithmetic, and causes reification to fail.

Last updated: May 08 2021 at 19:11 UTC