Documentation

Mathlib.Tactic.CC.MkProof

Make proofs from a congruence closure #

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.CCM (α : Type) :
Type

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

Equations
source
@[inline]
def Mathlib.Tactic.CC.CCM.run {α : Type} (x : CCM α) (c : CCStructure) :
Lean.MetaM (α × CCStructure)

Run a computation in the CCM monad.

Equations
source
@[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.
source
@[inline]
def Mathlib.Tactic.CC.CCM.getCache :
CCM CCCongrTheoremCache

Read the cache field of the state.

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

Look up an entry associated with the given expression.

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

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

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

Is e the root of its congruence class?

Equations
source
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.

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

Update the modification time of the congruence class of e.

source
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.
source
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.
source
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.
source
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
source
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.
source
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.
source
@[inline]
def Mathlib.Tactic.CC.CCM.isEqTrue (e : Lean.Expr) :
CCM Bool

Is the proposition e known to be true?

Equations
source
@[inline]
def Mathlib.Tactic.CC.CCM.isEqFalse (e : Lean.Expr) :
CCM Bool

Is the proposition e known to be false?

Equations
source
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
source
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
source
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.

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

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

Turn a delayed proof into an actual proof term.

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

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

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

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