Carlos Simpson---work in progress

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.

A forward automation tool

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!

A weak version of the axiom of choice

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.

Cohomology in intuitionist type theory

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

Writing math using a program

Here is a little first attempt at a program to create Coq expressions directly from OCaml. Version of Monday, September 3rd 2002.

A wish-list for notation

Here we give some parameters and axioms that attempt to start constituting a wish-list for notations that could be used in an economical way.

Version of Thursday, October 3rd 2002.

Version of Tuesday, October 22nd 2002.

Set-theoretical mathematics

Here we give a development of some mathematics in ZFC-style set theory. This combines functions-in-ZFC from the top of the page, with the preceding wish-list. There are almost no proofs though (the lemmas are skipped with a joker).

Version of Thursday, April 17th 2003.

Interpreting set-theory

A short start on a program to interpret documents which might be written in a style similar to the previous item.

Very preliminary version of Friday, May 16th 2003.

The classical semantics in Coq

A beginning of an axiomatic system for classical semantics in Coq, integrating a little bit more information than e.g. in Benjamin Werner's developpement (note on the other hand that our axioms put in place the semantics given by Werner in his paper).

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.

Disturbance due to measure in Coq

Here is an example of two theorems of the form "A" and "A"->False, where the phrases "A" are typographically identical. Putting the two together yields a Universe Inconsistency, because the word "Type" is assigned a different universe index in the two cases.

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)

Computer theorem proving in math, A paper based on my talk at the PQR conference, Brussels, June 2003.

Categories in set-theoretical style

Friday, April 16th: an incomplete version of stuff about categories, functors, natural transformations, presheaves, limits, and a start on the theorem that presheaf categories into categories having limits, have limits. The file index.
Friday, May 14th: a more complete version of stuff about categories, functors, natural transformations, presheaves, limits, the theorem that presheaf categories into categories having limits, have limits. The file index.
The file index for a thinned-down and slightly modified version concerning only categories, June 18th 2004.

Limits in functor categories

A revised version of the May version of Categories in set-theoretical style, incorporating June's notational fixes. We prove the existence of limits (and summarily colimits) in functor categories. Here is the file index for the version of Wednesday, August 11th 2004.

A further expanded edition of Thursday, September 23rd, 2004: with 20 files it comes in a tar-compacted directory nc_cat_th. Recall the instructions (for linux-like systems): (0) tar -xvf nccatth230904.tar (1) cd nc_cat_th (2) touch .depend (3) coq_makefile -o makefile *.v (4) make depend (5) make all
The category theory contribution is now available on CCSD and ArXiV. The Coq source files are available as annex files on the CCSD (you have to click on ``Fiche detaille'') and bundled with the source file in ArXiV (you have to go to ``other formats'' then ``source'' and you get a tar archive with the tex source plus all the proof files). To be more direct, here is a tar archive containing the proof files plus a pdf file of the paper.

Gabriel-Zisman localization

My current project is to prove Theorem 1.2 of Gabriel-Zisman on the construction and universal property of the localization of categories. They left the proof to the reader. Note that this theory is essential before we can discuss Quillen's closed model categories. We would also have to consider calculi of fractions but that will be for later.

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.

Updated version---March 2005

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.

April 7, 2006: the files have been regrouped into a smaller number of big files, with a very small reorganization of some modules:
set.v, func.v, ord.v, cat.v, gz.v.
Friday, April 13th, 2007: some further reorganization, porting to Coq 8.1; this includes replacing ad-hoc string objects by standard-library strings; also a slow start on trees in the comb.v file.
set.v, func.v, ord.v, comb.v, cat.v, gz.v, or everything in a single tar archive.