Commit 2024-05-15 13:09 600a5fa3

View on Github →

feat: port cc tactic (2/3) (#11960) In this PR, we implements process when an new equation is added to a congruence closure. Also, Lean.Expr.relSidesIfSymm? is removed in #11162, but this def is required for cc tactic, so we recover this.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/CC/Addition.lean

added def Mathlib.Tactic.CC.CCM.add

added def Mathlib.Tactic.CC.CCM.addACEq

added def Mathlib.Tactic.CC.CCM.addCongruenceTable

added def Mathlib.Tactic.CC.CCM.addEqvCore

added def Mathlib.Tactic.CC.CCM.addEqvStep

added def Mathlib.Tactic.CC.CCM.addOccurrence

added def Mathlib.Tactic.CC.CCM.addSymmCongruenceTable

added def Mathlib.Tactic.CC.CCM.checkEqTrue

added def Mathlib.Tactic.CC.CCM.checkInvariant

added def Mathlib.Tactic.CC.CCM.checkNewSubsingletonEq

added def Mathlib.Tactic.CC.CCM.collapseAC

added def Mathlib.Tactic.CC.CCM.collectFnRoots

added def Mathlib.Tactic.CC.CCM.compareSymm

added def Mathlib.Tactic.CC.CCM.compareSymmAux

added def Mathlib.Tactic.CC.CCM.composeAC

added def Mathlib.Tactic.CC.CCM.dbgTraceACEq

added def Mathlib.Tactic.CC.CCM.dbgTraceACState

added def Mathlib.Tactic.CC.CCM.eraseRBHSOccs

added def Mathlib.Tactic.CC.CCM.eraseROccs

added def Mathlib.Tactic.CC.CCM.eraseRRHSOccs

added def Mathlib.Tactic.CC.CCM.flipDelayedProofCore

added def Mathlib.Tactic.CC.CCM.flipProof

added def Mathlib.Tactic.CC.CCM.flipProofCore

added def Mathlib.Tactic.CC.CCM.getACTodo

added def Mathlib.Tactic.CC.CCM.getCache

added def Mathlib.Tactic.CC.CCM.getEntry

added def Mathlib.Tactic.CC.CCM.getEqFalseProof

added def Mathlib.Tactic.CC.CCM.getEqTrueProof

added def Mathlib.Tactic.CC.CCM.getEqcLambdas

added def Mathlib.Tactic.CC.CCM.getInconsistencyProof

added def Mathlib.Tactic.CC.CCM.getPropEqProof

added def Mathlib.Tactic.CC.CCM.getRoot

added def Mathlib.Tactic.CC.CCM.getTodo

added def Mathlib.Tactic.CC.CCM.hasHEqProofs

added def Mathlib.Tactic.CC.CCM.insertEraseROcc

added def Mathlib.Tactic.CC.CCM.insertEraseROccs

added def Mathlib.Tactic.CC.CCM.insertRBHSOccs

added def Mathlib.Tactic.CC.CCM.insertROccs

added def Mathlib.Tactic.CC.CCM.insertRRHSOccs

added def Mathlib.Tactic.CC.CCM.internalize

added def Mathlib.Tactic.CC.CCM.internalizeAC

added def Mathlib.Tactic.CC.CCM.internalizeACVar

added def Mathlib.Tactic.CC.CCM.isAC

added def Mathlib.Tactic.CC.CCM.isCgRoot

added def Mathlib.Tactic.CC.CCM.isEqFalse

added def Mathlib.Tactic.CC.CCM.isEqTrue

added def Mathlib.Tactic.CC.CCM.isEqv

added def Mathlib.Tactic.CC.CCM.isNotEqv

added def Mathlib.Tactic.CC.CCM.mayPropagate

added def Mathlib.Tactic.CC.CCM.mkACProof

added def Mathlib.Tactic.CC.CCM.mkACSimpProof

added def Mathlib.Tactic.CC.CCM.mkACSuperposeProof

added def Mathlib.Tactic.CC.CCM.mkCCCongrTheorem

added def Mathlib.Tactic.CC.CCM.mkCCHCongrTheorem

added def Mathlib.Tactic.CC.CCM.mkCongruencesKey

added def Mathlib.Tactic.CC.CCM.mkNeOfEqOfNe

added def Mathlib.Tactic.CC.CCM.mkNeOfNeOfEq

added def Mathlib.Tactic.CC.CCM.mkSymmCongruencesKey

added def Mathlib.Tactic.CC.CCM.mkTrans

added def Mathlib.Tactic.CC.CCM.mkTransOpt

added def Mathlib.Tactic.CC.CCM.modifyACTodo

added def Mathlib.Tactic.CC.CCM.modifyCache

added def Mathlib.Tactic.CC.CCM.modifyTodo

added def Mathlib.Tactic.CC.CCM.normalize

added def Mathlib.Tactic.CC.CCM.processAC

added def Mathlib.Tactic.CC.CCM.processTodo

added def Mathlib.Tactic.CC.CCM.propagateAndDown

added def Mathlib.Tactic.CC.CCM.propagateBeta

added def Mathlib.Tactic.CC.CCM.propagateBetaToEqc

added def Mathlib.Tactic.CC.CCM.propagateDown

added def Mathlib.Tactic.CC.CCM.propagateEqDown

added def Mathlib.Tactic.CC.CCM.propagateExistsDown

added def Mathlib.Tactic.CC.CCM.propagateInstImplicit

added def Mathlib.Tactic.CC.CCM.propagateNotDown

added def Mathlib.Tactic.CC.CCM.propagateOrDown

added def Mathlib.Tactic.CC.CCM.propagateProjectionConstructor

added def Mathlib.Tactic.CC.CCM.propagateValueInconsistency

added def Mathlib.Tactic.CC.CCM.pushEq

added def Mathlib.Tactic.CC.CCM.pushHEq

added def Mathlib.Tactic.CC.CCM.pushReflEq

added def Mathlib.Tactic.CC.CCM.pushSubsingletonEq

added def Mathlib.Tactic.CC.CCM.pushTodo

added def Mathlib.Tactic.CC.CCM.reinsertParents

added def Mathlib.Tactic.CC.CCM.removeParents

added def Mathlib.Tactic.CC.CCM.run

added def Mathlib.Tactic.CC.CCM.setACVar

added def Mathlib.Tactic.CC.CCM.setFO

added def Mathlib.Tactic.CC.CCM.simplifyAC

added def Mathlib.Tactic.CC.CCM.simplifyACCore

added def Mathlib.Tactic.CC.CCM.simplifyACStep

added def Mathlib.Tactic.CC.CCM.superposeAC

Modified Mathlib/Tactic/CC/Datatypes.lean

modified def Mathlib.Tactic.CC.ACApps.append

modified def Mathlib.Tactic.CC.ACApps.diff

modified def Mathlib.Tactic.CC.ACApps.intersection

Created Mathlib/Tactic/Relation/Symm.lean

added def Lean.Expr.relSidesIfSymm?

Modified scripts/noshake.json

Modified scripts/style-exceptions.txt