Zulip Chat Archive

Stream: general

Topic: linarith nnreal


view this post on Zulip Johan Commelin (Oct 12 2020 at 12:17):

Should this be in scope for linarith?

import data.real.nnreal

example (a b c d : nnreal)
  (hba : b  a)
  (hcb : c  b)
  (hd0 : 0 < d)
  (hdc : d  c)
  (h1 : a + b + c + d = 1) :
  a + 2 * b + 3 * c + 4 * d  a + 3 * b + 3 * c + 3 * d :=
begin
  linarith
end

view this post on Zulip Johan Commelin (Oct 12 2020 at 12:20):

Changing nnreal to real makes linarith solve it

view this post on Zulip Johan Commelin (Oct 12 2020 at 13:12):

linarith only looks at typeclasses, right?

view this post on Zulip Johan Commelin (Oct 12 2020 at 13:14):

There is a linear_ordered_semiring instance for nnreal. But maybe linarith doesn't like the semi?

view this post on Zulip Rob Lewis (Oct 12 2020 at 13:49):

linarith wants to subtract.


Last updated: May 11 2021 at 21:10 UTC