Zulip Chat Archive

Stream: maths

Topic: omega with atoms?

view this post on Zulip Kevin Buzzard (Nov 26 2019 at 16:39):

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,

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?

view this post on Zulip Rob Lewis (Nov 26 2019 at 16:43):

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

view this post on Zulip Rob Lewis (Nov 26 2019 at 16:44):

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

view this post on Zulip Seul Baek (Nov 28 2019 at 21:45):

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.

view this post on Zulip Kevin Buzzard (Nov 28 2019 at 22:17):

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

view this post on Zulip Rob Lewis (Nov 28 2019 at 22:24):

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

Last updated: May 19 2021 at 00:40 UTC