M2 ENS Lyon, Approximation Theory and Proof Assistants: Certified Computations

Nicolas Brisebarre et Damien Pous

Nicolas Brisebarre's page for the course

General information

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

Files for the course

Summary of tactics:

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)

References on the mathematical theory underlying Coq

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.

Other related keywords are Martin Löf dependent type theory, the lambda-cube and pure type systems (PTS).

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

Moving from CC to CIC is a bit like adding primitive integers to the language.

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).

The following lecture notes by Herman Geuvers might also be interesting, depending on how far you want to go: it's reasonably short and it leads you to dependent types.

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).

Other tutorials

See also resources available there.

Installing Coq

  1. 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.
  2. 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.
  3. Detailed instructions for debian/ubuntu systems:
    1. remove everything ocaml/opam/coq related from your system:

      sudo apt remove ocaml* coq* opam*
      rm -rf ~/.opam

    2. 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

    3. 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

    4. install required dependencies:

      sudo apt install [whatever was listed above]

    5. install coq, coqide, coq-interval:

      opam install coq coqide coq-interval

You are successful if: Drop me an email if you can't get this to work before the lecture on Monday 14th.