## 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: May 11 2021 at 00:31 UTC