Stream: maths

Topic: playing with nlinarith

Kevin Buzzard (Jun 23 2020 at 20:19):

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 (Jun 23 2020 at 20:29):

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 (Jun 23 2020 at 20:29):

The second one should work when the refactor PR lands.

Bryan Gin-ge Chen (Jun 23 2020 at 20:33):

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

Heather Macbeth (Jun 23 2020 at 21:25):

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 (Jun 23 2020 at 22:30):

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

Heather Macbeth (Jun 23 2020 at 22:33):

I have proved it, don't worry :)

Kevin Buzzard (Jun 23 2020 at 22:35):

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

Heather Macbeth (Jun 23 2020 at 22:35):

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 (Jun 23 2020 at 22:36):

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 (Jun 23 2020 at 22:37):

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

Kevin Buzzard (Jun 23 2020 at 22:43):

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 (Jun 23 2020 at 22:48):

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 (Jun 24 2020 at 06:21):

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 (Jun 24 2020 at 07:42):

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 (Jun 24 2020 at 07:45):

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.

Last updated: May 11 2021 at 16:22 UTC