\documentclass{article} \usepackage{fullpage} \usepackage{hevea} \usepackage{url} \input{./macros.tex} \newcommand{\coqtt}[1]{{\tt #1}} \newcommand{\coqimp}{{\mbox{\tt ->}}} \newcommand{\coqequiv}{{\mbox{\tt <->}}} \newcommand{\question}[1]{ \subsection*{\aname{no:number}{Question:~\sf{#1}}} \addcontentsline{toc}{subsection}{\ahrefloc{no:number}{#1}} \addcontentsline{htoc}{subsection}{\ahrefloc{no:number}{#1}}} %{\subsubsection{Question:~\sf{#1}}}} \newcommand{\answer}{{\bf Answer:~}} \newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}} \begin{document} \urldef{\refman}{\url}{http://coq.inria.fr/doc/main.html} \urldef{\InitWf}{\url} {http://coq.inria.fr/library/Coq.Init.Wf.html} \urldef{\LogicBerardi}{\url} {http://coq.inria.fr/library/Coq.Logic.Berardi.html} \urldef{\LogicClassical}{\url} {http://coq.inria.fr/library/Coq.Logic.Classical.html} \urldef{\LogicClassicalFacts}{\url} {http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html} \urldef{\LogicProofIrrelevance}{\url} {http://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html} \urldef{\LogicEqdep}{\url} {http://coq.inria.fr/library/Coq.Logic.Eqdep.html} \urldef{\LogicEqdepDec}{\url} {http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html} \begin{center} \begin{Large} Frequently Asked Questions \end{Large} \medskip {\Coq} version 8 \end{center} \tableofcontents \section{General} \question{What is {\Coq}?} \answer {\Coq} is a proof assistant with two main application fields: proving program correctness and formalising mathematical theories. {\Coq} offers also automatic extraction of zero-defect programs from a proof of their specification. \question{How to use {\Coq}?} \answer{{\Coq} offers a development environment in which you can alternatively define predicates, functions or sets and state claims to be interactively proved. {\Coq} comes with a large library of predefined notions both from the standard mathematical background (natural, integer and real numbers, sets and relations, ...) and from the standard computer science background (lists, binary numbers, finite sets, dictionaries, ...). {\Coq} comes with a graphical interface. \question{What are the main applications done in {\Coq}?} \answer Largest developments are Java certification, safety of cryptographic protocols, advanced 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}'s logic intuitionistic or classical?} \answer {\Coq} theory is basically intuitionistic (i.e. excluded-middle $A\lor\neg A$ is not granted by default) with the possibility to reason classically on demand by requiring an optional module stating $A\lor\neg A$. \question{What's the status of proofs in {\Coq}} \answer {\Coq} proofs are build with tactics allowing both forward reasoning (stating 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. Especially, loops must come with an evidence of their termination. \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 interactively by using LCF-style tactics. \question{How is equational reasoning working in {\Coq}?} \answer {\Coq} comes with an internal notion of computation called {\em conversion} (e.g. $(x+1)+y$ is internally equivalent to $(x+y)+1$; similarly applying argument $a$ to a function mapping $x$ to some expression $t$ converts to the expression $t$ where $x$ is replaced by $a$). This notion of conversion (which is decidable because {\Coq} programs are terminating) covers a certain part of equational reasoning but is limited to sequential evaluation of expressions of (not necessarily closed) programs. Besides conversion, equations have to be treated by hand or using specialised tactics. \question{What are the high-level tactics of {\Coq}} \begin{itemize} \item Decision of quantifier-free Presburger's Arithmetic \item Simplification of expressions on rings and fields \item Decision of closed systems of equations \item Semi-decision of first-order logic \item Prolog-style proof search, possibly involving equalities \end{itemize} \question{What are the main libraries of {\Coq}} \begin{itemize} \item Basic Peano's arithmetic \item Binary integer numbers \item Real analysis \item Libraries for lists, boolean, maps. \item Libraries for relations, sets \end{itemize} \section{Equality} %\subsection{Equality on Terms} \question{How can I prove that 2 terms in an inductive set are equal? Or different?} \answer Cf "Decide Equality" and "Discriminate" in the \ahref{\refman}{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} \noindent 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 \vfile{\LogicClassical}{Classical}) implies proof-irrelevance is shown in files \vfile{\LogicProofIrrelevance}{ProofIrrelevance} and \vfile{\LogicBerardi}{Berardi}. Alternatively, propositional extensionality (i.e. \coqtt{(A \coqequiv B) \coqimp A=B}, defined in \vfile{\LogicClassicalFacts}{ClassicalFacts}), also implies proof-irrelevance. % It is an ongoing work of research to natively include proof % irrelevance in {\Coq}. \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 provable if equality on the domain of the first component is decidable (look at \verb=inj_right_pair= from file \vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general case. However, it is consistent (with the Calculus of Constructions) to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually provides an axiom (equivalent to Streicher's axiom $K$) which entails the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}). \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{What is Streicher's axiom $K$} \label{Streicher} \answer Streicher's axiom $K$ \cite{HofStr98} asserts dependent elimination of reflexive equality proofs. \begin{coq_example*} Axiom Streicher_K : forall (A:Type) (x:A) (P: x=x -> Prop), P (refl_equal x) -> forall p: x=x, P p. \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 (see file \vfile{\LogicEqdepDec}{Eqdep\_dec}). 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} \cite{HofStr98} which states that \begin{coq_example*} Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2. \end{coq_example*} Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98} \begin{coq_example*} Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x. \end{coq_example*} Axiom $K$ is also equivalent to \begin{coq_example*} Axiom eq_rec_eq : forall (A:Set) (x:A) (P: A->Set) (p:P x) (h: x=x), p = eq_rect x P p x h. \end{coq_example*} It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs). \begin{coq_example*} Inductive eq_dep (U:Set) (P:U -> Set) (p:U) (x:P p) : forall q:U, P q -> Prop := eq_dep_intro : eq_dep U P p x p x. Axiom eq_dep_eq : forall (U:Set) (u:U) (P:U -> Set) (p1 p2:P u), eq_dep U P u p1 u p2 -> p1 = p2. \end{coq_example*} All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}. % \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 := fun X:Set => ~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))). intro Heq; assert (H: discr bool). intro H; apply (H true false); destruct x; auto. rewrite Heq in H; apply H; clear H. destruct a; destruct b as [|n]; intro H0; eauto. destruct n; [ apply (H0 2); 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 of sets satisfied by the elements of the sets. As an example, let's consider the following theorem. \begin{coq_example*} Theorem le_le : forall m n:nat, {x : nat | x <= m} = {x : nat | x <= n} -> m = n. \end{coq_example*} A typical property is to have cardinality $n$. \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*} Let {\tt A}, {\tt B} be types. To deal with extensionality on \verb=A->B=, the recommended approach is to define his own extensional equality on \verb=A->B=. \begin{coq_eval} Variables A B : Set. \end{coq_eval} \begin{coq_example*} Definition ext_eq (f g: A->B) := forall x:A, f x = g x. \end{coq_example*} and to reason on \verb=A->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 [Girard 1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding can be found in file {\tt Logic/Hurkens.v} of {\Coq} standard library. For instance, when the user see {\tt forall (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 forall 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 fun (x:Type) (y:forall 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) : Type := existST : forall X:Set, P X -> sigST P. \end{coq_example*} In the {\tt Set} impredicative variant of {\Coq}, large inductive definitions in {\tt Set} have restricted elimination schemes to prevent inconsistencies. Especially, projecting the set or the proposition content of a large inductive definition is forbidden. If it were allowed, it would be possible to encode e.g. Burali-Forti paradox \cite{Gir70,Coq85}. \question{Why Injection does not work on impredicative {\tt Set}?} 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 : forall x y:nat, intro _ x = intro _ y -> x = y. Proof. 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{Recursion} \question{Why can't I define a non terminating program?} \answer Because otherwise the decidability of the type-checking algorithm (which involves evaluation of programs) is not ensured. On another side, if non terminating proofs were allowed, we could get a proof of {\tt False}: \begin{coq_example*} (* This is fortunately not allowed! *) Fixpoint InfiniteProof (n:nat) : False := InfiniteProof n. Theorem Paradox : False. Proof (InfiniteProof O). \end{coq_example*} \question{Why only structurally well-founded loops are allowed?} \answer The structural order on inductive types is a simple and powerful notion of termination. The consistency of the Calculus of Inductive Constructions relies on it and another consistency proof would have to be made for stronger termination arguments (such as the termination of the evaluation of CIC programs themselves!). In spite of this, all non-pathological termination orders can be mapped to a structural order. Tools to do this are provided in the file \vfile{\InitWf}{Wf} of the standard library of {\Coq}. \question{How to define loops based on non structurally smaller recursive calls?} \answer The procedure is as follows (we consider the definition of {\tt mergesort} as an example). \begin{itemize} \item Define the termination order, say {\tt R} on the type {\tt A} of the arguments of the loop. \begin{coq_eval} Open Scope R_scope. Require Import List. \end{coq_eval} \begin{coq_example*} Definition R (a b:list nat) := length a < length b. \end{coq_example*} \item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}). \begin{coq_example*} Lemma Rwf : well_founded (A:=R). \end{coq_example*} \item Define the step function (which needs proofs that recursive calls are on smaller arguments). \begin{coq_example*} 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 := (* ... *) . 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{coq_example*} \item Define the recursive function by fixpoint on the step function. \begin{coq_example*} Definition merge := Fix Rwf (fun _ => list nat) merge_step. \end{coq_example*} \end{itemize} \question{What is behind these accessibility and well-foundedness proofs?} \answer Well-foundedness of some relation {\tt R} on some type {\tt A} is defined as the accessibility of all elements of {\tt A} along {\tt R}. \begin{coq_example} Print well_founded. Print Acc. \end{coq_example} The structure of the accessibility predicate is a well-founded tree branching at each node {\tt x} in {\tt A} along all the nodes {\tt x'} less than {\tt x} along {\tt R}. Any sequence of elements of {\tt A} decreasing along the order {\tt R} are branches in the accessibility tree. Hence any decreasing along {\tt R} is mapped into a structural decreasing in the accessibility tree of {\tt R}. This is emphasised in the definition of {\tt fix} which recurs not on its argument {\tt x:A} but on the accessibility of this argument along {\tt R}. See file \vfile{\InitWf}{Wf}. \section{Elimination, Case Analysis and Induction} %\subsection{Parametric elimination} \question{What is parametric elimination?} \answer {\em 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 eq_ind. 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 nestruct} and {\tt case}, {\tt simple induction} and {\tt simple destruct}. % \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 {\tt Prop}, use the command {\tt Scheme} and apply the elimination scheme using the \verb=using= option of \verb=elim=, \verb=destruct= or \verb=induction=. \question{How to eliminate impossible cases of an inductive definition} \answer Use {\tt inversion}. %\subsection{Induction} \question{How to perform double induction?} \answer In general a double induction is simply solved by an induction on the first hypothesis followed by an inversion over the second hypothesis. Here is an example \begin{coq_eval} Reset Initial. \end{coq_eval} \begin{coq_example} Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n:nat, even n -> even (S (S n)). Inductive odd : nat -> Prop := | odd_SO : odd 1 | odd_S : forall n:nat, odd n -> odd (S (S n)). Goal forall n:nat, even n -> odd n -> False. induction 1. inversion 1. inversion 1. apply IHeven; trivial. Qed. \end{coq_example} \Rem In case the type of the second induction hypothesis is not dependent, {\tt inversion} can just be replaced by {\tt destruct}. \question{How to define a function by double recursion?} \answer The same trick applies, you can even use the pattern-matching compilation algorithm to do the work for you. Here is an example: \begin{coq_example} Fixpoint minus (n m:nat) {struct n} : nat := match n, m with | O, _ => 0 | S k, O => S k | S k, S l => minus k l end. Print minus. \end{coq_example} \Rem In case of dependencies in the type of the induction objects $t_1$ and $t_2$, an extra argument stating $t_1=t_2$ must be given to the fixpoint definition \question{How to perform nested induction?} \answer To reason by nested induction, just reason by induction on the successive components. \begin{coq_eval} Require Import Arith. \end{coq_eval} \begin{coq_example} Infix "<" := lt (at level 50, no associativity). Infix "<=" := le (at level 50, no associativity). Lemma le_or_lt : forall n n0:nat, n0 < n \/ n <= n0. induction n; destruct n0; auto with arith. destruct (IHn n0); auto with arith. \end{coq_example} \question{How to define a function by nested recursion?} \answer The same trick applies. Here is the example of Ackermann function. \begin{coq_example} Fixpoint ack (n:nat) : nat -> nat := match n with | O => S | S n' => (fix ack' (m:nat) : nat := match m with | O => ack n' 1 | S m' => ack n' (ack' m') end) end. \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} 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 : forall n:nat, nats n = Cons n (nats (S n)). Proof. intro; change (nats n = match nats n with | 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-synthetised from the copied-pasted term in the same way as it is in the original term. Consider for instance {\tt (@eq Type True True)}. This term is printed as {\tt True=True} and re-parsed as {\tt (@eq 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_eval} Reset Initial. \end{coq_eval} \begin{coq_example*} Inductive Def1 : Set := c1 : Def1. Inductive DefProp : Def1 -> Set := c2 : forall d:Def1, DefProp d. Inductive Comb : Set := c3 : forall d:Def1, DefProp d -> Comb. Lemma eq_comb : forall (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_eval} Abort. \end{coq_eval} \begin{coq_example*} Scheme DefProp_elim := Induction for DefProp Sort Prop. Lemma eq_comb : forall d1 d1':Def1, d1 = d1' -> forall (d2:DefProp d1) (d2':DefProp d1'), c3 d1 d2 = c3 d1' d2'. intros. destruct H. destruct d2 using DefProp_elim. destruct 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 0 | pS : forall n:nat, natProp n -> natProp (S n). Inductive package : Set := pack : forall n:nat, natProp n -> package. Lemma eq_pack : forall n n':nat, n = n' -> forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'. \end{coq_example*} \answer \begin{coq_eval} Abort. \end{coq_eval} \begin{coq_example*} Scheme natProp_elim := Induction for natProp Sort Prop. Definition pack_S : package -> package. destruct 1. apply (pack (S n)). apply pS; assumption. Defined. Lemma eq_pack : forall n n':nat, n = n' -> forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'. intros n n' Heq np np'. generalize dependent n'. induction np using natProp_elim. induction np' using natProp_elim; intros; auto. discriminate Heq. induction np' using natProp_elim; intros; auto. discriminate Heq. change (pack_S (pack n np) = pack_S (pack n0 np')). apply (f_equal (A:=package)). apply IHnp. 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 (fun x:A => P x)}. Since {\Coq} does not reason up to $\eta$-conversion, this is different from \texttt{sig P}. \bibliographystyle{plain} \bibliography{biblio} \end{document}