playing with nlinarith

Stream: maths

[Kevin Buzzard]

Fully expecting the answer "no": is it easy to make these work? They both naively look in scope to me, but I am quite naive.

example (x : ℝ) (h1 : 0 ≤ x) (h2 : 0 ≠ x) : 0 < x := by linarith

example (a b : ℝ) (hab : 0 < a * b) (ha : 0 < a) : 0 < b := by nlinarith

[Rob Lewis]

The first one: linarith doesn't do neq in hypotheses, since it leads to exponential blowups. (2^n linarith runs for n neq hypotheses.) It should solve the contrapositive.

[Rob Lewis]

The second one should work when the refactor PR lands.

[Bryan Gin-ge Chen]

Is anyone working on reviewing the PR? It's beyond my abilities, unfortunately.

[Heather Macbeth]

On the same subject, here's something I wanted to do yesterday:

example (a b : ℝ) (h1 : 0 ≤ a) (h2 : 1 ≤ a * b) : 0 < a

Will this also be in range after the refactor?

[Kevin Buzzard]

If you rewrite le_iff_lt_or_eq at h1 then this might be in scope for other tactics like simp

[Heather Macbeth]

I have proved it, don't worry :)

[Kevin Buzzard]

We are just dreaming of the "it's obvious" tactic but apparently writing this is harder than it looks...

[Heather Macbeth]

Also, to be clear, I am not demanding a supernlinarith which solves this particular problem! Just, like Kevin, curious about exactly what the new algorithm will do.

[Anatole Dedecker]

Kevin Buzzard said:

We are just dreaming of the "it's obvious" tactic but apparently writing this is harder than it looks...

My father would say "by classical argument, it's obvious"

[Kevin Buzzard]

I think that maybe sledgehammers can solve this sort of goal? It might take longer than a human though...

[Kevin Buzzard]

Sorry Heather, I didn't mean to imply that you couldn't prove it :-) I've spent all day trying to prove things like this using only tactics and not rewriting any lemmas from the library, or as few as possible. I've been jumping through hoops with by_contradiction and push_neg on the basis that it's easier to teach them than to teach the entire contents of the library :-/

[Heather Macbeth]

That's interesting; who is your target audience? Is the idea that breaking facts down into library_search-able pieces is too intimidating?

[Kevin Buzzard]

I am playing with the real number game. You want to get onto interesting maths ASAP but conversely you don't want to have to teach the user 100 mathlib lemmas just so they can do trivial things. This leaves you with real problems sometimes because they have a-b=c and they want a=b+c but have no idea about sub_eq_iff_add_left or whatever the lemma will be called. Teaching all these lemma names doesn't scale for one off apps like this and there's the added problem that sometimes working forwards is the natural way to go whereas most tactics operate on the goal

[Rob Lewis]

Heather Macbeth said:

On the same subject, here's something I wanted to do yesterday:

example (a b : ℝ) (h1 : 0 ≤ a) (h2 : 1 ≤ a * b) : 0 < a

Will this also be in range after the refactor?

No, this is out of scope (for nra too).

[Rob Lewis]

nlinarith is a tiny bit of preprocessing on top of linarith. The party line is, don't expect it to do anything and be excited if it works. If it fails and nra solves the equivalent goal in Coq, we can investigate.