From 0063c4c985078fd181c4a3a149ccbb06752edc97 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 15 Mar 2019 13:32:36 +0100 Subject: Remove clutter by moving historic unmaintained dev/doc files to an archive subfolder. --- dev/doc/COMPATIBILITY | 201 --------- dev/doc/archive/COMPATIBILITY | 201 +++++++++ dev/doc/archive/extensions.txt | 18 + dev/doc/archive/naming-conventions.tex | 606 +++++++++++++++++++++++++++ dev/doc/archive/newsyntax.tex | 725 +++++++++++++++++++++++++++++++++ dev/doc/archive/notes-on-conversion.v | 71 ++++ dev/doc/archive/old_svn_branches.txt | 33 ++ dev/doc/archive/perf-analysis | 167 ++++++++ dev/doc/archive/versions-history.tex | 451 ++++++++++++++++++++ dev/doc/extensions.txt | 19 - dev/doc/naming-conventions.tex | 606 --------------------------- dev/doc/newsyntax.tex | 725 --------------------------------- dev/doc/notes-on-conversion.v | 73 ---- dev/doc/old_svn_branches.txt | 33 -- dev/doc/perf-analysis | 167 -------- dev/doc/versions-history.tex | 451 -------------------- 16 files changed, 2272 insertions(+), 2275 deletions(-) delete mode 100644 dev/doc/COMPATIBILITY create mode 100644 dev/doc/archive/COMPATIBILITY create mode 100644 dev/doc/archive/extensions.txt create mode 100644 dev/doc/archive/naming-conventions.tex create mode 100644 dev/doc/archive/newsyntax.tex create mode 100644 dev/doc/archive/notes-on-conversion.v create mode 100644 dev/doc/archive/old_svn_branches.txt create mode 100644 dev/doc/archive/perf-analysis create mode 100644 dev/doc/archive/versions-history.tex delete mode 100644 dev/doc/extensions.txt delete mode 100644 dev/doc/naming-conventions.tex delete mode 100644 dev/doc/newsyntax.tex delete mode 100644 dev/doc/notes-on-conversion.v delete mode 100644 dev/doc/old_svn_branches.txt delete mode 100644 dev/doc/perf-analysis delete mode 100644 dev/doc/versions-history.tex (limited to 'dev/doc') diff --git a/dev/doc/COMPATIBILITY b/dev/doc/COMPATIBILITY deleted file mode 100644 index a81afca32d..0000000000 --- a/dev/doc/COMPATIBILITY +++ /dev/null @@ -1,201 +0,0 @@ -Note: this file isn't used anymore. Incompatibilities are documented -as part of CHANGES. - -Potential sources of incompatibilities between Coq V8.6 and V8.7 ----------------------------------------------------------------- - -- Extra superfluous names in introduction patterns may now raise an - error rather than a warning when the superfluous name is already in - use. The easy fix is to remove the superfluous name. - -Potential sources of incompatibilities between Coq V8.5 and V8.6 ----------------------------------------------------------------- - -Symptom: An obligation generated by Program or an abstracted subproof -has different arguments. -Cause: Set Shrink Abstract and Set Shrink Obligations are on by default -and the subproof does not use the argument. -Remedy: -- Adapt the script. -- Write an explicit lemma to prove the obligation/subproof and use it - instead (compatible with 8.4). -- Unset the option for the program/proof the obligation/subproof originates - from. - -Symptom: In a goal, order of hypotheses, or absence of an equality of -the form "x = t" or "t = x", or no unfolding of a local definition. -Cause: This might be connected to a number of fixes in the tactic -"subst". The former behavior can be reactivated by issuing "Unset -Regular Subst Tactic". - -Potential sources of incompatibilities between Coq V8.4 and V8.5 ----------------------------------------------------------------- - -* List of typical changes to be done to adapt files from Coq 8.4 * -* to Coq 8.5 when not using compatibility option "-compat 8.4". * - -Symptom: "The reference omega was not found in the current environment". -Cause: "Require Omega" does not import the tactic "omega" any more -Possible solutions: -- use "Require Import OmegaTactic" (not compatible with 8.4) -- use "Require Import Omega" (compatible with 8.4) -- add definition "Ltac omega := Coq.omega.Omega.omega." - -Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective) -Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives -Possible solutions: -- use "dintuition" instead; it is stronger than "intuition" and works - uniformly on non standard connectives, such as n-ary conjunctions or disjunctions - (not compatible with 8.4) -- do the script differently - -Symptom: The constructor foo (in type bar) expects n arguments. -Cause: parameters must now be given in patterns -Possible solutions: -- use option "Set Asymmetric Patterns" (compatible with 8.4) -- add "_" for the parameters (not compatible with 8.4) -- turn the parameters into implicit arguments (compatible with 8.4) - -Symptom: "NPeano.Nat.foo" not existing anymore -Possible solutions: -- use "Nat.foo" instead - -Symptom: typing problems with proj1_sig or similar -Cause: coercion from sig to sigT and similar coercions have been - removed so as to make the initial state easier to understand for - beginners -Solution: change proj1_sig into projT1 and similarly (compatible with 8.4) - -* Other detailed changes * - -(see also file CHANGES) - -- options for *coq* compilation (see below for ocaml). - -** [-I foo] is now deprecated and will not add directory foo to the - coq load path (only for ocaml, see below). Just replace [-I foo] by - [-Q foo ""] in your project file and re-generate makefile. Or - perform the same operation directly in your makefile if you edit it - by hand. - -** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq - load path. - -** Option [-I foo -as bar] is unchanged but discouraged unless you - compile ocaml code. Use -Q foo bar instead. - - for more details: file CHANGES or section "Customization at launch - time" of the reference manual. - -- Command line options for ocaml Compilation of ocaml code (plugins) - -** [-I foo] is *not* deprecated to add foo to the ocaml load path. - -** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to - the coq load path with logical name bar (shortcut for -I foo -Q foo - bar). - - for more details: file CHANGES or section "Customization at launch - time" of the reference manual. - -- Universe Polymorphism. - -- Refinement, unification and tactics are now aware of universes, - resulting in more localized errors. Universe inconsistencies - should no more get raised at Qed time but during the proof. - Unification *always* produces well-typed substitutions, hence - some rare cases of unifications that succeeded while producing - ill-typed terms before will now fail. - -- The [change p with c] tactic semantics changed, now typechecking - [c] at each matching occurrence [t] of the pattern [p], and - converting [t] with [c]. - -- Template polymorphic inductive types: the partial application - of a template polymorphic type (e.g. list) is not polymorphic. - An explicit parameter application (e.g [fun A => list A]) or - [apply (list _)] will result in a polymorphic instance. - -- The type inference algorithm now takes opacity of constants into - account. This may have effects on tactics using type inference - (e.g. induction). Extra "Transparent" might have to be added to - revert opacity of constants. - -Type classes. - -- When writing an Instance foo : Class A := {| proj := t |} (note the - vertical bars), support for typechecking the projections using the - type information and switching to proof mode is no longer available. - Use { } (without the vertical bars) instead. - -Tactic abstract. - -- Auxiliary lemmas generated by the abstract tactic are removed from - the global environment and inlined in the proof term when a proof - is ended with Qed. The behavior of 8.4 can be obtained by ending - proofs with "Qed exporting" or "Qed exporting ident, .., ident". - -Potential sources of incompatibilities between Coq V8.3 and V8.4 ----------------------------------------------------------------- - -(see also file CHANGES) - -The main known incompatibilities between 8.3 and 8.4 are consequences -of the following changes: - -- The reorganization of the library of numbers: - - Several definitions have new names or are defined in modules of - different names, but a special care has been taken to have this - renaming transparent for the user thanks to compatibility notations. - - However some definitions have changed, what might require some - adaptations. The most noticeable examples are: - - The "?=" notation which now bind to Pos.compare rather than former - Pcompare (now Pos.compare_cont). - - Changes in names may induce different automatically generated - names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec"). - - Z.add has a new definition, hence, applying "simpl" on subterms of - its body might give different results than before. - - BigN.shiftl and BigN.shiftr have reversed arguments order, the - power function in BigN now takes two BigN. - -- Other changes in libraries: - - - The definition of functions over "vectors" (list of fixed length) - have changed. - - TheoryList.v has been removed. - -- Slight changes in tactics: - - - Less unfolding of fixpoints when applying destruct or inversion on - a fixpoint hiding an inductive type (add an extra call to simpl to - preserve compatibility). - - Less unexpected local definitions when applying "destruct" - (incompatibilities solvable by adapting name hypotheses). - - Tactic "apply" might succeed more often, e.g. by now solving - pattern-matching of the form ?f x y = g(x,y) (compatibility - ensured by using "Unset Tactic Pattern Unification"), but also - because it supports (full) betaiota (using "simple apply" might - then help). - - Tactic autorewrite does no longer instantiate pre-existing - existential variables. - - Tactic "info" is now available only for auto, eauto and trivial. - -- Miscellaneous changes: - - - The command "Load" is now atomic for backtracking (use "Unset - Atomic Load" for compatibility). - - -Incompatibilities beyond 8.4... - -- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is - now "A -> (B <-> C)" - -- Tactics: tauto and intuition no longer accidentally destruct binary - connectives or records other than and, or, prod, sum, iff. In most - of cases, dtauto or dintuition, though stronger than 8.3 tauto and - 8.3 intuition will provide compatibility. - -- "Solve Obligations using" is now "Solve Obligations with". diff --git a/dev/doc/archive/COMPATIBILITY b/dev/doc/archive/COMPATIBILITY new file mode 100644 index 0000000000..a81afca32d --- /dev/null +++ b/dev/doc/archive/COMPATIBILITY @@ -0,0 +1,201 @@ +Note: this file isn't used anymore. Incompatibilities are documented +as part of CHANGES. + +Potential sources of incompatibilities between Coq V8.6 and V8.7 +---------------------------------------------------------------- + +- Extra superfluous names in introduction patterns may now raise an + error rather than a warning when the superfluous name is already in + use. The easy fix is to remove the superfluous name. + +Potential sources of incompatibilities between Coq V8.5 and V8.6 +---------------------------------------------------------------- + +Symptom: An obligation generated by Program or an abstracted subproof +has different arguments. +Cause: Set Shrink Abstract and Set Shrink Obligations are on by default +and the subproof does not use the argument. +Remedy: +- Adapt the script. +- Write an explicit lemma to prove the obligation/subproof and use it + instead (compatible with 8.4). +- Unset the option for the program/proof the obligation/subproof originates + from. + +Symptom: In a goal, order of hypotheses, or absence of an equality of +the form "x = t" or "t = x", or no unfolding of a local definition. +Cause: This might be connected to a number of fixes in the tactic +"subst". The former behavior can be reactivated by issuing "Unset +Regular Subst Tactic". + +Potential sources of incompatibilities between Coq V8.4 and V8.5 +---------------------------------------------------------------- + +* List of typical changes to be done to adapt files from Coq 8.4 * +* to Coq 8.5 when not using compatibility option "-compat 8.4". * + +Symptom: "The reference omega was not found in the current environment". +Cause: "Require Omega" does not import the tactic "omega" any more +Possible solutions: +- use "Require Import OmegaTactic" (not compatible with 8.4) +- use "Require Import Omega" (compatible with 8.4) +- add definition "Ltac omega := Coq.omega.Omega.omega." + +Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective) +Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives +Possible solutions: +- use "dintuition" instead; it is stronger than "intuition" and works + uniformly on non standard connectives, such as n-ary conjunctions or disjunctions + (not compatible with 8.4) +- do the script differently + +Symptom: The constructor foo (in type bar) expects n arguments. +Cause: parameters must now be given in patterns +Possible solutions: +- use option "Set Asymmetric Patterns" (compatible with 8.4) +- add "_" for the parameters (not compatible with 8.4) +- turn the parameters into implicit arguments (compatible with 8.4) + +Symptom: "NPeano.Nat.foo" not existing anymore +Possible solutions: +- use "Nat.foo" instead + +Symptom: typing problems with proj1_sig or similar +Cause: coercion from sig to sigT and similar coercions have been + removed so as to make the initial state easier to understand for + beginners +Solution: change proj1_sig into projT1 and similarly (compatible with 8.4) + +* Other detailed changes * + +(see also file CHANGES) + +- options for *coq* compilation (see below for ocaml). + +** [-I foo] is now deprecated and will not add directory foo to the + coq load path (only for ocaml, see below). Just replace [-I foo] by + [-Q foo ""] in your project file and re-generate makefile. Or + perform the same operation directly in your makefile if you edit it + by hand. + +** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq + load path. + +** Option [-I foo -as bar] is unchanged but discouraged unless you + compile ocaml code. Use -Q foo bar instead. + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + +- Command line options for ocaml Compilation of ocaml code (plugins) + +** [-I foo] is *not* deprecated to add foo to the ocaml load path. + +** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to + the coq load path with logical name bar (shortcut for -I foo -Q foo + bar). + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + +- Universe Polymorphism. + +- Refinement, unification and tactics are now aware of universes, + resulting in more localized errors. Universe inconsistencies + should no more get raised at Qed time but during the proof. + Unification *always* produces well-typed substitutions, hence + some rare cases of unifications that succeeded while producing + ill-typed terms before will now fail. + +- The [change p with c] tactic semantics changed, now typechecking + [c] at each matching occurrence [t] of the pattern [p], and + converting [t] with [c]. + +- Template polymorphic inductive types: the partial application + of a template polymorphic type (e.g. list) is not polymorphic. + An explicit parameter application (e.g [fun A => list A]) or + [apply (list _)] will result in a polymorphic instance. + +- The type inference algorithm now takes opacity of constants into + account. This may have effects on tactics using type inference + (e.g. induction). Extra "Transparent" might have to be added to + revert opacity of constants. + +Type classes. + +- When writing an Instance foo : Class A := {| proj := t |} (note the + vertical bars), support for typechecking the projections using the + type information and switching to proof mode is no longer available. + Use { } (without the vertical bars) instead. + +Tactic abstract. + +- Auxiliary lemmas generated by the abstract tactic are removed from + the global environment and inlined in the proof term when a proof + is ended with Qed. The behavior of 8.4 can be obtained by ending + proofs with "Qed exporting" or "Qed exporting ident, .., ident". + +Potential sources of incompatibilities between Coq V8.3 and V8.4 +---------------------------------------------------------------- + +(see also file CHANGES) + +The main known incompatibilities between 8.3 and 8.4 are consequences +of the following changes: + +- The reorganization of the library of numbers: + + Several definitions have new names or are defined in modules of + different names, but a special care has been taken to have this + renaming transparent for the user thanks to compatibility notations. + + However some definitions have changed, what might require some + adaptations. The most noticeable examples are: + - The "?=" notation which now bind to Pos.compare rather than former + Pcompare (now Pos.compare_cont). + - Changes in names may induce different automatically generated + names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec"). + - Z.add has a new definition, hence, applying "simpl" on subterms of + its body might give different results than before. + - BigN.shiftl and BigN.shiftr have reversed arguments order, the + power function in BigN now takes two BigN. + +- Other changes in libraries: + + - The definition of functions over "vectors" (list of fixed length) + have changed. + - TheoryList.v has been removed. + +- Slight changes in tactics: + + - Less unfolding of fixpoints when applying destruct or inversion on + a fixpoint hiding an inductive type (add an extra call to simpl to + preserve compatibility). + - Less unexpected local definitions when applying "destruct" + (incompatibilities solvable by adapting name hypotheses). + - Tactic "apply" might succeed more often, e.g. by now solving + pattern-matching of the form ?f x y = g(x,y) (compatibility + ensured by using "Unset Tactic Pattern Unification"), but also + because it supports (full) betaiota (using "simple apply" might + then help). + - Tactic autorewrite does no longer instantiate pre-existing + existential variables. + - Tactic "info" is now available only for auto, eauto and trivial. + +- Miscellaneous changes: + + - The command "Load" is now atomic for backtracking (use "Unset + Atomic Load" for compatibility). + + +Incompatibilities beyond 8.4... + +- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is + now "A -> (B <-> C)" + +- Tactics: tauto and intuition no longer accidentally destruct binary + connectives or records other than and, or, prod, sum, iff. In most + of cases, dtauto or dintuition, though stronger than 8.3 tauto and + 8.3 intuition will provide compatibility. + +- "Solve Obligations using" is now "Solve Obligations with". diff --git a/dev/doc/archive/extensions.txt b/dev/doc/archive/extensions.txt new file mode 100644 index 0000000000..36d63029f1 --- /dev/null +++ b/dev/doc/archive/extensions.txt @@ -0,0 +1,18 @@ +Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ? +====================================================================== + +Exemple de l'ajout de l'entrée "clause": + +- ajouter un type ClauseArgType dans interp/genarg.ml{,i}, avec les + wit_, rawwit_, et globwit_ correspondants + +- ajouter partout où Genarg.argument_type est filtré le cas traitant de + ce nouveau ClauseArgType + +- utiliser le rawwit_clause pour définir une entrée clause du bon + type et du bon nom dans le module Tactic de pcoq.ml4 + +- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il + faut rejouter clause dans le GLOBAL du GEXTEND + +- seulement après, le nom clause sera accessible dans les TACTIC EXTEND ! diff --git a/dev/doc/archive/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex new file mode 100644 index 0000000000..0b0811d81b --- /dev/null +++ b/dev/doc/archive/naming-conventions.tex @@ -0,0 +1,606 @@ +\documentclass[a4paper]{article} +\usepackage{fullpage} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{amsfonts} + +\parindent=0pt +\parskip=10pt + +%%%%%%%%%%%%% +% Macros +\newcommand\itemrule[3]{ +\subsubsection{#1} +\begin{quote} +\begin{tt} +#3 +\end{tt} +\end{quote} +\begin{quote} +Name: \texttt{#2} +\end{quote}} + +\newcommand\formula[1]{\begin{tt}#1\end{tt}} +\newcommand\tactic[1]{\begin{tt}#1\end{tt}} +\newcommand\command[1]{\begin{tt}#1\end{tt}} +\newcommand\term[1]{\begin{tt}#1\end{tt}} +\newcommand\library[1]{\texttt{#1}} +\newcommand\name[1]{\texttt{#1}} + +\newcommand\zero{\texttt{zero}} +\newcommand\op{\texttt{op}} +\newcommand\opPrime{\texttt{op'}} +\newcommand\opSecond{\texttt{op''}} +\newcommand\phimapping{\texttt{phi}} +\newcommand\D{\texttt{D}} +\newcommand\elt{\texttt{elt}} +\newcommand\rel{\texttt{rel}} +\newcommand\relp{\texttt{rel'}} + +%%%%%%%%%%%%% + +\begin{document} + +\begin{center} +\begin{huge} +Proposed naming conventions for the Coq standard library +\end{huge} +\end{center} +\bigskip + +The following document describes a proposition of canonical naming +schemes for the Coq standard library. Obviously and unfortunately, the +current state of the library is not as homogeneous as it would be if +it would systematically follow such a scheme. To tend in this +direction, we however recommend to follow the following suggestions. + +\tableofcontents + +\section{General conventions} + +\subsection{Variable names} + +\begin{itemize} + +\item Variables are preferably quantified at the head of the + statement, even if some premisses do not depend of one of them. For + instance, one would state +\begin{quote} +\begin{tt} + {forall x y z:D, x <= y -> x+z <= y+z} +\end{tt} +\end{quote} +and not +\begin{quote} +\begin{tt} + {forall x y:D, x <= y -> forall z:D, x+z <= y+z} +\end{tt} +\end{quote} + +\item Variables are preferably quantified (and named) in the order of + ``importance'', then of appearance, from left to right, even if + for the purpose of some tactics it would have been more convenient + to have, say, the variables not occurring in the conclusion + first. For instance, one would state +\begin{quote} +\begin{tt} + {forall x y z:D, x+z <= y+z -> x <= y} +\end{tt} +\end{quote} +and not +\begin{quote} +\begin{tt} + {forall z x y:D, x+z <= y+z -> x <= y} +\end{tt} +\end{quote} +nor +\begin{quote} +\begin{tt} + {forall x y z:D, y+x <= z+x -> y <= z} +\end{tt} +\end{quote} + +\item Choice of effective names is domain-dependent. For instance, on + natural numbers, the convention is to use the variables $n$, $m$, + $p$, $q$, $r$, $s$ in this order. + + On generic domains, the convention is to use the letters $x$, $y$, + $z$, $t$. When more than three variables are needed, indexing variables + + It is conventional to use specific names for variables having a + special meaning. For instance, $eps$ or $\epsilon$ can be used to + denote a number intended to be as small as possible. Also, $q$ and + $r$ can be used to denote a quotient and a rest. This is good + practice. + +\end{itemize} + +\subsection{Disjunctive statements} + +A disjunctive statement with a computational content will be suffixed +by \name{\_inf}. For instance, if + +\begin{quote} +\begin{tt} +{forall x y, op x y = zero -> x = zero \/ y = zero} +\end{tt} +\end{quote} +has name \texttt{D\_integral}, then +\begin{quote} +\begin{tt} +{forall x y, op x y = zero -> \{x = zero\} + \{y = zero\}} +\end{tt} +\end{quote} +will have name \texttt{D\_integral\_inf}. + +As an exception, decidability statements, such as +\begin{quote} +\begin{tt} +{forall x y, \{x = y\} + \{x <> y\}} +\end{tt} +\end{quote} +will have a named ended in \texttt{\_dec}. Idem for cotransitivity +lemmas which are inherently computational that are ended in +\texttt{\_cotrans}. + +\subsection{Inductive types constructor names} + +As a general rule, constructor names start with the name of the +inductive type being defined as in \texttt{Inductive Z := Z0 : Z | + Zpos : Z -> Z | Zneg : Z -> Z} to the exception of very standard +types like \texttt{bool}, \texttt{nat}, \texttt{list}... + +For inductive predicates, constructor names also start with the name +of the notion being defined with one or more suffixes separated with +\texttt{\_} for discriminating the different cases as e.g. in + +\begin{verbatim} +Inductive even : nat -> Prop := + | even_O : even 0 + | even_S n : odd n -> even (S n) +with odd : nat -> Prop := + | odd_S n : even n -> odd (S n). +\end{verbatim} + +As a general rule, inductive predicate names should be lowercase (to +the exception of notions referring to a proper name, e.g. \texttt{Bezout}) +and multiple words must be separated by ``{\_}''. + +As an exception, when extending libraries whose general rule is that +predicates names start with a capital letter, the convention of this +library should be kept and the separation between multiple words is +done by making the initial of each work a capital letter (if one of +these words is a proper name, then a ``{\_}'' is added to emphasize +that the capital letter is proper and not an application of the rule +for marking the change of word). + +Inductive predicates that characterize the specification of a function +should be named after the function it specifies followed by +\texttt{\_spec} as in: + +\begin{verbatim} +Inductive nth_spec : list A -> nat -> A -> Prop := + | nth_spec_O a l : nth_spec (a :: l) 0 a + | nth_spec_S n a b l : nth_spec l n a -> nth_spec (b :: l) (S n) a. +\end{verbatim} + +\section{Equational properties of operations} + +\subsection{General conventions} + +If the conclusion is in the other way than listed below, add suffix +\name{\_reverse} to the lemma name. + +\subsection{Specific conventions} + +\itemrule{Associativity of binary operator {\op} on domain {\D}}{Dop\_assoc} +{forall x y z:D, op x (op y z) = op (op x y) z} + + Remark: Symmetric form: \name{Dop\_assoc\_reverse}: + \formula{forall x y z:D, op (op x y) z = op x (op y z)} + +\itemrule{Commutativity of binary operator {\op} on domain {\D}}{Dop\_comm} +{forall x y:D, op x y = op y x} + + Remark: Avoid \formula{forall x y:D, op y x = op x y}, or at worst, call it + \name{Dop\_comm\_reverse} + +\itemrule{Left neutrality of element elt for binary operator {\op}}{Dop\_elt\_l} +{forall x:D, op elt x = x} + + Remark: In English, ``{\elt} is an identity for {\op}'' seems to be + a more common terminology. + +\itemrule{Right neutrality of element elt for binary operator {\op}}{Dop\_elt\_r} +{forall x:D, op x elt = x} + + Remark: By convention, if the identities are reminiscent to zero or one, they + are written 1 and 0 in the name of the property. + +\itemrule{Left absorption of element elt for binary operator {\op}}{Dop\_elt\_l} +{forall x:D, op elt x = elt} + + Remarks: + \begin{itemize} + \item In French school, this property is named "elt est absorbant pour op" + \item English, the property seems generally named "elt is a zero of op" + \item In the context of lattices, this a boundedness property, it may + be called "elt is a bound on D", or referring to a (possibly + arbitrarily oriented) order "elt is a least element of D" or "elt + is a greatest element of D" + \end{itemize} + +\itemrule{Right absorption of element {\elt} for binary operator {\op}}{Dop\_elt\_l [BAD ??]} +{forall x:D, op x elt = elt} + +\itemrule{Left distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_l} +{forall x y z:D, op (op' x y) z = op' (op x z) (op y z)} + + Remark: Some authors say ``distribution''. + +\itemrule{Right distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_r} +{forall x y z:D, op z (op' x y) = op' (op z x) (op z y)} + + Remark: Note the order of arguments. + +\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} +{forall x y:D, op (op' x y) = op' (op x) (op y)} + +\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} +{forall x y:D, op (op' x y) = op' (op x) (op y)} + + Remark: For a non commutative operation with inversion of arguments, as in + \formula{forall x y z:D, op (op' x y) = op' (op y) (op y z)}, + we may probably still call the property distributivity since there + is no ambiguity. + + Example: \formula{forall n m : Z, -(n+m) = (-n)+(-m)}. + + Example: \formula{forall l l' : list A, rev (l++l') = (rev l)++(rev l')}. + +\itemrule{Left extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l} +{forall x y:D, op (op' x y) = op' (op x) y} + + Question: Call it left commutativity ?? left swap ? + +\itemrule{Right extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r} +{forall x y:D, op (op' x y) = op' x (op y)} + +\itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} +{forall x:D, op x x = x} + +\itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent} +{forall x:D, op (op x) = op x} + + Remark: This is actually idempotency of {\op} wrt to composition and + identity. + +\itemrule{Idempotency of element elt for binary operator {\op} on domain {\D}}{Dop\_elt\_idempotent} +{op elt elt = elt} + + Remark: Generally useless in CIC for concrete, computable operators + + Remark: The general definition is ``exists n, iter n op x = x''. + +\itemrule{Nilpotency of element elt wrt a ring D with additive neutral +element {\zero} and multiplicative binary operator +{\op}}{Delt\_nilpotent} +{op elt elt = zero} + + Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''. + +\itemrule{Zero-product property in a ring D with additive neutral +element {\zero} and multiplicative binary operator +{\op}}{D\_integral} +{forall x y, op x y = zero -> x = zero \/ y = zero} + + Remark: We leave the ring structure of D implicit; the Coq library + uses either \texttt{\_is\_O} (for \texttt{nat}), \texttt{\_integral} + (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for + \texttt{NZ}). + + Remark: The French school says ``integrité''. + +\itemrule{Nilpotency of binary operator {\op} wrt to its absorbing element +zero in D}{Dop\_nilpotent} {forall x, op x x = zero} + + Remark: Did not find this definition on the web, but it used in + the Coq library (to characterize \name{xor}). + +\itemrule{Involutivity of unary op on D}{Dop\_involutive} +{forall x:D, op (op x) = x} + +\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the left}{Dop\_op'\_absorption\_l\_l} +{forall x y:D, op x (op' x y) = x} + +\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the right}{Dop\_op'\_absorption\_l\_r} +{forall x y:D, op x (op' y x) = x} + + Remark: Similarly for \name{Dop\_op'\_absorption\_r\_l} and \name{Dop\_op'\_absorption\_r\_r}. + +\itemrule{De Morgan law's for binary operators {\opPrime} and {\opSecond} wrt +to unary op on domain {\D}}{Dop'\_op''\_de\_morgan, +Dop''\_op'\_de\_morgan ?? \mbox{leaving the complementing operation +implicit})} +{forall x y:D, op (op' x y) = op'' (op x) (op y)\\ +forall x y:D, op (op'' x y) = op' (op x) (op y)} + +\itemrule{Left complementation of binary operator {\op} by means of unary {\opPrime} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_op'\_opp\_l} +{forall x:D, op (op' x) x = elt} + +Remark: If the name of the opposite function is reminiscent of the +notion of complement (e.g. if it is called \texttt{opp}), one can +simply say {Dop\_opp\_l}. + +\itemrule{Right complementation of binary operator {\op} by means of unary {\op'} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_opp\_r} +{forall x:D, op x (op' x) = elt} + +Example: \formula{Radd\_opp\_l: forall r : R, - r + r = 0} + +\itemrule{Associativity of binary operators {\op} and {\op'}}{Dop\_op'\_assoc} +{forall x y z, op x (op' y z) = op (op' x y) z} + +Example: \formula{forall x y z, x + (y - z) = (x + y) - z} + +\itemrule{Right extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_r} +{forall x y z, op x (op' y z) = op' (op x y) z} + +Remark: This requires {\op} and {\opPrime} to have their right and left +argument respectively and their return types identical. + +Example: \formula{forall x y z, x + (y - z) = (x + y) - z} + +Remark: Other less natural combinations are possible, such +as \formula{forall x y z, op x (op' y z) = op' y (op x z)}. + +\itemrule{Left extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_l} +{forall x y z, op (op' x y) z = op' x (op y z)} + +Remark: Operations are not necessarily internal composition laws. It +is only required that {\op} and {\opPrime} have their right and left +argument respectively and their return type identical. + +Remark: When the type are heterogeneous, only one extrusion law is possible and it can simply be named {Dop\_op'\_extrusion}. + +Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}. + +%====================================================================== +%\section{Properties of elements} + +%Remark: Not used in current library + + + +%====================================================================== +\section{Preservation and compatibility properties of operations} + +\subsection{With respect to equality} + +\itemrule{Injectivity of unary operator {\op}}{Dop\_inj} +{forall x y:D, op x = op y -> x = y} + +\itemrule{Left regularity of binary operator {\op}}{Dop\_reg\_l, Dop\_inj\_l, or Dop\_cancel\_l} +{forall x y z:D, op z x = op z y -> x = y} + + Remark: Note the order of arguments. + + Remark: The Coq usage is to called it regularity but the English + standard seems to be cancellation. The recommended form is not + decided yet. + + Remark: Shall a property like $n^p \leq n^q \rightarrow p \leq q$ + (for $n\geq 1$) be called cancellation or should it be reserved for + operators that have an inverse? + +\itemrule{Right regularity of binary operator {\op}}{Dop\_reg\_r, Dop\_inj\_r, Dop\_cancel\_r} +{forall x y z:D, op x z = op y z -> x = y} + +\subsection{With respect to a relation {\rel}} + +\itemrule{Compatibility of unary operator {\op}}{Dop\_rel\_compat} +{forall x y:D, rel x y -> rel (op x) (op y)} + +\itemrule{Left compatibility of binary operator {\op}}{Dop\_rel\_compat\_l} +{forall x y z:D, rel x y -> rel (op z x) (op z y)} + +\itemrule{Right compatibility of binary operator {\op}}{Dop\_rel\_compat\_r} +{forall x y z:D, rel x y -> rel (op x z) (op y z)} + + Remark: For equality, use names of the form \name{Dop\_eq\_compat\_l} or + \name{Dop\_eq\_compat\_r} +(\formula{forall x y z:D, y = x -> op y z = op x z} and +\formula{forall x y z:D, y = x -> op y z = op x z}) + + Remark: Should we admit (or even prefer) the name + \name{Dop\_rel\_monotone}, \name{Dop\_rel\_monotone\_l}, + \name{Dop\_rel\_monotone\_r} when {\rel} is an order ? + +\itemrule{Left regularity of binary operator {\op}}{Dop\_rel\_reg\_l} +{forall x y z:D, rel (op z x) (op z y) -> rel x y} + +\itemrule{Right regularity of binary operator {\op}}{Dop\_rel\_reg\_r} +{forall x y z:D, rel (op x z) (op y z) -> rel x y} + + Question: Would it be better to have \name{z} as first argument, since it + is missing in the conclusion ?? (or admit we shall use the options + ``\texttt{with p}''?) + +\itemrule{Left distributivity of binary operator {\op} over {\opPrime} along relation {\rel} on domain {\D}}{Dop\_op'\_rel\_distr\_l} +{forall x y z:D, rel (op (op' x y) z) (op' (op x z) (op y z))} + + Example: standard property of (not necessarily distributive) lattices + + Remark: In a (non distributive) lattice, by swapping join and meet, + one would like also, +\formula{forall x y z:D, rel (op' (op x z) (op y z)) (op (op' x y) z)}. + How to name it with a symmetric name (use + \name{Dop\_op'\_rel\_distr\_mon\_l} and + \name{Dop\_op'\_rel\_distr\_anti\_l})? + +\itemrule{Commutativity of binary operator {\op} along (equivalence) relation {\rel} on domain {\D}}{Dop\_op'\_rel\_comm} +{forall x y z:D, rel (op x y) (op y x)} + + Example: +\formula{forall l l':list A, Permutation (l++l') (l'++l)} + +\itemrule{Irreducibility of binary operator {\op} on domain {\D}}{Dop\_irreducible} +{forall x y z:D, z = op x y -> z = x $\backslash/$ z = y} + + Question: What about the constructive version ? Call it \name{Dop\_irreducible\_inf} ? +\formula{forall x y z:D, z = op x y -> \{z = x\} + \{z = y\}} + +\itemrule{Primality of binary operator {\op} along relation {\rel} on domain {\D}}{Dop\_rel\_prime} +{forall x y z:D, rel z (op x y) -> rel z x $\backslash/$ rel z y} + + +%====================================================================== +\section{Morphisms} + +\itemrule{Morphism between structures {\D} and {\D'}}{\name{D'\_of\_D}}{D -> D'} + +Remark: If the domains are one-letter long, one can used \texttt{IDD'} as for +\name{INR} or \name{INZ}. + +\itemrule{Morphism {\phimapping} mapping unary operators {\op} to {\op'}}{phi\_op\_op', phi\_op\_op'\_morphism} +{forall x:D, phi (op x) = op' (phi x)} + +Remark: If the operators have the same name in both domains, one use +\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}. + +Example: \formula{Z\_of\_nat\_mult: forall n m : nat, Z\_of\_nat (n * m) = (Z\_of\_nat n * Z\_of\_nat m)\%Z}. + +Remark: If the operators have different names on distinct domains, one +can use \texttt{op\_op'}. + +\itemrule{Morphism {\phimapping} mapping binary operators {\op} to +{\op'}}{phi\_op\_op', phi\_op\_op'\_morphism} {forall +x y:D, phi (op x y) = op' (phi x) (phi y)} + +Remark: If the operators have the same name in both domains, one use +\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}. + +Remark: If the operators have different names on distinct domains, one +can use \texttt{op\_op'}. + +\itemrule{Morphism {\phimapping} mapping binary operator {\op} to +binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism} +{forall x y:D, phi (op x y) <-> rel (phi x) (phi y)} + +Remark: If the operator and the relation have similar name, one uses +\texttt{phi\_op}. + +Question: How to name each direction? (add \_elim for -> and \_intro +for <- ?? -- as done in Bool.v ??) + +Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}. + +%====================================================================== +\section{Preservation and compatibility properties of operations wrt order} + +\itemrule{Compatibility of binary operator {\op} wrt (strict order) {\rel} and (large order) {\rel'}}{Dop\_rel\_rel'\_compat} +{forall x y z t:D, rel x y -> rel' z t -> rel (op x z) (op y t)} + +\itemrule{Compatibility of binary operator {\op} wrt (large order) {\relp} and (strict order) {\rel}}{Dop\_rel'\_rel\_compat} +{forall x y z t:D, rel' x y -> rel z t -> rel (op x z) (op y t)} + + +%====================================================================== +\section{Properties of relations} + +\itemrule{Reflexivity of relation {\rel} on domain {\D}}{Drel\_refl} +{forall x:D, rel x x} + +\itemrule{Symmetry of relation {\rel} on domain {\D}}{Drel\_sym} +{forall x y:D, rel x y -> rel y x} + +\itemrule{Transitivity of relation {\rel} on domain {\D}}{Drel\_trans} +{forall x y z:D, rel x y -> rel y z -> rel x z} + +\itemrule{Antisymmetry of relation {\rel} on domain {\D}}{Drel\_antisym} +{forall x y:D, rel x y -> rel y x -> x = y} + +\itemrule{Irreflexivity of relation {\rel} on domain {\D}}{Drel\_irrefl} +{forall x:D, \~{} rel x x} + +\itemrule{Asymmetry of relation {\rel} on domain {\D}}{Drel\_asym} +{forall x y:D, rel x y -> \~{} rel y x} + +\itemrule{Cotransitivity of relation {\rel} on domain {\D}}{Drel\_cotrans} +{forall x y z:D, rel x y -> \{rel z y\} + \{rel x z\}} + +\itemrule{Linearity of relation {\rel} on domain {\D}}{Drel\_trichotomy} +{forall x y:D, \{rel x y\} + \{x = y\} + \{rel y x\}} + + Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear}, or + \name{Drel\_connected}? Use + $\backslash/$ ? or use a ternary sumbool, or a ternary disjunction, + for nicer elimination. + +\itemrule{Informative decidability of relation {\rel} on domain {\D}}{Drel\_dec (or Drel\_dect, Drel\_dec\_inf ?)} +{forall x y:D, \{rel x y\} + \{\~{} rel x y\}} + + Remark: If equality: \name{D\_eq\_dec} or \name{D\_dec} (not like + \name{eq\_nat\_dec}) + +\itemrule{Non informative decidability of relation {\rel} on domain {\D}}{Drel\_dec\_prop (or Drel\_dec)} +{forall x y:D, rel x y $\backslash/$ \~{} rel x y} + +\itemrule{Inclusion of relation {\rel} in relation {\rel}' on domain {\D}}{Drel\_rel'\_incl (or Drel\_incl\_rel')} +{forall x y:D, rel x y -> rel' x y} + + Remark: Use \name{Drel\_rel'\_weak} for a strict inclusion ?? + +%====================================================================== +\section{Relations between properties} + +\itemrule{Equivalence of properties \texttt{P} and \texttt{Q}}{P\_Q\_iff} +{forall x1 .. xn, P <-> Q} + + Remark: Alternatively use \name{P\_iff\_Q} if it is too difficult to + recover what pertains to \texttt{P} and what pertains to \texttt{Q} + in their concatenation (as e.g. in + \texttt{Godel\_Dummett\_iff\_right\_distr\_implication\_over\_disjunction}). + +%====================================================================== +\section{Arithmetical conventions} + +\begin{minipage}{6in} +\renewcommand{\thefootnote}{\thempfootnote} % For footnotes... +\begin{tabular}{lll} +Zero on domain {\D} & D0 & (notation \verb=0=)\\ +One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\ +Successor on domain {\D} & Dsucc\\ +Predessor on domain {\D} & Dpred\\ +Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}} + & (infix notation \verb=+= [50,L])\\ +Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\ +Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ +Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\ +Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\ +Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\ +Minimal element on domain {\D} & Dmin\\ +Maximal element on domain {\D} & Dmax\\ +Large less than order on {\D} & Dle & (infix notations \verb!<=! and \verb!>=! [70,N]))\\ +Strict less than order on {\D} & Dlt & (infix notations \verb=<= and \verb=>= [70,N]))\\ +\end{tabular} +\bigskip +\end{minipage} + +\bigskip + +The status of \verb!>=! and \verb!>! is undecided yet. It will eithet +be accepted only as parsing notations or may also accepted as a {\em + definition} for the \verb!<=! and \verb! ... +\end{verbatim} +ce qui introduit un constructeur moralement équivalent à une +application situé à une priorité totalement différente (les +``bindings'' seraient au plus haut niveau alors que l'application est +à un niveau bas). + + +\begin{figure} +\begin{rulebox} +\DEFNT{binding-term} + \NT{constr} ~\TERM{with} ~\STAR{\NT{binding}} +\SEPDEF +\DEFNT{binding} + \NT{constr} +\end{rulebox} +\caption{Grammaire des bindings} +\label{bindings} +\end{figure} + +\subsection{Enregistrements} + +Il faudrait aménager la syntaxe des enregistrements dans l'optique +d'avoir des enregistrements anonymes (termes de première classe), même +si pour l'instant, on ne dispose que d'enregistrements définis a +toplevel. + +Exemple de syntaxe pour les types d'enregistrements: +\begin{verbatim} +{ x1 : A1; + x2 : A2(x1); + _ : T; (* Pas de projection disponible *) + y; (* Type infere *) + ... (* ; optionnel pour le dernier champ *) +} +\end{verbatim} + +Exemple de syntaxe pour le constructeur: +\begin{verbatim} +{ x1 = O; + x2 : A2(x1) = v1; + _ = v2; + ... +} +\end{verbatim} +Quant aux dépendences, une convention pourrait être de considérer les +champs non annotés par le type comme non dépendants. + +Plusieurs interrogations: +\begin{itemize} +\item l'ordre des champs doit-il être respecté ? + sinon, que faire pour les champs sans projection ? +\item autorise-t-on \texttt{v1} a mentionner \texttt{x1} (comme dans + la définition d'un module), ce qui se comporterait comme si on avait + écrit \texttt{v1} à la place. Cela pourrait être une autre manière + de déclarer les dépendences +\end{itemize} + +La notation pointée pour les projections pose un problème de parsing, +sauf si l'on a une convention lexicale qui discrimine les noms de +modules des projections et identificateurs: \texttt{x.y.z} peut être +compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}. + + +\section{Grammaire des termes} +\label{constrsyntax} + +\subsection{Quelques principes} + +\begin{enumerate} +\item Diminuer le nombre de niveaux de priorité en regroupant les + règles qui se ressemblent: infixes, préfixes, lieurs (constructions + ouvertes à droite), etc. +\item Éviter de surcharger la signification d'un symbole (ex: + \verb+( )+ comme parenthésage et produit dans la V7). +\item Faire en sorte que les membres gauches (motifs de Cases, lieurs + d'abstraction ou de produits) utilisent une syntaxe compatible avec + celle des membres droits (branches de Cases et corps de fonction). +\end{enumerate} + +\subsection{Présentation de la grammaire} + +\begin{figure} +\begin{rulebox} +\DEFNT{paren-constr} + \NT{cast-constr}~\TERM{,}~\NT{paren-constr} &\RNAME{pair} +\nlsep \NT{cast-constr} +\SEPDEF +\DEFNT{cast-constr} + \NT{constr}~\TERM{\!\!:}~\NT{cast-constr} &\RNAME{cast} +\nlsep \NT{constr} +\SEPDEF +\DEFNT{constr} + \NT{appl-constr}~\NT{infix}~\NT{constr} &\RNAME{infix} +\nlsep \NT{prefix}~\NT{constr} &\RNAME{prefix} +\nlsep \NT{constr}~\NT{postfix} &\RNAME{postfix} +\nlsep \NT{appl-constr} +\SEPDEF +\DEFNT{appl-constr} + \NT{appl-constr}~\PLUS{\NT{appl-arg}} &\RNAME{apply} +\nlsep \TERM{@}~\NT{global}~\PLUS{\NT{simple-constr}} &\RNAME{expl-apply} +\nlsep \NT{simple-constr} +\SEPDEF +\DEFNT{appl-arg} + \TERM{@}~\NT{int}~\TERM{\!:=}~\NT{simple-constr} &\RNAME{impl-arg} +\nlsep \NT{simple-constr} +\SEPDEF +\DEFNT{simple-constr} + \NT{atomic-constr} +\nlsep \TERM{(}~\NT{paren-constr}~\TERM{)} +\nlsep \NT{match-constr} +\nlsep \NT{fix-constr} +%% \nlsep \TERM{<\!\!:ast\!\!:<}~\NT{ast}~\TERM{>\!>} &\RNAME{quotation} +\end{rulebox} +\caption{Grammaire des termes} +\label{constr} +\end{figure} + +\begin{figure} +\begin{rulebox} +\DEFNT{prefix} + \TERM{!}~\PLUS{\NT{binder}}~\TERM{.}~ &\RNAME{prod} +\nlsep \TERM{fun} ~\PLUS{\NT{binder}} ~\TERM{$\Rightarrow$} &\RNAME{lambda} +\nlsep \TERM{let}~\NT{ident}~\STAR{\NT{binder}} ~\TERM{=}~\NT{constr} + ~\TERM{in} &\RNAME{let} +%\nlsep \TERM{let (}~\NT{comma-ident-list}~\TERM{) =}~\NT{constr} +% ~\TERM{in} &~~~\RNAME{let-case} +\nlsep \TERM{if}~\NT{constr}~\TERM{then}~\NT{constr}~\TERM{else} + &\RNAME{if-case} +\nlsep \TERM{eval}~\NT{red-fun}~\TERM{in} &\RNAME{eval} +\SEPDEF +\DEFNT{infix} + \TERM{$\rightarrow$} & \RNAME{impl} +\SEPDEF +\DEFNT{atomic-constr} + \TERM{_} +\nlsep \TERM{?}\NT{int} +\nlsep \NT{sort} +\nlsep \NT{global} +\SEPDEF +\DEFNT{binder} + \NT{ident} &\RNAME{infer} +\nlsep \TERM{(}~\NT{ident}~\NT{type}~\TERM{)} &\RNAME{binder} +\SEPDEF +\DEFNT{type} + \TERM{\!:}~\NT{constr} +\nlsep \epsilon +\end{rulebox} +\caption{Grammaires annexes aux termes} +\label{gram-annexes} +\end{figure} + +La grammaire des termes (correspondant à l'état \texttt{barestate}) +est décrite figures~\ref{constr} et~\ref{gram-annexes}. On constate +par rapport aux précédentes versions de Coq d'importants changements +de priorité, le plus marquant étant celui de l'application qui se +trouve désormais juste au dessus\footnote{La convention est de +considérer les opérateurs moins lieurs comme ``au dessus'', +c'est-à-dire ayant un niveau de priorité plus élévé (comme c'est le +cas avec le niveau de la grammaire actuelle des termes).} des +constructions fermées à gauche et à droite. + +La grammaire des noms globaux est la suivante: +\begin{eqnarray*} +\DEFNT{global} + \NT{ident} +%% \nlsep \TERM{\$}\NT{ident} +\nlsep \NT{ident}\TERM{.}\NT{global} +\end{eqnarray*} + +Le $\TERM{_}$ dénote les termes à synthétiser. Les métavariables sont +reconnues au niveau du lexer pour ne pas entrer en conflit avec le +$\TERM{?}$ de l'existentielle. + +Les opérateurs infixes ou préfixes sont tous au même niveau de +priorité du point de vue de Camlp4. La solution envisagée est de les +gérer à la manière de Yacc, avec une pile (voir discussions plus +bas). Ainsi, l'implication est un infixe normal; la quantification +universelle et le let sont vus comme des opérateurs préfixes avec un +niveau de priorité plus haut (i.e. moins lieur). Il subsiste des +problèmes si l'on ne veut pas écrire de parenthèses dans: +\begin{verbatim} + A -> (!x. B -> (let y = C in D)) +\end{verbatim} + +La solution proposée est d'analyser le membre droit d'un infixe de +manière à autoriser les préfixes et les infixes de niveau inférieur, +et d'exiger le parenthésage que pour les infixes de niveau supérieurs. + +En revanche, à l'affichage, certains membres droits seront plus +lisibles s'ils n'utilisent pas cette astuce: +\begin{verbatim} +(fun x => x) = fun x => x +\end{verbatim} + +La proposition est d'autoriser ce type d'écritures au parsing, mais +l'afficheur écrit de manière standardisée en mettant quelques +parenthèses superflues: $\TERM{=}$ serait symétrique alors que +$\rightarrow$ appellerait l'afficheur de priorité élevée pour son +sous-terme droit. + +Les priorités des opérateurs primitifs sont les suivantes (le signe +$*$ signifie que pour le membre droit les opérateurs préfixes seront +affichés sans parenthèses quel que soit leur priorité): +$$ +\begin{array}{c|l} +$symbole$ & $priorité$ \\ +\hline +\TERM{!} & 200\,R* \\ +\TERM{fun} & 200\,R* \\ +\TERM{let} & 200\,R* \\ +\TERM{if} & 200\,R \\ +\TERM{eval} & 200\,R \\ +\rightarrow & 90\,R* +\end{array} +$$ + +Il y a deux points d'entrée pour les termes: $\NT{constr}$ et +$\NT{simple-constr}$. Le premier peut être utilisé lorsqu'il est suivi +d'un séparateur particulier. Dans le cas où l'on veut une liste de +termes séparés par un espace, il faut lire des $\NT{simple-constr}$. + + + +Les constructions $\TERM{fix}$ et $\TERM{cofix}$ (voir aussi +figure~\ref{gram-fix}) sont fermées par end pour simplifier +l'analyse. Sinon, une expression de point fixe peut être suivie par un +\TERM{in} ou un \TERM{and}, ce qui pose les mêmes problèmes que le +``dangling else'': dans +\begin{verbatim} +fix f1 x {x} = fix f2 y {y} = ... and ... in ... +\end{verbatim} +il faut définir une stratégie pour associer le \TERM{and} et le +\TERM{in} au bon point fixe. + +Un autre avantage est de faire apparaitre que le \TERM{fix} est un +constructeur de terme de première classe et pas un lieur: +\begin{verbatim} +fix f1 ... and f2 ... +in f1 end x +\end{verbatim} +Les propositions précédentes laissaient \texttt{f1} et \texttt{x} +accolés, ce qui est source de confusion lorsque l'on fait par exemple +\texttt{Pattern (f1 x)}. + +Les corps de points fixes et co-points fixes sont identiques, bien que +ces derniers n'aient pas d'information de décroissance. Cela +fonctionne puisque l'annotation est optionnelle. Cela préfigure des +cas où l'on arrive à inférer quel est l'argument qui décroit +structurellement (en particulier dans le cas où il n'y a qu'un seul +argument). + +\begin{figure} +\begin{rulebox} +\DEFNT{fix-expr} + \TERM{fix}~\NT{fix-decls} ~\NT{fix-select} ~\TERM{end} &\RNAME{fix} +\nlsep \TERM{cofix}~\NT{cofix-decls}~\NT{fix-select} ~\TERM{end} &\RNAME{cofix} +\SEPDEF +\DEFNT{fix-decls} + \NT{fix-decl}~\TERM{and}~\NT{fix-decls} +\nlsep \NT{fix-decl} +\SEPDEF +\DEFNT{fix-decl} + \NT{ident}~\PLUS{\NT{binder}}~\NT{type}~\NT{annot} + ~\TERM{=}~\NT{constr} +\SEPDEF +\DEFNT{annot} + \TERM{\{}~\NT{ident}~\TERM{\}} +\nlsep \epsilon +\SEPDEF +\DEFNT{fix-select} + \TERM{in}~\NT{ident} +\nlsep \epsilon +\end{rulebox} +\caption{Grammaires annexes des points fixes} +\label{gram-fix} +\end{figure} + +La construction $\TERM{Case}$ peut-être considérée comme +obsolète. Quant au $\TERM{Match}$ de la V6, il disparaît purement et +simplement. + +\begin{figure} +\begin{rulebox} +\DEFNT{match-expr} + \TERM{match}~\NT{case-items}~\NT{case-type}~\TERM{with}~ + \NT{branches}~\TERM{end} &\RNAME{match} +\nlsep \TERM{match}~\NT{case-items}~\TERM{with}~ + \NT{branches}~\TERM{end} &\RNAME{infer-match} +%%\nlsep \TERM{case}~\NT{constr}~\NT{case-predicate}~\TERM{of}~ +%% \STAR{\NT{constr}}~\TERM{end} &\RNAME{case} +\SEPDEF +\DEFNT{case-items} + \NT{case-item} ~\TERM{\&} ~\NT{case-items} +\nlsep \NT{case-item} +\SEPDEF +\DEFNT{case-item} + \NT{constr}~\NT{pred-pattern} &\RNAME{dep-case} +\nlsep \NT{constr} &\RNAME{nodep-case} +\SEPDEF +\DEFNT{case-type} + \TERM{$\Rightarrow$}~\NT{constr} +\nlsep \epsilon +\SEPDEF +\DEFNT{pred-pattern} + \TERM{as}~\NT{ident} ~\TERM{\!:}~\NT{constr} +\SEPDEF +\DEFNT{branches} + \TERM{|} ~\NT{patterns} ~\TERM{$\Rightarrow$} + ~\NT{constr} ~\NT{branches} +\nlsep \epsilon +\SEPDEF +\DEFNT{patterns} + \NT{pattern} ~\TERM{\&} ~\NT{patterns} +\nlsep \NT{pattern} +\SEPDEF +\DEFNT{pattern} ... +\end{rulebox} +\caption{Grammaires annexes du filtrage} +\label{gram-match} +\end{figure} + +De manière globale, l'introduction de définitions dans les termes se +fait avec le symbole $=$, et le $\!:=$ est réservé aux définitions au +niveau vernac. Il y avait un manque de cohérence dans la +V6, puisque l'on utilisait $=$ pour le $\TERM{let}$ et $\!:=$ pour les +points fixes et les commandes vernac. + +% OBSOLETE: lieurs multiples supprimes +%On peut remarquer que $\NT{binder}$ est un sous-ensemble de +%$\NT{simple-constr}$, à l'exception de $\texttt{(a,b\!\!:T)}$: en tant +%que lieur, {\tt a} et {\tt b} sont tous deux contraints, alors qu'en +%tant que terme, seul {\tt b} l'est. Cela qui signifie que l'objectif +%de rendre compatibles les membres gauches et droits est {\it presque} +%atteint. + +\subsection{Infixes} + +\subsubsection{Infixes extensibles} + +Le problème de savoir si la liste des symboles pouvant apparaître en +infixe est fixée ou extensible par l'utilisateur reste à voir. + +Notons que la solution où les symboles infixes sont des +identificateurs que l'on peut définir paraît difficilement praticable: +par exemple $\texttt{Logic.eq}$ n'est pas un opérateur binaire, mais +ternaire. Il semble plus simple de garder des déclarations infixes qui +relient un symbole infixe à un terme avec deux ``trous''. Par exemple: + +$$\begin{array}{c|l} +$infixe$ & $identificateur$ \\ +\hline += & \texttt{Logic.eq _ ?1 ?2} \\ +== & \texttt{JohnMajor.eq _ ?1 _ ?2} +\end{array}$$ + +La syntaxe d'une déclaration d'infixe serait par exemple: +\begin{verbatim} +Infix "=" 50 := Logic.eq _ ?1 ?2; +\end{verbatim} + + +\subsubsection{Gestion des précédences} + +Les infixes peuvent être soit laissé à Camlp4, ou bien (comme ici) +considérer que tous les opérateurs ont la même précédence et gérer +soit même la recomposition des termes à l'aide d'une pile (comme +Yacc). + + +\subsection{Extensions de syntaxe} + +\subsubsection{Litéraux numériques} + +La proposition est de considerer les litéraux numériques comme de +simples identificateurs. Comme il en existe une infinité, il faut un +nouveau mécanisme pour leur associer une définition. Par exemple, en +ce qui concerne \texttt{Arith}, la définition de $5$ serait +$\texttt{S}~4$. Pour \texttt{ZArith}, $5$ serait $\texttt{xI}~2$. + +Comme les infixes, les constantes numériques peuvent être qualifiées +pour indiquer dans quels module est le type que l'on veut +référencer. Par exemple (si on renomme \texttt{Arith} en \texttt{N} et +\texttt{ZArith} en \texttt{Z}): \verb+N.5+, \verb+Z.5+. + +\begin{eqnarray*} +\EXTNT{global} + \NT{int} +\end{eqnarray*} + +\subsubsection{Nouveaux lieurs} + +$$ +\begin{array}{rclr} +\EXTNT{constr} + \TERM{ex}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr} &\RNAME{ex} +\nlsep \TERM{ex}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}~\TERM{,}~\NT{constr} + &\RNAME{ex2} +\nlsep \TERM{ext}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr} &\RNAME{exT} +\nlsep \TERM{ext}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}~\TERM{,}~\NT{constr} + &\RNAME{exT2} +\end{array} +$$ + +Pour l'instant l'existentielle n'admet qu'une seule variable, ce qui +oblige à écrire des cascades de $\TERM{ex}$. + +Pour parser les existentielles avec deux prédicats, on peut considérer +\TERM{\&} comme un infixe intermédiaire et l'opérateur existentiel en +présence de cet infixe se transforme en \texttt{ex2}. + +\subsubsection{Nouveaux infixes} + +Précédences des opérateurs infixes (les plus grands associent moins fort): +$$ +\begin{array}{l|l|c|l} +$identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ +\hline +\texttt{iff} & $Logic$ & \longleftrightarrow & 100 \\ +\texttt{or} & $Logic$ & \vee & 80\, R \\ +\texttt{sum} & $Datatypes$ & + & 80\, R \\ +\texttt{and} & $Logic$ & \wedge & 70\, R \\ +\texttt{prod} & $Datatypes$ & * & 70\, R \\ +\texttt{not} & $Logic$ & \tilde{} & 60\, L \\ +\texttt{eq _} & $Logic$ & = & 50 \\ +\texttt{eqT _} & $Logic_Type$ & = & 50 \\ +\texttt{identityT _} & $Data_Type$ & = & 50 \\ +\texttt{le} & $Peano$ & $<=$ & 50 \\ +\texttt{lt} & $Peano$ & $<$ & 50 \\ +\texttt{ge} & $Peano$ & $>=$ & 50 \\ +\texttt{gt} & $Peano$ & $>$ & 50 \\ +\texttt{Zle} & $zarith_aux$ & $<=$ & 50 \\ +\texttt{Zlt} & $zarith_aux$ & $<$ & 50 \\ +\texttt{Zge} & $zarith_aux$ & $>=$ & 50 \\ +\texttt{Zgt} & $zarith_aux$ & $>$ & 50 \\ +\texttt{Rle} & $Rdefinitions$ & $<=$ & 50 \\ +\texttt{Rlt} & $Rdefinitions$ & $<$ & 50 \\ +\texttt{Rge} & $Rdefinitions$ & $>=$ & 50 \\ +\texttt{Rgt} & $Rdefinitions$ & $>$ & 50 \\ +\texttt{plus} & $Peano$ & + & 40\,L \\ +\texttt{Zplus} & $fast_integer$ & + & 40\,L \\ +\texttt{Rplus} & $Rdefinitions$ & + & 40\,L \\ +\texttt{minus} & $Minus$ & - & 40\,L \\ +\texttt{Zminus} & $zarith_aux$ & - & 40\,L \\ +\texttt{Rminus} & $Rdefinitions$ & - & 40\,L \\ +\texttt{Zopp} & $fast_integer$ & - & 40\,L \\ +\texttt{Ropp} & $Rdefinitions$ & - & 40\,L \\ +\texttt{mult} & $Peano$ & * & 30\,L \\ +\texttt{Zmult} & $fast_integer$ & * & 30\,L \\ +\texttt{Rmult} & $Rdefinitions$ & * & 30\,L \\ +\texttt{Rdiv} & $Rdefinitions$ & / & 30\,L \\ +\texttt{pow} & $Rfunctions$ & \hat & 20\,L \\ +\texttt{fact} & $Rfunctions$ & ! & 20\,L \\ +\end{array} +$$ + +Notons qu'il faudrait découper {\tt Logic_Type} en deux car celui-ci +définit deux égalités, ou alors les mettre dans des modules différents. + +\subsection{Exemples} + +\begin{verbatim} +Definition not (A:Prop) := A->False; +Inductive eq (A:Set) (x:A) : A->Prop := + refl_equal : eq A x x; +Inductive ex (A:Set) (P:A->Prop) : Prop := + ex_intro : !x. P x -> ex A P; +Lemma not_all_ex_not : !(P:U->Prop). ~(!n. P n) -> ?n. ~ P n; +Fixpoint plus n m : nat {struct n} := + match n with + O => m + | (S k) => S (plus k m) + end; +\end{verbatim} + +\subsection{Questions ouvertes} + +Voici les points sur lesquels la discussion est particulièrement +ouverte: +\begin{itemize} +\item choix d'autres symboles pour les quantificateurs \TERM{!} et + \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!} + pour la qunatification universelle, mais on choisirait quelquechose + comme \TERM{ex} pour l'existentielle, afin de ne pas suggérer trop + de symétrie entre ces quantificateurs (l'un est primitif, l'autre + pas). +\item syntaxe particulière pour les \texttt{sig}, \texttt{sumor}, etc. +\item la possibilité d'introduire plusieurs variables du même type est + pour l'instant supprimée au vu des problèmes de compatibilité de + syntaxe entre les membres gauches et membres droits. L'idée étant + que l'inference de type permet d'éviter le besoin de déclarer tous + les types. +\end{itemize} + +\subsection{Autres extensions} + +\subsubsection{Lieur multiple} + +L'écriture de types en présence de polymorphisme est souvent assez +pénible: +\begin{verbatim} +Check !(A:Set) (x:A) (B:Set) (y:B). P A x B y; +\end{verbatim} + +On pourrait avoir des déclarations introduisant à la fois un type +d'une certaine sorte et une variable de ce type: +\begin{verbatim} +Check !(x:A:Set) (y:B:Set). P A x B y; +\end{verbatim} + +Noter que l'on aurait pu écrire: +\begin{verbatim} +Check !A x B y. P A (x:A:Set) B (y:B:Set); +\end{verbatim} + +\section{Syntaxe des tactiques} + +\subsection{Questions diverses} + +Changer ``Pattern nl c ... nl c'' en ``Pattern [ nl ] c ... [ nl ] c'' +pour permettre des chiffres seuls dans la catégorie syntaxique des +termes. + +Par uniformité remplacer ``Unfold nl c'' par ``Unfold [ nl ] c'' ? + +Même problème pour l'entier de Specialize (ou virer Specialize ?) ? + +\subsection{Questions en suspens} + +\verb=EAuto= : deux syntaxes différentes pour la recherche en largeur +et en profondeur ? Quelle recherche par défaut ? + +\section*{Remarques pêle-mêle (HH)} + +Autoriser la syntaxe + +\begin{verbatim} +Variable R (a : A) (b : B) : Prop. +Hypotheses H (a : A) (b : B) : Prop; Y (u : U) : V. +Variables H (a : A) (b : B), J (k : K) : nat; Z (v : V) : Set. +\end{verbatim} + +Renommer eqT, refl_eqT, eqT_ind, eqT_rect, eqT_rec en eq, refl_equal, etc. +Remplacer == en =. + +Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ?? + +\section{Moulinette} + +\begin{itemize} + +\item Mettre \verb=/= et * au même niveau dans R. + +\item Changer la précédence du - unaire dans R. + +\item Ajouter Require Arith par necessite si Require ArithRing ou Require ZArithRing. + +\item Ajouter Require ZArith par necessite si Require ZArithRing ou Require Omega. + +\item Enlever le Export de Bool, Arith et ZARith de Ring quand inapproprié et +l'ajouter à côté des Require Ring. + +\item Remplacer "Check n" par "n:Check ..." + +\item Renommer Variable/Hypothesis hors section en Parameter/Axiom. + +\item Renommer les \verb=command0=, \verb=command1=, ... \verb=lcommand= etc en +\verb=constr0=, \verb=constr1=, ... \verb=lconstr=. + +\item Remplacer les noms Coq.omega.Omega par Coq.Omega ... + +\item Remplacer AddPath par Add LoadPath (ou + court) + +\item Unify + and \{\}+\{\} and +\{\} using Prop $\leq$ Set ?? + +\item Remplacer Implicit Arguments On/Off par Set/Unset Implicit Arguments. + +\item La syntaxe \verb=Intros (a,b)= est inutile, \verb=Intros [a b]= fait l'affaire. + +\item Virer \verb=Goal= sans argument (synonyme de \verb=Proof= et sans effets). + +\item Remplacer Save. par Qed. + +\item Remplacer \verb=Zmult_Zplus_distr= par \verb=Zmult_plus_distr_r= +et \verb=Zmult_plus_distr= par \verb=Zmult_plus_distr_l=. + +\end{itemize} + +\end{document} diff --git a/dev/doc/archive/notes-on-conversion.v b/dev/doc/archive/notes-on-conversion.v new file mode 100644 index 0000000000..a78ecd181a --- /dev/null +++ b/dev/doc/archive/notes-on-conversion.v @@ -0,0 +1,71 @@ +(**********************************************************************) +(* A few examples showing the current limits of the conversion algorithm *) +(**********************************************************************) + +(*** We define (pseudo-)divergence from Ackermann function ***) + +Definition ack (n : nat) := + (fix F (n0 : nat) : nat -> nat := + match n0 with + | O => S + | S n1 => + fun m : nat => + (fix F0 (n2 : nat) : nat := + match n2 with + | O => F n1 1 + | S n3 => F n1 (F0 n3) + end) m + end) n. + +Notation OMEGA := (ack 4 4). + +Definition f (x:nat) := x. + +(* Evaluation in tactics can somehow be controlled *) +Lemma l1 : OMEGA = OMEGA. +reflexivity. (* succeed: identity *) +Qed. (* succeed: identity *) + +Lemma l2 : OMEGA = f OMEGA. +reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) +Abort. (* but it reduces the right side first! *) + +Lemma l3 : f OMEGA = OMEGA. +reflexivity. (* succeed: reduce left side first *) +Qed. (* succeed: expected concl (the one with f) is on the left *) + +Lemma l4 : OMEGA = OMEGA. +assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) +unfold f in H. (* succeed: no type-checking *) +exact H. (* succeed: identity *) +Qed. (* fail: "f" is on the left *) + +(* This example would fail whatever the preferred side is *) +Lemma l5 : OMEGA = f OMEGA. +unfold f. +assert (f OMEGA = OMEGA) by reflexivity. +unfold f in H. +exact H. +Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) + +(**********************************************************************) +(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) +(* (proof of span_ind_uninject_prop *) + +In the proof, a problem of the form (Equal S t1 t2) +is "simpl"ified, then "red"uced to (Equal S' t1 t1) +where the new t1's are surrounded by invisible coercions. +A reflexivity steps conclude the proof. + +The trick is that Equal projects the equality in the setoid S, and +that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). + +At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) +and the algorithm is to first compare S and S', and t1 and t2. +Unfortunately it does not work, and since t1 and t2 involve concrete +instances of algebraic structures, it takes a lot of time to realize that +it is not convertible. + +The only hope to improve this problem is to observe that S' hides +(behind two indirections) a Setoid constructor. This could be the +argument to solve the problem. diff --git a/dev/doc/archive/old_svn_branches.txt b/dev/doc/archive/old_svn_branches.txt new file mode 100644 index 0000000000..ee56ee24e9 --- /dev/null +++ b/dev/doc/archive/old_svn_branches.txt @@ -0,0 +1,33 @@ +## During the migration to git, some old branches and tags have not been +## converted to directly visible git branches or tags. They are still there +## in the archive, their names on the gforge repository are in the 3rd +## column below (e.g. remotes/V8-0-bugfix). After a git clone, they +## could always be accessed by their git hashref (2nd column below). + +# SVN # GIT # Symbolic name on gforge repository + +r5 d2f789d remotes/tags/start +r1714 0605b7c remotes/V7 +r2583 372f3f0 remotes/tags/modules-2-branching +r2603 6e15d9a remotes/modules +r2866 76a93fa remotes/tags/modules-2-before-grammar +r2951 356f749 remotes/tags/before-modules +r2952 8ee67df remotes/tags/modules-2-update +r2956 fb11bd9 remotes/modules-2 +r3193 4d23172 remotes/mowgli +r3194 c91e99b remotes/tags/mowgli-before-merge +r3500 5078d29 remotes/mowgli2 +r3672 63b0886 remotes/V7-3-bugfix +r5086 bdceb72 remotes/V7-4-bugfix +r5731 a274456 remotes/recriture +r9046 e19553c remotes/tags/trunk +r9146 b38ce05 remotes/coq-diff-tool +r9786 a05abf8 remotes/ProofIrrelevance +r10294 fdf8871 remotes/InternalExtraction +r10408 df97909 remotes/TypeClasses +r10673 4e19bca remotes/bertot +r11130 bfd1cb3 remotes/proofs +r12282 a726b30 remotes/revised-theories +r13855 bae3a8e remotes/native +r14062 b77191b remotes/recdef +r16421 9f4bfa8 remotes/V8-0-bugfix diff --git a/dev/doc/archive/perf-analysis b/dev/doc/archive/perf-analysis new file mode 100644 index 0000000000..ac54fa6f73 --- /dev/null +++ b/dev/doc/archive/perf-analysis @@ -0,0 +1,167 @@ +Performance analysis (trunk repository) +--------------------------------------- + +Jun 7, 2010: delayed re-typing of Ltac instances in matching + (-1% on HighSchoolGeometry, -2% on JordanCurveTheorem) + +Jun 4, 2010: improvement in eauto and type classes inference by removing + systematic preparation of debugging pretty-printing streams (std_ppcmds) + (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk; + -6% in HighSchoolGeometry) + +Apr 19, 2010: small improvement obtained by reducing evar instantiation + from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert, + -2% AreaMethod, -15% in Ssreflect) + +Apr 17, 2010: small improvement obtained by not repeating unification + twice in auto (-2% in Compcert, -2% in Algebra) + +Feb 15, 2010: Global decrease due to unicode inefficiency repaired + +Jan 8, 2010: Global increase due to an inefficiency in unicode treatment + +Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to + exact (generally not significative but, e.g., +25% on Subst, +8% on + ZFC, +5% on AreaMethod) + +Oct 19, 2009: Change in modules (CoLoR +35%) + +Aug 9, 2009: new files added in AreaMethod + +May 21, 2008: New version of CoRN + (needs +84% more time to compile) + +Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu) + (+28% CoRN) + +Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug + fixes, control of zeta in rewrite, auto (??)) + (-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg, + but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%) + +Mar 11, 2008: + (+19% PersistentUnionFind wrt Mar 3, +21% Angles, + +270% Continuations between 7/3 and 18/4) + +Mar 7, 2008: + (-10% PersistentUnionFind wrt Mar 3) + +Feb 20, 2008: temporary 1-day slow down + (+64% LinAlg) + +Feb 14, 2008: + (-10% PersistentUnionFind, -19% Groups) + +Feb 7, 8, 2008: temporary 2-days long slow down + (+20 LinAlg, +50% BDDs) + +Feb 2, 2008: many updates of the module system + (-13% LinAlg, -50% AMM11262, -5% Goedel, -1% PersistentUnionFind, + -42% ExactRealArithmetic, -41% Icharate, -42% Kildall, -74% SquareMatrices) + +Jan 1, 2008: merge of TypeClasses branch + (+8% PersistentUnionFind, +36% LinAlg, +76% Goedel) + +Nov 16, 17, 2007: + (+18% Cantor, +4% LinAlg, +27% IEEE1394 on 2 days) + +Nov 8, 2007: + (+18% Cantor, +16% LinAlg, +55% Continuations, +200% IEEE1394, +170% CTLTCTL, + +220% SquareMatrices) + +Oct 29, V8.1 (+ 3% geometry but CoRN, Godel, Kildall, Stalmark stables) + +Between Oct 12 and Oct 27, 2007: inefficiency temporarily introduced in the + tactic interpreter (from revision 10222 to 10267) + (+22% CoRN, +10% geometry, ...) + +Sep 16, 2007: + (+16% PersistentUnionFind on 3 days, LinAlg stable, + +Sep 4, 2007: + (+26% PersistentUnionFind, LinAlg stable, + +Jun 6, 2007: optimization of the need for type unification in with-bindings + (-3.5% Stalmark, -6% Kildall) + +May 20, 21, 22, 2007: improved inference of with-bindings (including activation + of unification on types) + (+4% PICALC, +5% Stalmark, +7% Kildall) + +May 11, 2007: added primitive integers (+6% CoLoR, +7% CoRN, +5% FSets, ...) + +Between Feb 22 and March 16, 2007: bench temporarily moved on JMN's + computer (-25% CoRN, -25% Fairisle, ...) + +Oct 29 and Oct 30, 2006: abandoned attempt to add polymorphism on definitions + (+4% in general during these two days) + +Oct 17, 2006: improvement in new field [r9248] + (QArith -3%, geometry: -2%) + +Oct 5, 2006: fixing wrong unification of Meta below binders + (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, LinAlg: +7%, + DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%) + +Sep 26, 2006: new field [r9178-9181] + (QArith: -16%, geometry: -5%, Float: +6%, BDDS:+5% but no ring in it) + + Sep 12, 2006: Rocq/AREA_METHOD extended (~ 530s) + Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s) + May 30, 2006: Nancy/CoLoR added (~ 319s) + +May 23, 2006: new, lighter version of polymorphic inductive types + (CoRN: -27%, back to Mar-24 time) + +May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -) + +May 5, 2006: improvement in closure (array instead of lists) + (e.g. CatsInZFC: -10%, CoRN: -3%, + +May 23, 2006: polymorphic inductive types (precise, heavy algorithm) + (CoRN: +37%) + + Dec 29, 2005: new test and use of -vm in Stalmarck + + Dec 27, 2005: contrib Karatsuba added (~ 30s) + +Dec 28, 2005: size decrease + mainly due to Defined moved to Qed in FSets (reduction from 95M to 7Mo) + +Dec 1-14, 2005: benchmarking server down + between the two dates: Godel: -10%, CoRN: -10% + probably due to changes around vm (new informative Cast, + change of equality in named_context_val) + + Oct 6, 2005: contribs IPC and Tait added (~ 22s and ~ 25s) + +Aug 19, 2005: time decrease after application of "Array.length x=0" Xavier's + suggestions for optimisation + (e.g. Nijmegen/QArith: -3%, Nijmegen/CoRN: -7%, Godel: -3%) + + Aug 1, 2005: contrib Kildall added (~ 65s) + +Jul 26-Aug 2, 2005: bench down + +Jul 14-15, 2005: 4 contribs failed including CoRN + +Jul 14, 2005: time increase after activation of "closure optimisation" + (e.g. Nijmegen/QArith: +8%, Nijmegen/CoRN: +3%, Godel: +13%) + + Jul 7, 2005: adding contrib Fermat4 + + Jun 17, 2005: contrib Goodstein extended and moved to CantorOrdinals (~ 30s) + + May 19, 2005: contrib Goodstein and prfx (~ 9s) added + +Apr 21, 2005: strange time decrease + (could it be due to the change of Back and Reset mechanism) + (e.g. Nijmegen/CoRN: -2%, Nijmegen/QARITH: -4%, Godel: -11%) + +Mar 20, 2005: fixed Logic.with_check bug + global time decrease (e.g. Nijmegen/CoRN: -3%, Nijmegen/QARITH: -1.5%) + +Jan 31-Feb 8, 2005: small instability + (e.g. CoRN: ~2015s -> ~1999s -> ~2032s, Godel: ~340s -> ~370s) + + Jan 13, 2005: contrib SumOfTwoSquare added (~ 38s) diff --git a/dev/doc/archive/versions-history.tex b/dev/doc/archive/versions-history.tex new file mode 100644 index 0000000000..25dabad497 --- /dev/null +++ b/dev/doc/archive/versions-history.tex @@ -0,0 +1,451 @@ +\documentclass[a4paper]{book} +\usepackage{fullpage} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{amsfonts} + +\newcommand{\feature}[1]{{\em #1}} + +\begin{document} + +\begin{center} +\begin{huge} +A history of Coq versions +\end{huge} +\end{center} +\bigskip + +\centerline{\large 1984-1989: The Calculus of Constructions} + +\bigskip +\centerline{\large (see README.V1-V5 for details)} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline + +CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\ + & 1984 to 13 February 1985 & \feature{of Constructions}, implementation \\ + & frozen 22 December 1984 & language is a predecessor of CAML\\ + +CONSTR V1.11& mention of dates from 6 December\\ + & 1984 to 19 February 1985 (freeze date) &\\ + +CoC V2.8& dated 16 December 1985 (freeze date)\\ + +CoC V2.9& & \feature{cumulative hierarchy of universes}\\ + +CoC V2.13& dated 25 June 1986 (freeze date)\\ + +CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\ + & dated 20 November 1986 & implementation language now named CAML\\ + +CoC V3.2& dated 27 November 1986\\ + +CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\ + +CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\ + +CoC V4.1& dated 24 July 1987 (freeze date)\\ + +CoC V4.2& dated 10 September 1987\\ + +CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\ + & frozen November 1987 & \feature{section mechanism}\\ + & & \feature{logical vs computational content (sorte Spec)}\\ + & & \feature{LCF engine}\\ + +CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\ + & frozen March 1988\\ + +CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\ + & demonstrated in June 1988\\ + +CoC V4.6& dated 1 September 1988 & start of LEGO fork\\ + +CoC V4.7& started 6 September 1988 \\ + +CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\ + +CoC V4.8.5& dated 1 February 1989 & \\ + +CoC V4.9& dated 1 March 1989 (release date)\\ + +CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\ +\end{tabular} + +\bigskip + +\noindent Note: CoC above stands as an abbreviation for {\em Calculus of + Constructions}, official name of the system. +\bigskip +\bigskip + +\newpage + +\centerline{\large 1989-now: The Calculus of Inductive Constructions} +\mbox{}\\ +\centerline{I- RCS archives in Caml and Caml-Light} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq V5.0 & headers dated 1 January 1990 & internal use \\ + & & \feature{inductive types with primitive recursor}\\ + +Coq V5.1 & ended 12 July 1990 & internal use \\ + +Coq V5.2 & log dated 4 October 1990 & internal use \\ + +Coq V5.3 & log dated 12 October 1990 & internal use \\ + +Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\ + +Coq V5.5 & started 6 December 1990 & internal use \\ + +Coq V5.6 beta & 1991 & first announce of the new Coq based on CIC \\ + & & (in May at TYPES?)\\ + & & \feature{rewrite tactic}\\ + & & use of RCS at least from February 1991\\ + +Coq V5.6& 7 August 1991 & \\ + +Coq V5.6 patch 1& 13 November 1991 & \\ + +Coq V5.6 (last) & mention of 27 November 1992\\ + +Coq V5.7.0& 1992 & translation to Caml-Light \footnotemark\\ + +Coq V5.8& 12 February 1993 & \feature{Program} (version 1), \feature{simpl}\\ + +& & has the xcoq graphical interface\\ + +& & first explicit notion of standard library\\ + +& & includes a MacOS 7-9 version\\ + +Coq V5.8.1& released 28 April 1993 & with xcoq graphical interface and MacOS 7-9 support\\ + +Coq V5.8.2& released 9 July 1993 & with xcoq graphical interface and MacOS 7-9 support\\ + +Coq V5.8.3& released 6 December 1993 % Announce on coq-club + & with xcoq graphical interface and MacOS 7-9 support\\ + + & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\ + +Coq V5.9 alpha& 7 July 1993 & +experimental version based on evars refinement \\ + & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\ + & & version), not released\\ + +& March 1994 & \feature{tauto} tactic in V5.9 branch\\ + +Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\ + & & not released\\ +\end{tabular} + +\bigskip +\bigskip + +\footnotetext{archive lost?} + +\newpage + +\centerline{II- Starting with CVS archives in Caml-Light} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq V5.10 ``Murthy'' & 22 January 1994 & +introduction of the ``DOPN'' structure\\ + & & \feature{eapply/prolog} tactics\\ + & & private use of cvs on madiran.inria.fr\\ + +Coq V5.10.1 ``Murthy''& 15 April 1994 \\ + +Coq V5.10.2 ``Murthy''& 19 April 1994 & \feature{mutual inductive types, fixpoint} (from Lyon's branch)\\ + +Coq V5.10.3& 28 April 1994 \\ + +Coq V5.10.5& dated 13 May 1994 & \feature{inversion}, \feature{discriminate}, \feature{injection} \\ + & & \feature{type synthesis of hidden arguments}\\ + & & \feature{separate compilation}, \feature{reset mechanism} \\ + +Coq V5.10.6& dated 30 May 1994\\ +Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\ + +Coq V5.10.9& announced on 17 August 1994 & + % Announced by Catherine Parent on coqdev + % Version avec une copie de THEORIES pour les inductifs mutuels + \\ + +Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\ +Coq Rocq's archive & on 16 February 1995 & set up of ``V5.10'' cvs archive on pauillac.inria.fr \\ + & & with first dispatch of files over src/* directories\\ + +Coq V5.10.12& dated 30 January 1995 & on Lyon's cvs\\ + +Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\ + +Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\ + +Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW + +Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\ + & & MS-DOS version released on 30 October 1995\\ + % still available at ftp://ftp.ens-lyon.fr/pub/LIP/COQ/V5.10.14.old/ in May 2009 + % also known in /net/pauillac/constr archive as ``V5.11 old'' \\ + % A copy of Coq V5.10.15 dated 1 January 1996 coming from Lyon's CVS is + % known in /net/pauillac/constr archive as ``V5.11 new old'' \\ + +Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\ + % Announce on coq-club by BW + % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive + & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW + +Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\ +\end{tabular} + +\bigskip +\bigskip + +\newpage + +\centerline{III- A CVS archive in Caml Special Light} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\ + & & to Caml Special Light (to later become Objective Caml)\\ + & & has implicit arguments and coercions\\ + & & has coinductive types\\ + +Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\ + & & \feature{omega} [10-9-1996] \\ + & & \feature{natural language proof printing} (stopped from Coq V7) [6-9-1996]\\ + & & \feature{pattern-matching compilation} [7-10-1996]\\ + & & \feature{ring} (version 1, ACSimpl) [11-12-1996]\\ + +Coq V6.1& released December 1996 & \\ + +Coq V6.2beta& released 30 January 1998 & % Announced on coq-club 2-2-1998 by CP + \feature{SearchIsos} (stopped from Coq V7) [9-11-1997]\\ + & & grammar extension mechanism moved to Camlp4 [12-6-1997]\\ + & & \feature{refine tactic}\\ + & & includes a Windows version\\ + +Coq V6.2& released 4 May 1998 & % Announced on coq-club 5-5-1998 by CP + \feature{ring} (version 2) [7-4-1998] \\ + +Coq V6.2.1& released 23 July 1998\\ + +Coq V6.2.2 beta& released 30 January 1998\\ + +Coq V6.2.2& released 23 September 1998\\ + +Coq V6.2.3& released 22 December 1998 & \feature{Real numbers library} [from 13-11-1998] \\ + +Coq V6.2.4& released 8 February 1999\\ + +Coq V6.3& released 27 July 1999 & \feature{autorewrite} [25-3-1999]\\ + & & \feature{Correctness} (deprecated in V8, led to Why) [28-10-1997]\\ + +Coq V6.3.1& released 7 December 1999\\ +\end{tabular} +\medskip +\bigskip + +\newpage +\centerline{IV- New CVS, back to a kernel-centric implementation} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\ + & & \feature{kernel-centric} architecture \\ + & & more care for outside readers\\ + & & (indentation, ocaml warning protection)\\ +Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\ +Coq V7.0beta2& released 2 February 2001\\ + +Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\ + & & \feature{field} (version 1) [19-4-2001], \feature{fourier} [20-4-2001] \\ + +Coq V7.1& released 25 September 2001 & \feature{setoid rewriting} (version 1) [10-7-2001]\\ + +Coq V7.2& released 10 January 2002\\ + +Coq V7.3& released 16 May 2002\\ + +Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\ + & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\ + +Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\ +\end{tabular} + +\medskip +\bigskip + +\centerline{V- New concrete syntax} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\ + +Coq V8.0pl1& released 18 July 2004\\ + +Coq V8.0pl2& released 22 January 2005\\ + +Coq V8.0pl3& released 13 January 2006\\ + +Coq V8.0pl4& released 26 January 2007\\ + +Coq ``svn'' archive & 6 March 2006 & cvs archive moved to subversion control management\\ + +Coq V8.1beta& released 12 July 2006 & \feature{bytecode compiler} [20-10-2004] \\ + & & \feature{setoid rewriting} (version 2) [3-9-2004]\\ + & & \feature{functional induction} [1-2-2006]\\ + & & \feature{Strings library} [8-2-2006], \feature{FSets/FMaps library} [15-3-2006] \\ + & & \feature{Program} (version 2, Russell) [5-3-2006] \\ + & & \feature{declarative language} [20-9-2006]\\ + & & \feature{ring} (version 3) [18-11-2005]\\ + +Coq V8.1gamma& released 7 November 2006 & \feature{field} (version 2) [29-9-2006]\\ + +Coq V8.1& released 10 February 2007 & \\ + +Coq V8.1pl1& released 27 July 2007 & \\ +Coq V8.1pl2& released 13 October 2007 & \\ +Coq V8.1pl3& released 13 December 2007 & \\ +Coq V8.1pl4& released 9 October 2008 & \\ + +Coq V8.2 beta1& released 13 June 2008 & \\ +Coq V8.2 beta2& released 19 June 2008 & \\ +Coq V8.2 beta3& released 27 June 2008 & \\ +Coq V8.2 beta4& released 8 August 2008 & \\ + +Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \feature{machine words} [11-5-2007]\\ + & & \feature{big integers} [11-5-2007], \feature{abstract arithmetics} [9-2007]\\ + & & \feature{setoid rewriting} (version 3) [18-12-2007] \\ + & & \feature{micromega solving platform} [19-5-2008]\\ + +& & a first package released on +February 11 was incomplete\\ +Coq V8.2pl1& released 4 July 2009 & \\ +Coq V8.2pl2& released 29 June 2010 & \\ +\end{tabular} + +\medskip +\bigskip + +\newpage +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\ +Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\ +Coq V8.3pl1& released 23 December 2010 & \\ +Coq V8.3pl2& released 19 April 2011 & \\ +Coq V8.3pl3& released 19 December 2011 & \\ +Coq V8.3pl3& released 26 March 2012 & \\ +Coq V8.3pl5& released 28 September 2012 & \\ +Coq V8.4 beta & released 27 December 2011 & \feature{modular arithmetic library} [2010-2012]\\ +&& \feature{vector library} [10-12-2010]\\ +&& \feature{structured scripts} [22-4-2010]\\ +&& \feature{eta-conversion} [20-9-2010]\\ +&& \feature{new proof engine available} [10-12-2010]\\ +Coq V8.4 beta2 & released 21 May 2012 & \\ +Coq V8.4 & released 12 August 2012 &\\ +Coq V8.4pl1& released 22 December 2012 & \\ +Coq V8.4pl2& released 4 April 2013 & \\ +Coq V8.4pl3& released 21 December 2013 & \\ +Coq V8.4pl4& released 24 April 2014 & \\ +Coq V8.4pl5& released 22 October 2014 & \\ +Coq V8.4pl6& released 9 April 2015 & \\ + +Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ +&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{new proof engine deployed} [2-11-2013]\\ +&& \feature{universe polymorphism} [6-5-2014]\\ +&& \feature{primitive projections} [6-5-2014]\\ +&& \feature{miscellaneous optimizations}\\ + +Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ + +Coq V8.5 & released 22 January 2016 & \\ + +Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\ +&& \feature{Ltac profiling} [14-6-2016]\\ +&& \feature{warning system} [29-6-2016]\\ +&& \feature{miscellaneous optimizations}\\ + +Coq V8.6 & released 14 December 2016 & \\ + +Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\ +&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\ +&& \feature{further optimizations}\\ + +Coq V8.7 beta 2 & released 6 October 2017 & \\ + +Coq V8.7.0 & released 18 October 2017 & \\ + +Coq V8.7.1 & released 15 December 2017 & \\ + +Coq V8.7.2 & released 17 February 2018 & \\ + +Coq V8.8 beta1 & released 19 March 2018 & \\ + +Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\ +&& \feature{effort towards better documented, better structured ML API}\\ +&& \feature{miscellaneous changes/improvements of existing features}\\ + +\end{tabular} + +\medskip +\bigskip +\newpage + +\centerline{\large Other important dates} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Lechenadec's version in C& mention of \\ + & 13 January 1985 on \\ + & some vernacular files\\ +Set up of the coq-club mailing list & 28 July 1993\\ + +Coq V6.0 ``evars'' & & experimentation based on evars +refinement started \\ + & & in 1991 by Gilles from V5.6 beta,\\ + & & with work by Hugo in July 1992\\ + +Coq V6.0 ``evars'' ``light'' & July 1993 & Hugo's port of the first +evars-based experimentation \\ + & & to Coq V5.7, version from October/November +1992\\ + +CtCoq & released 25 October 1995 & first beta-version \\ % Announce on coq-club by Janet + +Proto with explicit substitutions & 1997 &\\ + +Coq web site & 15 April 1998 & new site designed by David Delahaye \\ + +Coq web site & January 2004 & web site new style \\ + & & designed by Julien Narboux and Florent Kirchner \\ + +Coq web site & April 2009 & new Drupal-based site \\ + & & designed by Jean-Marc Notin and Denis Cousineau \\ + +\end{tabular} + +\end{document} diff --git a/dev/doc/extensions.txt b/dev/doc/extensions.txt deleted file mode 100644 index 075496db7c..0000000000 --- a/dev/doc/extensions.txt +++ /dev/null @@ -1,19 +0,0 @@ -Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ? -====================================================================== - -Exemple de l'ajout de l'entrée "clause": - -- ajouter un type ClauseArgType dans interp/genarg.ml{,i}, avec les - wit_, rawwit_, et globwit_ correspondants - -- ajouter partout où Genarg.argument_type est filtré le cas traitant de - ce nouveau ClauseArgType - -- utiliser le rawwit_clause pour définir une entrée clause du bon - type et du bon nom dans le module Tactic de pcoq.ml4 - -- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il - faut rejouter clause dans le GLOBAL du GEXTEND - -- seulement après, le nom clause sera accessible dans les TACTIC EXTEND ! - diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex deleted file mode 100644 index 337b9226df..0000000000 --- a/dev/doc/naming-conventions.tex +++ /dev/null @@ -1,606 +0,0 @@ -\documentclass[a4paper]{article} -\usepackage{fullpage} -\usepackage[utf8]{inputenc} -\usepackage[T1]{fontenc} -\usepackage{amsfonts} - -\parindent=0pt -\parskip=10pt - -%%%%%%%%%%%%% -% Macros -\newcommand\itemrule[3]{ -\subsubsection{#1} -\begin{quote} -\begin{tt} -#3 -\end{tt} -\end{quote} -\begin{quote} -Name: \texttt{#2} -\end{quote}} - -\newcommand\formula[1]{\begin{tt}#1\end{tt}} -\newcommand\tactic[1]{\begin{tt}#1\end{tt}} -\newcommand\command[1]{\begin{tt}#1\end{tt}} -\newcommand\term[1]{\begin{tt}#1\end{tt}} -\newcommand\library[1]{\texttt{#1}} -\newcommand\name[1]{\texttt{#1}} - -\newcommand\zero{\texttt{zero}} -\newcommand\op{\texttt{op}} -\newcommand\opPrime{\texttt{op'}} -\newcommand\opSecond{\texttt{op''}} -\newcommand\phimapping{\texttt{phi}} -\newcommand\D{\texttt{D}} -\newcommand\elt{\texttt{elt}} -\newcommand\rel{\texttt{rel}} -\newcommand\relp{\texttt{rel'}} - -%%%%%%%%%%%%% - -\begin{document} - -\begin{center} -\begin{huge} -Proposed naming conventions for the Coq standard library -\end{huge} -\end{center} -\bigskip - -The following document describes a proposition of canonical naming -schemes for the Coq standard library. Obviously and unfortunately, the -current state of the library is not as homogeneous as it would be if -it would systematically follow such a scheme. To tend in this -direction, we however recommend to follow the following suggestions. - -\tableofcontents - -\section{General conventions} - -\subsection{Variable names} - -\begin{itemize} - -\item Variables are preferably quantified at the head of the - statement, even if some premisses do not depend of one of them. For - instance, one would state -\begin{quote} -\begin{tt} - {forall x y z:D, x <= y -> x+z <= y+z} -\end{tt} -\end{quote} -and not -\begin{quote} -\begin{tt} - {forall x y:D, x <= y -> forall z:D, x+z <= y+z} -\end{tt} -\end{quote} - -\item Variables are preferably quantified (and named) in the order of - ``importance'', then of appearance, from left to right, even if - for the purpose of some tactics it would have been more convenient - to have, say, the variables not occurring in the conclusion - first. For instance, one would state -\begin{quote} -\begin{tt} - {forall x y z:D, x+z <= y+z -> x <= y} -\end{tt} -\end{quote} -and not -\begin{quote} -\begin{tt} - {forall z x y:D, x+z <= y+z -> x <= y} -\end{tt} -\end{quote} -nor -\begin{quote} -\begin{tt} - {forall x y z:D, y+x <= z+x -> y <= z} -\end{tt} -\end{quote} - -\item Choice of effective names is domain-dependent. For instance, on - natural numbers, the convention is to use the variables $n$, $m$, - $p$, $q$, $r$, $s$ in this order. - - On generic domains, the convention is to use the letters $x$, $y$, - $z$, $t$. When more than three variables are needed, indexing variables - - It is conventional to use specific names for variables having a - special meaning. For instance, $eps$ or $\epsilon$ can be used to - denote a number intended to be as small as possible. Also, $q$ and - $r$ can be used to denote a quotient and a rest. This is good - practice. - -\end{itemize} - -\subsection{Disjunctive statements} - -A disjunctive statement with a computational content will be suffixed -by \name{\_inf}. For instance, if - -\begin{quote} -\begin{tt} -{forall x y, op x y = zero -> x = zero \/ y = zero} -\end{tt} -\end{quote} -has name \texttt{D\_integral}, then -\begin{quote} -\begin{tt} -{forall x y, op x y = zero -> \{x = zero\} + \{y = zero\}} -\end{tt} -\end{quote} -will have name \texttt{D\_integral\_inf}. - -As an exception, decidability statements, such as -\begin{quote} -\begin{tt} -{forall x y, \{x = y\} + \{x <> y\}} -\end{tt} -\end{quote} -will have a named ended in \texttt{\_dec}. Idem for cotransitivity -lemmas which are inherently computational that are ended in -\texttt{\_cotrans}. - -\subsection{Inductive types constructor names} - -As a general rule, constructor names start with the name of the -inductive type being defined as in \texttt{Inductive Z := Z0 : Z | - Zpos : Z -> Z | Zneg : Z -> Z} to the exception of very standard -types like \texttt{bool}, \texttt{nat}, \texttt{list}... - -For inductive predicates, constructor names also start with the name -of the notion being defined with one or more suffixes separated with -\texttt{\_} for discriminating the different cases as e.g. in - -\begin{verbatim} -Inductive even : nat -> Prop := - | even_O : even 0 - | even_S n : odd n -> even (S n) -with odd : nat -> Prop := - | odd_S n : even n -> odd (S n). -\end{verbatim} - -As a general rule, inductive predicate names should be lowercase (to -the exception of notions referring to a proper name, e.g. \texttt{Bezout}) -and multiple words must be separated by ``{\_}''. - -As an exception, when extending libraries whose general rule is that -predicates names start with a capital letter, the convention of this -library should be kept and the separation between multiple words is -done by making the initial of each work a capital letter (if one of -these words is a proper name, then a ``{\_}'' is added to emphasize -that the capital letter is proper and not an application of the rule -for marking the change of word). - -Inductive predicates that characterize the specification of a function -should be named after the function it specifies followed by -\texttt{\_spec} as in: - -\begin{verbatim} -Inductive nth_spec : list A -> nat -> A -> Prop := - | nth_spec_O a l : nth_spec (a :: l) 0 a - | nth_spec_S n a b l : nth_spec l n a -> nth_spec (b :: l) (S n) a. -\end{verbatim} - -\section{Equational properties of operations} - -\subsection{General conventions} - -If the conclusion is in the other way than listed below, add suffix -\name{\_reverse} to the lemma name. - -\subsection{Specific conventions} - -\itemrule{Associativity of binary operator {\op} on domain {\D}}{Dop\_assoc} -{forall x y z:D, op x (op y z) = op (op x y) z} - - Remark: Symmetric form: \name{Dop\_assoc\_reverse}: - \formula{forall x y z:D, op (op x y) z = op x (op y z)} - -\itemrule{Commutativity of binary operator {\op} on domain {\D}}{Dop\_comm} -{forall x y:D, op x y = op y x} - - Remark: Avoid \formula{forall x y:D, op y x = op x y}, or at worst, call it - \name{Dop\_comm\_reverse} - -\itemrule{Left neutrality of element elt for binary operator {\op}}{Dop\_elt\_l} -{forall x:D, op elt x = x} - - Remark: In English, ``{\elt} is an identity for {\op}'' seems to be - a more common terminology. - -\itemrule{Right neutrality of element elt for binary operator {\op}}{Dop\_elt\_r} -{forall x:D, op x elt = x} - - Remark: By convention, if the identities are reminiscent to zero or one, they - are written 1 and 0 in the name of the property. - -\itemrule{Left absorption of element elt for binary operator {\op}}{Dop\_elt\_l} -{forall x:D, op elt x = elt} - - Remarks: - \begin{itemize} - \item In French school, this property is named "elt est absorbant pour op" - \item English, the property seems generally named "elt is a zero of op" - \item In the context of lattices, this a boundedness property, it may - be called "elt is a bound on D", or referring to a (possibly - arbitrarily oriented) order "elt is a least element of D" or "elt - is a greatest element of D" - \end{itemize} - -\itemrule{Right absorption of element {\elt} for binary operator {\op}}{Dop\_elt\_l [BAD ??]} -{forall x:D, op x elt = elt} - -\itemrule{Left distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_l} -{forall x y z:D, op (op' x y) z = op' (op x z) (op y z)} - - Remark: Some authors say ``distribution''. - -\itemrule{Right distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_r} -{forall x y z:D, op z (op' x y) = op' (op z x) (op z y)} - - Remark: Note the order of arguments. - -\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} -{forall x y:D, op (op' x y) = op' (op x) (op y)} - -\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} -{forall x y:D, op (op' x y) = op' (op x) (op y)} - - Remark: For a non commutative operation with inversion of arguments, as in - \formula{forall x y z:D, op (op' x y) = op' (op y) (op y z)}, - we may probably still call the property distributivity since there - is no ambiguity. - - Example: \formula{forall n m : Z, -(n+m) = (-n)+(-m)}. - - Example: \formula{forall l l' : list A, rev (l++l') = (rev l)++(rev l')}. - -\itemrule{Left extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l} -{forall x y:D, op (op' x y) = op' (op x) y} - - Question: Call it left commutativity ?? left swap ? - -\itemrule{Right extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r} -{forall x y:D, op (op' x y) = op' x (op y)} - -\itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} -{forall x:D, op x x = x} - -\itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent} -{forall x:D, op (op x) = op x} - - Remark: This is actually idempotency of {\op} wrt to composition and - identity. - -\itemrule{Idempotency of element elt for binary operator {\op} on domain {\D}}{Dop\_elt\_idempotent} -{op elt elt = elt} - - Remark: Generally useless in CIC for concrete, computable operators - - Remark: The general definition is ``exists n, iter n op x = x''. - -\itemrule{Nilpotency of element elt wrt a ring D with additive neutral -element {\zero} and multiplicative binary operator -{\op}}{Delt\_nilpotent} -{op elt elt = zero} - - Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''. - -\itemrule{Zero-product property in a ring D with additive neutral -element {\zero} and multiplicative binary operator -{\op}}{D\_integral} -{forall x y, op x y = zero -> x = zero \/ y = zero} - - Remark: We leave the ring structure of D implicit; the Coq library - uses either \texttt{\_is\_O} (for \texttt{nat}), \texttt{\_integral} - (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for - \texttt{NZ}). - - Remark: The French school says ``integrité''. - -\itemrule{Nilpotency of binary operator {\op} wrt to its absorbing element -zero in D}{Dop\_nilpotent} {forall x, op x x = zero} - - Remark: Did not find this definition on the web, but it used in - the Coq library (to characterize \name{xor}). - -\itemrule{Involutivity of unary op on D}{Dop\_involutive} -{forall x:D, op (op x) = x} - -\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the left}{Dop\_op'\_absorption\_l\_l} -{forall x y:D, op x (op' x y) = x} - -\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the right}{Dop\_op'\_absorption\_l\_r} -{forall x y:D, op x (op' y x) = x} - - Remark: Similarly for \name{Dop\_op'\_absorption\_r\_l} and \name{Dop\_op'\_absorption\_r\_r}. - -\itemrule{De Morgan law's for binary operators {\opPrime} and {\opSecond} wrt -to unary op on domain {\D}}{Dop'\_op''\_de\_morgan, -Dop''\_op'\_de\_morgan ?? \mbox{leaving the complementing operation -implicit})} -{forall x y:D, op (op' x y) = op'' (op x) (op y)\\ -forall x y:D, op (op'' x y) = op' (op x) (op y)} - -\itemrule{Left complementation of binary operator {\op} by means of unary {\opPrime} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_op'\_opp\_l} -{forall x:D, op (op' x) x = elt} - -Remark: If the name of the opposite function is reminiscent of the -notion of complement (e.g. if it is called \texttt{opp}), one can -simply say {Dop\_opp\_l}. - -\itemrule{Right complementation of binary operator {\op} by means of unary {\op'} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_opp\_r} -{forall x:D, op x (op' x) = elt} - -Example: \formula{Radd\_opp\_l: forall r : R, - r + r = 0} - -\itemrule{Associativity of binary operators {\op} and {\op'}}{Dop\_op'\_assoc} -{forall x y z, op x (op' y z) = op (op' x y) z} - -Example: \formula{forall x y z, x + (y - z) = (x + y) - z} - -\itemrule{Right extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_r} -{forall x y z, op x (op' y z) = op' (op x y) z} - -Remark: This requires {\op} and {\opPrime} to have their right and left -argument respectively and their return types identical. - -Example: \formula{forall x y z, x + (y - z) = (x + y) - z} - -Remark: Other less natural combinations are possible, such -as \formula{forall x y z, op x (op' y z) = op' y (op x z)}. - -\itemrule{Left extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_l} -{forall x y z, op (op' x y) z = op' x (op y z)} - -Remark: Operations are not necessarily internal composition laws. It -is only required that {\op} and {\opPrime} have their right and left -argument respectively and their return type identical. - -Remark: When the type are heterogeneous, only one extrusion law is possible and it can simply be named {Dop\_op'\_extrusion}. - -Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}. - -%====================================================================== -%\section{Properties of elements} - -%Remark: Not used in current library - - - -%====================================================================== -\section{Preservation and compatibility properties of operations} - -\subsection{With respect to equality} - -\itemrule{Injectivity of unary operator {\op}}{Dop\_inj} -{forall x y:D, op x = op y -> x = y} - -\itemrule{Left regularity of binary operator {\op}}{Dop\_reg\_l, Dop\_inj\_l, or Dop\_cancel\_l} -{forall x y z:D, op z x = op z y -> x = y} - - Remark: Note the order of arguments. - - Remark: The Coq usage is to called it regularity but the English - standard seems to be cancellation. The recommended form is not - decided yet. - - Remark: Shall a property like $n^p \leq n^q \rightarrow p \leq q$ - (for $n\geq 1$) be called cancellation or should it be reserved for - operators that have an inverse? - -\itemrule{Right regularity of binary operator {\op}}{Dop\_reg\_r, Dop\_inj\_r, Dop\_cancel\_r} -{forall x y z:D, op x z = op y z -> x = y} - -\subsection{With respect to a relation {\rel}} - -\itemrule{Compatibility of unary operator {\op}}{Dop\_rel\_compat} -{forall x y:D, rel x y -> rel (op x) (op y)} - -\itemrule{Left compatibility of binary operator {\op}}{Dop\_rel\_compat\_l} -{forall x y z:D, rel x y -> rel (op z x) (op z y)} - -\itemrule{Right compatibility of binary operator {\op}}{Dop\_rel\_compat\_r} -{forall x y z:D, rel x y -> rel (op x z) (op y z)} - - Remark: For equality, use names of the form \name{Dop\_eq\_compat\_l} or - \name{Dop\_eq\_compat\_r} -(\formula{forall x y z:D, y = x -> op y z = op x z} and -\formula{forall x y z:D, y = x -> op y z = op x z}) - - Remark: Should we admit (or even prefer) the name - \name{Dop\_rel\_monotone}, \name{Dop\_rel\_monotone\_l}, - \name{Dop\_rel\_monotone\_r} when {\rel} is an order ? - -\itemrule{Left regularity of binary operator {\op}}{Dop\_rel\_reg\_l} -{forall x y z:D, rel (op z x) (op z y) -> rel x y} - -\itemrule{Right regularity of binary operator {\op}}{Dop\_rel\_reg\_r} -{forall x y z:D, rel (op x z) (op y z) -> rel x y} - - Question: Would it be better to have \name{z} as first argument, since it - is missing in the conclusion ?? (or admit we shall use the options - ``\texttt{with p}''?) - -\itemrule{Left distributivity of binary operator {\op} over {\opPrime} along relation {\rel} on domain {\D}}{Dop\_op'\_rel\_distr\_l} -{forall x y z:D, rel (op (op' x y) z) (op' (op x z) (op y z))} - - Example: standard property of (not necessarily distributive) lattices - - Remark: In a (non distributive) lattice, by swapping join and meet, - one would like also, -\formula{forall x y z:D, rel (op' (op x z) (op y z)) (op (op' x y) z)}. - How to name it with a symmetric name (use - \name{Dop\_op'\_rel\_distr\_mon\_l} and - \name{Dop\_op'\_rel\_distr\_anti\_l})? - -\itemrule{Commutativity of binary operator {\op} along (equivalence) relation {\rel} on domain {\D}}{Dop\_op'\_rel\_comm} -{forall x y z:D, rel (op x y) (op y x)} - - Example: -\formula{forall l l':list A, Permutation (l++l') (l'++l)} - -\itemrule{Irreducibility of binary operator {\op} on domain {\D}}{Dop\_irreducible} -{forall x y z:D, z = op x y -> z = x $\backslash/$ z = y} - - Question: What about the constructive version ? Call it \name{Dop\_irreducible\_inf} ? -\formula{forall x y z:D, z = op x y -> \{z = x\} + \{z = y\}} - -\itemrule{Primality of binary operator {\op} along relation {\rel} on domain {\D}}{Dop\_rel\_prime} -{forall x y z:D, rel z (op x y) -> rel z x $\backslash/$ rel z y} - - -%====================================================================== -\section{Morphisms} - -\itemrule{Morphism between structures {\D} and {\D'}}{\name{D'\_of\_D}}{D -> D'} - -Remark: If the domains are one-letter long, one can used \texttt{IDD'} as for -\name{INR} or \name{INZ}. - -\itemrule{Morphism {\phimapping} mapping unary operators {\op} to {\op'}}{phi\_op\_op', phi\_op\_op'\_morphism} -{forall x:D, phi (op x) = op' (phi x)} - -Remark: If the operators have the same name in both domains, one use -\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}. - -Example: \formula{Z\_of\_nat\_mult: forall n m : nat, Z\_of\_nat (n * m) = (Z\_of\_nat n * Z\_of\_nat m)\%Z}. - -Remark: If the operators have different names on distinct domains, one -can use \texttt{op\_op'}. - -\itemrule{Morphism {\phimapping} mapping binary operators {\op} to -{\op'}}{phi\_op\_op', phi\_op\_op'\_morphism} {forall -x y:D, phi (op x y) = op' (phi x) (phi y)} - -Remark: If the operators have the same name in both domains, one use -\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}. - -Remark: If the operators have different names on distinct domains, one -can use \texttt{op\_op'}. - -\itemrule{Morphism {\phimapping} mapping binary operator {\op} to -binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism} -{forall x y:D, phi (op x y) <-> rel (phi x) (phi y)} - -Remark: If the operator and the relation have similar name, one uses -\texttt{phi\_op}. - -Question: How to name each direction? (add \_elim for -> and \_intro -for <- ?? -- as done in Bool.v ??) - -Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}. - -%====================================================================== -\section{Preservation and compatibility properties of operations wrt order} - -\itemrule{Compatibility of binary operator {\op} wrt (strict order) {\rel} and (large order) {\rel'}}{Dop\_rel\_rel'\_compat} -{forall x y z t:D, rel x y -> rel' z t -> rel (op x z) (op y t)} - -\itemrule{Compatibility of binary operator {\op} wrt (large order) {\relp} and (strict order) {\rel}}{Dop\_rel'\_rel\_compat} -{forall x y z t:D, rel' x y -> rel z t -> rel (op x z) (op y t)} - - -%====================================================================== -\section{Properties of relations} - -\itemrule{Reflexivity of relation {\rel} on domain {\D}}{Drel\_refl} -{forall x:D, rel x x} - -\itemrule{Symmetry of relation {\rel} on domain {\D}}{Drel\_sym} -{forall x y:D, rel x y -> rel y x} - -\itemrule{Transitivity of relation {\rel} on domain {\D}}{Drel\_trans} -{forall x y z:D, rel x y -> rel y z -> rel x z} - -\itemrule{Antisymmetry of relation {\rel} on domain {\D}}{Drel\_antisym} -{forall x y:D, rel x y -> rel y x -> x = y} - -\itemrule{Irreflexivity of relation {\rel} on domain {\D}}{Drel\_irrefl} -{forall x:D, \~{} rel x x} - -\itemrule{Asymmetry of relation {\rel} on domain {\D}}{Drel\_asym} -{forall x y:D, rel x y -> \~{} rel y x} - -\itemrule{Cotransitivity of relation {\rel} on domain {\D}}{Drel\_cotrans} -{forall x y z:D, rel x y -> \{rel z y\} + \{rel x z\}} - -\itemrule{Linearity of relation {\rel} on domain {\D}}{Drel\_trichotomy} -{forall x y:D, \{rel x y\} + \{x = y\} + \{rel y x\}} - - Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear}, or - \name{Drel\_connected}? Use - $\backslash/$ ? or use a ternary sumbool, or a ternary disjunction, - for nicer elimination. - -\itemrule{Informative decidability of relation {\rel} on domain {\D}}{Drel\_dec (or Drel\_dect, Drel\_dec\_inf ?)} -{forall x y:D, \{rel x y\} + \{\~{} rel x y\}} - - Remark: If equality: \name{D\_eq\_dec} or \name{D\_dec} (not like - \name{eq\_nat\_dec}) - -\itemrule{Non informative decidability of relation {\rel} on domain {\D}}{Drel\_dec\_prop (or Drel\_dec)} -{forall x y:D, rel x y $\backslash/$ \~{} rel x y} - -\itemrule{Inclusion of relation {\rel} in relation {\rel}' on domain {\D}}{Drel\_rel'\_incl (or Drel\_incl\_rel')} -{forall x y:D, rel x y -> rel' x y} - - Remark: Use \name{Drel\_rel'\_weak} for a strict inclusion ?? - -%====================================================================== -\section{Relations between properties} - -\itemrule{Equivalence of properties \texttt{P} and \texttt{Q}}{P\_Q\_iff} -{forall x1 .. xn, P <-> Q} - - Remark: Alternatively use \name{P\_iff\_Q} if it is too difficult to - recover what pertains to \texttt{P} and what pertains to \texttt{Q} - in their concatenation (as e.g. in - \texttt{Godel\_Dummett\_iff\_right\_distr\_implication\_over\_disjunction}). - -%====================================================================== -\section{Arithmetical conventions} - -\begin{minipage}{6in} -\renewcommand{\thefootnote}{\thempfootnote} % For footnotes... -\begin{tabular}{lll} -Zero on domain {\D} & D0 & (notation \verb=0=)\\ -One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\ -Successor on domain {\D} & Dsucc\\ -Predessor on domain {\D} & Dpred\\ -Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}} - & (infix notation \verb=+= [50,L])\\ -Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\ -Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ -Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\ -Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\ -Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\ -Minimal element on domain {\D} & Dmin\\ -Maximal element on domain {\D} & Dmax\\ -Large less than order on {\D} & Dle & (infix notations \verb!<=! and \verb!>=! [70,N]))\\ -Strict less than order on {\D} & Dlt & (infix notations \verb=<= and \verb=>= [70,N]))\\ -\end{tabular} -\bigskip -\end{minipage} - -\bigskip - -The status of \verb!>=! and \verb!>! is undecided yet. It will eithet -be accepted only as parsing notations or may also accepted as a {\em - definition} for the \verb!<=! and \verb! ... -\end{verbatim} -ce qui introduit un constructeur moralement équivalent à une -application situé à une priorité totalement différente (les -``bindings'' seraient au plus haut niveau alors que l'application est -à un niveau bas). - - -\begin{figure} -\begin{rulebox} -\DEFNT{binding-term} - \NT{constr} ~\TERM{with} ~\STAR{\NT{binding}} -\SEPDEF -\DEFNT{binding} - \NT{constr} -\end{rulebox} -\caption{Grammaire des bindings} -\label{bindings} -\end{figure} - -\subsection{Enregistrements} - -Il faudrait aménager la syntaxe des enregistrements dans l'optique -d'avoir des enregistrements anonymes (termes de première classe), même -si pour l'instant, on ne dispose que d'enregistrements définis a -toplevel. - -Exemple de syntaxe pour les types d'enregistrements: -\begin{verbatim} -{ x1 : A1; - x2 : A2(x1); - _ : T; (* Pas de projection disponible *) - y; (* Type infere *) - ... (* ; optionnel pour le dernier champ *) -} -\end{verbatim} - -Exemple de syntaxe pour le constructeur: -\begin{verbatim} -{ x1 = O; - x2 : A2(x1) = v1; - _ = v2; - ... -} -\end{verbatim} -Quant aux dépendences, une convention pourrait être de considérer les -champs non annotés par le type comme non dépendants. - -Plusieurs interrogations: -\begin{itemize} -\item l'ordre des champs doit-il être respecté ? - sinon, que faire pour les champs sans projection ? -\item autorise-t-on \texttt{v1} a mentionner \texttt{x1} (comme dans - la définition d'un module), ce qui se comporterait comme si on avait - écrit \texttt{v1} à la place. Cela pourrait être une autre manière - de déclarer les dépendences -\end{itemize} - -La notation pointée pour les projections pose un problème de parsing, -sauf si l'on a une convention lexicale qui discrimine les noms de -modules des projections et identificateurs: \texttt{x.y.z} peut être -compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}. - - -\section{Grammaire des termes} -\label{constrsyntax} - -\subsection{Quelques principes} - -\begin{enumerate} -\item Diminuer le nombre de niveaux de priorité en regroupant les - règles qui se ressemblent: infixes, préfixes, lieurs (constructions - ouvertes à droite), etc. -\item Éviter de surcharger la signification d'un symbole (ex: - \verb+( )+ comme parenthésage et produit dans la V7). -\item Faire en sorte que les membres gauches (motifs de Cases, lieurs - d'abstraction ou de produits) utilisent une syntaxe compatible avec - celle des membres droits (branches de Cases et corps de fonction). -\end{enumerate} - -\subsection{Présentation de la grammaire} - -\begin{figure} -\begin{rulebox} -\DEFNT{paren-constr} - \NT{cast-constr}~\TERM{,}~\NT{paren-constr} &\RNAME{pair} -\nlsep \NT{cast-constr} -\SEPDEF -\DEFNT{cast-constr} - \NT{constr}~\TERM{\!\!:}~\NT{cast-constr} &\RNAME{cast} -\nlsep \NT{constr} -\SEPDEF -\DEFNT{constr} - \NT{appl-constr}~\NT{infix}~\NT{constr} &\RNAME{infix} -\nlsep \NT{prefix}~\NT{constr} &\RNAME{prefix} -\nlsep \NT{constr}~\NT{postfix} &\RNAME{postfix} -\nlsep \NT{appl-constr} -\SEPDEF -\DEFNT{appl-constr} - \NT{appl-constr}~\PLUS{\NT{appl-arg}} &\RNAME{apply} -\nlsep \TERM{@}~\NT{global}~\PLUS{\NT{simple-constr}} &\RNAME{expl-apply} -\nlsep \NT{simple-constr} -\SEPDEF -\DEFNT{appl-arg} - \TERM{@}~\NT{int}~\TERM{\!:=}~\NT{simple-constr} &\RNAME{impl-arg} -\nlsep \NT{simple-constr} -\SEPDEF -\DEFNT{simple-constr} - \NT{atomic-constr} -\nlsep \TERM{(}~\NT{paren-constr}~\TERM{)} -\nlsep \NT{match-constr} -\nlsep \NT{fix-constr} -%% \nlsep \TERM{<\!\!:ast\!\!:<}~\NT{ast}~\TERM{>\!>} &\RNAME{quotation} -\end{rulebox} -\caption{Grammaire des termes} -\label{constr} -\end{figure} - -\begin{figure} -\begin{rulebox} -\DEFNT{prefix} - \TERM{!}~\PLUS{\NT{binder}}~\TERM{.}~ &\RNAME{prod} -\nlsep \TERM{fun} ~\PLUS{\NT{binder}} ~\TERM{$\Rightarrow$} &\RNAME{lambda} -\nlsep \TERM{let}~\NT{ident}~\STAR{\NT{binder}} ~\TERM{=}~\NT{constr} - ~\TERM{in} &\RNAME{let} -%\nlsep \TERM{let (}~\NT{comma-ident-list}~\TERM{) =}~\NT{constr} -% ~\TERM{in} &~~~\RNAME{let-case} -\nlsep \TERM{if}~\NT{constr}~\TERM{then}~\NT{constr}~\TERM{else} - &\RNAME{if-case} -\nlsep \TERM{eval}~\NT{red-fun}~\TERM{in} &\RNAME{eval} -\SEPDEF -\DEFNT{infix} - \TERM{$\rightarrow$} & \RNAME{impl} -\SEPDEF -\DEFNT{atomic-constr} - \TERM{_} -\nlsep \TERM{?}\NT{int} -\nlsep \NT{sort} -\nlsep \NT{global} -\SEPDEF -\DEFNT{binder} - \NT{ident} &\RNAME{infer} -\nlsep \TERM{(}~\NT{ident}~\NT{type}~\TERM{)} &\RNAME{binder} -\SEPDEF -\DEFNT{type} - \TERM{\!:}~\NT{constr} -\nlsep \epsilon -\end{rulebox} -\caption{Grammaires annexes aux termes} -\label{gram-annexes} -\end{figure} - -La grammaire des termes (correspondant à l'état \texttt{barestate}) -est décrite figures~\ref{constr} et~\ref{gram-annexes}. On constate -par rapport aux précédentes versions de Coq d'importants changements -de priorité, le plus marquant étant celui de l'application qui se -trouve désormais juste au dessus\footnote{La convention est de -considérer les opérateurs moins lieurs comme ``au dessus'', -c'est-à-dire ayant un niveau de priorité plus élévé (comme c'est le -cas avec le niveau de la grammaire actuelle des termes).} des -constructions fermées à gauche et à droite. - -La grammaire des noms globaux est la suivante: -\begin{eqnarray*} -\DEFNT{global} - \NT{ident} -%% \nlsep \TERM{\$}\NT{ident} -\nlsep \NT{ident}\TERM{.}\NT{global} -\end{eqnarray*} - -Le $\TERM{_}$ dénote les termes à synthétiser. Les métavariables sont -reconnues au niveau du lexer pour ne pas entrer en conflit avec le -$\TERM{?}$ de l'existentielle. - -Les opérateurs infixes ou préfixes sont tous au même niveau de -priorité du point de vue de Camlp4. La solution envisagée est de les -gérer à la manière de Yacc, avec une pile (voir discussions plus -bas). Ainsi, l'implication est un infixe normal; la quantification -universelle et le let sont vus comme des opérateurs préfixes avec un -niveau de priorité plus haut (i.e. moins lieur). Il subsiste des -problèmes si l'on ne veut pas écrire de parenthèses dans: -\begin{verbatim} - A -> (!x. B -> (let y = C in D)) -\end{verbatim} - -La solution proposée est d'analyser le membre droit d'un infixe de -manière à autoriser les préfixes et les infixes de niveau inférieur, -et d'exiger le parenthésage que pour les infixes de niveau supérieurs. - -En revanche, à l'affichage, certains membres droits seront plus -lisibles s'ils n'utilisent pas cette astuce: -\begin{verbatim} -(fun x => x) = fun x => x -\end{verbatim} - -La proposition est d'autoriser ce type d'écritures au parsing, mais -l'afficheur écrit de manière standardisée en mettant quelques -parenthèses superflues: $\TERM{=}$ serait symétrique alors que -$\rightarrow$ appellerait l'afficheur de priorité élevée pour son -sous-terme droit. - -Les priorités des opérateurs primitifs sont les suivantes (le signe -$*$ signifie que pour le membre droit les opérateurs préfixes seront -affichés sans parenthèses quel que soit leur priorité): -$$ -\begin{array}{c|l} -$symbole$ & $priorité$ \\ -\hline -\TERM{!} & 200\,R* \\ -\TERM{fun} & 200\,R* \\ -\TERM{let} & 200\,R* \\ -\TERM{if} & 200\,R \\ -\TERM{eval} & 200\,R \\ -\rightarrow & 90\,R* -\end{array} -$$ - -Il y a deux points d'entrée pour les termes: $\NT{constr}$ et -$\NT{simple-constr}$. Le premier peut être utilisé lorsqu'il est suivi -d'un séparateur particulier. Dans le cas où l'on veut une liste de -termes séparés par un espace, il faut lire des $\NT{simple-constr}$. - - - -Les constructions $\TERM{fix}$ et $\TERM{cofix}$ (voir aussi -figure~\ref{gram-fix}) sont fermées par end pour simplifier -l'analyse. Sinon, une expression de point fixe peut être suivie par un -\TERM{in} ou un \TERM{and}, ce qui pose les mêmes problèmes que le -``dangling else'': dans -\begin{verbatim} -fix f1 x {x} = fix f2 y {y} = ... and ... in ... -\end{verbatim} -il faut définir une stratégie pour associer le \TERM{and} et le -\TERM{in} au bon point fixe. - -Un autre avantage est de faire apparaitre que le \TERM{fix} est un -constructeur de terme de première classe et pas un lieur: -\begin{verbatim} -fix f1 ... and f2 ... -in f1 end x -\end{verbatim} -Les propositions précédentes laissaient \texttt{f1} et \texttt{x} -accolés, ce qui est source de confusion lorsque l'on fait par exemple -\texttt{Pattern (f1 x)}. - -Les corps de points fixes et co-points fixes sont identiques, bien que -ces derniers n'aient pas d'information de décroissance. Cela -fonctionne puisque l'annotation est optionnelle. Cela préfigure des -cas où l'on arrive à inférer quel est l'argument qui décroit -structurellement (en particulier dans le cas où il n'y a qu'un seul -argument). - -\begin{figure} -\begin{rulebox} -\DEFNT{fix-expr} - \TERM{fix}~\NT{fix-decls} ~\NT{fix-select} ~\TERM{end} &\RNAME{fix} -\nlsep \TERM{cofix}~\NT{cofix-decls}~\NT{fix-select} ~\TERM{end} &\RNAME{cofix} -\SEPDEF -\DEFNT{fix-decls} - \NT{fix-decl}~\TERM{and}~\NT{fix-decls} -\nlsep \NT{fix-decl} -\SEPDEF -\DEFNT{fix-decl} - \NT{ident}~\PLUS{\NT{binder}}~\NT{type}~\NT{annot} - ~\TERM{=}~\NT{constr} -\SEPDEF -\DEFNT{annot} - \TERM{\{}~\NT{ident}~\TERM{\}} -\nlsep \epsilon -\SEPDEF -\DEFNT{fix-select} - \TERM{in}~\NT{ident} -\nlsep \epsilon -\end{rulebox} -\caption{Grammaires annexes des points fixes} -\label{gram-fix} -\end{figure} - -La construction $\TERM{Case}$ peut-être considérée comme -obsolète. Quant au $\TERM{Match}$ de la V6, il disparaît purement et -simplement. - -\begin{figure} -\begin{rulebox} -\DEFNT{match-expr} - \TERM{match}~\NT{case-items}~\NT{case-type}~\TERM{with}~ - \NT{branches}~\TERM{end} &\RNAME{match} -\nlsep \TERM{match}~\NT{case-items}~\TERM{with}~ - \NT{branches}~\TERM{end} &\RNAME{infer-match} -%%\nlsep \TERM{case}~\NT{constr}~\NT{case-predicate}~\TERM{of}~ -%% \STAR{\NT{constr}}~\TERM{end} &\RNAME{case} -\SEPDEF -\DEFNT{case-items} - \NT{case-item} ~\TERM{\&} ~\NT{case-items} -\nlsep \NT{case-item} -\SEPDEF -\DEFNT{case-item} - \NT{constr}~\NT{pred-pattern} &\RNAME{dep-case} -\nlsep \NT{constr} &\RNAME{nodep-case} -\SEPDEF -\DEFNT{case-type} - \TERM{$\Rightarrow$}~\NT{constr} -\nlsep \epsilon -\SEPDEF -\DEFNT{pred-pattern} - \TERM{as}~\NT{ident} ~\TERM{\!:}~\NT{constr} -\SEPDEF -\DEFNT{branches} - \TERM{|} ~\NT{patterns} ~\TERM{$\Rightarrow$} - ~\NT{constr} ~\NT{branches} -\nlsep \epsilon -\SEPDEF -\DEFNT{patterns} - \NT{pattern} ~\TERM{\&} ~\NT{patterns} -\nlsep \NT{pattern} -\SEPDEF -\DEFNT{pattern} ... -\end{rulebox} -\caption{Grammaires annexes du filtrage} -\label{gram-match} -\end{figure} - -De manière globale, l'introduction de définitions dans les termes se -fait avec le symbole $=$, et le $\!:=$ est réservé aux définitions au -niveau vernac. Il y avait un manque de cohérence dans la -V6, puisque l'on utilisait $=$ pour le $\TERM{let}$ et $\!:=$ pour les -points fixes et les commandes vernac. - -% OBSOLETE: lieurs multiples supprimes -%On peut remarquer que $\NT{binder}$ est un sous-ensemble de -%$\NT{simple-constr}$, à l'exception de $\texttt{(a,b\!\!:T)}$: en tant -%que lieur, {\tt a} et {\tt b} sont tous deux contraints, alors qu'en -%tant que terme, seul {\tt b} l'est. Cela qui signifie que l'objectif -%de rendre compatibles les membres gauches et droits est {\it presque} -%atteint. - -\subsection{Infixes} - -\subsubsection{Infixes extensibles} - -Le problème de savoir si la liste des symboles pouvant apparaître en -infixe est fixée ou extensible par l'utilisateur reste à voir. - -Notons que la solution où les symboles infixes sont des -identificateurs que l'on peut définir paraît difficilement praticable: -par exemple $\texttt{Logic.eq}$ n'est pas un opérateur binaire, mais -ternaire. Il semble plus simple de garder des déclarations infixes qui -relient un symbole infixe à un terme avec deux ``trous''. Par exemple: - -$$\begin{array}{c|l} -$infixe$ & $identificateur$ \\ -\hline -= & \texttt{Logic.eq _ ?1 ?2} \\ -== & \texttt{JohnMajor.eq _ ?1 _ ?2} -\end{array}$$ - -La syntaxe d'une déclaration d'infixe serait par exemple: -\begin{verbatim} -Infix "=" 50 := Logic.eq _ ?1 ?2; -\end{verbatim} - - -\subsubsection{Gestion des précédences} - -Les infixes peuvent être soit laissé à Camlp4, ou bien (comme ici) -considérer que tous les opérateurs ont la même précédence et gérer -soit même la recomposition des termes à l'aide d'une pile (comme -Yacc). - - -\subsection{Extensions de syntaxe} - -\subsubsection{Litéraux numériques} - -La proposition est de considerer les litéraux numériques comme de -simples identificateurs. Comme il en existe une infinité, il faut un -nouveau mécanisme pour leur associer une définition. Par exemple, en -ce qui concerne \texttt{Arith}, la définition de $5$ serait -$\texttt{S}~4$. Pour \texttt{ZArith}, $5$ serait $\texttt{xI}~2$. - -Comme les infixes, les constantes numériques peuvent être qualifiées -pour indiquer dans quels module est le type que l'on veut -référencer. Par exemple (si on renomme \texttt{Arith} en \texttt{N} et -\texttt{ZArith} en \texttt{Z}): \verb+N.5+, \verb+Z.5+. - -\begin{eqnarray*} -\EXTNT{global} - \NT{int} -\end{eqnarray*} - -\subsubsection{Nouveaux lieurs} - -$$ -\begin{array}{rclr} -\EXTNT{constr} - \TERM{ex}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr} &\RNAME{ex} -\nlsep \TERM{ex}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}~\TERM{,}~\NT{constr} - &\RNAME{ex2} -\nlsep \TERM{ext}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr} &\RNAME{exT} -\nlsep \TERM{ext}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}~\TERM{,}~\NT{constr} - &\RNAME{exT2} -\end{array} -$$ - -Pour l'instant l'existentielle n'admet qu'une seule variable, ce qui -oblige à écrire des cascades de $\TERM{ex}$. - -Pour parser les existentielles avec deux prédicats, on peut considérer -\TERM{\&} comme un infixe intermédiaire et l'opérateur existentiel en -présence de cet infixe se transforme en \texttt{ex2}. - -\subsubsection{Nouveaux infixes} - -Précédences des opérateurs infixes (les plus grands associent moins fort): -$$ -\begin{array}{l|l|c|l} -$identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ -\hline -\texttt{iff} & $Logic$ & \longleftrightarrow & 100 \\ -\texttt{or} & $Logic$ & \vee & 80\, R \\ -\texttt{sum} & $Datatypes$ & + & 80\, R \\ -\texttt{and} & $Logic$ & \wedge & 70\, R \\ -\texttt{prod} & $Datatypes$ & * & 70\, R \\ -\texttt{not} & $Logic$ & \tilde{} & 60\, L \\ -\texttt{eq _} & $Logic$ & = & 50 \\ -\texttt{eqT _} & $Logic_Type$ & = & 50 \\ -\texttt{identityT _} & $Data_Type$ & = & 50 \\ -\texttt{le} & $Peano$ & $<=$ & 50 \\ -\texttt{lt} & $Peano$ & $<$ & 50 \\ -\texttt{ge} & $Peano$ & $>=$ & 50 \\ -\texttt{gt} & $Peano$ & $>$ & 50 \\ -\texttt{Zle} & $zarith_aux$ & $<=$ & 50 \\ -\texttt{Zlt} & $zarith_aux$ & $<$ & 50 \\ -\texttt{Zge} & $zarith_aux$ & $>=$ & 50 \\ -\texttt{Zgt} & $zarith_aux$ & $>$ & 50 \\ -\texttt{Rle} & $Rdefinitions$ & $<=$ & 50 \\ -\texttt{Rlt} & $Rdefinitions$ & $<$ & 50 \\ -\texttt{Rge} & $Rdefinitions$ & $>=$ & 50 \\ -\texttt{Rgt} & $Rdefinitions$ & $>$ & 50 \\ -\texttt{plus} & $Peano$ & + & 40\,L \\ -\texttt{Zplus} & $fast_integer$ & + & 40\,L \\ -\texttt{Rplus} & $Rdefinitions$ & + & 40\,L \\ -\texttt{minus} & $Minus$ & - & 40\,L \\ -\texttt{Zminus} & $zarith_aux$ & - & 40\,L \\ -\texttt{Rminus} & $Rdefinitions$ & - & 40\,L \\ -\texttt{Zopp} & $fast_integer$ & - & 40\,L \\ -\texttt{Ropp} & $Rdefinitions$ & - & 40\,L \\ -\texttt{mult} & $Peano$ & * & 30\,L \\ -\texttt{Zmult} & $fast_integer$ & * & 30\,L \\ -\texttt{Rmult} & $Rdefinitions$ & * & 30\,L \\ -\texttt{Rdiv} & $Rdefinitions$ & / & 30\,L \\ -\texttt{pow} & $Rfunctions$ & \hat & 20\,L \\ -\texttt{fact} & $Rfunctions$ & ! & 20\,L \\ -\end{array} -$$ - -Notons qu'il faudrait découper {\tt Logic_Type} en deux car celui-ci -définit deux égalités, ou alors les mettre dans des modules différents. - -\subsection{Exemples} - -\begin{verbatim} -Definition not (A:Prop) := A->False; -Inductive eq (A:Set) (x:A) : A->Prop := - refl_equal : eq A x x; -Inductive ex (A:Set) (P:A->Prop) : Prop := - ex_intro : !x. P x -> ex A P; -Lemma not_all_ex_not : !(P:U->Prop). ~(!n. P n) -> ?n. ~ P n; -Fixpoint plus n m : nat {struct n} := - match n with - O => m - | (S k) => S (plus k m) - end; -\end{verbatim} - -\subsection{Questions ouvertes} - -Voici les points sur lesquels la discussion est particulièrement -ouverte: -\begin{itemize} -\item choix d'autres symboles pour les quantificateurs \TERM{!} et - \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!} - pour la qunatification universelle, mais on choisirait quelquechose - comme \TERM{ex} pour l'existentielle, afin de ne pas suggérer trop - de symétrie entre ces quantificateurs (l'un est primitif, l'autre - pas). -\item syntaxe particulière pour les \texttt{sig}, \texttt{sumor}, etc. -\item la possibilité d'introduire plusieurs variables du même type est - pour l'instant supprimée au vu des problèmes de compatibilité de - syntaxe entre les membres gauches et membres droits. L'idée étant - que l'inference de type permet d'éviter le besoin de déclarer tous - les types. -\end{itemize} - -\subsection{Autres extensions} - -\subsubsection{Lieur multiple} - -L'écriture de types en présence de polymorphisme est souvent assez -pénible: -\begin{verbatim} -Check !(A:Set) (x:A) (B:Set) (y:B). P A x B y; -\end{verbatim} - -On pourrait avoir des déclarations introduisant à la fois un type -d'une certaine sorte et une variable de ce type: -\begin{verbatim} -Check !(x:A:Set) (y:B:Set). P A x B y; -\end{verbatim} - -Noter que l'on aurait pu écrire: -\begin{verbatim} -Check !A x B y. P A (x:A:Set) B (y:B:Set); -\end{verbatim} - -\section{Syntaxe des tactiques} - -\subsection{Questions diverses} - -Changer ``Pattern nl c ... nl c'' en ``Pattern [ nl ] c ... [ nl ] c'' -pour permettre des chiffres seuls dans la catégorie syntaxique des -termes. - -Par uniformité remplacer ``Unfold nl c'' par ``Unfold [ nl ] c'' ? - -Même problème pour l'entier de Specialize (ou virer Specialize ?) ? - -\subsection{Questions en suspens} - -\verb=EAuto= : deux syntaxes différentes pour la recherche en largeur -et en profondeur ? Quelle recherche par défaut ? - -\section*{Remarques pêle-mêle (HH)} - -Autoriser la syntaxe - -\begin{verbatim} -Variable R (a : A) (b : B) : Prop. -Hypotheses H (a : A) (b : B) : Prop; Y (u : U) : V. -Variables H (a : A) (b : B), J (k : K) : nat; Z (v : V) : Set. -\end{verbatim} - -Renommer eqT, refl_eqT, eqT_ind, eqT_rect, eqT_rec en eq, refl_equal, etc. -Remplacer == en =. - -Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ?? - -\section{Moulinette} - -\begin{itemize} - -\item Mettre \verb=/= et * au même niveau dans R. - -\item Changer la précédence du - unaire dans R. - -\item Ajouter Require Arith par necessite si Require ArithRing ou Require ZArithRing. - -\item Ajouter Require ZArith par necessite si Require ZArithRing ou Require Omega. - -\item Enlever le Export de Bool, Arith et ZARith de Ring quand inapproprié et -l'ajouter à côté des Require Ring. - -\item Remplacer "Check n" par "n:Check ..." - -\item Renommer Variable/Hypothesis hors section en Parameter/Axiom. - -\item Renommer les \verb=command0=, \verb=command1=, ... \verb=lcommand= etc en -\verb=constr0=, \verb=constr1=, ... \verb=lconstr=. - -\item Remplacer les noms Coq.omega.Omega par Coq.Omega ... - -\item Remplacer AddPath par Add LoadPath (ou + court) - -\item Unify + and \{\}+\{\} and +\{\} using Prop $\leq$ Set ?? - -\item Remplacer Implicit Arguments On/Off par Set/Unset Implicit Arguments. - -\item La syntaxe \verb=Intros (a,b)= est inutile, \verb=Intros [a b]= fait l'affaire. - -\item Virer \verb=Goal= sans argument (synonyme de \verb=Proof= et sans effets). - -\item Remplacer Save. par Qed. - -\item Remplacer \verb=Zmult_Zplus_distr= par \verb=Zmult_plus_distr_r= -et \verb=Zmult_plus_distr= par \verb=Zmult_plus_distr_l=. - -\end{itemize} - -\end{document} diff --git a/dev/doc/notes-on-conversion.v b/dev/doc/notes-on-conversion.v deleted file mode 100644 index a81f170c63..0000000000 --- a/dev/doc/notes-on-conversion.v +++ /dev/null @@ -1,73 +0,0 @@ -(**********************************************************************) -(* A few examples showing the current limits of the conversion algorithm *) -(**********************************************************************) - -(*** We define (pseudo-)divergence from Ackermann function ***) - -Definition ack (n : nat) := - (fix F (n0 : nat) : nat -> nat := - match n0 with - | O => S - | S n1 => - fun m : nat => - (fix F0 (n2 : nat) : nat := - match n2 with - | O => F n1 1 - | S n3 => F n1 (F0 n3) - end) m - end) n. - -Notation OMEGA := (ack 4 4). - -Definition f (x:nat) := x. - -(* Evaluation in tactics can somehow be controlled *) -Lemma l1 : OMEGA = OMEGA. -reflexivity. (* succeed: identity *) -Qed. (* succeed: identity *) - -Lemma l2 : OMEGA = f OMEGA. -reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) -Abort. (* but it reduces the right side first! *) - -Lemma l3 : f OMEGA = OMEGA. -reflexivity. (* succeed: reduce left side first *) -Qed. (* succeed: expected concl (the one with f) is on the left *) - -Lemma l4 : OMEGA = OMEGA. -assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) -unfold f in H. (* succeed: no type-checking *) -exact H. (* succeed: identity *) -Qed. (* fail: "f" is on the left *) - -(* This example would fail whatever the preferred side is *) -Lemma l5 : OMEGA = f OMEGA. -unfold f. -assert (f OMEGA = OMEGA) by reflexivity. -unfold f in H. -exact H. -Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) - -(**********************************************************************) -(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) -(* (proof of span_ind_uninject_prop *) - -In the proof, a problem of the form (Equal S t1 t2) -is "simpl"ified, then "red"uced to (Equal S' t1 t1) -where the new t1's are surrounded by invisible coercions. -A reflexivity steps conclude the proof. - -The trick is that Equal projects the equality in the setoid S, and -that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). - -At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) -and the algorithm is to first compare S and S', and t1 and t2. -Unfortunately it does not work, and since t1 and t2 involve concrete -instances of algebraic structures, it takes a lot of time to realize that -it is not convertible. - -The only hope to improve this problem is to observe that S' hides -(behind two indirections) a Setoid constructor. This could be the -argument to solve the problem. - - diff --git a/dev/doc/old_svn_branches.txt b/dev/doc/old_svn_branches.txt deleted file mode 100644 index ee56ee24e9..0000000000 --- a/dev/doc/old_svn_branches.txt +++ /dev/null @@ -1,33 +0,0 @@ -## During the migration to git, some old branches and tags have not been -## converted to directly visible git branches or tags. They are still there -## in the archive, their names on the gforge repository are in the 3rd -## column below (e.g. remotes/V8-0-bugfix). After a git clone, they -## could always be accessed by their git hashref (2nd column below). - -# SVN # GIT # Symbolic name on gforge repository - -r5 d2f789d remotes/tags/start -r1714 0605b7c remotes/V7 -r2583 372f3f0 remotes/tags/modules-2-branching -r2603 6e15d9a remotes/modules -r2866 76a93fa remotes/tags/modules-2-before-grammar -r2951 356f749 remotes/tags/before-modules -r2952 8ee67df remotes/tags/modules-2-update -r2956 fb11bd9 remotes/modules-2 -r3193 4d23172 remotes/mowgli -r3194 c91e99b remotes/tags/mowgli-before-merge -r3500 5078d29 remotes/mowgli2 -r3672 63b0886 remotes/V7-3-bugfix -r5086 bdceb72 remotes/V7-4-bugfix -r5731 a274456 remotes/recriture -r9046 e19553c remotes/tags/trunk -r9146 b38ce05 remotes/coq-diff-tool -r9786 a05abf8 remotes/ProofIrrelevance -r10294 fdf8871 remotes/InternalExtraction -r10408 df97909 remotes/TypeClasses -r10673 4e19bca remotes/bertot -r11130 bfd1cb3 remotes/proofs -r12282 a726b30 remotes/revised-theories -r13855 bae3a8e remotes/native -r14062 b77191b remotes/recdef -r16421 9f4bfa8 remotes/V8-0-bugfix diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis deleted file mode 100644 index ac54fa6f73..0000000000 --- a/dev/doc/perf-analysis +++ /dev/null @@ -1,167 +0,0 @@ -Performance analysis (trunk repository) ---------------------------------------- - -Jun 7, 2010: delayed re-typing of Ltac instances in matching - (-1% on HighSchoolGeometry, -2% on JordanCurveTheorem) - -Jun 4, 2010: improvement in eauto and type classes inference by removing - systematic preparation of debugging pretty-printing streams (std_ppcmds) - (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk; - -6% in HighSchoolGeometry) - -Apr 19, 2010: small improvement obtained by reducing evar instantiation - from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert, - -2% AreaMethod, -15% in Ssreflect) - -Apr 17, 2010: small improvement obtained by not repeating unification - twice in auto (-2% in Compcert, -2% in Algebra) - -Feb 15, 2010: Global decrease due to unicode inefficiency repaired - -Jan 8, 2010: Global increase due to an inefficiency in unicode treatment - -Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to - exact (generally not significative but, e.g., +25% on Subst, +8% on - ZFC, +5% on AreaMethod) - -Oct 19, 2009: Change in modules (CoLoR +35%) - -Aug 9, 2009: new files added in AreaMethod - -May 21, 2008: New version of CoRN - (needs +84% more time to compile) - -Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu) - (+28% CoRN) - -Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug - fixes, control of zeta in rewrite, auto (??)) - (-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg, - but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%) - -Mar 11, 2008: - (+19% PersistentUnionFind wrt Mar 3, +21% Angles, - +270% Continuations between 7/3 and 18/4) - -Mar 7, 2008: - (-10% PersistentUnionFind wrt Mar 3) - -Feb 20, 2008: temporary 1-day slow down - (+64% LinAlg) - -Feb 14, 2008: - (-10% PersistentUnionFind, -19% Groups) - -Feb 7, 8, 2008: temporary 2-days long slow down - (+20 LinAlg, +50% BDDs) - -Feb 2, 2008: many updates of the module system - (-13% LinAlg, -50% AMM11262, -5% Goedel, -1% PersistentUnionFind, - -42% ExactRealArithmetic, -41% Icharate, -42% Kildall, -74% SquareMatrices) - -Jan 1, 2008: merge of TypeClasses branch - (+8% PersistentUnionFind, +36% LinAlg, +76% Goedel) - -Nov 16, 17, 2007: - (+18% Cantor, +4% LinAlg, +27% IEEE1394 on 2 days) - -Nov 8, 2007: - (+18% Cantor, +16% LinAlg, +55% Continuations, +200% IEEE1394, +170% CTLTCTL, - +220% SquareMatrices) - -Oct 29, V8.1 (+ 3% geometry but CoRN, Godel, Kildall, Stalmark stables) - -Between Oct 12 and Oct 27, 2007: inefficiency temporarily introduced in the - tactic interpreter (from revision 10222 to 10267) - (+22% CoRN, +10% geometry, ...) - -Sep 16, 2007: - (+16% PersistentUnionFind on 3 days, LinAlg stable, - -Sep 4, 2007: - (+26% PersistentUnionFind, LinAlg stable, - -Jun 6, 2007: optimization of the need for type unification in with-bindings - (-3.5% Stalmark, -6% Kildall) - -May 20, 21, 22, 2007: improved inference of with-bindings (including activation - of unification on types) - (+4% PICALC, +5% Stalmark, +7% Kildall) - -May 11, 2007: added primitive integers (+6% CoLoR, +7% CoRN, +5% FSets, ...) - -Between Feb 22 and March 16, 2007: bench temporarily moved on JMN's - computer (-25% CoRN, -25% Fairisle, ...) - -Oct 29 and Oct 30, 2006: abandoned attempt to add polymorphism on definitions - (+4% in general during these two days) - -Oct 17, 2006: improvement in new field [r9248] - (QArith -3%, geometry: -2%) - -Oct 5, 2006: fixing wrong unification of Meta below binders - (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, LinAlg: +7%, - DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%) - -Sep 26, 2006: new field [r9178-9181] - (QArith: -16%, geometry: -5%, Float: +6%, BDDS:+5% but no ring in it) - - Sep 12, 2006: Rocq/AREA_METHOD extended (~ 530s) - Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s) - May 30, 2006: Nancy/CoLoR added (~ 319s) - -May 23, 2006: new, lighter version of polymorphic inductive types - (CoRN: -27%, back to Mar-24 time) - -May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -) - -May 5, 2006: improvement in closure (array instead of lists) - (e.g. CatsInZFC: -10%, CoRN: -3%, - -May 23, 2006: polymorphic inductive types (precise, heavy algorithm) - (CoRN: +37%) - - Dec 29, 2005: new test and use of -vm in Stalmarck - - Dec 27, 2005: contrib Karatsuba added (~ 30s) - -Dec 28, 2005: size decrease - mainly due to Defined moved to Qed in FSets (reduction from 95M to 7Mo) - -Dec 1-14, 2005: benchmarking server down - between the two dates: Godel: -10%, CoRN: -10% - probably due to changes around vm (new informative Cast, - change of equality in named_context_val) - - Oct 6, 2005: contribs IPC and Tait added (~ 22s and ~ 25s) - -Aug 19, 2005: time decrease after application of "Array.length x=0" Xavier's - suggestions for optimisation - (e.g. Nijmegen/QArith: -3%, Nijmegen/CoRN: -7%, Godel: -3%) - - Aug 1, 2005: contrib Kildall added (~ 65s) - -Jul 26-Aug 2, 2005: bench down - -Jul 14-15, 2005: 4 contribs failed including CoRN - -Jul 14, 2005: time increase after activation of "closure optimisation" - (e.g. Nijmegen/QArith: +8%, Nijmegen/CoRN: +3%, Godel: +13%) - - Jul 7, 2005: adding contrib Fermat4 - - Jun 17, 2005: contrib Goodstein extended and moved to CantorOrdinals (~ 30s) - - May 19, 2005: contrib Goodstein and prfx (~ 9s) added - -Apr 21, 2005: strange time decrease - (could it be due to the change of Back and Reset mechanism) - (e.g. Nijmegen/CoRN: -2%, Nijmegen/QARITH: -4%, Godel: -11%) - -Mar 20, 2005: fixed Logic.with_check bug - global time decrease (e.g. Nijmegen/CoRN: -3%, Nijmegen/QARITH: -1.5%) - -Jan 31-Feb 8, 2005: small instability - (e.g. CoRN: ~2015s -> ~1999s -> ~2032s, Godel: ~340s -> ~370s) - - Jan 13, 2005: contrib SumOfTwoSquare added (~ 38s) diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex deleted file mode 100644 index 1c4913d201..0000000000 --- a/dev/doc/versions-history.tex +++ /dev/null @@ -1,451 +0,0 @@ -\documentclass[a4paper]{book} -\usepackage{fullpage} -\usepackage[utf8]{inputenc} -\usepackage[T1]{fontenc} -\usepackage{amsfonts} - -\newcommand{\feature}[1]{{\em #1}} - -\begin{document} - -\begin{center} -\begin{huge} -A history of Coq versions -\end{huge} -\end{center} -\bigskip - -\centerline{\large 1984-1989: The Calculus of Constructions} - -\bigskip -\centerline{\large (see README.V1-V5 for details)} -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -version & date & comments \\ -\hline - -CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\ - & 1984 to 13 February 1985 & \feature{of Constructions}, implementation \\ - & frozen 22 December 1984 & language is a predecessor of CAML\\ - -CONSTR V1.11& mention of dates from 6 December\\ - & 1984 to 19 February 1985 (freeze date) &\\ - -CoC V2.8& dated 16 December 1985 (freeze date)\\ - -CoC V2.9& & \feature{cumulative hierarchy of universes}\\ - -CoC V2.13& dated 25 June 1986 (freeze date)\\ - -CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\ - & dated 20 November 1986 & implementation language now named CAML\\ - -CoC V3.2& dated 27 November 1986\\ - -CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\ - -CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\ - -CoC V4.1& dated 24 July 1987 (freeze date)\\ - -CoC V4.2& dated 10 September 1987\\ - -CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\ - & frozen November 1987 & \feature{section mechanism}\\ - & & \feature{logical vs computational content (sorte Spec)}\\ - & & \feature{LCF engine}\\ - -CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\ - & frozen March 1988\\ - -CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\ - & demonstrated in June 1988\\ - -CoC V4.6& dated 1 September 1988 & start of LEGO fork\\ - -CoC V4.7& started 6 September 1988 \\ - -CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\ - -CoC V4.8.5& dated 1 February 1989 & \\ - -CoC V4.9& dated 1 March 1989 (release date)\\ - -CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\ -\end{tabular} - -\bigskip - -\noindent Note: CoC above stands as an abbreviation for {\em Calculus of - Constructions}, official name of the system. -\bigskip -\bigskip - -\newpage - -\centerline{\large 1989-now: The Calculus of Inductive Constructions} -\mbox{}\\ -\centerline{I- RCS archives in Caml and Caml-Light} -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -version & date & comments \\ -\hline -Coq V5.0 & headers dated 1 January 1990 & internal use \\ - & & \feature{inductive types with primitive recursor}\\ - -Coq V5.1 & ended 12 July 1990 & internal use \\ - -Coq V5.2 & log dated 4 October 1990 & internal use \\ - -Coq V5.3 & log dated 12 October 1990 & internal use \\ - -Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\ - -Coq V5.5 & started 6 December 1990 & internal use \\ - -Coq V5.6 beta & 1991 & first announce of the new Coq based on CIC \\ - & & (in May at TYPES?)\\ - & & \feature{rewrite tactic}\\ - & & use of RCS at least from February 1991\\ - -Coq V5.6& 7 August 1991 & \\ - -Coq V5.6 patch 1& 13 November 1991 & \\ - -Coq V5.6 (last) & mention of 27 November 1992\\ - -Coq V5.7.0& 1992 & translation to Caml-Light \footnotemark\\ - -Coq V5.8& 12 February 1993 & \feature{Program} (version 1), \feature{simpl}\\ - -& & has the xcoq graphical interface\\ - -& & first explicit notion of standard library\\ - -& & includes a MacOS 7-9 version\\ - -Coq V5.8.1& released 28 April 1993 & with xcoq graphical interface and MacOS 7-9 support\\ - -Coq V5.8.2& released 9 July 1993 & with xcoq graphical interface and MacOS 7-9 support\\ - -Coq V5.8.3& released 6 December 1993 % Announce on coq-club - & with xcoq graphical interface and MacOS 7-9 support\\ - - & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\ - -Coq V5.9 alpha& 7 July 1993 & -experimental version based on evars refinement \\ - & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\ - & & version), not released\\ - -& March 1994 & \feature{tauto} tactic in V5.9 branch\\ - -Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\ - & & not released\\ -\end{tabular} - -\bigskip -\bigskip - -\footnotetext{archive lost?} - -\newpage - -\centerline{II- Starting with CVS archives in Caml-Light} -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -version & date & comments \\ -\hline -Coq V5.10 ``Murthy'' & 22 January 1994 & -introduction of the ``DOPN'' structure\\ - & & \feature{eapply/prolog} tactics\\ - & & private use of cvs on madiran.inria.fr\\ - -Coq V5.10.1 ``Murthy''& 15 April 1994 \\ - -Coq V5.10.2 ``Murthy''& 19 April 1994 & \feature{mutual inductive types, fixpoint} (from Lyon's branch)\\ - -Coq V5.10.3& 28 April 1994 \\ - -Coq V5.10.5& dated 13 May 1994 & \feature{inversion}, \feature{discriminate}, \feature{injection} \\ - & & \feature{type synthesis of hidden arguments}\\ - & & \feature{separate compilation}, \feature{reset mechanism} \\ - -Coq V5.10.6& dated 30 May 1994\\ -Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\ - -Coq V5.10.9& announced on 17 August 1994 & - % Announced by Catherine Parent on coqdev - % Version avec une copie de THEORIES pour les inductifs mutuels - \\ - -Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\ -Coq Rocq's archive & on 16 February 1995 & set up of ``V5.10'' cvs archive on pauillac.inria.fr \\ - & & with first dispatch of files over src/* directories\\ - -Coq V5.10.12& dated 30 January 1995 & on Lyon's cvs\\ - -Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\ - -Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\ - -Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW - -Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\ - & & MS-DOS version released on 30 October 1995\\ - % still available at ftp://ftp.ens-lyon.fr/pub/LIP/COQ/V5.10.14.old/ in May 2009 - % also known in /net/pauillac/constr archive as ``V5.11 old'' \\ - % A copy of Coq V5.10.15 dated 1 January 1996 coming from Lyon's CVS is - % known in /net/pauillac/constr archive as ``V5.11 new old'' \\ - -Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\ - % Announce on coq-club by BW - % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive - & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW - -Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\ -\end{tabular} - -\bigskip -\bigskip - -\newpage - -\centerline{III- A CVS archive in Caml Special Light} -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -version & date & comments \\ -\hline -Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\ - & & to Caml Special Light (to later become Objective Caml)\\ - & & has implicit arguments and coercions\\ - & & has coinductive types\\ - -Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\ - & & \feature{omega} [10-9-1996] \\ - & & \feature{natural language proof printing} (stopped from Coq V7) [6-9-1996]\\ - & & \feature{pattern-matching compilation} [7-10-1996]\\ - & & \feature{ring} (version 1, ACSimpl) [11-12-1996]\\ - -Coq V6.1& released December 1996 & \\ - -Coq V6.2beta& released 30 January 1998 & % Announced on coq-club 2-2-1998 by CP - \feature{SearchIsos} (stopped from Coq V7) [9-11-1997]\\ - & & grammar extension mechanism moved to Camlp4 [12-6-1997]\\ - & & \feature{refine tactic}\\ - & & includes a Windows version\\ - -Coq V6.2& released 4 May 1998 & % Announced on coq-club 5-5-1998 by CP - \feature{ring} (version 2) [7-4-1998] \\ - -Coq V6.2.1& released 23 July 1998\\ - -Coq V6.2.2 beta& released 30 January 1998\\ - -Coq V6.2.2& released 23 September 1998\\ - -Coq V6.2.3& released 22 December 1998 & \feature{Real numbers library} [from 13-11-1998] \\ - -Coq V6.2.4& released 8 February 1999\\ - -Coq V6.3& released 27 July 1999 & \feature{autorewrite} [25-3-1999]\\ - & & \feature{Correctness} (deprecated in V8, led to Why) [28-10-1997]\\ - -Coq V6.3.1& released 7 December 1999\\ -\end{tabular} -\medskip -\bigskip - -\newpage -\centerline{IV- New CVS, back to a kernel-centric implementation} -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -version & date & comments \\ -\hline -Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\ - & & \feature{kernel-centric} architecture \\ - & & more care for outside readers\\ - & & (indentation, ocaml warning protection)\\ -Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\ -Coq V7.0beta2& released 2 February 2001\\ - -Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\ - & & \feature{field} (version 1) [19-4-2001], \feature{fourier} [20-4-2001] \\ - -Coq V7.1& released 25 September 2001 & \feature{setoid rewriting} (version 1) [10-7-2001]\\ - -Coq V7.2& released 10 January 2002\\ - -Coq V7.3& released 16 May 2002\\ - -Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\ - & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\ - -Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\ -\end{tabular} - -\medskip -\bigskip - -\centerline{V- New concrete syntax} -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -version & date & comments \\ -\hline -Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\ - -Coq V8.0pl1& released 18 July 2004\\ - -Coq V8.0pl2& released 22 January 2005\\ - -Coq V8.0pl3& released 13 January 2006\\ - -Coq V8.0pl4& released 26 January 2007\\ - -Coq ``svn'' archive & 6 March 2006 & cvs archive moved to subversion control management\\ - -Coq V8.1beta& released 12 July 2006 & \feature{bytecode compiler} [20-10-2004] \\ - & & \feature{setoid rewriting} (version 2) [3-9-2004]\\ - & & \feature{functional induction} [1-2-2006]\\ - & & \feature{Strings library} [8-2-2006], \feature{FSets/FMaps library} [15-3-2006] \\ - & & \feature{Program} (version 2, Russell) [5-3-2006] \\ - & & \feature{declarative language} [20-9-2006]\\ - & & \feature{ring} (version 3) [18-11-2005]\\ - -Coq V8.1gamma& released 7 November 2006 & \feature{field} (version 2) [29-9-2006]\\ - -Coq V8.1& released 10 February 2007 & \\ - -Coq V8.1pl1& released 27 July 2007 & \\ -Coq V8.1pl2& released 13 October 2007 & \\ -Coq V8.1pl3& released 13 December 2007 & \\ -Coq V8.1pl4& released 9 October 2008 & \\ - -Coq V8.2 beta1& released 13 June 2008 & \\ -Coq V8.2 beta2& released 19 June 2008 & \\ -Coq V8.2 beta3& released 27 June 2008 & \\ -Coq V8.2 beta4& released 8 August 2008 & \\ - -Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \feature{machine words} [11-5-2007]\\ - & & \feature{big integers} [11-5-2007], \feature{abstract arithmetics} [9-2007]\\ - & & \feature{setoid rewriting} (version 3) [18-12-2007] \\ - & & \feature{micromega solving platform} [19-5-2008]\\ - -& & a first package released on -February 11 was incomplete\\ -Coq V8.2pl1& released 4 July 2009 & \\ -Coq V8.2pl2& released 29 June 2010 & \\ -\end{tabular} - -\medskip -\bigskip - -\newpage -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\ -Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\ -Coq V8.3pl1& released 23 December 2010 & \\ -Coq V8.3pl2& released 19 April 2011 & \\ -Coq V8.3pl3& released 19 December 2011 & \\ -Coq V8.3pl3& released 26 March 2012 & \\ -Coq V8.3pl5& released 28 September 2012 & \\ -Coq V8.4 beta & released 27 December 2011 & \feature{modular arithmetic library} [2010-2012]\\ -&& \feature{vector library} [10-12-2010]\\ -&& \feature{structured scripts} [22-4-2010]\\ -&& \feature{eta-conversion} [20-9-2010]\\ -&& \feature{new proof engine available} [10-12-2010]\\ -Coq V8.4 beta2 & released 21 May 2012 & \\ -Coq V8.4 & released 12 August 2012 &\\ -Coq V8.4pl1& released 22 December 2012 & \\ -Coq V8.4pl2& released 4 April 2013 & \\ -Coq V8.4pl3& released 21 December 2013 & \\ -Coq V8.4pl4& released 24 April 2014 & \\ -Coq V8.4pl5& released 22 October 2014 & \\ -Coq V8.4pl6& released 9 April 2015 & \\ - -Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ -&& \feature{asynchonous evaluation} [8-8-2013]\\ -&& \feature{new proof engine deployed} [2-11-2013]\\ -&& \feature{universe polymorphism} [6-5-2014]\\ -&& \feature{primitive projections} [6-5-2014]\\ -&& \feature{miscellaneous optimizations}\\ - -Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ - -Coq V8.5 & released 22 January 2016 & \\ - -Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\ -&& \feature{Ltac profiling} [14-6-2016]\\ -&& \feature{warning system} [29-6-2016]\\ -&& \feature{miscellaneous optimizations}\\ - -Coq V8.6 & released 14 December 2016 & \\ - -Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\ -&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\ -&& \feature{further optimizations}\\ - -Coq V8.7 beta 2 & released 6 October 2017 & \\ - -Coq V8.7.0 & released 18 October 2017 & \\ - -Coq V8.7.1 & released 15 December 2017 & \\ - -Coq V8.7.2 & released 17 February 2018 & \\ - -Coq V8.8 beta1 & released 19 March 2018 & \\ - -Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\ -&& \feature{effort towards better documented, better structured ML API}\\ -&& \feature{miscellaneous changes/improvements of existing features}\\ - -\end{tabular} - -\medskip -\bigskip -\newpage - -\centerline{\large Other important dates} -\mbox{}\\ -\mbox{}\\ -\begin{tabular}{l|l|l} -version & date & comments \\ -\hline -Lechenadec's version in C& mention of \\ - & 13 January 1985 on \\ - & some vernacular files\\ -Set up of the coq-club mailing list & 28 July 1993\\ - -Coq V6.0 ``evars'' & & experimentation based on evars -refinement started \\ - & & in 1991 by Gilles from V5.6 beta,\\ - & & with work by Hugo in July 1992\\ - -Coq V6.0 ``evars'' ``light'' & July 1993 & Hugo's port of the first -evars-based experimentation \\ - & & to Coq V5.7, version from October/November -1992\\ - -CtCoq & released 25 October 1995 & first beta-version \\ % Announce on coq-club by Janet - -Proto with explicit substitutions & 1997 &\\ - -Coq web site & 15 April 1998 & new site designed by David Delahaye \\ - -Coq web site & January 2004 & web site new style \\ - & & designed by Julien Narboux and Florent Kirchner \\ - -Coq web site & April 2009 & new Drupal-based site \\ - & & designed by Jean-Marc Notin and Denis Cousineau \\ - -\end{tabular} - -\end{document} -- cgit v1.2.3