linarith?

Stream: general

[Bolton Bailey]

Another thread was asking about how to see exactly what linarith is doing (show_term is too verbose to be useful). I was thinking about this in the context of the relatively new tactic linear_combination. It seems to me that just as linear_combination proves an equality by way of a formal sum of known equalities, linarith proves an inequality as a formal sum of known inequalities. What would it take to add a linarith? tactic that outputs a try this : linear_combination ... call? Is linear_combination designed to work with inequalities? If not, could it be modified to do so?

[Mario Carneiro]

There is no tactic that can currently handle proofs by linear certificate

[Eric Wieser]

polyrith produces the type of proof that linear_combination can use