Make proofs from 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 : CCM α) (c : CCStructure) : Lean.MetaM (α × CCStructure)

Run a computation in the CCM monad.

Equations

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

@[inline]

def Mathlib.Tactic.CC.CCM.modifyCache (f : CCCongrTheoremCache → CCCongrTheoremCache) : 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.getCache : CCM 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) : CCM (Option Entry)

Look up an entry associated with the given expression.

Equations

• Mathlib.Tactic.CC.CCM.getEntry e = do let __do_lift ← get pure __do_lift.entries[e]?

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

partial def Mathlib.Tactic.CC.CCM.isCongruent (e₁ e₂ : Lean.Expr) : 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.mkCCHCongrTheorem (fn : Lean.Expr) (nargs : ℕ) : CCM (Option 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) : CCM (Option CCCongrTheorem)

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

Equations

• Mathlib.Tactic.CC.CCM.mkCCCongrTheorem e = Mathlib.Tactic.CC.CCM.mkCCHCongrTheorem e.getAppFn e.getAppNumArgs

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

Update the modification time of the congruence class of e.

def Mathlib.Tactic.CC.CCM.hasHEqProofs (root : Lean.Expr) : 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 heqProofs : Bool) : 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 : DelayedExpr) (flipped heqProofs : Bool) : CCM 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 : EntryExpr) (flipped heqProofs : Bool) : CCM 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.
• Mathlib.Tactic.CC.CCM.flipProof (↑H_2) flipped heqProofs = Mathlib.Tactic.CC.EntryExpr.ofExpr <$> Mathlib.Tactic.CC.CCM.flipProofCore H_2 flipped heqProofs
• Mathlib.Tactic.CC.CCM.flipProof H flipped heqProofs = pure H

def Mathlib.Tactic.CC.CCM.isEqv (e₁ e₂ : Lean.Expr) : 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₁ e₂ : Lean.Expr) : 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) : 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) : 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₁ 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 (some H₁) H₂ heqProofs = Mathlib.Tactic.CC.CCM.mkTrans H₁ H₂ heqProofs
• Mathlib.Tactic.CC.CCM.mkTransOpt none H₂ heqProofs = pure H₂

partial def Mathlib.Tactic.CC.CCM.mkCongrProofCore (lhs rhs : Lean.Expr) (heqProofs : Bool) : 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₁ e₂ : Lean.Expr) (heqProofs : Bool) : 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₁ e₂ : Lean.Expr) (heqProofs : Bool) : 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 : DelayedExpr) : CCM Lean.Expr

Turn a delayed proof into an actual proof term.

partial def Mathlib.Tactic.CC.CCM.mkProof (lhs rhs : Lean.Expr) (H : EntryExpr) (heqProofs : Bool) : 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₁ e₂ : Lean.Expr) (asHEq : Bool) : 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₁ e₂ : Lean.Expr) : 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₁ e₂ : Lean.Expr) : 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) : 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) : 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 b : Lean.Expr) : 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 : 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.mkNeOfEqOfNe (a a₁ a₁NeB : Lean.Expr) : 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₁ b₁ b : Lean.Expr) : 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.mkACProof (e₁ 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 t s r sr : ACApps) (tEqs : DelayedExpr) : Lean.MetaM 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.simplifyACCore (e lhs rhs : ACApps) (H : DelayedExpr) : CCM (ACApps × 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.
• Mathlib.Tactic.CC.CCM.simplifyACCore e lhs rhs H = do guard (lhs.isSubset e = true) if (e == lhs) = true then pure (rhs, H) else failure

def Mathlib.Tactic.CC.CCM.simplifyACStep (e : ACApps) : CCM (Option (ACApps × 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 : ACApps) : CCM (Option (ACApps × 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.