aboutsummaryrefslogtreecommitdiff
path: root/doc/faq/FAQ.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/faq/FAQ.tex')
-rw-r--r--doc/faq/FAQ.tex275
1 files changed, 175 insertions, 100 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 5a66910722..213fb03137 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.
@@ -503,19 +503,26 @@ $\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$
\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.
+Figure~\ref{fig:axioms} is a summary of the relative strength of these
+axioms, most proofs can be found in directory {\tt Logic} of the standard
+library. (Statements in boldface are the most ``interesting'' ones for
+Coq.) The justification of their validity relies on the interpretability
+in set theory.
+\begin{figure}[htbp]
%HEVEA\imgsrc{axioms.png}
%BEGIN LATEX
+\begin{center}
\ifpdf % si on est en pdflatex
-\includegraphics[width=1.0\textwidth]{axioms.png}
+\scalebox{0.65}{\input{axioms.pdf_t}}
\else
-\includegraphics[width=1.0\textwidth]{axioms.eps}
+\scalebox{0.65}{\input{axioms.eps_t}}
\fi
+\end{center}
%END LATEX
+\caption{The dependency graph of axioms in the Calculus of Inductive Constructions}
+\label{fig:axioms}
+\end{figure}
\Question{What standard axioms are inconsistent with {\Coq}?}
@@ -703,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
@@ -740,19 +747,19 @@ the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).
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 :
+Lemma eq_jdef :
forall x y:nat, intro _ x = intro _ y -> x = y.
Proof.
intros x y H; injection H.
\end{coq_example*}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
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
@@ -834,26 +841,41 @@ mapped to {\Prop}.
Use some theorem or assumption or use the {\split} tactic.
\begin{coq_example}
-Goal forall A B:Prop, A->B-> A/\B.
+Goal forall A B:Prop, A -> B -> A/\B.
intros.
split.
assumption.
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+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:
+If you want to decompose a hypothesis into several hypotheses, you can
+use the {\destruct} tactic:
\begin{coq_example}
-Goal forall A B:Prop, A/\B-> B.
+Goal forall A B:Prop, A/\B -> B.
intros.
-decompose [and] H.
+destruct H as [H1 H2].
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
+You can also perform the destruction at the time of introduction:
+
+\begin{coq_example}
+Goal forall A B:Prop, A/\B -> B.
+intros A B [H1 H2].
+assumption.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is a disjunction, how can I prove it?}
@@ -863,26 +885,28 @@ reasoning step, use the {\tt classic} axiom to prove the right part with the ass
that the left part of the disjunction is false.
\begin{coq_example}
-Goal forall A B:Prop, A-> A\/B.
+Goal forall A B:Prop, A -> A\/B.
intros.
left.
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+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])
+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])
+Ltac classical_left :=
+match goal with
+| _:_ |- _ \/ ?X1 => (elim (classic X1);intro;[right;trivial|left])
end.
@@ -890,8 +914,10 @@ Goal forall A B:Prop, (~A -> B) -> A\/B.
intros.
classical_right.
auto.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is an universally quantified statement, how can I prove it?}
@@ -920,8 +946,10 @@ Goal exists x:nat, forall y, x+y=y.
exists 0.
intros.
auto.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is solvable by some lemma, how can I prove it?}
@@ -939,8 +967,10 @@ Qed.
Goal 3+0 = 3.
apply mylemma.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
@@ -957,8 +987,10 @@ Just use the {\reflexivity} tactic.
Goal forall x, 0+x = x.
intros.
reflexivity.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is a {\tt let x := a in ...}, how can I prove it?}
@@ -972,13 +1004,21 @@ 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?}
+As with conjunctive hypotheses, you can use the {\destruct} tactic or
+the {\intros} tactic to decompose them into several hypotheses.
-\begin{verbatim}
-Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H.
-\end{verbatim}
+\begin{coq_example*}
+Require Import Arith.
+\end{coq_example*}
+\begin{coq_example}
+Goal forall x, (exists y, x * y = 1) -> x = 1.
+intros x [y H].
+apply mult_is_one in H.
+easy.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is an equality, how can I swap the left and right hand terms?}
@@ -989,8 +1029,10 @@ Goal forall x y : nat, x=y -> y=x.
intros.
symmetry.
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My hypothesis is an equality, how can I swap the left and right hand terms?}
@@ -1001,8 +1043,10 @@ Goal forall x y : nat, x=y -> y=x.
intros.
symmetry in H.
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is an equality, how can I prove it by transitivity?}
@@ -1014,8 +1058,10 @@ intros.
transitivity y.
assumption.
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+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?}
@@ -1051,7 +1097,6 @@ 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?}
@@ -1088,8 +1133,10 @@ Use the {\assumption} tactic.
Goal 1=1 -> 1=1.
intro.
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+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?}
@@ -1099,8 +1146,10 @@ Use the {\exact} tactic.
Goal 1=1 -> 1=1 -> 1=1.
intros.
exact H0.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{What can be the difference between applying one hypothesis or another in the context of the last question?}
@@ -1116,8 +1165,10 @@ Just use the {\tauto} tactic.
Goal forall A B:Prop, A-> (A\/B) /\ A.
intros.
tauto.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is a first order formula, how can I prove it?}
@@ -1134,8 +1185,10 @@ Just use the {\congruence} tactic.
Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
intros.
congruence.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?}
@@ -1146,8 +1199,10 @@ Just use the {\congruence} tactic.
Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
intros.
congruence.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?}
@@ -1158,11 +1213,13 @@ Just use the {\ring} tactic.
Require Import ZArith.
Require Ring.
Local Open Scope Z_scope.
-Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b.
+Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b.
intros.
ring.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?}
@@ -1172,30 +1229,30 @@ Just use the {\field} tactic.
Require Import Reals.
Require Ring.
Local Open Scope R_scope.
-Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1.
+Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1.
intros.
field.
-cut (b*a <>0 -> a<>0).
-cut (b*a <>0 -> b<>0).
-auto.
-auto with real.
-auto with real.
-Qed.
+split ; auto with real.
\end{coq_example}
+\begin{coq_example*}
+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}
Require Import ZArith.
Require Omega.
Local Open Scope Z_scope.
-Goal forall a : Z, a>0 -> a+a > a.
+Goal forall a : Z, a>0 -> a+a > a.
intros.
omega.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+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?}
@@ -1218,16 +1275,22 @@ assert (A->C).
intro;apply H0;apply H;assumption.
apply H2.
assumption.
+\end{coq_example}
+\begin{coq_example*}
Qed.
+\end{coq_example*}
+\begin{coq_example}
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}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
@@ -1318,8 +1381,10 @@ H1
*)
intros A B C H H0 H1.
repeat split;assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{I want to automatize the use of some tactic, how can I do it?}
@@ -1332,8 +1397,10 @@ Goal forall A B C : Prop, A -> B/\C -> A/\B/\C.
Proof with assumption.
intros.
split...
-Qed.
\end{coq_example}
+\begin{coq_example*}
+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?}
@@ -1345,8 +1412,10 @@ Local Open Scope Z_scope.
Goal forall a b c : Z, a+b=b+a.
Proof with try solve [ring].
intros...
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{How can I do the opposite of the {\intro} tactic?}
@@ -1358,8 +1427,10 @@ intros.
generalize H.
intro.
auto.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+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?}
@@ -1426,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}
@@ -1465,7 +1536,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.
+You can use the {\tt give\_up} tactic to omit a portion of a proof.
\Question{How can I state a conjecture?}
@@ -1497,8 +1568,10 @@ You can use the {\discriminate} tactic.
Inductive toto : Set := | C1 : toto | C2 : toto.
Goal C1 <> C2.
discriminate.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?}
@@ -1546,20 +1619,20 @@ If you type for instance the following ``definition'':
Reset Initial.
\end{coq_eval}
\begin{coq_example}
-Definition max (n p : nat) := if n <= p then p else n.
+Fail 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,
+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.
@@ -1633,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.
@@ -1714,7 +1787,7 @@ mergesort} as an example).
the arguments of the loop.
\begin{coq_eval}
-Open Scope R_scope.
+Reset Initial.
Require Import List.
\end{coq_eval}
@@ -1727,21 +1800,25 @@ Definition R (a b:list nat) := length a < length b.
\begin{coq_example*}
Lemma Rwf : well_founded R.
\end{coq_example*}
+\begin{coq_eval}
+Admitted.
+\end{coq_eval}
\item Define the step function (which needs proofs that recursive
calls are on smaller arguments).
-\begin{verbatim}
-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 := (* ... *) .
+\begin{coq_example*}
+Definition split (l : list nat)
+ : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}.
+Admitted.
+Definition concat (l1 l2 : list nat) : list nat.
+Admitted.
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{verbatim}
+\end{coq_example*}
\item Define the recursive function by fixpoint on the step function.
@@ -1796,9 +1873,9 @@ induction 1.
inversion 1.
inversion 1. apply IHeven; trivial.
\end{coq_example}
-\begin{coq_eval}
+\begin{coq_example*}
Qed.
-\end{coq_eval}
+\end{coq_example*}
In case the type of the second induction hypothesis is not
dependent, {\tt inversion} can just be replaced by {\tt destruct}.
@@ -1833,10 +1910,10 @@ 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) ->
+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 *)
@@ -1844,9 +1921,9 @@ induction n; [assumption | apply HmS; apply IHn].
(* case Sm *)
intro n; apply HSn; apply IHm.
\end{coq_example}
-\begin{coq_eval}
+\begin{coq_example*}
Qed.
-\end{coq_eval}
+\end{coq_example*}
\Question{How to define a function by nested recursion?}
@@ -1881,7 +1958,7 @@ Set Implicit Arguments.
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 :
+Lemma Stream_unfold :
forall n:nat, nats n = Cons n (nats (S n)).
Proof.
intro;
@@ -1889,8 +1966,10 @@ Proof.
| Cons x s => Cons x s
end).
case (nats n); reflexivity.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
@@ -2325,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?}
@@ -2460,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}.
@@ -2508,8 +2587,8 @@ 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
+A dependent type is a type which depends on some term. For instance
+``vector of size n'' is a dependent type representing all the vectors
of size $n$. Its type depends on $n$
\Question{What is a proof by reflection?}
@@ -2559,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.
@@ -2571,20 +2650,16 @@ eapply eq_trans.
Show Existentials.
eassumption.
assumption.
-Qed.
\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
\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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 15:02:27 +0000