From 6cf8d80ac0a9869d97373d6813441eabebce8980 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 23 Feb 2006 13:58:10 +0000 Subject: Nettoyage de l'archive doc et restructuration avant intégration à l'archive principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/AddRefMan-pre.tex | 58 - doc/Anomalies.tex | 34 - doc/Cases.tex | 698 --------- doc/Changes.html | 126 -- doc/Changes.tex | 24 - doc/ChangesV6-2.tex | 921 ------------ doc/ChangesV6-3-1.tex | 160 -- doc/ChangesV6-3.tex | 302 ---- doc/ChangesV7-0.tex | 757 ---------- doc/Coercion.tex | 541 ------- doc/Correctness.tex | 930 ------------ doc/Extraction.tex | 664 --------- doc/Helm.tex | 317 ---- doc/INSTALL | 65 + doc/LICENCE | 606 ++++++++ doc/Library.tex | 60 - doc/Makefile.rt | 43 + doc/Natural.tex | 425 ------ doc/Omega.tex | 226 --- doc/Polynom.tex | 504 ------- doc/Program.tex | 850 ----------- doc/Recursive-Definition.tex | 251 ---- doc/RefMan-add.tex | 54 - doc/RefMan-cas.tex | 692 --------- doc/RefMan-cic.tex | 1480 ------------------- doc/RefMan-coi.tex | 406 ----- doc/RefMan-com.tex | 280 ---- doc/RefMan-cover.tex | 46 - doc/RefMan-ext.tex | 1173 --------------- doc/RefMan-gal.tex | 1451 ------------------ doc/RefMan-ide.tex | 327 ----- doc/RefMan-ind.tex | 498 ------- doc/RefMan-int.tex | 147 -- doc/RefMan-lib.tex | 1102 -------------- doc/RefMan-ltac.tex | 1057 ------------- doc/RefMan-mod.tex | 396 ----- doc/RefMan-modr.tex | 586 -------- doc/RefMan-oth.tex | 773 ---------- doc/RefMan-pre.tex | 519 ------- doc/RefMan-pro.tex | 389 ----- doc/RefMan-syn.tex | 1016 ------------- doc/RefMan-tac.tex | 3096 --------------------------------------- doc/RefMan-tacex.tex | 1208 --------------- doc/RefMan-tus.tex | 2015 ------------------------- doc/RefMan-uti.tex | 276 ---- doc/RefMan.txt | 74 - doc/Reference-Manual.tex | 124 -- doc/Setoid.tex | 158 -- doc/Translator.tex | 898 ------------ doc/Tutorial-cover.tex | 48 - doc/Tutorial.tex | 1584 -------------------- doc/biblio.bib | 1144 --------------- doc/book-html.sty | 133 -- doc/common/macros.tex | 497 +++++++ doc/common/title.tex | 89 ++ doc/coq-html.sty | 6 - doc/coqdoc.tex | 476 ------ doc/coqide-queries.png | Bin 27316 -> 0 bytes doc/coqide.png | Bin 20953 -> 0 bytes doc/cover.html | 36 - doc/discussion-syntaxe.txt | 349 ----- doc/faq.tex | 800 ---------- doc/faq/FAQ.tex | 2441 ++++++++++++++++++++++++++++++ doc/faq/axioms.eps | 378 +++++ doc/faq/axioms.fig | 84 ++ doc/faq/axioms.png | Bin 0 -> 10075 bytes doc/faq/fk.bib | 2215 ++++++++++++++++++++++++++++ doc/faq/hevea.sty | 78 + doc/faq/interval_discr.v | 419 ++++++ doc/headers.tex | 102 -- doc/macros.tex | 497 ------- doc/main-0.html | 29 - doc/main.html | 13 - doc/newfaq/axioms.eps | 378 ----- doc/newfaq/axioms.fig | 84 -- doc/newfaq/faq.cls | 70 - doc/newfaq/faq.sty | 883 ----------- doc/newfaq/fk.bib | 2215 ---------------------------- doc/newfaq/interval_discr.v | 419 ------ doc/newfaq/main.tex | 2441 ------------------------------ doc/newfaq/main.v001.gif | 0 doc/newfaq/run.sh | 6 - doc/refman/AddRefMan-pre.tex | 58 + doc/refman/Cases.tex | 698 +++++++++ doc/refman/Coercion.tex | 541 +++++++ doc/refman/Extraction.tex | 664 +++++++++ doc/refman/Helm.tex | 317 ++++ doc/refman/Natural.tex | 425 ++++++ doc/refman/Omega.tex | 226 +++ doc/refman/Polynom.tex | 504 +++++++ doc/refman/RefMan-add.tex | 54 + doc/refman/RefMan-cas.tex | 692 +++++++++ doc/refman/RefMan-cic.tex | 1480 +++++++++++++++++++ doc/refman/RefMan-coi.tex | 406 +++++ doc/refman/RefMan-com.tex | 280 ++++ doc/refman/RefMan-ext.tex | 1173 +++++++++++++++ doc/refman/RefMan-gal.tex | 1451 ++++++++++++++++++ doc/refman/RefMan-ide.tex | 327 +++++ doc/refman/RefMan-ind.tex | 498 +++++++ doc/refman/RefMan-int.tex | 147 ++ doc/refman/RefMan-lib.tex | 1102 ++++++++++++++ doc/refman/RefMan-ltac.tex | 1057 +++++++++++++ doc/refman/RefMan-mod.tex | 396 +++++ doc/refman/RefMan-modr.tex | 586 ++++++++ doc/refman/RefMan-oth.tex | 773 ++++++++++ doc/refman/RefMan-pre.tex | 519 +++++++ doc/refman/RefMan-pro.tex | 389 +++++ doc/refman/RefMan-syn.tex | 1016 +++++++++++++ doc/refman/RefMan-tac.tex | 3096 +++++++++++++++++++++++++++++++++++++++ doc/refman/RefMan-tacex.tex | 1208 +++++++++++++++ doc/refman/RefMan-tus.tex | 2015 +++++++++++++++++++++++++ doc/refman/RefMan-uti.tex | 276 ++++ doc/refman/Reference-Manual.tex | 124 ++ doc/refman/Setoid.tex | 158 ++ doc/refman/biblio.bib | 1144 +++++++++++++++ doc/refman/coqdoc.tex | 476 ++++++ doc/refman/coqide-queries.png | Bin 0 -> 27316 bytes doc/refman/coqide.png | Bin 0 -> 20953 bytes doc/refman/cover.html | 36 + doc/refman/headers.tex | 102 ++ doc/refman/hevea.sty | 78 + doc/refman/index.html | 29 + doc/rt/RefMan-cover.tex | 46 + doc/rt/Tutorial-cover.tex | 48 + doc/stdlib/Library.tex | 60 + doc/syntax.txt | 68 - doc/title.tex | 89 -- doc/tools/Translator.tex | 898 ++++++++++++ doc/tov8 | 5 - doc/tradv8.ml4 | 105 -- doc/tutorial/Tutorial.tex | 1584 ++++++++++++++++++++ doc/v8.txt | 50 - 132 files changed, 34072 insertions(+), 40119 deletions(-) delete mode 100644 doc/AddRefMan-pre.tex delete mode 100755 doc/Anomalies.tex delete mode 100644 doc/Cases.tex delete mode 100644 doc/Changes.html delete mode 100755 doc/Changes.tex delete mode 100755 doc/ChangesV6-2.tex delete mode 100644 doc/ChangesV6-3-1.tex delete mode 100644 doc/ChangesV6-3.tex delete mode 100755 doc/ChangesV7-0.tex delete mode 100644 doc/Coercion.tex delete mode 100644 doc/Correctness.tex delete mode 100755 doc/Extraction.tex delete mode 100644 doc/Helm.tex create mode 100644 doc/INSTALL create mode 100644 doc/LICENCE delete mode 100755 doc/Library.tex create mode 100644 doc/Makefile.rt delete mode 100755 doc/Natural.tex delete mode 100755 doc/Omega.tex delete mode 100644 doc/Polynom.tex delete mode 100644 doc/Program.tex delete mode 100755 doc/Recursive-Definition.tex delete mode 100755 doc/RefMan-add.tex delete mode 100755 doc/RefMan-cas.tex delete mode 100755 doc/RefMan-cic.tex delete mode 100755 doc/RefMan-coi.tex delete mode 100755 doc/RefMan-com.tex delete mode 100644 doc/RefMan-cover.tex delete mode 100644 doc/RefMan-ext.tex delete mode 100644 doc/RefMan-gal.tex delete mode 100644 doc/RefMan-ide.tex delete mode 100755 doc/RefMan-ind.tex delete mode 100755 doc/RefMan-int.tex delete mode 100755 doc/RefMan-lib.tex delete mode 100644 doc/RefMan-ltac.tex delete mode 100644 doc/RefMan-mod.tex delete mode 100644 doc/RefMan-modr.tex delete mode 100644 doc/RefMan-oth.tex delete mode 100755 doc/RefMan-pre.tex delete mode 100755 doc/RefMan-pro.tex delete mode 100755 doc/RefMan-syn.tex delete mode 100644 doc/RefMan-tac.tex delete mode 100644 doc/RefMan-tacex.tex delete mode 100755 doc/RefMan-tus.tex delete mode 100755 doc/RefMan-uti.tex delete mode 100644 doc/RefMan.txt delete mode 100644 doc/Reference-Manual.tex delete mode 100644 doc/Setoid.tex delete mode 100644 doc/Translator.tex delete mode 100644 doc/Tutorial-cover.tex delete mode 100755 doc/Tutorial.tex delete mode 100755 doc/biblio.bib delete mode 100644 doc/book-html.sty create mode 100755 doc/common/macros.tex create mode 100755 doc/common/title.tex delete mode 100644 doc/coq-html.sty delete mode 100644 doc/coqdoc.tex delete mode 100644 doc/coqide-queries.png delete mode 100644 doc/coqide.png delete mode 100644 doc/cover.html delete mode 100644 doc/discussion-syntaxe.txt delete mode 100644 doc/faq.tex create mode 100644 doc/faq/FAQ.tex create mode 100644 doc/faq/axioms.eps create mode 100644 doc/faq/axioms.fig create mode 100644 doc/faq/axioms.png create mode 100644 doc/faq/fk.bib create mode 100644 doc/faq/hevea.sty create mode 100644 doc/faq/interval_discr.v delete mode 100644 doc/headers.tex delete mode 100755 doc/macros.tex delete mode 100644 doc/main-0.html delete mode 100644 doc/main.html delete mode 100644 doc/newfaq/axioms.eps delete mode 100644 doc/newfaq/axioms.fig delete mode 100644 doc/newfaq/faq.cls delete mode 100644 doc/newfaq/faq.sty delete mode 100644 doc/newfaq/fk.bib delete mode 100644 doc/newfaq/interval_discr.v delete mode 100644 doc/newfaq/main.tex delete mode 100644 doc/newfaq/main.v001.gif delete mode 100755 doc/newfaq/run.sh create mode 100644 doc/refman/AddRefMan-pre.tex create mode 100644 doc/refman/Cases.tex create mode 100644 doc/refman/Coercion.tex create mode 100755 doc/refman/Extraction.tex create mode 100644 doc/refman/Helm.tex create mode 100755 doc/refman/Natural.tex create mode 100755 doc/refman/Omega.tex create mode 100644 doc/refman/Polynom.tex create mode 100755 doc/refman/RefMan-add.tex create mode 100755 doc/refman/RefMan-cas.tex create mode 100755 doc/refman/RefMan-cic.tex create mode 100755 doc/refman/RefMan-coi.tex create mode 100755 doc/refman/RefMan-com.tex create mode 100644 doc/refman/RefMan-ext.tex create mode 100644 doc/refman/RefMan-gal.tex create mode 100644 doc/refman/RefMan-ide.tex create mode 100755 doc/refman/RefMan-ind.tex create mode 100755 doc/refman/RefMan-int.tex create mode 100755 doc/refman/RefMan-lib.tex create mode 100644 doc/refman/RefMan-ltac.tex create mode 100644 doc/refman/RefMan-mod.tex create mode 100644 doc/refman/RefMan-modr.tex create mode 100644 doc/refman/RefMan-oth.tex create mode 100755 doc/refman/RefMan-pre.tex create mode 100755 doc/refman/RefMan-pro.tex create mode 100755 doc/refman/RefMan-syn.tex create mode 100644 doc/refman/RefMan-tac.tex create mode 100644 doc/refman/RefMan-tacex.tex create mode 100755 doc/refman/RefMan-tus.tex create mode 100755 doc/refman/RefMan-uti.tex create mode 100644 doc/refman/Reference-Manual.tex create mode 100644 doc/refman/Setoid.tex create mode 100755 doc/refman/biblio.bib create mode 100644 doc/refman/coqdoc.tex create mode 100644 doc/refman/coqide-queries.png create mode 100644 doc/refman/coqide.png create mode 100644 doc/refman/cover.html create mode 100644 doc/refman/headers.tex create mode 100644 doc/refman/hevea.sty create mode 100644 doc/refman/index.html create mode 100644 doc/rt/RefMan-cover.tex create mode 100644 doc/rt/Tutorial-cover.tex create mode 100755 doc/stdlib/Library.tex delete mode 100644 doc/syntax.txt delete mode 100755 doc/title.tex create mode 100644 doc/tools/Translator.tex delete mode 100755 doc/tov8 delete mode 100644 doc/tradv8.ml4 create mode 100755 doc/tutorial/Tutorial.tex delete mode 100644 doc/v8.txt diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex deleted file mode 100644 index 5312b8fc2f..0000000000 --- a/doc/AddRefMan-pre.tex +++ /dev/null @@ -1,58 +0,0 @@ -%\coverpage{Addendum to the Reference Manual}{\ } -%\addcontentsline{toc}{part}{Additional documentation} -\setheaders{Presentation of the Addendum} -\chapter*{Presentation of the Addendum} - -Here you will find several pieces of additional documentation for the -\Coq\ Reference Manual. Each of this chapters is concentrated on a -particular topic, that should interest only a fraction of the \Coq\ -users: that's the reason why they are apart from the Reference -Manual. - -\begin{description} - -\item[Extended pattern-matching] This chapter details the use of - generalized pattern-matching. It is contributed by Cristina Cornes - and Hugo Herbelin. - -\item[Implicit coercions] This chapter details the use of the coercion - mechanism. It is contributed by Amokrane Saïbi. - -%\item[Proof of imperative programs] This chapter explains how to -% prove properties of annotated programs with imperative features. -% It is contributed by Jean-Christophe Filliâtre - -\item[Program extraction] This chapter explains how to extract in practice ML - files from $\FW$ terms. It is contributed by Jean-Christophe - Filliâtre and Pierre Letouzey. - -%\item[Natural] This chapter is due to Yann Coscoy. It is the user -% manual of the tools he wrote for printing proofs in natural -% language. At this time, French and English languages are supported. - -\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole - class of arithmetic problems. - -%\item[Program] The \texttt{Program} technology intends to inverse the -% extraction mechanism. It allows the developments of certified -% programs in \Coq. This chapter is due to Catherine Parent. {\bf This -% feature is not available in {\Coq} version 7.} - -\item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This - chapter explains how to use it and how it works. - The chapter is contributed by Patrick Loiseleur. - -\item[The {\tt Setoid\_replace} tactic] This is a - tactic to do rewriting on types equipped with specific (only partially - substitutive) equality. The chapter is contributed by Clément Renard. - - -\end{description} - -\atableofcontents - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/Anomalies.tex b/doc/Anomalies.tex deleted file mode 100755 index a21577db0e..0000000000 --- a/doc/Anomalies.tex +++ /dev/null @@ -1,34 +0,0 @@ -\documentclass[11pt]{article} - -\input{./title} - -\title{Known bugs of \Coq{} V6.2} -\author{\ } -\begin{document} -\maketitle - -\begin{itemize} - -\item {\tt Program} may fail to build pattern in {\tt Cases} -expressions. Instead an old style {\tt Case} expression without -patterns is generated. - -\item The option {\tt Set Printing Synth} sometimes fails to decide if -a elimination predicates is synthetisable. If a term printed without -the elimination predicate is not correctly re-interpreted by Coq, then -turn off the {\tt Printing Synth} mode. - -\item {\tt Unfold} and {\tt Pattern} may incorrectly number the -occurrences of constants or subterms when {\tt Cases} expression are involved. - -\item \texttt{Transparent} and \texttt{Opaque} are not synchronous - with the \texttt{Reset} mecanism. If a constant was transparent at - point \texttt{A}, if you set it opaque and do \texttt{Reset A}, it - is still opaque and that may cause problems if you try to replay - tactic scripts between \texttt{A} and the current point. - -\end{itemize} - -\end{document} - -% $Id$ diff --git a/doc/Cases.tex b/doc/Cases.tex deleted file mode 100644 index 95411afae9..0000000000 --- a/doc/Cases.tex +++ /dev/null @@ -1,698 +0,0 @@ -\achapter{Extended pattern-matching}\defaultheaders -\aauthor{Cristina Cornes} - -\label{Mult-match-full} -\ttindex{Cases} -\index{ML-like patterns} - -This section describes the full form of pattern-matching in {\Coq} terms. - -\asection{Patterns}\label{implementation} The full syntax of {\tt -match} is presented in figures~\ref{term-syntax} -and~\ref{term-syntax-aux}. Identifiers in patterns are either -constructor names or variables. Any identifier that is not the -constructor of an inductive or coinductive type is considered to be a -variable. A variable name cannot occur more than once in a given -pattern. It is recommended to start variable names by a lowercase -letter. - -If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor -symbol and $\vec{x}$ is a linear vector of variables, it is called -{\em simple}: it is the kind of pattern recognized by the basic -version of {\tt match}. If a pattern is -not simple we call it {\em nested}. - -A variable pattern matches any value, and the identifier is bound to -that value. The pattern ``\texttt{\_}'' (called ``don't care'' or -``wildcard'' symbol) also matches any value, but does not bind anything. It -may occur an arbitrary number of times in a pattern. Alias patterns -written \texttt{(}{\sl pattern} \texttt{as} {\sl identifier}\texttt{)} are -also accepted. This pattern matches the same values as {\sl pattern} -does and {\sl identifier} is bound to the matched value. A list of -patterns separated with commas -is also considered as a pattern and is called {\em multiple -pattern}. - -Since extended {\tt match} expressions are compiled into the primitive -ones, the expressiveness of the theory remains the same. Once the -stage of parsing has finished only simple patterns remain. An easy way -to see the result of the expansion is by printing the term with -\texttt{Print} if the term is a constant, or using the command -\texttt{Check}. - -The extended \texttt{match} still accepts an optional {\em elimination -predicate} given after the keyword \texttt{return}. Given a pattern -matching expression, if all the right hand sides of \texttt{=>} ({\em -rhs} in short) have the same type, then this type can be sometimes -synthesized, and so we can omit the \texttt{return} part. Otherwise -the predicate after \texttt{return} has to be provided, like for the basic -\texttt{match}. - -Let us illustrate through examples the different aspects of extended -pattern matching. Consider for example the function that computes the -maximum of two natural numbers. We can write it in primitive syntax -by: - -\begin{coq_example} -Fixpoint max (n m:nat) {struct m} : nat := - match n with - | O => m - | S n' => match m with - | O => S n' - | S m' => S (max n' m') - end - end. -\end{coq_example} - -Using multiple patterns in the definition allows to write: - -\begin{coq_example} -Reset max. -Fixpoint max (n m:nat) {struct m} : nat := - match n, m with - | O, _ => m - | S n', O => S n' - | S n', S m' => S (max n' m') - end. -\end{coq_example} - -which will be compiled into the previous form. - -The pattern-matching compilation strategy examines patterns from left -to right. A \texttt{match} expression is generated {\bf only} when -there is at least one constructor in the column of patterns. E.g. the -following example does not build a \texttt{match} expression. - -\begin{coq_example} -Check (fun x:nat => match x return nat with - | y => y - end). -\end{coq_example} - -We can also use ``\texttt{as} patterns'' to associate a name to a -sub-pattern: - -\begin{coq_example} -Reset max. -Fixpoint max (n m:nat) {struct n} : nat := - match n, m with - | O, _ => m - | S n' as p, O => p - | S n', S m' => S (max n' m') - end. -\end{coq_example} - -Here is now an example of nested patterns: - -\begin{coq_example} -Fixpoint even (n:nat) : bool := - match n with - | O => true - | S O => false - | S (S n') => even n' - end. -\end{coq_example} - -This is compiled into: - -\begin{coq_example} -Print even. -\end{coq_example} - -In the previous examples patterns do not conflict with, but -sometimes it is comfortable to write patterns that admit a non -trivial superposition. Consider -the boolean function \texttt{lef} that given two natural numbers -yields \texttt{true} if the first one is less or equal than the second -one and \texttt{false} otherwise. We can write it as follows: - -\begin{coq_example} -Fixpoint lef (n m:nat) {struct m} : bool := - match n, m with - | O, x => true - | x, O => false - | S n, S m => lef n m - end. -\end{coq_example} - -Note that the first and the second multiple pattern superpose because -the couple of values \texttt{O O} matches both. Thus, what is the result -of the function on those values? To eliminate ambiguity we use the -{\em textual priority rule}: we consider patterns ordered from top to -bottom, then a value is matched by the pattern at the $ith$ row if and -only if it is not matched by some pattern of a previous row. Thus in the -example, -\texttt{O O} is matched by the first pattern, and so \texttt{(lef O O)} -yields \texttt{true}. - -Another way to write this function is: - -\begin{coq_example} -Reset lef. -Fixpoint lef (n m:nat) {struct m} : bool := - match n, m with - | O, x => true - | S n, S m => lef n m - | _, _ => false - end. -\end{coq_example} - - -Here the last pattern superposes with the first two. Because -of the priority rule, the last pattern -will be used only for values that do not match neither the first nor -the second one. - -Terms with useless patterns are not accepted by the -system. Here is an example: -% Test failure -\begin{coq_eval} -Set Printing Depth 50. - (********** The following is not correct and should produce **********) - (**************** Error: This clause is redundant ********************) -\end{coq_eval} -\begin{coq_example} -Check (fun x:nat => - match x with - | O => true - | S _ => false - | x => true - end). -\end{coq_example} - -\asection{About patterns of parametric types} -When matching objects of a parametric type, constructors in patterns -{\em do not expect} the parameter arguments. Their value is deduced -during expansion. - -Consider for example the polymorphic lists: - -\begin{coq_example} -Inductive List (A:Set) : Set := - | nil : List A - | cons : A -> List A -> List A. -\end{coq_example} - -We can check the function {\em tail}: - -\begin{coq_example} -Check - (fun l:List nat => - match l with - | nil => nil nat - | cons _ l' => l' - end). -\end{coq_example} - - -When we use parameters in patterns there is an error message: -% Test failure -\begin{coq_eval} -Set Printing Depth 50. -(********** The following is not correct and should produce **********) -(******** Error: The constructor cons expects 2 arguments ************) -\end{coq_eval} -\begin{coq_example} -Check - (fun l:List nat => - match l with - | nil A => nil nat - | cons A _ l' => l' - end). -\end{coq_example} - - - -\asection{Matching objects of dependent types} -The previous examples illustrate pattern matching on objects of -non-dependent types, but we can also -use the expansion strategy to destructure objects of dependent type. -Consider the type \texttt{listn} of lists of a certain length: - -\begin{coq_example} -Inductive listn : nat -> Set := - | niln : listn 0 - | consn : forall n:nat, nat -> listn n -> listn (S n). -\end{coq_example} - -\asubsection{Understanding dependencies in patterns} -We can define the function \texttt{length} over \texttt{listn} by: - -\begin{coq_example} -Definition length (n:nat) (l:listn n) := n. -\end{coq_example} - -Just for illustrating pattern matching, -we can define it by case analysis: - -\begin{coq_example} -Reset length. -Definition length (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn n _ _ => S n - end. -\end{coq_example} - -We can understand the meaning of this definition using the -same notions of usual pattern matching. - -% -% Constraining of dependencies is not longer valid in V7 -% -\iffalse -Now suppose we split the second pattern of \texttt{length} into two -cases so to give an -alternative definition using nested patterns: -\begin{coq_example} -Definition length1 (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn n _ niln => S n - | consn n _ (consn _ _ _) => S n - end. -\end{coq_example} - -It is obvious that \texttt{length1} is another version of -\texttt{length}. We can also give the following definition: -\begin{coq_example} -Definition length2 (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn n _ niln => 1 - | consn n _ (consn m _ _) => S (S m) - end. -\end{coq_example} - -If we forget that \texttt{listn} is a dependent type and we read these -definitions using the usual semantics of pattern matching, we can conclude -that \texttt{length1} -and \texttt{length2} are different functions. -In fact, they are equivalent -because the pattern \texttt{niln} implies that \texttt{n} can only match -the value $0$ and analogously the pattern \texttt{consn} determines that \texttt{n} can -only match values of the form $(S~v)$ where $v$ is the value matched by -\texttt{m}. - -The converse is also true. If -we destructure the length value with the pattern \texttt{O} then the list -value should be $niln$. -Thus, the following term \texttt{length3} corresponds to the function -\texttt{length} but this time defined by case analysis on the dependencies instead of on the list: - -\begin{coq_example} -Definition length3 (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn O _ _ => 1 - | consn (S n) _ _ => S (S n) - end. -\end{coq_example} - -When we have nested patterns of dependent types, the semantics of -pattern matching becomes a little more difficult because -the set of values that are matched by a sub-pattern may be conditioned by the -values matched by another sub-pattern. Dependent nested patterns are -somehow constrained patterns. -In the examples, the expansion of -\texttt{length1} and \texttt{length2} yields exactly the same term - but the -expansion of \texttt{length3} is completely different. \texttt{length1} and -\texttt{length2} are expanded into two nested case analysis on -\texttt{listn} while \texttt{length3} is expanded into a case analysis on -\texttt{listn} containing a case analysis on natural numbers inside. - - -In practice the user can think about the patterns as independent and -it is the expansion algorithm that cares to relate them. \\ -\fi -% -% -% - -\asubsection{When the elimination predicate must be provided} -The examples given so far do not need an explicit elimination predicate - because all the rhs have the same type and the -strategy succeeds to synthesize it. -Unfortunately when dealing with dependent patterns it often happens -that we need to write cases where the type of the rhs are -different instances of the elimination predicate. -The function \texttt{concat} for \texttt{listn} -is an example where the branches have different type -and we need to provide the elimination predicate: - -\begin{coq_example} -Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n return listn (n + m) with - | niln => l' - | consn n' a y => consn (n' + m) a (concat n' y m l') - end. -\end{coq_example} -The elimination predicate is {\tt fun (n:nat) (l:listn n) => listn~(n+m)}. -In general if $m$ has type $(I~q_1\ldots q_r~t_1\ldots t_s)$ where -$q_1\ldots q_r$ are parameters, the elimination predicate should be of -the form~: -{\tt fun $y_1$\ldots $y_s$ $x$:($I$~$q_1$\ldots $q_r$~$y_1$\ldots - $y_s$) => P}. - -In the concrete syntax, it should be written~: -\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_\ldots \_~y_1\ldots y_s)~\kw{return}~Q~\kw{with}~\ldots~\kw{end}\] - -The variables which appear in the \kw{in} and \kw{as} clause are new -and bounded in the property $Q$ in the \kw{return} clause. The -parameters of the inductive definitions should not be mentioned and -are replaced by \kw{\_}. - -Recall that a list of patterns is also a pattern. So, when -we destructure several terms at the same time and the branches have -different type we need to provide -the elimination predicate for this multiple pattern. -It is done using the same scheme, each term may be associated to an -\kw{as} and \kw{in} clause in order to introduce a dependent product. - -For example, an equivalent definition for \texttt{concat} (even though the matching on the second term is trivial) would have -been: - -\begin{coq_example} -Reset concat. -Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n, l' return listn (n + m) with - | niln, x => x - | consn n' a y, x => consn (n' + m) a (concat n' y m x) - end. -\end{coq_example} - -% Notice that this time, the predicate \texttt{[n,\_:nat](listn (plus n -% m))} is binary because we -% destructure both \texttt{l} and \texttt{l'} whose types have arity one. -% In general, if we destructure the terms $e_1\ldots e_n$ -% the predicate will be of arity $m$ where $m$ is the sum of the -% number of dependencies of the type of $e_1, e_2,\ldots e_n$ -% (the $\lambda$-abstractions -% should correspond from left to right to each dependent argument of the -% type of $e_1\ldots e_n$). -When the arity of the predicate (i.e. number of abstractions) is not -correct Coq raises an error message. For example: - -% Test failure -\begin{coq_eval} -Reset concat. -Set Printing Depth 50. -(********** The following is not correct and should produce ***********) -(** Error: the term l' has type listn m while it is expected to have **) -(** type listn (?31 + ?32) **) -\end{coq_eval} -\begin{coq_example} -Fixpoint concat - (n:nat) (l:listn n) (m:nat) - (l':listn m) {struct l} : listn (n + m) := - match l, l' with - | niln, x => x - | consn n' a y, x => consn (n' + m) a (concat n' y m x) - end. -\end{coq_example} - -\asection{Using pattern matching to write proofs} -In all the previous examples the elimination predicate does not depend -on the object(s) matched. But it may depend and the typical case -is when we write a proof by induction or a function that yields an -object of dependent type. An example of proof using \texttt{match} in -given in section \ref{refine-example} - -For example, we can write -the function \texttt{buildlist} that given a natural number -$n$ builds a list of length $n$ containing zeros as follows: - -\begin{coq_example} -Fixpoint buildlist (n:nat) : listn n := - match n return listn n with - | O => niln - | S n => consn n 0 (buildlist n) - end. -\end{coq_example} - -We can also use multiple patterns. -Consider the following definition of the predicate less-equal -\texttt{Le}: - -\begin{coq_example} -Inductive LE : nat -> nat -> Prop := - | LEO : forall n:nat, LE 0 n - | LES : forall n m:nat, LE n m -> LE (S n) (S m). -\end{coq_example} - -We can use multiple patterns to write the proof of the lemma - \texttt{(n,m:nat) (LE n m)}\verb=\/=\texttt{(LE m n)}: - -\begin{coq_example} -Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n := - match n, m return LE n m \/ LE m n with - | O, x => or_introl (LE x 0) (LEO x) - | x, O => or_intror (LE x 0) (LEO x) - | S n as n', S m as m' => - match dec n m with - | or_introl h => or_introl (LE m' n') (LES n m h) - | or_intror h => or_intror (LE n' m') (LES m n h) - end - end. -\end{coq_example} -In the example of \texttt{dec}, -the first \texttt{match} is dependent while -the second is not. - -% In general, consider the terms $e_1\ldots e_n$, -% where the type of $e_i$ is an instance of a family type -% $\lb (\vec{d_i}:\vec{D_i}) \mto T_i$ ($1\leq i -% \leq n$). Then, in expression \texttt{match} $e_1,\ldots, -% e_n$ \texttt{of} \ldots \texttt{end}, the -% elimination predicate ${\cal P}$ should be of the form: -% $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$ - -The user can also use \texttt{match} in combination with the tactic -\texttt{refine} (see section \ref{refine}) to build incomplete proofs -beginning with a \texttt{match} construction. - -\asection{Pattern-matching on inductive objects involving local -definitions} - -If local definitions occur in the type of a constructor, then there -are two ways to match on this constructor. Either the local -definitions are skipped and matching is done only on the true arguments -of the constructors, or the bindings for local definitions can also -be caught in the matching. - -Example. - -\begin{coq_eval} -Reset Initial. -Require Import Arith. -\end{coq_eval} - -\begin{coq_example*} -Inductive list : nat -> Set := - | nil : list 0 - | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)). -\end{coq_example*} - -In the next example, the local definition is not caught. - -\begin{coq_example} -Fixpoint length n (l:list n) {struct l} : nat := - match l with - | nil => 0 - | cons n l0 => S (length (2 * n) l0) - end. -\end{coq_example} - -But in this example, it is. - -\begin{coq_example} -Fixpoint length' n (l:list n) {struct l} : nat := - match l with - | nil => 0 - | cons _ m l0 => S (length' m l0) - end. -\end{coq_example} - -\Rem for a given matching clause, either none of the local -definitions or all of them can be caught. - -\asection{Pattern-matching and coercions} - -If a mismatch occurs between the expected type of a pattern and its -actual type, a coercion made from constructors is sought. If such a -coercion can be found, it is automatically inserted around the -pattern. - -Example: - -\begin{coq_example} -Inductive I : Set := - | C1 : nat -> I - | C2 : I -> I. -Coercion C1 : nat >-> I. -Check (fun x => match x with - | C2 O => 0 - | _ => 0 - end). -\end{coq_example} - - -\asection{When does the expansion strategy fail ?}\label{limitations} -The strategy works very like in ML languages when treating -patterns of non-dependent type. -But there are new cases of failure that are due to the presence of -dependencies. - -The error messages of the current implementation may be sometimes -confusing. When the tactic fails because patterns are somehow -incorrect then error messages refer to the initial expression. But the -strategy may succeed to build an expression whose sub-expressions are -well typed when the whole expression is not. In this situation the -message makes reference to the expanded expression. We encourage -users, when they have patterns with the same outer constructor in -different equations, to name the variable patterns in the same -positions with the same name. -E.g. to write {\small\texttt{(cons n O x) => e1}} -and {\small\texttt{(cons n \_ x) => e2}} instead of -{\small\texttt{(cons n O x) => e1}} and -{\small\texttt{(cons n' \_ x') => e2}}. -This helps to maintain certain name correspondence between the -generated expression and the original. - -Here is a summary of the error messages corresponding to each situation: - -\begin{ErrMsgs} -\item \sverb{The constructor } {\sl - ident} \sverb{expects } {\sl num} \sverb{arguments} - - \sverb{The variable } {\sl ident} \sverb{is bound several times - in pattern } {\sl term} - - \sverb{Found a constructor of inductive type} {\term} - \sverb{while a constructor of} {\term} \sverb{is expected} - - Patterns are incorrect (because constructors are not applied to - the correct number of the arguments, because they are not linear or - they are wrongly typed) - -\item \errindex{Non exhaustive pattern-matching} - -the pattern matching is not exhaustive - -\item \sverb{The elimination predicate } {\sl term} \sverb{should be - of arity } {\sl num} \sverb{(for non dependent case) or } {\sl - num} \sverb{(for dependent case)} - -The elimination predicate provided to \texttt{match} has not the - expected arity - - -%\item the whole expression is wrongly typed - -% CADUC ? -% , or the synthesis of -% implicit arguments fails (for example to find the elimination -% predicate or to resolve implicit arguments in the rhs). - -% There are {\em nested patterns of dependent type}, the elimination -% predicate corresponds to non-dependent case and has the form -% $[x_1:T_1]...[x_n:T_n]T$ and {\bf some} $x_i$ occurs {\bf free} in -% $T$. Then, the strategy may fail to find out a correct elimination -% predicate during some step of compilation. In this situation we -% recommend the user to rewrite the nested dependent patterns into -% several \texttt{match} with {\em simple patterns}. - -\item {\tt Unable to infer a match predicate\\ - Either there is a type incompatiblity or the problem involves\\ - dependencies} - - There is a type mismatch between the different branches - - Then the user should provide an elimination predicate. - -% Obsolete ? -% \item because of nested patterns, it may happen that even though all -% the rhs have the same type, the strategy needs dependent elimination -% and so an elimination predicate must be provided. The system warns -% about this situation, trying to compile anyway with the -% non-dependent strategy. The risen message is: - -% \begin{itemize} -% \item {\tt Warning: This pattern matching may need dependent -% elimination to be compiled. I will try, but if fails try again -% giving dependent elimination predicate.} -% \end{itemize} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% % LA PROPAGATION DES CONTRAINTES ARRIERE N'EST PAS FAITE DANS LA V7 -% TODO -% \item there are {\em nested patterns of dependent type} and the -% strategy builds a term that is well typed but recursive calls in fix -% point are reported as illegal: -% \begin{itemize} -% \item {\tt Error: Recursive call applied to an illegal term ...} -% \end{itemize} - -% This is because the strategy generates a term that is correct w.r.t. -% the initial term but which does not pass the guard condition. In -% this situation we recommend the user to transform the nested dependent -% patterns into {\em several \texttt{match} of simple patterns}. Let us -% explain this with an example. Consider the following definition of a -% function that yields the last element of a list and \texttt{O} if it is -% empty: - -% \begin{coq_example} -% Fixpoint last [n:nat; l:(listn n)] : nat := -% match l of -% (consn _ a niln) => a -% | (consn m _ x) => (last m x) | niln => O -% end. -% \end{coq_example} - -% It fails because of the priority between patterns, we know that this -% definition is equivalent to the following more explicit one (which -% fails too): - -% \begin{coq_example*} -% Fixpoint last [n:nat; l:(listn n)] : nat := -% match l of -% (consn _ a niln) => a -% | (consn n _ (consn m b x)) => (last n (consn m b x)) -% | niln => O -% end. -% \end{coq_example*} - -% Note that the recursive call {\tt (last n (consn m b x))} is not -% guarded. When treating with patterns of dependent types the strategy -% interprets the first definition of \texttt{last} as the second -% one\footnote{In languages of the ML family the first definition would -% be translated into a term where the variable \texttt{x} is shared in -% the expression. When patterns are of non-dependent types, Coq -% compiles as in ML languages using sharing. When patterns are of -% dependent types the compilation reconstructs the term as in the -% second definition of \texttt{last} so to ensure the result of -% expansion is well typed.}. Thus it generates a term where the -% recursive call is rejected by the guard condition. - -% You can get rid of this problem by writing the definition with -% \emph{simple patterns}: - -% \begin{coq_example} -% Fixpoint last [n:nat; l:(listn n)] : nat := -% <[_:nat]nat>match l of -% (consn m a x) => Cases x of niln => a | _ => (last m x) end -% | niln => O -% end. -% \end{coq_example} - -\end{ErrMsgs} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/Changes.html b/doc/Changes.html deleted file mode 100644 index 87082c6b8e..0000000000 --- a/doc/Changes.html +++ /dev/null @@ -1,126 +0,0 @@ - -
-
-The Coq Proof Assistant
- Reference Manual