linarith preprocessing

Stream: metaprogramming / tactics

[Rob Lewis]

Yesterday at LftCM, @Heather Macbeth asked about adapting linarith to understand nonnegativity of norms. I think this is a nice exercise for anyone looking for a metaprogramming exercise, so I'm posting it as a suggestion here.

The goal: a tactic norm_nlinarith, that does everything nlinarith does except it also uses proofs of 0 ≤ ∥x∥ for every ∥x∥ that appears in the problem.

linarith has a notion of a preprocessor. In fact, nlinarith is exactly linarith plus one extra preprocessor. norm_nlinarith requires adding one simple preprocessing step before this nlinarith` step.

There's already a function find_squares that's used there; something similar, even simpler, could be done to look for norm expressions. If you followed my metaprogramming videos you know how to create a proof term showing a norm is nonnegative. (It's very much like the example showing a natural number is nonnegative.)

The wrapper tactic norm_nlinarith (better name to be determined) would have to insert the new preprocessor at the right place in the preprocessor list.

[Rob Lewis]

Maybe @Heather Macbeth has suggestions of some test cases for this tactic!

[Mario Carneiro]

Maybe the commonalities of nlinarith and norm_nlinarith could be generalized to a preprocessor that does the general process of searching for some kind of subterm and adding some kind of lemma based on the term to the context

[Heather Macbeth]

Along the lines Mario mentions, it would be nice to be able to do linarith [norm_nonneg, triangle], like one can with rw or simp: to mention just the lemmas, and have the tactic add to the hypotheses all possible applications of those lemmas to the expressions in the goal. At the moment one has to be more specific and say linarith [triangle a b].

[Heather Macbeth]

It's been a long time, but #8104 has some great examples of tasks that I wish linarith preprocessing could automate.

import analysis.normed_space.basic

variables {E : Type*} [normed_group E] [normed_space ℝ E]

example {x v w : E}
  (h t : ℝ)
  (h_lt_1 : h < 1)
  (hpos : 0 < h)
  (ht : t ∈ set.Ico (0:ℝ) 1) :
  ∥h • v + (t * h) • w∥ ≤ h * (∥v∥ + ∥w∥) :=
calc  ∥h • v + (t * h) • w∥
    ≤ ∥h • v∥ + ∥(t * h) • w∥ : norm_add_le _ _
... = h * ∥v∥ + t * (h * ∥w∥) :
  by simp only [norm_smul, real.norm_eq_abs, hpos.le, abs_of_nonneg, abs_mul, ht.left,
                mul_assoc]
... ≤ h * ∥v∥ + 1 * (h * ∥w∥) :
  add_le_add (le_refl _) (mul_le_mul_of_nonneg_right ht.2.le
    (mul_nonneg hpos.le (norm_nonneg _)))
... = h * (∥v∥ + ∥w∥) : by ring

example {x v w : E}
  (ε h t : ℝ)
  (εpos : 0 < ε)
  (h_lt_1 : h < 1)
  (hpos : 0 < h)
  (ht : t ∈ set.Ico (0:ℝ) 1)
  (I : ∥h • v + (t * h) • w∥ ≤ h * (∥v∥ + ∥w∥)) :
  ε * ∥h • v + (t * h) • w∥ * ∥h • w∥ ≤ ε * (∥h • v∥ + ∥h • w∥) * ∥h • w∥ :=
begin
  apply mul_le_mul_of_nonneg_right _ (norm_nonneg _),
  apply mul_le_mul_of_nonneg_left _ (εpos.le),
  apply (norm_add_le _ _).trans,
  refine add_le_add (le_refl _) _,
  simp only [norm_smul, real.norm_eq_abs, abs_mul, abs_of_nonneg, ht.1, hpos.le, mul_assoc],
  exact mul_le_of_le_one_left (mul_nonneg hpos.le (norm_nonneg _)) ht.2.le,
end

[Heather Macbeth]

(cc @Sebastien Gouezel)

[Sebastien Gouezel]

Yes, it was pretty painful :-)