Zulip Chat Archive

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