Andrew Tolmach

Essential Coq from Scratch

Coq is a mechanized proof assistant that is widely used for reasoning
about programs, programming languages, and programming tools.
While it enjoys a very simple foundational core based on type theory,
the full Coq system is rich and complex, and can be daunting for beginners.
These lectures will give a pragmatic introduction to the essential features of Coq,
based on the early chapters of the online textbook "Software Foundations in Coq" by
B. Pierce et al., available at  http://www.cis.upenn.edu/~bcpierce/sf/.  (Be
sure to download a recent copy, as the text is frequently updated.)
They will be complemented with plenty of hands-on exercises.

Lecture topics will include:

- Proving properties of functional programs on numbers and lists.
- Inductive data, propositions, and proofs.
- Definition of logical connectives and quantifiers.

To take advantage of these lectures, it is definitely necessary to spend some
time working with Coq yourself, so plan to spend some of your evenings doing
this!   You should arrive with Coq version 8.2 installed on your laptop; it can be
obtained from http://coq.inria.fr/download.   You will also need an interactive
development environment for Coq, either the CoqIde tool that comes with the
system, or, if you are an emacs user, the Proof General tool (http://proofgeneral.inf.ed.ac.uk/).


Recommended exercises from the first five chapters of Software Foundations:


Basics.v
------------

ESSENTIALS:
  all 1 star exercises       
  andb_true_elim2
  beq_nat_refl
  more_exercises (ble_nat,refl, zero_nbeq_S, etc. )
  decreasing

STRONGLY RECOMMENDED:
  mult_comm
  binary

Lists.v
---------

ESSENTIALS:
  all 1 star exercises       
  list_exercises
  list_design
  beq_natlist
  apply_exercises

STRONGLY RECOMMENDED:
  alternate
  bag_functions
  bag_theorem
  bag_count_sum


Poly.v
--------

ESSENTIALS:
  all 1 star exercises
  map_rev
  override_neq      
  beq_nat_eq'
  plus_n_n_injective
  override_same
  beq_nat_trans

STRONGLY RECOMMENDED:
  combine_split (and a suitable inverse)
  override_permute


Ind.v
-------

ESSENTIALS:
   All 1 star exercises
   Give tactic proof AND proof object that if n is even, then so is 4+n.
   double_even
   ev_sum
   MyProp_0
   MyProp_plustwo
   ev_MyProp

STRONGLY RECOMMENDED:
   ev_ev_even
   gen_dep_practice
   palindrome


Logic.v
----------

ESSENTIALS:
   All 1 star exercises
   even_ev
   definition of True as an inductive Prop
   not_eq_beq_false
   dist_exists_or
   R_provability
   le_exercises (at least some of them)

STRONGLY RECOMMENDED:
   MyProp_iff_ev
   R_fact
   no_repeats



Comments