Process when an new equation is added to a congruence closure

@[inline]

def Mathlib.Tactic.CC.CCM.modifyTodo (f : Array TodoEntry → Array TodoEntry) : CCM Unit

Update the todo field of the state.

@[inline]

def Mathlib.Tactic.CC.CCM.modifyACTodo (f : Array ACTodoEntry → Array ACTodoEntry) : CCM Unit

Update the acTodo field of the state.

@[inline]

def Mathlib.Tactic.CC.CCM.getTodo : CCM (Array TodoEntry)

Read the todo field of the state.

@[inline]

def Mathlib.Tactic.CC.CCM.getACTodo : CCM (Array ACTodoEntry)

Read the acTodo field of the state.

def Mathlib.Tactic.CC.CCM.pushTodo (lhs rhs : Lean.Expr) (H : EntryExpr) (heqProof : Bool) : CCM Unit

Add a new entry to the end of the todo list.

See also pushEq, pushHEq and pushReflEq.

@[inline]

def Mathlib.Tactic.CC.CCM.pushEq (lhs rhs : Lean.Expr) (H : EntryExpr) : CCM Unit

Add the equality proof H : lhs = rhs to the end of the todo list.

@[inline]

def Mathlib.Tactic.CC.CCM.pushHEq (lhs rhs : Lean.Expr) (H : EntryExpr) : CCM Unit

Add the heterogeneous equality proof H : HEq lhs rhs to the end of the todo list.

@[inline]

def Mathlib.Tactic.CC.CCM.pushReflEq (lhs rhs : Lean.Expr) : CCM Unit

Add rfl : lhs = rhs to the todo list.

def Mathlib.Tactic.CC.CCM.addOccurrence (parent child : Lean.Expr) (symmTable : Bool) : CCM Unit

Update the child so its parent becomes parent.

def Mathlib.Tactic.CC.CCM.propagateInstImplicit (e : Lean.Expr) : CCM Unit

Record the instance e and add it to the set of known defeq instances.

def Mathlib.Tactic.CC.CCM.mkCongruencesKey (e : Lean.Expr) : CCM CongruencesKey

Return the CongruencesKey associated with an expression of the form f a.

def Mathlib.Tactic.CC.CCM.mkSymmCongruencesKey (lhs rhs : Lean.Expr) : CCM SymmCongruencesKey

Return the SymmCongruencesKey associated with the equality lhs = rhs.

def Mathlib.Tactic.CC.CCM.compareSymmAux (lhs₁ rhs₁ lhs₂ rhs₂ : Lean.Expr) : CCM Bool

Auxiliary function for comparing lhs₁ ~ rhs₁ and lhs₂ ~ rhs₂, when ~ is symmetric/commutative. It returns true (equal) for a ~ b b ~ a.

def Mathlib.Tactic.CC.CCM.compareSymm (k₁ k₂ : Lean.Expr × Lean.Name) : CCM Bool

Given k₁ := (R₁ lhs₁ rhs₁, `R₁) and k₂ := (R₂ lhs₂ rhs₂, `R₂), return true if R₁ lhs₁ rhs₁ is equivalent to R₂ lhs₂ rhs₂ modulo the symmetry of R₁ and R₂.

def Mathlib.Tactic.CC.CCM.checkEqTrue (e : Lean.Expr) : CCM Unit

Given e := R lhs rhs, if R is a reflexive relation and lhs is equivalent to rhs, add equality e = True.

def Mathlib.Tactic.CC.CCM.addCongruenceTable (e : Lean.Expr) : CCM Unit

If the congruence table (congruences field) has congruent expression to e, add the equality to the todo list. If not, add e to the congruence table.

def Mathlib.Tactic.CC.CCM.addSymmCongruenceTable (e : Lean.Expr) : CCM Unit

If the symm congruence table (symmCongruences field) has congruent expression to e, add the equality to the todo list. If not, add e to the symm congruence table.

def Mathlib.Tactic.CC.CCM.pushSubsingletonEq (a b : Lean.Expr) : CCM Unit

Given subsingleton elements a and b which are not necessarily of the same type, if the types of a and b are equivalent, add the (heterogeneous) equality proof between a and b to the todo list.

def Mathlib.Tactic.CC.CCM.checkNewSubsingletonEq (oldRoot newRoot : Lean.Expr) : CCM Unit

Given the equivalent expressions oldRoot and newRoot the root of oldRoot is newRoot, if oldRoot has root representative of subsingletons, try to push the equality proof between their root representatives to the todo list, or update the root representative to newRoot.

