A Tutorial on Equations
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. The general design and implementation of the plug-in presented in [Sozeau and Mangin 2019] 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.
In this tutorial talk, we will present Eqations’ main features from the user point-of-view. This includes Eqations’ grammar for defining programs by dependent pattern-matching and well- founded recursion, highlighting the treatment of Uniqueness of Identity Proofs and the facilities provided for the definition of well- founded or structurally recursive nested or mutually recursive functions. The package also includes supporting tactics for reason- ing a posteriori on Eqations definitions: an elimination principle tailored to the function definition and a set of rewrite rules cor- responding to its clauses; both allow the development of concise and robust proof scripts involving the definitions. Finally, the de- pendent pattern-matching engine at the core of Eqations is also made available in proof mode through a general purpose depen- dent pattern-matching tactic that is more expressive than current destruction tactics and intro-patterns (destruct, inversion or Ssreflect’s elim and vanilla Coq or Ssreflect intro-patterns). The material presented here is part of lecture notes to be integrated in an upcoming volume of Software Foundations centered on the use of advanced tools in Coq.
|Equations Tutorial Source (An_Equations_Tutorial-CoqPL20.v)||27KiB|
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
10:30 - 12:30
Contributed TalksCoqPL at Maurepas
Chair(s): Amin Timany imec-Distrinet KU-Leuven
|Deriving Instances with Dependent Types|
Arthur Azevedo de Amorim Carnegie Mellon University, USAFile Attached
|The use of Coq for Common Criteria Evaluations|
Yves Bertot INRIA, Maxime Dénès Inria, Vincent Laporte Inria, Arnaud Fontaine ANSSI, Thomas Letan ANSSIFile Attached
|Verifying concurrent Go code in Coq with Goose|
Tej Chajed Massachusetts Institute of Technology, USA, Joseph Tassarotti Boston College, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USALink to publication File Attached
|A Tutorial on Equations|
Matthieu Sozeau InriaMedia Attached File Attached