nlinarith

1import Mathlib.Tactic.Linarith
2
3-- nlinarith handles products of variables
4example (x y : Int) (hx : x ≥ 0) (hy : y ≥ 0) : x * y ≥ 0 := by
5  nlinarith [sq_nonneg x, sq_nonneg y, sq_nonneg (x + y), sq_nonneg (x - y)]
6
7-- Squares are non-negative
8example (x : Int) : x * x ≥ 0 := by
9  nlinarith [sq_nonneg x]

1import Mathlib.Tactic.Linarith
2
3-- Use nlinarith when goals involve:
4-- 1. Products of variables
5example (a b : Int) (ha : a ≥ 1) (hb : b ≥ 1) : a * b ≥ 1 := by
6  nlinarith [sq_nonneg a, sq_nonneg b, sq_nonneg (a-1), sq_nonneg (b-1)]
7
8-- 2. Squares or powers
9example (x : Int) (h : x ≥ 2) : x * x ≥ 4 := by
10  nlinarith [sq_nonneg x, sq_nonneg (x - 2)]
11
12-- 3. Bounds that multiply
13example (x y : Int) (hx : 0 ≤ x) (hx' : x ≤ 3) (hy : 0 ≤ y) (hy' : y ≤ 4) : 
14    x * y ≤ 12 := by
15  nlinarith [sq_nonneg x, sq_nonneg y, sq_nonneg (3-x), sq_nonneg (4-y)]

1import Mathlib.Tactic.Linarith
2
3-- nlinarith often needs hints about non-negativity
4example (a b : Int) (ha : a ≥ 0) (hb : b ≥ 0) (h : a + b = 0) : a = 0 := by
5  nlinarith [sq_nonneg a, sq_nonneg b]
6
7-- Common hint: sq_nonneg for any expression
8-- sq_nonneg x proves x^2 ≥ 0
9
10example (x y : Int) : (x - y)^2 ≥ 0 := sq_nonneg (x - y)
11-- This is: x^2 - 2*x*y + y^2 ≥ 0

1import Mathlib.Tactic.Linarith
2
3-- Prove (a + b)^2 ≥ 4ab from (a - b)^2 ≥ 0
4example (a b : Int) : (a + b)^2 ≥ 4 * a * b := by
5  have h : (a - b)^2 ≥ 0 := sq_nonneg (a - b)
6  -- (a-b)^2 = a^2 - 2ab + b^2 ≥ 0
7  -- So a^2 + b^2 ≥ 2ab
8  -- Thus (a+b)^2 = a^2 + 2ab + b^2 = (a^2+b^2) + 2ab ≥ 2ab + 2ab = 4ab
9  nlinarith [sq_nonneg a, sq_nonneg b]

1import Mathlib.Tactic.Linarith
2
3-- linarith: linear only
4example (x y : Int) (h1 : x + y ≤ 10) (h2 : x ≥ 3) : y ≤ 7 := by
5  linarith  -- Works!
6
7-- nlinarith: handles nonlinear
8example (x : Int) (h : x ≥ 3) : x * x ≥ 9 := by
9  -- linarith  -- Fails
10  nlinarith [sq_nonneg x, sq_nonneg (x - 3)]  -- Works!
11
12-- nlinarith is slower, use linarith when possible

1import Mathlib.Tactic.Linarith
2
3-- Prove bounds on quadratic expressions
4theorem quadratic_lower_bound (x : Int) (h : x ≥ 1) : 
5    x^2 + x ≥ 2 := by
6  nlinarith [sq_nonneg x, sq_nonneg (x - 1)]

1import Mathlib.Tactic.Linarith
2
3-- Bounded inputs give bounded outputs
4theorem product_bound (x y : Int) 
5    (hx1 : 1 ≤ x) (hx2 : x ≤ 10)
6    (hy1 : 1 ≤ y) (hy2 : y ≤ 10) :
7    1 ≤ x * y ∧ x * y ≤ 100 := by
8  constructor
9  · nlinarith [sq_nonneg x, sq_nonneg y, sq_nonneg (x-1), sq_nonneg (y-1)]
10  · nlinarith [sq_nonneg (10-x), sq_nonneg (10-y)]

1import Mathlib.Tactic.Linarith
2
3-- (a^2 + b^2)(c^2 + d^2) ≥ (ac + bd)^2
4-- This is Cauchy-Schwarz for 2D vectors
5theorem cauchy_schwarz_2d (a b c d : Int) : 
6    (a^2 + b^2) * (c^2 + d^2) ≥ (a*c + b*d)^2 := by
7  have h : (a*d - b*c)^2 ≥ 0 := sq_nonneg (a*d - b*c)
8  nlinarith [sq_nonneg a, sq_nonneg b, sq_nonneg c, sq_nonneg d]

1import Mathlib.Tactic.Linarith
2
3-- When nlinarith fails:
4
5-- 1. Add more sq_nonneg hints
6example (x : Int) (h : x ≥ 5) : x^2 ≥ 25 := by
7  nlinarith [sq_nonneg x, sq_nonneg (x - 5)]
8
9-- 2. Break into cases
10-- 3. Use other tactics (polyrith, positivity)
11-- 4. Prove intermediate lemmas