Damien Pous' sessions, on Mondays, 8am, will be given only online, on BBB (classroom M2IF-CR13).

- 14/09/2020 (propositional logic, predicate logic):
file with holes,
answers (html version).
*Bonus:*impredicative encodings. - 21/09/2020 (predicate logic, natural numbers):
file with holes,
answers (html version).
*Bonus:*binary numbers. - 28/09/2020 (real numbers): file with holes, answers (html version).
- 05/10/2020 (Weierstrass' theorem 1/3: binomials)
- 12/10/2020 (Weierstrass' theorem 2/3: polynomials, continuity)
- 14/10/2020 (Weierstrass' theorem 3/3: Bernstein polynomials): file with holes.
- 19/10/2020 (Certified approximations 1/3: intervals, Chebyshev polynomials)
- 22/10/2020 (Certified approximations 2/3: models)
- 2/11/2020 (Certified approximations 3/3: Newton): tarball with holes.

For an exhaustive list, see Coq documentation on tactics (you can look for a specific tactic there).

## Basic tactics | |

intro H. intros HA HAB. intros H [H|H']. | (introduce hypotheses, possibly decomposing them on the fly) |

apply H. apply H, H'. apply (H H'). apply (te A). apply H in H'. | (apply an hypothesis, a theorem, or a term) |

assert(H: T). assert(H: T) by tac. | (prove a lemma inside a proof) |

split. left. right. exists. | (proving a conjunction, a discjunction, an exists) |

destruct H as [H1 H2]. destruct H as [H1|H2]. destruct H as [x Hx]. destruct (te A) as [HA HnA]. |
(decompose an hypothesis or a term) |

contradict H. | (close the goal by contradicting an hypothesis) |

assumption. | (close the goal by using one of the hypotheses) |

reflexivity. | (prove an equality by reflexivity) |

rewrite H, (plus_comm x). rewrite H in H'. rewrite <- H. rewrite H at 2. | (rewrite using an equality) |

induction n as [|m IH]. | (proceeed by induction on n ( = destruct + induction hypothesis)) |

set (x:=e). | (give a name to a term or a pattern) |

simpl. simpl in H. | (simplify the goal or an hypothesis by computation) |

## High-level tactics | |

tauto. | (solve a propositional tautology) |

trivial. | (try simple things such as assumption or reflexivity, leave the goal unchanged if it does not work) |

easy. | (try simple things such as assumption or reflexivity, fails if this does not solve the goal) |

ring. | (solve ring equations (polynomials)) |

ring_simplify. | (expand/simplify polynomials) |

field. | (solve field equations) |

field_simplify. | (expand/simplify field expressions) |

lia. | (linear integer arithmetic - max, plus, minus, le, lt... but not mult) |

lra. | (linear real arithmetic - idem) |

## Tactic combinators | |

tac1; tac2. | (apply tac2 to all subgoals generated by tac1) |

repeat tac. | (repeatedly apply tac) |

now tac. | (apply tac and conclude easily (e.g., with assumption)) |

try tac. | (try to apply tac, not complaining if it fails---à consommer avec modération) |

The mathematical background of Coq is the
*calculus of inductive constructions (CIC)*,
which is an extension of the
*calculus of constructions (CC)*,
which is an extension of the
*simply typed lambda calculus.*

There are three main additions leading from the simply typed lambda calculus to CC:

- type constructors (like
`'a list`

in OCaml/Haskell) - type polymorphism (like the function
`map: ('a -> 'b) -> 'a list -> 'b list`

in OCaml/Haskell, and actually a bit more - dependent types (nothing like that in mainstream programming languages)

If you have no background in lambda calculus, I recommend that you read chapters 3, 7, and 11 of Proofs and Types (and also the beginning of chapter 4, not for the proof of normalisation itself, but for understanding what is normalisation).

- Chapter 3 (and 4) will give you a very quick intro on the simply typed lambda calculus
- Chapter 7 will show you how to extend it with integers
- Chapter 11 will show you type polymorphism (System F, a bit more advanced)

The above two references are not Coq-specific, but they present precisely the actual theory behind Coq. Then there is the Coq'Art book, which is Coq-specific, but more focused on learning Coq than its underlying theory (still, it might be a very good read, especially the first chapters).

- Software foundations (only Volume 1 is relevant for the present course)
- Mike Naha' tutorial
- CPDT (like Volume 2 of Software foundations, more relevant if you want to reason about programs rather than doing analysis)

- Please install Coq 8.12 and the coq-interval library. I recommend you to use opam, as explained here. This should work very well on Unix-based systems (linux/MacOS). If you run another OS, please consider using a virtual machine.
- You will also need an editor with some support for Coq. If you are familiar with emacs, please install Proof General. Otherwise, you can use the dedicated IDE, called CoqIDE.
- Detailed instructions for debian/ubuntu systems:
- remove everything ocaml/opam/coq related from your system:
`sudo apt remove ocaml* coq* opam*`

rm -rf ~/.opam - install ocaml and opam:
`[sudo add-apt-repository ppa:avsm/ppa] # under ubuntu, the goal is to get opam 2`

sudo apt update

sudo apt install ocaml opam - initialise opam and check dependencies:
`opam init # accept that it setups things in your initialisation files`

eval $(opam env)

opam install opam-depext

opam repo add coq-released https://coq.inria.fr/opam/released

opam update

opam-depext coq coq-ide coq-interval

# possibly the last command will propose you do do the next step directly - install required dependencies:
`sudo apt install [whatever was listed above]`

- install coq, coqide, coq-interval:
`opam install coq coqide coq-interval`

- remove everything ocaml/opam/coq related from your system:

- running the command
`coqtop`

in a terminal tells you `Welcome to Coq 8.12'; - you can open the following file
in
`coqide`

or`emacs`

, and then you can repeatedly press the button with a green arrow going down or type`C-c C-b`

and eventually see `Well_done is defined'.