The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Hi Daniel,

Several of these topics are also covered in the Software Foundations textbook 
(http://www.cis.upenn.edu/~bcpierce/sf).  

Would it make sense, for your intended audience, to take some initial prefix 
of SF as background and build the remainder of the tutorial as a "companion 
volume" that could be distributed together with SF?  We have already done 
this with some smaller companion contributions such as Arthur Chargueraud's 
two chapters on Coq automation and Andrew Tolmach's chapter on normalization. 
 In the long run, I would love to see SF turn into a collection of loosely 
integrated electronic textbooks on a range of topics (PL metatheory, 
formalized mathematics, verified compilation, verified algorithms, …).  

Besides saving you some (hopefully substantial) work on explaining basic 
aspects of Coq, we can offer you some reasonably polished conventions and 
tools for organizing and (HTML-) typesetting your material, exercises with 
hidden solutions, terse variants for use in lectures, etc.  And everyone 
benefits from the synergy of one combined effort instead of two smaller ones.

If this might be of interest, let me know and we can discuss further.

      - Benjamin




On Sep 24, 2011, at 12:20 AM, Daniel Schepler wrote:

> 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