Expand description
crush — the grind-style closer: E-match quantified equality lemmas into
the ground e-graph, then discharge the goal by certified congruence closure.
Lean’s grind fuses an e-graph, E-matching of annotated lemmas, and theory
solvers. This is the congruence+instantiation core of that, built entirely
on machinery that already certifies: the ground equality graph and its
transitive/congruence explanations ([crate::engine::cert_congruence_path]),
and the one-sided matcher that fires a ∀-lemma at a ground subterm
(crate::unify::match_term_pattern). Each instantiation is a
InferenceRule::UniversalInstTerm chain from the lemma; the final goal
closes by rewriting a known atom through the congruence-derived equalities.
The whole result is one kernel-checked derivation — unlike grind, whose
core is trusted.
Signature demo (which plain auto cannot do): ∀x. f(x)=g(x), a=b,
P(g(b)) ⊢ P(f(a)).