*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8523 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 53 insertions, 17 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 3102302b96..3aabb98416 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -51,6 +51,7 @@
 \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 }}
@@ -58,6 +59,7 @@
 \def\reflexivity{{\tt reflexivity }}
 \def\transitivity{{\tt transitivity }}
 \def\symmetry{{\tt symmetry }}
+\def\Focus{{\tt Focus }}
 
 
 \begin{document}
@@ -75,9 +77,9 @@
 %%%%%%%
 
 \begin{abstract}
-This note intends to provide an easy way to get aquainted with the
+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 newcommers will face, and to give
+to some of the questions any newcomers will face, and to give
 pointers to other references when possible.
 \end{abstract}
 
@@ -115,9 +117,9 @@ The Coq tool is a proof assistant which:
 Coq is written in the Objective Caml language and uses the Camlp4 Pre-processor-pretty-printer for Objective Caml.
 
 \Question[name]{Did you really need to name it like that ?}
-Some french computer scientists have a tradition of naming their
+Some French computer scientists have a tradition of naming their
 software as animal species: Caml, Elan, Foc or Krakatoa are examples
-of this tacit convention. In french, ``coq'' means rooster, and it
+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.
 
@@ -149,7 +151,7 @@ Eduardo Giménez' thesis~\cite{EGThese}
 
 You can either extract a program from a proof use the extraction
 mechanism or use dedicated tools, such as \Why and \Krakatoa, to prove
-annotated programs written in other langages.
+annotated programs written in other languages.
 
 \Question[nbusers]{How many \Coq users are there ?}
 
@@ -184,7 +186,7 @@ Coq is used by Trusted Logic to prove properties of the JavaCard system.
 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 
 \url{http://pauillac.inria.fr/coq/doc-eng.html}.
-All these documents are viewable either in browsable html, or as
+All these documents are viewable either in browsable HTML, or as
 downloadable postscripts.
 
 \Question[coqfaq]{Where can I find this faq on the web ?}
@@ -236,8 +238,8 @@ You can use the web interface at \url{http://coq.inria.fr/bin/coq-bugs}.
 
 \section{Installation}
 
-\Question[coqlicence]{What is the licence of \Coq ?}
-It is distributed under the GNU Lesser General Licence (LGPL).
+\Question[coqlicence]{What is the license of \Coq ?}
+It is distributed under the GNU Lesser General License (LGPL).
 
 \Question[coqsources]{Where can I find the sources of \Coq ?}
 The sources of \Coq can be found online in the tar.gz'ed packages
@@ -272,7 +274,7 @@ Qed.
 
 \Question[conjonctionhyp]{My goal contains a conjunction as an hypothesis, how can I use it ?}
 
-If you want to decompose your hypohtesis into other hypothesis you can use the \decompose tactic :
+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.
@@ -436,6 +438,22 @@ Qed.
 \end{coq_example}
 
 
+\Question[letgoal]{My goal is a {\tt let}, how can I prove it ?}
+
+Just use the \destruct or \case tactics.
+
+
+\Question[existentialhyp]{My goal contains some existancial hypotheses, how can I use it ?}
+
+You can use the tactic \elim with you hypotheses as an argument.
+
+\Question[existentialhypdecomp]{My goal contains some existancial 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[symmetry]{My goal is an equality, how can I swap the left and right hand terms ?}
 
 Just use the \symmetry tactic.
@@ -489,7 +507,7 @@ exact H0.
 Qed.
 \end{coq_example}
 
-\Question[assumption2bis]{What can be the difference between applying one hypothese or another in the context of the last question ?}
+\Question[assumption2bis]{What can be the difference between applying one hypotheses 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 hyphoteses can lead to different programs.
 
@@ -525,8 +543,8 @@ You can use the \case or \destruct tactics.
 \Question[namedintros]{Why should I name my intros ?}
 
 When you use the \intro tactic you don't have to give a name to your
-hyphothesis. If you do so the names will be generated by \Coq but your
-scripts won't be modular. If you add some hyphothesis to your theorem
+hypothesis. If you do so the names will be generated by \Coq but your
+scripts won't be modular. 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.
 
@@ -541,6 +559,13 @@ 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.
 
+\Question[assertback]{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 \elim followed by \intro or you can use the following \Ltac command :
+\begin{verbatim}
+Ltac assert_later t := cut t;[intro|idtac]. 
+\end{verbatim}
+
 
 \Question[proofwith]{I want to automatize the use of some tactic how can I do it ?}
 
@@ -576,6 +601,8 @@ Qed.
 
 \Question[subgoalsorder]{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[hyphotesisorder]{How can I change the order of the hypothesis ?}
 
@@ -706,11 +733,11 @@ that is still unknown.
 \Question[reflection]{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
+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
+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.
@@ -723,22 +750,31 @@ and the last chapter of the Coq'Art.
 
 \Question[coqlatex]{How can I generate some latex from my development ?}
 
+You can use {\tt coqdoc}.
+
 \Question[coqhtml]{How can I generate some HTML from my development ?}
 
-\Question[depgraph]{How can I generate some dependancy graph from my development ?}
+You can use {\tt coqdoc}.
+
+\Question[depgraph]{How can I generate some dependency graph from my development ?}
+
+
 
 \Question[coqtex]{How can I cite some \Coq in my latex document ?}
 
+You can use {\tt coq\_tex}.
 
 \section{CoqIde}
 
 \Question[coqidedescr]{What is \CoqIde ?}
 
+\CoqIde is a gtk based gui for \Coq.
+
 \section{Extraction}
 
 \Question[extraction]{What is program extraction ?}
 
-Program extraction consist in generating a prgram from a constructive proof.
+Program extraction consist in generating a program from a constructive proof.
 
 \Question[extraclang]{Which language can I extract to ?}