omega with atoms?

Stream: maths

[Kevin Buzzard]

Should I expect omega to kill this goal:

1 goal
n : ℕ,
G_C G_L : list ℤ,
hG : length G_C + length G_L = n + 1,
iv : ℕ,
hi : iv < length G_C
⊢ iv + (length G_C - iv - 1) + length G_L = n

It doesn't seem to, I get the clear tactic failed, target type depends on 'G_C' error. Is this just a bug? If I do this

      generalize hc : length G_C = c,
      rw hc at *,
      clear hc G_C,
      generalize hl : length G_L = l,
      rw hl at *,
      clear hl G_L,
      omega,

then it works fine, i.e. I tell Lean that length G_C is just a constant natural. I also had to do the clears or else I get other errors. Is this just the same bug in omega?

[Rob Lewis]

It's omega being overly sensitive about the context again. You can post it here. https://github.com/leanprover-community/mathlib/issues/1484

[Rob Lewis]

These things need @Seul Baek 's attention though. I don't really want to start touching the omega internals myself.

[Seul Baek]

Sorry for taking a long time to fix with things. I pushed a bugfix which now makes omega treat any non-constant integer or natural number as a variable. I think it should now work with terms like length l or fib n.

[Kevin Buzzard]

Thanks @Seul Baek ! There's no hurry, it's an open source project and I'm sure you have other things to do, but I really appreciate it. I have an MSc student who is extensively using omega! If I remember correctly, you told me how it worked in Amsterdam :D

[Rob Lewis]

Yes, thank you Seul! Just looking at the size of the PR, I'm very glad I didn't try this myself.