## Stream: general

### Topic: app_builder_exception in nlinarith

#### 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]


#### Heather Macbeth (Jul 16 2020 at 20:29):

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

#### 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

#### 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?

#### Alex J. Best (Jul 16 2020 at 20:34):

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

#### Simon Hudon (Jul 16 2020 at 20:34):

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

#### 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"

#### Simon Hudon (Jul 16 2020 at 20:36):

Can you remember where you make use of pow_two_nonneg?

#### 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.

#### 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?

#### Alex J. Best (Jul 16 2020 at 20:39):

Looks like set_option trace.linarith true might also be helpful

#### Heather Macbeth (Jul 16 2020 at 20:39):

Yes, that would make sense!

#### 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 ...)

#### Rob Lewis (Jul 16 2020 at 20:56):

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

That's great!

#### 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.

#### Alex J. Best (Jul 16 2020 at 22:59):

#3417

Last updated: May 13 2021 at 21:12 UTC