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.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Update the acTodo field of the state.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Read the todo field of the state.

Equations

• Mathlib.Tactic.CC.CCM.getTodo = do let __do_lift ← get pure __do_lift.todo

@[inline]

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

Read the acTodo field of the state.

Equations

• Mathlib.Tactic.CC.CCM.getACTodo = do let __do_lift ← get pure __do_lift.acTodo

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.

Equations

• Mathlib.Tactic.CC.CCM.pushTodo lhs rhs H heqProof = Mathlib.Tactic.CC.CCM.modifyTodo fun (todo : Array Mathlib.Tactic.CC.TodoEntry) => todo.push (lhs, rhs, H, heqProof)

@[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.

Equations

• Mathlib.Tactic.CC.CCM.pushEq lhs rhs H = Mathlib.Tactic.CC.CCM.pushTodo lhs rhs H false

@[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.

Equations

• Mathlib.Tactic.CC.CCM.pushHEq lhs rhs H = Mathlib.Tactic.CC.CCM.pushTodo lhs rhs H true

@[inline]

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

Add rfl : lhs = rhs to the todo list.

Equations

• Mathlib.Tactic.CC.CCM.pushReflEq lhs rhs = Mathlib.Tactic.CC.CCM.pushEq lhs rhs Mathlib.Tactic.CC.EntryExpr.refl

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

Update the child so its parent becomes parent.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.CC.CCM.mkCongruencesKey e = failure

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

Return the SymmCongruencesKey associated with the equality lhs = rhs.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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₂.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Trace the state of AC module.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.CC.CCM.insertEraseROccs (↑e_2) lhs inLHS isInsert = Mathlib.Tactic.CC.CCM.insertEraseROcc e_2 lhs inLHS isInsert

@[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.

Equations

• Mathlib.Tactic.CC.CCM.insertROccs e lhs inLHS = Mathlib.Tactic.CC.CCM.insertEraseROccs e lhs inLHS true

@[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.

Equations

• Mathlib.Tactic.CC.CCM.eraseROccs e lhs inLHS = Mathlib.Tactic.CC.CCM.insertEraseROccs e lhs inLHS false

@[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.

Equations

• Mathlib.Tactic.CC.CCM.insertRBHSOccs lhs rhs = do Mathlib.Tactic.CC.CCM.insertROccs lhs lhs true Mathlib.Tactic.CC.CCM.insertROccs rhs lhs false

@[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.

Equations

• Mathlib.Tactic.CC.CCM.eraseRBHSOccs lhs rhs = do Mathlib.Tactic.CC.CCM.eraseROccs lhs lhs true Mathlib.Tactic.CC.CCM.eraseROccs rhs lhs false

@[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.

Equations

• Mathlib.Tactic.CC.CCM.insertRRHSOccs e lhs = Mathlib.Tactic.CC.CCM.insertROccs e lhs false

@[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.

Equations

• Mathlib.Tactic.CC.CCM.eraseRRHSOccs e lhs = Mathlib.Tactic.CC.CCM.eraseROccs e lhs false

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.CC.CCM.mkACSuperposeProof ra sb a b r s ts (Mathlib.Tactic.CC.ACApps.apps op args) tsEqa trEqb = failure
• Mathlib.Tactic.CC.CCM.mkACSuperposeProof ra sb a b r s ts tr tsEqa trEqb = failure

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.CC.CCM.superposeAC ts a tsEqa = pure PUnit.unit

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

Process the tasks in the acTodo field.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.CC.CCM.isAC e = pure none

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Propagate equality from a and b to a ∧ b.

Equations

• One or more equations did not get rendered due to their size.

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

Propagate equality from a and b to a ∨ b.

Equations

• One or more equations did not get rendered due to their size.

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

Propagate equality from a to ¬a.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.CC.CCM.propagateIteUp e = failure

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

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

Equations

• One or more equations did not get rendered due to their size.

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?

Equations

• Mathlib.Tactic.CC.CCM.mayPropagate e = (e.isAppOfArity `Iff 2 || e.isAppOfArity `And 2 || e.isAppOfArity `Or 2 || e.isAppOfArity `Not 1 || e.isArrow || e.isIte)

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Check for integrity of the CCStructure.

Equations

• Mathlib.Tactic.CC.CCM.checkInvariant = do let __do_lift ← get guard (__do_lift.checkInvariant = true)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Propagate equality from ¬a to a.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Propagate equality from e to subexpressions of e.

Equations

• One or more equations did not get rendered due to their size.

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).

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Process the tasks in the todo field.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Mathlib.Tactic.CC.CCM.internalize e = do Mathlib.Tactic.CC.CCM.internalizeCore e none Mathlib.Tactic.CC.CCM.processTodo

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.

Equations

• Mathlib.Tactic.CC.CCM.addEqvCore lhs rhs H heqProof = do Mathlib.Tactic.CC.CCM.pushTodo lhs rhs (↑H) heqProof Mathlib.Tactic.CC.CCM.processTodo

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

Add proof : type to the congruence closure.