An extensible equality checking algorithm for dependent type theories

MaRDI QIDQ5028472zbMATH OpenFDO

Authors Andrej Bauer, Anja Petković Komel

Publication date 9 February 2022

Full work available at URL https://arxiv.org/abs/2103.07397, https://lmcs.episciences.org/8980

zbMATH Keywords

equality checkingproof assistanttype theory

Mathematics Subject Classification ID

Type theory (03B38) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We also give sufficient syntactic criteria for recognizing such rules, as well as a simple pattern-matching algorithm for applying them. A third component of the algorithm is a suitable notion of principal arguments, which determines a notion of normal form. By varying these, we obtain known notions, such as weak head-normal and strong normal forms. We prove that our algorithm is sound. We implemented it in the Andromeda 2 proof assistant, which supports user-definable type theories. The user need only provide the equality rules they wish to use, which the algorithm automatically classifies as computation or extensionality rules, and select appropriate principal arguments.

Recommendations

• Equality checking for general type theories in Andromeda 2
• Coq without type casts: a complete proof of Coq Modulo Theory
• Type checking dependent (record) types and subtyping
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• Foundations of Software Science and Computational Structures

Cites work

• A Modular Type Reconstruction Algorithm
• Equality checking for general type theories in Andromeda 2
• Extensional equivalence and singleton types
• scientific article; zbMATH DE number 512787 (Why is no real title available?)
• Interacting with Modal Logics in the Coq Proof Assistant
• On irrelevance and algorithmic equality in predicative type theory
• The Lean theorem prover (system description)
• The locally nameless representation

Cited in

(9)

• Partial type equivalences for verified dependent interoperability
• A modular type-checking algorithm for type theory with singleton types and proof irrelevance
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Equality checking for general type theories in Andromeda 2
• Checking Emptiness of Non-Deterministic Regular Types with Set Operators
• Finitary type theories with and without contexts
• The rewster: type preserving rewrite rules for the Coq proof assistant
• A correspondence between type checking via reduction and type checking via evaluation

Describes a project that uses

Uses Software

• Lean

This page was built for publication: An extensible equality checking algorithm for dependent type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5028472)