Process when an new equation is added to a congruence closure

@[reducible, inline]

abbrev Mathlib.Tactic.CC.CCM (α : Type) : Type

The monad for the cc tactic stores the current state of the tactic.

Equations

• Mathlib.Tactic.CC.CCM = StateRefT' IO.RealWorld Mathlib.Tactic.CC.CCStructure Lean.MetaM

@[inline]

def Mathlib.Tactic.CC.CCM.run {α : Type} (x : Mathlib.Tactic.CC.CCM α) (c : Mathlib.Tactic.CC.CCStructure) : Lean.MetaM (α × Mathlib.Tactic.CC.CCStructure)

Run a computation in the CCM monad.

Equations

• x.run c = StateRefT'.run x c

@[inline]

def Mathlib.Tactic.CC.CCM.modifyTodo (f : Array Mathlib.Tactic.CC.TodoEntry → Array Mathlib.Tactic.CC.TodoEntry) : Mathlib.Tactic.CC.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 Mathlib.Tactic.CC.ACTodoEntry → Array Mathlib.Tactic.CC.ACTodoEntry) : Mathlib.Tactic.CC.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.modifyCache (f : Mathlib.Tactic.CC.CCCongrTheoremCache → Mathlib.Tactic.CC.CCCongrTheoremCache) : Mathlib.Tactic.CC.CCM Unit

Update the cache field of the state.

Equations

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

@[inline]

def Mathlib.Tactic.CC.CCM.getTodo : Mathlib.Tactic.CC.CCM (Array Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.CCM (Array Mathlib.Tactic.CC.ACTodoEntry)

Read the acTodo field of the state.

Equations

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

@[inline]

def Mathlib.Tactic.CC.CCM.getCache : Mathlib.Tactic.CC.CCM Mathlib.Tactic.CC.CCCongrTheoremCache

Read the cache field of the state.

Equations

• Mathlib.Tactic.CC.CCM.getCache = do let __do_lift ← get pure __do_lift.cache

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

Look up an entry associated with the given expression.

Equations

• Mathlib.Tactic.CC.CCM.getEntry e = do let __do_lift ← get pure (Batteries.RBMap.find? __do_lift.entries e)

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

Use the normalizer to normalize e.

If no normalizer was configured, returns e itself.

Equations

• Mathlib.Tactic.CC.CCM.normalize e = do let __do_lift ← get match __do_lift.normalizer with | some normalizer => liftM (normalizer.normalize e) | x => pure e

def Mathlib.Tactic.CC.CCM.pushTodo (lhs : Lean.Expr) (rhs : Lean.Expr) (H : Mathlib.Tactic.CC.EntryExpr) (heqProof : Bool) : Mathlib.Tactic.CC.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 : Lean.Expr) (rhs : Lean.Expr) (H : Mathlib.Tactic.CC.EntryExpr) : Mathlib.Tactic.CC.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 : Lean.Expr) (rhs : Lean.Expr) (H : Mathlib.Tactic.CC.EntryExpr) : Mathlib.Tactic.CC.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 : Lean.Expr) (rhs : Lean.Expr) : Mathlib.Tactic.CC.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.getRoot (e : Lean.Expr) : Mathlib.Tactic.CC.CCM Lean.Expr

Return the root expression of the expression's congruence class.

Equations

• Mathlib.Tactic.CC.CCM.getRoot e = do let __do_lift ← get pure (__do_lift.root e)

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

Is e the root of its congruence class?

Equations

• Mathlib.Tactic.CC.CCM.isCgRoot e = do let __do_lift ← get pure (__do_lift.isCgRoot e)

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

Update the child so its parent becomes parent.

Equations

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

