### Andrew Tolmach

 Essential Coq from ScratchCoq is a mechanized proof assistant that is widely used for reasoningabout 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 sometime working with Coq yourself, so plan to spend some of your evenings doingthis!   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. )  decreasingSTRONGLY RECOMMENDED:  mult_comm  binaryLists.v---------ESSENTIALS:  all 1 star exercises          list_exercises  list_design   beq_natlist  apply_exercisesSTRONGLY RECOMMENDED:  alternate  bag_functions  bag_theorem  bag_count_sumPoly.v --------ESSENTIALS:  all 1 star exercises  map_rev  override_neq         beq_nat_eq'  plus_n_n_injective  override_same  beq_nat_transSTRONGLY RECOMMENDED:  combine_split (and a suitable inverse)  override_permuteInd.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_MyPropSTRONGLY RECOMMENDED:   ev_ev_even   gen_dep_practice    palindromeLogic.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