Zulip Chat Archive

Stream: new members

Topic: linarith and integer division


view this post on Zulip Markus Himmel (Jul 12 2020 at 14:43):

I vaguely recall having seen a thread about this before, but I can't find it, so I'll ask it again: Is linarith supposed to be able to handle things like the following?

example (i : ) (hi : i < 9) : i / 3 < 3 :=
-- by linarith does not work
by interval_cases i; exact dec_trivial

If not, is there some tactic that can automatically deal with this that compiles significantly faster than the above proof?

view this post on Zulip Jalex Stark (Jul 12 2020 at 14:49):

omega?

view this post on Zulip Markus Himmel (Jul 12 2020 at 14:50):

omega also fails for me

view this post on Zulip Jalex Stark (Jul 12 2020 at 14:55):

huh, interval_cases is the slow part

view this post on Zulip Reid Barton (Jul 12 2020 at 14:55):

I know this doesn't meet your criteria, but nat.div_lt_of_lt_mul hi

view this post on Zulip Alex J. Best (Jul 12 2020 at 14:56):

Omega won't work when there is multiplication or division unfortunately.

view this post on Zulip Reid Barton (Jul 12 2020 at 14:56):

not even multiplication by constants?

view this post on Zulip Reid Barton (Jul 12 2020 at 14:57):

preprocessing for division by constants is less trivial but still possible

view this post on Zulip Alex J. Best (Jul 12 2020 at 15:01):

Oops you are right, multiplication by constants is handled, just division is not.

view this post on Zulip Jalex Stark (Jul 12 2020 at 15:01):

qify is the tactic we want?

example (i : ) (hi : i < 9) : i / 3 < 3 := by linarith

view this post on Zulip Alex J. Best (Jul 12 2020 at 15:01):

And suggets 100 finds Reid's proof :grinning:

view this post on Zulip Rob Lewis (Jul 12 2020 at 15:04):

Note that this qification is nontrivial, since i / 3 isn't equal to (i : ℚ) / 3.


Last updated: May 11 2021 at 00:31 UTC