leanprover/tutorial — pull request #15 by avigad (2014-12-21 20:44:49+00:00)
Title: chapter on inductive types

In Chapter 4, I added some information on print commands, notations, overloading, etc. I also wrote a draft of Chapter 5, on inductive definitions.

I think it is coming along nicely. Within the next couple of days, I will write a short introduction and make that "Chapter 1". I will then renumber the later chapters. I will also proofread everything and make a round of revisions.

I told Soonho that it would be good to be more systematic about exercises. He said he will try to work out a nice enviroment, that we can use e.g.

#+BEGIN_EXERCISE

#+END_EXERCISE

I noticed that #+BEGIN_SRC blocks do not always respect the spacing in the file. I think it happens after the "calc" command. For example, in Chapter 5, it happens in the proof after the phrase "almost writes itself", and in the proof before, and two of the proofs afterwards. They are correct in the PDF version.

Should we continue to call this a "tutorial"? It is becoming more like a book. Perhaps it would be better to call it the "introduction", or "tpl" (for "Theorem Proving in Lean"). Eventually, when the work is mature enough, I think we might want to release it the same way as the HoTT book:

http://homotopytypetheory.org/book/

That way people can buy a hardcopy if they want, and we have a more citable resource. That seemed to work quite well for the HoTT people. It seems that Lulu will sell updated versions as they become available.

BTW, here is what I have in mind for upcoming chapters:

More on Induction and Recursion
o Structural recursion (the function definition package)
o Structural induction
o Well-bounded induction and recursion

Structuring Theories and Proofs
o Using blocks in proofs (proof .. qed, visible, etc.)
o Using tactics in proofs
o Namespaces (private, protected, and all the options)
o Sections and Contexts

Type Classes and Algebraic Structures
o ...

The Classical Axioms
o ...

Homotopy Type Theory
o ...

Elaboration and unification
o ...

Also chapters on automation, particular applications, ...