The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I'm thinking of writing a new tutorial on (plug subject in here).  My 
ambition 
would be to have it be a sort of complement to Adam's CPDT book: where Adam 
covers the programming side of using Coq, I'd focus more on the formal proofs 
side.

A rough preliminary outline of what I'd cover would be:

* Introduction (currently, thinking of using some examples from basic group 
theory).
* Using sections and multiple files.
* Typeclasses, along the lines of MathClasses -- and use these heavily 
throughout the rest of the tutorial.
* Induction.
* Defining inductive types and inductive Props (mostly focusing on inductive 
props, thinking of them as "the subset generated by some generators and 
closure conditions").  Include a discussion on what it means to "use 
induction 
on an inductively defined Prop", since this is something that's likely to be 
unfamiliar to most mathematicians.
* Subsets (both Ensembles library and subset types), and the Program 
Definition 
/ Lemma feature to make working with subset types more readable.
* An overview of the Howard-Curry isomorphism and its use in Coq, with a view 
towards understanding how proof terms work and being able to write some basic 
proof terms.
* A section going over some of the basic logical axioms available in the 
standard library, and some personal philosophical musings on when to use the 
axioms and when to try to avoid them if possible.
* A brief description of the type hierarchy.
* Introduction to proof automation, though almost certainly not going as far 
as Adam goes. :)  Probably leading up to an example I've worked out, of 
proving associativity of addition on binary positive integers, where I'll go 
through the development of an automated proof by extending what it tries 
until 
it can cover all 27 cases.
* Proof by reflection (a.k.a. "it's true because my certified CAS says so").  
This would certainly be a good place for a reference to CPDT, for obvious 
reasons.

One thing that I'd definitely want to cover is some examples where destruct 
or 
rewrite won't work because of dependent types, and how to handle these 
situations.  I can't think of any simple examples off the top of my head, but 
it's definitely something that periodically comes up in my work.  I'm also 
not 
sure where that would fit into the presentation.

Anyway, I'm wondering if there's interest in seeing this come to fruition, or 
maybe some topics you'd like to see covered that I left out or forgot.
-- 
Daniel Schepler