Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq. Matthieu Sozeau and Cyprien Mangin. In: Proc. ACM Program. Lang. 3, ICFP, Article 86 (August 2019), 29 pages. DOI, slides.
This article presents the foundations of version 1.2 of the Equations package.
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 high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. 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 based on an original handling of the no-confusion property of constructors.
The following archive contains
all examples included in the paper, in full, along with a version of the
proof of normalization for Predicative System F and a reflexive tactic
for solving polynomial equations (1.8MB, MD5 hash:
All the examples from the article are also available to play with
running the following virtual machine in Virtual Box, setup with
Ubuntu-64, Coq 8.9.0 and Equations-1.2:
(5.2GB, MD5 hash: