## Stream: metaprogramming / tactics

### Topic: linarith preprocessing

#### Rob Lewis (Jul 16 2020 at 08:51):

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 (Jul 16 2020 at 08:52):

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

#### Mario Carneiro (Jul 16 2020 at 09:00):

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 (Jul 16 2020 at 14:04):

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]`.

Last updated: May 09 2021 at 22:13 UTC