A New Elimination Rule for the Calculus of Inductive Constructions

Bruno Barras 1, 2 Pierre Corbineau 3 Benjamin Grégoire 4 Hugo Herbelin 2 Jorge Sacchini 4
2 TYPICAL - Types, Logic and computing
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
4 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In Type Theory, definition by dependently-typed case analysis can be expressed by means of a set of equations — the semantic approach — or by an explicit pattern-matching construction — the syntactic approach. We aim at putting together the best of both approaches by extending the pattern-matching construction found in the Coq proof assistant in order to obtain the expressivity and flexibility of equation-based case analysis while remaining in a syntax-based setting, thus making dependently-typed programming more tractable in the Coq system. We provide a new rule that permits the omission of impossible cases, handles the propagation of inversion constraints, and allows to derive Streicher's K axiom. We show that subject reduction holds, and sketch a proof of relative consistency.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00524938
Contributor : Hugo Herbelin <>
Submitted on : Friday, October 29, 2010 - 11:03:47 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on : Friday, October 26, 2012 - 12:35:58 PM

File

types-BarCorGreHerSac08-dep-ma...
Files produced by the author(s)

Identifiers

Collections

Citation

Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Sacchini. A New Elimination Rule for the Calculus of Inductive Constructions. Types for Proofs and Programs, Mar 2008, Torino, Italy. pp.32-48, ⟨10.1007/978-3-642-02444-3_3⟩. ⟨inria-00524938⟩

Share

Metrics

Record views

826

Files downloads

229