Zulip Chat Archive

Stream: general

Topic: app_builder_exception in `nlinarith`


view this post on Zulip Heather Macbeth (Jul 16 2020 at 20:27):

I encountered some odd behaviour in nlinarith today. Any ideas about what might be causing it? @Rob Lewis

import analysis.normed_space.basic
variables {R : Type*} [normed_ring R]

-- works
example (t : R) (a b : ) (h : a  b) : t^2 * a  t^2 * b :=
mul_le_mul_of_nonneg_left h (norm_nonneg (t^2))

-- fails, "app_builder_exception"
example (t : R) (a b : ) (h : a  b) : t^2 * a  t^2 * b :=
by nlinarith [norm_nonneg (t^2)]

-- works
example (t : R)  (a b : ) (h : a  b) : a  t^2 + b :=
by linarith [norm_nonneg (t^2)]

-- works
example (t : R) (a b : ) (h : a  b) : t * a  t * b :=
by nlinarith [norm_nonneg t]

view this post on Zulip Heather Macbeth (Jul 16 2020 at 20:29):

(By the way, is there a way to get rid of those red boxes?)

view this post on Zulip Simon Hudon (Jul 16 2020 at 20:31):

In the error message, there should be the name of a flag that you can set for more information

view this post on Zulip Heather Macbeth (Jul 16 2020 at 20:34):

Indeed, it tells me to use the command "set_option trace.app_builder true". I haven't done this before -- how do I use this command? Is it in the VSCode preferences?

view this post on Zulip Alex J. Best (Jul 16 2020 at 20:34):

You can just type it before the example on a blank line

view this post on Zulip Simon Hudon (Jul 16 2020 at 20:34):

No, you copy and paste it in your code, right before the troublesome declaration

view this post on Zulip Heather Macbeth (Jul 16 2020 at 20:35):

Thanks! Here's the result: "[app_builder] failed to create an 'pow_two_nonneg'-application, there are missing implicit arguments"

view this post on Zulip Simon Hudon (Jul 16 2020 at 20:36):

Can you remember where you make use of pow_two_nonneg?

view this post on Zulip Heather Macbeth (Jul 16 2020 at 20:37):

I don't believe I used it at all. It doesn't appear in the example code I gave.

view this post on Zulip Alex J. Best (Jul 16 2020 at 20:39):

nlinarith is presumably seeing the square and going ah-ha thats positive, even though that doesn't really make sense for R?

view this post on Zulip Alex J. Best (Jul 16 2020 at 20:39):

Looks like set_option trace.linarith true might also be helpful

view this post on Zulip Heather Macbeth (Jul 16 2020 at 20:39):

Yes, that would make sense!

view this post on Zulip Bryan Gin-ge Chen (Jul 16 2020 at 20:40):

(The red boxes in Zulip should disappear after pygments makes a new release and we bug Zulip to update their pygments. It's been 4 months since the last pygments release, but I don't want to bug them, since they're just open source volunteers ...)

view this post on Zulip Rob Lewis (Jul 16 2020 at 20:56):

This should be easy to fix, I'll look into it tomorrow!

view this post on Zulip Heather Macbeth (Jul 16 2020 at 20:59):

That's great!

view this post on Zulip Rob Lewis (Jul 16 2020 at 21:04):

Without looking at the code, I'm certain @Alex J. Best is right, and the fix is just to continue if this call to mk_app fails. An enterprising young tactic writer could fix this with one line before I wake up.

view this post on Zulip Alex J. Best (Jul 16 2020 at 22:59):

#3417


Last updated: May 13 2021 at 21:12 UTC