Module cc 

Congruence Closure Tactic

Proves equalities over uninterpreted functions using Union-Find with congruence propagation. This implements a simplified Downey-Sethi-Tarjan algorithm.

Algorithm

The congruence closure tactic works in four steps:

1. Build E-graph: Add all subterms from goal and hypotheses
2. Merge hypotheses: For each hypothesis x = y, merge x and y
3. Propagate: When x = y and f(x), f(y) exist, merge f(x) and f(y)
4. Check: Goal a = b holds iff a and b are in the same equivalence class

Supported Goals

• Direct equalities: Eq a a (reflexivity)
• Implications: (Eq x y) -> (Eq (f x) (f y)) (congruence)
• Nested implications with multiple hypotheses

E-Graph Structure

The E-graph maintains:

• A Union-Find for equivalence classes
• Hash-consing for structural sharing
• Use lists for efficient congruence propagation

Structs

EGraph

E-graph with congruence closure.

UnionFind

Union-Find data structure with path compression and union by rank.

Enums

ENode

Node in the E-graph representing a term.

Functions

check_goal

Check if a goal is provable by congruence closure.

decompose_goal

Decompose a goal into hypotheses and conclusion.

reify

Reify a Syntax term into an E-graph node.