diff options
Diffstat (limited to 'doc/faq/FAQ.tex')
| -rw-r--r-- | doc/faq/FAQ.tex | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index fbb866e87..48b61827d 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -228,7 +228,7 @@ 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 +(no object, no label ...), so that it is highly improbable 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. @@ -710,7 +710,7 @@ 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 +\ref{le-uniqueness} an axiom-free proof of the uniqueness 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 @@ -1497,7 +1497,7 @@ 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}. +You can state explicitly what this implicit argument is. See \ref{implicit}. \Question{How can I explicit some implicit argument ?}\label{implicit} @@ -1625,14 +1625,14 @@ Fail Definition max (n p : nat) := if n <= p then p else n. 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, +proven theorems. 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$. +$n$ and $p$, determines whether $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. @@ -1706,7 +1706,7 @@ immediate, whereas one can't wait for the result of 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$ +function}, i.e. a complex object, able not only to tell whether $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. @@ -2404,8 +2404,8 @@ You can use {\tt coqdoc}. \Question{How can I generate some dependency graph from my development?} -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/). +You can use the tool \verb|coqgraph| developed by Philippe Audebaud in 2002. +This tool transforms dependencies 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?} @@ -2539,7 +2539,7 @@ modifiers keys available through GTK. The straightest way to get rid of the problem is to edit by hand your coqiderc (either \verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\ \verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) - and replace any occurence of \texttt{MOD4} by \texttt{MOD1}. +and replace any occurrence of \texttt{MOD4} by \texttt{MOD1}. @@ -2638,7 +2638,7 @@ existential variable which eventually got erased by some computation. You may backtrack to the faulty occurrence of {\eauto} or {\eapply} and give the missing argument an explicit value. Alternatively, you can use the commands \texttt{Show Existentials.} and -\texttt{Existential.} to display and instantiate the remainig +\texttt{Existential.} to display and instantiate the remaining existential variables. |