diff options
| author | herbelin | 2004-05-05 16:39:37 +0000 |
|---|---|---|
| committer | herbelin | 2004-05-05 16:39:37 +0000 |
| commit | 065b90d939737359087e91da08c05a54fdb1ec12 (patch) | |
| tree | 05f42170a3ce3f54b719e5d8f5a3d7490dfc1c50 | |
| parent | 33f22b5496af7e1da96a40956a7b7124a1b67032 (diff) | |
MAJ diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8571 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/newfaq/axioms.eps | 20 | ||||
| -rw-r--r-- | doc/newfaq/axioms.fig | 6 | ||||
| -rw-r--r-- | doc/newfaq/main.tex | 516 | ||||
| -rw-r--r-- | doc/newfaq/main.v001.gif | bin | 5289 -> 5314 bytes |
4 files changed, 300 insertions, 242 deletions
diff --git a/doc/newfaq/axioms.eps b/doc/newfaq/axioms.eps index 914b48ec98..3f3c01c43a 100644 --- a/doc/newfaq/axioms.eps +++ b/doc/newfaq/axioms.eps @@ -1,7 +1,7 @@ %!PS-Adobe-2.0 EPSF-2.0 %%Title: axioms.fig %%Creator: fig2dev Version 3.2 Patchlevel 4 -%%CreationDate: Fri Apr 30 17:32:43 2004 +%%CreationDate: Wed May 5 18:30:03 2004 %%For: herbelin@limoux.polytechnique.fr (Hugo Herbelin) %%BoundingBox: 0 0 437 372 %%Magnification: 1.0000 @@ -355,15 +355,6 @@ gs 1 -1 sc (Not excluded-middle) col0 sh gr 3600 6000 m gs 1 -1 sc (Axiom K on A) col0 sh gr /Times-Roman-iso ff 180.00 scf sf -3600 6300 m -gs 1 -1 sc (Unicity 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 (Unicity of equality proofs on A) 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 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 @@ -372,6 +363,15 @@ 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 diff --git a/doc/newfaq/axioms.fig b/doc/newfaq/axioms.fig index 328e324d63..f07759302f 100644 --- a/doc/newfaq/axioms.fig +++ b/doc/newfaq/axioms.fig @@ -76,9 +76,9 @@ Single 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 3390 3600 6300 Unicity of reflexivity proofs for equality on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 2325 3600 6600 Unicity of equality proofs on A\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 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/newfaq/main.tex b/doc/newfaq/main.tex index 072b90ff88..caad5de5a5 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -99,6 +99,8 @@ {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} @@ -146,7 +148,7 @@ pointers to other references when possible. 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 +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 @@ -156,7 +158,7 @@ answers, feel free to write to us\ldots \section{Presentation} -\Question{What is {\Coq} ?}\label{whatiscoq} +\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} @@ -167,7 +169,7 @@ In particular, {\Coq} allows: \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 ?} +\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 @@ -182,24 +184,13 @@ resolution, ...) but the main style for proving theorems is interactively by using LCF-style tactics. -\Question{What are the other theorem provers ?} +\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, Alfa, Elf, Kiv, Mizar, NqThm, $\Omega$mega\ldots -\Question{What's the status of proofs in \Coq} - -{\Coq} proofs are build with tactics allowing both forward -reasoning (stating - -cannot be accepted without a proof expressed in the Calculus of -Inductive Constructions. The correctness of a proof relies on a -relatively small proof-checker at the kernel of {\Coq} (8000 lines of ML -code). Even {\Coq} decision procedures are producing proofs which are -double-checked by the kernel. - -\Question{Who do I have to trust when I see a proof checked by Coq ?} +\Question{Who do I have to trust when I see a proof checked by Coq?} You have to trust : @@ -224,24 +215,28 @@ Eduardo Giménez' thesis~\cite{EGThese} \end{description} -\Question{How can I use {\Coq} to prove programs ?} +\Question{How can I use {\Coq} to prove programs?} -You can either extract a program from a proof use the extraction +You can either extract a program from a proof by using the extraction mechanism or use dedicated tools, such as \Why, \Krakatoa, \Caduceus, to prove annotated programs written in other languages. -\Question{How many {\Coq} users are there ?} +\Question{How many {\Coq} users are there?} -Estimation is about 100 regular users. +An estimation is about 100 regular users. -\Question{How old is {\Coq} ?} -The first official release of {\Coq} (v. 4.10) was distributed in 1989. +\Question{How old is {\Coq}?} -\Question{What are the \Coq-related tools ?} +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?} \begin{description} -\item[Coqide] A GTK based gui for \Coq. -\item[Pcoq] A gui for {\Coq} with proof by pointing and pretty printing. +\item[Coqide] A GTK based GUI for \Coq. +\item[Pcoq] A GUI for {\Coq} with proof by pointing and pretty printing. \item[Helm/Mowgli] A rendering, searching and publishing tool. \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. @@ -263,40 +258,46 @@ The first official release of {\Coq} (v. 4.10) was distributed in 1989. \item Prolog-style proof search, possibly involving equalities \end{itemize} -\Question{What are the main libraries of \Coq} +\Question{What are the main libraries available for \Coq} \begin{itemize} -\item Basic Peano's arithmetic -\item Binary integer numbers -\item Real analysis -\item Libraries for lists, boolean, maps. -\item Libraries for relations, sets +\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 academic applications for {\Coq} ?} +\Question{What are the academic applications for {\Coq}?} + +{\Coq} is used for formalizing mathematicians, for teaching, +and for proving properties of algorithms or programs libraries. -{\Coq} is used by mathematicians for formalizing large parts of mathematics, by teachers, and computer scientists to prove programs and APIs. +The largest mathematical formalization has been done at the University +of Nijmegen (see the Constructive Coq Repository at Nijmegen +\ahref{http://vacuumcleaner.cs.kun.nl/c-corn}{\url{http://vacuumcleaner.cs.kun.nl/c-corn}}. -\Question{What are the industrial applications for {\Coq} ?} + +\Question{What are the industrial applications for {\Coq}?} {\Coq} is used by Trusted Logic to prove properties of the JavaCard system. -todo christine compilo lustre ? +todo christine compilo lustre? %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Documentation} -\Question{Where can I find documentation about {\Coq} ?} +\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 online at -\ahref{http://coq.inria.fr/coq/doc-eng.html}{\url{http://coq.inria.fr/coq/doc-eng.html}}. +\ahref{http://coq.inria.fr/doc-eng.html}{\url{http://coq.inria.fr/doc-eng.html}}. All these documents are viewable either in browsable HTML, or as downloadable postscripts. -\Question{Where can I find this FAQ on the web ?} +\Question{Where can I find this FAQ on the web?} This FAQ is available online at \ahref{http://coq.inria.fr/faq.html}{\url{http://coq.inria.fr/faq.html}}. @@ -305,7 +306,7 @@ This FAQ is available online at \ahref{http://coq.inria.fr/faq.html}{\url{http:/ 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} ?} +\Question{Is there any mailing list about {\Coq}?} The main {\Coq} mailing list is \url{coq-club@coq.inria.fr}, which broadcasts questions and suggestions about the implementation, the logical formalism or proof developments. See @@ -317,12 +318,12 @@ The archives of the {\Coq} mailing list are available at \ahref{http://coq.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} ?} +\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} ?} +\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 @@ -332,15 +333,15 @@ students, and engineers interested in formal methods and the development of zero-default software.'' \end{quote} -\Question{Where can I find some {\Coq} examples ?} +\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{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/distrib-eng.html}{\url{http://coq.inria.fr/distrib-eng.html}}. +\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} +\Question{How can I report a bug?}\label{coqbug} You can use the web interface at \ahref{http://coq.inria.fr/bin/coq-bugs}{\url{http://coq.inria.fr/bin/coq-bugs}}. @@ -350,23 +351,23 @@ You can use the web interface at \ahref{http://coq.inria.fr/bin/coq-bugs}{\url{h \section{Installation} -\Question{What is the license of {\Coq} ?} +\Question{What is the license of {\Coq}?} It is distributed under the GNU Lesser General License (LGPL). -\Question{Where can I find the sources of {\Coq} ?} +\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/distrib-eng.html}{\url{http://coq.inria.fr/distrib-eng.html}}). Development sources can be accessed via anonymous CVS : \ahref{http://coqcvs.inria.fr/}{\url{http://coqcvs.inria.fr/}} -\Question{On which platform {\Coq} is available ?} +\Question{On which platform is {\Coq} available?} Compiled binaries are available for Linux, MacOS X, Solaris, and -Windows. The sources can be easily adapted to all platforms supporting Objective Caml. +Windows. The sources can be easily compiled on all platforms supporting Objective Caml. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Logic} +\section{The logic of {\Coq}} -\subsection{The logic of {\Coq}} +\subsection{General} \Question{What is the logic of \Coq?} @@ -381,13 +382,25 @@ predicates, and a stratified hierarchy of sets. {\Coq} theory is basically intuitionistic (i.e. excluded-middle $A\lor\neg A$ is not granted by default) with the possibility to reason classically on demand by requiring an -optional module stating $A\lor\neg A$. +optional axiom stating $A\lor\neg A$. \Question{Can I define non-terminating programs in \Coq?} No, all programs in {\Coq} are terminating. Especially, loops must come with an evidence of their termination. +\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}?} @@ -410,7 +423,6 @@ standard library of {\Coq}. The most interesting ones are Here is a summary of the relative strength of these axioms, most proofs can be found in directory {\tt Logic} of the standard library. -%\include{axioms} \includegraphics{axioms} \Question{What standard axioms are inconsistent with {\Coq}?} @@ -451,7 +463,6 @@ 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} -which states that \begin{coq_example*} Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2. @@ -484,29 +495,47 @@ Axiom eq_dep U P u p1 u p2 -> p1 = p2. \end{coq_example*} -\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{Can I identify two functions that have the same behaviour (extensionality)?} +\Question{What is proof-irrelevance} +\label{proof-irrelevance} - Extensionality of functions is an axiom in, say set theory, -but from a programming point of view, extensionality cannot be {\em a -priori} accepted since it would identify, say programs as mergesort -and quicksort. +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 corresponds to a model where provability, whatever the +proof is, is more important than the computational content of the +proof. This is in harmony with the common purely logical +interpretation of {\Prop}. Contrastingly, proof-irrelevance is +inconsistent in {\Set} in harmony with the computational meaning of +the sort {\Set}. + +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}). + +Conversely, proof-irrelevance directly implies Streicher's axiom $K$. + +\Question{What about functional extensionality?} + +Extensionality of functions is an axiom in, say set theory, but from a +programing point of view, extensionality cannot be {\em a priori} +accepted since it would identify, say programs such as mergesort and +quicksort. %\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=, the recommended approach is to define his +\verb=A->B=, the recommended approach is to define one's own extensional equality on \verb=A->B=. \begin{coq_eval} @@ -520,46 +549,63 @@ Definition ext_eq (f g: A->B) := forall x:A, f x = g x. and to reason on \verb=A->B= as a setoid (see the Chapter on Setoids in the Reference Manual). -\Question{Is {\Type} impredicative (that is, letting -\coqtt{T:=(X:Type)X->X}, can I apply an expression \coqtt{t} of type \coqtt{T} to \coqtt{T} itself)?} +\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. - No, {\Type} is stratified. This is hidden for the +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 Girard's systems $U-$ and $U$ -could be encoded 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. +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 +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) => z x x}. - +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?} -\label{proof-irrelevance} - In the base {\Coq} system, the answer is no. However, if +In the base {\Coq} system, the answer is no. However, if classical logic is set, the answer is yes for propositions in {\Prop}. - -More precisely, the equality of all proofs of a given proposition is called -{\em proof-irrelevance}. Proof-irrelevance (in {\Prop}) can be assumed - without leading to contradiction in {\Coq}. - - That classical logic (what can be assumed in {\Coq} by requiring the file - \vfile{\LogicClassical}{Classical}) implies proof-irrelevance is shown in files - \vfile{\LogicProofIrrelevance}{ProofIrrelevance} and \vfile{\LogicBerardi}{Berardi}. - - Alternatively, propositional extensionality (i.e. \coqtt{(A - {\coqequiv} B) {\coqimp} A=B}, defined in \vfile{\LogicClassicalFacts}{ClassicalFacts}), - also implies proof-irrelevance. +See question \ref{proof-irrelevance}. % It is an ongoing work of research to natively include proof % irrelevance in {\Coq}. @@ -586,27 +632,14 @@ 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{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{Impredicativity} -\Question{Why Injection does not work on impredicative {\tt Set}?} +\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: + variant of \Coq): \begin{coq_eval} Reset Initial. @@ -653,10 +686,10 @@ paradox \cite{Gir70,Coq85}. %%%%%%% -\subsection{My goal is ..., how can I prove it ?} +\subsection{My goal is ..., how can I prove it?} -\Question{My goal is a conjunction, 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} @@ -668,7 +701,7 @@ assumption. Qed. \end{coq_example} -\Question{My goal contains a conjunction as an hypothesis, how can I use it ?} +\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 : @@ -681,7 +714,7 @@ Qed. \end{coq_example} -\Question{My goal is a disjunction, how can I prove it ?} +\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 @@ -703,12 +736,12 @@ Require Import Classical. Ltac classical_right := match goal with -| _:_ |- ?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) +| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) end. Ltac classical_left := match goal with -| _:_ |- _ \/ ?X1 => (elim (classic X1);intro;[right;trivial|left]) +| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) end. @@ -719,7 +752,7 @@ auto. Qed. \end{coq_example} -\Question{My goal is an universally quantified statement, how can I prove it ?} +\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 @@ -728,7 +761,7 @@ 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 ?} +\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} @@ -740,7 +773,7 @@ Qed. \end{coq_example} -\Question{My goal is solvable by some lemma, how can I prove it ?} +\Question{My goal is solvable by some lemma, how can I prove it?} Just use the {\apply} tactic. @@ -760,12 +793,12 @@ Qed. -\Question{My goal contains False as an hypotheses, how can I prove it ?} +\Question{My goal contains False as an hypotheses, 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 ?} +\Question{My goal is an equality of two convertible terms, how can I prove it?} Just use the {\reflexivity} tactic. @@ -776,28 +809,28 @@ reflexivity. Qed. \end{coq_example} -\Question{My goal is a {\tt let x := a in ...}, how can I prove it ?} +\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 ?} +\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 ?} +\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 ?} +\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 ?} +\Question{My goal is an equality, how can I swap the left and right hand terms?} Just use the {\symmetry} tactic. \begin{coq_example} @@ -808,7 +841,7 @@ assumption. Qed. \end{coq_example} -\Question{My hypothesis is an equality, how can I swap the left and right hand terms ?} +\Question{My hypothesis is an equality, how can I swap the left and right hand terms?} Just use the {\symmetryin} tactic. @@ -821,7 +854,7 @@ Qed. \end{coq_example} -\Question{My goal is an equality, how can I prove it by transitivity ?} +\Question{My goal is an equality, how can I prove it by transitivity?} Just use the {\transitivity} tactic. \begin{coq_example} @@ -834,7 +867,7 @@ 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 ?} +\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. @@ -870,7 +903,7 @@ 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 ?} +\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. @@ -896,7 +929,7 @@ Qed. \end{coq_example} -\Question{My goal is one of the hypotheses, how can I prove it ?} +\Question{My goal is one of the hypotheses, how can I prove it?} Use the {\assumption} tactic. @@ -908,7 +941,7 @@ 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 ?} +\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} @@ -918,14 +951,14 @@ 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 ?} +\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 ?} +\Question{My goal is a propositional tautology, how can I prove it?} Just use the {\tauto} tactic. \begin{coq_example} @@ -935,13 +968,13 @@ tauto. Qed. \end{coq_example} -\Question{My goal is a first order formula, how can I prove it ?} +\Question{My goal is a first order formula, how can I prove it?} Just use the semi-decision tactic : \firstorder. todo : demander un exemple ŕ Pierre -\Question{My goal is solvable by a sequence of rewrites, how can I prove it ?} +\Question{My goal is solvable by a sequence of rewrites, how can I prove it?} Just use the {\congruence} tactic. \begin{coq_example} @@ -952,7 +985,7 @@ Qed. \end{coq_example} -\Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it ?} +\Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?} Just use the {\congruence} tactic. @@ -964,7 +997,7 @@ Qed. \end{coq_example} -\Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it ?} +\Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?} Just use the {\ring} tactic. @@ -978,7 +1011,7 @@ ring. Qed. \end{coq_example} -\Question{My goal is an equality on some field (e.g. real numbers), how can I prove it ?} +\Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?} Just use the {\field} tactic. @@ -994,7 +1027,7 @@ 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 ?} +\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} @@ -1008,13 +1041,13 @@ 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 ?} +\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 ?} +\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 @@ -1042,73 +1075,73 @@ Qed. -\Question{I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it ?} +\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} ?} +\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 ?} +\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 ?} +\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} ?} +\Question{What is {\eauto}?} This is the same tactic as \auto, but it does some {\eapply} instead of \apply. todo les espaces -\Question{How can I speed up {\auto} ?} +\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 ?} +\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 ?} +\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 ?} +\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 ?} +\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 ?} +\Question{How can I reduce some term?} You can use the {\simpl} tactic. -\Question{How can I declare a shortcut for some term ?} +\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 ?} +\Question{How can I perform case analysis?} You can use the {\case} or {\destruct} tactics. -\Question{Why should I name my intros ?} +\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 @@ -1116,7 +1149,7 @@ 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 ?} +\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}. @@ -1133,7 +1166,7 @@ repeat split;assumption. Qed. \end{coq_example} -\Question{I want to automatize the use of some tactic, how can I do it ?} +\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. @@ -1147,7 +1180,7 @@ 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 ?} +\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} @@ -1160,7 +1193,7 @@ intros... Qed. \end{coq_example} -\Question{How can I do the opposite of the {\intro} tactic ?} +\Question{How can I do the opposite of the {\intro} tactic?} You can use the {\generalize} tactic. @@ -1173,20 +1206,20 @@ 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 ?} +\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 }'' ?} +\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 ?} +\Question{How can I instantiate some metavariable?} Just use the {\instantiate} tactic. -\Question{What is the use of the {\pattern} 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 @@ -1195,7 +1228,7 @@ 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 ?} +\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 @@ -1236,7 +1269,7 @@ is rendered into something like Otherwise said, {\generalize} is not rendered in a forward-reasoning way, while {\assert} is. -\Question{Is there anyway to do pattern matching with dependent types ?} +\Question{Is there anyway to do pattern matching with dependent types?} todo @@ -1245,38 +1278,38 @@ todo -\Question{How can I change the order of the subgoals ?} +\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 ?} +\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 ?} +\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 ?} +\Question{How can I delete some hypothesis?} You can use the {\tt Clear} command. -\Question{How can use a proof which is not finished ?} +\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 ?} +\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 ?} +\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 behaviour when you use a lemma rather than a +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 ?} +\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. @@ -1287,7 +1320,7 @@ a look at the manual for further information. \subsection{General} -\Question{How can I prove that two constructors are different ?} +\Question{How can I prove that two constructors are different?} You can use the {\discriminate} tactic. @@ -1298,7 +1331,7 @@ discriminate. Qed. \end{coq_example} -\Question{During an inductive proof, how to get rid of impossible cases of an inductive definition ?} +\Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?} Use the {\inversion} tactic. @@ -1316,13 +1349,21 @@ trivial but the proof of \coqtt{n+0=n} is not?} Print plus. \end{coq_example} -{\noindent} the expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons +{\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=. \subsection{Recursion} @@ -1402,7 +1443,7 @@ Definition merge := Fix Rwf (fun _ => list nat) merge_step. \end{itemize} -\Question{What is behind these accessibility and well-foundedness proofs?} +\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}. @@ -1512,10 +1553,9 @@ Fixpoint ack (n:nat) : nat -> nat := \subsection{Co-inductive types} -\Question{I have a cofixpoint t:=F(t) and I want to prove t=F(t). What is -the simplest way?} +\Question{I have a cofixpoint $t:=F(t)$ and I want to prove $t=F(t)$. How to do it?} - Just case-expand F(t) then complete by a trivial case analysis. +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} @@ -1541,7 +1581,7 @@ Qed. \section{Syntax and notations} -\Question{I do not want to type ``forall'' because it is too long, what can I do ?} +\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} @@ -1551,7 +1591,7 @@ or if your are using {\CoqIde} you can define a pretty symbol for for all and an -\Question{How can I define a notation for square ?} +\Question{How can I define a notation for square?} You can use for instance : \begin{verbatim} @@ -1564,13 +1604,13 @@ Notation "x $^˛$" := (Rmult x x) (at level 20). 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 ?} +\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 ?} +\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 ! @@ -1582,20 +1622,20 @@ You can do ``Print Grammar constr'', and decode the output from camlp4, good luc %%%%%%% \section{\Ltac} -\Question{What is {\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{Why do I always get the same error message?} -\Question{Is there any printing command in {\Ltac} ?} +\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} ?} +\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} @@ -1608,7 +1648,7 @@ should be added around it. For example: Ltac twoIntro := let x:=intro in (x;x). \end{coq_example} -\Question{What is the syntax for pattern matching in {\Ltac} ?} +\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: @@ -1625,7 +1665,7 @@ end. \end{center} Underscore matches all terms. -\Question{What is the semantics for match goal ?} +\Question{What is the semantics for match goal?} {\tt match goal} matches the current goal against a series of patterns: {$hyp_1 {\ldots} hyp_n$ \textbar- $ccl$}. It uses a @@ -1633,7 +1673,7 @@ first-order unification algorithm, and tries all the possible combinations of $hyp_i$ before dropping the branch and moving to the next one. Underscore matches all terms. -\Question{How can I generate a new name ?} +\Question{How can I generate a new name?} You can use the following syntax : {\tt let id:=fresh in \ldots}\\ @@ -1643,16 +1683,16 @@ Ltac introIdGen := let id:=fresh in intro id. \end{coq_example} -\Question{How can I access the type of a term ?} +\Question{How can I access the type of a term?} You can use typeof. todo -\Question{How can I define static and dynamic code ?} +\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 ?} +\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. @@ -1662,7 +1702,7 @@ You have some examples of tactics written in Ocaml in the ``contrib'' directory \section{Case studies} -\Question{How can I define vectors or lists of size n ?} +\Question{How can I define vectors or lists of size n?} \Question{How to prove that 2 sets are different?} @@ -1792,21 +1832,21 @@ Qed. \section{Publishing tools} -\Question{How can I generate some latex from my development ?} +\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 ?} +\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 generate some dependency graph from my development?} -\Question{How can I cite some {\Coq} in my latex document ?} +\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 ?} +\Question{How can I cite the {\Coq} reference manual?} You can use this bibtex entry : \begin{verbatim} @@ -1820,26 +1860,44 @@ You can use this bibtex entry : } \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} ?} +\Question{What is {\CoqIde}?} -{\CoqIde} is a gtk based gui for \Coq. +{\CoqIde} is a gtk based GUI for \Coq. -\Question{How to enable Emacs keybindings ?} +\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 ?} +\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} +\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} @@ -1851,7 +1909,7 @@ Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident). 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 utf8# from inside +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} @@ -1860,7 +1918,7 @@ To enable these notations automatically start coqide with 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} +\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. @@ -1889,13 +1947,13 @@ Glib.Utf8.from_unichar 0x2200;; do not need . \end{itemize} -\Question{How to build a custom {\CoqIde} with user ml code ?} +\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 ?} +\Question{How to customize the shortcuts for menus?} Two solutions are offered: \begin{itemize} \item Edit \$HOME/.coqide.keys by hand or @@ -1918,15 +1976,15 @@ Glib.Utf8.from_unichar 0x2200;; \section{Extraction} -\Question{What is program extraction ?} +\Question{What is program extraction?} Program extraction consist in generating a program from a constructive proof. -\Question{Which language can I extract to ?} +\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 ?} +\Question{How can I extract an incomplete proof?} You can provide programs for your axioms. @@ -1935,36 +1993,36 @@ You can provide programs for your axioms. %%%%%%% \section{Glossary} -\Question{Can you explain me what an evaluable constant is ?} +\Question{Can you explain me what an evaluable constant is?} An evaluable constant is a constant which is unfoldable. -\Question{What is a goal ?} +\Question{What is a goal?} The goal is the statement to be proved. -\Question{What is a meta variable ?} +\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 ?} +\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 ?} +\Question{What is The Vernacular?} It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots} -\Question{What is a dependent type ?} +\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 ?} +\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 @@ -1976,39 +2034,39 @@ 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 ?} +\Question{What is intuitionistic logic?} This is any logic which does not assume that ``A or not A''. -\Question{What is proof-irrelevance ?} +\Question{What is proof-irrelevance?} See question \ref{proof-irrelevance} -\Question{What is the difference between opaque and transparent ?}{\label{opaque}} +\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 ?} +\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} ?} +\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*)'' ?} +\Question{What can I do if I get ``(*No more subgoals but non-instantiated existential variables*)''?} -\Question{What can I do if I get ``Cannot solve a second-order unification problem'' ?} +\Question{What can I do if I get ``Cannot solve a second-order unification problem''?} You can help {\Coq} using the {\pattern} tactic. @@ -2045,7 +2103,7 @@ again the missing coercion. \section{Conclusion and Farewell.} \label{ccl} -\Question{What if my question isn't answered here ?} +\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 diff --git a/doc/newfaq/main.v001.gif b/doc/newfaq/main.v001.gif Binary files differindex dd8baf8117..e3b012cef7 100644 --- a/doc/newfaq/main.v001.gif +++ b/doc/newfaq/main.v001.gif |
