Topic: omega with atoms?
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, 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
Rob Lewis (Nov 26 2019 at 16:43):
omega being overly sensitive about the context again. You can post it here. https://github.com/leanprover-community/mathlib/issues/1484
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.
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
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
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