# Zulip Chat Archive

## 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