Verification and creation of proofs by computer

Refer to the old version of this page for historical versions.


Set theory, category theory, and Gabriel-Zisman localization

The latest version of everything, ported to Coq 8.1, in a small number of files. Each file is fairly big but organized into modules:
set.v, func.v, ord.v, comb.v, cat.v, gz.v. Here is everything in a single tar archive.

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). This was in June 2003. In July 2003, an early treatment of ordered sets was started. In
September 2003, was the gadget of using very short
abbreviations for standard tactics. October 2003: a general format for notation for objects.
We get up to a proof of Zorn's lemma, and start on the problem of notation for objects. In November 2003, an
alphabetic string datatype as the basis for notation
was done by hand (this is later supplanted by Coq's string datatype).The version of February 2004

treats more stuff about well-ordered sets, transfinite induction, ordinals, and contains a small development on topology showing that the product of two connected spaces is connected.

Categories in set-theoretical style

April and May 2004, we do basic category theory including categories, functors, natural transformations, presheaves, limits, and a start on the theorem that presheaf categories into categories having limits, have limits. 

Limits in functor categories

A revised version of the May version of Categories in set-theoretical style, incorporates June's notational fixes. We prove the existence of limits (and summarily colimits) in functor categories. The category theory contribution is 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

As an application of the category theory development, we give a full proof of 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, we define the free category making free use of the Omega tactic to deal with arithmetic of indices in uples of arrows.

For the second step,  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).

For the third and fourth steps, 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. We give 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.

At the end of the first version (January 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.

In an update of March 2005, 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. The original files refered to above can be found on the old version of this page. In the latest version things have been reorganized into a small number of bigger files. 

Here are the CCSD and ArXiV versions of the preprint Files for Gabriel-Zisman localization ps, pdf, gzfiles.tar.gz containing the files for this work. This preprint goes with the paper referred to above. 



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. The latest version is h1V8.v in Coq v8.0beta, January 2004


Disturbance due to measure in Coq

This is an independent development of 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. The idea is that this could be considered as a kind of quantum mechanical
behavior. The latest version is
quaV8.v in Coq v8.0beta, January 2004.

Old experiments

Functions in classical Zermelo-Fraenkel (with choice) 

An experiment in writing formal mathematics in Coq:
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.



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 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.