Zulip Chat Archive

Stream: new members

Topic: linarith and integer division


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?

Jalex Stark (Jul 12 2020 at 14:49):

omega?

Markus Himmel (Jul 12 2020 at 14:50):

omega also fails for me

Jalex Stark (Jul 12 2020 at 14:55):

huh, interval_cases is the slow part

Reid Barton (Jul 12 2020 at 14:55):

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

Alex J. Best (Jul 12 2020 at 14:56):

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

Reid Barton (Jul 12 2020 at 14:56):

not even multiplication by constants?

Reid Barton (Jul 12 2020 at 14:57):

preprocessing for division by constants is less trivial but still possible

Alex J. Best (Jul 12 2020 at 15:01):

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

Jalex Stark (Jul 12 2020 at 15:01):

qify is the tactic we want?

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

Alex J. Best (Jul 12 2020 at 15:01):

And suggets 100 finds Reid's proof :grinning:

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: Dec 20 2023 at 11:08 UTC