Zulip Chat Archive

Stream: general

Topic: linarith?

Bolton Bailey (Aug 22 2022 at 19:37):

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 (Aug 22 2022 at 22:32):

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

Eric Wieser (Dec 08 2022 at 01:30):

polyrith produces the type of proof that linear_combination can use

Last updated: Aug 03 2023 at 10:10 UTC