Equations reloaded

Cyprien Mangin 1, 2 Matthieu Sozeau 1, 2
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful proof principles for demonstrating properties about them. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities that can be reused to define enhanced versions of dependent elimination tactics. We introduce verified optimizations of the simplifier that allow generating smaller and simpler Equations definitions and proof terms for these tactics in general.
Document type :
Preprints, Working Papers, ...
Liste complète des métadonnées

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01671777
Contributor : Matthieu Sozeau <>
Submitted on : Saturday, December 15, 2018 - 5:15:20 PM
Last modification on : Friday, January 4, 2019 - 5:33:38 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01671777, version 2

Collections

Citation

Cyprien Mangin, Matthieu Sozeau. Equations reloaded. 2018. ⟨hal-01671777v2⟩

Share

Metrics

Record views

22

Files downloads

64