FAQ

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

1 files changed, 520 insertions, 0 deletions

diff --git a/doc/faq.tex b/doc/faq.tex
new file mode 100644
index 000000000..93c479d29
--- /dev/null
+++ b/doc/faq.tex
@@ -0,0 +1,520 @@
+\documentclass{article}
+
+\usepackage{hevea}
+\usepackage{url}
+
+\newcommand{\coqtt}[1]{{\tt #1}}
+\newcommand{\coqimp}{{$->$}}
+\newcommand{\coqequiv}{{$<->$}}
+
+\begin{document}
+\urldef{\refman}{\url}{http://coq.inria.fr/doc/main.html}
+
+\begin{center}
+\begin{Large}
+Frequently Asked Questions
+\end{Large}
+\medskip
+Coq version 7
+\end{center}
+
+\section{General}
+
+\paragraph{Question}: What is Coq?
+
+\paragraph{Answer}: Coq is a proof assistant with two main
+application fields: proving program correctness and formalizing mathematical
+theories. Coq offers also automatic extraction of zero-defect programs
+from a proof of their specification.
+
+\paragraph{Question}: What are the main applications done in Coq?
+
+\paragraph{Answer}: ??
+
+\paragraph{Question}: What is the logic of Coq?
+
+\paragraph{Answer}: Coq is based on an axiom-free type theory called
+the Calculus of Inductive Constructions (see Coquand \cite{Coquand--}
+and Coquand--Paulin-Mohring \cite{CoqMoh}). It includes higher-order
+functions and predicates, inductive and co-inductive datatypes,
+inductively and co-inductively defined propositions and a stratified
+hierarchy of sets.
+
+\paragraph{Question}: Is Coq logic constructive?
+
+\paragraph{Answer}: Coq theory is constructive, but classical
+reasoning on proposition can be loaded as an external module.
+
+\paragraph{Question}: Is Coq about proofs or provability?
+
+\paragraph{Answer}: Coq is definitely about proofs. A statement
+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.
+
+\paragraph{Question}: Can I define non-terminating program in Coq?
+
+\paragraph{Answer}: No, all programs in Coq are terminating. To
+reason on non-terminating programs, you must turn your program into a
+terminating one by giving a bound on ``time'' as an extra parameter.
+
+\paragraph{Question}: Is Coq a theorem prover?
+
+\paragraph{Answer}: Coq comes with a few decision procedures (on
+propositional calculus, Presburger arithmetic, ring simplification,
+resolution based on first-order matching, ...) but the main style for
+proving theorems is by using LCF-style tactics.
+
+\paragraph{Question}: How is equational reasoning working in Coq?
+
+\paragraph{Answer}: Coq is reasoning modulo sequential evaluation of
+(not necessarily closed) programs (it is decidable because Coq
+programs are terminating). This equality is called {\em conversion}.
+Besides conversion, equations are to be treated by hand or using
+specialized tactics (e.g. simplifications on fields).
+
+\section{Equality}
+
+\subsection{Equality on Terms}
+
+\paragraph{Question}: How can I prove that 2 terms in an inductive sets are equal? Or different?
+
+\paragraph{Answer}: Cf "Decide Equality" and "Discriminate" in the Reference Manual.
+
+\paragraph{Question}: Why is the proof of \coqtt{0+n=n} on natural numbers
+trivial but the proof of \coqtt{n+0=n} is not?
+
+\paragraph{Answer}: Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument
+
+\begin{coq_example}
+Print plus.
+\end{coq_example}
+
+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{+}.
+
+\paragraph{Question}: I have two proofs of the same proposition. Can I prove they are equal?
+
+\paragraph{Answer}: Let's consider two cases.
+
+  1) These are two proofs of the equality, say of $x$ and $y$. We could
+  think these proofs are equal since equality is inductively defined
+  and the only possible proof of an equality is \verb=refl_equal=:
+
+\begin{coq_example*}
+Theorem only_one_proof_of_an_equality : (x,y:A)(p1,p2:(x=y))p1=p2.
+\end{coq_example*}
+
+  If equality on A is decidable, which is the case for most inductive
+  sets: nat, list, ... and for some inductive predicates: le, lt, ,
+  then it is provable. But this is not provable in the general
+  case. Effectively, it is known from Streicher [1995] that the
+  statement is independent of Coq, that is there are models of Coq
+  (actually of the Calculus of Constructions without inductive types)
+  which invalidates it.
+
+  2) More generally, if B is an arbitrary proposition and b1, b2 are
+  two proofs of B, it is not provable that b1=b2.
+
+  More precisely, the fact this is always provable is known as
+  proof-irrelevance. Proof-irrelevance (in Prop) can be assumed
+  without leading to contradiction in Coq. Especially,
+  proof-irrelevance limited to the propositional world does not break
+  the computational interpretation of the Set level.
+
+  Alternatively, assuming classical logic (what can be done in Coq
+  by requiring the file \verb=Classical.v=) also implies
+  proof-irrelevance (as shown in file \verb=Berardi.v=)
+
+  Alternatively again, assuming propositional extensionality (that is
+  \coqtt{(A \coqequiv B) \coqimp A=B}), also implies proof-irrelevance.
+
+\subsection{Equality on types}
+
+\paragraph{Question}: How to prove that 2 sets are differents?
+
+\paragraph{Answer}: You need to find a property true on one set and false on
+the other one. As an example we show how to prove that bool and nat are
+discriminable. As discrimination property we take the property to have
+no more than 2 elements.
+
+\begin{coq_example*}
+Theorem nat_bool_discr : ~bool==nat.
+Proof.
+  Pose discr := [X:Set]~(a,b:X)~(x:X)~x=a->~x=b->False.
+  Intro Heq; Assert H : (discr bool).
+    Intro H; Apply (H true false); NewDestruct x; Auto.
+  Rewrite Heq in H; Apply H; Clear H.
+  NewDestruct a; NewDestruct b; Intro H0; EAuto.
+  NewDestruct n; [Apply (H0 (S (S O))); Discriminate | EAuto].
+Qed.
+\end{coq_example*}
+
+\paragraph{Question}: How to exploit equalities on sets
+
+\paragraph{Answer}: To extract information from an equality on sets, you need to find a
+predicate satisfied by the elements of the sets. As an example we show
+the following theorem.
+
+\begin{coq_example*}
+Inductive discr_int_n [n:nat;X:Set] : Prop :=
+  intro : (fst:X->nat)(snd:(x:X)(le (fst x) n))
+            ((x,y:X)(exist ? [z](le z n) (fst x) (snd x))=
+                (exist ? [z](le z n) (fst y) (snd y))->x=y)
+          -> (discr_int_n n X).
+
+Theorem le_le: (m,n:nat){x:nat | (le x m)} = {x:nat | (le x n)} -> m = n.
+Intros.
+Assert Hdiscr : (discr_int_n m {x:nat | (le x m)}).
+Split with (proj1_sig nat [x:?](le x m)) (proj2_sig nat [x:?](le x m)).
+NewDestruct x; NewDestruct y.
+Exact [x:?]x.
+Rewrite H in Hdiscr.
+Elim Hdiscr.
+Assert H1:=(snd (exist nat [z](le z (S n)) (S n) (le_n (S n)))).
+...
+\end{coq_example*}
+
+\section{Axioms}
+
+\paragraph{Question}: Can I identify two functions that have the same behaviour?
+
+\paragraph{Answer}: This is known as extensionality of equality
+between functions.
+
+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.
+
+However, from a logical point of view, equality can be made
+extensional without breaking the consistency (see [??]). This is
+achieved by adding the following axiom to our theory:
+
+\begin{coq_example*}
+  Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g.
+\end{coq_example*}
+
+Rather than adding an axiom, a better approach could be to define
+its one extensional equality on $A \rightarrow B$:
+
+\begin{coq_example*}
+  Definition ext_eq [f,g:A->B] := (x:A)(f x)=(g x).
+\end{coq_example*}
+
+and to reason on $A \rightarrow B$ as a setoid (see the Chapter on Setoids in the
+Reference Manual).
+
+
+\paragraph{Question}: Can I identify the different proofs of a proposition?
+
+\paragraph{Answer}: Yes, this is known as proof-irrelevance and it is consistent with
+the core theory of Coq. See also section "Equality on terms".
+
+
+\paragraph{Question}: Is \coqtt{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) ?
+
+\paragraph{Answer}: 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 [cf Girard 1972, Coquand
+1991, Hurkens 1993, Miquel 2001].
+
+  For instance, when the user see {\tt (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 {\coqtt
+(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: {\coqtt [x:=Type][y:(X;Type)X \coqimp X](z x x)}.
+
+\section{Inductive types}
+
+\paragraph{Question}: What is a "large inductive definition"?
+
+\paragraph{Answer}: An inductive definition is called large if its constructors embed
+sets or propositions. As an example, here is a large inductive type:
+
+\begin{coq_example*}
+  Inductive sigST [P:Set->Set] : Set
+      := existST : (X:Set)(P X) -> (sigST P).
+\end{coq_example*}
+
+   Large inductive definition have restricted elimination scheme to
+prevent inconsistencies. Especially, projecting the set or the
+proposition content of a large inductive definition is forbidden. If
+it were allowed, we could be able to construct the set of all sets
+equipped with a well-founded relation and show that this sets is
+itself equipped with a well-founded relation, leading to a
+contradiction (this is Burali-Forti paradox).
+
+
+\paragraph{Question}: Why Injection does not work on impredicative types? E.g. in this case:
+
+\begin{coq_example*}
+  Inductive I : Set := intro : (k:Set)k -> I.
+  Lemma eq_jdef : (x,y:nat) (intro ? x)=(intro ? y) -> x=y.
+  Intros x y H; Injection H.
+\end{coq_example*}
+
+\paragraph{Answer}: 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
+Burali-Forti paradox). The question remains open whether injectivity
+is consistent on some large inductive types not expressive enough to
+encode known paradoxes (such as type I above).
+
+\section{Elimination, Case Analysis and Induction}
+
+\subsection{Parametric elimination}
+
+\paragraph{Question}: What is parametric elimination?
+
+\paragraph{Answer}: Parametric elimination is a 
+generalisation of the substitutivity of equality. Only inductive types
+with non-constant parameters are concerned with this kind of dependent
+elimination. Typical examples of inductive types enjoying parametric
+elimination in Coq standard library are the equality predicate
+\verb=eq= and the less than predicate on natural numbers \verb=le=.
+
+\begin{coq_example*}
+Print eq.
+Print le.
+\end{coq_example*}
+
+\begin{coq_example*}
+Inductive le [n,m] : nat]  : nat->Prop :=
+      le_n : n=m->(le n m) | le_S : (p:nat)(le n p)->(le n (S p))
+\end{coq_example*}
+
+Assuming equality defined, all other kind of parametric elimination
+can be expressed using equality. For instance, parametric
+elimination of \verb=le= can be restated as:
+
+\begin{verbatim}
+le_ind: (n:nat; n0:nat; P:(nat->Prop))
+        (n=n0->(P n0))
+        ->((m:nat)(le n m)->(P m)->n0=(S m)->(P n0))
+        ->(le n n0)->(P n0)
+\end{verbatim}
+
+\subsection{Dependent elimination}
+
+\paragraph{Question}: What means dependent elimination?
+
+\paragraph{Answer}: Dependent elimination is a generalisation of the
+standard Peano's induction principle on natural numbers.  This
+elimination asserts that to prove a property P on say the set nat of
+natural numbers, it is enough to prove the property on O and to prove
+it on successor numbers. Combined with fixpoints, this directly
+provides with usual Peano's induction scheme.
+
+Non dependent elimination is when elimination is used to build an
+object whose type does not depend on the eliminated object. An example
+of non dependent elimination is recursion, or the simpler form of
+{\coqtt if $\ldots$ then $\ldots$ else}.
+
+The relevant tactics to deal with this kind of elimination are Elim,
+Induction, Destruct and Case.
+
+
+% \paragraph{Question}: Does the elimination in Prop follows a
+%   different rule than the elimination in Set?
+
+% \paragraph{Answer}: There are two kinds of dependent case analysis. The result type of a
+% case analysis may depend on the matched object (this is what is
+% usually intended by dependent) but may also depend on the non-constant
+% arguments of the type of the matched object without being dependent of
+% the object itself.
+
+%   This is typically what happens in a proof using equality. The result
+% does not depend on the proof of the equality itself but crucially
+% depends on the second compared argument of the equality.
+
+%   It happens that proofs using elimination (i.e. case analysis or
+% induction) on objects at the Set level are usually dependent on the
+% matched term. This is because propositions precisely depend on the
+% object on which an induction or case analysis is applied. Conversely,
+% it happens that proofs using elimination on objects at the Prop level
+% (typically elimination on equality proofs) are usually not dependent
+% on the matched object. This is because proofs usually stay at the
+% proof level and a few developments are stating things about proofs.
+% But, again, to be not dependent on the matched objet does not mean not
+% dependent at all. For equality, dependency on the second compared
+% argument is precisely what provides with the substitutivity schema of
+% equality.
+
+\paragraph{Question}: Why is dependent elimination in Prop not
+available by default.
+
+\paragraph{Answer}: 
+This is just because most of the time it is not needed. To derive a
+dependent elimination principle in Prop, use the command Scheme and
+apply the elimination scheme using the \verb=with= option of
+\verb=Elim=.
+
+
+
+\subsection{Induction}
+
+\paragraph{Question}: How to perform double induction?
+
+\paragraph{Answer}: To reason by induction on pairs, just reason by induction on the first component the by case analysis on the second component. Here is an example:
+
+\begin{coq_example}
+Lemma le_or_lt : (n,n0:nat) n0<n \/ n<=n0.
+NewInduction n; NewDestruct n0; Auto with arith.
+NewDestruct (IHn n0); Auto with arith.
+\end{coq_example}
+
+\paragraph{Question}: How to define a function by recursion on 2 arguments?
+
+\paragraph{Answer}: The same trick applies, except that you need to write by hand the nesting of two fixpoint combinators. Here is an example:
+
+\begin{coq_example}
+TODO
+\end{coq_example}
+
+
+\section{Coinductive types}
+
+\paragraph{Question}: I have a cofixpoint t:=F(t) and I want to prove t=F(t). What is
+the simplest way?
+
+\paragraph{Answer}: Just case-expand F(t) then complete by a trivial case analysis.
+Here is what it gives on e.g. the type of streams on naturals
+
+\begin{coq_example}
+  Set Implicit Arguments.
+  CoInductive Stream [A : Set]  : Set := Cons : A->(Stream A)->(Stream A)
+  CoFixpoint nats : nat -> (Stream nat) := [n](Cons n (nats (S n))).
+
+  Lemma Stream_unfold : (n:nat)(nats n)= (Cons n (nats (S n))).
+  Proof.
+    Intro; Change (nats n) = (Cases (nats n) of (Cons x s) => (Cons x s) end).
+    Case (nats n); Reflexivity.
+  Qed.
+\end{coq_example}
+
+\section{Miscellaneous}
+
+\paragraph{Question}: I copy-paste a term and Coq says it is not convertible
+to the original term. Sometimes it even say the copied term is not
+well-typed.
+
+\paragraph{Answer}: This is probably due to invisible implicit information (implicit
+arguments, coercions and Cases annotations) in the printed term, which
+is not re-synthetized from the copied-pasted term in the same way as
+it is in the original term.
+
+  Consider for instance (eqT Type True True). This term is printed as
+True==True and re-parsed as (eqT Prop True True). Both are not
+convertible and, e.g. Pattern and LetTac are beaten by that.
+
+  There is currently no satisfactory answer to the problem.
+ 
+  Due to coercions, one may even face type-checking errors. In some
+rare cases, the criterion to hide coercions is a bit too loosy, which
+may result in a typing error message if the parser is not able to find
+again the missing coercion.
+
+\paragraph{Question}: I have a problem of dependent elimination on
+proofs, how to solve it?
+
+\begin{coq_example*}
+Inductive Def1 : Set
+   := c1 : Def1.
+
+Inductive DefProp : Def1 -> Set
+   := c2 : (d:Def1)(DefProp d).
+
+Inductive Comb : Set
+   := c3 : (d:Def1)(DefProp d) -> Comb.
+
+Lemma eq_comb
+   : (d1,d1':Def1; d2:(DefProp d1); d2':(DefProp d1')) d1=d1' ->
+     (c3 d1 d2)=(c3 d1' d2').
+\end{coq_example*}
+
+\paragraph{Answer}: You need to derive the dependent elimination
+scheme for DefProp by hand using {\coqtt Scheme}.
+
+\begin{coq_example*}
+Scheme DefProp_elim := Induction for DefProp Sort Prop.
+
+Lemma eq_comb
+   : (d1,d1':Def1)d1=d1'->(d2:(DefProp d1); d2':(DefProp d1'))
+     (c3 d1 d2)=(c3 d1' d2').
+Intros.
+NewDestruct H.
+NewDestruct d2 using DefProp_elim.
+NewDestruct d2' using DefProp_elim.
+Reflexivity.
+Qed.
+\end{coq_example*}
+
+\paragraph{Question}: And what if I want to prove the following?
+
+\begin{coq_example*}
+Inductive natProp : nat -> Prop
+   := p0 : (natProp O)
+   |  pS : (n:nat)(natProp n) -> (natProp (S n)).
+
+Inductive package : Set
+   := pack : (n:nat)(natProp n) -> package.
+
+Lemma eq_pack
+   : (n,n':nat)
+     n=n' ->
+     (np:(natProp n); np':(natProp n'))
+     (pack n np)=(pack n' np').
+\end{coq_example*}
+
+\paragraph{Answer}:
+
+\begin{coq_example*}
+Scheme natProp_elim := Induction for natProp Sort Prop.
+
+Definition pack_S : package -> package. 
+NewDestruct 1.
+Apply (pack (S n)).
+Apply pS; Assumption.
+Defined.
+
+Lemma eq_pack
+   : (n:nat)
+     (np:(natProp n))(n':nat)( np':(natProp n'))
+     n=n' -> 
+     (pack n np)=(pack n' np').
+Intros n np.
+Elim np using natProp_elim.
+Intros n' np'; Elim np' using natProp_elim; Intros; Auto. 
+Discriminate H0.
+Intros n0 np0 Hrec n' np'; Elim np' using natProp_elim; Intros; Auto. 
+Discriminate H.
+Change (pack_S (pack n0 np0))=(pack_S (pack n1 n2)).
+Apply (f_equal package).
+Apply Hrec.
+Auto.
+Qed.
+\end{coq_example*}
+
+\paragraph{Question}: Why does Coq tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}
+
+\paragraph{Answer}:
+
+This is because \texttt{\{x:A|(P x)\}} is a notation for \texttt{(sig A [x:A](p x))}. Since Coq does not reason up to $\eta$-conversion, this is different from
+\texttt{(sig A P)}.
+
+\end{document}