[Club2] Mi. 2.08; 15.00 (Turing)

[Norbert Schirmer]

Nächste Woche:

Mittwoch, 2.08; 15.00 (Turing 00.09.055)

Sean McLaughlin: Introduction to Gonthier's proof methods

Abstract

 In 2005, Georges Gonthier completed perhaps the most ambitious
mathematics formalization project to date, a Coq proof of the
Four Color Theorem.  Despite the enormity of the effort,
the proof scripts are surprisingly compact: 35,000 lines
(1.5 MB) of definitions and proof scripts.
These statistics include a complete development
of the real numbers using Dedekind cuts, a proof that all
real models are isomorphic, as well as a combinatorial analog of
the Jordan Curve Theorem.
   To achieve such succinct formalization, Gonthier made at least two
novel contributions.  First, he developed a tactic language which he
found more efficient to use than the given Coq tactics.  The commands
of the language resemble the UNIX shell, where a few orthogonal
commands and options give a wide variety of tactic composition without
much typing.  Secondly, he used computational reflection extensively
and developed a way to use it at different levels of
granularity, particularly on a small scale.
   This talk will be an introduction to Gonthier's proof
methods.  I will begin by describing the proof
shell, and will give some illustrative examples where I feel it is
especially effective.  I will continue by presenting some of the many
ways reflection is used in the Gonthier method, in particular his
novel "small scale reflection".
   The talk will assume a familiarity with interactive proving and
higher order logic.  No explicit knowledge of Coq is necessary, though
an understanding of dependent types will be helpful in understanding
the examples.


   Norbert