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.
Conference DaySat 25 JanDisplayed time zone: Saskatchewan, Central America change
10:30 - 12:30
|Deriving Instances with Dependent Types|
Arthur Azevedo de AmorimCarnegie Mellon University, USAFile Attached
|The use of Coq for Common Criteria Evaluations|
|Verifying concurrent Go code in Coq with Goose|
Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USALink to publication File Attached
|A Tutorial on Equations|
Matthieu SozeauInriaMedia Attached File Attached