|
|
| The picture "Le coq mécanisé" is courtesy of Lilia Anisimova |
These lecture notes are the result of the author's personal experience
of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in
large-scale research projects. The present manuscript offers a brief
and practically-oriented introduction to the basic concepts of
mechanized reasoning and interactive theorem proving.
The primary audience of the manuscript are the readers with expertise
in software development and programming and knowledge of discrete
mathematic disciplines on the level of an undergraduate university
program. The high-level goal of the course is, therefore, to
demonstrate how much the rigorous mathematical reasoning and
development of robust and intellectually manageable programs have in
common, and how understanding of common programming language concepts
provides a solid background for building mathematical abstractions and
proving theorems formally. The low-level goal of this course is to
provide an overview of the Coq proof assistant, taken in its both
incarnations: as an expressive functional programming language with
dependent types and as a proof assistant providing support for
mechanized interactive theorem proving.
By aiming these two goals, this manuscript is, thus, intended to
provide a demonstration how the concepts familiar from the mainstream
programming languages and serving as parts of good programming
practices can provide illuminating insights about the nature of
reasoning in Coq's logical foundations and make it possible to reduce
the burden of mechanical theorem proving. These insights will
eventually give the reader a freedom to focus solely on the
essential part of the formal development instead of fighting
with the proof assistant in futile attempts to encode the "obvious"
mathematical intuition.
@misc{Sergey:PnP,
author = {Ilya Sergey},
title = {{Programs and Proofs: Mechanizing Mathematics with Dependent Types}},
month = {August},
year = {2014},
note = {Lecture notes with exercises},
doi = {10.5281/zenodo.4996238}
}