## Stream: general

### Topic: nonlinear linarith

#### Patrick Massot (May 08 2020 at 20:10):

In the teaching stream, Heather pointed out the usefulness of nra in Coq. The description sounds like it would be pretty doable to have in mathlib. @Rob Lewis What would it take besides the name change to convince you to give it a try?

#### Patrick Massot (May 08 2020 at 20:17):

Maybe I should emphasize I don't really mean Rob should do this, I simply couldn't resist using the combination of relation to linarith and to American politics.

#### Mario Carneiro (May 09 2020 at 05:05):

Isn't nonlinear arithmetic undecidable? That means we need a more precise description of what it can and can't do

#### Mario Carneiro (May 09 2020 at 05:06):

Is it just linarith with a fancy simp set?

#### Kevin Buzzard (May 09 2020 at 07:01):

How does linarith with a fancy simp set work? Does it try the simp set first?

#### Patrick Massot (May 09 2020 at 09:17):

I'm sorry, I should have copy-pasted in addition to giving a link:

This tactic is an experimental proof procedure for non-linear arithmetic. The tactic performs a limited amount of non-linear reasoning before running the linear prover of lra. This pre-processing does the following:

• If the context contains an arithmetic expression of the form e[x2] where x is a monomial, the context is enriched with x2≥0 ;
• For all pairs of hypotheses e1≥0, e2≥0, the context is enriched with e1×e2≥0

After this pre-processing, the linear prover of lra searches for a proof by abstracting monomials by variables.

#### Mario Carneiro (May 09 2020 at 09:21):

For all pairs of hypotheses e1≥0, e2≥0, the context is enriched with e1×e2≥0

Doesn't this diverge?

#### Patrick Massot (May 09 2020 at 09:24):

I guess they first generate the list of assumptions of the form e ≥0

#### Mario Carneiro (May 09 2020 at 09:54):

Is this supposed to work?

import tactic.linarith

example {α:Type} [linear_ordered_ring α] (a b : α)
(h : 0 ≤ a) (h : 0 ≤ b) : 0 ≤ a + b := by linarith

done tactic failed, there are unsolved goals
state:
α : Type,
_inst_1 : linear_ordered_ring α,
a b : α,
h : 0 ≤ a,
h : 0 ≤ b,
a_1 : 0 > a + b
⊢ -a - b + (a + b) = 0


#### Mario Carneiro (May 09 2020 at 09:55):

In any case, I think this does the requisite preprocessing:

import tactic.linarith

namespace tactic

meta def find_squares : expr → tactic unit
| e@(%%a ^ 2) := do
find_squares a,
trace a,
try (do
p ← mk_app pow_two_nonneg [a],
t ← infer_type p,
assertv h t p) >> skip
| e := () <$e.traverse (λ e, e <$ find_squares e)

meta def nra : tactic unit :=
do ls ← local_context,
ls' ← ls.mfoldr (λ h l, do
t ← infer_type h,
find_squares t,
match t with
| (0 ≤ %%a) := return (h :: l)
| _ := return l
end) [],
target >>= find_squares,
ls'.mmap' (λ a, ls'.mmap' \$ λ b, do
p ← mk_app mul_nonneg [a, b],
t ← infer_type p,
assertv h t p),
tactic.interactive.linarith none none none

example {α:Type} [linear_ordered_ring α] (a b : α) : 0 ≤ a ^ 2 + b ^ 2 := by nra
end tactic


#### Mario Carneiro (May 09 2020 at 10:17):

(Oops, linear_ordered_ring is not supported by ring because it is not commutative)

#2637

Thanks Mario!

#### Patrick Massot (May 09 2020 at 11:18):

Oh, you forgot to change the name :sad:

#### Patrick Massot (May 09 2020 at 11:19):

Shouldn't we have a general policy to avoid evil names?

#### Mario Carneiro (May 09 2020 at 11:46):

you mean nra is a bad name?

#### Mario Carneiro (May 09 2020 at 11:47):

I generally bias for not changing names, especially for a direct port like this, in order to make it easier for people to find

#### Mario Carneiro (May 09 2020 at 11:49):

I also prefer short tactic names

#### Mario Carneiro (May 09 2020 at 11:49):

but if people have a preferred name I can change it to whatever. nonlinarith?

#### Patrick Massot (May 09 2020 at 12:38):

I don't how this is perceived in the US, but outside of your country NRA is perceived as one the world most evil combination of letters.

#### Johan Commelin (May 09 2020 at 12:42):

linarith!

taken

#### Mario Carneiro (May 09 2020 at 12:43):

by linarith

bah

#### Patrick Massot (May 09 2020 at 12:43):

We really need that come_on_lean tactic and stop discussing names

#### Johan Commelin (May 09 2020 at 12:43):

sudo linarith!

lol

#### Reid Barton (May 09 2020 at 12:45):

Hmm there's like 100 "Food & Drink" emoji, but none that are uncontroversially a sandwich...

Last updated: May 14 2021 at 00:42 UTC