← All papers
Congruence Closure in Intensional Type Theory
cs.LO
Jan 16, 2017 · v2
TL;DR
Implements a congruence closure procedure used in Lean's automation for intensional type theory.
Abstract
Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence closure algorithms can support the expressive logics based on intensional type theory (ITT) that underpin many interactive theorem provers. The authors present an efficient and proof-producing congruence closure procedure that applies to every function in ITT regardless of dependencies among the arguments, relying only on the uniqueness of identity proofs axiom.
Problem
Congruence closure procedures are core components of SMT solvers and automated reasoning, but no known algorithms supported the expressive logics of intensional type theory (ITT) with dependent function types, where arguments may have dependencies.
Approach
The authors present a congruence closure procedure that applies to every function in intensional type theory regardless of dependencies among arguments. The procedure is both efficient and proof-producing, relying only on the uniqueness of identity proofs (UIP) axiom.
Results
The procedure handles all functions in ITT including those with dependent arguments, produces proofs, and is efficient enough for use in interactive theorem provers. It requires only the UIP axiom rather than full extensionality.