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.