Commit 2025-06-19 05:18 a978d177

View on Github →

chore(Tactic/Linarith): put linarith declarations into Mathlib.Tactic namespace (#25955) The Name.isMetaProgramming function is used to exclude lemmas from library search tactics. Thus, it is important that lemmas that are only meant for use in a tactic implementation have a name flagged by Name.isMetaProgramming. So, this PR renames everying in Mathlib/Tactic/Linarith to the namespace Mathlib.Tactic.Linarith (which previously was just Linarith)

Estimated changes

Modified Mathlib/Tactic/Linarith/Datatypes.lean

deleted def Linarith.Branch

deleted structure Linarith.CertificateOracle

deleted def Linarith.Comp.add

deleted def Linarith.Comp.cmp

deleted def Linarith.Comp.coeffOf

deleted def Linarith.Comp.isContr

deleted def Linarith.Comp.scale

deleted def Linarith.Comp.vars

deleted structure Linarith.Comp

deleted def Linarith.GlobalBranchingPreprocessor.process

deleted structure Linarith.GlobalBranchingPreprocessor

deleted def Linarith.GlobalPreprocessor.branching

deleted structure Linarith.GlobalPreprocessor

deleted def Linarith.Linexp.cmp

deleted def Linarith.Linexp.contains

deleted def Linarith.Linexp.get

deleted def Linarith.Linexp.scale

deleted def Linarith.Linexp.vars

deleted def Linarith.Linexp.zfind

deleted def Linarith.Preprocessor.globalize

deleted structure Linarith.Preprocessor

deleted structure Linarith.PreprocessorBase

deleted def Linarith.linarithGetProofsMessage

deleted def Linarith.linarithTraceProofs

deleted def Linarith.mkSingleCompZeroOf

deleted def Linarith.parseCompAndExpr

added def Mathlib.Tactic.Linarith.Branch

added structure Mathlib.Tactic.Linarith.CertificateOracle

added def Mathlib.Tactic.Linarith.Comp.add

added def Mathlib.Tactic.Linarith.Comp.cmp

added def Mathlib.Tactic.Linarith.Comp.coeffOf

added def Mathlib.Tactic.Linarith.Comp.isContr

added def Mathlib.Tactic.Linarith.Comp.scale

added def Mathlib.Tactic.Linarith.Comp.vars

added structure Mathlib.Tactic.Linarith.Comp

added def Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.process

added structure Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor

added def Mathlib.Tactic.Linarith.GlobalPreprocessor.branching

added structure Mathlib.Tactic.Linarith.GlobalPreprocessor

added def Mathlib.Tactic.Linarith.Linexp.cmp

added def Mathlib.Tactic.Linarith.Linexp.contains

added def Mathlib.Tactic.Linarith.Linexp.get

added def Mathlib.Tactic.Linarith.Linexp.scale

added def Mathlib.Tactic.Linarith.Linexp.vars

added def Mathlib.Tactic.Linarith.Linexp.zfind

added def Mathlib.Tactic.Linarith.Preprocessor.globalize

added structure Mathlib.Tactic.Linarith.Preprocessor

added structure Mathlib.Tactic.Linarith.PreprocessorBase

added def Mathlib.Tactic.Linarith.linarithGetProofsMessage

added def Mathlib.Tactic.Linarith.linarithTraceProofs

added def Mathlib.Tactic.Linarith.mkSingleCompZeroOf

added def Mathlib.Tactic.Linarith.parseCompAndExpr

Modified Mathlib/Tactic/Linarith/Frontend.lean

deleted def Linarith.ExprMultiMap.find

deleted def Linarith.ExprMultiMap.insert

deleted def Linarith.LinarithConfig.updateReducibility

deleted structure Linarith.LinarithConfig

deleted def Linarith.applyContrLemma

deleted def Linarith.findLinarithContradiction

deleted def Linarith.getContrLemma

deleted def Linarith.partitionByType

deleted def Linarith.runLinarith

added def Mathlib.Tactic.Linarith.ExprMultiMap.find

added def Mathlib.Tactic.Linarith.ExprMultiMap.insert

added def Mathlib.Tactic.Linarith.LinarithConfig.updateReducibility

added structure Mathlib.Tactic.Linarith.LinarithConfig

added def Mathlib.Tactic.Linarith.applyContrLemma

added def Mathlib.Tactic.Linarith.elabLinarithArg

added def Mathlib.Tactic.Linarith.findLinarithContradiction

added def Mathlib.Tactic.Linarith.getContrLemma

added def Mathlib.Tactic.Linarith.partitionByType

added def Mathlib.Tactic.Linarith.runLinarith

deleted def elabLinarithArg

Modified Mathlib/Tactic/Linarith/Lemmas.lean

deleted theorem Linarith.add_lt_of_le_of_neg

deleted theorem Linarith.add_lt_of_neg_of_le

deleted theorem Linarith.add_neg

deleted theorem Linarith.add_nonpos

deleted theorem Linarith.eq_of_eq_of_eq

deleted theorem Linarith.eq_of_not_lt_of_not_gt

deleted theorem Linarith.le_of_eq_of_le

deleted theorem Linarith.le_of_le_of_eq

deleted theorem Linarith.lt_irrefl

deleted theorem Linarith.lt_of_eq_of_lt

deleted theorem Linarith.lt_of_lt_of_eq

deleted theorem Linarith.mul_eq

deleted theorem Linarith.mul_neg

deleted theorem Linarith.mul_nonpos

deleted theorem Linarith.mul_zero_eq

deleted theorem Linarith.natCast_nonneg

deleted theorem Linarith.sub_neg_of_lt

deleted theorem Linarith.sub_nonpos_of_le

deleted theorem Linarith.zero_lt_one

deleted theorem Linarith.zero_mul_eq

added theorem Mathlib.Tactic.Linarith.add_lt_of_le_of_neg

added theorem Mathlib.Tactic.Linarith.add_lt_of_neg_of_le

added theorem Mathlib.Tactic.Linarith.add_neg

added theorem Mathlib.Tactic.Linarith.add_nonpos

added theorem Mathlib.Tactic.Linarith.eq_of_eq_of_eq

added theorem Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt

added theorem Mathlib.Tactic.Linarith.le_of_eq_of_le

added theorem Mathlib.Tactic.Linarith.le_of_le_of_eq

added theorem Mathlib.Tactic.Linarith.lt_irrefl

added theorem Mathlib.Tactic.Linarith.lt_of_eq_of_lt

added theorem Mathlib.Tactic.Linarith.lt_of_lt_of_eq

added theorem Mathlib.Tactic.Linarith.mul_eq

added theorem Mathlib.Tactic.Linarith.mul_neg

added theorem Mathlib.Tactic.Linarith.mul_nonpos

added theorem Mathlib.Tactic.Linarith.mul_zero_eq

added theorem Mathlib.Tactic.Linarith.natCast_nonneg

added theorem Mathlib.Tactic.Linarith.sub_neg_of_lt

added theorem Mathlib.Tactic.Linarith.sub_nonpos_of_le

added theorem Mathlib.Tactic.Linarith.zero_lt_one

added theorem Mathlib.Tactic.Linarith.zero_mul_eq

Modified Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean

deleted def Linarith.CertificateOracle.fourierMotzkin

deleted def Linarith.CompSource.flatten

deleted def Linarith.CompSource.toString

deleted inductive Linarith.CompSource

deleted structure Linarith.LinarithData

deleted def Linarith.PComp.add

deleted def Linarith.PComp.assump

deleted def Linarith.PComp.cmp

deleted def Linarith.PComp.isContr

deleted def Linarith.PComp.maybeMinimal

deleted def Linarith.PComp.scale

deleted structure Linarith.PComp

deleted def Linarith.elimAllVarsM

deleted def Linarith.elimVar

deleted def Linarith.elimVarM

deleted def Linarith.elimWithSet

deleted def Linarith.getMaxVar

deleted def Linarith.getPCompSet

deleted def Linarith.mkLinarithData

deleted def Linarith.pelimVar

deleted def Linarith.splitSetByVarSign

deleted def Linarith.update

deleted def Linarith.validate

added def Mathlib.Tactic.Linarith.CertificateOracle.fourierMotzkin

added def Mathlib.Tactic.Linarith.CompSource.flatten

added def Mathlib.Tactic.Linarith.CompSource.toString

added inductive Mathlib.Tactic.Linarith.CompSource

added structure Mathlib.Tactic.Linarith.LinarithData

added def Mathlib.Tactic.Linarith.PComp.add

added def Mathlib.Tactic.Linarith.PComp.assump

added def Mathlib.Tactic.Linarith.PComp.cmp

added def Mathlib.Tactic.Linarith.PComp.isContr

added def Mathlib.Tactic.Linarith.PComp.maybeMinimal

added def Mathlib.Tactic.Linarith.PComp.scale

added structure Mathlib.Tactic.Linarith.PComp

added def Mathlib.Tactic.Linarith.elimAllVarsM

added def Mathlib.Tactic.Linarith.elimVar

added def Mathlib.Tactic.Linarith.elimVarM

added def Mathlib.Tactic.Linarith.elimWithSet

added def Mathlib.Tactic.Linarith.getMaxVar

added def Mathlib.Tactic.Linarith.getPCompSet

added def Mathlib.Tactic.Linarith.mkLinarithData

added def Mathlib.Tactic.Linarith.pelimVar

added def Mathlib.Tactic.Linarith.splitSetByVarSign

added def Mathlib.Tactic.Linarith.update

added def Mathlib.Tactic.Linarith.validate

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean

deleted def Linarith.SimplexAlgorithm.CertificateOracle.simplexAlgorithmDense

deleted def Linarith.SimplexAlgorithm.CertificateOracle.simplexAlgorithmSparse

deleted def Linarith.SimplexAlgorithm.postprocess

deleted def Linarith.SimplexAlgorithm.preprocess

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.CertificateOracle.simplexAlgorithmDense

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.CertificateOracle.simplexAlgorithmSparse

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.postprocess

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.preprocess

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean

deleted structure Linarith.SimplexAlgorithm.DenseMatrix

deleted structure Linarith.SimplexAlgorithm.SparseMatrix

deleted structure Linarith.SimplexAlgorithm.Tableau

added structure Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix

added structure Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix

added structure Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean

deleted def Linarith.SimplexAlgorithm.Gauss.findNonzeroRow

deleted def Linarith.SimplexAlgorithm.Gauss.getTableau

deleted def Linarith.SimplexAlgorithm.Gauss.getTableauImp

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.findNonzeroRow

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableau

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableauImp

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean

deleted def Linarith.SimplexAlgorithm.extractSolution

deleted def Linarith.SimplexAlgorithm.findPositiveVector

deleted def Linarith.SimplexAlgorithm.stateLP

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.extractSolution

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.findPositiveVector

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.stateLP

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/SimplexAlgorithm.lean

deleted inductive Linarith.SimplexAlgorithm.SimplexAlgorithmException

deleted def Linarith.SimplexAlgorithm.checkSuccess

deleted def Linarith.SimplexAlgorithm.chooseEnteringVar

deleted def Linarith.SimplexAlgorithm.chooseExitingVar

deleted def Linarith.SimplexAlgorithm.choosePivots

deleted def Linarith.SimplexAlgorithm.doPivotOperation

deleted def Linarith.SimplexAlgorithm.runSimplexAlgorithm

added inductive Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.checkSuccess

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.chooseEnteringVar

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.chooseExitingVar

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.choosePivots

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.doPivotOperation

added def Mathlib.Tactic.Linarith.SimplexAlgorithm.runSimplexAlgorithm

Modified Mathlib/Tactic/Linarith/Parsing.lean

deleted def Linarith.Monom.lt

deleted def Linarith.Monom.one

deleted def Linarith.Sum.mul

deleted def Linarith.Sum.one

deleted def Linarith.Sum.scaleByMonom

deleted def Linarith.SumOfMonom

deleted def Linarith.elimMonom

deleted def Linarith.linearFormOfAtom

deleted def Linarith.linearFormsAndMaxVar

deleted def Linarith.one

deleted def Linarith.scalar

deleted def Linarith.toComp

deleted def Linarith.toCompFold

deleted def Linarith.var

added def Mathlib.Tactic.Linarith.Monom.lt

added def Mathlib.Tactic.Linarith.Monom.one

added def Mathlib.Tactic.Linarith.Sum.mul

added def Mathlib.Tactic.Linarith.Sum.one

added def Mathlib.Tactic.Linarith.Sum.scaleByMonom

added def Mathlib.Tactic.Linarith.SumOfMonom

added def Mathlib.Tactic.Linarith.elimMonom

added def Mathlib.Tactic.Linarith.linearFormOfAtom

added def Mathlib.Tactic.Linarith.linearFormsAndMaxVar

added def Mathlib.Tactic.Linarith.one

added def Mathlib.Tactic.Linarith.scalar

added def Mathlib.Tactic.Linarith.toComp

added def Mathlib.Tactic.Linarith.toCompFold

added def Mathlib.Tactic.Linarith.var

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

deleted def Linarith.Expr.Ord

deleted def Linarith.cancelDenoms

deleted def Linarith.compWithZero

deleted def Linarith.defaultPreprocessors

deleted def Linarith.flipNegatedComparison

deleted def Linarith.isNatCoe

deleted def Linarith.mkNonstrictIntProof

deleted def Linarith.mk_natCast_nonneg_prf

deleted def Linarith.natToInt

deleted def Linarith.nlinarithExtras

deleted def Linarith.normalizeDenominatorsLHS

deleted def Linarith.preprocess

deleted def Linarith.removeNe

deleted def Linarith.removeNegations

deleted def Linarith.strengthenStrictInt

deleted theorem Linarith.without_one_mul

added def Mathlib.Tactic.Linarith.Expr.Ord

added def Mathlib.Tactic.Linarith.cancelDenoms

added def Mathlib.Tactic.Linarith.compWithZero

added def Mathlib.Tactic.Linarith.defaultPreprocessors

added def Mathlib.Tactic.Linarith.flipNegatedComparison

added def Mathlib.Tactic.Linarith.isNatCoe

added def Mathlib.Tactic.Linarith.mkNonstrictIntProof

added def Mathlib.Tactic.Linarith.mk_natCast_nonneg_prf

added def Mathlib.Tactic.Linarith.natToInt

added def Mathlib.Tactic.Linarith.nlinarithExtras

added def Mathlib.Tactic.Linarith.normalizeDenominatorsLHS

added def Mathlib.Tactic.Linarith.preprocess

added def Mathlib.Tactic.Linarith.removeNe

added def Mathlib.Tactic.Linarith.removeNegations

added def Mathlib.Tactic.Linarith.strengthenStrictInt

added theorem Mathlib.Tactic.Linarith.without_one_mul

Modified Mathlib/Tactic/Linarith/Verification.lean

deleted def Linarith.addExprs'

deleted def Linarith.addExprs

deleted def Linarith.addIneq

deleted def Linarith.addNegEqProofs

deleted def Linarith.leftOfIneqProof

deleted def Linarith.mkLTZeroProof

deleted def Linarith.mkNegOneLtZeroProof

deleted def Linarith.mulExpr'

deleted def Linarith.mulExpr

deleted def Linarith.proveEqZeroUsing

deleted def Linarith.proveFalseByLinarith

deleted def Linarith.typeOfIneqProof

added def Mathlib.Tactic.Linarith.addExprs'

added def Mathlib.Tactic.Linarith.addExprs

added def Mathlib.Tactic.Linarith.addIneq

added def Mathlib.Tactic.Linarith.addNegEqProofs

added def Mathlib.Tactic.Linarith.leftOfIneqProof

added def Mathlib.Tactic.Linarith.mkLTZeroProof

added def Mathlib.Tactic.Linarith.mkNegOneLtZeroProof

added def Mathlib.Tactic.Linarith.mulExpr'

added def Mathlib.Tactic.Linarith.mulExpr

added def Mathlib.Tactic.Linarith.proveEqZeroUsing

added def Mathlib.Tactic.Linarith.proveFalseByLinarith

added def Mathlib.Tactic.Linarith.typeOfIneqProof