Skip to Main content Skip to Navigation
Conference papers

Definitional Proof-Irrelevance without K

Gaëtan Gilbert 1 Jesper Cockx 2 Sozeau Matthieu 3, 4 Nicolas Tabareau 1 
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
3 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
Abstract : Definitional equality—or conversion—for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms—such as uniqueness of identity proofs (UIP)—that are incompatible with other extensions, such as univalence. In this paper, taking inspiration from homotopy type theory, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) by using techniques coming from recent development on dependent pattern matching without UIP. We show the generality of our approach by providing implementations for both Coq and Agda, both of which are planned to be integrated in future versions of those proof assistants.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Gaëtan Gilbert Connect in order to contact the contributor
Submitted on : Wednesday, August 22, 2018 - 6:09:03 PM
Last modification on : Wednesday, September 28, 2022 - 3:04:05 PM
Long-term archiving on: : Friday, November 23, 2018 - 6:04:30 PM


Files produced by the author(s)


  • HAL Id : hal-01859964, version 1


Gaëtan Gilbert, Jesper Cockx, Sozeau Matthieu, Nicolas Tabareau. Definitional Proof-Irrelevance without K. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019, Jan 2019, Lisbon, Portugal. ⟨hal-01859964v1⟩



Record views


Files downloads