Congruence closure

The congruence closure tactic cc tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b). It is a finishing tactic, i.e. it is meant to close the current goal, not to make some inconclusive progress. A mostly trivial example would be:

example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by
  cc

As an example requiring some thinking to do by hand, consider:

example (f : ℕ → ℕ) (x : ℕ)
    (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
    f x = x := by
  cc

The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas.

The cc implementation in Lean does a few more tricks: for example it derives a = b from Nat.succ a = Nat.succ b, and Nat.succ a != Nat.zero for any a.

• The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)

• The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).

def Mathlib.Tactic.CC.CCState.mkCore (config : Mathlib.Tactic.CC.CCConfig) : Mathlib.Tactic.CC.CCState

Make an new CCState from the given config.

Equations

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

def Mathlib.Tactic.CC.CCState.mkUsingHsCore (config : Mathlib.Tactic.CC.CCConfig) : Lean.MetaM Mathlib.Tactic.CC.CCState

Create a congruence closure state object from the given config using the hypotheses in the current goal.

Equations

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

def Mathlib.Tactic.CC.CCState.rootsCore (ccs : Mathlib.Tactic.CC.CCState) (nonsingleton : Bool) : List Lean.Expr

Returns the root expression for each equivalence class in the graph. If the Bool argument is set to true then it only returns roots of non-singleton classes.

Equations

• ccs.rootsCore nonsingleton = (ccs.getRoots #[] nonsingleton).toList

def Mathlib.Tactic.CC.CCState.incGMT (ccs : Mathlib.Tactic.CC.CCState) : Mathlib.Tactic.CC.CCState

Increment the Global Modification time.

Equations

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

def Mathlib.Tactic.CC.CCState.internalize (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.MetaM Mathlib.Tactic.CC.CCState

Add the given expression to the graph.

Equations

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

def Mathlib.Tactic.CC.CCState.add (ccs : Mathlib.Tactic.CC.CCState) (H : Lean.Expr) : Lean.MetaM Mathlib.Tactic.CC.CCState

Add the given proof term as a new rule. The proof term H must be an Eq _ _, HEq _ _, Iff _ _, or a negation of these.

Equations

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

def Mathlib.Tactic.CC.CCState.isEqv (ccs : Mathlib.Tactic.CC.CCState) (e₁ e₂ : Lean.Expr) : Lean.MetaM Bool

Check whether two expressions are in the same equivalence class.

Equations

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

def Mathlib.Tactic.CC.CCState.isNotEqv (ccs : Mathlib.Tactic.CC.CCState) (e₁ e₂ : Lean.Expr) : Lean.MetaM Bool

Check whether two expressions are not in the same equivalence class.

Equations

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

def Mathlib.Tactic.CC.CCState.eqvProof (ccs : Mathlib.Tactic.CC.CCState) (e₁ e₂ : Lean.Expr) : Lean.MetaM Lean.Expr

Returns a proof term that the given terms are equivalent in the given CCState

Equations

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

def Mathlib.Tactic.CC.CCState.proofFor (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.MetaM Lean.Expr

proofFor cc e constructs a proof for e if it is equivalent to true in CCState

Equations

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

def Mathlib.Tactic.CC.CCState.refutationFor (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.MetaM Lean.Expr

refutationFor cc e constructs a proof for Not e if it is equivalent to False in CCState

Equations

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

def Mathlib.Tactic.CC.CCState.proofForFalse (ccs : Mathlib.Tactic.CC.CCState) : Lean.MetaM Lean.Expr

If the given state is inconsistent, return a proof for False. Otherwise fail.

Equations

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

def Mathlib.Tactic.CC.CCState.mkUsingHs : Lean.MetaM Mathlib.Tactic.CC.CCState

Create a congruence closure state object using the hypotheses in the current goal.

Equations

• Mathlib.Tactic.CC.CCState.mkUsingHs = Mathlib.Tactic.CC.CCState.mkUsingHsCore { ignoreInstances := true, ac := true, hoFns := none, em := true, values := false }

def Mathlib.Tactic.CC.CCState.roots (s : Mathlib.Tactic.CC.CCState) : List Lean.Expr

The root expressions for each equivalence class in the graph.

Equations

• s.roots = s.rootsCore true

instance Mathlib.Tactic.CC.CCState.instToMessageData : Lean.ToMessageData Mathlib.Tactic.CC.CCState

Equations

• Mathlib.Tactic.CC.CCState.instToMessageData = { toMessageData := fun (s : Mathlib.Tactic.CC.CCState) => s.ppEqcs }

partial def Mathlib.Tactic.CC.CCState.eqcOfCore (s : Mathlib.Tactic.CC.CCState) (e f : Lean.Expr) (r : List Lean.Expr) : List Lean.Expr

Continue to append following expressions in the equivalence class of e to r until f is found.

def Mathlib.Tactic.CC.CCState.eqcOf (s : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : List Lean.Expr

The equivalence class of e.

Equations

• s.eqcOf e = s.eqcOfCore e e []

def Mathlib.Tactic.CC.CCState.eqcSize (s : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : ℕ

The size of the equivalence class of e.

Equations

• s.eqcSize e = (s.eqcOf e).length

partial def Mathlib.Tactic.CC.CCState.foldEqcCore {α : Sort u_1} (s : Mathlib.Tactic.CC.CCState) (f : α → Lean.Expr → α) (first c : Lean.Expr) (a : α) : α

Fold f over the equivalence class of c, accumulating the result in a. Loops until the element first is encountered.

See foldEqc for folding f over all elements of the equivalence class.

def Mathlib.Tactic.CC.CCState.foldEqc {α : Sort u_1} (s : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) (a : α) (f : α → Lean.Expr → α) : α

Fold the function of f over the equivalence class of e.

Equations

• s.foldEqc e a f = s.foldEqcCore f e e a

def Mathlib.Tactic.CC.CCState.foldEqcM {α : Type} {m : Type → Type} [Monad m] (s : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) (a : α) (f : α → Lean.Expr → m α) : m α

Fold the monadic function of f over the equivalence class of e.

Equations

• s.foldEqcM e a f = s.foldEqc e (pure a) fun (act : m α) (e : Lean.Expr) => do let a ← act f a e

def Lean.MVarId.cc (m : Lean.MVarId) (cfg : Mathlib.Tactic.CC.CCConfig := { ignoreInstances := true, ac := true, hoFns := none, em := true, values := false }) : Lean.MetaM Unit

Applies congruence closure to solve the given metavariable. This procedure tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b).

The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas. The cc implementation in Lean does a few more tricks: for example it derives a = b from Nat.succ a = Nat.succ b, and Nat.succ a != Nat.zero for any a.

• The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)
• The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).

Equations

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

def Mathlib.Tactic.CC.elabCCConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Mathlib.Tactic.CC.CCConfig

Allow elaboration of CCConfig arguments to tactics.

Equations

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

def Mathlib.Tactic.cc : Lean.ParserDescr

The congruence closure tactic cc tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b). It is a finishing tactic, i.e. it is meant to close the current goal, not to make some inconclusive progress. A mostly trivial example would be:

example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by
  cc

As an example requiring some thinking to do by hand, consider:

example (f : ℕ → ℕ) (x : ℕ)
    (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
    f x = x := by
  cc

Equations

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