Commit 2024-04-24 13:42 069f405e

View on Github →

feat: port cc tactic (1/3) (#11956) In this PR, we implements datatypes which is used in cc tactic. Also, Init.CCLemmas is removed in #10696, but this module is required for cc tactic, so we recover this module as Tactic.CC.Lemmas.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/CC/Datatypes.lean

added def Mathlib.Tactic.CC.ACApps.append

added def Mathlib.Tactic.CC.ACApps.diff

added def Mathlib.Tactic.CC.ACApps.intersection

added def Mathlib.Tactic.CC.ACApps.isSubset

added def Mathlib.Tactic.CC.ACApps.mkApps

added def Mathlib.Tactic.CC.ACApps.mkFlatApps

added def Mathlib.Tactic.CC.ACApps.toExpr

added inductive Mathlib.Tactic.CC.ACApps

added def Mathlib.Tactic.CC.ACEntry.ROccs

added structure Mathlib.Tactic.CC.ACEntry

added structure Mathlib.Tactic.CC.CCConfig

added structure Mathlib.Tactic.CC.CCCongrTheorem

added structure Mathlib.Tactic.CC.CCCongrTheoremKey

added structure Mathlib.Tactic.CC.CCNormalizer

added structure Mathlib.Tactic.CC.CCPropagationHandler

added def Mathlib.Tactic.CC.CCState.checkEqc

added def Mathlib.Tactic.CC.CCState.checkInvariant

added def Mathlib.Tactic.CC.CCState.getNumROccs

added def Mathlib.Tactic.CC.CCState.getRoots

added def Mathlib.Tactic.CC.CCState.getVarWithLeastLHSOccs

added def Mathlib.Tactic.CC.CCState.getVarWithLeastOccs

added def Mathlib.Tactic.CC.CCState.getVarWithLeastRHSOccs

added def Mathlib.Tactic.CC.CCState.inSingletonEqc

added def Mathlib.Tactic.CC.CCState.isCgRoot

added def Mathlib.Tactic.CC.CCState.mkEntryCore

added def Mathlib.Tactic.CC.CCState.mt

added def Mathlib.Tactic.CC.CCState.next

added def Mathlib.Tactic.CC.CCState.ppAC

added def Mathlib.Tactic.CC.CCState.ppACDecl

added def Mathlib.Tactic.CC.CCState.ppACDecls

added def Mathlib.Tactic.CC.CCState.ppACExpr

added def Mathlib.Tactic.CC.CCState.ppACR

added def Mathlib.Tactic.CC.CCState.ppEqc

added def Mathlib.Tactic.CC.CCState.ppEqcs

added def Mathlib.Tactic.CC.CCState.ppParentOccs

added def Mathlib.Tactic.CC.CCState.ppParentOccsAux

added def Mathlib.Tactic.CC.CCState.root

added structure Mathlib.Tactic.CC.CCState

added structure Mathlib.Tactic.CC.CCStructure

added inductive Mathlib.Tactic.CC.CongruencesKey

added inductive Mathlib.Tactic.CC.DelayedExpr

added structure Mathlib.Tactic.CC.Entry

added inductive Mathlib.Tactic.CC.EntryExpr

added structure Mathlib.Tactic.CC.ParentOcc

added structure Mathlib.Tactic.CC.SymmCongruencesKey

added def Mathlib.Tactic.CC.isInterpretedValue

added def Mathlib.Tactic.CC.isValue

added def Mathlib.Tactic.CC.liftFromEq

added def Mathlib.Tactic.CC.mkCCHCongrWithArity

Created Mathlib/Tactic/CC/Lemmas.lean

added theorem Mathlib.Tactic.CC.and_eq_of_eq

added theorem Mathlib.Tactic.CC.and_eq_of_eq_false_left

added theorem Mathlib.Tactic.CC.and_eq_of_eq_false_right

added theorem Mathlib.Tactic.CC.and_eq_of_eq_true_left

added theorem Mathlib.Tactic.CC.and_eq_of_eq_true_right

added theorem Mathlib.Tactic.CC.eq_false_of_not_eq_true

added theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_left

added theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_right

added theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_left

added theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_right

added theorem Mathlib.Tactic.CC.eq_true_of_not_eq_false

added theorem Mathlib.Tactic.CC.false_of_a_eq_not_a

added theorem Mathlib.Tactic.CC.if_eq_of_eq

added theorem Mathlib.Tactic.CC.if_eq_of_eq_false

added theorem Mathlib.Tactic.CC.if_eq_of_eq_true

added theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_left

added theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_right

added theorem Mathlib.Tactic.CC.iff_eq_true_of_eq

added theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_left

added theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_right

added theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_left

added theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_right

added theorem Mathlib.Tactic.CC.imp_eq_true_of_eq

added theorem Mathlib.Tactic.CC.not_eq_of_eq_false

added theorem Mathlib.Tactic.CC.not_eq_of_eq_true

added theorem Mathlib.Tactic.CC.not_imp_eq_of_eq_false_right

added theorem Mathlib.Tactic.CC.or_eq_of_eq

added theorem Mathlib.Tactic.CC.or_eq_of_eq_false_left

added theorem Mathlib.Tactic.CC.or_eq_of_eq_false_right

added theorem Mathlib.Tactic.CC.or_eq_of_eq_true_left

added theorem Mathlib.Tactic.CC.or_eq_of_eq_true_right

Modified scripts/nolints.json