Skip to Main content Skip to Navigation
Journal articles

Equations reloaded

Matthieu Sozeau 1, 2 Cyprien Mangin 1, 2
1 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, UPD7 - Université Paris Diderot - Paris 7
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 :
Journal articles
Complete list of metadata

Cited literature [44 references]  Display  Hide  Download
Contributor : Matthieu Sozeau Connect in order to contact the contributor
Submitted on : Monday, December 9, 2019 - 1:45:44 PM
Last modification on : Friday, January 21, 2022 - 3:19:49 AM


Files produced by the author(s)



Matthieu Sozeau, Cyprien Mangin. Equations reloaded. Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (ICFP), pp.1-29. ⟨10.1145/3341690⟩. ⟨hal-01671777v3⟩



Les métriques sont temporairement indisponibles