Zulip Chat Archive

Stream: general

Topic: nonlinear linarith


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 05:06):

Is it just linarith with a fancy simp set?

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:01):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 09 2020 at 09:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 10:17):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 11:12):

#2637

view this post on Zulip Patrick Massot (May 09 2020 at 11:16):

Thanks Mario!

view this post on Zulip Patrick Massot (May 09 2020 at 11:18):

Oh, you forgot to change the name :sad:

view this post on Zulip Patrick Massot (May 09 2020 at 11:19):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 11:46):

you mean nra is a bad name?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 11:49):

I also prefer short tactic names

view this post on Zulip Mario Carneiro (May 09 2020 at 11:49):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 09 2020 at 12:40):

nra = not really additive

view this post on Zulip Johan Commelin (May 09 2020 at 12:42):

linarith!

view this post on Zulip Mario Carneiro (May 09 2020 at 12:43):

taken

view this post on Zulip Mario Carneiro (May 09 2020 at 12:43):

by linarith

view this post on Zulip Johan Commelin (May 09 2020 at 12:43):

bah

view this post on Zulip Patrick Massot (May 09 2020 at 12:43):

We really need that come_on_lean tactic and stop discussing names

view this post on Zulip Johan Commelin (May 09 2020 at 12:43):

sudo linarith!

view this post on Zulip Mario Carneiro (May 09 2020 at 12:43):

lol

view this post on Zulip 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