nat equalities

Stream: general

[Johan Commelin]

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]

Hmm, it's working for me? web editor

[Johan Commelin]

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

[Bryan Gin-ge Chen]

I guess for more control you could try:

begin
  revert i n hi,
  omega manual nat,
end

[Johan Commelin]

What exactly does that do?

[Bryan Gin-ge Chen]

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]

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]

@Bryan Gin-ge Chen Brilliant! That worked!

[Scott Morrison]

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

[Scott Morrison]

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

[Bryan Gin-ge Chen]

It does, but sometimes it gets the reverts wrong.

[Scott Morrison]

Are these bugs in omega, or an essential difficulty?

[Mario Carneiro]

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

[Mario Carneiro]

@Seul Baek

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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.

[Johan Commelin]

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]

@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]

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

[Johan Commelin]

But I'm also fine with manual mode.

[Johan Commelin]

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

[Seul Baek]

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.