An experiment in writing formal mathematics in Coq:
functions in classical Zermelo-Fraenkel (with choice)
version 1: Friday, April 13th 2001; (ps file for version 1)---note however that there is extra source materiel contained in the tex file.
Here is an experimental program written in c, intended to be a sort of
pre-compiler help tool for Coq:
widget5---a version of Friday, June 8th 2001.
Here is a rewriting of the start of the experimental ZFC file above, adapted for use with widget5: startA.v---a version of Monday, June 11th 2001.
For the faint of heart, here is a much smaller example showing how widget5 can do rewriting. Run widget5 specifying the following file; erase the Remarks in the section at the end, and run the command r (then recopy the resulting output from the OUT.html file back into the .v file): assoc1.v---then try to continue in the same way!
We develop some basic set theory within Coq, using a weak version of the axiom of choice (this version might be compatible with impredicativity of the sort Set but of course it doesnt allow creation of choice functions towards types of sort Set): Choice.v---a version of Monday, June 24th 2002.
Here is a file containing a definition of first cohomology plus a proof of the first part of the long exact sequence, showing that the first cohomology is in a certain sense the obstruction to lifting sections of a surjection: h1.v---a version of Monday, June 24th 2002.
An update h1a.v of Thursday November 6th 2003 makes minor changes so it compiles under Coq 7.4.
Here is the translation into Coq v8.0beta syntax made using coqc -translate, Friday January 9th, 2004
Version of Thursday, October 3rd 2002.
Version of Tuesday, October 22nd 2002.
Version of Thursday, April 17th 2003.
Very preliminary version of Friday, May 16th 2003.
Version of Tuesday, June 17th 2003.
In the second version of Monday, July 7th 2003, we just begin to treat ordered sets.
A gadget in the version of Monday, September 29th 2003: some very short abbreviations for standard tactics.
The version of Monday, October 6th 2003 presents a general format for notation for objects.
The version of Friday, October 17th 2003 consists of two files: groundwork6.v (to be compiled first) and order.v . We get up to a proof of Zorn's lemma.
The version of Wednesday, October 22nd 2003 consists of three files: groundwork7.v , notation8.v , order1.v , and incorporates notation for various different types of objects.
Monday, November 10th 2003: new versions notation9.v and order2.v incorporate an alphabetic string datatype as the basis for notation.
Monday, February 9th 2004: a revised version migrates to Coq v8, improves
organisation of the files, treats more stuff about well-ordered sets, transfinite induction,
ordinals. Also contains a small development on topology showing that the product of two
connected spaces is connected. The
index file points to the various files.
An update ( index file ) of Tuesday, February 17th, 2004.
Version of Tuesday, October 14th 2003
Translated to Coq v8.0beta syntax on Friday January 9th, 2004 (using the coqc -translate option provided with v8.0beta)
The project involves several steps:
(1)---Construction of the free category on a graph and study of functors and natural transformations from there;
(2)---Construction of the quotient category by a relation, and again functors and natural transformation from there;
(3)---Defining the localization by the formula given in Gabriel-Zisman, as a quotient of a free category; and
(4)---Proving the universal property as stated in their Theorem 1.2.
For the first step, here is a preliminary version of the file freecat1.v (Friday, November 5th, 2004). It should compile within the environment defined by the category-theory contribution above.
For the second step, here is a preliminary version of the file qcat1.v (Saturday, November 13th, 2004). Again, it should compile within the environment defined by the category-theory contribution above. Here we construct the quotient category by a relation (assuming the relation is trivial on objects). We also give a criterion for full faithfulness of the pullback or composition functor with a functor, with a view towards applying this to get GZ's Theorem 1.2 in step (4).
Here is a preliminary version for the third and fourth steps: gzdef1.v (Tuesday, November 16th, 2004). We define the Gabriel-Zisman graph and their relation on the associated free category; the localization is constructed as the quotient of the free category by this relation. The main step is to construct the dotted arrow completing the commutative diagram whenever we have a functor which sends elements of the multiplicative system to invertible morphisms.
Continuing on the same subject, we can treat the calculus of fractions. Here (gzfractions1.v, Thursay, January 20th, 2005) is a construction of the localization by left fractions under the assumption that the multiplicative system has a calculus of left fractions; together with a proof of the easiest version of the universal property: just enough to be able to get it isomorphic to the localization constructed above.
In the last file of this series (gzloc1.v, Friday, January 28th, 2005) we complete the above by discussing the general definition of localization by universal property and show that our constructions satisfy this definition. This gives unicity up to a functorial isomorphism. We treat right fractions by equivalence with left fractions in the opposite category, and for both left and right fractions we draw the main conclusion which is that if the localizing system has a calculus of fractions then there is a simple description of the morphisms of the localized category (for example the general one defined in gzdef1.v). This description is not easy to find directly from the fraction condition and the general construction, rather its proof passes through the other specific construction in gzfractions1.v plus the unicity isomorphism of gzloc1.v.
Here are the files for an updated version, Friday March 18th, 2005:
updateA.v, freecat.v, qcat.v, gzdef.v, left_fractions.v, gzloc.v, infinite.v, lfcx.v.
The first file is a collection of various results which logically should go back into previous places within the category theory development (recall that the above files are to be compiled within the category-theory environment available above). The next files are as above (with "gzfractions" renamed to "left_fractions"). The file "infinite.v" is a digression to prove some basic results about infinite cardinals, namely that the product and union operations preserve cardinality of infinite cardinals. The last file "lfcx.v" contains a construction of a little counterexample showing that there can be localizing systems which satisfy left fractions but in which the equivalence relation needs to be defined using intermediate arrows not in the localizing system, because we don't assume the "3 for 2" condition.
Here is a tar archive with all of the files (including the above plus the set theory and category theory ones) which need to be compiled together: gzfiles.tar.gz.