These are slides for a course given at the school Interaction of Proof Assistants and Mathematis in Regensburg, Germany, in September 2023.
Slides and examples
In this tutorial, we want to address an audience of mathematician, assuming that most of them have not had any contact with interactive theorem provers yet. However, we want them to understand what can be done with inductive types, recursion, real numbers, canonical structures, and mathematical component's big operators and matrices.
- Introduction to Coq, Part 1: introduction to the calculus of constructions and inductive types slides, Example file
- Introduction to Coq, Part 2: Automation for a variety of problems slides, Example file
- Three themes for proofs in Coq:
General recursion, adding structure to types,
and algebraic reasoning with mathematical components
slides,
examples for general recursion, examples with canonical structures, example of linear algebra reasoning with mathematical components.