diff options
Diffstat (limited to 'doc/faq')
| -rw-r--r-- | doc/faq/FAQ.tex | 2481 | ||||
| -rw-r--r-- | doc/faq/axioms.eps | 378 | ||||
| -rw-r--r-- | doc/faq/axioms.fig | 84 | ||||
| -rw-r--r-- | doc/faq/axioms.png | bin | 0 -> 10075 bytes | |||
| -rw-r--r-- | doc/faq/fk.bib | 2221 | ||||
| -rw-r--r-- | doc/faq/hevea.sty | 78 | ||||
| -rw-r--r-- | doc/faq/interval_discr.v | 419 |
7 files changed, 5661 insertions, 0 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex new file mode 100644 index 00000000..2b5d898f --- /dev/null +++ b/doc/faq/FAQ.tex @@ -0,0 +1,2481 @@ +\RequirePackage{ifpdf} +\ifpdf % si on est en pdflatex +\documentclass[a4paper,pdftex]{article} +\else +\documentclass[a4paper]{article} +\fi +\pagestyle{plain} + +% yay les symboles +\usepackage{stmaryrd} +\usepackage{amssymb} +\usepackage{url} +%\usepackage{multicol} +\usepackage{hevea} +\usepackage{fullpage} +\usepackage[latin1]{inputenc} +\usepackage[english]{babel} + +\ifpdf % si on est en pdflatex + \usepackage[pdftex]{graphicx} +\else + \usepackage[dvips]{graphicx} +\fi + +%\input{../macros.tex} + +% Making hevea happy +%HEVEA \renewcommand{\textbar}{|} +%HEVEA \renewcommand{\textunderscore}{\_} + +\def\Question#1{\stepcounter{question}\subsubsection{#1}} + +% version et date +\def\faqversion{0.1} + +% les macros d'amour +\def\Coq{\textsc{Coq}} +\def\Why{\textsc{Why}} +\def\Caduceus{\textsc{Caduceus}} +\def\Krakatoa{\textsc{Krakatoa}} +\def\Ltac{\textsc{Ltac}} +\def\CoqIde{\textsc{CoqIde}} + +\newcommand{\coqtt}[1]{{\tt #1}} +\newcommand{\coqimp}{{\mbox{\tt ->}}} +\newcommand{\coqequiv}{{\mbox{\tt <->}}} + + +% macro pour les tactics +\def\split{{\tt split}} +\def\assumption{{\tt assumption}} +\def\auto{{\tt auto}} +\def\trivial{{\tt trivial}} +\def\tauto{{\tt tauto}} +\def\left{{\tt left}} +\def\right{{\tt right}} +\def\decompose{{\tt decompose}} +\def\intro{{\tt intro}} +\def\intros{{\tt intros}} +\def\field{{\tt field}} +\def\ring{{\tt ring}} +\def\apply{{\tt apply}} +\def\exact{{\tt exact}} +\def\cut{{\tt cut}} +\def\assert{{\tt assert}} +\def\solve{{\tt solve}} +\def\idtac{{\tt idtac}} +\def\fail{{\tt fail}} +\def\existstac{{\tt exists}} +\def\firstorder{{\tt firstorder}} +\def\congruence{{\tt congruence}} +\def\gb{{\tt gb}} +\def\generalize{{\tt generalize}} +\def\abstracttac{{\tt abstract}} +\def\eapply{{\tt eapply}} +\def\unfold{{\tt unfold}} +\def\rewrite{{\tt rewrite}} +\def\replace{{\tt replace}} +\def\simpl{{\tt simpl}} +\def\elim{{\tt elim}} +\def\set{{\tt set}} +\def\pose{{\tt pose}} +\def\case{{\tt case}} +\def\destruct{{\tt destruct}} +\def\reflexivity{{\tt reflexivity}} +\def\transitivity{{\tt transitivity}} +\def\symmetry{{\tt symmetry}} +\def\Focus{{\tt Focus}} +\def\discriminate{{\tt discriminate}} +\def\contradiction{{\tt contradiction}} +\def\intuition{{\tt intuition}} +\def\try{{\tt try}} +\def\repeat{{\tt repeat}} +\def\eauto{{\tt eauto}} +\def\subst{{\tt subst}} +\def\symmetryin{{\tt symmetryin}} +\def\instantiate{{\tt instantiate}} +\def\inversion{{\tt inversion}} +\def\Defined{{\tt Defined}} +\def\Qed{{\tt Qed}} +\def\pattern{{\tt pattern}} +\def\Type{{\tt Type}} +\def\Prop{{\tt Prop}} +\def\Set{{\tt Set}} + + +\newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}} +\urldef{\InitWf}{\url} + {http://coq.inria.fr/library/Coq.Init.Wf.html} +\urldef{\LogicBerardi}{\url} + {http://coq.inria.fr/library/Coq.Logic.Berardi.html} +\urldef{\LogicClassical}{\url} + {http://coq.inria.fr/library/Coq.Logic.Classical.html} +\urldef{\LogicClassicalFacts}{\url} + {http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html} +\urldef{\LogicClassicalDescription}{\url} + {http://coq.inria.fr/library/Coq.Logic.ClassicalDescription.html} +\urldef{\LogicProofIrrelevance}{\url} + {http://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html} +\urldef{\LogicEqdep}{\url} + {http://coq.inria.fr/library/Coq.Logic.Eqdep.html} +\urldef{\LogicEqdepDec}{\url} + {http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html} + + + + +\begin{document} +\bibliographystyle{plain} +\newcounter{question} +\renewcommand{\thesubsubsection}{\arabic{question}} + +%%%%%%% Coq pour les nuls %%%%%%% + +\title{Coq Version 8.0 for the Clueless\\ + \large(\protect\ref{lastquestion} + \ Hints) +} +\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux} +\maketitle + +%%%%%%% + +\begin{abstract} +This note intends to provide an easy way to get acquainted with the +{\Coq} theorem prover. It tries to formulate appropriate answers +to some of the questions any newcomers will face, and to give +pointers to other references when possible. +\end{abstract} + +%%%%%%% + +%\begin{multicols}{2} +\tableofcontents +%\end{multicols} + +%%%%%%% + +\newpage + +\section{Introduction} +This FAQ is the sum of the questions that came to mind as we developed +proofs in \Coq. Since we are singularly short-minded, we wrote the +answers we found on bits of papers to have them at hand whenever the +situation occurs again. This is pretty much the result of that: a +collection of tips one can refer to when proofs become intricate. Yes, +this means we won't take the blame for the shortcomings of this +FAQ. But if you want to contribute and send in your own question and +answers, feel free to write to us\ldots + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section{Presentation} + +\Question{What is {\Coq}?}\label{whatiscoq} +The {\Coq} tool is a formal proof management system: a proof done with {\Coq} is mechanically checked by the machine. +In particular, {\Coq} allows: +\begin{itemize} + \item the definition of mathematical objects and programming objects, + \item to state mathematical theorems and software specifications, + \item to interactively develop formal proofs of these theorems, + \item to check these proofs by a small certification ``kernel''. +\end{itemize} +{\Coq} is based on a logical framework called ``Calculus of Inductive +Constructions'' extended by a modular development system for theories. + +\Question{Did you really need to name it like that?} +Some French computer scientists have a tradition of naming their +software as animal species: Caml, Elan, Foc or Phox are examples +of this tacit convention. In French, ``coq'' means rooster, and it +sounds like the initials of the Calculus of Constructions CoC on which +it is based. + +\Question{Is {\Coq} a theorem prover?} + +{\Coq} comes with decision and semi-decision procedures ( +propositional calculus, Presburger's arithmetic, ring and field +simplification, resolution, ...) but the main style for proving +theorems is interactively by using LCF-style tactics. + + +\Question{What are the other theorem provers?} +Many other theorem provers are available for use nowadays. +Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar +to {\Coq} by the way they interact with the user. Other relatives of +{\Coq} are ACL2, Agda/Alfa, Twelf, Kiv, Mizar, NqThm, +\begin{htmlonly}% +Omega\ldots +\end{htmlonly} +\begin{latexonly}% +{$\Omega$}mega\ldots +\end{latexonly} + +\Question{What do I have to trust when I see a proof checked by Coq?} + +You have to trust: + +\begin{description} +\item[The theory behind Coq] The theory of {\Coq} version 8.0 is +generally admitted to be consistent wrt Zermelo-Fraenkel set theory + +inaccessible cardinals. Proofs of consistency of subsystems of the +theory of Coq can be found in the literature. +\item[The Coq kernel implementation] You have to trust that the +implementation of the {\Coq} kernel mirrors the theory behind {\Coq}. The +kernel is intentionally small to limit the risk of conceptual or +accidental implementation bugs. +\item[The Objective Caml compiler] The {\Coq} kernel is written using the +Objective Caml language but it uses only the most standard features +(no object, no label ...), so that it is highly unprobable that an +Objective Caml bug breaks the consistency of {\Coq} without breaking all +other kinds of features of {\Coq} or of other software compiled with +Objective Caml. +\item[Your hardware] In theory, if your hardware does not work +properly, it can accidentally be the case that False becomes +provable. But it is more likely the case that the whole {\Coq} system +will be unusable. You can check your proof using different computers +if you feel the need to. +\item[Your axioms] Your axioms must be consistent with the theory +behind {\Coq}. +\end{description} + + +\Question{Where can I find information about the theory behind {\Coq}?} +\begin{description} +\item[The Calculus of Inductive Constructions] The +\ahref{http://coq.inria.fr/doc/Reference-Manual006.html}{corresponding} +chapter and the chapter on +\ahref{http://coq.inria.fr/doc/Reference-Manual007.html}{modules} in +the {\Coq} Reference Manual. +\item[Type theory] A book~\cite{ProofsTypes} or some lecture +notes~\cite{Types:Dowek}. +\item[Inductive types] +Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}. +\item[Co-Inductive types] +Eduardo Giménez' thesis~\cite{EGThese}. +\item[Miscellaneous] A +\ahref{http://coq.inria.fr/doc/biblio.html}{bibliography} about Coq +\end{description} + + +\Question{How can I use {\Coq} to prove programs?} + +You can either extract a program from a proof by using the extraction +mechanism or use dedicated tools, such as +\ahref{http://why.lri.fr}{\Why}, +\ahref{http://krakatoa.lri.fr}{\Krakatoa}, +\ahref{http://why.lri.fr/caduceus/index.en.html}{\Caduceus}, to prove +annotated programs written in other languages. + +%\Question{How many {\Coq} users are there?} +% +%An estimation is about 100 regular users. + +\Question{How old is {\Coq}?} + +The first implementation is from 1985 (it was named {\sf CoC} which is +the acronym of the name of the logic it implemented: the Calculus of +Constructions). The first official release of {\Coq} (version 4.10) +was distributed in 1989. + +\Question{What are the \Coq-related tools?} + +There are graphical user interfaces: +\begin{description} +\item[Coqide] A GTK based GUI for \Coq. +\item[Pcoq] A GUI for {\Coq} with proof by pointing and pretty printing. +\item[coqwc] A tool similar to {\tt wc} to count lines in {\Coq} files. +\item[Proof General] A emacs mode for {\Coq} and many other proof assistants. +\end{description} + +There are documentation and browsing tools: + +\begin{description} +\item[Helm/Mowgli] A rendering, searching and publishing tool. +\item[coq-tex] A tool to insert {\Coq} examples within .tex files. +\item[coqdoc] A documentation tool for \Coq. +\end{description} + +There are front-ends for specific languages: + +\begin{description} +\item[Why] A back-end generator of verification conditions. +\item[Krakatoa] A Java code certification tool that uses both {\Coq} and {\Why} to verify the soundness of implementations with regards to the specifications. +\item[Caduceus] A C code certification tool that uses both {\Coq} and \Why. +\item[Zenon] A first-order theorem prover. +\item[Focal] The \ahref{http://focal.inria.fr}{Focal} project aims at building an environment to develop certified computer algebra libraries. +\end{description} + +\Question{What are the high-level tactics of \Coq} + +\begin{itemize} +\item Decision of quantifier-free Presburger's Arithmetic +\item Simplification of expressions on rings and fields +\item Decision of closed systems of equations +\item Semi-decision of first-order logic +\item Prolog-style proof search, possibly involving equalities +\end{itemize} + +\Question{What are the main libraries available for \Coq} + +\begin{itemize} +\item Basic Peano's arithmetic, binary integer numbers, rational numbers, +\item Real analysis, +\item Libraries for lists, boolean, maps, floating-point numbers, +\item Libraries for relations, sets and constructive algebra, +\item Geometry +\end{itemize} + + +\Question{What are the mathematical applications for {\Coq}?} + +{\Coq} is used for formalizing mathematical theories, for teaching, +and for proving properties of algorithms or programs libraries. + +The largest mathematical formalization has been done at the University +of Nijmegen (see the +\ahref{http://vacuumcleaner.cs.kun.nl/c-corn}{Constructive Coq +Repository at Nijmegen}). + +A symbolic step has also been obtained by formalizing in full a proof +of the Four Color Theorem. + +\Question{What are the industrial applications for {\Coq}?} + +{\Coq} is used e.g. to prove properties of the JavaCard system +(especially by Schlumberger and Trusted Logic). It has +also been used to formalize the semantics of the Lucid-Synchrone +data-flow synchronous calculus used by Esterel-Technologies. + +\iffalse +todo christine compilo lustre? +\fi + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section{Documentation} + +\Question{Where can I find documentation about {\Coq}?} +All the documentation about \Coq, from the reference manual~\cite{Coq:manual} to +friendly tutorials~\cite{Coq:Tutorial} and documentation of the standard library, is available +\ahref{http://coq.inria.fr/doc-eng.html}{online}. +All these documents are viewable either in browsable HTML, or as +downloadable postscripts. + +\Question{Where can I find this FAQ on the web?} + +This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{http://coq.inria.fr/doc/faq.html}}. + +\Question{How can I submit suggestions / improvements / additions for this FAQ?} + +This FAQ is unfinished (in the sense that there are some obvious +sections that are missing). Please send contributions to \texttt{Florent.Kirchner at lix.polytechnique.fr} and \texttt{Julien.Narboux at inria.fr}. + +\Question{Is there any mailing list about {\Coq}?} +The main {\Coq} mailing list is \url{coq-club@pauillac.inria.fr}, which +broadcasts questions and suggestions about the implementation, the +logical formalism or proof developments. See +\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://pauillac.inria.fr/mailman/listinfo/coq-club}} for +subscription. For bugs reports see question \ref{coqbug}. + +\Question{Where can I find an archive of the list?} +The archives of the {\Coq} mailing list are available at +\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{http://coq.inria.fr/pipermail/coq-club}}. + + +\Question{How can I be kept informed of new releases of {\Coq}?} + +New versions of {\Coq} are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to {\Coq} on \ahref{http://freshmeat.net/projects/coq/}{\url{http://freshmeat.net/projects/coq/}}. + + +\Question{Is there any book about {\Coq}?} + +The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004: +\begin{quote} +``This book provides a pragmatic introduction to the development of +proofs and certified programs using \Coq. With its large collection of +examples and exercises it is an invaluable tool for researchers, +students, and engineers interested in formal methods and the +development of zero-default software.'' +\end{quote} + +\Question{Where can I find some {\Coq} examples?} + +There are examples in the manual~\cite{Coq:manual} and in the +Coq'Art~\cite{Coq:coqart} exercises \ahref{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}. +You can also find large developments using +{\Coq} in the {\Coq} user contributions: +\ahref{http://coq.inria.fr/contrib-eng.html}{\url{http://coq.inria.fr/contrib-eng.html}}. + +\Question{How can I report a bug?}\label{coqbug} + +You can use the web interface accessible at \ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link ``contacts''. + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section{Installation} + +\Question{What is the license of {\Coq}?} +{\Coq} is distributed under the GNU Lesser General License +(LGPL). + +\Question{Where can I find the sources of {\Coq}?} +The sources of {\Coq} can be found online in the tar.gz'ed packages +(\ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link +``download''). Development sources can be accessed at +\ahref{http://coq.gforge.inria.fr/}{\url{http://coq.gforge.inria.fr/}} + +\Question{On which platform is {\Coq} available?} +Compiled binaries are available for Linux, MacOS X, and Windows. The +sources can be easily compiled on all platforms supporting Objective +Caml. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section{The logic of {\Coq}} + +\subsection{General} + +\Question{What is the logic of \Coq?} + +{\Coq} is based on an axiom-free type theory called +the Calculus of Inductive Constructions (see Coquand \cite{CoHu86}, +Luo~\cite{Luo90} +and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order +functions and predicates, inductive and co-inductive datatypes and +predicates, and a stratified hierarchy of sets. + +\Question{Is \Coq's logic intuitionistic or classical?} + +{\Coq}'s logic is modular. The core logic is intuitionistic +(i.e. excluded-middle $A\vee\neg A$ is not granted by default). It can +be extended to classical logic on demand by requiring an +optional module stating $A\vee\neg A$. + +\Question{Can I define non-terminating programs in \Coq?} + +All programs in {\Coq} are terminating. Especially, loops +must come with an evidence of their termination. + +Non-terminating programs can be simulated by passing around a +bound on how long the program is allowed to run before dying. + +\Question{How is equational reasoning working in {\Coq}?} + + {\Coq} comes with an internal notion of computation called +{\em conversion} (e.g. $(x+1)+y$ is internally equivalent to +$(x+y)+1$; similarly applying argument $a$ to a function mapping $x$ +to some expression $t$ converts to the expression $t$ where $x$ is +replaced by $a$). This notion of conversion (which is decidable +because {\Coq} programs are terminating) covers a certain part of +equational reasoning but is limited to sequential evaluation of +expressions of (not necessarily closed) programs. Besides conversion, +equations have to be treated by hand or using specialised tactics. + +\subsection{Axioms} + +\Question{What axioms can be safely added to {\Coq}?} + +There are a few typical useful axioms that are independent from the +Calculus of Inductive Constructions and that can be safely added to +{\Coq}. These axioms are stated in the directory {\tt Logic} of the +standard library of {\Coq}. The most interesting ones are + +\begin{itemize} +\item Excluded-middle: $\forall A:Prop, A \vee \neg A$ +\item Proof-irrelevance: $\forall A:Prop \forall p_1 p_2:A, p_1=p_2$ +\item Unicity of equality proofs (or equivalently Streicher's axiom $K$): +$\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$ +\item The axiom of unique choice: $\forall x \exists! y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$ +\item The functional axiom of choice: $\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$ +\item Extensionality of predicates: $\forall P Q:A\rightarrow Prop, (\forall x, P(x) \leftrightarrow Q(x)) \rightarrow P=Q$ +\item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$ +\end{itemize} + +Here is a summary of the relative strength of these axioms, most +proofs can be found in directory {\tt Logic} of the standard library. +The justification of their validity relies on the interpretability in +set theory. + +%HEVEA\imgsrc{axioms.png} +%BEGIN LATEX +\ifpdf % si on est en pdflatex +\includegraphics[width=1.0\textwidth]{axioms.png} +\else +\includegraphics[width=1.0\textwidth]{axioms.eps} +\fi +%END LATEX + +\Question{What standard axioms are inconsistent with {\Coq}?} + +The axiom of unique choice together with classical logic +(e.g. excluded-middle) are inconsistent in the variant of the Calculus +of Inductive Constructions where {\Set} is impredicative. + +As a consequence, the functional form of the axiom of choice and +excluded-middle, or any form of the axiom of choice together with +predicate extensionality are inconsistent in the {\Set}-impredicative +version of the Calculus of Inductive Constructions. + +The main purpose of the \Set-predicative restriction of the Calculus +of Inductive Constructions is precisely to accommodate these axioms +which are quite standard in mathematical usage. + +The $\Set$-predicative system is commonly considered consistent by +interpreting it in a standard set-theoretic boolean model, even with +classical logic, axiom of choice and predicate extensionality added. + +\Question{What is Streicher's axiom $K$} +\label{Streicher} + +Streicher's axiom $K$~\cite{HofStr98} is an axiom that asserts +dependent elimination of reflexive equality proofs. + +\begin{coq_example*} +Axiom Streicher_K : + forall (A:Type) (x:A) (P: x=x -> Prop), + P (refl_equal x) -> forall p: x=x, P p. +\end{coq_example*} + +In the general case, axiom $K$ is an independent statement of the +Calculus of Inductive Constructions. However, it is true on decidable +domains (see file \vfile{\LogicEqdepDec}{Eqdep\_dec}). It is also +trivially a consequence of proof-irrelevance (see +\ref{proof-irrelevance}) hence of classical logic. + +Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} \cite{HofStr98} + +\begin{coq_example*} +Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2. +\end{coq_example*} + +Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98} + +\begin{coq_example*} +Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x. +\end{coq_example*} + +Axiom $K$ is also equivalent to + +\begin{coq_example*} +Axiom + eq_rec_eq : + forall (A:Set) (x:A) (P: A->Set) (p:P x) (h: x=x), + p = eq_rect x P p x h. +\end{coq_example*} + +It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs). + +\begin{coq_example*} +Inductive eq_dep (U:Set) (P:U -> Set) (p:U) (x:P p) : +forall q:U, P q -> Prop := + eq_dep_intro : eq_dep U P p x p x. +Axiom + eq_dep_eq : + forall (U:Set) (u:U) (P:U -> Set) (p1 p2:P u), + eq_dep U P u p1 u p2 -> p1 = p2. +\end{coq_example*} + +\Question{What is proof-irrelevance} +\label{proof-irrelevance} + +A specificity of the Calculus of Inductive Constructions is to permit +statements about proofs. This leads to the question of comparing two +proofs of the same proposition. Identifying all proofs of the same +proposition is called {\em proof-irrelevance}: +$$ +\forall A:\Prop, \forall p q:A, p=q +$$ + +Proof-irrelevance (in {\Prop}) can be assumed without contradiction in +{\Coq}. It expresses that only provability matters, whatever the exact +form of the proof is. This is in harmony with the common purely +logical interpretation of {\Prop}. Contrastingly, proof-irrelevance is +inconsistent in {\Set} since there are types in {\Set}, such as the +type of booleans, that are provably more than 2 elements. + +Proof-irrelevance (in {\Prop}) is a consequence of classical logic +(see proofs in file \vfile{\LogicClassical}{Classical} and +\vfile{\LogicBerardi}{Berardi}). Proof-irrelevance is also a +consequence of propositional extensionality (i.e. \coqtt{(A {\coqequiv} B) +{\coqimp} A=B}, see the proof in file +\vfile{\LogicClassicalFacts}{ClassicalFacts}). + +Proof-irrelevance directly implies Streicher's axiom $K$. + +\Question{What about functional extensionality?} + +Extensionality of functions is admittedly consistent with the +Set-predicative Calculus of Inductive Constructions. + +%\begin{coq_example*} +% Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g. +%\end{coq_example*} + +Let {\tt A}, {\tt B} be types. To deal with extensionality on +\verb=A->B= without relying on a general extensionality axiom, +a possible approach is to define one's own extensional equality on +\verb=A->B=. + +\begin{coq_eval} +Variables A B : Set. +\end{coq_eval} + +\begin{coq_example*} +Definition ext_eq (f g: A->B) := forall x:A, f x = g x. +\end{coq_example*} + +and to reason on \verb=A->B= as a setoid (see the Chapter on +Setoids in the Reference Manual). + +\Question{Is {\Prop} impredicative?} + +Yes, the sort {\Prop} of propositions is {\em +impredicative}. Otherwise said, a statement of the form $\forall +A:Prop, P(A)$ can be instantiated by itself: if $\forall A:\Prop, P(A)$ +is provable, then $P(\forall A:\Prop, P(A))$ is. + +\Question{Is {\Set} impredicative?} + +No, the sort {\Set} lying at the bottom of the hierarchy of +computational types is {\em predicative} in the basic {\Coq} system. +This means that a family of types in {\Set}, e.g. $\forall A:\Set, A +\rightarrow A$, is not a type in {\Set} and it cannot be applied on +itself. + +However, the sort {\Set} was impredicative in the original versions of +{\Coq}. For backward compatibility, or for experiments by +knowledgeable users, the logic of {\Coq} can be set impredicative for +{\Set} by calling {\Coq} with the option {\tt -impredicative-set}. + +{\Set} has been made predicative from version 8.0 of {\Coq}. The main +reason is to interact smoothly with a classical mathematical world +where both excluded-middle and the axiom of description are valid (see +file \vfile{\LogicClassicalDescription}{ClassicalDescription} for a +proof that excluded-middle and description implies the double negation +of excluded-middle in {\Set} and file {\tt Hurkens\_Set.v} from the +user contribution {\tt Rocq/PARADOXES} for a proof that +impredicativity of {\Set} implies the simple negation of +excluded-middle in {\Set}). + +\Question{Is {\Type} impredicative?} + +No, {\Type} is stratified. This is hidden for the +user, but {\Coq} internally maintains a set of constraints ensuring +stratification. + +If {\Type} were impredicative then it would be possible to encode +Girard's systems $U-$ and $U$ in {\Coq} and it is known from Girard, +Coquand, Hurkens and Miquel that systems $U-$ and $U$ are inconsistent +[Girard 1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding +can be found in file {\tt Logic/Hurkens.v} of {\Coq} standard library. + +For instance, when the user see {\tt $\forall$ X:Type, X->X : Type}, each +occurrence of {\Type} is implicitly bound to a different level, say +$\alpha$ and $\beta$ and the actual statement is {\tt +forall X:Type($\alpha$), X->X : Type($\beta$)} with the constraint +$\alpha<\beta$. + +When a statement violates a constraint, the message {\tt Universe +inconsistency} appears. Example: {\tt fun (x:Type) (y:$\forall$ X:Type, X +{\coqimp} X) => y x x}. + +\Question{I have two proofs of the same proposition. Can I prove they are equal?} + +In the base {\Coq} system, the answer is generally no. However, if +classical logic is set, the answer is yes for propositions in {\Prop}. +The answer is also yes if proof irrelevance holds (see question +\ref{proof-irrelevance}). + +There are also ``simple enough'' propositions for which you can prove +the equality without requiring any extra axioms. This is typically +the case for propositions defined deterministically as a first-order +inductive predicate on decidable sets. See for instance in question +\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of +the proposition {\tt le m n} (less or equal on {\tt nat}). + +% It is an ongoing work of research to natively include proof +% irrelevance in {\Coq}. + +\Question{I have two proofs of an equality statement. Can I prove they are +equal?} + + Yes, if equality is decidable on the domain considered (which +is the case for {\tt nat}, {\tt bool}, etc): see {\Coq} file +\verb=Eqdep_dec.v=). No otherwise, unless +assuming Streicher's axiom $K$ (see \cite{HofStr98}) or a more general +assumption such as proof-irrelevance (see \ref{proof-irrelevance}) or +classical logic. + +All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}. + +\Question{Can I prove that the second components of equal dependent +pairs are equal?} + + The answer is the same as for proofs of equality +statements. It is provable if equality on the domain of the first +component is decidable (look at \verb=inj_right_pair= from file +\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general +case. However, it is consistent (with the Calculus of Constructions) +to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually +provides an axiom (equivalent to Streicher's axiom $K$) which entails +the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}). + +\subsection{Impredicativity} + +\Question{Why {\tt injection} does not work on impredicative {\tt Set}?} + + E.g. in this case (this occurs only in the {\tt Set}-impredicative + variant of \Coq): + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Inductive I : Type := + intro : forall k:Set, k -> I. +Lemma eq_jdef : + forall x y:nat, intro _ x = intro _ y -> x = y. +Proof. + intros x y H; injection H. +\end{coq_example*} + + Injectivity of constructors is restricted to predicative types. If +injectivity on large inductive types were not restricted, we would be +allowed to derive an inconsistency (e.g. following the lines of +Burali-Forti paradox). The question remains open whether injectivity +is consistent on some large inductive types not expressive enough to +encode known paradoxes (such as type I above). + + +\Question{What is a ``large inductive definition''?} + +An inductive definition in {\Prop} or {\Set} is called large +if its constructors embed sets or propositions. As an example, here is +a large inductive type: + +\begin{coq_example*} +Inductive sigST (P:Set -> Set) : Type := + existST : forall X:Set, P X -> sigST P. +\end{coq_example*} + +In the {\tt Set} impredicative variant of {\Coq}, large inductive +definitions in {\tt Set} have restricted elimination schemes to +prevent inconsistencies. Especially, projecting the set or the +proposition content of a large inductive definition is forbidden. If +it were allowed, it would be possible to encode e.g. Burali-Forti +paradox \cite{Gir70,Coq85}. + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\section{Talkin' with the Rooster} + + +%%%%%%% +\subsection{My goal is ..., how can I prove it?} + + +\Question{My goal is a conjunction, how can I prove it?} + +Use some theorem or assumption or use the {\split} tactic. +\begin{coq_example} +Goal forall A B:Prop, A->B-> A/\B. +intros. +split. +assumption. +assumption. +Qed. +\end{coq_example} + +\Question{My goal contains a conjunction as an hypothesis, how can I use it?} + +If you want to decompose your hypothesis into other hypothesis you can use the {\decompose} tactic: + +\begin{coq_example} +Goal forall A B:Prop, A/\B-> B. +intros. +decompose [and] H. +assumption. +Qed. +\end{coq_example} + + +\Question{My goal is a disjunction, how can I prove it?} + +You can prove the left part or the right part of the disjunction using +{\left} or {\right} tactics. If you want to do a classical +reasoning step, use the {\tt classic} axiom to prove the right part with the assumption +that the left part of the disjunction is false. + +\begin{coq_example} +Goal forall A B:Prop, A-> A\/B. +intros. +left. +assumption. +Qed. +\end{coq_example} + +An example using classical reasoning: + +\begin{coq_example} +Require Import Classical. + +Ltac classical_right := +match goal with +| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) +end. + +Ltac classical_left := +match goal with +| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) +end. + + +Goal forall A B:Prop, (~A -> B) -> A\/B. +intros. +classical_right. +auto. +Qed. +\end{coq_example} + +\Question{My goal is an universally quantified statement, how can I prove it?} + +Use some theorem or assumption or introduce the quantified variable in +the context using the {\intro} tactic. If there are several +variables you can use the {\intros} tactic. A good habit is to +provide names for these variables: {\Coq} will do it anyway, but such +automatic naming decreases legibility and robustness. + + +\Question{My goal is an existential, how can I prove it?} + +Use some theorem or assumption or exhibit the witness using the {\existstac} tactic. +\begin{coq_example} +Goal exists x:nat, forall y, x+y=y. +exists 0. +intros. +auto. +Qed. +\end{coq_example} + + +\Question{My goal is solvable by some lemma, how can I prove it?} + +Just use the {\apply} tactic. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example} +Lemma mylemma : forall x, x+0 = x. +auto. +Qed. + +Goal 3+0 = 3. +apply mylemma. +Qed. +\end{coq_example} + + + +\Question{My goal contains False as an hypothesis, how can I prove it?} + +You can use the {\contradiction} or {\intuition} tactics. + + +\Question{My goal is an equality of two convertible terms, how can I prove it?} + +Just use the {\reflexivity} tactic. + +\begin{coq_example} +Goal forall x, 0+x = x. +intros. +reflexivity. +Qed. +\end{coq_example} + +\Question{My goal is a {\tt let x := a in ...}, how can I prove it?} + +Just use the {\intro} tactic. + + +\Question{My goal is a {\tt let (a, ..., b) := c in}, how can I prove it?} + +Just use the {\destruct} c as (a,...,b) tactic. + + +\Question{My goal contains some existential hypotheses, how can I use it?} + +You can use the tactic {\elim} with you hypotheses as an argument. + +\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?} + +\begin{verbatim} +Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H. +\end{verbatim} + + +\Question{My goal is an equality, how can I swap the left and right hand terms?} + +Just use the {\symmetry} tactic. +\begin{coq_example} +Goal forall x y : nat, x=y -> y=x. +intros. +symmetry. +assumption. +Qed. +\end{coq_example} + +\Question{My hypothesis is an equality, how can I swap the left and right hand terms?} + +Just use the {\symmetryin} tactic. + +\begin{coq_example} +Goal forall x y : nat, x=y -> y=x. +intros. +symmetry in H. +assumption. +Qed. +\end{coq_example} + + +\Question{My goal is an equality, how can I prove it by transitivity?} + +Just use the {\transitivity} tactic. +\begin{coq_example} +Goal forall x y z : nat, x=y -> y=z -> x=z. +intros. +transitivity y. +assumption. +assumption. +Qed. +\end{coq_example} + + +\Question{My goal would be solvable using {\tt apply;assumption} if it would not create meta-variables, how can I prove it?} + +You can use {\tt eapply yourtheorem;eauto} but it won't work in all cases ! (for example if more than one hypothesis match one of the subgoals generated by \eapply) so you should rather use {\tt try solve [eapply yourtheorem;eauto]}, otherwise some metavariables may be incorrectly instantiated. + +\begin{coq_example} +Lemma trans : forall x y z : nat, x=y -> y=z -> x=z. +intros. +transitivity y;assumption. +Qed. + +Goal forall x y z : nat, x=y -> y=z -> x=z. +intros. +eapply trans;eauto. +Qed. + +Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z. +intros. +eapply trans;eauto. +Undo. +eapply trans. +apply H. +auto. +Qed. + +Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z. +intros. +eapply trans;eauto. +Undo. +try solve [eapply trans;eauto]. +eapply trans. +apply H. +auto. +Qed. + +\end{coq_example} + +\Question{My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?} + +You can use a what is called a hints' base. + +\begin{coq_example} +Require Import ZArith. +Require Ring. +Open Local Scope Z_scope. +Lemma toto1 : 1+1 = 2. +ring. +Qed. +Lemma toto2 : 2+2 = 4. +ring. +Qed. +Lemma toto3 : 2+1 = 3. +ring. +Qed. + +Hint Resolve toto1 toto2 toto3 : mybase. + +Goal 2+(1+1)=4. +auto with mybase. +Qed. +\end{coq_example} + + +\Question{My goal is one of the hypotheses, how can I prove it?} + +Use the {\assumption} tactic. + +\begin{coq_example} +Goal 1=1 -> 1=1. +intro. +assumption. +Qed. +\end{coq_example} + + +\Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?} + +Use the {\exact} tactic. +\begin{coq_example} +Goal 1=1 -> 1=1 -> 1=1. +intros. +exact H0. +Qed. +\end{coq_example} + +\Question{What can be the difference between applying one hypothesis or another in the context of the last question?} + +From a proof point of view it is equivalent but if you want to extract +a program from your proof, the two hypotheses can lead to different +programs. + + +\Question{My goal is a propositional tautology, how can I prove it?} + +Just use the {\tauto} tactic. +\begin{coq_example} +Goal forall A B:Prop, A-> (A\/B) /\ A. +intros. +tauto. +Qed. +\end{coq_example} + +\Question{My goal is a first order formula, how can I prove it?} + +Just use the semi-decision tactic: \firstorder. + +\iffalse +todo: demander un exemple à Pierre +\fi + +\Question{My goal is solvable by a sequence of rewrites, how can I prove it?} + +Just use the {\congruence} tactic. +\begin{coq_example} +Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a. +intros. +congruence. +Qed. +\end{coq_example} + + +\Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?} + +Just use the {\congruence} tactic. + +\begin{coq_example} +Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b. +intros. +congruence. +Qed. +\end{coq_example} + + +\Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?} + +Just use the {\ring} tactic. + +\begin{coq_example} +Require Import ZArith. +Require Ring. +Open Local Scope Z_scope. +Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. +intros. +ring. +Qed. +\end{coq_example} + +\Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?} + +Just use the {\field} tactic. + +\begin{coq_example} +Require Import Reals. +Require Ring. +Open Local Scope R_scope. +Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. +intros. +field. +assumption. +Qed. +\end{coq_example} + + +\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?} + + +\begin{coq_example} +Require Import ZArith. +Require Omega. +Open Local Scope Z_scope. +Goal forall a : Z, a>0 -> a+a > a. +intros. +omega. +Qed. +\end{coq_example} + + +\Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?} + +You need the {\gb} tactic (see Loïc Pottier's homepage). + +\subsection{Tactics usage} + +\Question{I want to state a fact that I will use later as an hypothesis, how can I do it?} + +If you want to use forward reasoning (first proving the fact and then +using it) you just need to use the {\assert} tactic. If you want to use +backward reasoning (proving your goal using an assumption and then +proving the assumption) use the {\cut} tactic. + +\begin{coq_example} +Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. +intros. +assert (A->C). +intro;apply H0;apply H;assumption. +apply H2. +assumption. +Qed. + +Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. +intros. +cut (A->C). +intro. +apply H2;assumption. +intro;apply H0;apply H;assumption. +Qed. +\end{coq_example} + + + + +\Question{I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it?} + +You can use {\cut} followed by {\intro} or you can use the following {\Ltac} command: +\begin{verbatim} +Ltac assert_later t := cut t;[intro|idtac]. +\end{verbatim} + +\Question{What is the difference between {\Qed} and {\Defined}?} + +These two commands perform type checking, but when {\Defined} is used the new definition is set as transparent, otherwise it is defined as opaque (see \ref{opaque}). + + +\Question{How can I know what a tactic does?} + +You can use the {\tt info} command. + + + +\Question{Why {\auto} does not work? How can I fix it?} + +You can increase the depth of the proof search or add some lemmas in the base of hints. +Perhaps you may need to use \eauto. + +\Question{What is {\eauto}?} + +This is the same tactic as \auto, but it relies on {\eapply} instead of \apply. + +\iffalse +todo les espaces +\fi + +\Question{How can I speed up {\auto}?} + +You can use \texttt{info }\auto to replace {\auto} by the tactics it generates. +You can split your hint bases into smaller ones. + + +\Question{What is the equivalent of {\tauto} for classical logic?} + +Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation. + + +\Question{I want to replace some term with another in the goal, how can I do it?} + +If one of your hypothesis (say {\tt H}) states that the terms are equal you can use the {\rewrite} tactic. Otherwise you can use the {\replace} {\tt with} tactic. + +\Question{I want to replace some term with another in an hypothesis, how can I do it?} + +You can use the {\rewrite} {\tt in} tactic. + +\Question{I want to replace some symbol with its definition, how can I do it?} + +You can use the {\unfold} tactic. + +\Question{How can I reduce some term?} + +You can use the {\simpl} tactic. + +\Question{How can I declare a shortcut for some term?} + +You can use the {\set} or {\pose} tactics. + +\Question{How can I perform case analysis?} + +You can use the {\case} or {\destruct} tactics. + + +\Question{Why should I name my intros?} + +When you use the {\intro} tactic you don't have to give a name to your +hypothesis. If you do so the name will be generated by {\Coq} but your +scripts may be less robust. If you add some hypothesis to your theorem +(or change their order), you will have to change your proof to adapt +to the new names. + +\Question{How can I automatize the naming?} + +You can use the {\tt Show Intro.} or {\tt Show Intros.} commands to generate the names and use your editor to generate a fully named {\intro} tactic. +This can be automatized within {\tt xemacs}. + +\begin{coq_example} +Goal forall A B C : Prop, A -> B -> C -> A/\B/\C. +Show Intros. +(* +A B C H H0 +H1 +*) +intros A B C H H0 H1. +repeat split;assumption. +Qed. +\end{coq_example} + +\Question{I want to automatize the use of some tactic, how can I do it?} + +You need to use the {\tt proof with T} command and add {\ldots} at the +end of your sentences. + +For instance: +\begin{coq_example} +Goal forall A B C : Prop, A -> B/\C -> A/\B/\C. +Proof with assumption. +intros. +split... +Qed. +\end{coq_example} + +\Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it?} + +You need to use the {\try} and {\solve} tactics. For instance: +\begin{coq_example} +Require Import ZArith. +Require Ring. +Open Local Scope Z_scope. +Goal forall a b c : Z, a+b=b+a. +Proof with try solve [ring]. +intros... +Qed. +\end{coq_example} + +\Question{How can I do the opposite of the {\intro} tactic?} + +You can use the {\generalize} tactic. + +\begin{coq_example} +Goal forall A B : Prop, A->B-> A/\B. +intros. +generalize H. +intro. +auto. +Qed. +\end{coq_example} + +\Question{One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it?} + +You can use the {\subst} tactic. This will rewrite the equality everywhere and clear the assumption. + +\Question{What can I do if I get ``{\tt generated subgoal term has metavariables in it }''?} + +You should use the {\eapply} tactic, this will generate some goals containing metavariables. + +\Question{How can I instantiate some metavariable?} + +Just use the {\instantiate} tactic. + + +\Question{What is the use of the {\pattern} tactic?} + +The {\pattern} tactic transforms the current goal, performing +beta-expansion on all the applications featuring this tactic's +argument. For instance, if the current goal includes a subterm {\tt +phi(t)}, then {\tt pattern t} transforms the subterm into {\tt (fun +x:A => phi(x)) t}. This can be useful when {\apply} fails on matching, +to abstract the appropriate terms. + +\Question{What is the difference between assert, cut and generalize?} + +PS: Notice for people that are interested in proof rendering that \assert +and {\pose} (and \cut) are not rendered the same as {\generalize} (see the +HELM experimental rendering tool at \ahref{http://helm.cs.unibo.it/library.html}{\url{http://helm.cs.unibo.it}}, link +HELM, link COQ Online). Indeed {\generalize} builds a beta-expanded term +while \assert, {\pose} and {\cut} uses a let-in. + +\begin{verbatim} + (* Goal is T *) + generalize (H1 H2). + (* Goal is A->T *) + ... a proof of A->T ... +\end{verbatim} + +is rendered into something like +\begin{verbatim} + (h) ... the proof of A->T ... + we proved A->T + (h0) by (H1 H2) we proved A + by (h h0) we proved T +\end{verbatim} +while +\begin{verbatim} + (* Goal is T *) + assert q := (H1 H2). + (* Goal is A *) + ... a proof of A ... + (* Goal is A |- T *) + ... a proof of T ... +\end{verbatim} +is rendered into something like +\begin{verbatim} + (q) ... the proof of A ... + we proved A + ... the proof of T ... + we proved T +\end{verbatim} +Otherwise said, {\generalize} is not rendered in a forward-reasoning way, +while {\assert} is. + +\Question{What can I do if \Coq can not infer some implicit argument ?} + +You can state explicitely what this implicit argument is. See \ref{implicit}. + +\Question{How can I explicit some implicit argument ?}\label{implicit} + +Just use \texttt{A:=term} where \texttt{A} is the argument. + +For instance if you want to use the existence of ``nil'' on nat*nat lists: +\begin{verbatim} +exists (nil (A:=(nat*nat))). +\end{verbatim} + +\iffalse +\Question{Is there anyway to do pattern matching with dependent types?} + +todo +\fi + +\subsection{Proof management} + + +\Question{How can I change the order of the subgoals?} + +You can use the {\Focus} command to concentrate on some goal. When the goal is proved you will see the remaining goals. + +\Question{How can I change the order of the hypothesis?} + +You can use the {\tt Move ... after} command. + +\Question{How can I change the name of an hypothesis?} + +You can use the {\tt Rename ... into} command. + +\Question{How can I delete some hypothesis?} + +You can use the {\tt Clear} command. + +\Question{How can use a proof which is not finished?} + +You can use the {\tt Admitted} command to state your current proof as an axiom. + +\Question{How can I state a conjecture?} + +You can use the {\tt Admitted} command to state your current proof as an axiom. + +\Question{What is the difference between a lemma, a fact and a theorem?} + +From {\Coq} point of view there are no difference. But some tools can +have a different behavior when you use a lemma rather than a +theorem. For instance {\tt coqdoc} will not generate documentation for +the lemmas within your development. + +\Question{How can I organize my proofs?} + +You can organize your proofs using the section mechanism of \Coq. Have +a look at the manual for further information. + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\section{Inductive and Co-inductive types} + +\subsection{General} + +\Question{How can I prove that two constructors are different?} + +You can use the {\discriminate} tactic. + +\begin{coq_example} +Inductive toto : Set := | C1 : toto | C2 : toto. +Goal C1 <> C2. +discriminate. +Qed. +\end{coq_example} + +\Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?} + +Use the {\inversion} tactic. + + +\Question{How can I prove that 2 terms in an inductive set are equal? Or different?} + +Have a look at \coqtt{decide equality} and \coqtt{discriminate} in the \ahref{http://coq.inria.fr/doc/main.html}{Reference Manual}. + +\Question{Why is the proof of \coqtt{0+n=n} on natural numbers +trivial but the proof of \coqtt{n+0=n} is not?} + + Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument + +\begin{coq_example} +Print plus. +\end{coq_example} + +{\noindent} The expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons +modulo evaluation of expressions, \coqtt{0+n} and \coqtt{n} are +considered equal and the theorem \coqtt{0+n=n} is an instance of the +reflexivity of equality. On the other side, \coqtt{n+0} does not +evaluate to \coqtt{n} and a proof by induction on \coqtt{n} is +necessary to trigger the evaluation of \coqtt{+}. + +\Question{Why is dependent elimination in Prop not +available by default?} + + +This is just because most of the time it is not needed. To derive a +dependent elimination principle in {\tt Prop}, use the command {\tt Scheme} and +apply the elimination scheme using the \verb=using= option of +\verb=elim=, \verb=destruct= or \verb=induction=. + + +\Question{Argh! I cannot write expressions like ``~{\tt if n <= p then p else n}~'', as in any programming language} +\label{minmax} + +The short answer : You should use {\texttt le\_lt\_dec n p} instead.\\ + +That's right, you can't. +If you type for instance the following ``definition'': +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Definition max (n p : nat) := if n <= p then p else n. +\end{coq_example} + +As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a +statement that belongs to the mathematical world. There are many ways to +prove such a proposition, either by some computation, or using some already +proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy, +using some theorems on arithmetical operations. If you compute both numbers +before comparing them, you risk to use a lot of time and space. + + +On the contrary, a function for computing the greatest of two natural numbers +is an algorithm which, called on two natural numbers +$n$ and $p$, determines wether $n\leq p$ or $p < n$. +Such a function is a \emph{decision procedure} for the inequality of + \texttt{nat}. The possibility of writing such a procedure comes +directly from de decidability of the order $\leq$ on natural numbers. + + +When you write a piece of code like +``~\texttt{if n <= p then \dots{} else \dots}~'' +in a +programming language like \emph{ML} or \emph{Java}, a call to such a +decision procedure is generated. The decision procedure is in general +a primitive function, written in a low-level language, in the correctness +of which you have to trust. + +The standard Library of the system \emph{Coq} contains a +(constructive) proof of decidability of the order $\leq$ on +\texttt{nat} : the function \texttt{le\_lt\_dec} of +the module \texttt{Compare\_dec} of library \texttt{Arith}. + +The following code shows how to define correctly \texttt{min} and +\texttt{max}, and prove some properties of these functions. + +\begin{coq_example} +Require Import Compare_dec. + +Definition max (n p : nat) := if le_lt_dec n p then p else n. + +Definition min (n p : nat) := if le_lt_dec n p then n else p. + +Eval compute in (min 4 7). + +Theorem min_plus_max : forall n p, min n p + max n p = n + p. +Proof. + intros n p; + unfold min, max; + case (le_lt_dec n p); + simpl; auto with arith. +Qed. + +Theorem max_equiv : forall n p, max n p = p <-> n <= p. +Proof. + unfold max; intros n p; case (le_lt_dec n p);simpl; auto. + intuition auto with arith. + split. + intro e; rewrite e; auto with arith. + intro H; absurd (p < p); eauto with arith. +Qed. +\end{coq_example} + +\Question{I wrote my own decision procedure for $\leq$, which +is much faster than yours, but proving such theorems as + \texttt{max\_equiv} seems to be quite difficult} + +Your code is probably the following one: + +\begin{coq_example} +Fixpoint my_le_lt_dec (n p :nat) {struct n}: bool := + match n, p with 0, _ => true + | S n', S p' => my_le_lt_dec n' p' + | _ , _ => false + end. + +Definition my_max (n p:nat) := if my_le_lt_dec n p then p else n. + +Definition my_min (n p:nat) := if my_le_lt_dec n p then n else p. +\end{coq_example} + + +For instance, the computation of \texttt{my\_max 567 321} is almost +immediate, whereas one can't wait for the result of +\texttt{max 56 32}, using \emph{Coq's} \texttt{le\_lt\_dec}. + +This is normal. Your definition is a simple recursive function which +returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified +function}, i.e. a complex object, able not only to tell wether $n\leq p$ +or $p<n$, but also of building a complete proof of the correct inequality. +What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min} +and \texttt{max} is the building of a huge proof term. + +Nevertheless, \texttt{le\_lt\_dec} is very useful. Its type +is a strong specification, using the +\texttt{sumbool} type (look at the reference manual or chapter 9 of +\cite{coqart}). Eliminations of the form +``~\texttt{case (le\_lt\_dec n p)}~'' provide proofs of +either $n \leq p$ or $p < n$, allowing to prove easily theorems as in +question~\ref{minmax}. Unfortunately, this not the case of your +\texttt{my\_le\_lt\_dec}, which returns a quite non-informative boolean +value. + + +\begin{coq_example} +Check le_lt_dec. +\end{coq_example} + +You should keep in mind that \texttt{le\_lt\_dec} is useful to build +certified programs which need to compare natural numbers, and is not +designed to compare quickly two numbers. + +Nevertheless, the \emph{extraction} of \texttt{le\_lt\_dec} towards +\emph{Ocaml} or \emph{Haskell}, is a reasonable program for comparing two +natural numbers in Peano form in linear time. + +It is also possible to keep your boolean function as a decision procedure, +but you have to establish yourself the relationship between \texttt{my\_le\_lt\_dec} and the propositions $n\leq p$ and $p<n$: + +\begin{coq_example*} +Theorem my_le_lt_dec_true : + forall n p, my_le_lt_dec n p = true <-> n <= p. + +Theorem my_le_lt_dec_false : + forall n p, my_le_lt_dec n p = false <-> p < n. +\end{coq_example*} + + +\subsection{Recursion} + +\Question{Why can't I define a non terminating program?} + + Because otherwise the decidability of the type-checking +algorithm (which involves evaluation of programs) is not ensured. On +another side, if non terminating proofs were allowed, we could get a +proof of {\tt False}: + +\begin{coq_example*} +(* This is fortunately not allowed! *) +Fixpoint InfiniteProof (n:nat) : False := InfiniteProof n. +Theorem Paradox : False. +Proof (InfiniteProof O). +\end{coq_example*} + + +\Question{Why only structurally well-founded loops are allowed?} + + The structural order on inductive types is a simple and +powerful notion of termination. The consistency of the Calculus of +Inductive Constructions relies on it and another consistency proof +would have to be made for stronger termination arguments (such +as the termination of the evaluation of CIC programs themselves!). + +In spite of this, all non-pathological termination orders can be mapped +to a structural order. Tools to do this are provided in the file +\vfile{\InitWf}{Wf} of the standard library of {\Coq}. + +\Question{How to define loops based on non structurally smaller +recursive calls?} + + The procedure is as follows (we consider the definition of {\tt +mergesort} as an example). + +\begin{itemize} + +\item Define the termination order, say {\tt R} on the type {\tt A} of +the arguments of the loop. + +\begin{coq_eval} +Open Scope R_scope. +Require Import List. +\end{coq_eval} + +\begin{coq_example*} +Definition R (a b:list nat) := length a < length b. +\end{coq_example*} + +\item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}). + +\begin{coq_example*} +Lemma Rwf : well_founded R. +\end{coq_example*} + +\item Define the step function (which needs proofs that recursive +calls are on smaller arguments). + +\begin{coq_example*} +Definition split (l : list nat) + : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l} + := (* ... *) . +Definition concat (l1 l2 : list nat) : list nat := (* ... *) . +Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) := + let (lH1,lH2) := (split l) in + let (l1,H1) := lH1 in + let (l2,H2) := lH2 in + concat (f l1 H1) (f l2 H2). +\end{coq_example*} + +\item Define the recursive function by fixpoint on the step function. + +\begin{coq_example*} +Definition merge := Fix Rwf (fun _ => list nat) merge_step. +\end{coq_example*} + +\end{itemize} + +\Question{What is behind the accessibility and well-foundedness proofs?} + + Well-foundedness of some relation {\tt R} on some type {\tt A} +is defined as the accessibility of all elements of {\tt A} along {\tt R}. + +\begin{coq_example} +Print well_founded. +Print Acc. +\end{coq_example} + +The structure of the accessibility predicate is a well-founded tree +branching at each node {\tt x} in {\tt A} along all the nodes {\tt x'} +less than {\tt x} along {\tt R}. Any sequence of elements of {\tt A} +decreasing along the order {\tt R} are branches in the accessibility +tree. Hence any decreasing along {\tt R} is mapped into a structural +decreasing in the accessibility tree of {\tt R}. This is emphasised in +the definition of {\tt fix} which recurs not on its argument {\tt x:A} +but on the accessibility of this argument along {\tt R}. + +See file \vfile{\InitWf}{Wf}. + +\Question{How to perform simultaneous double induction?} + + In general a (simultaneous) double induction is simply solved by an +induction on the first hypothesis followed by an inversion over the +second hypothesis. Here is an example + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example} +Inductive even : nat -> Prop := + | even_O : even 0 + | even_S : forall n:nat, even n -> even (S (S n)). + +Inductive odd : nat -> Prop := + | odd_SO : odd 1 + | odd_S : forall n:nat, odd n -> odd (S (S n)). + +Lemma not_even_and_odd : forall n:nat, even n -> odd n -> False. +induction 1. + inversion 1. + inversion 1. apply IHeven; trivial. +\end{coq_example} +\begin{coq_eval} +Qed. +\end{coq_eval} + +In case the type of the second induction hypothesis is not +dependent, {\tt inversion} can just be replaced by {\tt destruct}. + +\Question{How to define a function by simultaneous double recursion?} + + The same trick applies, you can even use the pattern-matching +compilation algorithm to do the work for you. Here is an example: + +\begin{coq_example} +Fixpoint minus (n m:nat) {struct n} : nat := + match n, m with + | O, _ => 0 + | S k, O => S k + | S k, S l => minus k l + end. +Print minus. +\end{coq_example} + +In case of dependencies in the type of the induction objects +$t_1$ and $t_2$, an extra argument stating $t_1=t_2$ must be given to +the fixpoint definition + +\Question{How to perform nested and double induction?} + + To reason by nested (i.e. lexicographic) induction, just reason by +induction on the successive components. + +\smallskip + +Double induction (or induction on pairs) is a restriction of the +lexicographic induction. Here is an example of double induction. + +\begin{coq_example} +Lemma nat_double_ind : +forall P : nat -> nat -> Prop, P 0 0 -> + (forall m n, P m n -> P m (S n)) -> + (forall m n, P m n -> P (S m) n) -> + forall m n, P m n. +intros P H00 HmS HSn; induction m. +(* case 0 *) +induction n; [assumption | apply HmS; apply IHn]. +(* case Sm *) +intro n; apply HSn; apply IHm. +\end{coq_example} +\begin{coq_eval} +Qed. +\end{coq_eval} + +\Question{How to define a function by nested recursion?} + + The same trick applies. Here is the example of Ackermann +function. + +\begin{coq_example} +Fixpoint ack (n:nat) : nat -> nat := + match n with + | O => S + | S n' => + (fix ack' (m:nat) : nat := + match m with + | O => ack n' 1 + | S m' => ack n' (ack' m') + end) + end. +\end{coq_example} + + +\subsection{Co-inductive types} + +\Question{I have a cofixpoint $t:=F(t)$ and I want to prove $t=F(t)$. How to do it?} + +Just case-expand $F({\tt t})$ then complete by a trivial case analysis. +Here is what it gives on e.g. the type of streams on naturals + +\begin{coq_eval} +Set Implicit Arguments. +\end{coq_eval} +\begin{coq_example} +CoInductive Stream (A:Set) : Set := + Cons : A -> Stream A -> Stream A. +CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)). +Lemma Stream_unfold : + forall n:nat, nats n = Cons n (nats (S n)). +Proof. + intro; + change (nats n = match nats n with + | Cons x s => Cons x s + end). + case (nats n); reflexivity. +Qed. +\end{coq_example} + + + +\section{Syntax and notations} + +\Question{I do not want to type ``forall'' because it is too long, what can I do?} + +You can define your own notation for forall: +\begin{verbatim} +Notation "fa x : t, P" := (forall x:t, P) (at level 200, x ident). +\end{verbatim} +or if your are using {\CoqIde} you can define a pretty symbol for for all and an input method (see \ref{forallcoqide}). + + + +\Question{How can I define a notation for square?} + +You can use for instance: +\begin{verbatim} +Notation "x ^2" := (Rmult x x) (at level 20). +\end{verbatim} +Note that you can not use: +\begin{texttt} +Notation "x $^²$" := (Rmult x x) (at level 20). +\end{texttt} +because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8. + + +\Question{Why ``no associativity'' and ``left associativity'' at the same level does not work?} + +Because we relie on camlp4 for syntactical analysis and camlp4 does not really implement no associativity. By default, non associative operators are defined as right associative. + + + +\Question{How can I know the associativity associated with a level?} + +You can do ``Print Grammar constr'', and decode the output from camlp4, good luck ! + +\section{Modules} + + + + +%%%%%%% +\section{\Ltac} + +\Question{What is {\Ltac}?} + +{\Ltac} is the tactic language for \Coq. It provides the user with a +high-level ``toolbox'' for tactic creation. + +\Question{Why do I always get the same error message?} + + +\Question{Is there any printing command in {\Ltac}?} + +You can use the {\idtac} tactic with a string argument. This string +will be printed out. The same applies to the {\fail} tactic + +\Question{What is the syntax for let in {\Ltac}?} + +If $x_i$ are identifiers and $e_i$ and $expr$ are tactic expressions, then let reads: +\begin{center} +{\tt let $x_1$:=$e_1$ with $x_2$:=$e_2$\ldots with $x_n$:=$e_n$ in +$expr$}. +\end{center} +Beware that if $expr$ is complex (i.e. features at least a sequence) parenthesis +should be added around it. For example: +\begin{coq_example} +Ltac twoIntro := let x:=intro in (x;x). +\end{coq_example} + +\Question{What is the syntax for pattern matching in {\Ltac}?} + +Pattern matching on a term $expr$ (non-linear first order unification) +with patterns $p_i$ and tactic expressions $e_i$ reads: +\begin{center} +\hspace{10ex} +{\tt match $expr$ with +\hspace*{2ex}$p_1$ => $e_1$ +\hspace*{1ex}\textbar$p_2$ => $e_2$ +\hspace*{1ex}\ldots +\hspace*{1ex}\textbar$p_n$ => $e_n$ +\hspace*{1ex}\textbar\ \textunderscore\ => $e_{n+1}$ +end. +} +\end{center} +Underscore matches all terms. + +\Question{What is the semantics for ``match goal''?} + +The semantics of {\tt match goal} depends on whether it returns +tactics or not. The {\tt match goal} expression matches the current +goal against a series of patterns: {$hyp_1 {\ldots} hyp_n$ \textbar- +$ccl$}. It uses a first-order unification algorithm and in case of +success, if the right-hand-side is an expression, it tries to type it +while if the right-hand-side is a tactic, it tries to apply it. If the +typing or the tactic application fails, the {\tt match goal} tries all +the possible combinations of $hyp_i$ before dropping the branch and +moving to the next one. Underscore matches all terms. + +\Question{Why can't I use a ``match goal'' returning a tactic in a non +tail-recursive position?} + +This is precisely because the semantics of {\tt match goal} is to +apply the tactic on the right as soon as a pattern unifies what is +meaningful only in tail-recursive uses. + +The semantics in non tail-recursive call could have been the one used +for terms (i.e. fail if the tactic expression is not typable, but +don't try to apply it). For uniformity of semantics though, this has +been rejected. + +\Question{How can I generate a new name?} + +You can use the following syntax: +{\tt let id:=fresh in \ldots}\\ +For example: +\begin{coq_example} +Ltac introIdGen := let id:=fresh in intro id. +\end{coq_example} + + +\iffalse +\Question{How can I access the type of a term?} + +You can use typeof. +todo +\fi + +\Question{How can I define static and dynamic code?} + +\section{Tactics written in Ocaml} + +\Question{Can you show me an example of a tactic written in OCaml?} + +You have some examples of tactics written in Ocaml in the ``contrib'' directory of {\Coq} sources. + + + + +\section{Case studies} + + +\Question{How can I define vectors or lists of size n?} + +\Question{How to prove that 2 sets are different?} + + You need to find a property true on one set and false on the +other one. As an example we show how to prove that {\tt bool} and {\tt +nat} are discriminable. As discrimination property we take the +property to have no more than 2 elements. + +\begin{coq_example*} +Theorem nat_bool_discr : bool <> nat. +Proof. + pose (discr := + fun X:Set => + ~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))). + intro Heq; assert (H: discr bool). + intro H; apply (H true false); destruct x; auto. + rewrite Heq in H; apply H; clear H. + destruct a; destruct b as [|n]; intro H0; eauto. + destruct n; [ apply (H0 2); discriminate | eauto ]. +Qed. +\end{coq_example*} + +\Question{Is there an axiom-free proof of Streicher's axiom $K$ for +the equality on {\tt nat}?} +\label{K-nat} + +Yes, because equality is decidable on {\tt nat}. Here is the proof. + +\begin{coq_example*} +Require Import Eqdep_dec. +Require Import Peano_dec. +Theorem K_nat : + forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. +Proof. +intros; apply K_dec_set with (p := p). +apply eq_nat_dec. +assumption. +Qed. +\end{coq_example*} + +Similarly, we have + +\begin{coq_example*} +Theorem eq_rect_eq_nat : + forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h. +Proof. +intros; apply K_nat with (p := h); reflexivity. +Qed. +\end{coq_example*} + +\Question{How to prove that two proofs of {\tt n<=m} on {\tt nat} are equal?} +\label{le-uniqueness} + +This is provable without requiring any axiom because axiom $K$ +directly holds on {\tt nat}. Here is a proof using question \ref{K-nat}. + +\begin{coq_example*} +Require Import Arith. +Scheme le_ind' := Induction for le Sort Prop. +Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q. +Proof. +induction p using le_ind'; intro q. + replace (le_n n) with + (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)). + 2:reflexivity. + generalize (refl_equal n). + pattern n at 2 4 6 10, q; case q; [intro | intros m l e]. + rewrite <- eq_rect_eq_nat; trivial. + contradiction (le_Sn_n m); rewrite <- e; assumption. + replace (le_S n m p) with + (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))). + 2:reflexivity. + generalize (refl_equal (S m)). + pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS]. + contradiction (le_Sn_n m); rewrite Heq; assumption. + injection HeqS; intro Heq; generalize l HeqS. + rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat. + rewrite (IHp l0); reflexivity. +Qed. +\end{coq_example*} + +\Question{How to exploit equalities on sets} + +To extract information from an equality on sets, you need to +find a predicate of sets satisfied by the elements of the sets. As an +example, let's consider the following theorem. + +\begin{coq_example*} +Theorem interval_discr : + forall m n:nat, + {x : nat | x <= m} = {x : nat | x <= n} -> m = n. +\end{coq_example*} + +We have a proof requiring the axiom of proof-irrelevance. We +conjecture that proof-irrelevance can be circumvented by introducing a +primitive definition of discrimination of the proofs of +\verb!{x : nat | x <= m}!. + +\begin{latexonly}% +The proof can be found in file {\tt interval$\_$discr.v} in this directory. +%Here is the proof +%\begin{small} +%\begin{flushleft} +%\begin{texttt} +%\def_{\ifmmode\sb\else\subscr\fi} +%\include{interval_discr.v} +%%% WARNING semantics of \_ has changed ! +%\end{texttt} +%$a\_b\_c$ +%\end{flushleft} +%\end{small} +\end{latexonly}% +\begin{htmlonly}% +\ahref{./interval_discr.v}{Here} is the proof. +\end{htmlonly} + +\Question{I have a problem of dependent elimination on +proofs, how to solve it?} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Inductive Def1 : Set := c1 : Def1. +Inductive DefProp : Def1 -> Prop := + c2 : forall d:Def1, DefProp d. +Inductive Comb : Set := + c3 : forall d:Def1, DefProp d -> Comb. +Lemma eq_comb : + forall (d1 d1':Def1) (d2:DefProp d1) (d2':DefProp d1'), + d1 = d1' -> c3 d1 d2 = c3 d1' d2'. +\end{coq_example*} + + You need to derive the dependent elimination +scheme for DefProp by hand using {\coqtt Scheme}. + +\begin{coq_eval} +Abort. +\end{coq_eval} + +\begin{coq_example*} +Scheme DefProp_elim := Induction for DefProp Sort Prop. +Lemma eq_comb : + forall d1 d1':Def1, + d1 = d1' -> + forall (d2:DefProp d1) (d2':DefProp d1'), c3 d1 d2 = c3 d1' d2'. +intros. +destruct H. +destruct d2 using DefProp_elim. +destruct d2' using DefProp_elim. +reflexivity. +Qed. +\end{coq_example*} + + +\Question{And what if I want to prove the following?} + +\begin{coq_example*} +Inductive natProp : nat -> Prop := + | p0 : natProp 0 + | pS : forall n:nat, natProp n -> natProp (S n). +Inductive package : Set := + pack : forall n:nat, natProp n -> package. +Lemma eq_pack : + forall n n':nat, + n = n' -> + forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'. +\end{coq_example*} + + + +\begin{coq_eval} +Abort. +\end{coq_eval} +\begin{coq_example*} +Scheme natProp_elim := Induction for natProp Sort Prop. +Definition pack_S : package -> package. +destruct 1. +apply (pack (S n)). +apply pS; assumption. +Defined. +Lemma eq_pack : + forall n n':nat, + n = n' -> + forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'. +intros n n' Heq np np'. +generalize dependent n'. +induction np using natProp_elim. +induction np' using natProp_elim; intros; auto. + discriminate Heq. +induction np' using natProp_elim; intros; auto. + discriminate Heq. +change (pack_S (pack n np) = pack_S (pack n0 np')). +apply (f_equal (A:=package)). +apply IHnp. +auto. +Qed. +\end{coq_example*} + + + + + + + +\section{Publishing tools} + +\Question{How can I generate some latex from my development?} + +You can use {\tt coqdoc}. + +\Question{How can I generate some HTML from my development?} + +You can use {\tt coqdoc}. + +\Question{How can I generate some dependency graph from my development?} + +\Question{How can I cite some {\Coq} in my latex document?} + +You can use {\tt coq\_tex}. + +\Question{How can I cite the {\Coq} reference manual?} + +You can use this bibtex entry: +\begin{verbatim} +@Manual{Coq:manual, + title = {The Coq proof assistant reference manual}, + author = {\mbox{The Coq development team}}, + organization = {LogiCal Project}, + note = {Version 8.0}, + year = {2004}, + url = "http://coq.inria.fr" +} +\end{verbatim} + +\Question{Where can I publish my developments in {\Coq}?} + +You can submit your developments as a user contribution to the {\Coq} +development team. This ensures its liveness along the evolution and +possible changes of {\Coq}. + +You can also submit your developments to the HELM/MoWGLI repository at +the University of Bologna (see +\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}). For +developments submitted in this database, it is possible to visualize +the developments in natural language and execute various retrieving +requests. + +\Question{How can I read my proof in natural language?} + +You can submit your proof to the HELM/MoWGLI repository and use the +rendering tool provided by the server (see +\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}). + +\section{\CoqIde} + +\Question{What is {\CoqIde}?} + +{\CoqIde} is a gtk based GUI for \Coq. + +\Question{How to enable Emacs keybindings?} + Insert \texttt{gtk-key-theme-name = "Emacs"} + in your \texttt{.coqide-gtk2rc} file. It may be in the current dir + or in \verb#$HOME# dir. This is done by default. + +%$ juste pour que la coloration emacs marche + +\Question{How to enable antialiased fonts?} + + Set the \verb#GDK_USE_XFT# variable to \verb#1#. This is by default with \verb#Gtk >= 2.2#. + If some of your fonts are not available, set \verb#GDK_USE_XFT# to \verb#0#. + +\Question{How to use those Forall and Exists pretty symbols?}\label{forallcoqide} + Thanks to the notation features in \Coq, you just need to insert these +lines in your {\Coq} buffer:\\ +\begin{texttt} +Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident). +\end{texttt}\\ +\begin{texttt} +Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident). +\end{texttt} + +Copy/Paste of these lines from this file will not work outside of \CoqIde. +You need to load a file containing these lines or to enter the $\forall$ +using an input method (see \ref{inputmeth}). To try it just use \verb#Require Import utf8# from inside +\CoqIde. +To enable these notations automatically start coqide with +\begin{verbatim} + coqide -l utf8 +\end{verbatim} +In the ide subdir of {\Coq} library, you will find a sample utf8.v with some +pretty simple notations. + +\Question{How to define an input method for non ASCII symbols?}\label{inputmeth} + +\begin{itemize} +\item First solution: type \verb#<CONTROL><SHIFT>2200# to enter a forall in the script widow. + 2200 is the hexadecimal code for forall in unicode charts and is encoded as + in UTF-8. + 2203 is for exists. See \ahref{http://www.unicode.org}{\url{http://www.unicode.org}} for more codes. +\item Second solution: rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. + Under X11, you need to use something like +\begin{verbatim} + xmodmap -e "keycode 24 = a A F13 F13" + xmodmap -e "keycode 26 = e E F14 F14" +\end{verbatim} + and then to add +\begin{verbatim} + bind "F13" {"insert-at-cursor" ("")} + bind "F14" {"insert-at-cursor" ("")} +\end{verbatim} + to your "binding "text"" section in \verb#.coqiderc-gtk2rc.# + The strange ("") argument is the UTF-8 encoding for + 0x2200. + You can compute these encodings using the lablgtk2 toplevel with +\begin{verbatim} +Glib.Utf8.from_unichar 0x2200;; +\end{verbatim} + Further symbols can be bound on higher Fxx keys or on even on other keys you + do not need . +\end{itemize} + +\Question{How to build a custom {\CoqIde} with user ml code?} + Use + coqmktop -ide -byte m1.cmo...mi.cmo + or + coqmktop -ide -opt m1.cmx...mi.cmx + +\Question{How to customize the shortcuts for menus?} + Two solutions are offered: +\begin{itemize} +\item Edit \$HOME/.coqide.keys by hand or +\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then + from \CoqIde, you may select a menu entry and press the desired + shortcut. +\end{itemize} + +\Question{What encoding should I use? What is this $\backslash$x\{iiii\} in my file?} + The encoding option is related to the way files are saved. + Keep it as UTF-8 until it becomes important for you to exchange files + with non UTF-8 aware applications. + If you choose something else than UTF-8, then missing characters will + be encoded by $\backslash$x\{....\} or $\backslash$x\{........\} + where each dot is an hex. digit. + The number between braces is the hexadecimal UNICODE index for the + missing character. + + + + +\section{Extraction} + +\Question{What is program extraction?} + +Program extraction consist in generating a program from a constructive proof. + +\Question{Which language can I extract to?} + +You can extract your programs to Objective Caml and Haskell. + +\Question{How can I extract an incomplete proof?} + +You can provide programs for your axioms. + + + +%%%%%%% +\section{Glossary} + +\Question{Can you explain me what an evaluable constant is?} + +An evaluable constant is a constant which is unfoldable. + +\Question{What is a goal?} + +The goal is the statement to be proved. + +\Question{What is a meta variable?} + +A meta variable in {\Coq} represents a ``hole'', i.e. a part of a proof +that is still unknown. + +\Question{What is Gallina?} + +Gallina is the specification language of \Coq. Complete documentation +of this language can be found in the Reference Manual. + +\Question{What is The Vernacular?} + +It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots} + + +\Question{What is a dependent type?} + +A dependant type is a type which depends on some term. For instance +``vector of size n'' is a dependant type representing all the vectors +of size $n$. Its type depends on $n$ + +\Question{What is a proof by reflection?} + +This is a proof generated by some computation which is done using the +internal reduction of {\Coq} (not using the tactic language of {\Coq} +(\Ltac) nor the implementation language for \Coq). An example of +tactic using the reflection mechanism is the {\ring} tactic. The +reflection method consist in reflecting a subset of {\Coq} language (for +example the arithmetical expressions) into an object of the \Coq +language itself (in this case an inductive type denoting arithmetical +expressions). For more information see~\cite{howe,harrison,boutin} +and the last chapter of the Coq'Art. + +\Question{What is intuitionistic logic?} + +This is any logic which does not assume that ``A or not A''. + + +\Question{What is proof-irrelevance?} + +See question \ref{proof-irrelevance} + + +\Question{What is the difference between opaque and transparent?}{\label{opaque}} + +Opaque definitions can not be unfolded but transparent ones can. + + +\section{Troubleshooting} + +\Question{What can I do when {\tt Qed.} is slow?} + +Sometime you can use the {\abstracttac} tactic, which makes as if you had +stated some local lemma, this speeds up the typing process. + +\Question{Why \texttt{Reset Initial.} does not work when using \texttt{coqc}?} + +The initial state corresponds to the state of coqtop when the interactive +session began. It does not make sense in files to compile. + + +\Question{What can I do if I get ``No more subgoals but non-instantiated existential variables''?} + +This means that {\eauto} or {\eapply} didn't instantiate an +existential variable which eventually got erased by some computation. +You have to backtrack to the faulty occurrence of {\eauto} or +{\eapply} and give the missing argument an explicit value. + +\Question{What can I do if I get ``Cannot solve a second-order unification problem''?} + +You can help {\Coq} using the {\pattern} tactic. + +\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?} + + This is because \texttt{\{x:A|P x\}} is a notation for +\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to +$\eta$-conversion, this is different from \texttt{sig P}. + + +\Question{I copy-paste a term and {\Coq} says it is not convertible + to the original term. Sometimes it even says the copied term is not +well-typed.} + + This is probably due to invisible implicit information (implicit +arguments, coercions and Cases annotations) in the printed term, which +is not re-synthesised from the copied-pasted term in the same way as +it is in the original term. + + Consider for instance {\tt (@eq Type True True)}. This term is +printed as {\tt True=True} and re-parsed as {\tt (@eq Prop True +True)}. The two terms are not convertible (hence they fool tactics +like {\tt pattern}). + + There is currently no satisfactory answer to the problem. However, +the command {\tt Set Printing All} is useful for diagnosing the +problem. + + Due to coercions, one may even face type-checking errors. In some +rare cases, the criterion to hide coercions is a bit too loose, which +may result in a typing error message if the parser is not able to find +again the missing coercion. + + + +\section{Conclusion and Farewell.} +\label{ccl} + +\Question{What if my question isn't answered here?} +\label{lastquestion} + +Don't panic \verb+:-)+. You can try the {\Coq} manual~\cite{Coq:manual} for a technical +description of the prover. The Coq'Art~\cite{Coq:coqart} is the first +book written on {\Coq} and provides a comprehensive review of the +theorem prover as well as a number of example and exercises. Finally, +the tutorial~\cite{Coq:Tutorial} provides a smooth introduction to +theorem proving in \Coq. + + +%%%%%%% +\newpage +\nocite{LaTeX:intro} +\nocite{LaTeX:symb} +\bibliography{fk} + +%%%%%%% +\typeout{*********************************************} +\typeout{********* That makes \thequestion{\space} questions **********} +\typeout{*********************************************} + +\end{document} diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps new file mode 100644 index 00000000..3f3c01c4 --- /dev/null +++ b/doc/faq/axioms.eps @@ -0,0 +1,378 @@ +%!PS-Adobe-2.0 EPSF-2.0 +%%Title: axioms.fig +%%Creator: fig2dev Version 3.2 Patchlevel 4 +%%CreationDate: Wed May 5 18:30:03 2004 +%%For: herbelin@limoux.polytechnique.fr (Hugo Herbelin) +%%BoundingBox: 0 0 437 372 +%%Magnification: 1.0000 +%%EndComments +/$F2psDict 200 dict def +$F2psDict begin +$F2psDict /mtrx matrix put +/col-1 {0 setgray} bind def +/col0 {0.000 0.000 0.000 srgb} bind def +/col1 {0.000 0.000 1.000 srgb} bind def +/col2 {0.000 1.000 0.000 srgb} bind def +/col3 {0.000 1.000 1.000 srgb} bind def +/col4 {1.000 0.000 0.000 srgb} bind def +/col5 {1.000 0.000 1.000 srgb} bind def +/col6 {1.000 1.000 0.000 srgb} bind def +/col7 {1.000 1.000 1.000 srgb} bind def +/col8 {0.000 0.000 0.560 srgb} bind def +/col9 {0.000 0.000 0.690 srgb} bind def +/col10 {0.000 0.000 0.820 srgb} bind def +/col11 {0.530 0.810 1.000 srgb} bind def +/col12 {0.000 0.560 0.000 srgb} bind def +/col13 {0.000 0.690 0.000 srgb} bind def +/col14 {0.000 0.820 0.000 srgb} bind def +/col15 {0.000 0.560 0.560 srgb} bind def +/col16 {0.000 0.690 0.690 srgb} bind def +/col17 {0.000 0.820 0.820 srgb} bind def +/col18 {0.560 0.000 0.000 srgb} bind def +/col19 {0.690 0.000 0.000 srgb} bind def +/col20 {0.820 0.000 0.000 srgb} bind def +/col21 {0.560 0.000 0.560 srgb} bind def +/col22 {0.690 0.000 0.690 srgb} bind def +/col23 {0.820 0.000 0.820 srgb} bind def +/col24 {0.500 0.190 0.000 srgb} bind def +/col25 {0.630 0.250 0.000 srgb} bind def +/col26 {0.750 0.380 0.000 srgb} bind def +/col27 {1.000 0.500 0.500 srgb} bind def +/col28 {1.000 0.630 0.630 srgb} bind def +/col29 {1.000 0.750 0.750 srgb} bind def +/col30 {1.000 0.880 0.880 srgb} bind def +/col31 {1.000 0.840 0.000 srgb} bind def + +end +save +newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpath +-90.0 435.2 translate +1 -1 scale + +/cp {closepath} bind def +/ef {eofill} bind def +/gr {grestore} bind def +/gs {gsave} bind def +/sa {save} bind def +/rs {restore} bind def +/l {lineto} bind def +/m {moveto} bind def +/rm {rmoveto} bind def +/n {newpath} bind def +/s {stroke} bind def +/sh {show} bind def +/slc {setlinecap} bind def +/slj {setlinejoin} bind def +/slw {setlinewidth} bind def +/srgb {setrgbcolor} bind def +/rot {rotate} bind def +/sc {scale} bind def +/sd {setdash} bind def +/ff {findfont} bind def +/sf {setfont} bind def +/scf {scalefont} bind def +/sw {stringwidth} bind def +/tr {translate} bind def +/tnt {dup dup currentrgbcolor + 4 -2 roll dup 1 exch sub 3 -1 roll mul add + 4 -2 roll dup 1 exch sub 3 -1 roll mul add + 4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb} + bind def +/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul + 4 -2 roll mul srgb} bind def +/reencdict 12 dict def /ReEncode { reencdict begin +/newcodesandnames exch def /newfontname exch def /basefontname exch def +/basefontdict basefontname findfont def /newfont basefontdict maxlength dict def +basefontdict { exch dup /FID ne { dup /Encoding eq +{ exch dup length array copy newfont 3 1 roll put } +{ exch newfont 3 1 roll put } ifelse } { pop pop } ifelse } forall +newfont /FontName newfontname put newcodesandnames aload pop +128 1 255 { newfont /Encoding get exch /.notdef put } for +newcodesandnames length 2 idiv { newfont /Encoding get 3 1 roll put } repeat +newfontname newfont definefont pop end } def +/isovec [ +8#055 /minus 8#200 /grave 8#201 /acute 8#202 /circumflex 8#203 /tilde +8#204 /macron 8#205 /breve 8#206 /dotaccent 8#207 /dieresis +8#210 /ring 8#211 /cedilla 8#212 /hungarumlaut 8#213 /ogonek 8#214 /caron +8#220 /dotlessi 8#230 /oe 8#231 /OE +8#240 /space 8#241 /exclamdown 8#242 /cent 8#243 /sterling +8#244 /currency 8#245 /yen 8#246 /brokenbar 8#247 /section 8#250 /dieresis +8#251 /copyright 8#252 /ordfeminine 8#253 /guillemotleft 8#254 /logicalnot +8#255 /hyphen 8#256 /registered 8#257 /macron 8#260 /degree 8#261 /plusminus +8#262 /twosuperior 8#263 /threesuperior 8#264 /acute 8#265 /mu 8#266 /paragraph +8#267 /periodcentered 8#270 /cedilla 8#271 /onesuperior 8#272 /ordmasculine +8#273 /guillemotright 8#274 /onequarter 8#275 /onehalf +8#276 /threequarters 8#277 /questiondown 8#300 /Agrave 8#301 /Aacute +8#302 /Acircumflex 8#303 /Atilde 8#304 /Adieresis 8#305 /Aring +8#306 /AE 8#307 /Ccedilla 8#310 /Egrave 8#311 /Eacute +8#312 /Ecircumflex 8#313 /Edieresis 8#314 /Igrave 8#315 /Iacute +8#316 /Icircumflex 8#317 /Idieresis 8#320 /Eth 8#321 /Ntilde 8#322 /Ograve +8#323 /Oacute 8#324 /Ocircumflex 8#325 /Otilde 8#326 /Odieresis 8#327 /multiply +8#330 /Oslash 8#331 /Ugrave 8#332 /Uacute 8#333 /Ucircumflex +8#334 /Udieresis 8#335 /Yacute 8#336 /Thorn 8#337 /germandbls 8#340 /agrave +8#341 /aacute 8#342 /acircumflex 8#343 /atilde 8#344 /adieresis 8#345 /aring +8#346 /ae 8#347 /ccedilla 8#350 /egrave 8#351 /eacute +8#352 /ecircumflex 8#353 /edieresis 8#354 /igrave 8#355 /iacute +8#356 /icircumflex 8#357 /idieresis 8#360 /eth 8#361 /ntilde 8#362 /ograve +8#363 /oacute 8#364 /ocircumflex 8#365 /otilde 8#366 /odieresis 8#367 /divide +8#370 /oslash 8#371 /ugrave 8#372 /uacute 8#373 /ucircumflex +8#374 /udieresis 8#375 /yacute 8#376 /thorn 8#377 /ydieresis] def +/Times-Roman /Times-Roman-iso isovec ReEncode +/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def +/$F2psEnd {$F2psEnteredState restore end} def + +$F2psBegin +10 setmiterlimit +0 slj 0 slc + 0.06000 0.06000 sc +% +% Fig objects follow +% +% +% here starts figure with depth 50 +% Arc +7.500 slw +gs clippath +3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp +eoclip +n 3600.0 6750.0 150.0 90.0 -90.0 arc +gs col0 s gr + gr + +% arrowhead +n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l cp gs 0.00 setgray ef gr col0 s +% Arc +gs clippath +3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp +eoclip +n 3600.0 6450.0 150.0 90.0 -90.0 arc +gs col0 s gr + gr + +% arrowhead +n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l cp gs 0.00 setgray ef gr col0 s +% Arc +gs clippath +3626 6020 m 3599 5966 l 3465 6034 l 3586 6007 l 3492 6087 l cp +3599 6333 m 3626 6279 l 3492 6212 l 3586 6293 l 3465 6265 l cp +eoclip +n 3600.0 6150.0 150.0 90.0 -90.0 arc +gs col0 s gr + gr + +% arrowhead +n 3492 6087 m 3586 6007 l 3465 6034 l 3492 6087 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3465 6265 m 3586 6293 l 3492 6212 l 3465 6265 l cp gs 0.00 setgray ef gr col0 s +% Arc +gs clippath +3626 6320 m 3599 6266 l 3465 6334 l 3586 6307 l 3492 6387 l cp +3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp +eoclip +n 3600.0 6450.0 150.0 90.0 -90.0 arc +gs col0 s gr + gr + +% arrowhead +n 3492 6387 m 3586 6307 l 3465 6334 l 3492 6387 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l cp gs 0.00 setgray ef gr col0 s +% Arc +gs clippath +3626 6620 m 3599 6566 l 3465 6634 l 3586 6607 l 3492 6687 l cp +3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp +eoclip +n 3600.0 6750.0 150.0 90.0 -90.0 arc +gs col0 s gr + gr + +% arrowhead +n 3492 6687 m 3586 6607 l 3465 6634 l 3492 6687 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l cp gs 0.00 setgray ef gr col0 s +% Arc +gs clippath +3626 6920 m 3599 6866 l 3465 6934 l 3586 6907 l 3492 6987 l cp +3599 7233 m 3626 7179 l 3492 7112 l 3586 7193 l 3465 7165 l cp +eoclip +n 3600.0 7050.0 150.0 90.0 -90.0 arc +gs col0 s gr + gr + +% arrowhead +n 3492 6987 m 3586 6907 l 3465 6934 l 3492 6987 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3465 7165 m 3586 7193 l 3492 7112 l 3465 7165 l cp gs 0.00 setgray ef gr col0 s +% Arc +gs clippath +4168 4060 m 4227 4068 l 4247 3919 l 4202 4034 l 4188 3911 l cp +eoclip +n 14032.5 5272.5 9908.2 -159.9 -172.9 arcn +gs col0 s gr + gr + +% arrowhead +n 4188 3911 m 4202 4034 l 4247 3919 l 4188 3911 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +4170 5790 m 4230 5790 l 4230 5639 l 4200 5759 l 4170 5639 l cp +eoclip +n 4200 5175 m + 4200 5775 l gs col0 s gr gr + +% arrowhead +n 4170 5639 m 4200 5759 l 4230 5639 l 4170 5639 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +4553 5749 m 4567 5807 l 4714 5771 l 4591 5771 l 4700 5713 l cp +eoclip +n 7050 5175 m + 4575 5775 l gs col0 s gr gr + +% arrowhead +n 4700 5713 m 4591 5771 l 4714 5771 l 4700 5713 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +4170 4890 m 4230 4890 l 4230 4739 l 4200 4859 l 4170 4739 l cp +eoclip +n 4200 4275 m + 4200 4875 l gs col0 s gr gr + +% arrowhead +n 4170 4739 m 4200 4859 l 4230 4739 l 4170 4739 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +7131 4907 m 7147 4850 l 7001 4810 l 7109 4871 l 6985 4868 l cp +eoclip +n 4950 4275 m + 7125 4875 l gs col0 s gr gr + +% arrowhead +n 6985 4868 m 7109 4871 l 7001 4810 l 6985 4868 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +7167 4057 m 7225 4071 l 7262 3924 l 7204 4034 l 7204 3910 l cp +eoclip +n 7725 1950 m + 7200 4050 l gs col0 s gr gr + +% arrowhead +n 7204 3910 m 7204 4034 l 7262 3924 l 7204 3910 l cp gs 0.00 setgray ef gr col0 s +% Polyline +n 4350 3075 m + 7350 1950 l gs col0 s gr +% Polyline +gs clippath +7170 4890 m 7230 4890 l 7230 4739 l 7200 4859 l 7170 4739 l cp +eoclip +n 7200 4275 m + 7200 4875 l gs col0 s gr gr + +% arrowhead +n 7170 4739 m 7200 4859 l 7230 4739 l 7170 4739 l cp gs 0.00 setgray ef gr col0 s +% Polyline +n 3075 1875 m + 3975 1875 l gs col0 s gr +% Polyline +gs clippath +5520 4065 m 5580 4065 l 5580 3914 l 5550 4034 l 5520 3914 l cp +5580 3660 m 5520 3660 l 5520 3811 l 5550 3691 l 5580 3811 l cp +eoclip +n 5550 3675 m + 5550 4050 l gs col0 s gr gr + +% arrowhead +n 5580 3811 m 5550 3691 l 5520 3811 l 5580 3811 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 5520 3914 m 5550 4034 l 5580 3914 l 5520 3914 l cp gs 0.00 setgray ef gr col0 s +% Polyline +n 4575 4050 m + 6450 4050 l gs col0 s gr +% Polyline +gs clippath +3495 2265 m 3555 2265 l 3555 2114 l 3525 2234 l 3495 2114 l cp +3555 1860 m 3495 1860 l 3495 2011 l 3525 1891 l 3555 2011 l cp +eoclip +n 3525 1875 m + 3525 2250 l gs col0 s gr gr + +% arrowhead +n 3555 2011 m 3525 1891 l 3495 2011 l 3555 2011 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3495 2114 m 3525 2234 l 3555 2114 l 3495 2114 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +2219 3988 m 2279 3991 l 2285 3840 l 2251 3959 l 2225 3838 l cp +eoclip +n 2325 1875 m + 2250 3975 l gs col0 s gr gr + +% arrowhead +n 2225 3838 m 2251 3959 l 2285 3840 l 2225 3838 l cp gs 0.00 setgray ef gr col0 s +% Polyline +n 7800 1275 m + 2100 1275 l gs col0 s gr +/Times-Roman-iso ff 180.00 scf sf +6600 5100 m +gs 1 -1 sc (Proof-irrelevance) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3675 4200 m +gs 1 -1 sc (Excluded-middle) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +6900 1800 m +gs 1 -1 sc (Predicate extensionality) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3375 3525 m +gs 1 -1 sc (\(Diaconescu\)) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +4650 3600 m +gs 1 -1 sc (Propositional degeneracy) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3825 1800 m +gs 1 -1 sc (Relational choice axiom) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +1725 1800 m +gs 1 -1 sc (Description principle) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +2550 2400 m +gs 1 -1 sc (Functional choice axiom) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3600 5100 m +gs 1 -1 sc (Decidability of equality on $A$) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +4425 4575 m +gs 1 -1 sc (\(needs Prop-impredicativity\)) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +5025 4725 m +gs 1 -1 sc (\(Berardi\)) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +1500 3075 m +gs 1 -1 sc (\(if Set impredicative\)) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +1500 4200 m +gs 1 -1 sc (Not excluded-middle) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3600 6000 m +gs 1 -1 sc (Axiom K on A) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3600 7200 m +gs 1 -1 sc (Invariance by substitution of reflexivity proofs for equality on A) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +6150 4200 m +gs 1 -1 sc (Propositional extensionality) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +2100 1200 m +gs 1 -1 sc (The dependency graph of axioms in the Calculus of Inductive Constructions) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3600 6900 m +gs 1 -1 sc (Injectivity of equality on sigma-types on A) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3600 6300 m +gs 1 -1 sc (Uniqueness of reflexivity proofs for equality on A) col0 sh gr +/Times-Roman-iso ff 180.00 scf sf +3600 6600 m +gs 1 -1 sc (Uniqueness of equality proofs on A) col0 sh gr +% here ends figure; +$F2psEnd +rs +showpage diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig new file mode 100644 index 00000000..f0775930 --- /dev/null +++ b/doc/faq/axioms.fig @@ -0,0 +1,84 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600 + 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300 + 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6150.000 3600 6300 3450 6150 3600 6000 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 7050.000 3600 7200 3450 7050 3600 6900 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 5272.500 4725 1875 4425 2850 4200 4050 + 1 1 1.00 60.00 120.00 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 4200 5175 4200 5775 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 7050 5175 4575 5775 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 4200 4275 4200 4875 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 4950 4275 7125 4875 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 7725 1950 7200 4050 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 4350 3075 7350 1950 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 7200 4275 7200 4875 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 3075 1875 3975 1875 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 + 5550 3675 5550 4050 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 4575 4050 6450 4050 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 + 3525 1875 3525 2250 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 2325 1875 2250 3975 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 7800 1275 2100 1275 +4 0 0 50 -1 0 12 0.0000 4 135 1305 6600 5100 Proof-irrelevance\001 +4 0 0 50 -1 0 12 0.0000 4 135 1260 3675 4200 Excluded-middle\001 +4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 1800 Predicate extensionality\001 +4 0 0 50 -1 0 12 0.0000 4 180 1050 3375 3525 (Diaconescu)\001 +4 0 0 50 -1 0 12 0.0000 4 180 1905 4650 3600 Propositional degeneracy\001 +4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 1800 Relational choice axiom\001 +4 0 0 50 -1 0 12 0.0000 4 180 1575 1725 1800 Description principle\001 +4 0 0 50 -1 0 12 0.0000 4 135 1830 2550 2400 Functional choice axiom\001 +4 0 0 50 -1 0 12 0.0000 4 195 2340 3600 5100 Decidability of equality on $A$\001 +4 0 0 50 -1 0 12 0.0000 4 180 2175 4425 4575 (needs Prop-impredicativity)\001 +4 0 0 50 -1 0 12 0.0000 4 180 705 5025 4725 (Berardi)\001 +4 0 0 50 -1 0 12 0.0000 4 180 1620 1500 3075 (if Set impredicative)\001 +4 0 0 50 -1 0 12 0.0000 4 135 1560 1500 4200 Not excluded-middle\001 +4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 6000 Axiom K on A\001 +4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 7200 Invariance by substitution of reflexivity proofs for equality on A\001 +4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 4200 Propositional extensionality\001 +4 0 0 50 -1 0 12 0.0000 4 180 5700 2100 1200 The dependency graph of axioms in the Calculus of Inductive Constructions\001 +4 0 0 50 -1 0 12 0.0000 4 180 3210 3600 6900 Injectivity of equality on sigma-types on A\001 +4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 6300 Uniqueness of reflexivity proofs for equality on A\001 +4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 6600 Uniqueness of equality proofs on A\001 diff --git a/doc/faq/axioms.png b/doc/faq/axioms.png Binary files differnew file mode 100644 index 00000000..2aee0916 --- /dev/null +++ b/doc/faq/axioms.png diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib new file mode 100644 index 00000000..d41ab7f0 --- /dev/null +++ b/doc/faq/fk.bib @@ -0,0 +1,2221 @@ +%%%%%%% FAQ %%%%%%% + +@book{ProofsTypes, + Author="Girard, Jean-Yves and Yves Lafont and Paul Taylor", + Title="Proofs and Types", + Publisher="Cambrige Tracts in Theoretical Computer Science, Cambridge University Press", + Year="1989" +} + +@misc{Types:Dowek, + author = "Gilles Dowek", + title = "Th{\'e}orie des types", + year = 2002, + howpublished = "Lecture notes", + url= "http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz" +} + +@PHDTHESIS{EGThese, + author = {Eduardo Giménez}, + title = {Un Calcul de Constructions Infinies et son application +a la vérification de systèmes communicants}, + type = {thèse d'Université}, + school = {Ecole Normale Supérieure de Lyon}, + month = {December}, + year = {1996}, +} + + +%%%%%%% Semantique %%%%%%% + +@misc{Sem:cours, + author = "François Pottier", + title = "{Typage et Programmation}", + year = "2002", + howpublished = "Lecture notes", + note = "DEA PSPL" +} + +@inproceedings{Sem:Dubois, + author = {Catherine Dubois}, + editor = {Mark Aagaard and + John Harrison}, + title = "{Proving ML Type Soundness Within Coq}", + pages = {126-144}, + booktitle = {TPHOLs}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {1869}, + year = {2000}, + isbn = {3-540-67863-8}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@techreport{Sem:Plotkin, +author = {Gordon D. Plotkin}, +institution = {Aarhus University}, +number = {{DAIMI FN-19}}, +title = {{A structural approach to operational semantics}}, +year = {1981} +} + +@article{Sem:RemyV98, + author = "Didier R{\'e}my and J{\'e}r{\^o}me Vouillon", + title = "Objective {ML}: + An effective object-oriented extension to {ML}", + journal = "Theory And Practice of Object Systems", + year = 1998, + volume = "4", + number = "1", + pages = "27--50", + note = {A preliminary version appeared in the proceedings + of the 24th ACM Conference on Principles + of Programming Languages, 1997} +} + +@book{Sem:Winskel, + AUTHOR = {Winskel, Glynn}, + TITLE = {The Formal Semantics of Programming Languages}, + NOTE = {WIN g2 93:1 P-Ex}, + YEAR = {1993}, + PUBLISHER = {The MIT Press}, + SERIES = {Foundations of Computing}, + } + +@Article{Sem:WrightFelleisen, + refkey = "C1210", + title = "A Syntactic Approach to Type Soundness", + author = "Andrew K. Wright and Matthias Felleisen", + pages = "38--94", + journal = "Information and Computation", + month = "15~" # nov, + year = "1994", + volume = "115", + number = "1" +} + +@inproceedings{Sem:Nipkow-MOD, + author={Tobias Nipkow}, + title={Jinja: Towards a Comprehensive Formal Semantics for a + {J}ava-like Language}, + booktitle={Proc.\ Marktobderdorf Summer School 2003}, + publisher={IOS Press},editor={H. Schwichtenberg and K. Spies}, + year=2003, + note={To appear} +} + +%%%%%%% Coq %%%%%%% + +@book{Coq:coqart, + title = "Interactive Theorem Proving and Program Development, + Coq'Art: The Calculus of Inductive Constructions", + author = "Yves Bertot and Pierre Castéran", + publisher = "Springer Verlag", + series = "Texts in Theoretical Computer Science. An + EATCS series", + year = 2004 +} + +@phdthesis{Coq:Del01, + AUTHOR = "David Delahaye", + TITLE = "Conception de langages pour décrire les preuves et les + automatisations dans les outils d'aide à la preuve", + SCHOOL = {Universit\'e Paris~6}, + YEAR = "2001", + Type = {Th\`ese de Doctorat} +} + +@techreport{Coq:gimenez-tut, + author = "Eduardo Gim\'enez", + title = "A Tutorial on Recursive Types in Coq", + number = "RT-0221", + pages = "42 p.", + url = "citeseer.nj.nec.com/gimenez98tutorial.html" } + +@phdthesis{Coq:Mun97, + AUTHOR = "César Mu{\~{n}}oz", + TITLE = "Un calcul de substitutions pour la repr\'esentation + de preuves partielles en th\'eorie de types", + SCHOOL = {Universit\'e Paris~7}, + Number = {Unit\'e de recherche INRIA-Rocquencourt, TU-0488}, + YEAR = "1997", + Note = {English version available as INRIA research report RR-3309}, + Type = {Th\`ese de Doctorat} +} + +@PHDTHESIS{Coq:Filliatre99, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Preuve de programmes imp\'eratifs en th\'eorie des types}}, + TYPE = {Th{\`e}se de Doctorat}, + SCHOOL = {Universit\'e Paris-Sud}, + YEAR = 1999, + MONTH = {July}, +} + +@manual{Coq:Tutorial, + AUTHOR = {G\'erard Huet and Gilles Kahn and Christine Paulin-Mohring}, + TITLE = {{The Coq Proof Assistant A Tutorial}}, + YEAR = 2004 +} + +%%%%%%% PVS %%%%%%% + +@manual{PVS:prover, + title = "{PVS} Prover Guide", + author = "N. Shankar and S. Owre and J. M. Rushby and D. W. J. + Stringer-Calvert", + month = sep, + year = "1999", + organization = "Computer Science Laboratory, SRI International", + address = "Menlo Park, CA", +} + +@techreport{PVS-Semantics:TR, + TITLE = {The Formal Semantics of {PVS}}, + AUTHOR = {Sam Owre and Natarajan Shankar}, + NUMBER = {CR-1999-209321}, + INSTITUTION = {Computer Science Laboratory, SRI International}, + ADDRESS = {Menlo Park, CA}, + MONTH = may, + YEAR = 1999, +} + +@techreport{PVS-Tactics:DiVito, + TITLE = {A {PVS} Prover Strategy Package for Common Manipulations}, + AUTHOR = {Ben L. Di Vito}, + NUMBER = {TM-2002-211647}, + INSTITUTION = {Langley Research Center}, + ADDRESS = {Hampton, VA}, + MONTH = apr, + YEAR = 2002, +} + +@misc{PVS-Tactics:cours, + author = "César Muñoz", + title = "Strategies in {PVS}", + howpublished = "Lecture notes", + note = "National Institute of Aerospace", + year = 2002 +} + +@techreport{PVS-Tactics:field, + author = "C. Mu{\~n}oz and M. Mayero", + title = "Real Automation in the Field", + institution = "ICASE-NASA Langley", + number = "NASA/CR-2001-211271 Interim ICASE Report No. 39", + month = "dec", + year = "2001" +} + +%%%%%%% Autres Prouveurs %%%%%%% + +@misc{ACL2:repNuPrl, + author = "James L. Caldwell and John Cowles", + title = "{Representing Nuprl Proof Objects in ACL2: toward a proof checker for Nuprl}", + url = "http://www.cs.uwyo.edu/~jlc/papers/proof_checking.ps" } + +@inproceedings{Elan:ckl-strat, + author = {H. Cirstea and C. Kirchner and L. Liquori}, + title = "{Rewrite Strategies in the Rewriting Calculus}", + booktitle = {WRLA'02}, + publisher = "{Elsevier Science B.V.}", + series = {Electronic Notes in Theoretical Computer Science}, + volume = {71}, + year = {2003}, +} + +@book{LCF:GMW, + author = {M. Gordon and R. Milner and C. Wadsworth}, + publisher = {sv}, + series = {lncs}, + volume = 78, + title = {Edinburgh {LCF}: A Mechanized Logic of Computation}, + year = 1979 +} + +%%%%%%% LaTeX %%%%%%% + +@manual{LaTeX:symb, + title = "The Great, Big List of \LaTeX\ Symbols", + author = "David Carlisle and Scott Pakin and Alexander Holt", + month = feb, + year = 2001, +} + +@manual{LaTeX:intro, + title = "The Not So Short Introduction to \LaTeX2e", + author = "Tobias Oetiker", + month = jan, + year = 1999, +} + +@MANUAL{CoqManualV7, + AUTHOR = {{The {Coq} Development Team}}, + TITLE = {{The Coq Proof Assistant Reference Manual -- Version + V7.1}}, + YEAR = {2001}, + MONTH = OCT, + NOTE = {http://coq.inria.fr} +} + +@MANUAL{CoqManual96, + TITLE = {The {Coq Proof Assistant Reference Manual} Version 6.1}, + AUTHOR = {B. Barras and S. Boutin and C. Cornes and J. Courant and + J.-C. Filli\^atre and + H. Herbelin and G. Huet and P. Manoury and C. Mu{\~{n}}oz and + C. Murthy and C. Parent and C. Paulin-Mohring and + A. Sa{\"\i}bi and B. Werner}, + ORGANIZATION = {{INRIA-Rocquencourt}-{CNRS-ENS Lyon}}, + URL = {ftp://ftp.inria.fr/INRIA/coq/V6.1/doc/Reference-Manual.dvi.gz}, + YEAR = 1996, + MONTH = DEC +} + +@MANUAL{CoqTutorial99, + AUTHOR = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring}, + TITLE = {The {\sf Coq} Proof Assistant - A tutorial - Version 6.3}, + MONTH = JUL, + YEAR = {1999}, + ABSTRACT = {http://coq.inria.fr/doc/tutorial.html} +} + +@MANUAL{CoqTutorialV7, + AUTHOR = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring}, + TITLE = {The {\sf Coq} Proof Assistant - A tutorial - Version 7.1}, + MONTH = OCT, + YEAR = {2001}, + NOTE = {http://coq.inria.fr} +} + +@TECHREPORT{modelpa2000, + AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg + and J.-F. Monin and C. Paulin and A. Petit and D. Rouillard}, + TITLE = {Automates temporisés CALIFE}, + INSTITUTION = {Calife}, + YEAR = 2000, + URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz}, + TYPE = {Fourniture {F1.1}} +} + +@TECHREPORT{CaFrPaRo2000, + AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard}, + TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates}, + INSTITUTION = {Calife}, + YEAR = 2000, + URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz}, + TYPE = {Fourniture {F5.4}} +} + +@PROCEEDINGS{TPHOLs99, + TITLE = {International Conference on + Theorem Proving in Higher Order Logics (TPHOLs'99)}, + YEAR = 1999, + EDITOR = {Y. Bertot and G. Dowek and C. Paulin-Mohring and L. Th{\'e}ry}, + SERIES = {Lecture Notes in Computer Science}, + MONTH = SEP, + PUBLISHER = {{Sprin\-ger-Verlag}}, + ADDRESS = {Nice}, + TYPE_PUBLI = {editeur} +} + +@INPROCEEDINGS{Pau01, + AUTHOR = {Christine Paulin-Mohring}, + TITLE = {Modelisation of Timed Automata in {Coq}}, + BOOKTITLE = {Theoretical Aspects of Computer Software (TACS'2001)}, + PAGES = {298--315}, + YEAR = 2001, + EDITOR = {N. Kobayashi and B. Pierce}, + VOLUME = 2215, + SERIES = {Lecture Notes in Computer Science}, + PUBLISHER = {Springer-Verlag} +} + +@PHDTHESIS{Moh89b, + AUTHOR = {C. Paulin-Mohring}, + MONTH = JAN, + SCHOOL = {{Paris 7}}, + TITLE = {Extraction de programmes dans le {Calcul des Constructions}}, + TYPE = {Thèse d'université}, + YEAR = {1989}, + URL = {http://www.lri.fr/~paulin/these.ps.gz} +} + +@ARTICLE{HuMo92, + AUTHOR = {G. Huet and C. Paulin-Mohring}, + EDITION = {INRIA}, + JOURNAL = {Courrier du CNRS - Informatique}, + TITLE = {Preuves et Construction de Programmes}, + YEAR = {1992}, + CATEGORY = {national} +} + +@INPROCEEDINGS{LePa94, + AUTHOR = {F. Leclerc and C. Paulin-Mohring}, + TITLE = {Programming with Streams in {Coq}. A case study : The Sieve of Eratosthenes}, + EDITOR = {H. Barendregt and T. Nipkow}, + VOLUME = 806, + SERIES = {Lecture Notes in Computer Science}, + BOOKTITLE = {{Types for Proofs and Programs, Types' 93}}, + YEAR = 1994, + PUBLISHER = {Springer-Verlag} +} + +@INPROCEEDINGS{Moh86, + AUTHOR = {C. Mohring}, + ADDRESS = {Cambridge, MA}, + BOOKTITLE = {Symposium on Logic in Computer Science}, + PUBLISHER = {IEEE Computer Society Press}, + TITLE = {Algorithm Development in the {Calculus of Constructions}}, + YEAR = {1986} +} + +@INPROCEEDINGS{Moh89a, + AUTHOR = {C. Paulin-Mohring}, + ADDRESS = {Austin}, + BOOKTITLE = {Sixteenth Annual ACM Symposium on Principles of Programming Languages}, + MONTH = JAN, + PUBLISHER = {ACM}, + TITLE = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}}, + YEAR = {1989} +} + +@INCOLLECTION{Moh89c, + AUTHOR = {C. Paulin-Mohring}, + TITLE = {{R\'ealisabilit\'e et extraction de programmes}}, + BOOKTITLE = {Logique et Informatique : une introduction}, + PUBLISHER = {INRIA}, + YEAR = 1991, + EDITOR = {B. Courcelle}, + VOLUME = 8, + SERIES = {Collection Didactique}, + PAGES = {163-180}, + CATEGORY = {national} +} + +@INPROCEEDINGS{Moh93, + AUTHOR = {C. Paulin-Mohring}, + BOOKTITLE = {Proceedings of the conference Typed Lambda Calculi a +nd Applications}, + EDITOR = {M. Bezem and J.-F. Groote}, + INSTITUTION = {LIP-ENS Lyon}, + NOTE = {LIP research report 92-49}, + NUMBER = 664, + SERIES = {Lecture Notes in Computer Science}, + TITLE = {{Inductive Definitions in the System {Coq} - Rules and Properties}}, + TYPE = {research report}, + YEAR = 1993 +} + +@ARTICLE{PaWe92, + AUTHOR = {C. Paulin-Mohring and B. Werner}, + JOURNAL = {Journal of Symbolic Computation}, + TITLE = {{Synthesis of ML programs in the system Coq}}, + VOLUME = {15}, + YEAR = {1993}, + PAGES = {607--640} +} + +@INPROCEEDINGS{Pau96, + AUTHOR = {C. Paulin-Mohring}, + TITLE = {Circuits as streams in {Coq} : Verification of a sequential multiplier}, + BOOKTITLE = {Types for Proofs and Programs, TYPES'95}, + EDITOR = {S. Berardi and M. Coppo}, + SERIES = {Lecture Notes in Computer Science}, + YEAR = 1996, + VOLUME = 1158 +} + +@PHDTHESIS{Pau96b, + AUTHOR = {Christine Paulin-Mohring}, + TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur}, + SCHOOL = {Université Claude Bernard Lyon I}, + YEAR = 1996, + MONTH = DEC, + TYPE = {Habilitation à diriger les recherches}, + URL = {http://www.lri.fr/~paulin/habilitation.ps.gz} +} + +@INPROCEEDINGS{PfPa89, + AUTHOR = {F. Pfenning and C. Paulin-Mohring}, + BOOKTITLE = {Proceedings of Mathematical Foundations of Programming Semantics}, + NOTE = {technical report CMU-CS-89-209}, + PUBLISHER = {Springer-Verlag}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 442, + TITLE = {Inductively defined types in the {Calculus of Constructions}}, + YEAR = {1990} +} + +@MISC{krakatoa02, + AUTHOR = {Claude March\'e and Christine Paulin and Xavier Urbain}, + TITLE = {The \textsc{Krakatoa} proof tool}, + YEAR = 2002, + NOTE = {\url{http://krakatoa.lri.fr/}} +} + +@ARTICLE{marche03jlap, + AUTHOR = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain}, + TITLE = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}}, + JOURNAL = {Journal of Logic and Algebraic Programming}, + YEAR = 2003, + NOTE = {To appear}, + URL = {http://krakatoa.lri.fr}, + TOPICS = {team} +} +@ARTICLE{marche04jlap, + AUTHOR = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain}, + TITLE = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}}, + JOURNAL = {Journal of Logic and Algebraic Programming}, + YEAR = 2004, + VOLUME = 58, + NUMBER = {1--2}, + PAGES = {89--106}, + URL = {http://krakatoa.lri.fr}, + TOPICS = {team} +} + +@TECHREPORT{catano03deliv, + AUTHOR = {N{\'e}stor Cata{\~n}o and Marek Gawkowski and +Marieke Huisman and Bart Jacobs and Claude March{\'e} and Christine Paulin +and Erik Poll and Nicole Rauch and Xavier Urbain}, + TITLE = {Logical Techniques for Applet Verification}, + INSTITUTION = {VerifiCard Project}, + YEAR = 2003, + TYPE = {Deliverable}, + NUMBER = {5.2}, + TOPICS = {team}, + NOTE = {Available from \url{http://www.verificard.org}} +} + +@TECHREPORT{kmu2002rr, + AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain}, + TITLE = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria}, + INSTITUTION = {LRI}, + YEAR = 2002, + TYPE = {Research Report}, + NUMBER = 1304, + TYPE_PUBLI = {interne}, + TOPICS = {team}, + NOTE = {\url{http://www.lri.fr/~urbain/textes/rr1304.ps.gz}}, + URL = {http://www.lri.fr/~urbain/textes/rr1304.ps.gz} +} + +@ARTICLE{marche2004jsc, + AUTHOR = {Claude March\'e and Xavier Urbain}, + TITLE = {Modular {\&} Incremental Proofs of {AC}-Termination}, + JOURNAL = {Journal of Symbolic Computation}, + YEAR = 2004, + TOPICS = {team} +} + +@INPROCEEDINGS{contejean03wst, + AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain}, + TITLE = {{Proving Termination of Rewriting with {\sc C\textit{i}ME}}}, + CROSSREF = {wst03}, + PAGES = {71--73}, + NOTE = {\url{http://cime.lri.fr/}}, + URL = {http://cime.lri.fr/}, + YEAR = 2003, + TYPE_PUBLI = {icolcomlec}, + TOPICS = {team} +} + +@TECHREPORT{contejean04rr, + AUTHOR = {Evelyne Contejean and Claude March{\'e} and Ana-Paula Tom{\'a}s and Xavier Urbain}, + TITLE = {Mechanically proving termination using polynomial interpretations}, + INSTITUTION = {LRI}, + YEAR = {2004}, + TYPE = {Research Report}, + NUMBER = {1382}, + TYPE_PUBLI = {interne}, + TOPICS = {team}, + URL = {http://www.lri.fr/~urbain/textes/rr1382.ps.gz} +} + +@UNPUBLISHED{duran_sub, + AUTHOR = {Francisco Duran and Salvador Lucas and + Claude {March\'e} and {Jos\'e} Meseguer and Xavier Urbain}, + TITLE = {Termination of Membership Equational Programs}, + NOTE = {Submitted} +} + +@PROCEEDINGS{comon95lncs, + TITLE = {Term Rewriting}, + BOOKTITLE = {Term Rewriting}, + TOPICS = {team, cclserver}, + YEAR = 1995, + EDITOR = {Hubert Comon and Jean-Pierre Jouannaud}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = {909}, + PUBLISHER = {{Sprin\-ger-Verlag}}, + ORGANIZATION = {French Spring School of Theoretical Computer + Science}, + TYPE_PUBLI = {editeur}, + CLEF_LABO = {CJ95} +} + +@PROCEEDINGS{lics94, + TITLE = {Proceedings of the Ninth Annual IEEE Symposium on Logic + in Computer Science}, + BOOKTITLE = {Proceedings of the Ninth Annual IEEE Symposium on Logic + in Computer Science}, + YEAR = 1994, + MONTH = JUL, + ADDRESS = {Paris, France}, + ORGANIZATION = {{IEEE} Comp. Soc. Press} +} + +@PROCEEDINGS{rta91, + TITLE = {4th International Conference on Rewriting Techniques and + Applications}, + BOOKTITLE = {4th International Conference on Rewriting Techniques and + Applications}, + EDITOR = {Ronald. V. Book}, + YEAR = 1991, + MONTH = APR, + ADDRESS = {Como, Italy}, + PUBLISHER = {{Sprin\-ger-Verlag}}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 488 +} + +@PROCEEDINGS{rta96, + TITLE = {7th International Conference on Rewriting Techniques and + Applications}, + BOOKTITLE = {7th International Conference on Rewriting Techniques and + Applications}, + EDITOR = {Harald Ganzinger}, + PUBLISHER = {{Sprin\-ger-Verlag}}, + YEAR = 1996, + MONTH = JUL, + ADDRESS = {New Brunswick, NJ, USA}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 1103 +} + +@PROCEEDINGS{rta97, + TITLE = {8th International Conference on Rewriting Techniques and + Applications}, + BOOKTITLE = {8th International Conference on Rewriting Techniques and + Applications}, + EDITOR = {Hubert Comon}, + PUBLISHER = {{Sprin\-ger-Verlag}}, + YEAR = 1997, + MONTH = JUN, + ADDRESS = {Barcelona, Spain}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = {1232} +} + +@PROCEEDINGS{rta98, + TITLE = {9th International Conference on Rewriting Techniques and + Applications}, + BOOKTITLE = {9th International Conference on Rewriting Techniques and + Applications}, + EDITOR = {Tobias Nipkow}, + PUBLISHER = {{Sprin\-ger-Verlag}}, + YEAR = 1998, + MONTH = APR, + ADDRESS = {Tsukuba, Japan}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = {1379} +} + +@PROCEEDINGS{rta00, + TITLE = {11th International Conference on Rewriting Techniques and Applications}, + BOOKTITLE = {11th International Conference on Rewriting Techniques and Applications}, + EDITOR = {Leo Bachmair}, + PUBLISHER = {{Sprin\-ger-Verlag}}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 1833, + MONTH = JUL, + YEAR = 2000, + ADDRESS = {Norwich, UK} +} + +@PROCEEDINGS{srt95, + TITLE = {Proceedings of the Conference on Symbolic Rewriting + Techniques}, + BOOKTITLE = {Proceedings of the Conference on Symbolic Rewriting + Techniques}, + YEAR = 1995, + EDITOR = {Manuel Bronstein and Volker Weispfenning}, + ADDRESS = {Monte Verita, Switzerland} +} + +@BOOK{comon01cclbook, + BOOKTITLE = {Constraints in Computational Logics}, + TITLE = {Constraints in Computational Logics}, + EDITOR = {Hubert Comon and Claude March{\'e} and Ralf Treinen}, + YEAR = 2001, + PUBLISHER = {{Sprin\-ger-Verlag}}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 2002, + TOPICS = {team}, + TYPE_PUBLI = {editeur} +} + +@PROCEEDINGS{wst03, + BOOKTITLE = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}}, + TITLE = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}}, + YEAR = {2003}, + EDITOR = {Albert Rubio}, + MONTH = JUN, + NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain} +} + +@INPROCEEDINGS{FilliatreLetouzey03, + AUTHOR = {J.-C. Filli\^atre and P. Letouzey}, + TITLE = {{Functors for Proofs and Programs}}, + BOOKTITLE = {Proceedings of The European Symposium on Programming}, + YEAR = 2004, + ADDRESS = {Barcelona, Spain}, + MONTH = {March 29-April 2}, + NOTE = {To appear}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz} +} + +@TECHREPORT{Filliatre03, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Why: a multi-language multi-prover verification tool}}, + INSTITUTION = {{LRI, Universit\'e Paris Sud}}, + TYPE = {{Research Report}}, + NUMBER = {1366}, + MONTH = {March}, + YEAR = 2003, + URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz} +} + +@ARTICLE{FilliatrePottier02, + AUTHOR = {J.-C. Filli{\^a}tre and F. Pottier}, + TITLE = {{Producing All Ideals of a Forest, Functionally}}, + JOURNAL = {Journal of Functional Programming}, + VOLUME = 13, + NUMBER = 5, + PAGES = {945--956}, + MONTH = {September}, + YEAR = 2003, + URL = {http://www.lri.fr/~filliatr/ftp/publis/kr-fp.ps.gz}, + ABSTRACT = { + We present a functional implementation of Koda and Ruskey's + algorithm for generating all ideals of a forest poset as a Gray + code. Using a continuation-based approach, we give an extremely + concise formulation of the algorithm's core. Then, in a number of + steps, we derive a first-order version whose efficiency is + comparable to a C implementation given by Knuth.} +} + +@UNPUBLISHED{FORS01, + AUTHOR = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar}, + TITLE = {Deciding Propositional Combinations of Equalities and Inequalities}, + NOTE = {Unpublished}, + MONTH = OCT, + YEAR = 2001, + URL = {http://www.lri.fr/~filliatr/ftp/publis/ics.ps}, + ABSTRACT = { + We address the problem of combining individual decision procedures + into a single decision procedure. Our combination approach is based + on using the canonizer obtained from Shostak's combination algorithm + for equality. We illustrate our approach with a combination + algorithm for equality, disequality, arithmetic inequality, and + propositional logic. Unlike the Nelson--Oppen combination where the + processing of equalities is distributed across different closed + decision procedures, our combination involves the centralized + processing of equalities in a single procedure. The termination + argument for the combination is based on that for Shostak's + algorithm. We also give soundness and completeness arguments.} +} + +@INPROCEEDINGS{ICS, + AUTHOR = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar}, + TITLE = {{ICS: Integrated Canonization and Solving (Tool presentation)}}, + BOOKTITLE = {Proceedings of CAV'2001}, + EDITOR = {G. Berry and H. Comon and A. Finkel}, + PUBLISHER = {Springer-Verlag}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 2102, + PAGES = {246--249}, + YEAR = 2001 +} + +@INPROCEEDINGS{Filliatre01a, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {La supériorité de l'ordre supérieur}, + BOOKTITLE = {Journées Francophones des Langages Applicatifs}, + PAGES = {15--26}, + MONTH = {Janvier}, + YEAR = 2002, + ADDRESS = {Anglet, France}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz}, + CODE = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps}, + ABSTRACT = { + Nous présentons ici une écriture fonctionnelle de l'algorithme de + Koda-Ruskey, un algorithme pour engendrer une large famille + de codes de Gray. En s'inspirant de techniques de programmation par + continuation, nous aboutissons à un code de neuf lignes seulement, + bien plus élégant que les implantations purement impératives + proposées jusqu'ici, notamment par Knuth. Dans un second temps, + nous montrons comment notre code peut être légèrement modifié pour + aboutir à une version de complexité optimale. + Notre implantation en Objective Caml rivalise d'efficacité avec les + meilleurs codes C. Nous détaillons les calculs de complexité, + un exercice intéressant en présence d'ordre supérieur et d'effets de + bord combinés.} +} + +@TECHREPORT{Filliatre00c, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Design of a proof assistant: Coq version 7}}, + INSTITUTION = {{LRI, Universit\'e Paris Sud}}, + TYPE = {{Research Report}}, + NUMBER = {1369}, + MONTH = {October}, + YEAR = 2000, + URL = {http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz}, + ABSTRACT = { + We present the design and implementation of the new version of the + Coq proof assistant. The main novelty is the isolation of the + critical part of the system, which consists in a type checker for + the Calculus of Inductive Constructions. This kernel is now + completely independent of the rest of the system and has been + rewritten in a purely functional way. This leads to greater clarity + and safety, without compromising efficiency. It also opens the way to + the ``bootstrap'' of the Coq system, where the kernel will be + certified using Coq itself.} +} + +@TECHREPORT{Filliatre00b, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Hash consing in an ML framework}}, + INSTITUTION = {{LRI, Universit\'e Paris Sud}}, + TYPE = {{Research Report}}, + NUMBER = {1368}, + MONTH = {September}, + YEAR = 2000, + URL = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing.ps.gz}, + ABSTRACT = { + Hash consing is a technique to share values that are structurally + equal. Beyond the obvious advantage of saving memory blocks, hash + consing may also be used to gain speed in several operations (like + equality test) and data structures (like sets or maps) when sharing is + maximal. However, physical adresses cannot be used directly for this + purpose when the garbage collector is likely to move blocks + underneath. We present an easy solution in such a framework, with + many practical benefits.} +} + +@MISC{ocamlweb, + AUTHOR = {J.-C. Filli\^atre and C. March\'e}, + TITLE = {{ocamlweb, a literate programming tool for Objective Caml}}, + NOTE = {Available at \url{http://www.lri.fr/~filliatr/ocamlweb/}}, + URL = {http://www.lri.fr/~filliatr/ocamlweb/} +} + +@ARTICLE{Filliatre00a, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Verification of Non-Functional Programs + using Interpretations in Type Theory}}, + JOURNAL = {Journal of Functional Programming}, + VOLUME = 13, + NUMBER = 4, + PAGES = {709--745}, + MONTH = {July}, + YEAR = 2003, + NOTE = {English translation of~\cite{Filliatre99}.}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, + ABSTRACT = {We study the problem of certifying programs combining imperative and + functional features within the general framework of type theory. + + Type theory constitutes a powerful specification language, which is + naturally suited for the proof of purely functional programs. To + deal with imperative programs, we propose a logical interpretation + of an annotated program as a partial proof of its specification. The + construction of the corresponding partial proof term is based on a + static analysis of the effects of the program, and on the use of + monads. The usual notion of monads is refined in order to account + for the notion of effect. The missing subterms in the partial proof + term are seen as proof obligations, whose actual proofs are left to + the user. We show that the validity of those proof obligations + implies the total correctness of the program. + We also establish a result of partial completeness. + + This work has been implemented in the Coq proof assistant. + It appears as a tactic taking an annotated program as argument and + generating a set of proof obligations. Several nontrivial + algorithms have been certified using this tactic.} +} + +@ARTICLE{Filliatre99c, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Formal Proof of a Program: Find}}, + JOURNAL = {Science of Computer Programming}, + YEAR = 2001, + NOTE = {To appear}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}, + ABSTRACT = {In 1971, C.~A.~R.~Hoare gave the proof of correctness and termination of a + rather complex algorithm, in a paper entitled \emph{Proof of a + program: Find}. It is a hand-made proof, where the + program is given together with its formal specification and where + each step is fully + justified by a mathematical reasoning. We present here a formal + proof of the same program in the system Coq, using the + recent tactic of the system developed to establishing the total + correctness of + imperative programs. We follow Hoare's paper as close as + possible, keeping the same program and the same specification. We + show that we get exactly the same proof obligations, which are + proved in a straightforward way, following the original paper. + We also explain how more informal reasonings of Hoare's proof are + formalized in the system Coq. + This demonstrates the adequacy of the system Coq in the + process of certifying imperative programs.} +} + +@TECHREPORT{Filliatre99b, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{A theory of monads parameterized by effects}}, + INSTITUTION = {{LRI, Universit\'e Paris Sud}}, + TYPE = {{Research Report}}, + NUMBER = {1367}, + MONTH = {November}, + YEAR = 1999, + URL = {http://www.lri.fr/~filliatr/ftp/publis/monads.ps.gz}, + ABSTRACT = {Monads were introduced in computer science to express the semantics + of programs with computational effects, while type and effect + inference was introduced to mark out those effects. + In this article, we propose a combination of the notions of effects + and monads, where the monadic operators are parameterized by effects. + We establish some relationships between those generalized monads and + the classical ones. + Then we use a generalized monad to translate imperative programs + into purely functional ones. We establish the correctness of that + translation. This work has been put into practice in the Coq proof + assistant to establish the correctness of imperative programs.} +} + +@PHDTHESIS{Filliatre99, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Preuve de programmes imp\'eratifs en th\'eorie des types}}, + TYPE = {Th{\`e}se de Doctorat}, + SCHOOL = {Universit\'e Paris-Sud}, + YEAR = 1999, + MONTH = {July}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}, + ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant + traits impératifs et fonctionnels dans le cadre de la théorie des + types. + + La théorie des types constitue un puissant langage de spécification, + naturellement adapté à la preuve de programmes purement + fonctionnels. Pour y certifier également des programmes impératifs, + nous commençons par exprimer leur sémantique de manière purement + fonctionnelle. Cette traduction repose sur une analyse statique des + effets de bord des programmes, et sur l'utilisation de la notion de + monade, notion que nous raffinons en l'associant à la notion d'effet + de manière générale. Nous montrons que cette traduction est + sémantiquement correcte. + + Puis, à partir d'un programme annoté, nous construisons une preuve + de sa spécification, traduite de manière fonctionnelle. Cette preuve + est bâtie sur la traduction fonctionnelle précédemment + introduite. Elle est presque toujours incomplète, les parties + manquantes étant autant d'obligations de preuve qui seront laissées + à la charge de l'utilisateur. Nous montrons que la validité de ces + obligations entraîne la correction totale du programme. + + Nous avons implanté notre travail dans l'assistant de preuve + Coq, avec lequel il est dès à présent distribué. Cette + implantation se présente sous la forme d'une tactique prenant en + argument un programme annoté et engendrant les obligations de + preuve. Plusieurs algorithmes non triviaux ont été certifiés à + l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de + Knuth-Morris-Pratt).} +} + +@INPROCEEDINGS{FilliatreMagaud99, + AUTHOR = {J.-C. Filli\^atre and N. Magaud}, + TITLE = {{Certification of sorting algorithms in the system Coq}}, + BOOKTITLE = {Theorem Proving in Higher Order Logics: + Emerging Trends}, + YEAR = 1999, + ABSTRACT = {We present the formal proofs of total correctness of three sorting + algorithms in the system Coq, namely \textit{insertion sort}, + \textit{quicksort} and \textit{heapsort}. The implementations are + imperative programs working in-place on a given array. Those + developments demonstrate the usefulness of inductive types and higher-order + logic in the process of software certification. They also + show that the proof of rather complex algorithms may be done in a + small amount of time --- only a few days for each development --- + and without great difficulty.}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz} +} + +@INPROCEEDINGS{Filliatre98, + AUTHOR = {J.-C. Filli\^atre}, + TITLE = {{Proof of Imperative Programs in Type Theory}}, + BOOKTITLE = {International Workshop, TYPES '98, Kloster Irsee, Germany}, + PUBLISHER = {Springer-Verlag}, + VOLUME = 1657, + SERIES = {Lecture Notes in Computer Science}, + MONTH = MAR, + YEAR = {1998}, + ABSTRACT = {We present a new approach to certifying imperative programs, + in the context of Type Theory. + The key is a functional translation of imperative programs, which is + made possible by an analysis of their effects. + On sequential imperative programs, we get the same proof + obligations as those given by Floyd-Hoare logic, + but our approach also includes functional constructions. + As a side-effect, we propose a way to eradicate the use of auxiliary + variables in specifications. + This work has been implemented in the Coq Proof Assistant and applied + on non-trivial examples.}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/types98.ps.gz} +} + +@TECHREPORT{Filliatre97, + AUTHOR = {J.-C. Filli\^atre}, + INSTITUTION = {LIP - ENS Lyon}, + NUMBER = {97--04}, + TITLE = {{Finite Automata Theory in Coq: + A constructive proof of Kleene's theorem}}, + TYPE = {Research Report}, + MONTH = {February}, + YEAR = {1997}, + ABSTRACT = {We describe here a development in the system Coq + of a piece of Finite Automata Theory. The main result is the Kleene's + theorem, expressing that regular expressions and finite automata + define the same languages. From a constructive proof of this result, + we automatically obtain a functional program that compiles any + regular expression into a finite automata, which constitutes the main + part of the implementation of {\tt grep}-like programs. This + functional program is obtained by the automatic method of {\em + extraction} which removes the logical parts of the proof to keep only + its informative contents. Starting with an idea of what we would + have written in ML, we write the specification and do the proofs in + such a way that we obtain the expected program, which is therefore + efficient.}, + URL = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR97/RR97-04.ps.Z} +} + +@TECHREPORT{Filliatre95, + AUTHOR = {J.-C. Filli\^atre}, + INSTITUTION = {LIP - ENS Lyon}, + NUMBER = {96--25}, + TITLE = {{A decision procedure for Direct Predicate + Calculus: study and implementation in + the Coq system}}, + TYPE = {Research Report}, + MONTH = {February}, + YEAR = {1995}, + ABSTRACT = {The paper of J. Ketonen and R. Weyhrauch \emph{A + decidable fragment of Predicate Calculus} defines a decidable + fragment of first-order predicate logic - Direct Predicate Calculus + - as the subset which is provable in Gentzen sequent calculus + without the contraction rule, and gives an effective decision + procedure for it. This report is a detailed study of this + procedure. We extend the decidability to non-prenex formulas. We + prove that the intuitionnistic fragment is still decidable, with a + refinement of the same procedure. An intuitionnistic version has + been implemented in the Coq system using a translation into + natural deduction.}, + URL = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-25.ps.Z} +} + +@TECHREPORT{Filliatre94, + AUTHOR = {J.-C. Filli\^atre}, + MONTH = {Juillet}, + INSTITUTION = {Ecole Normale Sup\'erieure}, + TITLE = {{Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct~: \'etude et impl\'ementation dans le syst\`eme Coq}}, + TYPE = {Rapport de {DEA}}, + YEAR = {1994}, + URL = {ftp://ftp.lri.fr/LRI/articles/filliatr/memoire.dvi.gz} +} + +@TECHREPORT{CourantFilliatre93, + AUTHOR = {J. Courant et J.-C. Filli\^atre}, + MONTH = {Septembre}, + INSTITUTION = {Ecole Normale Sup\'erieure}, + TITLE = {{Formalisation de la th\'eorie des langages + formels en Coq}}, + TYPE = {Rapport de ma\^{\i}trise}, + YEAR = {1993}, + URL = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.dvi.gz}, + URL2 = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.ps.gz} +} + +@INPROCEEDINGS{tphols2000-Letouzey, + crossref = "tphols2000", + title = "Formalizing {S}t{\aa}lmarck's algorithm in {C}oq", + author = "Pierre Letouzey and Laurent Th{\'e}ry", + pages = "387--404"} + +@PROCEEDINGS{tphols2000, + editor = "J. Harrison and M. Aagaard", + booktitle = "Theorem Proving in Higher Order Logics: + 13th International Conference, TPHOLs 2000", + series = "Lecture Notes in Computer Science", + volume = 1869, + year = 2000, + publisher = "Springer-Verlag"} + +@InCollection{howe, + author = {Doug Howe}, + title = {Computation Meta theory in Nuprl}, + booktitle = {The Proceedings of the Ninth International Conference of Autom +ated Deduction}, + volume = {310}, + editor = {E. Lusk and R. Overbeek}, + publisher = {Springer-Verlag}, + pages = {238--257}, + year = {1988} +} + +@TechReport{harrison, + author = {John Harrison}, + title = {Meta theory and Reflection in Theorem Proving:a Survey and Cri +tique}, + institution = {SRI International Cambridge Computer Science Research Center}, + year = {1995}, + number = {CRC-053} +} + +@InCollection{cc, + author = {Thierry Coquand and Gérard Huet}, + title = {The Calculus of Constructions}, + booktitle = {Information and Computation}, + year = {1988}, + volume = {76}, + number = {2/3} +} + + +@InProceedings{coquandcci, + author = {Thierry Coquand and Christine Paulin-Mohring}, + title = {Inductively defined types}, + booktitle = {Proceedings of Colog'88}, + year = {1990}, + editor = {P. Martin-Löf and G. Mints}, + volume = {417}, + series = {LNCS}, + publisher = {Springer-Verlag} +} + + +@InProceedings{boutin, + author = {Samuel Boutin}, + title = {Using reflection to build efficient and certified decision pro +cedures.}, + booktitle = {Proceedings of TACS'97}, + year = {1997}, + editor = {M. Abadi and T. Ito}, + volume = {1281}, + series = {LNCS}, + publisher = {Springer-Verlag} +} + +@Manual{Coq:manual, + title = {The Coq proof assistant reference manual}, + author = {\mbox{The Coq development team}}, + organization = {LogiCal Project}, + note = {Version 8.0}, + year = {2004}, + url = "http://coq.inria.fr" +} + +@string{jfp = "Journal of Functional Programming"} +@STRING{lncs="Lecture Notes in Computer Science"} +@STRING{lnai="Lecture Notes in Artificial Intelligence"} +@string{SV = "{Sprin\-ger-Verlag}"} + +@INPROCEEDINGS{Aud91, + AUTHOR = {Ph. Audebaud}, + BOOKTITLE = {Proceedings of the sixth Conf. on Logic in Computer Science.}, + PUBLISHER = {IEEE}, + TITLE = {Partial {Objects} in the {Calculus of Constructions}}, + YEAR = {1991} +} + +@PHDTHESIS{Aud92, + AUTHOR = {Ph. Audebaud}, + SCHOOL = {{Universit\'e} Bordeaux I}, + TITLE = {Extension du Calcul des Constructions par Points fixes}, + YEAR = {1992} +} + +@INPROCEEDINGS{Audebaud92b, + AUTHOR = {Ph. Audebaud}, + BOOKTITLE = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}}, + EDITOR = {{B. Nordstr\"om and K. Petersson and G. Plotkin}}, + NOTE = {Also Research Report LIP-ENS-Lyon}, + PAGES = {pp 21--34}, + TITLE = {{CC+ : an extension of the Calculus of Constructions with fixpoints}}, + YEAR = {1992} +} + +@INPROCEEDINGS{Augustsson85, + AUTHOR = {L. Augustsson}, + TITLE = {{Compiling Pattern Matching}}, + BOOKTITLE = {Conference Functional Programming and +Computer Architecture}, + YEAR = {1985} +} + +@ARTICLE{BaCo85, + AUTHOR = {J.L. Bates and R.L. Constable}, + JOURNAL = {ACM transactions on Programming Languages and Systems}, + TITLE = {Proofs as {Programs}}, + VOLUME = {7}, + YEAR = {1985} +} + +@BOOK{Bar81, + AUTHOR = {H.P. Barendregt}, + PUBLISHER = {North-Holland}, + TITLE = {The Lambda Calculus its Syntax and Semantics}, + YEAR = {1981} +} + +@TECHREPORT{Bar91, + AUTHOR = {H. Barendregt}, + INSTITUTION = {Catholic University Nijmegen}, + NOTE = {In Handbook of Logic in Computer Science, Vol II}, + NUMBER = {91-19}, + TITLE = {Lambda {Calculi with Types}}, + YEAR = {1991} +} + +@ARTICLE{BeKe92, + AUTHOR = {G. Bellin and J. Ketonen}, + JOURNAL = {Theoretical Computer Science}, + PAGES = {115--142}, + TITLE = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation}, + VOLUME = {95}, + YEAR = {1992} +} + +@BOOK{Bee85, + AUTHOR = {M.J. Beeson}, + PUBLISHER = SV, + TITLE = {Foundations of Constructive Mathematics, Metamathematical Studies}, + YEAR = {1985} +} + +@BOOK{Bis67, + AUTHOR = {E. Bishop}, + PUBLISHER = {McGraw-Hill}, + TITLE = {Foundations of Constructive Analysis}, + YEAR = {1967} +} + +@BOOK{BoMo79, + AUTHOR = {R.S. Boyer and J.S. Moore}, + KEY = {BoMo79}, + PUBLISHER = {Academic Press}, + SERIES = {ACM Monograph}, + TITLE = {A computational logic}, + YEAR = {1979} +} + +@MASTERSTHESIS{Bou92, + AUTHOR = {S. Boutin}, + MONTH = sep, + SCHOOL = {{Universit\'e Paris 7}}, + TITLE = {Certification d'un compilateur {ML en Coq}}, + YEAR = {1992} +} + +@inproceedings{Bou97, + title = {Using reflection to build efficient and certified decision procedure +s}, + author = {S. Boutin}, + booktitle = {TACS'97}, + editor = {Martin Abadi and Takahashi Ito}, + publisher = SV, + series = lncs, + volume=1281, + PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, + year = {1997} +} + +@PhdThesis{Bou97These, + author = {S. Boutin}, + title = {R\'eflexions sur les quotients}, + school = {Paris 7}, + year = 1997, + type = {th\`ese d'Universit\'e}, + month = apr +} + +@ARTICLE{Bru72, + AUTHOR = {N.J. de Bruijn}, + JOURNAL = {Indag. Math.}, + TITLE = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}}, + VOLUME = {34}, + YEAR = {1972} +} + + +@INCOLLECTION{Bru80, + AUTHOR = {N.J. de Bruijn}, + BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, + EDITOR = {J.P. Seldin and J.R. Hindley}, + PUBLISHER = {Academic Press}, + TITLE = {A survey of the project {Automath}}, + YEAR = {1980} +} + +@TECHREPORT{COQ93, + AUTHOR = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner}, + INSTITUTION = {INRIA}, + MONTH = may, + NUMBER = {154}, + TITLE = {{The Coq Proof Assistant User's Guide Version 5.8}}, + YEAR = {1993} +} + +@TECHREPORT{CPar93, + AUTHOR = {C. Parent}, + INSTITUTION = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, + MONTH = oct, + NOTE = {Also in~\cite{Nijmegen93}}, + NUMBER = {93-29}, + TITLE = {Developing certified programs in the system {Coq}- {The} {Program} tactic}, + YEAR = {1993} +} + +@PHDTHESIS{CPar95, + AUTHOR = {C. Parent}, + SCHOOL = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, + TITLE = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, + YEAR = {1995} +} + +@BOOK{Caml, + AUTHOR = {P. Weis and X. Leroy}, + PUBLISHER = {InterEditions}, + TITLE = {Le langage Caml}, + YEAR = {1993} +} + +@INPROCEEDINGS{ChiPotSimp03, + AUTHOR = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, + ADDRESS = {Berg en Dal, The Netherlands}, + TITLE = {Mathematical Quotients and Quotient Types in Coq}, + BOOKTITLE = {TYPES'02}, + PUBLISHER = SV, + SERIES = LNCS, + VOLUME = {2646}, + YEAR = {2003} +} + +@TECHREPORT{CoC89, + AUTHOR = {Projet Formel}, + INSTITUTION = {INRIA}, + NUMBER = {110}, + TITLE = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}}, + YEAR = {1989} +} + +@INPROCEEDINGS{CoHu85a, + AUTHOR = {Thierry Coquand and Gérard Huet}, + ADDRESS = {Linz}, + BOOKTITLE = {EUROCAL'85}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, + VOLUME = {203}, + YEAR = {1985} +} + +@INPROCEEDINGS{CoHu85b, + AUTHOR = {Thierry Coquand and Gérard Huet}, + BOOKTITLE = {Logic Colloquium'85}, + EDITOR = {The Paris Logic Group}, + PUBLISHER = {North-Holland}, + TITLE = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}}, + YEAR = {1987} +} + +@ARTICLE{CoHu86, + AUTHOR = {Thierry Coquand and Gérard Huet}, + JOURNAL = {Information and Computation}, + NUMBER = {2/3}, + TITLE = {The {Calculus of Constructions}}, + VOLUME = {76}, + YEAR = {1988} +} + +@INPROCEEDINGS{CoPa89, + AUTHOR = {Thierry Coquand and Christine Paulin-Mohring}, + BOOKTITLE = {Proceedings of Colog'88}, + EDITOR = {P. Martin-L\"of and G. Mints}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {Inductively defined types}, + VOLUME = {417}, + YEAR = {1990} +} + +@BOOK{Con86, + AUTHOR = {R.L. {Constable et al.}}, + PUBLISHER = {Prentice-Hall}, + TITLE = {{Implementing Mathematics with the Nuprl Proof Development System}}, + YEAR = {1986} +} + +@PHDTHESIS{Coq85, + AUTHOR = {Thierry Coquand}, + MONTH = jan, + SCHOOL = {Universit\'e Paris~7}, + TITLE = {Une Th\'eorie des Constructions}, + YEAR = {1985} +} + +@INPROCEEDINGS{Coq86, + AUTHOR = {Thierry Coquand}, + ADDRESS = {Cambridge, MA}, + BOOKTITLE = {Symposium on Logic in Computer Science}, + PUBLISHER = {IEEE Computer Society Press}, + TITLE = {{An Analysis of Girard's Paradox}}, + YEAR = {1986} +} + +@INPROCEEDINGS{Coq90, + AUTHOR = {Thierry Coquand}, + BOOKTITLE = {Logic and Computer Science}, + EDITOR = {P. Oddifredi}, + NOTE = {INRIA Research Report 1088, also in~\cite{CoC89}}, + PUBLISHER = {Academic Press}, + TITLE = {{Metamathematical Investigations of a Calculus of Constructions}}, + YEAR = {1990} +} + +@INPROCEEDINGS{Coq91, + AUTHOR = {Thierry Coquand}, + BOOKTITLE = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science}, + TITLE = {{A New Paradox in Type Theory}}, + MONTH = {August}, + YEAR = {1991} +} + +@INPROCEEDINGS{Coq92, + AUTHOR = {Thierry Coquand}, + TITLE = {{Pattern Matching with Dependent Types}}, + YEAR = {1992}, + crossref = {Bastad92} +} + +@INPROCEEDINGS{Coquand93, + AUTHOR = {Thierry Coquand}, + TITLE = {{Infinite Objects in Type Theory}}, + YEAR = {1993}, + crossref = {Nijmegen93} +} + +@MASTERSTHESIS{Cou94a, + AUTHOR = {J. Courant}, + MONTH = sep, + SCHOOL = {DEA d'Informatique, ENS Lyon}, + TITLE = {Explicitation de preuves par r\'ecurrence implicite}, + YEAR = {1994} +} + +@INPROCEEDINGS{Del99, + author = "Delahaye, D.", + title = "Information Retrieval in a Coq Proof Library using + Type Isomorphisms", + booktitle = {Proceedings of TYPES'99, L\"okeberg}, + publisher = SV, + series = lncs, + year = "1999", + url = + "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# + "{\sf TYPES99-SIsos.ps.gz}" +} + +@INPROCEEDINGS{Del00, + author = "Delahaye, D.", + title = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}", + booktitle = "Proceedings of Logic for Programming and Automated Reasoning + (LPAR), Reunion Island", + publisher = SV, + series = LNCS, + volume = "1955", + pages = "85--95", + month = "November", + year = "2000", + url = + "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# + "{\sf LPAR2000-ltac.ps.gz}" +} + +@INPROCEEDINGS{DelMay01, + author = "Delahaye, D. and Mayero, M.", + title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels + en {\Coq}}, + booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier", + publisher = "INRIA", + month = "Janvier", + year = "2001", + url = + "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# + "{\sf JFLA2000-Field.ps.gz}" +} + +@TECHREPORT{Dow90, + AUTHOR = {G. Dowek}, + INSTITUTION = {INRIA}, + NUMBER = {1283}, + TITLE = {Naming and Scoping in a Mathematical Vernacular}, + TYPE = {Research Report}, + YEAR = {1990} +} + +@ARTICLE{Dow91a, + AUTHOR = {G. Dowek}, + JOURNAL = {Compte-Rendus de l'Acad\'emie des Sciences}, + NOTE = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, + NUMBER = {12}, + PAGES = {951--956}, + TITLE = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, + VOLUME = {I, 312}, + YEAR = {1991} +} + +@INPROCEEDINGS{Dow91b, + AUTHOR = {G. Dowek}, + BOOKTITLE = {Proceedings of Mathematical Foundation of Computer Science}, + NOTE = {Also INRIA Research Report}, + PAGES = {151--160}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, + VOLUME = {520}, + YEAR = {1991} +} + +@PHDTHESIS{Dow91c, + AUTHOR = {G. Dowek}, + MONTH = dec, + SCHOOL = {Universit\'e Paris 7}, + TITLE = {D\'emonstration automatique dans le Calcul des Constructions}, + YEAR = {1991} +} + +@article{Dow92a, + AUTHOR = {G. Dowek}, + TITLE = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, + YEAR = 1993, + journal = tcs, + volume = 107, + number = 2, + pages = {349-356} +} + + +@ARTICLE{Dow94a, + AUTHOR = {G. Dowek}, + JOURNAL = {Annals of Pure and Applied Logic}, + VOLUME = {69}, + PAGES = {135--155}, + TITLE = {Third order matching is decidable}, + YEAR = {1994} +} + +@INPROCEEDINGS{Dow94b, + AUTHOR = {G. Dowek}, + BOOKTITLE = {Proceedings of the second international conference on typed lambda calculus and applications}, + TITLE = {Lambda-calculus, Combinators and the Comprehension Schema}, + YEAR = {1995} +} + +@INPROCEEDINGS{Dyb91, + AUTHOR = {P. Dybjer}, + BOOKTITLE = {Logical Frameworks}, + EDITOR = {G. Huet and G. Plotkin}, + PAGES = {59--79}, + PUBLISHER = {Cambridge University Press}, + TITLE = {Inductive sets and families in {Martin-L{\"o}f's} + Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, + VOLUME = {14}, + YEAR = {1991} +} + +@ARTICLE{Dyc92, + AUTHOR = {Roy Dyckhoff}, + JOURNAL = {The Journal of Symbolic Logic}, + MONTH = sep, + NUMBER = {3}, + TITLE = {Contraction-free sequent calculi for intuitionistic logic}, + VOLUME = {57}, + YEAR = {1992} +} + +@MASTERSTHESIS{Fil94, + AUTHOR = {J.-C. Filli\^atre}, + MONTH = sep, + SCHOOL = {DEA d'Informatique, ENS Lyon}, + TITLE = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}}, + YEAR = {1994} +} + +@TECHREPORT{Filliatre95, + AUTHOR = {J.-C. Filli\^atre}, + INSTITUTION = {LIP-ENS-Lyon}, + TITLE = {A decision procedure for Direct Predicate Calculus}, + TYPE = {Research report}, + NUMBER = {96--25}, + YEAR = {1995} +} + +@Article{Filliatre03jfp, + author = {J.-C. Filli{\^a}tre}, + title = {Verification of Non-Functional Programs + using Interpretations in Type Theory}, + journal = jfp, + volume = 13, + number = 4, + pages = {709--745}, + month = jul, + year = 2003, + note = {[English translation of \cite{Filliatre99}]}, + url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, + topics = "team, lri", + type_publi = "irevcomlec" +} + + +@PhdThesis{Filliatre99, + author = {J.-C. Filli\^atre}, + title = {Preuve de programmes imp\'eratifs en th\'eorie des types}, + type = {Th{\`e}se de Doctorat}, + school = {Universit\'e Paris-Sud}, + year = 1999, + month = {July}, + url = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}} +} + +@Unpublished{Filliatre99c, + author = {J.-C. Filli\^atre}, + title = {{Formal Proof of a Program: Find}}, + month = {January}, + year = 2000, + note = {Submitted to \emph{Science of Computer Programming}}, + url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}} +} + +@InProceedings{FilliatreMagaud99, + author = {J.-C. Filli\^atre and N. Magaud}, + title = {Certification of sorting algorithms in the system {\Coq}}, + booktitle = {Theorem Proving in Higher Order Logics: + Emerging Trends}, + year = 1999, + url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}} +} + +@UNPUBLISHED{Fle90, + AUTHOR = {E. Fleury}, + MONTH = jul, + NOTE = {Rapport de Stage}, + TITLE = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}}, + YEAR = {1990} +} + +@BOOK{Fourier, + AUTHOR = {Jean-Baptiste-Joseph Fourier}, + PUBLISHER = {Gauthier-Villars}, + TITLE = {Fourier's method to solve linear + inequations/equations systems.}, + YEAR = {1890} +} + +@INPROCEEDINGS{Gim94, + AUTHOR = {Eduardo Gim\'enez}, + BOOKTITLE = {Types'94 : Types for Proofs and Programs}, + NOTE = {Extended version in LIP research report 95-07, ENS Lyon}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {Codifying guarded definitions with recursive schemes}, + VOLUME = {996}, + YEAR = {1994} +} + +@TechReport{Gim98, + author = {E. Gim\'enez}, + title = {A Tutorial on Recursive Types in Coq}, + institution = {INRIA}, + year = 1998, + month = mar +} + +@INPROCEEDINGS{Gimenez95b, + AUTHOR = {E. Gim\'enez}, + BOOKTITLE = {Workshop on Types for Proofs and Programs}, + SERIES = LNCS, + NUMBER = {1158}, + PAGES = {135-152}, + TITLE = {An application of co-Inductive types in Coq: + verification of the Alternating Bit Protocol}, + EDITORS = {S. Berardi and M. Coppo}, + PUBLISHER = SV, + YEAR = {1995} +} + +@INPROCEEDINGS{Gir70, + AUTHOR = {Jean-Yves Girard}, + BOOKTITLE = {Proceedings of the 2nd Scandinavian Logic Symposium}, + PUBLISHER = {North-Holland}, + TITLE = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types}, + YEAR = {1970} +} + +@PHDTHESIS{Gir72, + AUTHOR = {Jean-Yves Girard}, + SCHOOL = {Universit\'e Paris~7}, + TITLE = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur}, + YEAR = {1972} +} + + + +@BOOK{Gir89, + AUTHOR = {Jean-Yves Girard and Yves Lafont and Paul Taylor}, + PUBLISHER = {Cambridge University Press}, + SERIES = {Cambridge Tracts in Theoretical Computer Science 7}, + TITLE = {Proofs and Types}, + YEAR = {1989} +} + +@TechReport{Har95, + author = {John Harrison}, + title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, + institution = {SRI International Cambridge Computer Science Research Centre,}, + year = 1995, + type = {Technical Report}, + number = {CRC-053}, + abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html} +} + +@MASTERSTHESIS{Hir94, + AUTHOR = {Daniel Hirschkoff}, + MONTH = sep, + SCHOOL = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, + TITLE = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, + YEAR = {1994} +} + +@INPROCEEDINGS{HofStr98, + AUTHOR = {Martin Hofmann and Thomas Streicher}, + TITLE = {The groupoid interpretation of type theory}, + BOOKTITLE = {Proceedings of the meeting Twenty-five years of constructive type theory}, + PUBLISHER = {Oxford University Press}, + YEAR = {1998} +} + +@INCOLLECTION{How80, + AUTHOR = {W.A. Howard}, + BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, + EDITOR = {J.P. Seldin and J.R. Hindley}, + NOTE = {Unpublished 1969 Manuscript}, + PUBLISHER = {Academic Press}, + TITLE = {The Formulae-as-Types Notion of Constructions}, + YEAR = {1980} +} + + + +@InProceedings{Hue87tapsoft, + author = {G. Huet}, + title = {Programming of Future Generation Computers}, + booktitle = {Proceedings of TAPSOFT87}, + series = LNCS, + volume = 249, + pages = {276--286}, + year = 1987, + publisher = SV +} + +@INPROCEEDINGS{Hue87, + AUTHOR = {G. Huet}, + BOOKTITLE = {Programming of Future Generation Computers}, + EDITOR = {K. Fuchi and M. Nivat}, + NOTE = {Also in \cite{Hue87tapsoft}}, + PUBLISHER = {Elsevier Science}, + TITLE = {Induction Principles Formalized in the {Calculus of Constructions}}, + YEAR = {1988} +} + + + +@INPROCEEDINGS{Hue88, + AUTHOR = {G. Huet}, + BOOKTITLE = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, + EDITOR = {R. Narasimhan}, + NOTE = {Also in~\cite{CoC89}}, + PUBLISHER = {World Scientific Publishing}, + TITLE = {{The Constructive Engine}}, + YEAR = {1989} +} + +@BOOK{Hue89, + EDITOR = {G. Huet}, + PUBLISHER = {Addison-Wesley}, + SERIES = {The UT Year of Programming Series}, + TITLE = {Logical Foundations of Functional Programming}, + YEAR = {1989} +} + +@INPROCEEDINGS{Hue92, + AUTHOR = {G. Huet}, + BOOKTITLE = {Proceedings of 12th FST/TCS Conference, New Delhi}, + PAGES = {229--240}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {The Gallina Specification Language : A case study}, + VOLUME = {652}, + YEAR = {1992} +} + +@ARTICLE{Hue94, + AUTHOR = {G. Huet}, + JOURNAL = {J. Functional Programming}, + PAGES = {371--394}, + PUBLISHER = {Cambridge University Press}, + TITLE = {Residual theory in $\lambda$-calculus: a formal development}, + VOLUME = {4,3}, + YEAR = {1994} +} + +@INCOLLECTION{HuetLevy79, + AUTHOR = {G. Huet and J.-J. L\'{e}vy}, + TITLE = {Call by Need Computations in Non-Ambigous +Linear Term Rewriting Systems}, + NOTE = {Also research report 359, INRIA, 1979}, + BOOKTITLE = {Computational Logic, Essays in Honor of +Alan Robinson}, + EDITOR = {J.-L. Lassez and G. Plotkin}, + PUBLISHER = {The MIT press}, + YEAR = {1991} +} + +@ARTICLE{KeWe84, + AUTHOR = {J. Ketonen and R. Weyhrauch}, + JOURNAL = {Theoretical Computer Science}, + PAGES = {297--307}, + TITLE = {A decidable fragment of {P}redicate {C}alculus}, + VOLUME = {32}, + YEAR = {1984} +} + +@BOOK{Kle52, + AUTHOR = {S.C. Kleene}, + PUBLISHER = {North-Holland}, + SERIES = {Bibliotheca Mathematica}, + TITLE = {Introduction to Metamathematics}, + YEAR = {1952} +} + +@BOOK{Kri90, + AUTHOR = {J.-L. Krivine}, + PUBLISHER = {Masson}, + SERIES = {Etudes et recherche en informatique}, + TITLE = {Lambda-calcul {types et mod\`eles}}, + YEAR = {1990} +} + +@BOOK{LE92, + EDITOR = {G. Huet and G. Plotkin}, + PUBLISHER = {Cambridge University Press}, + TITLE = {Logical Environments}, + YEAR = {1992} +} + +@BOOK{LF91, + EDITOR = {G. Huet and G. Plotkin}, + PUBLISHER = {Cambridge University Press}, + TITLE = {Logical Frameworks}, + YEAR = {1991} +} + +@ARTICLE{Laville91, + AUTHOR = {A. Laville}, + TITLE = {Comparison of Priority Rules in Pattern +Matching and Term Rewriting}, + JOURNAL = {Journal of Symbolic Computation}, + VOLUME = {11}, + PAGES = {321--347}, + YEAR = {1991} +} + +@INPROCEEDINGS{LePa94, + AUTHOR = {F. Leclerc and C. Paulin-Mohring}, + BOOKTITLE = {{Types for Proofs and Programs, Types' 93}}, + EDITOR = {H. Barendregt and T. Nipkow}, + PUBLISHER = SV, + SERIES = {LNCS}, + TITLE = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, + VOLUME = {806}, + YEAR = {1994} +} + +@TECHREPORT{Leroy90, + AUTHOR = {X. Leroy}, + TITLE = {The {ZINC} experiment: an economical implementation +of the {ML} language}, + INSTITUTION = {INRIA}, + NUMBER = {117}, + YEAR = {1990} +} + +@INPROCEEDINGS{Let02, + author = {P. Letouzey}, + title = {A New Extraction for Coq}, + booktitle = {Proceedings of the TYPES'2002 workshop}, + year = 2002, + note = {to appear}, + url = {draft at \url{http://www.lri.fr/~letouzey/download/extraction2002.ps.gz}} +} + +@BOOK{MaL84, + AUTHOR = {{P. Martin-L\"of}}, + PUBLISHER = {Bibliopolis}, + SERIES = {Studies in Proof Theory}, + TITLE = {Intuitionistic Type Theory}, + YEAR = {1984} +} + +@ARTICLE{MaSi94, + AUTHOR = {P. Manoury and M. Simonot}, + JOURNAL = {TCS}, + TITLE = {Automatizing termination proof of recursively defined function}, + YEAR = {To appear} +} + +@INPROCEEDINGS{Moh89a, + AUTHOR = {Christine Paulin-Mohring}, + ADDRESS = {Austin}, + BOOKTITLE = {Sixteenth Annual ACM Symposium on Principles of Programming Languages}, + MONTH = jan, + PUBLISHER = {ACM}, + TITLE = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}}, + YEAR = {1989} +} + +@PHDTHESIS{Moh89b, + AUTHOR = {Christine Paulin-Mohring}, + MONTH = jan, + SCHOOL = {{Universit\'e Paris 7}}, + TITLE = {Extraction de programmes dans le {Calcul des Constructions}}, + YEAR = {1989} +} + +@INPROCEEDINGS{Moh93, + AUTHOR = {Christine Paulin-Mohring}, + BOOKTITLE = {Proceedings of the conference Typed Lambda Calculi and Applications}, + EDITOR = {M. Bezem and J.-F. Groote}, + NOTE = {Also LIP research report 92-49, ENS Lyon}, + NUMBER = {664}, + PUBLISHER = SV, + SERIES = {LNCS}, + TITLE = {{Inductive Definitions in the System Coq - Rules and Properties}}, + YEAR = {1993} +} + +@BOOK{Moh97, + AUTHOR = {Christine Paulin-Mohring}, + MONTH = jan, + PUBLISHER = {{ENS Lyon}}, + TITLE = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}}, + YEAR = {1997} +} + +@MASTERSTHESIS{Mun94, + AUTHOR = {C. Mu{\~n}oz}, + MONTH = sep, + SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, + TITLE = {D\'emonstration automatique dans la logique propositionnelle intuitionniste}, + YEAR = {1994} +} + +@PHDTHESIS{Mun97d, + AUTHOR = "C. Mu{\~{n}}oz", + TITLE = "Un calcul de substitutions pour la repr\'esentation + de preuves partielles en th\'eorie de types", + SCHOOL = {Universit\'e Paris 7}, + YEAR = "1997", + Note = {Version en anglais disponible comme rapport de + recherche INRIA RR-3309}, + Type = {Th\`ese de Doctorat} +} + +@BOOK{NoPS90, + AUTHOR = {B. {Nordstr\"om} and K. Peterson and J. Smith}, + BOOKTITLE = {Information Processing 83}, + PUBLISHER = {Oxford Science Publications}, + SERIES = {International Series of Monographs on Computer Science}, + TITLE = {Programming in {Martin-L\"of's} Type Theory}, + YEAR = {1990} +} + +@ARTICLE{Nor88, + AUTHOR = {B. {Nordstr\"om}}, + JOURNAL = {BIT}, + TITLE = {Terminating General Recursion}, + VOLUME = {28}, + YEAR = {1988} +} + +@BOOK{Odi90, + EDITOR = {P. Odifreddi}, + PUBLISHER = {Academic Press}, + TITLE = {Logic and Computer Science}, + YEAR = {1990} +} + +@INPROCEEDINGS{PaMS92, + AUTHOR = {M. Parigot and P. Manoury and M. Simonot}, + ADDRESS = {St. Petersburg, Russia}, + BOOKTITLE = {Logic Programming and automated reasoning}, + EDITOR = {A. Voronkov}, + MONTH = jul, + NUMBER = {624}, + PUBLISHER = SV, + SERIES = {LNCS}, + TITLE = {{ProPre : A Programming language with proofs}}, + YEAR = {1992} +} + +@ARTICLE{PaWe92, + AUTHOR = {Christine Paulin-Mohring and Benjamin Werner}, + JOURNAL = {Journal of Symbolic Computation}, + PAGES = {607--640}, + TITLE = {{Synthesis of ML programs in the system Coq}}, + VOLUME = {15}, + YEAR = {1993} +} + +@ARTICLE{Par92, + AUTHOR = {M. Parigot}, + JOURNAL = {Theoretical Computer Science}, + NUMBER = {2}, + PAGES = {335--356}, + TITLE = {{Recursive Programming with Proofs}}, + VOLUME = {94}, + YEAR = {1992} +} + +@INPROCEEDINGS{Parent95b, + AUTHOR = {C. Parent}, + BOOKTITLE = {{Mathematics of Program Construction'95}}, + PUBLISHER = SV, + SERIES = {LNCS}, + TITLE = {{Synthesizing proofs from programs in +the Calculus of Inductive Constructions}}, + VOLUME = {947}, + YEAR = {1995} +} + +@INPROCEEDINGS{Prasad93, + AUTHOR = {K.V. Prasad}, + BOOKTITLE = {{Proceedings of CONCUR'93}}, + PUBLISHER = SV, + SERIES = {LNCS}, + TITLE = {{Programming with broadcasts}}, + VOLUME = {715}, + YEAR = {1993} +} + +@BOOK{RC95, + author = "di~Cosmo, R.", + title = "Isomorphisms of Types: from $\lambda$-calculus to information + retrieval and language design", + series = "Progress in Theoretical Computer Science", + publisher = "Birkhauser", + year = "1995", + note = "ISBN-0-8176-3763-X" +} + +@TECHREPORT{Rou92, + AUTHOR = {J. Rouyer}, + INSTITUTION = {INRIA}, + MONTH = nov, + NUMBER = {1795}, + TITLE = {{D{\'e}veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}}, + YEAR = {1992} +} + +@TECHREPORT{Saibi94, + AUTHOR = {A. Sa\"{\i}bi}, + INSTITUTION = {INRIA}, + MONTH = dec, + NUMBER = {2345}, + TITLE = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}}, + YEAR = {1994} +} + + +@MASTERSTHESIS{Ter92, + AUTHOR = {D. Terrasse}, + MONTH = sep, + SCHOOL = {IARFA}, + TITLE = {{Traduction de TYPOL en COQ. Application \`a Mini ML}}, + YEAR = {1992} +} + +@TECHREPORT{ThBeKa92, + AUTHOR = {L. Th\'ery and Y. Bertot and G. Kahn}, + INSTITUTION = {INRIA Sophia}, + MONTH = may, + NUMBER = {1684}, + TITLE = {Real theorem provers deserve real user-interfaces}, + TYPE = {Research Report}, + YEAR = {1992} +} + +@BOOK{TrDa89, + AUTHOR = {A.S. Troelstra and D. van Dalen}, + PUBLISHER = {North-Holland}, + SERIES = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123}, + TITLE = {Constructivism in Mathematics, an introduction}, + YEAR = {1988} +} + +@PHDTHESIS{Wer94, + AUTHOR = {B. Werner}, + SCHOOL = {Universit\'e Paris 7}, + TITLE = {Une th\'eorie des constructions inductives}, + TYPE = {Th\`ese de Doctorat}, + YEAR = {1994} +} + +@PHDTHESIS{Bar99, + AUTHOR = {B. Barras}, + SCHOOL = {Universit\'e Paris 7}, + TITLE = {Auto-validation d'un système de preuves avec familles inductives}, + TYPE = {Th\`ese de Doctorat}, + YEAR = {1999} +} + +@UNPUBLISHED{ddr98, + AUTHOR = {D. de Rauglaudre}, + TITLE = {Camlp4 version 1.07.2}, + YEAR = {1998}, + NOTE = {In Camlp4 distribution} +} + +@ARTICLE{dowek93, + AUTHOR = {G. Dowek}, + TITLE = {{A Complete Proof Synthesis Method for the Cube of Type Systems}}, + JOURNAL = {Journal Logic Computation}, + VOLUME = {3}, + NUMBER = {3}, + PAGES = {287--315}, + MONTH = {June}, + YEAR = {1993} +} + +@INPROCEEDINGS{manoury94, + AUTHOR = {P. Manoury}, + TITLE = {{A User's Friendly Syntax to Define +Recursive Functions as Typed $\lambda-$Terms}}, + BOOKTITLE = {{Types for Proofs and Programs, TYPES'94}}, + SERIES = {LNCS}, + VOLUME = {996}, + MONTH = jun, + YEAR = {1994} +} + +@TECHREPORT{maranget94, + AUTHOR = {L. Maranget}, + INSTITUTION = {INRIA}, + NUMBER = {2385}, + TITLE = {{Two Techniques for Compiling Lazy Pattern Matching}}, + YEAR = {1994} +} + +@INPROCEEDINGS{puel-suarez90, + AUTHOR = {L.Puel and A. Su\'arez}, + BOOKTITLE = {{Conference Lisp and Functional Programming}}, + SERIES = {ACM}, + PUBLISHER = SV, + TITLE = {{Compiling Pattern Matching by Term +Decomposition}}, + YEAR = {1990} +} + +@MASTERSTHESIS{saidi94, + AUTHOR = {H. Saidi}, + MONTH = sep, + SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, + TITLE = {R\'esolution d'\'equations dans le syst\`eme T + de G\"odel}, + YEAR = {1994} +} + +@misc{streicher93semantical, + author = "T. Streicher", + title = "Semantical Investigations into Intensional Type Theory", + note = "Habilitationsschrift, LMU Munchen.", + year = "1993" } + + + +@Misc{Pcoq, + author = {Lemme Team}, + title = {Pcoq a graphical user-interface for {Coq}}, + note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} +} + + +@Misc{ProofGeneral, + author = {David Aspinall}, + title = {Proof General}, + note = {\url{http://proofgeneral.inf.ed.ac.uk/}} +} + + + +@Book{CoqArt, + author = {Yves bertot and Pierre Castéran}, + title = {Coq'Art}, + publisher = {Springer-Verlag}, + year = 2004, + note = {To appear} +} + +@INCOLLECTION{wadler87, + AUTHOR = {P. Wadler}, + TITLE = {Efficient Compilation of Pattern Matching}, + BOOKTITLE = {The Implementation of Functional Programming +Languages}, + EDITOR = {S.L. Peyton Jones}, + PUBLISHER = {Prentice-Hall}, + YEAR = {1987} +} + + +@COMMENT{cross-references, must be at end} + +@BOOK{Bastad92, + EDITOR = {B. Nordstr\"om and K. Petersson and G. Plotkin}, + PUBLISHER = {Available by ftp at site ftp.inria.fr}, + TITLE = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, + YEAR = {1992} +} + +@BOOK{Nijmegen93, + EDITOR = {H. Barendregt and T. Nipkow}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {Types for Proofs and Programs}, + VOLUME = {806}, + YEAR = {1994} +} + +@PHDTHESIS{Luo90, + AUTHOR = {Z. Luo}, + TITLE = {An Extended Calculus of Constructions}, + SCHOOL = {University of Edinburgh}, + YEAR = {1990} +} diff --git a/doc/faq/hevea.sty b/doc/faq/hevea.sty new file mode 100644 index 00000000..6d49aa8c --- /dev/null +++ b/doc/faq/hevea.sty @@ -0,0 +1,78 @@ +% hevea : hevea.sty +% This is a very basic style file for latex document to be processed +% with hevea. It contains definitions of LaTeX environment which are +% processed in a special way by the translator. +% Mostly : +% - latexonly, not processed by hevea, processed by latex. +% - htmlonly , the reverse. +% - rawhtml, to include raw HTML in hevea output. +% - toimage, to send text to the image file. +% The package also provides hevea logos, html related commands (ahref +% etc.), void cutting and image commands. +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{hevea}[2002/01/11] +\RequirePackage{comment} +\newif\ifhevea\heveafalse +\@ifundefined{ifimagen}{\newif\ifimagen\imagenfalse} +\makeatletter% +\newcommand{\heveasmup}[2]{% +\raise #1\hbox{$\m@th$% + \csname S@\f@size\endcsname + \fontsize\sf@size 0% + \math@fontsfalse\selectfont +#2% +}}% +\DeclareRobustCommand{\hevea}{H\kern-.15em\heveasmup{.2ex}{E}\kern-.15emV\kern-.15em\heveasmup{.2ex}{E}\kern-.15emA}% +\DeclareRobustCommand{\hacha}{H\kern-.15em\heveasmup{.2ex}{A}\kern-.15emC\kern-.1em\heveasmup{.2ex}{H}\kern-.15emA}% +\DeclareRobustCommand{\html}{\protect\heveasmup{0.ex}{HTML}} +%%%%%%%%% Hyperlinks hevea style +\newcommand{\ahref}[2]{{#2}} +\newcommand{\ahrefloc}[2]{{#2}} +\newcommand{\aname}[2]{{#2}} +\newcommand{\ahrefurl}[1]{\texttt{#1}} +\newcommand{\footahref}[2]{#2\footnote{\texttt{#1}}} +\newcommand{\mailto}[1]{\texttt{#1}} +\newcommand{\imgsrc}[2][]{} +\newcommand{\home}[1]{\protect\raisebox{-.75ex}{\char126}#1} +\AtBeginDocument +{\@ifundefined{url} +{%url package is not loaded +\let\url\ahref\let\oneurl\ahrefurl\let\footurl\footahref} +{}} +%% Void cutting instructions +\newcounter{cuttingdepth} +\newcommand{\tocnumber}{} +\newcommand{\notocnumber}{} +\newcommand{\cuttingunit}{} +\newcommand{\cutdef}[2][]{} +\newcommand{\cuthere}[2]{} +\newcommand{\cutend}{} +\newcommand{\htmlhead}[1]{} +\newcommand{\htmlfoot}[1]{} +\newcommand{\htmlprefix}[1]{} +\newenvironment{cutflow}[1]{}{} +\newcommand{\cutname}[1]{} +\newcommand{\toplinks}[3]{} +%%%% Html only +\excludecomment{rawhtml} +\newcommand{\rawhtmlinput}[1]{} +\excludecomment{htmlonly} +%%%% Latex only +\newenvironment{latexonly}{}{} +\newenvironment{verblatex}{}{} +%%%% Image file stuff +\def\toimage{\endgroup} +\def\endtoimage{\begingroup\def\@currenvir{toimage}} +\def\verbimage{\endgroup} +\def\endverbimage{\begingroup\def\@currenvir{verbimage}} +\newcommand{\imageflush}[1][]{} +%%% Bgcolor definition +\newsavebox{\@bgcolorbin} +\newenvironment{bgcolor}[2][] + {\newcommand{\@mycolor}{#2}\begin{lrbox}{\@bgcolorbin}\vbox\bgroup} + {\egroup\end{lrbox}% + \begin{flushleft}% + \colorbox{\@mycolor}{\usebox{\@bgcolorbin}}% + \end{flushleft}} +%%% Postlude +\makeatother diff --git a/doc/faq/interval_discr.v b/doc/faq/interval_discr.v new file mode 100644 index 00000000..972300da --- /dev/null +++ b/doc/faq/interval_discr.v @@ -0,0 +1,419 @@ +(** Sketch of the proof of {p:nat|p<=n} = {p:nat|p<=m} -> n=m + + - preliminary results on the irrelevance of boundedness proofs + - introduce the notion of finite cardinal |A| + - prove that |{p:nat|p<=n}| = n + - prove that |A| = n /\ |A| = m -> n = m if equality is decidable on A + - prove that equality is decidable on A + - conclude +*) + +(** * Preliminary results on [nat] and [le] *) + +(** Proving axiom K on [nat] *) + +Require Import Eqdep_dec. +Require Import Arith. + +Theorem eq_rect_eq_nat : + forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h. +Proof. +intros. +apply K_dec_set with (p := h). +apply eq_nat_dec. +reflexivity. +Qed. + +(** Proving unicity of proofs of [(n<=m)%nat] *) + +Scheme le_ind' := Induction for le Sort Prop. + +Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q. +Proof. +induction p using le_ind'; intro q. + replace (le_n n) with + (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)). + 2:reflexivity. + generalize (refl_equal n). + pattern n at 2 4 6 10, q; case q; [intro | intros m l e]. + rewrite <- eq_rect_eq_nat; trivial. + contradiction (le_Sn_n m); rewrite <- e; assumption. + replace (le_S n m p) with + (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))). + 2:reflexivity. + generalize (refl_equal (S m)). + pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS]. + contradiction (le_Sn_n m); rewrite Heq; assumption. + injection HeqS; intro Heq; generalize l HeqS. + rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat. + rewrite (IHp l0); reflexivity. +Qed. + +(** Proving irrelevance of boundedness proofs while building + elements of interval *) + +Lemma dep_pair_intro : + forall (n x y:nat) (Hx : x<=n) (Hy : y<=n), x=y -> + exist (fun x => x <= n) x Hx = exist (fun x => x <= n) y Hy. +Proof. +intros n x y Hx Hy Heq. +generalize Hy. +rewrite <- Heq. +intros. +rewrite (le_uniqueness_proof x n Hx Hy0). +reflexivity. +Qed. + +(** * Proving that {p:nat|p<=n} = {p:nat|p<=m} -> n=m *) + +(** Definition of having finite cardinality [n+1] for a set [A] *) + +Definition card (A:Set) n := + exists f, + (forall x:A, f x <= n) /\ + (forall x y:A, f x = f y -> x = y) /\ + (forall m, m <= n -> exists x:A, f x = m). + +Require Import Arith. + +(** Showing that the interval [0;n] has cardinality [n+1] *) + +Theorem card_interval : forall n, card {x:nat|x<=n} n. +Proof. +intro n. +exists (fun x:{x:nat|x<=n} => proj1_sig x). +split. +(* bounded *) +intro x; apply (proj2_sig x). +split. +(* injectivity *) +intros (p,Hp) (q,Hq). +simpl. +intro Hpq. +apply dep_pair_intro; assumption. +(* surjectivity *) +intros m Hmn. +exists (exist (fun x : nat => x <= n) m Hmn). +reflexivity. +Qed. + +(** Showing that equality on the interval [0;n] is decidable *) + +Lemma interval_dec : + forall n (x y : {m:nat|m<=n}), {x=y}+{x<>y}. +Proof. +intros n (p,Hp). +induction p; intros ([|q],Hq). +left. + apply dep_pair_intro. + reflexivity. +right. + intro H; discriminate H. +right. + intro H; discriminate H. +assert (Hp' : p <= n). + apply le_Sn_le; assumption. +assert (Hq' : q <= n). + apply le_Sn_le; assumption. +destruct (IHp Hp' (exist (fun m => m <= n) q Hq')) + as [Heq|Hneq]. +left. + injection Heq; intro Heq'. + apply dep_pair_intro. + apply eq_S. + assumption. +right. + intro HeqS. + injection HeqS; intro Heq. + apply Hneq. + apply dep_pair_intro. + assumption. +Qed. + +(** Showing that the cardinality relation is functional on decidable sets *) + +Lemma card_inj_aux : + forall (A:Type) f g n, + (forall x:A, f x <= 0) -> + (forall x y:A, f x = f y -> x = y) -> + (forall m, m <= S n -> exists x:A, g x = m) + -> False. +Proof. +intros A f g n Hfbound Hfinj Hgsurj. +destruct (Hgsurj (S n) (le_n _)) as (x,Hx). +destruct (Hgsurj n (le_S _ _ (le_n _))) as (x',Hx'). +assert (Hfx : 0 = f x). +apply le_n_O_eq. +apply Hfbound. +assert (Hfx' : 0 = f x'). +apply le_n_O_eq. +apply Hfbound. +assert (x=x'). +apply Hfinj. +rewrite <- Hfx. +rewrite <- Hfx'. +reflexivity. +rewrite H in Hx. +rewrite Hx' in Hx. +apply (n_Sn _ Hx). +Qed. + +(** For [dec_restrict], we use a lemma on the negation of equality +that requires proof-irrelevance. It should be possible to avoid this +lemma by generalizing over a first-order definition of [x<>y], say +[neq] such that [{x=y}+{neq x y}] and [~(x=y /\ neq x y)]; for such +[neq], unicity of proofs could be proven *) + + Require Import Classical. + Lemma neq_dep_intro : + forall (A:Set) (z x y:A) (p:x<>z) (q:y<>z), x=y -> + exist (fun x => x <> z) x p = exist (fun x => x <> z) y q. + Proof. + intros A z x y p q Heq. + generalize q; clear q; rewrite <- Heq; intro q. + rewrite (proof_irrelevance _ p q); reflexivity. + Qed. + +Lemma dec_restrict : + forall (A:Set), + (forall x y :A, {x=y}+{x<>y}) -> + forall z (x y :{a:A|a<>z}), {x=y}+{x<>y}. +Proof. +intros A Hdec z (x,Hx) (y,Hy). +destruct (Hdec x y) as [Heq|Hneq]. +left; apply neq_dep_intro; assumption. +right; intro Heq; injection Heq; exact Hneq. +Qed. + +Lemma pred_inj : forall n m, + 0 <> n -> 0 <> m -> pred m = pred n -> m = n. +Proof. +destruct n. +intros m H; destruct H; reflexivity. +destruct m. +intros _ H; destruct H; reflexivity. +simpl; intros _ _ H. +rewrite H. +reflexivity. +Qed. + +Lemma le_neq_lt : forall n m, n <= m -> n<>m -> n < m. +Proof. +intros n m Hle Hneq. +destruct (le_lt_eq_dec n m Hle). +assumption. +contradiction. +Qed. + +Lemma inj_restrict : + forall (A:Set) (f:A->nat) x y z, + (forall x y : A, f x = f y -> x = y) + -> x <> z -> f y < f z -> f z <= f x + -> pred (f x) = f y + -> False. + +(* Search error sans le type de f !! *) +Proof. +intros A f x y z Hfinj Hneqx Hfy Hfx Heq. +assert (f z <> f x). + apply sym_not_eq. + intro Heqf. + apply Hneqx. + apply Hfinj. + assumption. +assert (f x = S (f y)). + assert (0 < f x). + apply le_lt_trans with (f z). + apply le_O_n. + apply le_neq_lt; assumption. + apply pred_inj. + apply O_S. + apply lt_O_neq; assumption. + exact Heq. +assert (f z <= f y). +destruct (le_lt_or_eq _ _ Hfx). + apply lt_n_Sm_le. + rewrite <- H0. + assumption. + contradiction Hneqx. + symmetry. + apply Hfinj. + assumption. +contradiction (lt_not_le (f y) (f z)). +Qed. + +Theorem card_inj : forall m n (A:Set), + (forall x y :A, {x=y}+{x<>y}) -> + card A m -> card A n -> m = n. +Proof. +induction m; destruct n; +intros A Hdec + (f,(Hfbound,(Hfinj,Hfsurj))) + (g,(Hgbound,(Hginj,Hgsurj))). +(* 0/0 *) +reflexivity. +(* 0/Sm *) +destruct (card_inj_aux _ _ _ _ Hfbound Hfinj Hgsurj). +(* Sn/0 *) +destruct (card_inj_aux _ _ _ _ Hgbound Hginj Hfsurj). +(* Sn/Sm *) +destruct (Hgsurj (S n) (le_n _)) as (xSn,HSnx). +rewrite IHm with (n:=n) (A := {x:A|x<>xSn}). +reflexivity. +(* decidability of eq on {x:A|x<>xSm} *) +apply dec_restrict. +assumption. +(* cardinality of {x:A|x<>xSn} is m *) +pose (f' := fun x' : {x:A|x<>xSn} => + let (x,Hneq) := x' in + if le_lt_dec (f xSn) (f x) + then pred (f x) + else f x). +exists f'. +split. +(* f' is bounded *) +unfold f'. +intros (x,_). +destruct (le_lt_dec (f xSn) (f x)) as [Hle|Hge]. +change m with (pred (S m)). +apply le_pred. +apply Hfbound. +apply le_S_n. +apply le_trans with (f xSn). +exact Hge. +apply Hfbound. +split. +(* f' is injective *) +unfold f'. +intros (x,Hneqx) (y,Hneqy) Heqf'. +destruct (le_lt_dec (f xSn) (f x)) as [Hlefx|Hgefx]; +destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy]. +(* f xSn <= f x et f xSn <= f y *) +assert (Heq : x = y). + apply Hfinj. + assert (f xSn <> f y). + apply sym_not_eq. + intro Heqf. + apply Hneqy. + apply Hfinj. + assumption. + assert (0 < f y). + apply le_lt_trans with (f xSn). + apply le_O_n. + apply le_neq_lt; assumption. + assert (f xSn <> f x). + apply sym_not_eq. + intro Heqf. + apply Hneqx. + apply Hfinj. + assumption. + assert (0 < f x). + apply le_lt_trans with (f xSn). + apply le_O_n. + apply le_neq_lt; assumption. + apply pred_inj. + apply lt_O_neq; assumption. + apply lt_O_neq; assumption. + assumption. +apply neq_dep_intro; assumption. +(* f y < f xSn <= f x *) +destruct (inj_restrict A f x y xSn); assumption. +(* f x < f xSn <= f y *) +symmetry in Heqf'. +destruct (inj_restrict A f y x xSn); assumption. +(* f x < f xSn et f y < f xSn *) +assert (Heq : x=y). + apply Hfinj; assumption. +apply neq_dep_intro; assumption. +(* f' is surjective *) +intros p Hlep. +destruct (le_lt_dec (f xSn) p) as [Hle|Hlt]. +(* case f xSn <= p *) +destruct (Hfsurj (S p) (le_n_S _ _ Hlep)) as (x,Hx). +assert (Hneq : x <> xSn). + intro Heqx. + rewrite Heqx in Hx. + rewrite Hx in Hle. + apply le_Sn_n with p; assumption. +exists (exist (fun a => a<>xSn) x Hneq). +unfold f'. +destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt']. +rewrite Hx; reflexivity. +rewrite Hx in Hlt'. +contradiction (le_not_lt (f xSn) p). +apply lt_trans with (S p). +apply lt_n_Sn. +assumption. +(* case p < f xSn *) +destruct (Hfsurj p (le_S _ _ Hlep)) as (x,Hx). +assert (Hneq : x <> xSn). + intro Heqx. + rewrite Heqx in Hx. + rewrite Hx in Hlt. + apply (lt_irrefl p). + assumption. +exists (exist (fun a => a<>xSn) x Hneq). +unfold f'. +destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt']. + rewrite Hx in Hle'. + contradiction (lt_irrefl p). + apply lt_le_trans with (f xSn); assumption. + assumption. +(* cardinality of {x:A|x<>xSn} is n *) +pose (g' := fun x' : {x:A|x<>xSn} => + let (x,Hneq) := x' in + if Hdec x xSn then 0 else g x). +exists g'. +split. +(* g is bounded *) +unfold g'. +intros (x,_). +destruct (Hdec x xSn) as [_|Hneq]. +apply le_O_n. +assert (Hle_gx:=Hgbound x). +destruct (le_lt_or_eq _ _ Hle_gx). +apply lt_n_Sm_le. +assumption. +contradiction Hneq. +apply Hginj. +rewrite HSnx. +assumption. +split. +(* g is injective *) +unfold g'. +intros (x,Hneqx) (y,Hneqy) Heqg'. +destruct (Hdec x xSn) as [Heqx|_]. +contradiction Hneqx. +destruct (Hdec y xSn) as [Heqy|_]. +contradiction Hneqy. +assert (Heq : x=y). + apply Hginj; assumption. +apply neq_dep_intro; assumption. +(* g is surjective *) +intros p Hlep. +destruct (Hgsurj p (le_S _ _ Hlep)) as (x,Hx). +assert (Hneq : x<>xSn). + intro Heq. + rewrite Heq in Hx. + rewrite Hx in HSnx. + rewrite HSnx in Hlep. + contradiction (le_Sn_n _ Hlep). +exists (exist (fun a => a<>xSn) x Hneq). +simpl. +destruct (Hdec x xSn) as [Heqx|_]. +contradiction Hneq. +assumption. +Qed. + +(** Conclusion *) + +Theorem interval_discr : + forall n m, {p:nat|p<=n} = {p:nat|p<=m} -> n=m. +Proof. +intros n m Heq. +apply card_inj with (A := {p:nat|p<=n}). +apply interval_dec. +apply card_interval. +rewrite Heq. +apply card_interval. +Qed. |
