\documentclass{article} \def\jobname{faq.v} \usepackage{hevea} \usepackage{url} \input{./macros.tex} \newcommand{\coqtt}[1]{{\tt #1}} \newcommand{\coqimp}{{$->$}} \newcommand{\coqequiv}{{$<->$}} \newcommand{\question}[1]{ \subsection*{\aname{no:number}{Question:~\sf{#1}}} \addcontentsline{toc}{subsection}{\ahrefloc{no:number}{#1}}} %{\subsubsection{Question:~\sf{#1}}}} \newcommand{\answer}{{\bf Answer:~}} \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} \tableofcontents \section{General} \question{What is {\Coq}?} \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. \question{What are the main applications done in {\Coq}?} \answer Consequent developments include Java certification, safety of cryptographic protocols, medical robotics, constructive and classical analysis, algebraic topology, ... \question{What is the logic of {\Coq}?} \answer {\Coq} is based on an axiom-free type theory called the Calculus of Inductive Constructions (see Coquand \cite{CoHu86} and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order functions and predicates, inductive and co-inductive datatypes and predicates and a stratified hierarchy of sets. \question{Is {\Coq} logic constructive?} \answer {\Coq} theory is constructive, but classical reasoning on proposition can be loaded as an external module. \question{Is {\Coq} about proofs or provability?} \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. \question{Can I define non-terminating programs in {\Coq}?} \answer No, all programs in {\Coq} are terminating. To reason on non-terminating programs, you must turn your program into a terminating one by explicitly giving a bound on the number of iterations of the program. \question{Is {\Coq} a theorem prover?} \answer {\Coq} comes with a few decision procedures (on propositional calculus, Presburger arithmetic, ring and field simplification, resolution, ...) but the main style for proving theorems is by using LCF-style tactics. \question{How is equational reasoning working in {\Coq}?} \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} \question{How can I prove that 2 terms in an inductive sets are equal? Or different?} \answer Cf "Decide Equality" and "Discriminate" in the Reference Manual. \question{Why is the proof of \coqtt{0+n=n} on natural numbers trivial but the proof of \coqtt{n+0=n} is not?} \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{+}. \question{I have two proofs of the same proposition. Can I prove they are equal?} \label{proof-irrelevance} \answer In the base {\Coq} system, the answer is no. However, if classical logic is set, the answer is yes for propositions in {\Prop}. More precisely, the equality of all proofs of a given proposition is called {\em proof-irrelevance}. Proof-irrelevance (in {\Prop}) can be assumed without leading to contradiction in {\Coq}. That classical logic (what can be assumed in {\Coq} by requiring the file \verb=Classical.v=) implies proof-irrelevance is shown in files \verb=ProofIrrelevance.v= and \verb=Berardi.v=. Alternatively, propositional extensionality (i.e. \coqtt{(A \coqequiv B) \coqimp A=B}, defined in \verb=ClassicalFacts.v= ), also implies proof-irrelevance. It is an ongoing work of research to natively include proof irrelevance in {\Coq}. \question{I have two proofs of an equality statement. Can I prove they are equal?} \answer Yes, if equality is decidable on the domain considered (which is the case for {\tt nat}, {\tt bool}, etc): see {\Coq} file \verb=Eqdep_dec.v=). No otherwise, unless assuming Streicher's axiom $K$ (see \cite{HofStr98}) or a more general assumption such as proof-irrelevance (see \ref{proof-irrelevance}) or classical logic. \question{Can I prove that the second components of equal dependent pairs are equal?} \answer The answer is the same as for proofs of equality statements. It is yes if equality on the domain of the first component is decidable, no in the general case. More precisely it is a consequence of Streicher's axiom $K$. \question{What is Streicher's axiom $K$} \label{Streicher} \answer Streicher's axiom $K$ \cite{HofStr98} states that the only proof of a reflexivity statement is a reflexivity proof: \begin{coq_example*} Axiom K: (A:Set)(x:A)(p:x=x)p==(refl_equal ? x). \end{coq_example*} In the general case, axiom $K$ is an independent statement of the Calculus of Inductive Constructions. However, it is true on decidable domains. It is also trivially a consequence of proof-irrelevance (see \ref{proof-irrelevance}) hence of classical logic. Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} which states that \begin{coq_example*} Axiom UIP: (A:Set)(x,y:A)(p1,p2:x=y)p1==p2. \end{coq_example*} Axiom $K$ is also equivalent to the following statements. \begin{coq_example*} Axiom eq_rec_eq : (a:A)(P:A->Set)(p:(P p))(h:a=a) x=(eq_rec A a P p a h). Inductive eq_dep [p:U;x:(P p)] : (q:U)(P q)->Prop := eq_dep_intro : (eq_dep p x p x). Axiom eq_dep_eq : (a:A)(P:A->Set)(p1,p2:(P a))(eq_dep a x a y)->x=y. \end{coq_example*} All of these statements can be found in file \verb=Eqdep.v=. % \subsection{Equality on types} \question{How to prove that 2 sets are differents?} \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 {\tt bool} and {\tt 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*} \question{How to exploit equalities on sets} \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*} Theorem le_le: (m,n:nat){x:nat | (le x m)} = {x:nat | (le x n)} -> m = n. 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). Proof. 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} \question{Can I identify two functions that have the same behaviour (extensionality)?} \answer 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. %\begin{coq_example*} % Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g. %\end{coq_example*} To deal with extensionality, the recommended approach is to define his own 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). \question{Is {\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)?} \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 {\tt (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: {\tt [x:=Type][y:(X;Type)X \coqimp X](z x x)}. \section{Inductive types} \question{What is a "large inductive definition"?} \answer An inductive definition in {\Prop} pr {\Set} 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 encode e.g. Burali-Forti paradox \cite{Gir70,Coq85}. \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*} \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} \question{What is parametric elimination?} \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} %\subsection{Dependent elimination} \question{What means dependent elimination?} \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 {\tt 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 {\tt Elim}, {\tt Induction}, {\tt Destruct} and {\tt Case}, {\tt NewInduction} and {\tt NewDestruct}. % \question{Does the elimination in Prop follows a % different rule than the elimination in Set?} % \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. \question{Why is dependent elimination in Prop not available by default?} \answer This is just because most of the time it is not needed. To derive a dependent elimination principle in Prop, use the command {\tt Scheme} and apply the elimination scheme using the \verb=using= option of \verb=Elim=. %\subsection{Induction} \question{How to perform double induction?} \answer To reason by induction on pairs, just reason by induction on the first component then by case analysis on the second component. Here is an example: \begin{coq_eval} Require Arith. \end{coq_eval} \begin{coq_example} Infix "<" lt (at level 5, no associativity). Infix "<=" le (at level 5, no associativity). Lemma le_or_lt : (n,n0:nat) n0 nat := [m:nat]Cases n m of O _ => O | (S k) O => (S k) | (S k) (S l) => (minus k l) end. Print minus. \end{coq_example} \section{Coinductive types} \question{I have a cofixpoint t:=F(t) and I want to prove t=F(t). What is the simplest way?} \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} \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 well-typed.} \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 {\tt (eqT Type True True)}. This term is printed as {\tt True==True} and re-parsed as {\tt (eqT Prop True True)}. The two terms are not convertible (hence they fool tactics like {\tt Pattern}. 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. \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*} \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*} \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*} \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*} \question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?} \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)}. \bibliographystyle{plain} \bibliography{biblio} \end{document}