diff options
-rw-r--r-- | doc/faq/FAQ.tex | 41 |
1 files changed, 25 insertions, 16 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index a21de8f24..4309926b9 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -286,6 +286,8 @@ There are graphical user interfaces: \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. +\item[ProofWeb] The ProofWeb online web interface for {\Coq} (and other proof assistants), with a focus on teaching. +\item[ProverEditor] is an experimental Eclipse plugin with support for {\Coq}. \end{description} There are documentation and browsing tools: @@ -294,6 +296,7 @@ There are documentation and browsing tools: \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. +\item[coqgraph] A tool to generate a dependency graph from {\Coq} sources. \end{description} There are front-ends for specific languages: @@ -304,6 +307,9 @@ There are front-ends for specific languages: \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. +\item[Concoqtion] is a dependently-typed extension of Objective Caml (and of MetaOCaml) with specifications expressed and proved in Coq. +\item[Ynot] is an extension of Coq providing a "Hoare Type Theory" for specifying higher-order, imperative and concurrent programs. +\item[Ott]is a tool to translate the descriptions of the syntax and semantics of programming languages to the syntax of Coq, or of other provers. \end{description} \Question{What are the high-level tactics of \Coq} @@ -369,7 +375,7 @@ This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{ht \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}. +sections that are missing). Please send contributions to Coq-Club. \Question{Is there any mailing list about {\Coq}?} The main {\Coq} mailing list is \url{coq-club@pauillac.inria.fr}, which @@ -1124,7 +1130,11 @@ Open Local Scope R_scope. Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. intros. field. -assumption. +cut (b*a <>0 -> a<>0). +cut (b*a <>0 -> b<>0). +auto. +auto with real. +auto with real. Qed. \end{coq_example} @@ -1204,13 +1214,9 @@ Perhaps you may need to use \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 use \texttt{info }{\auto} to replace {\auto} by the tactics it generates. You can split your hint bases into smaller ones. @@ -1416,6 +1422,7 @@ 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. +You can use the {\tt admit} tactic to omit a portion of a proof. \Question{How can I state a conjecture?} @@ -1892,9 +1899,6 @@ You can do ``Print Grammar constr'', and decode the output from camlp4, good luc {\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 @@ -1971,7 +1975,9 @@ You can use typeof. todo \fi +\iffalse \Question{How can I define static and dynamic code?} +\fi \section{Tactics written in Ocaml} @@ -1984,8 +1990,10 @@ You have some examples of tactics written in Ocaml in the ``contrib'' directory \section{Case studies} - +\iffalse \Question{How can I define vectors or lists of size n?} +\fi + \Question{How to prove that 2 sets are different?} @@ -2204,7 +2212,8 @@ You can use {\tt coqdoc}. \Question{How can I generate some dependency graph from my development?} -You can use {\tt coq\_tex}. +You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002. +This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/). \Question{How can I cite some {\Coq} in my latex document?} @@ -2218,8 +2227,8 @@ You can use this bibtex entry: title = {The Coq proof assistant reference manual}, author = {\mbox{The Coq development team}}, organization = {LogiCal Project}, - note = {Version 8.0}, - year = {2004}, + note = {Version 8.2}, + year = {2009}, url = "http://coq.inria.fr" } \end{verbatim} @@ -2417,7 +2426,7 @@ 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 +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. @@ -2446,7 +2455,7 @@ 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 +The initial state corresponds to the state of \texttt{coqtop} when the interactive session began. It does not make sense in files to compile. |