A New Elimination Rule for the Calculus of Inductive Constructions - Archive ouverte HAL Access content directly
Conference Papers Year : 2009

A New Elimination Rule for the Calculus of Inductive Constructions

(1, 2) , (3) , (4) , (2) , (4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
types-BarCorGreHerSac08-dep-matching.pdf (235.88 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00524938 , version 1 (29-10-2010)

Identifiers

Cite

Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis 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⟩
499 View
190 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More