path: root/doc/faq.tex

\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}