app_builder_exception in `nlinarith`

Stream: general

[Heather Macbeth]

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]

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

[Simon Hudon]

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

[Heather Macbeth]

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]

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

[Simon Hudon]

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

[Heather Macbeth]

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

[Simon Hudon]

Can you remember where you make use of pow_two_nonneg?

[Heather Macbeth]

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

[Alex J. Best]

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]

Looks like set_option trace.linarith true might also be helpful

[Heather Macbeth]

Yes, that would make sense!

[Bryan Gin-ge Chen]

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

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

[Heather Macbeth]

That's great!

[Rob Lewis]

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]

#3417