def Mathlib.Tactic.CC.CCM.getEqcLambdas (e : Lean.Expr) (r : Array Lean.Expr := #[]) : CCM (Array Lean.Expr)

Get all lambda expressions in the equivalence class of e and append to r.

e must be the root of its equivalence class.

def Mathlib.Tactic.CC.CCM.propagateBeta (fn : Lean.Expr) (revArgs lambdas : Array Lean.Expr) (newLambdaApps : Array Lean.Expr := #[]) : CCM (Array Lean.Expr)

Remove fn and expressions whose type isn't def-eq to fn's type out from lambdas, return the remaining lambdas applied to the reversed arguments.

def Mathlib.Tactic.CC.CCM.dbgTraceACEq (header : String) (lhs rhs : ACApps) : CCM Unit

Given lhs, rhs, and header := "my header:", Trace my header: lhs = rhs.

def Mathlib.Tactic.CC.CCM.dbgTraceACState : CCM Unit

Trace the state of AC module.

def Mathlib.Tactic.CC.CCM.insertEraseROcc (arg : Lean.Expr) (lhs : ACApps) (inLHS isInsert : Bool) : CCM Unit

Insert or erase lhs to the occurrences of arg on an equality in acR.

def Mathlib.Tactic.CC.CCM.insertEraseROccs (e lhs : ACApps) (inLHS isInsert : Bool) : CCM Unit

Insert or erase lhs to the occurrences of arguments of e on an equality in acR.

@[inline]

def Mathlib.Tactic.CC.CCM.insertROccs (e lhs : ACApps) (inLHS : Bool) : CCM Unit

Insert lhs to the occurrences of arguments of e on an equality in acR.

@[inline]

def Mathlib.Tactic.CC.CCM.eraseROccs (e lhs : ACApps) (inLHS : Bool) : CCM Unit

Erase lhs to the occurrences of arguments of e on an equality in acR.

@[inline]

def Mathlib.Tactic.CC.CCM.insertRBHSOccs (lhs rhs : ACApps) : CCM Unit

Insert lhs to the occurrences on an equality in acR corresponding to the equality lhs := rhs.

@[inline]

def Mathlib.Tactic.CC.CCM.eraseRBHSOccs (lhs rhs : ACApps) : CCM Unit

Erase lhs to the occurrences on an equality in acR corresponding to the equality lhs := rhs.

@[inline]

def Mathlib.Tactic.CC.CCM.insertRRHSOccs (e lhs : ACApps) : CCM Unit

Insert lhs to the occurrences of arguments of e on the right hand side of an equality in acR.

@[inline]

def Mathlib.Tactic.CC.CCM.eraseRRHSOccs (e lhs : ACApps) : CCM Unit

Erase lhs to the occurrences of arguments of e on the right hand side of an equality in acR.

def Mathlib.Tactic.CC.CCM.composeAC (lhs rhs : ACApps) (H : DelayedExpr) : CCM Unit

Try to simplify the right hand sides of equalities in acR by H : lhs = rhs.

def Mathlib.Tactic.CC.CCM.collapseAC (lhs rhs : ACApps) (H : DelayedExpr) : CCM Unit

Try to simplify the left hand sides of equalities in acR by H : lhs = rhs.

def Mathlib.Tactic.CC.CCM.mkACSuperposeProof (ra sb a b r s ts tr : ACApps) (tsEqa trEqb : DelayedExpr) : Lean.MetaM DelayedExpr

Given ra := a*r sb := b*s ts := t*s tr := t*r tsEqa : t*s = a trEqb : t*r = b, return a proof for ra = sb.

We use a*b to denote an AC application. That is, (a*b)*(c*a) is the term a*a*b*c.

def Mathlib.Tactic.CC.CCM.superposeAC (ts a : ACApps) (tsEqa : DelayedExpr) : CCM Unit

Given tsEqa : ts = a, for each equality trEqb : tr = b in acR where the intersection t of ts and tr is nonempty, let ts = t*s and tr := t*r, add a new equality r*a = s*b.

def Mathlib.Tactic.CC.CCM.processAC : CCM Unit

Process the tasks in the acTodo field.

def Mathlib.Tactic.CC.CCM.addACEq (e₁ e₂ : Lean.Expr) : CCM Unit

Given AC variables e₁ and e₂ which are in the same equivalence class, add the proof of e₁ = e₂ to the AC module.

def Mathlib.Tactic.CC.CCM.setACVar (e : Lean.Expr) : CCM Unit

If the root expression of e is AC variable, add equality to AC module. If not, register the AC variable to the root entry.

def Mathlib.Tactic.CC.CCM.internalizeACVar (e : Lean.Expr) : CCM Bool

If e isn't an AC variable, set e as an new AC variable.

def Mathlib.Tactic.CC.CCM.isAC (e : Lean.Expr) : CCM (Option Lean.Expr)

If e is of the form op e₁ e₂ where op is an associative and commutative binary operator, return the canonical form of op.

partial def Mathlib.Tactic.CC.CCM.convertAC (op e : Lean.Expr) (args : Array Lean.Expr := #[]) : CCM (Array Lean.Expr × Lean.Expr)

Given e := op₁ (op₂ a₁ a₂) (op₃ a₃ a₄) where opₙs are canonicalized to op, internalize aₙs as AC variables and return (op (op a₁ a₂) (op a₃ a₄), args ++ #[a₁, a₂, a₃, a₄]).

def Mathlib.Tactic.CC.CCM.internalizeAC (e : Lean.Expr) (parent? : Option Lean.Expr) : CCM Unit

Internalize e so that the AC module can deal with the given expression.

If the expression does not contain an AC operator, or the parent expression is already processed by internalizeAC, this operation does nothing.

partial def Mathlib.Tactic.CC.CCM.internalizeAppLit (e : Lean.Expr) : CCM Unit

The specialized internalizeCore for applications or literals.

partial def Mathlib.Tactic.CC.CCM.internalizeCore (e : Lean.Expr) (parent? : Option Lean.Expr) : CCM Unit

Internalize e so that the congruence closure can deal with the given expression. Don't forget to process the tasks in the todo field later.

def Mathlib.Tactic.CC.CCM.propagateIffUp (e : Lean.Expr) : CCM Unit

Propagate equality from a and b to a ↔ b.

def Mathlib.Tactic.CC.CCM.propagateAndUp (e : Lean.Expr) : CCM Unit

Propagate equality from a and b to a ∧ b.

def Mathlib.Tactic.CC.CCM.propagateOrUp (e : Lean.Expr) : CCM Unit

Propagate equality from a and b to a ∨ b.

def Mathlib.Tactic.CC.CCM.propagateNotUp (e : Lean.Expr) : CCM Unit

Propagate equality from a to ¬a.

partial def Mathlib.Tactic.CC.CCM.propagateImpUp (e : Lean.Expr) : CCM Unit

Propagate equality from a and b to a → b.

def Mathlib.Tactic.CC.CCM.propagateIteUp (e : Lean.Expr) : CCM Unit

Propagate equality from p, a and b to if p then a else b.

def Mathlib.Tactic.CC.CCM.propagateEqUp (e : Lean.Expr) : CCM Unit

Propagate equality from a and b to disprove a = b.

partial def Mathlib.Tactic.CC.CCM.propagateUp (e : Lean.Expr) : CCM Unit

Propagate equality from subexpressions of e to e.

partial def Mathlib.Tactic.CC.CCM.applySimpleEqvs (e : Lean.Expr) : CCM Unit

This method is invoked during internalization and eagerly apply basic equivalences for term e Examples:

• If e := cast H e', then it merges the equivalence classes of cast H e' and e'

In principle, we could mark theorems such as cast_eq as simplification rules, but this created problems with the builtin support for cast-introduction in the ematching module in Lean 3. TODO: check if this is now possible in Lean 4.

Eagerly merging the equivalence classes is also more efficient.

partial def Mathlib.Tactic.CC.CCM.processSubsingletonElem (e : Lean.Expr) : CCM Unit

If e is a subsingleton element, push the equality proof between e and its canonical form to the todo list or register e as the canonical form of itself.

partial def Mathlib.Tactic.CC.CCM.mkEntry (e : Lean.Expr) (interpreted : Bool) : CCM Unit

Add an new entry for e to the congruence closure.

def Mathlib.Tactic.CC.CCM.mayPropagate (e : Lean.Expr) : Bool

Can we propagate equality from subexpressions of e to e?

def Mathlib.Tactic.CC.CCM.removeParents (e : Lean.Expr) (parentsToPropagate : Array Lean.Expr := #[]) : CCM (Array Lean.Expr)

Remove parents of e from the congruence table and the symm congruence table, and append parents to propagate equality, to parentsToPropagate. Returns the new value of parentsToPropagate.

partial def Mathlib.Tactic.CC.CCM.invertTrans (e : Lean.Expr) (newFlipped : Bool := false) (newTarget : Option Lean.Expr := none) (newProof : Option EntryExpr := none) : CCM Unit

The fields target and proof in e's entry are encoding a transitivity proof Let e.rootTarget and e.rootProof denote these fields.

e = e.rootTarget            := e.rootProof
_ = e.rootTarget.rootTarget := e.rootTarget.rootProof
 ...
_ = e.root                  := ...

The transitivity proof eventually reaches the root of the equivalence class. This method "inverts" the proof. That is, the target goes from e.root to e after we execute it.

def Mathlib.Tactic.CC.CCM.collectFnRoots (root : Lean.Expr) (fnRoots : Array Lean.Expr := #[]) : CCM (Array Lean.Expr)

Traverse the root's equivalence class, and for each function application, collect the function's equivalence class root.

def Mathlib.Tactic.CC.CCM.reinsertParents (e : Lean.Expr) : CCM Unit

Reinsert parents of e to the congruence table and the symm congruence table.

Together with removeParents, this allows modifying parents of an expression.

def Mathlib.Tactic.CC.CCM.checkInvariant : CCM Unit

Check for integrity of the CCStructure.

def Mathlib.Tactic.CC.CCM.propagateBetaToEqc (fnRoots lambdas : Array Lean.Expr) (newLambdaApps : Array Lean.Expr := #[]) : CCM (Array Lean.Expr)

For each fnRoot in fnRoots traverse its parents, and look for a parent prefix that is in the same equivalence class of the given lambdas.

remark All expressions in lambdas are in the same equivalence class

def Mathlib.Tactic.CC.CCM.propagateProjectionConstructor (p c : Lean.Expr) : CCM Unit

Given c a constructor application, if p is a projection application (not .proj _ _ _, but .app (.const projName _) _) such that major premise is equal to c, then propagate new equality.

Example: if p is of the form b.fst, c is of the form (x, y), and b = c, we add the equality (x, y).fst = x

def Mathlib.Tactic.CC.CCM.propagateConstructorEq (e₁ e₂ : Lean.Expr) : CCM Unit

Given a new equality e₁ = e₂, where e₁ and e₂ are constructor applications. Implement the following implications:

c a₁ ... aₙ = c b₁ ... bₙ => a₁ = b₁, ..., aₙ = bₙ

c₁ ... = c₂ ... => False

where c, c₁ and c₂ are constructors

partial def Mathlib.Tactic.CC.CCM.propagateConstructorEq.go (type val : Lean.Expr) : CCM Unit

Given an injective theorem val : type, whose type is the form of a₁ = a₂ ∧ HEq b₁ b₂ ∧ .., destruct val and push equality proofs to the todo list.

def Mathlib.Tactic.CC.CCM.propagateValueInconsistency (e₁ e₂ : Lean.Expr) : CCM Unit

Derive contradiction if we can get equality between different values.

def Mathlib.Tactic.CC.CCM.propagateAndDown (e : Lean.Expr) : CCM Unit

Propagate equality from a ∧ b = True to a = True and b = True.

def Mathlib.Tactic.CC.CCM.propagateOrDown (e : Lean.Expr) : CCM Unit

Propagate equality from a ∨ b = False to a = False and b = False.

def Mathlib.Tactic.CC.CCM.propagateNotDown (e : Lean.Expr) : CCM Unit

Propagate equality from ¬a to a.

def Mathlib.Tactic.CC.CCM.propagateEqDown (e : Lean.Expr) : CCM Unit

Propagate equality from (a = b) = True to a = b.

def Mathlib.Tactic.CC.CCM.propagateExistsDown (e : Lean.Expr) : CCM Unit

Propagate equality from ¬∃ x, p x to ∀ x, ¬p x.

def Mathlib.Tactic.CC.CCM.propagateDown (e : Lean.Expr) : CCM Unit

Propagate equality from e to subexpressions of e.

def Mathlib.Tactic.CC.CCM.addEqvStep (e₁ e₂ : Lean.Expr) (H : EntryExpr) (heqProof : Bool) : CCM Unit

Performs one step in the process when the new equation is added.

Here, H contains the proof that e₁ = e₂ (if heqProof is false) or HEq e₁ e₂ (if heqProof is true).

def Mathlib.Tactic.CC.CCM.addEqvStep.go (e₁ e₂ : Lean.Expr) (n₁ n₂ r₁ r₂ : Entry) (flipped : Bool) (H : EntryExpr) (heqProof : Bool) : CCM Unit

The auxiliary definition for addEqvStep to flip the input.

def Mathlib.Tactic.CC.CCM.processTodo : CCM Unit

Process the tasks in the todo field.

def Mathlib.Tactic.CC.CCM.internalize (e : Lean.Expr) : CCM Unit

Internalize e so that the congruence closure can deal with the given expression.

def Mathlib.Tactic.CC.CCM.addEqvCore (lhs rhs H : Lean.Expr) (heqProof : Bool) : CCM Unit

Add H : lhs = rhs or H : HEq lhs rhs to the congruence closure. Don't forget to internalize lhs and rhs beforehand.

def Mathlib.Tactic.CC.CCM.add (type proof : Lean.Expr) : CCM Unit

Add proof : type to the congruence closure.