From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- dev/doc/README-V1-V5.asciidoc | 378 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 378 insertions(+) create mode 100644 dev/doc/README-V1-V5.asciidoc (limited to 'dev/doc/README-V1-V5.asciidoc') diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc new file mode 100644 index 00000000..631fb92c --- /dev/null +++ b/dev/doc/README-V1-V5.asciidoc @@ -0,0 +1,378 @@ +Notes on the prehistory of Coq +============================== +:author: Thierry Coquand, Gérard Huet & Christine Paulin-Mohring +:revdate: September 2015 +:toc: +:toc-placement: preamble +:toclevels: 1 +:showtitle: + + +This document is a copy within the Coq archive of a document written +in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin +to accompany their public release of the archive of versions 1.10 to 6.2 +of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and +implemented in the Formel team, joint between the INRIA Rocquencourt +laboratory and the Ecole Normale Supérieure of Paris, from 1984 +onwards. + +Version 1 +--------- + +This software is a prototype type-checker for a higher-order logical +formalism known as the Theory of Constructions, presented in his PhD +thesis by Thierry Coquand, with influences from Girard's system F and +de Bruijn's Automath. The metamathematical analysis of the system is +the PhD work of Thierry Coquand. The software is mostly the work of +Gérard Huet. Most of the mathematical examples verified with the +software are due to Thierry Coquand. + +The programming language of the CONSTR software (as it was called at +the time) was a version of ML adapted from the Edinburgh LCF system +and running on a LISP backend. The main improvements from the original +LCF ML were that ML was compiled rather than interpreted (Gérard Huet +building on the original translator by Lockwood Morris), and that it +was enriched by recursively defined types (work of Guy +Cousineau). This ancestor of CAML was used and improved by Larry +Paulson for his implementation of Cambridge LCF. + +Software developments of this prototype occurred from late 1983 to +early 1985. + +Version 1.10 was frozen on December 22nd 1984. It is the version used +for the examples in Thierry Coquand's thesis, defended on January 31st +1985. There was a unique binding operator, used both for universal +quantification (dependent product) at the level of types and +functional abstraction (λ) at the level of terms/proofs, in the manner +of Automath. Substitution (λ-reduction) was implemented using de +Bruijn's indexes. + +Version 1.11 was frozen on February 19th, 1985. It is the version used +for the examples in the paper: Th. Coquand, G. Huet. __Constructions: A +Higher Order Proof System for Mechanizing Mathematics__ <>. + +Christine Paulin joined the team at this point, for her DEA research +internship. In her DEA memoir (August 1985) she presents developments +for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such +that _f(m)_ is greater than _n_, for _f_ an increasing integer +function, a challenge for constructive mathematics. She also encoded +the majority voting algorithm of Boyer and Moore. + +Version 2 +--------- + +The formal system, now renamed as the _Calculus of Constructions_, was +presented with a proof of consistency and comparisons with proof +systems of Per Martin Löf, Girard, and the Automath family of N. de +Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of +Constructions__ <>. + +An abstraction of the software design, in the form of an abstract +machine for proof checking, and a fuller sequence of mathematical +developments was presented in: Th. Coquand, G. Huet. __Concepts +Mathématiques et Informatiques Formalisés dans le Calcul des +Constructions__<>. + +Version 2.8 was frozen on December 16th, 1985, and served for +developing the exemples in the above papers. + +This calculus was then enriched in version 2.9 with a cumulative +hierarchy of universes. Universe levels were initially explicit +natural numbers. Another improvement was the possibility of automatic +synthesis of implicit type arguments, relieving the user of tedious +redundant declarations. + +Christine Paulin wrote an article __Algorithm development in the +Calculus of Constructions__ <>. Besides _lambo_ and _majority_, +she presents quicksort and a text formatting algorithm. + +Version 2.13 of the Calculus of Constructions with universes was +frozen on June 25th, 1986. + +A synthetic presentation of type theory along constructive lines with +ML algorithms was given by Gérard Huet in his May 1986 CMU course +notes _Formal Structures for Computation and Deduction_. Its chapter +_Induction and Recursion in the Theory of Constructions_ was presented +as an invited paper at the Joint Conference on Theory and Practice of +Software Development TAPSOFT’87 at Pise in March 1987, and published +as __Induction Principles Formalized in the Calculus of +Constructions__ <>. + +Version 3 +--------- + +This version saw the beginning of proof automation, with a search +algorithm inspired from PROLOG and the applicative logic programming +programs of the course notes _Formal structures for computation and +deduction_. The search algorithm was implemented in ML by Thierry +Coquand. The proof system could thus be used in two modes: proof +verification and proof synthesis, with tactics such as `AUTO`. + +The implementation language was now called CAML, for Categorical +Abstract Machine Language. It used as backend the LLM3 virtual machine +of Le Lisp by Jérôme Chailloux. The main developers of CAML were +Michel Mauny, Ascander Suarez and Pierre Weis. + +V3.1 was started in the summer of 1986, V3.2 was frozen at the end of +November 1986. V3.4 was developed in the first half of 1987. + +Thierry Coquand held a post-doctoral position in Cambrige University +in 1986-87, where he developed a variant implementation in SML, with +which he wrote some developments on fixpoints in Scott's domains. + +Version 4 +--------- + +This version saw the beginning of program extraction from proofs, with +two varieties of the type `Prop` of propositions, indicating +constructive intent. The proof extraction algorithms were implemented +by Christine Paulin-Mohring. + +V4.1 was frozen on July 24th, 1987. It had a first identified library +of mathematical developments (directory exemples), with libraries +Logic (containing impredicative encodings of intuitionistic logic and +algebraic primitives for booleans, natural numbers and list), `Peano` +developing second-order Peano arithmetic, `Arith` defining addition, +multiplication, euclidean division and factorial. Typical developments +were the Knaster-Tarski theorem and Newman's lemma from rewriting +theory. + +V4.2 was a joint development of a team consisting of Thierry Coquand, +Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the +log of changes. It was frozen on September 1987 as the last version +implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable +development system. + +V4.3 saw the first top-level of the system. Instead of evaluating +explicit quotations, the user could develop his mathematics in a +high-level language called the mathematical vernacular (following +Automath terminology). The user could develop files in the vernacular +notation (with .v extension) which were now separate from the `ml` +sources of the implementation. Gilles Dowek joined the team to +develop the vernacular language as his DEA internship research. + +A notion of sticky constant was introduced, in order to keep names of +lemmas when local hypotheses of proofs were discharged. This gave a +notion of global mathematical environment with local sections. + +Another significant practical change was that the system, originally +developped on the VAX central computer of our lab, was transferred on +SUN personal workstations, allowing a level of distributed +development. The extraction algorithm was modified, with three +annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and +`Type`. + +Version 4.3 was frozen at the end of November 1987, and was +distributed to an early community of users (among those were Hugo +Herbelin and Loic Colson). + +V4.4 saw the first version of (encoded) inductive types. Now natural +numbers could be defined as: + +[source, coq] +Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. + +These inductive types were encoded impredicatively in the calculus, +using a subsystem _rec_ due to Christine Paulin. V4.4 was frozen on +March 6th 1988. + +Version 4.5 was the first one to support inductive types and program +extraction. Its banner was _Calcul des Constructions avec +Réalisations et Synthèse_. The vernacular language was enriched to +accommodate extraction commands. + +The verification engine design was presented as: G. Huet. _The +Constructive Engine_. Version 4.5. Invited Conference, 2nd European +Symposium on Programming, Nancy, March 88. The final paper, +describing the V4.9 implementation, appeared in: A perspective in +Theoretical Computer Science, Commemorative Volume in memory of Gift +Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. + +Version 4.5 was demonstrated in June 1988 at the YoP Institute on +Logical Foundations of Functional Programming organized by Gérard Huet +at Austin, Texas. + +Version 4.6 was started during the summer of 1988. Its main +improvement was the complete rehaul of the proof synthesis engine by +Thierry Coquand, with a tree structure of goals. + +Its source code was communicated to Randy Pollack on September 2nd +1988. It evolved progressively into LEGO, proof system for Luo's +formalism of Extended Calculus of Constructions. + +The discharge tactic was modified by Gérard Huet to allow for +inter-dependencies in discharged lemmas. Christine Paulin improved the +inductive definition scheme in order to accommodate predicates of any +arity. + +Version 4.7 was started on September 6th, 1988. + +This version starts exploiting the CAML notion of module in order to +improve the modularity of the implementation. Now the term verifier is +identified as a proper module Machine, which the structure of its +internal data structures being hidden and thus accessible only through +the legitimate operations. This machine (the constructive engine) was +the trusted core of the implementation. The proof synthesis mechanism +was a separate proof term generator. Once a complete proof term was +synthesized with the help of tactics, it was entirely re-checked by +the engine. Thus there was no need to certify the tactics, and the +system took advantage of this fact by having tactics ignore the +universe levels, universe consistency check being relegated to the +final type-checking pass. This induced a certain puzzlement in early +users who saw, after a successful proof search, their `QED` followed +by silence, followed by a failure message due to a universe +inconsistency… + +The set of examples comprise set theory experiments by Hugo Herbelin, +and notably the Schroeder-Bernstein theorem. + +Version 4.8, started on October 8th, 1988, saw a major +re-implementation of the abstract syntax type `constr`, separating +variables of the formalism and metavariables denoting incomplete terms +managed by the search mechanism. A notion of level (with three values +`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement +clarifies the constructions, whose implementation is now fully +explicit. Structural equality is speeded up by using pointer equality, +yielding spectacular improvements. Thierry Coquand adapts the proof +synthesis to the new representation, and simplifies pattern matching +to first-order predicate calculus matching, with important performance +gain. + +A new representation of the universe hierarchy is then defined by +Gérard Huet. Universe levels are now implemented implicitly, through +a hidden graph of abstract levels constrained with an order relation. +Checking acyclicity of the graph insures well-foundedness of the +ordering, and thus consistency. This was documented in a memo _Adding +Type:Type to the Calculus of Constructions_ which was never published. + +The development version is released as a stable 4.8 at the end of +1988. + +Version 4.9 is released on March 1st 1989, with the new ``elastic'' +universe hierarchy. + +The spring of 1989 saw the first attempt at documenting the system +usage, with a number of papers describing the formalism: + +- _Metamathematical Investigations of a Calculus of Constructions_, by + Thierry Coquand <>, +- _Inductive definitions in the Calculus of Constructions_, by + Christine Paulin-Mohrin, +- _Extracting Fω's programs from proofs in the Calculus of + Constructions_, by Christine Paulin-Mohring <>, +- _The Constructive Engine_, by Gérard Huet <>, + +as well as a number of user guides: + +- _A short user's guide for the Constructions_ Version 4.10, by Gérard Huet +- _A Vernacular Syllabus_, by Gilles Dowek. +- _The Tactics Theorem Prover, User's guide_, Version 4.10, by Thierry + Coquand. + +Stable V4.10, released on May 1st, 1989, was then a mature system, +distributed with CAML V2.6. + +In the mean time, Thierry Coquand and Christine Paulin-Mohring had +been investigating how to add native inductive types to the Calculus +of Constructions, in the manner of Per Martin-Löf's Intuitionistic +Type Theory. The impredicative encoding had already been presented in: +F. Pfenning and C. Paulin-Mohring. __Inductively defined types in the +Calculus of Constructions__ <>. An extension of the calculus +with primitive inductive types appeared in: Th. Coquand and +C. Paulin-Mohring. __Inductively defined types__ <>. + +This led to the Calculus of Inductive Constructions, logical formalism +implemented in Versions 5 upward of the system, and documented in: +C. Paulin-Mohring. __Inductive Definitions in the System Coq - Rules +and Properties__ <>. + +The last version of CONSTR is Version 4.11, which was last distributed +in the spring of 1990. It was demonstrated at the first workshop of +the European Basic Research Action Logical Frameworks In Sophia +Antipolis in May 1990. + +At the end of 1989, Version 5.1 was started, and renamed as the system +Coq for the Calculus of Inductive Constructions. It was then ported to +the new stand-alone implementation of ML called Caml-light. + +In 1990 many changes occurred. Thierry Coquand left for Chalmers +University in Göteborg. Christine Paulin-Mohring took a CNRS +researcher position at the LIP laboratory of École Normale Supérieure +de Lyon. Project Formel was terminated, and gave rise to two teams: +Cristal at INRIA-Roquencourt, that continued developments in +functional programming with Caml-light then Ocaml, and Coq, continuing +the type theory research, with a joint team headed by Gérard Huet at +INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory +of CNRS-ENS Lyon. + +Chetan Murthy joined the team in 1991 and became the main software +architect of Version 5. He completely rehauled the implementation for +efficiency. Versions 5.6 and 5.8 were major distributed versions, +with complete documentation and a library of users' developements. The +use of the RCS revision control system, and systematic ChangeLog +files, allow a more precise tracking of the software developments. + +Developments from Version 6 upwards are documented in the credits +section of Coq's Reference Manual. + +==== +September 2015 + +Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. +==== + +[bibliography] +.Bibliographic references + +- [[[CH85]]] Th. Coquand, G. Huet. _Constructions: A Higher Order + Proof System for Mechanizing Mathematics_. Invited paper, EUROCAL85, + April 1985, Linz, Austria. Springer Verlag LNCS 203, pp. 151-184. + +- [[[CH88]]] T. Coquand and G. Huet. _The Calculus of Constructions_. + Submitted on June 30th 1985, accepted on December 5th, 1985, + Information and Computation. Preprint as Rapport de Recherche Inria + n°530, Mai 1986. Final version in Information and Computation + 76,2/3, Feb. 88. + +- [[[CH87]]] Th. Coquand, G. Huet. _Concepts Mathématiques et + Informatiques Formalisés dans le Calcul des Constructions_. Invited + paper, European Logic Colloquium, Orsay, July 1985. Preprint as + Rapport de recherche INRIA n°463, Dec. 85. Published in Logic + Colloquium 1985, North-Holland, 1987. + +- [[[P86]]] C. Paulin. _Algorithm development in the Calculus of + Constructions_, preprint as Rapport de recherche INRIA n°497, + March 86. Final version in Proceedings Symposium on Logic in Computer + Science, Cambridge, MA, 1986 (IEEE Computer Society Press). + +- [[[H88]]] G. Huet. _Induction Principles Formalized in the Calculus + of Constructions_ in Programming of Future Generation Computers, + Ed. K. Fuchi and M. Nivat, North-Holland, 1988. + +- [[[C90]]] Th. Coquand. _Metamathematical Investigations of a + Calculus of Constructions_, by INRIA Research Report N°1088, + Sept. 1989, published in Logic and Computer Science, + ed. P.G. Odifreddi, Academic Press, 1990. + +- [[[P89]]] C. Paulin. _Extracting F ω's programs from proofs in the + calculus of constructions_. 16th Annual ACM Symposium on Principles + of Programming Languages, Austin. 1989. + +- [[[H89]]] G. Huet. _The constructive engine_. A perspective in + Theoretical Computer Science. Commemorative Volume for Gift + Siromoney. World Scientific Publishing (1989). + +- [[[PP90]]] F. Pfenning and C. Paulin-Mohring. _Inductively defined + types in the Calculus of Constructions_. Preprint technical report + CMU-CS-89-209, final version in Proceedings of Mathematical + Foundations of Programming Semantics, volume 442, Lecture Notes in + Computer Science. Springer-Verlag, 1990 + +- [[[CP90]]] Th. Coquand and C. Paulin-Mohring. _Inductively defined + types_. In P. Martin-Löf and G. Mints, editors, Proceedings of + Colog'88, volume 417, Lecture Notes in Computer Science. + Springer-Verlag, 1990. + +- [[[P93]]] C. Paulin-Mohring. _Inductive Definitions in the System + Coq - Rules and Properties_. In M. Bezem and J.-F. Groote, editors, + Proceedings of the conference Typed Lambda Calculi and Applications, + volume 664, Lecture Notes in Computer Science, 1993. -- cgit v1.2.3