Commit 2024-11-09 18:52 9fcb1e10

View on Github →

refactor: move linarith Ineq datatype to standalone file (#18678) The linarith Ineq datatype is an enum with the constructors eq, le, and lt. This is pretty general, and in fact I would like to re-use it in the new version of linear_combination which handles inequalities (#16841). To enable this, this PR moves Linarith.Ineq (renamed Mathlib.Ineq) and its API to a new file Mathlib/Data/Ineq. Previously this material was in Mathlib/Tactic/Linarith/Datatypes. I also extend the API by adding two new MetaM functions, Lean.Expr.ineq? and Lean.Expr.ineqOrNotIneq?, which parse an expression to the Ineq it represents, if applicable. These will be used in #16841, but I decided that at the same time I might as well golf some of the linarith code to use these functions rather than parsing inequality expressions from scratch each time. The following functions from the linarith implementation get rewritten: Linarith/Datatypes Linarith.getRelSides (removed since entirely subsumed by Lean.Expr.ineq?) Linarith.parseCompAndExpr Linarith.mkSingleCompZeroOf Linarith/Preprocessing Linarith.filterComparisons Linarith.isNatProp Linarith.mkNonstrictIntProof Linarith.rearrangeComparison Linarith/Verification Linarith.leftOfIneqProof Linarith.typeOfIneqProof Linarith/Frontend Linarith.getContrLemma I also streamlined several of these functions in ways I believe are harmless:

rather than separately handling LT.lt and GT.gt (resp. LE.le and GE.ge) I just include a whnfR in the parsing function
in Linarith.rearrangeComparison I do not special-case the LHS or RHS being zero
in the preprocessor Linarith.compWithZero I drop the handling of negation hypotheses; this is harmless when the Linarith.removeNegations preprocessor has been run before the compWithZero preprocessor (which is the default), and although in principle it is possible to run linarith in a custom configuration which doesn't include the removeNegations preprocessor, in that case the negation hypotheses would never be relevant, so it wouldn't matter that the compWithZero preprocessor doesn't handle them.