partial def Mathlib.Tactic.CC.CCM.isCongruent (e₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.CCM Bool

Return true iff the given function application are congruent

e₁ should have the form f a and e₂ the form g b.

See paper: Congruence Closure for Intensional Type Theory.

def Mathlib.Tactic.CC.CCM.mkCongruencesKey (e : Lean.Expr) : Mathlib.Tactic.CC.CCM Mathlib.Tactic.CC.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.

def Mathlib.Tactic.CC.CCM.mkSymmCongruencesKey (lhs : Lean.Expr) (rhs : Lean.Expr) : Mathlib.Tactic.CC.CCM Mathlib.Tactic.CC.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.mkCCHCongrTheorem (fn : Lean.Expr) (nargs : Nat) : Mathlib.Tactic.CC.CCM (Option Mathlib.Tactic.CC.CCCongrTheorem)

Try to find a congruence theorem for an application of fn with nargs arguments, with support for HEq.

Equations

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

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

Try to find a congruence theorem for the expression e with support for HEq.

Equations

• Mathlib.Tactic.CC.CCM.mkCCCongrTheorem e = let fn := e.getAppFn; let nargs := e.getAppNumArgs; Mathlib.Tactic.CC.CCM.mkCCHCongrTheorem fn nargs

def Mathlib.Tactic.CC.CCM.propagateInstImplicit (e : Lean.Expr) : Mathlib.Tactic.CC.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.setFO (e : Lean.Expr) : Mathlib.Tactic.CC.CCM Unit

Treat the entry associated with e as a first-order function.

Equations

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

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

Update the modification time of the congruence class of e.

def Mathlib.Tactic.CC.CCM.hasHEqProofs (root : Lean.Expr) : Mathlib.Tactic.CC.CCM Bool

Does the congruence class with root root have any HEq proofs?

Equations

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

def Mathlib.Tactic.CC.CCM.flipProofCore (H : Lean.Expr) (flipped : Bool) (heqProofs : Bool) : Mathlib.Tactic.CC.CCM Lean.Expr

Apply symmetry to H, which is an Eq or a HEq.

• If heqProofs is true, ensure the result is a HEq (otherwise it is assumed to be Eq).
• If flipped is true, apply symm, otherwise keep the same direction.

Equations

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

def Mathlib.Tactic.CC.CCM.flipDelayedProofCore (H : Mathlib.Tactic.CC.DelayedExpr) (flipped : Bool) (heqProofs : Bool) : Mathlib.Tactic.CC.CCM Mathlib.Tactic.CC.DelayedExpr

In a delayed way, apply symmetry to H, which is an Eq or a HEq.

• If heqProofs is true, ensure the result is a HEq (otherwise it is assumed to be Eq).
• If flipped is true, apply symm, otherwise keep the same direction.

Equations

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

def Mathlib.Tactic.CC.CCM.flipProof (H : Mathlib.Tactic.CC.EntryExpr) (flipped : Bool) (heqProofs : Bool) : Mathlib.Tactic.CC.CCM Mathlib.Tactic.CC.EntryExpr

Apply symmetry to H, which is an Eq or a HEq.

• If heqProofs is true, ensure the result is a HEq (otherwise it is assumed to be Eq).
• If flipped is true, apply symm, otherwise keep the same direction.

Equations

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

def Mathlib.Tactic.CC.CCM.isEqv (e₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.CCM Bool

Are e₁ and e₂ known to be in the same equivalence class?

Equations

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

def Mathlib.Tactic.CC.CCM.isNotEqv (e₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.CCM Bool

Is e₁ ≠ e₂ known to be true?

Note that this is stronger than not (isEqv e₁ e₂): only if we can prove they are distinct this returns true.

Equations

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

@[inline]

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

Is the proposition e known to be true?

Equations

• Mathlib.Tactic.CC.CCM.isEqTrue e = Mathlib.Tactic.CC.CCM.isEqv e (Lean.Expr.const `True [])

@[inline]

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

Is the proposition e known to be false?

Equations

• Mathlib.Tactic.CC.CCM.isEqFalse e = Mathlib.Tactic.CC.CCM.isEqv e (Lean.Expr.const `False [])

def Mathlib.Tactic.CC.CCM.mkTrans (H₁ : Lean.Expr) (H₂ : Lean.Expr) (heqProofs : Bool) : Lean.MetaM Lean.Expr

Apply transitivity to H₁ and H₂, which are both Eq or HEq depending on heqProofs.

Equations

• Mathlib.Tactic.CC.CCM.mkTrans H₁ H₂ heqProofs = if heqProofs = true then Lean.Meta.mkHEqTrans H₁ H₂ else Lean.Meta.mkEqTrans H₁ H₂

def Mathlib.Tactic.CC.CCM.mkTransOpt (H₁? : Option Lean.Expr) (H₂ : Lean.Expr) (heqProofs : Bool) : Lean.MetaM Lean.Expr

Apply transitivity to H₁? and H₂, which are both Eq or HEq depending on heqProofs.

If H₁? is none, return H₂ instead.

Equations

• Mathlib.Tactic.CC.CCM.mkTransOpt H₁? H₂ heqProofs = match H₁? with | some H₁ => Mathlib.Tactic.CC.CCM.mkTrans H₁ H₂ heqProofs | none => pure H₂

partial def Mathlib.Tactic.CC.CCM.mkCongrProofCore (lhs : Lean.Expr) (rhs : Lean.Expr) (heqProofs : Bool) : Mathlib.Tactic.CC.CCM Lean.Expr

Use congruence on arguments to prove lhs = rhs.

That is, tries to prove that lhsFn lhsArgs[0] ... lhsArgs[n-1] = lhsFn rhsArgs[0] ... rhsArgs[n-1] by showing that lhsArgs[i] = rhsArgs[i] for all i.

Fails if the head function of lhs is not that of rhs.

partial def Mathlib.Tactic.CC.CCM.mkSymmCongrProof (e₁ : Lean.Expr) (e₂ : Lean.Expr) (heqProofs : Bool) : Mathlib.Tactic.CC.CCM (Option Lean.Expr)

If e₁ : R lhs₁ rhs₁, e₂ : R lhs₂ rhs₂ and lhs₁ = rhs₂, where R is a symmetric relation, prove R lhs₁ rhs₁ is equivalent to R lhs₂ rhs₂.

• if lhs₁ is known to equal lhs₂, return none
• if lhs₁ is not known to equal rhs₂, fail.

partial def Mathlib.Tactic.CC.CCM.mkCongrProof (e₁ : Lean.Expr) (e₂ : Lean.Expr) (heqProofs : Bool) : Mathlib.Tactic.CC.CCM Lean.Expr

Use congruence on arguments to prove e₁ = e₂.

Special case: if e₁ and e₂ have the form R lhs₁ rhs₁ and R lhs₂ rhs₂ such that R is symmetric and lhs₁ = rhs₂, then use those facts instead.

partial def Mathlib.Tactic.CC.CCM.mkDelayedProof (H : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.CCM Lean.Expr

Turn a delayed proof into an actual proof term.

partial def Mathlib.Tactic.CC.CCM.mkProof (lhs : Lean.Expr) (rhs : Lean.Expr) (H : Mathlib.Tactic.CC.EntryExpr) (heqProofs : Bool) : Mathlib.Tactic.CC.CCM Lean.Expr

Use the format of H to try and construct a proof or lhs = rhs:

• If H = .congr, then use congruence.
• If H = .eqTrue, try to prove lhs = True or rhs = True, if they have the format R a b, by proving a = b.
• Otherwise, return the (delayed) proof encoded by H itself.

partial def Mathlib.Tactic.CC.CCM.getEqProofCore (e₁ : Lean.Expr) (e₂ : Lean.Expr) (asHEq : Bool) : Mathlib.Tactic.CC.CCM (Option Lean.Expr)

If asHEq is true, then build a proof for HEq e₁ e₂. Otherwise, build a proof for e₁ = e₂. The result is none if e₁ and e₂ are not in the same equivalence class.

@[inline]

partial def Mathlib.Tactic.CC.CCM.getEqProof (e₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.CCM (Option Lean.Expr)

Build a proof for e₁ = e₂. The result is none if e₁ and e₂ are not in the same equivalence class.

@[inline]

partial def Mathlib.Tactic.CC.CCM.getHEqProof (e₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.CCM (Option Lean.Expr)

Build a proof for HEq e₁ e₂. The result is none if e₁ and e₂ are not in the same equivalence class.

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

Build a proof for e = True. Fails if e is not known to be true.

Equations

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

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

Build a proof for e = False. Fails if e is not known to be false.

Equations

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

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

Build a proof for a = b. Fails if a and b are not known to be equal.

Equations

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

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

Build a proof of False if the context is inconsistent. Returns none if False is not known to be true.

Equations

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

def Mathlib.Tactic.CC.CCM.compareSymmAux (lhs₁ : Lean.Expr) (rhs₁ : Lean.Expr) (lhs₂ : Lean.Expr) (rhs₂ : Lean.Expr) : Mathlib.Tactic.CC.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₁ : Lean.Expr × Lean.Name) (k₂ : Lean.Expr × Lean.Name) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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 : Lean.Expr) (b : Lean.Expr) : Mathlib.Tactic.CC.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 : Lean.Expr) (newRoot : Lean.Expr) : Mathlib.Tactic.CC.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 : optParam (Array Lean.Expr) #[]) : Mathlib.Tactic.CC.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 : Array Lean.Expr) (lambdas : Array Lean.Expr) (newLambdaApps : optParam (Array Lean.Expr) #[]) : Mathlib.Tactic.CC.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.mkNeOfEqOfNe (a : Lean.Expr) (a₁ : Lean.Expr) (a₁NeB : Lean.Expr) : Mathlib.Tactic.CC.CCM (Option Lean.Expr)

Given a, a₁ and a₁NeB : a₁ ≠ b, return a proof of a ≠ b if a and a₁ are in the same equivalence class.

Equations

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

def Mathlib.Tactic.CC.CCM.mkNeOfNeOfEq (aNeB₁ : Lean.Expr) (b₁ : Lean.Expr) (b : Lean.Expr) : Mathlib.Tactic.CC.CCM (Option Lean.Expr)

Given aNeB₁ : a ≠ b₁, b₁ and b, return a proof of a ≠ b if b and b₁ are in the same equivalence class.

Equations

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

def Mathlib.Tactic.CC.CCM.isAC (e : Lean.Expr) : Mathlib.Tactic.CC.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.

def Mathlib.Tactic.CC.CCM.dbgTraceACEq (header : String) (lhs : Mathlib.Tactic.CC.ACApps) (rhs : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.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.mkACProof (e₁ : Lean.Expr) (e₂ : Lean.Expr) : Lean.MetaM Lean.Expr

Return the proof of e₁ = e₂ using ac_rfl tactic.

Equations

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

def Mathlib.Tactic.CC.CCM.mkACSimpProof (tr : Mathlib.Tactic.CC.ACApps) (t : Mathlib.Tactic.CC.ACApps) (s : Mathlib.Tactic.CC.ACApps) (r : Mathlib.Tactic.CC.ACApps) (sr : Mathlib.Tactic.CC.ACApps) (tEqs : Mathlib.Tactic.CC.DelayedExpr) : Lean.MetaM Mathlib.Tactic.CC.DelayedExpr

Given tr := t*r sr := s*r tEqs : t = s, return a proof for tr = sr

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.

def Mathlib.Tactic.CC.CCM.mkACSuperposeProof (ra : Mathlib.Tactic.CC.ACApps) (sb : Mathlib.Tactic.CC.ACApps) (a : Mathlib.Tactic.CC.ACApps) (b : Mathlib.Tactic.CC.ACApps) (r : Mathlib.Tactic.CC.ACApps) (s : Mathlib.Tactic.CC.ACApps) (ts : Mathlib.Tactic.CC.ACApps) (tr : Mathlib.Tactic.CC.ACApps) (tsEqa : Mathlib.Tactic.CC.DelayedExpr) (trEqb : Mathlib.Tactic.CC.DelayedExpr) : Lean.MetaM Mathlib.Tactic.CC.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.

def Mathlib.Tactic.CC.CCM.simplifyACCore (e : Mathlib.Tactic.CC.ACApps) (lhs : Mathlib.Tactic.CC.ACApps) (rhs : Mathlib.Tactic.CC.ACApps) (H : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.CCM (Mathlib.Tactic.CC.ACApps × Mathlib.Tactic.CC.DelayedExpr)

Given e := lhs * r and H : lhs = rhs, return rhs * r and the proof of e = rhs * r.

Equations

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

def Mathlib.Tactic.CC.CCM.simplifyACStep (e : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.CCM (Option (Mathlib.Tactic.CC.ACApps × Mathlib.Tactic.CC.DelayedExpr))

The single step of simplifyAC.

Simplifies an expression e by either simplifying one argument to the AC operator, or the whole expression.

Equations

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

def Mathlib.Tactic.CC.CCM.simplifyAC (e : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.CCM (Option (Mathlib.Tactic.CC.ACApps × Mathlib.Tactic.CC.DelayedExpr))

If e can be simplified by the AC module, return the simplified term and the proof term of the equality.

Equations

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

def Mathlib.Tactic.CC.CCM.insertEraseROcc (arg : Lean.Expr) (lhs : Mathlib.Tactic.CC.ACApps) (inLHS : Bool) (isInsert : Bool) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (lhs : Mathlib.Tactic.CC.ACApps) (inLHS : Bool) (isInsert : Bool) : Mathlib.Tactic.CC.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.

@[inline]

def Mathlib.Tactic.CC.CCM.insertROccs (e : Mathlib.Tactic.CC.ACApps) (lhs : Mathlib.Tactic.CC.ACApps) (inLHS : Bool) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (lhs : Mathlib.Tactic.CC.ACApps) (inLHS : Bool) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (rhs : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (rhs : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (lhs : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (lhs : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (rhs : Mathlib.Tactic.CC.ACApps) (H : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.ACApps) (rhs : Mathlib.Tactic.CC.ACApps) (H : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.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.superposeAC (ts : Mathlib.Tactic.CC.ACApps) (a : Mathlib.Tactic.CC.ACApps) (tsEqa : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.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.

def Mathlib.Tactic.CC.CCM.processAC : Mathlib.Tactic.CC.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₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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.

partial def Mathlib.Tactic.CC.CCM.convertAC (op : Lean.Expr) (e : Lean.Expr) (args : optParam (Array Lean.Expr) #[]) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.CCM Unit

The specialized internalizeCore for applications or literals.

partial def Mathlib.Tactic.CC.CCM.internalizeCore (e : Lean.Expr) (parent? : Option Lean.Expr) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.CCM Unit

Propagate equality from a and b to a → b.

def Mathlib.Tactic.CC.CCM.propagateIteUp (e : Lean.Expr) : Mathlib.Tactic.CC.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.

def Mathlib.Tactic.CC.CCM.propagateEqUp (e : Lean.Expr) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.CCM Unit

Propagate equality from subexpressions of e to e.

partial def Mathlib.Tactic.CC.CCM.applySimpleEqvs (e : Lean.Expr) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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 : optParam (Array Lean.Expr) #[]) : Mathlib.Tactic.CC.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 : optParam Bool false) (newTarget : optParam (Option Lean.Expr) none) (newProof : optParam (Option Mathlib.Tactic.CC.EntryExpr) none) : Mathlib.Tactic.CC.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 : optParam (Array Lean.Expr) #[]) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.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 : Array Lean.Expr) (lambdas : Array Lean.Expr) (newLambdaApps : optParam (Array Lean.Expr) #[]) : Mathlib.Tactic.CC.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 : Lean.Expr) (c : Lean.Expr) : Mathlib.Tactic.CC.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₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.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 : Lean.Expr) (val : Lean.Expr) : Mathlib.Tactic.CC.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₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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₁ : Lean.Expr) (e₂ : Lean.Expr) (H : Mathlib.Tactic.CC.EntryExpr) (heqProof : Bool) : Mathlib.Tactic.CC.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₁ : Lean.Expr) (e₂ : Lean.Expr) (n₁ : Mathlib.Tactic.CC.Entry) (n₂ : Mathlib.Tactic.CC.Entry) (r₁ : Mathlib.Tactic.CC.Entry) (r₂ : Mathlib.Tactic.CC.Entry) (flipped : Bool) (H : Mathlib.Tactic.CC.EntryExpr) (heqProof : Bool) : Mathlib.Tactic.CC.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 : Mathlib.Tactic.CC.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) : Mathlib.Tactic.CC.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 : Lean.Expr) (rhs : Lean.Expr) (H : Lean.Expr) (heqProof : Bool) : Mathlib.Tactic.CC.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 : Lean.Expr) (proof : Lean.Expr) : Mathlib.Tactic.CC.CCM Unit

Add proof : type to the congruence closure.

Equations

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