linarith and integer division

Stream: new members

[Markus Himmel]

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]

omega?

[Markus Himmel]

omega also fails for me

[Jalex Stark]

huh, interval_cases is the slow part

[Reid Barton]

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

[Alex J. Best]

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

[Reid Barton]

not even multiplication by constants?

[Reid Barton]

preprocessing for division by constants is less trivial but still possible

[Alex J. Best]

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

[Jalex Stark]

qify is the tactic we want?

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

[Alex J. Best]

And suggets 100 finds Reid's proof :grinning:

[Rob Lewis]

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