Zulip Chat Archive

Stream: general

Topic: nat equalities


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

view this post on Zulip Bryan Gin-ge Chen (Jun 13 2019 at 13:28):

Hmm, it's working for me? web editor

view this post on Zulip Johan Commelin (Jun 13 2019 at 13:30):

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

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

view this post on Zulip Johan Commelin (Jun 13 2019 at 14:23):

What exactly does that do?

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

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

view this post on Zulip Johan Commelin (Jun 13 2019 at 14:37):

@Bryan Gin-ge Chen Brilliant! That worked!

view this post on Zulip Scott Morrison (Jun 13 2019 at 23:07):

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

view this post on Zulip Scott Morrison (Jun 13 2019 at 23:08):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 13 2019 at 23:24):

It does, but sometimes it gets the reverts wrong.

view this post on Zulip Scott Morrison (Jun 13 2019 at 23:29):

Are these bugs in omega, or an essential difficulty?

view this post on Zulip Mario Carneiro (Jun 13 2019 at 23:30):

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

view this post on Zulip Mario Carneiro (Jun 13 2019 at 23:30):

@Seul Baek

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

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

instead. I'll look into this.

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

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

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

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 14:48):

But I'm also fine with manual mode.

view this post on Zulip Johan Commelin (Jun 15 2019 at 14:48):

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

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