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