# Table of Contents

1.  [How to find me and support material](#org1c28eb4)
2.  [On your machine, install](#orgd1630f9)
3.  [Objectives](#orgbd47a2f)
    1.  [What do you prefer:](#org6da9c05)
        1.  [If you are in the first category,](#org2f78578)
        2.  [If you are in the second category,](#org6f62399)
        3.  [With Coq, doing maths becomes an IA](#orgc8cfe04)
4.  [An ubiquitous concept coming from computer science: TREES](#org713b2a5)
5.  [Coq: a proof assistant based on Type Theory](#orgc9c4ee8)
    1.  [Proof](#org7712208)
    2.  [Assistant](#org188d058)
    3.  [Type Theory](#org8740bb5)

Certified programs and proofs in Coq, OCaml and dependent Type Theory
Jean-François Monin, Verimag, Univ Grenoble Alpes
jean-francois.monin@univ-grenoble-alpes.fr

**Credits.**
These lectures are mainly based on a course (named LTPF) given in France for
about 6 years, and additional material related to my own research.
The main part benefited from inputs of the LTPF teaching team.
Special thanks to Pierre Corbineau for his contributions.


<a id="org1c28eb4"></a>

# How to find me and support material

    search engine -> monin verimag
    https://www-verimag.imag.fr/~monin/
       -> Teaching material for students -> ECNU-2024
       https://www-verimag.imag.fr/~monin/Enseignement/ECNU-2024


<a id="orgd1630f9"></a>

# On your machine, install

-   Coq
-   OCaml
-   for editing: coqide or emacs+proof-general

For them opam (pck manager for OCaml) is a good choice.

Possible alternative: vscode.

I use emacs+proof-general (independent from opam).

A basic installation will be enough (otherwise it may take time)


<a id="orgbd47a2f"></a>

# Objectives


<a id="org6da9c05"></a>

## What do you prefer:

-   create an exciting program?
-   or read/write a boring scientific paper?


<a id="org2f78578"></a>

### If you are in the first category,

Coq is for you.


<a id="org6f62399"></a>

### If you are in the second category,

Coq is for you as well:
Supporting paper-and-pencil elliptic "proofs" by a
machine-checked formal developement became a standard in
prominent conferences such as POPL.


<a id="orgc8cfe04"></a>

### With Coq, doing maths becomes an IA

1.  IA =

    Interesting Activity
    YOU become more intelligent,
    because you are doomed to UNDERSTAND what you are doing,
    
    -   Don't rush on the next exercises.
        Understand what you are doing, read the feedback of Coq.
    -   In this course I'll refrain to use dark magics.
        Everything will be explained in terms of elementary steps
        that are expected to be easy to follow.

2.  Disclaimer

    Using Coq is an addictive game


<a id="org713b2a5"></a>

# An ubiquitous concept coming from computer science: TREES

-   data structures
    e.g. binary trees, lists, Peano natural numbers
-   AST (Abstract Syntax Trees)
-   Proofs seen as proof trees
-   Operational semantics


<a id="orgc9c4ee8"></a>

# Coq: a proof assistant based on Type Theory


<a id="org7712208"></a>

## Proof

It is about mathematical reasoning.
Makes sense in (usual) Maths and in Computer Science,
which can be seen as a special branch of maths.

We will focus on Computer Science, in particular we will rely
on intuitions and knowledge famiiar to programmers:
no background on analysis, geometry or even Set Theory
is needed.
But we expect some familiarity with
&#x2013; data structures, especially recursive data structures
   such as trees and lists
&#x2013; programming, especially recursive programs
   (our programs we be called functions)
&#x2013; basic notions on typing, however this topic will be
   developed a lot.


<a id="org188d058"></a>

## Assistant

Coq is a software interactive tool helping the user to
develop definitions and theorems in an **interactive** way.
Ideally: <span class="underline">clever</span> inputs are entered by the human user, whereas
<span class="underline">tedious</span> details are machine-checked.
In practice: to be discussed; anyway the proof-checking performed
in tools like Coq is actually <span class="underline">very secure</span> by design. Kernel based.


<a id="org8740bb5"></a>

## Type Theory

An extension of a well-known good practice in programming.
The usual tension between benefits and constraints disappears
thanks to the power of polymorphism and dependent types.
PASCAL ADA.