Library Intro


What is this course about?

  • The precise art of formal reasoning.

  • Use a proof assistant (COQ) to formalize proofs.

  • Propositional logic as the scaffolding of reasoning

  • Foundational issues: classical vs intuitionistic logic

  • Express yourself precisely using the language of predicate logic
  • Finite sets and operations on sets, reasoning by cases.

  • Reasoning about natural numbers, proof by induction
  • Equational reasoning (Algebra).

  • Reasoning about programs and data structures.

What is Coq ?

  • COQ: a Proof Assistant based on the Calculus of Inductive Constructions}

  • Developed in France since 1989.

  • Growing user community.

  • Big proof developments:
    • Correctness of a C-compiler
    • 4 colour theorem

Why using a proof assistant?

  • Avoid holes in paper proofs.

  • Aid understanding. What is a proof?

  • Formal certification of software and hardware.

Using COQ

  • Download COQ from

  • Runs under MacOS, Windows, Linux

  • coqtop : command line interface

  • coqide : graphical user interface

  • proof general : emacs interface

  • coqtop and coqide installed on the lab machines

For reference

  • Coq Reference manual:

  • Coq Library doc:

  • Coq'Art, the book by Yves Bertot and Pierre Casteran (2004). (available in the library!)

Course organisation

  • Course page:

  • Coq Labs: every Tuesday (1600 - 1800) in A32, starting next week (11/10).

  • Weekly coursework, 1st available next Monday.

  • Use online submission system (cw).

  • Tutorials: start next week. See assignment on webpage.

  • Online class test on coq in December.

  • Online Forum: Information about coursework, discuss questions Please subscribe!