summaryrefslogtreecommitdiff
path: root/doc/RecTutorial
diff options
context:
space:
mode:
Diffstat (limited to 'doc/RecTutorial')
-rw-r--r--doc/RecTutorial/RecTutorial.tex3690
-rw-r--r--doc/RecTutorial/RecTutorial.v1232
-rw-r--r--doc/RecTutorial/coqartmacros.tex180
-rw-r--r--doc/RecTutorial/manbiblio.bib875
-rw-r--r--doc/RecTutorial/morebib.bib55
-rw-r--r--doc/RecTutorial/recmacros.tex75
6 files changed, 6107 insertions, 0 deletions
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
new file mode 100644
index 00000000..f2cb383e
--- /dev/null
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -0,0 +1,3690 @@
+\documentclass[11pt]{article}
+\title{A Tutorial on [Co-]Inductive Types in Coq}
+\author{Eduardo Gim\'enez\thanks{Eduardo.Gimenez@inria.fr},
+Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}}
+\date{May 1998 --- \today}
+
+\usepackage{multirow}
+% \usepackage{aeguill}
+% \externaldocument{RefMan-gal.v}
+% \externaldocument{RefMan-ext.v}
+% \externaldocument{RefMan-tac.v}
+% \externaldocument{RefMan-oth}
+% \externaldocument{RefMan-tus.v}
+% \externaldocument{RefMan-syn.v}
+% \externaldocument{Extraction.v}
+\input{recmacros}
+\input{coqartmacros}
+\newcommand{\refmancite}[1]{{}}
+% \newcommand{\refmancite}[1]{\cite{coqrefman}}
+% \newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}}
+
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{makeidx}
+% \usepackage{multind}
+\usepackage{alltt}
+\usepackage{verbatim}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{theorem}
+\usepackage[dvips]{epsfig}
+\usepackage{epic}
+\usepackage{eepic}
+% \usepackage{ecltree}
+\usepackage{moreverb}
+\usepackage{color}
+\usepackage{pifont}
+\usepackage{xr}
+\usepackage{url}
+
+\usepackage{alltt}
+\renewcommand{\familydefault}{ptm}
+\renewcommand{\seriesdefault}{m}
+\renewcommand{\shapedefault}{n}
+\newtheorem{exercise}{Exercise}[section]
+\makeindex
+\begin{document}
+\maketitle
+
+\begin{abstract}
+This document\footnote{The first versions of this document were entirely written by Eduardo Gimenez.
+Pierre Cast\'eran wrote the 2004 and 2006 revisions.} is an introduction to the definition and
+use of inductive and co-inductive types in the {\coq} proof environment. It explains how types like natural numbers and infinite streams are defined
+in {\coq}, and the kind of proof techniques that can be used to reason
+about them (case analysis, induction, inversion of predicates,
+co-induction, etc). Each technique is illustrated through an
+executable and self-contained {\coq} script.
+\end{abstract}
+%\RRkeyword{Proof environments, recursive types.}
+%\makeRT
+
+\addtocontents{toc}{\protect \thispagestyle{empty}}
+\pagenumbering{arabic}
+
+\cleardoublepage
+\tableofcontents
+\clearpage
+
+\section{About this document}
+
+This document is an introduction to the definition and use of
+inductive and co-inductive types in the {\coq} proof environment. It was born from the
+notes written for the course about the version V5.10 of {\coq}, given
+by Eduardo Gimenez at
+the Ecole Normale Sup\'erieure de Lyon in March 1996. This article is
+a revised and improved version of these notes for the version V8.0 of
+the system.
+
+
+We assume that the reader has some familiarity with the
+proofs-as-programs paradigm of Logic \cite{Coquand:metamathematical} and the generalities
+of the {\coq} system \cite{coqrefman}. You would take a greater advantage of
+this document if you first read the general tutorial about {\coq} and
+{\coq}'s FAQ, both available on \cite{coqsite}.
+A text book \cite{coqart}, accompanied with a lot of
+examples and exercises \cite{Booksite}, presents a detailed description
+of the {\coq} system and its underlying
+formalism: the Calculus of Inductive Construction.
+Finally, the complete description of {\coq} is given in the reference manual
+\cite{coqrefman}. Most of the tactics and commands we describe have
+several options, which we do not present exhaustively.
+If some script herein uses a non described feature, please refer to
+the Reference Manual.
+
+
+If you are familiar with other proof environments
+based on type theory and the LCF style ---like PVS, LEGO, Isabelle,
+etc--- then you will find not difficulty to guess the unexplained
+details.
+
+The better way to read this document is to start up the {\coq} system,
+type by yourself the examples and exercises, and observe the
+behavior of the system. All the examples proposed in this tutorial
+can be downloaded from the same site as the present document.
+
+
+The tutorial is organised as follows. The next section describes how
+inductive types are defined in {\coq}, and introduces some useful ones,
+like natural numbers, the empty type, the propositional equality type,
+and the logical connectives. Section \ref{CaseAnalysis} explains
+definitions by pattern-matching and their connection with the
+principle of case analysis. This principle is the most basic
+elimination rule associated with inductive or co-inductive types
+ and follows a
+general scheme that we illustrate for some of the types introduced in
+Section \ref{Introduction}. Section \ref{CaseTechniques} illustrates
+the pragmatics of this principle, showing different proof techniques
+based on it. Section \ref{StructuralInduction} introduces definitions
+by structural recursion and proofs by induction.
+Section~\ref{CaseStudy} presents some elaborate techniques
+about dependent case analysis. Finally, Section
+\ref{CoInduction} is a brief introduction to co-inductive types
+--i.e., types containing infinite objects-- and the principle of
+co-induction.
+
+
+Thanks to Bruno Barras, Yves Bertot, Hugo Herbelin, Jean-Fran\c{c}ois Monin
+and Michel L\'evy for their help.
+
+\subsection*{Lexical conventions}
+The \texttt{typewriter} font is used to represent text
+input by the user, while the \textit{italic} font is used to represent
+the text output by the system as answers.
+
+
+Moreover, the mathematical symbols \coqle{}, \coqdiff, \(\exists\),
+\(\forall\), \arrow{}, $\rightarrow{}$ \coqor{}, \coqand{}, and \funarrow{}
+stand for the character strings \citecoq{<=}, \citecoq{<>},
+\citecoq{exists}, \citecoq{forall}, \citecoq{->}, \citecoq{<-},
+\texttt{\char'134/}, \texttt{/\char'134}, and \citecoq{=>},
+respectively. For instance, the \coq{} statement
+%V8 A prendre
+% inclusion numero 1
+% traduction numero 1
+\begin{alltt}
+\hide{Open Scope nat_scope. Check (}forall A:Type,(exists x : A, forall (y:A), x <> y) -> 2 = 3\hide{).}
+\end{alltt}
+is written as follows in this tutorial:
+%V8 A prendre
+% inclusion numero 2
+% traduction numero 2
+\begin{alltt}
+\hide{Check (}{\prodsym}A:Type,(\exsym{}x:A, {\prodsym}y:A, x {\coqdiff} y) \arrow{} 2 = 3\hide{).}
+\end{alltt}
+
+When a fragment of \coq{} input text appears in the middle of
+regular text, we often place this fragment between double quotes
+``\dots.'' These double quotes do not belong to the \coq{} syntax.
+
+Finally, any
+string enclosed between \texttt{(*} and \texttt{*)} is a comment and
+is ignored by the \coq{} system.
+
+\section{Introducing Inductive Types}
+\label{Introduction}
+
+Inductive types are types closed with respect to their introduction
+rules. These rules explain the most basic or \textsl{canonical} ways
+of constructing an element of the type. In this sense, they
+characterize the recursive type. Different rules must be considered as
+introducing different objects. In order to fix ideas, let us introduce
+in {\coq} the most well-known example of a recursive type: the type of
+natural numbers.
+
+%V8 A prendre
+\begin{alltt}
+Inductive nat : Set :=
+ | O : nat
+ | S : nat\arrow{}nat.
+\end{alltt}
+
+The definition of a recursive type has two main parts. First, we
+establish what kind of recursive type we will characterize (a set, in
+this case). Second, we present the introduction rules that define the
+type ({\Z} and {\SUCC}), also called its {\sl constructors}. The constructors
+{\Z} and {\SUCC} determine all the elements of this type. In other
+words, if $n\mbox{:}\nat$, then $n$ must have been introduced either
+by the rule {\Z} or by an application of the rule {\SUCC} to a
+previously constructed natural number. In this sense, we can say
+that {\nat} is \emph{closed}. On the contrary, the type
+$\Set$ is an {\it open} type, since we do not know {\it a priori} all
+the possible ways of introducing an object of type \texttt{Set}.
+
+After entering this command, the constants {\nat}, {\Z} and {\SUCC} are
+available in the current context. We can see their types using the
+\texttt{Check} command \refmancite{Section \ref{Check}}:
+
+%V8 A prendre
+\begin{alltt}
+Check nat.
+\it{}nat : Set
+\tt{}Check O.
+\it{}O : nat
+\tt{}Check S.
+\it{}S : nat {\arrow} nat
+\end{alltt}
+
+Moreover, {\coq} adds to the context three constants named
+ $\natind$, $\natrec$ and $\natrect$, which
+ correspond to different principles of structural induction on
+natural numbers that {\coq} infers automatically from the definition. We
+will come back to them in Section \ref{StructuralInduction}.
+
+
+In fact, the type of natural numbers as well as several useful
+theorems about them are already defined in the basic library of {\coq},
+so there is no need to introduce them. Therefore, let us throw away
+our (re)definition of {\nat}, using the command \texttt{Reset}.
+
+%V8 A prendre
+\begin{alltt}
+Reset nat.
+Print nat.
+\it{}Inductive nat : Set := O : nat | S : nat \arrow{} nat
+For S: Argument scope is [nat_scope]
+\end{alltt}
+
+Notice that \coq{}'s \emph{interpretation scope} for natural numbers
+(called \texttt{nat\_scope})
+allows us to read and write natural numbers in decimal form (see \cite{coqrefman}). For instance, the constructor \texttt{O} can be read or written
+as the digit $0$, and the term ``~\texttt{S (S (S O))}~'' as $3$.
+
+%V8 A prendre
+\begin{alltt}
+Check O.
+\it 0 : nat.
+\tt
+Check (S (S (S O))).
+\it 3 : nat
+\end{alltt}
+
+Let us now take a look to some other
+recursive types contained in the standard library of {\coq}.
+
+\subsection{Lists}
+Lists are defined in library \citecoq{List}\footnote{Notice that in versions of
+{\coq}
+prior to 8.1, the parameter $A$ had sort \citecoq{Set} instead of \citecoq{Type};
+the constant \citecoq{list} was thus of type \citecoq{Set\arrow{} Set}.}
+
+
+\begin{alltt}
+Require Import List.
+Print list.
+\it
+Inductive list (A : Type) : Type:=
+ nil : list A | cons : A {\arrow} list A {\arrow} list A
+For nil: Argument A is implicit
+For cons: Argument A is implicit
+For list: Argument scope is [type_scope]
+For nil: Argument scope is [type_scope]
+For cons: Argument scopes are [type_scope _ _]
+\end{alltt}
+
+In this definition, \citecoq{A} is a \emph{general parameter}, global
+to both constructors.
+This kind of definition allows us to build a whole family of
+inductive types, indexed over the sort \citecoq{Type}.
+This can be observed if we consider the type of identifiers
+\citecoq{list}, \citecoq{cons} and \citecoq{nil}.
+Notice the notation \citecoq{(A := \dots)} which must be used
+when {\coq}'s type inference algorithm cannot infer the implicit
+parameter \citecoq{A}.
+\begin{alltt}
+Check list.
+\it list
+ : Type {\arrow} Type
+
+\tt Check (nil (A:=nat)).
+\it nil
+ : list nat
+
+\tt Check (nil (A:= nat {\arrow} nat)).
+\it nil
+ : list (nat {\arrow} nat)
+
+\tt Check (fun A: Type {\funarrow} (cons (A:=A))).
+\it fun A : Type {\funarrow} cons (A:=A)
+ : {\prodsym} A : Type, A {\arrow} list A {\arrow} list A
+
+\tt Check (cons 3 (cons 2 nil)).
+\it 3 :: 2 :: nil
+ : list nat
+
+\tt Check (nat :: bool ::nil).
+\it nat :: bool :: nil
+ : list Set
+
+\tt Check ((3<=4) :: True ::nil).
+\it (3<=4) :: True :: nil
+ : list Prop
+
+\tt Check (Prop::Set::nil).
+\it Prop::Set::nil
+ : list Type
+\end{alltt}
+
+\subsection{Vectors.}
+\label{vectors}
+
+Like \texttt{list}, \citecoq{vector} is a polymorphic type:
+if $A$ is a type, and $n$ a natural number, ``~\citecoq{vector $A$ $n$}~''
+is the type of vectors of elements of $A$ and size $n$.
+
+
+\begin{alltt}
+Require Import Bvector.
+
+Print vector.
+\it
+Inductive vector (A : Type) : nat {\arrow} Type :=
+ Vnil : vector A 0
+ | Vcons : A {\arrow} {\prodsym} n : nat, vector A n {\arrow} vector A (S n)
+For vector: Argument scopes are [type_scope nat_scope]
+For Vnil: Argument scope is [type_scope]
+For Vcons: Argument scopes are [type_scope _ nat_scope _]
+\end{alltt}
+
+
+Remark the difference between the two parameters $A$ and $n$:
+The first one is a \textsl{general parameter}, global to all the
+introduction rules,while the second one is an \textsl{index}, which is
+instantiated differently in the introduction rules.
+Such types parameterized by regular
+values are called \emph{dependent types}.
+
+\begin{alltt}
+Check (Vnil nat).
+\it Vnil nat
+ : vector nat 0
+
+\tt Check (fun (A:Type)(a:A){\funarrow} Vcons _ a _ (Vnil _)).
+\it fun (A : Type) (a : A) {\funarrow} Vcons A a 0 (Vnil A)
+ : {\prodsym} A : Type, A {\arrow} vector A 1
+
+
+\tt Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+\it Vcons nat 5 1 (Vcons nat 3 0 (Vnil nat))
+ : vector nat 2
+\end{alltt}
+
+\subsection{The contradictory proposition.}
+Another example of an inductive type is the contradictory proposition.
+This type inhabits the universe of propositions, and has no element
+at all.
+%V8 A prendre
+\begin{alltt}
+Print False.
+\it{} Inductive False : Prop :=
+\end{alltt}
+
+\noindent Notice that no constructor is given in this definition.
+
+\subsection{The tautological proposition.}
+Similarly, the
+tautological proposition {\True} is defined as an inductive type
+with only one element {\I}:
+
+%V8 A prendre
+\begin{alltt}
+Print True.
+\it{}Inductive True : Prop := I : True
+\end{alltt}
+
+\subsection{Relations as inductive types.}
+Some relations can also be introduced in a smart way as an inductive family
+of propositions. Let us take as example the order $n \leq m$ on natural
+numbers, called \citecoq{le} in {\coq}.
+ This relation is introduced through
+the following definition, quoted from the standard library\footnote{In the interpretation scope
+for Peano arithmetic:
+\citecoq{nat\_scope}, ``~\citecoq{n <= m}~'' is equivalent to
+``~\citecoq{le n m}~'' .}:
+
+
+
+
+%V8 A prendre
+\begin{alltt}
+Print le. \it
+Inductive le (n:nat) : nat\arrow{}Prop :=
+| le_n: n {\coqle} n
+| le_S: {\prodsym} m, n {\coqle} m \arrow{} n {\coqle} S m.
+\end{alltt}
+
+Notice that in this definition $n$ is a general parameter,
+while the second argument of \citecoq{le} is an index (see section
+~\ref{vectors}).
+ This definition
+introduces the binary relation $n {\leq} m$ as the family of unary predicates
+``\textsl{to be greater or equal than a given $n$}'', parameterized by $n$.
+
+The introduction rules of this type can be seen as a sort of Prolog
+rules for proving that a given integer $n$ is less or equal than another one.
+In fact, an object of type $n{\leq} m$ is nothing but a proof
+built up using the constructors \textsl{le\_n} and
+\textsl{le\_S} of this type. As an example, let us construct
+a proof that zero is less or equal than three using {\coq}'s interactive
+proof mode.
+Such an object can be obtained applying three times the second
+introduction rule of \citecoq{le}, to a proof that zero is less or equal
+than itself,
+which is provided by the first constructor of \citecoq{le}:
+
+%V8 A prendre
+\begin{alltt}
+Theorem zero_leq_three: 0 {\coqle} 3.
+Proof.
+\it{} 1 subgoal
+
+============================
+ 0 {\coqle} 3
+
+\tt{}Proof.
+ constructor 2.
+
+\it{} 1 subgoal
+============================
+ 0 {\coqle} 2
+
+\tt{} constructor 2.
+\it{} 1 subgoal
+============================
+ 0 {\coqle} 1
+
+\tt{} constructor 2
+\it{} 1 subgoal
+============================
+ 0 {\coqle} 0
+
+\tt{} constructor 1.
+
+\it{}Proof completed
+\tt{}Qed.
+\end{alltt}
+
+\noindent When
+the current goal is an inductive type, the tactic
+``~\citecoq{constructor $i$}~'' \refmancite{Section \ref{constructor}} applies the $i$-th constructor in the
+definition of the type. We can take a look at the proof constructed
+using the command \texttt{Print}:
+
+%V8 A prendre
+\begin{alltt}
+Print Print zero_leq_three.
+\it{}zero_leq_three =
+zero_leq_three = le_S 0 2 (le_S 0 1 (le_S 0 0 (le_n 0)))
+ : 0 {\coqle} 3
+\end{alltt}
+
+When the parameter $i$ is not supplied, the tactic \texttt{constructor}
+tries to apply ``~\texttt{constructor $1$}~'', ``~\texttt{constructor $2$}~'',\dots,
+``~\texttt{constructor $n$}~'' where $n$ is the number of constructors
+of the inductive type (2 in our example) of the conclusion of the goal.
+Our little proof can thus be obtained iterating the tactic
+\texttt{constructor} until it fails:
+
+%V8 A prendre
+\begin{alltt}
+Lemma zero_leq_three': 0 {\coqle} 3.
+ repeat constructor.
+Qed.
+\end{alltt}
+
+Notice that the strict order on \texttt{nat}, called \citecoq{lt}
+is not inductively defined: the proposition $n<p$ (notation for \citecoq{lt $n$ $p$})
+is reducible to \citecoq{(S $n$) $\leq$ p}.
+
+\begin{alltt}
+Print lt.
+\it
+lt = fun n m : nat {\funarrow} S n {\coqle} m
+ : nat {\arrow} nat {\arrow} Prop
+\tt
+Lemma zero_lt_three : 0 < 3.
+Proof.
+ repeat constructor.
+Qed.
+
+Print zero_lt_three.
+\it zero_lt_three = le_S 1 2 (le_S 1 1 (le_n 1))
+ : 0 < 3
+\end{alltt}
+
+
+
+\subsection{About general parameters (\coq{} version $\geq$ 8.1)}
+\label{parameterstuff}
+
+Since version $8.1$, it is possible to write more compact inductive definitions
+than in earlier versions.
+
+Consider the following alternative definition of the relation $\leq$ on
+type \citecoq{nat}:
+
+\begin{alltt}
+Inductive le'(n:nat):nat -> Prop :=
+ | le'_n : le' n n
+ | le'_S : forall p, le' (S n) p -> le' n p.
+
+Hint Constructors le'.
+\end{alltt}
+
+We notice that the type of the second constructor of \citecoq{le'}
+has an argument whose type is \citecoq{le' (S n) p}.
+This constrasts with earlier versions
+of {\coq}, in which a general parameter $a$ of an inductive
+type $I$ had to appear only in applications of the form $I\,\dots\,a$.
+
+Since version $8.1$, if $a$ is a general parameter of an inductive
+type $I$, the type of an argument of a constructor of $I$ may be
+of the form $I\,\dots\,t_a$ , where $t_a$ is any term.
+Notice that the final type of the constructors must be of the form
+$I\,\dots\,a$, since these constructors describe how to form
+inhabitants of type $I\,\dots\,a$ (this is the role of parameter $a$).
+
+Another example of this new feature is {\coq}'s definition of accessibility
+(see Section~\ref{WellFoundedRecursion}), which has a general parameter
+$x$; the constructor for the predicate
+``$x$ is accessible'' takes an argument of type ``$y$ is accessible''.
+
+
+
+In earlier versions of {\coq}, a relation like \citecoq{le'} would have to be
+defined without $n$ being a general parameter.
+
+\begin{alltt}
+Reset le'.
+
+Inductive le': nat-> nat -> Prop :=
+ | le'_n : forall n, le' n n
+ | le'_S : forall n p, le' (S n) p -> le' n p.
+\end{alltt}
+
+
+
+
+\subsection{The propositional equality type.} \label{equality}
+In {\coq}, the propositional equality between two inhabitants $a$ and
+$b$ of
+the same type $A$ ,
+noted $a=b$, is introduced as a family of recursive predicates
+``~\textsl{to be equal to $a$}~'', parameterised by both $a$ and its type
+$A$. This family of types has only one introduction rule, which
+corresponds to reflexivity.
+Notice that the syntax ``\citecoq{$a$ = $b$}~'' is an abbreviation
+for ``\citecoq{eq $a$ $b$}~'', and that the parameter $A$ is \emph{implicit},
+as it can be infered from $a$.
+%V8 A prendre
+\begin{alltt}
+Print eq.
+\it{} Inductive eq (A : Type) (x : A) : A \arrow{} Prop :=
+ refl_equal : x = x
+For eq: Argument A is implicit
+For refl_equal: Argument A is implicit
+For eq: Argument scopes are [type_scope _ _]
+For refl_equal: Argument scopes are [type_scope _]
+\end{alltt}
+
+Notice also that the first parameter $A$ of \texttt{eq} has type
+\texttt{Type}. The type system of {\coq} allows us to consider equality between
+various kinds of terms: elements of a set, proofs, propositions,
+types, and so on.
+Look at \cite{coqrefman, coqart} to get more details on {\coq}'s type
+system, as well as implicit arguments and argument scopes.
+
+
+\begin{alltt}
+Lemma eq_3_3 : 2 + 1 = 3.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
+Proof.
+ reflexivity.
+Qed.
+
+Print eq_proof_proof.
+\it eq_proof_proof =
+refl_equal (refl_equal (3 * 4))
+ : refl_equal (2 * 6) = refl_equal (3 * 4)
+\tt
+
+Lemma eq_lt_le : ( 2 < 4) = (3 {\coqle} 4).
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_nat_nat : nat = nat.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_Set_Set : Set = Set.
+Proof.
+ reflexivity.
+Qed.
+\end{alltt}
+
+\subsection{Logical connectives.} \label{LogicalConnectives}
+The conjunction and disjunction of two propositions are also examples
+of recursive types:
+
+\begin{alltt}
+Inductive or (A B : Prop) : Prop :=
+ or_introl : A \arrow{} A {\coqor} B | or_intror : B \arrow{} A {\coqor} B
+
+Inductive and (A B : Prop) : Prop :=
+ conj : A \arrow{} B \arrow{} A {\coqand} B
+
+\end{alltt}
+
+The propositions $A$ and $B$ are general parameters of these
+connectives. Choosing different universes for
+$A$ and $B$ and for the inductive type itself gives rise to different
+type constructors. For example, the type \textsl{sumbool} is a
+disjunction but with computational contents.
+
+\begin{alltt}
+Inductive sumbool (A B : Prop) : Set :=
+ left : A \arrow{} \{A\} + \{B\} | right : B \arrow{} \{A\} + \{B\}
+\end{alltt}
+
+
+
+This type --noted \texttt{\{$A$\}+\{$B$\}} in {\coq}-- can be used in {\coq}
+programs as a sort of boolean type, to check whether it is $A$ or $B$
+that is true. The values ``~\citecoq{left $p$}~'' and
+``~\citecoq{right $q$}~'' replace the boolean values \textsl{true} and
+\textsl{false}, respectively. The advantage of this type over
+\textsl{bool} is that it makes available the proofs $p$ of $A$ or $q$
+of $B$, which could be necessary to construct a verification proof
+about the program.
+For instance, let us consider the certified program \citecoq{le\_lt\_dec}
+of the Standard Library.
+
+\begin{alltt}
+Require Import Compare_dec.
+Check le_lt_dec.
+\it
+le_lt_dec
+ : {\prodsym} n m : nat, \{n {\coqle} m\} + \{m < n\}
+
+\end{alltt}
+
+We use \citecoq{le\_lt\_dec} to build a function for computing
+the max of two natural numbers:
+
+\begin{alltt}
+Definition max (n p :nat) := match le_lt_dec n p with
+ | left _ {\funarrow} p
+ | right _ {\funarrow} n
+ end.
+\end{alltt}
+
+In the following proof, the case analysis on the term
+``~\citecoq{le\_lt\_dec n p}~'' gives us an access to proofs
+of $n\leq p$ in the first case, $p<n$ in the other.
+
+\begin{alltt}
+Theorem le_max : {\prodsym} n p, n {\coqle} p {\arrow} max n p = p.
+Proof.
+ intros n p ; unfold max ; case (le_lt_dec n p); simpl.
+\it
+2 subgoals
+
+ n : nat
+ p : nat
+ ============================
+ n {\coqle} p {\arrow} n {\coqle} p {\arrow} p = p
+
+subgoal 2 is:
+ p < n {\arrow} n {\coqle} p {\arrow} n = p
+\tt
+ trivial.
+ intros; absurd (p < p); eauto with arith.
+Qed.
+\end{alltt}
+
+
+ Once the program verified, the proofs are
+erased by the extraction procedure:
+
+\begin{alltt}
+Extraction max.
+\it
+(** val max : nat {\arrow} nat {\arrow} nat **)
+
+let max n p =
+ match le_lt_dec n p with
+ | Left {\arrow} p
+ | Right {\arrow} n
+\end{alltt}
+
+Another example of use of \citecoq{sumbool} is given in Section
+\ref{WellFoundedRecursion}: the theorem \citecoq{eq\_nat\_dec} of
+library \citecoq{Coq.Arith.Peano\_dec} is used in an euclidean division
+algorithm.
+
+\subsection{The existential quantifier.}\label{ex-def}
+The existential quantifier is yet another example of a logical
+connective introduced as an inductive type.
+
+\begin{alltt}
+Inductive ex (A : Type) (P : A \arrow{} Prop) : Prop :=
+ ex_intro : {\prodsym} x : A, P x \arrow{} ex P
+\end{alltt}
+
+Notice that {\coq} uses the abreviation ``~\citecoq{\exsym\,$x$:$A$, $B$}~''
+for \linebreak ``~\citecoq{ex (fun $x$:$A$ \funarrow{} $B$)}~''.
+
+
+\noindent The former quantifier inhabits the universe of propositions.
+As for the conjunction and disjunction connectives, there is also another
+version of existential quantification inhabiting the universes $\Type_i$,
+which is written \texttt{sig $P$}. The syntax
+``~\citecoq{\{$x$:$A$ | $B$\}}~'' is an abreviation for ``~\citecoq{sig (fun $x$:$A$ {\funarrow} $B$)}~''.
+
+
+
+%\paragraph{The logical connectives.} Conjuction and disjuction are
+%also introduced as recursive types:
+%\begin{alltt}
+%Print or.
+%\end{alltt}
+%begin{alltt}
+%Print and.
+%\end{alltt}
+
+
+\subsection{Mutually Dependent Definitions}
+\label{MutuallyDependent}
+
+Mutually dependent definitions of recursive types are also allowed in
+{\coq}. A typical example of these kind of declaration is the
+introduction of the trees of unbounded (but finite) width:
+\label{Forest}
+\begin{alltt}
+Inductive tree(A:Type) : Type :=
+ node : A {\arrow} forest A \arrow{} tree A
+with forest (A: Set) : Type :=
+ nochild : forest A |
+ addchild : tree A \arrow{} forest A \arrow{} forest A.
+\end{alltt}
+\noindent Yet another example of mutually dependent types are the
+predicates \texttt{even} and \texttt{odd} on natural numbers:
+\label{Even}
+\begin{alltt}
+Inductive
+ even : nat\arrow{}Prop :=
+ evenO : even O |
+ evenS : {\prodsym} n, odd n \arrow{} even (S n)
+with
+ odd : nat\arrow{}Prop :=
+ oddS : {\prodsym} n, even n \arrow{} odd (S n).
+\end{alltt}
+
+\begin{alltt}
+Lemma odd_49 : odd (7 * 7).
+ simpl; repeat constructor.
+Qed.
+\end{alltt}
+
+
+
+\section{Case Analysis and Pattern-matching}
+\label{CaseAnalysis}
+\subsection{Non-dependent Case Analysis}
+An \textsl{elimination rule} for the type $A$ is some way to use an
+object $a:A$ in order to define an object in some type $B$.
+A natural elimination rule for an inductive type is \emph{case analysis}.
+
+
+For instance, any value of type {\nat} is built using either \texttt{O} or \texttt{S}.
+Thus, a systematic way of building a value of type $B$ from any
+value of type {\nat} is to associate to \texttt{O} a constant $t_O:B$ and
+to every term of the form ``~\texttt{S $p$}~'' a term $t_S:B$. The following
+construction has type $B$:
+\begin{alltt}
+match \(n\) return \(B\) with O \funarrow \(t\sb{O}\) | S p \funarrow \(t\sb{S}\) end
+\end{alltt}
+
+
+In most of the cases, {\coq} is able to infer the type $B$ of the object
+defined, so the ``\texttt{return $B$}'' part can be omitted.
+
+The computing rules associated with this construct are the expected ones
+(the notation $t_S\{q/\texttt{p}\}$ stands for the substitution of $p$ by
+$q$ in $t_S$ :)
+
+\begin{eqnarray*}
+\texttt{match $O$ return $b$ with O {\funarrow} $t_O$ | S p {\funarrow} $t_S$ end} &\Longrightarrow& t_O\\
+\texttt{match $S\;q$ return $b$ with O {\funarrow} $t_O$ | S p {\funarrow} $t_S$ end} &\Longrightarrow& t_S\{q/\texttt{p}\}
+\end{eqnarray*}
+
+
+\subsubsection{Example: the predecessor function.}\label{firstpred}
+An example of a definition by case analysis is the function which
+computes the predecessor of any given natural number:
+\begin{alltt}
+Definition pred (n:nat) := match n with
+ | O {\funarrow} O
+ | S m {\funarrow} m
+ end.
+
+Eval simpl in pred 56.
+\it{} = 55
+ : nat
+\tt
+Eval simpl in pred 0.
+\it{} = 0
+ : nat
+
+\tt{}Eval simpl in fun p {\funarrow} pred (S p).
+\it{} = fun p : nat {\funarrow} p
+ : nat {\arrow} nat
+\end{alltt}
+
+As in functional programming, tuples and wild-cards can be used in
+patterns \refmancite{Section \ref{ExtensionsOfCases}}. Such
+definitions are automatically compiled by {\coq} into an expression which
+may contain several nested case expressions. For example, the
+exclusive \emph{or} on booleans can be defined as follows:
+\begin{alltt}
+Definition xorb (b1 b2:bool) :=
+ match b1, b2 with
+ | false, true {\funarrow} true
+ | true, false {\funarrow} true
+ | _ , _ {\funarrow} false
+ end.
+\end{alltt}
+
+This kind of definition is compiled in {\coq} as follows\footnote{{\coq} uses
+the conditional ``~\citecoq{if $b$ then $a$ else $b$}~'' as an abreviation to
+``~\citecoq{match $b$ with true \funarrow{} $a$ | false \funarrow{} $b$ end}~''.}:
+
+\begin{alltt}
+Print xorb.
+xorb =
+fun b1 b2 : bool {\funarrow}
+if b1 then if b2 then false else true
+ else if b2 then true else false
+ : bool {\arrow} bool {\arrow} bool
+\end{alltt}
+
+\subsection{Dependent Case Analysis}
+\label{DependentCase}
+
+For a pattern matching construct of the form
+``~\citecoq{match n with \dots end}~'' a more general typing rule
+is obtained considering that the type of the whole expression
+may also depend on \texttt{n}.
+ For instance, let us consider some function
+$Q:\texttt{nat}\arrow{}\texttt{Type}$, and $n:\citecoq{nat}$.
+In order to build a term of type $Q\;n$, we can associate
+to the constructor \texttt{O} some term $t_O: Q\;\texttt{O}$ and to
+the pattern ``~\texttt{S p}~'' some term $t_S : Q\;(S\;p)$.
+Notice that the terms $t_O$ and $t_S$ do not have the same type.
+
+The syntax of the \emph{dependent case analysis} and its
+associated typing rule make precise how the resulting
+type depends on the argument of the pattern matching, and
+which constraint holds on the branches of the pattern matching:
+
+\label{Prod-sup-rule}
+\[
+\begin{array}[t]{l}
+Q: \texttt{nat}{\arrow}\texttt{Type}\quad{t_O}:{{Q\;\texttt{O}}} \quad
+\smalljuge{p:\texttt{nat}}{t_p}{{Q\;(\texttt{S}\;p)}} \quad n:\texttt{nat} \\
+\hline
+{\texttt{match \(n\) as \(n\sb{0}\) return \(Q\;n\sb{0}\) with | O \funarrow \(t\sb{O}\) | S p \funarrow \(t\sb{S}\) end}}:{{Q\;n}}
+\end{array}
+\]
+
+
+The interest of this rule of \textsl{dependent} pattern-matching is
+that it can also be read as the following logical principle (when $Q$ has type \citecoq{nat\arrow{}Prop}
+by \texttt{Prop} in the type of $Q$): in order to prove
+that a property $Q$ holds for all $n$, it is sufficient to prove that
+$Q$ holds for {\Z} and that for all $p:\nat$, $Q$ holds for
+$(\SUCC\;p)$. The former, non-dependent version of case analysis can
+be obtained from this latter rule just taking $Q$ as a constant
+function on $n$.
+
+Notice that destructuring $n$ into \citecoq{O} or ``~\citecoq{S p}~''
+ doesn't
+make appear in the goal the equalities ``~$n=\citecoq{O}$~''
+ and ``~$n=\citecoq{S p}$~''.
+They are ``internalized'' in the rules above (see section~\ref{inversion}.)
+
+\subsubsection{Example: strong specification of the predecessor function.}
+
+In Section~\ref{firstpred}, the predecessor function was defined directly
+as a function from \texttt{nat} to \texttt{nat}. It remains to prove
+that this function has some desired properties. Another way to proceed
+is to, first introduce a specification of what is the predecessor of a
+natural number, under the form of a {\coq} type, then build an inhabitant
+of this type: in other words, a realization of this specification. This way, the correctness
+of this realization is ensured by {\coq}'s type system.
+
+A reasonable specification for $\pred$ is to say that for all $n$
+there exists another $m$ such that either $m=n=0$, or $(\SUCC\;m)$
+is equal to $n$. The function $\pred$ should be just the way to
+compute such an $m$.
+
+\begin{alltt}
+Definition pred_spec (n:nat) :=
+ \{m:nat | n=0{\coqand} m=0 {\coqor} n = S m\}.
+
+Definition predecessor : {\prodsym} n:nat, pred_spec n.
+ intro n; case n.
+\it{}
+ n : nat
+ ============================
+ pred_spec 0
+
+\tt{} unfold pred_spec;exists 0;auto.
+\it{}
+ =========================================
+ {\prodsym} n0 : nat, pred_spec (S n0)
+\tt{}
+ unfold pred_spec; intro n0; exists n0; auto.
+Defined.
+\end{alltt}
+
+If we print the term built by {\coq}, its dependent pattern-matching structure can be observed:
+
+\begin{alltt}
+predecessor = fun n : nat {\funarrow}
+\textbf{match n as n0 return (pred_spec n0) with}
+\textbf{| O {\funarrow}}
+ exist (fun m : nat {\funarrow} 0 = 0 {\coqand} m = 0 {\coqor} 0 = S m) 0
+ (or_introl (0 = 1)
+ (conj (refl_equal 0) (refl_equal 0)))
+\textbf{| S n0 {\funarrow}}
+ exist (fun m : nat {\funarrow} S n0 = 0 {\coqand} m = 0 {\coqor} S n0 = S m) n0
+ (or_intror (S n0 = 0 {\coqand} n0 = 0) (refl_equal (S n0)))
+\textbf{end} : {\prodsym} n : nat, \textbf{pred_spec n}
+\end{alltt}
+
+
+Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at for tactics
+``~\texttt{destruct}~'', ``~\texttt{intro \emph{pattern}}~'', etc. in
+the reference manual and/or the book.
+
+\noindent The command \texttt{Extraction} \refmancite{Section
+\ref{ExtractionIdent}} can be used to see the computational
+contents associated to the \emph{certified} function \texttt{predecessor}:
+\begin{alltt}
+Extraction predecessor.
+\it
+(** val predecessor : nat {\arrow} pred_spec **)
+
+let predecessor = function
+ | O {\arrow} O
+ | S n0 {\arrow} n0
+\end{alltt}
+
+
+\begin{exercise} \label{expand}
+Prove the following theorem:
+\begin{alltt}
+Theorem nat_expand : {\prodsym} n:nat,
+ n = match n with
+ | 0 {\funarrow} 0
+ | S p {\funarrow} S p
+ end.
+\end{alltt}
+\end{exercise}
+
+\subsection{Some Examples of Case Analysis}
+\label{CaseScheme}
+The reader will find in the Reference manual all details about
+typing case analysis (chapter 4: Calculus of Inductive Constructions,
+and chapter 15: Extended Pattern-Matching).
+
+The following commented examples will show the different situations to consider.
+
+
+%\subsubsection{General Scheme}
+
+%Case analysis is then the most basic elimination rule that {\coq}
+%provides for inductive types. This rule follows a general schema,
+%valid for any inductive type $I$. First, if $I$ has type
+%``~$\forall\,(z_1:A_1)\ldots(z_r:A_r),S$~'', with $S$ either $\Set$, $\Prop$ or
+%$\Type$, then a case expression on $p$ of type ``~$R\;a_1\ldots a_r$~''
+% inhabits ``~$Q\;a_1\ldots a_r\;p$~''. The types of the branches of the case expression
+%are obtained from the definition of the type in this way: if the type
+%of the $i$-th constructor $c_i$ of $R$ is
+%``~$\forall\, (x_1:T_1)\ldots
+%(x_n:T_n),(R\;q_1\ldots q_r)$~'', then the $i-th$ branch must have the
+%form ``~$c_i\; x_1\; \ldots \;x_n\; \funarrow{}\; t_i$~'' where
+%$$(x_1:T_1),\ldots, (x_n:T_n) \vdash t_i : Q\;q_1\ldots q_r)$$
+% for non-dependent case
+%analysis, and $$(x_1:T_1)\ldots (x_n:T_n)\vdash t_i :Q\;q_1\ldots
+%q_r\;({c}_i\;x_1\;\ldots x_n)$$ for dependent one. In the
+%following section, we illustrate this general scheme for different
+%recursive types.
+%%\textbf{A vérifier}
+
+\subsubsection{The Empty Type}
+
+In a definition by case analysis, there is one branch for each
+introduction rule of the type. Hence, in a definition by case analysis
+on $p:\False$ there are no cases to be considered. In other words, the
+rule of (non-dependent) case analysis for the type $\False$ is
+(for $s$ in \texttt{Prop}, \texttt{Set} or \texttt{Type}):
+
+\begin{center}
+\snregla {\JM{Q}{s}\;\;\;\;\;
+ \JM{p}{\False}}
+ {\JM{\texttt{match $p$ return $Q$ with end}}{Q}}
+\end{center}
+
+As a corollary, if we could construct an object in $\False$, then it
+could be possible to define an object in any type. The tactic
+\texttt{contradiction} \refmancite{Section \ref{Contradiction}}
+corresponds to the application of the elimination rule above. It
+searches in the context for an absurd hypothesis (this is, a
+hypothesis whose type is $\False$) and then proves the goal by a case
+analysis of it.
+
+\begin{alltt}
+Theorem fromFalse : False \arrow{} 0=1.
+Proof.
+ intro H.
+ contradiction.
+Qed.
+\end{alltt}
+
+
+In {\coq} the negation is defined as follows :
+
+\begin{alltt}
+Definition not (P:Prop) := P {\arrow} False
+\end{alltt}
+
+The proposition ``~\citecoq{not $A$}~'' is also written ``~$\neg A$~''.
+
+If $A$ and $B$ are propositions, $a$ is a proof of $A$ and
+$H$ is a proof of $\neg A$,
+the term ``~\citecoq{match $H\;a$ return $B$ with end}~'' is a proof term of
+$B$.
+Thus, if your goal is $B$ and you have some hypothesis $H:\neg A$,
+the tactic ``~\citecoq{case $H$}~'' generates a new subgoal with
+statement $A$, as shown by the following example\footnote{Notice that
+$a\coqdiff b$ is just an abreviation for ``~\coqnot a= b~''}.
+
+\begin{alltt}
+Fact Nosense : 0 {\coqdiff} 0 {\arrow} 2 = 3.
+Proof.
+ intro H; case H.
+\it
+===========================
+ 0 = 0
+\tt
+ reflexivity.
+Qed.
+\end{alltt}
+
+The tactic ``~\texttt{absurd $A$}~'' (where $A$ is any proposition),
+is based on the same principle, but
+generates two subgoals: $A$ and $\neg A$, for solving $B$.
+
+\subsubsection{The Equality Type}
+
+Let $A:\Type$, $a$, $b$ of type $A$, and $\pi$ a proof of
+$a=b$. Non dependent case analysis of $\pi$ allows us to
+associate to any proof of ``~$Q\;a$~'' a proof of ``~$Q\;b$~'',
+where $Q:A\arrow{} s$ (where $s\in\{\Prop, \Set, \Type\}$).
+The following term is a proof of ``~$Q\;a\, \arrow{}\, Q\;b$~''.
+
+\begin{alltt}
+fun H : Q a {\funarrow}
+ match \(\pi\) in (_ = y) return Q y with
+ refl_equal {\funarrow} H
+ end
+\end{alltt}
+Notice the header of the \texttt{match} construct.
+It expresses how the resulting type ``~\citecoq{Q y}~'' depends on
+the \emph{type} of \texttt{p}.
+Notice also that in the pattern introduced by the keyword \texttt{in},
+the parameter \texttt{a} in the type ``~\texttt{a = y}~'' must be
+implicit, and replaced by a wildcard '\texttt{\_}'.
+
+
+Therefore, case analysis on a proof of the equality $a=b$
+amounts to replacing all the occurrences of the term $b$ with the term
+$a$ in the goal to be proven. Let us illustrate this through an
+example: the transitivity property of this equality.
+\begin{alltt}
+Theorem trans : {\prodsym} n m p:nat, n=m \arrow{} m=p \arrow{} n=p.
+Proof.
+ intros n m p eqnm.
+\it{}
+ n : nat
+ m : nat
+ p : nat
+ eqnm : n = m
+ ============================
+ m = p {\arrow} n = p
+\tt{} case eqnm.
+\it{}
+ n : nat
+ m : nat
+ p : nat
+ eqnm : n = m
+ ============================
+ n = p {\arrow} n = p
+\tt{} trivial.
+Qed.
+\end{alltt}
+
+%\noindent The case analysis on the hypothesis $H:n=m$ yields the
+%tautological subgoal $n=p\rightarrow n=p$, that is directly proven by
+%the tactic \texttt{Trivial}.
+
+\begin{exercise}
+Prove the symmetry property of equality.
+\end{exercise}
+
+Instead of using \texttt{case}, we can use the tactic
+\texttt{rewrite} \refmancite{Section \ref{Rewrite}}. If $H$ is a proof
+of $a=b$, then
+``~\citecoq{rewrite $H$}~''
+ performs a case analysis on a proof of $b=a$, obtained by applying a
+symmetry theorem to $H$. This application of symmetry allows us to rewrite
+the equality from left to right, which looks more natural. An optional
+parameter (either \texttt{\arrow{}} or \texttt{$\leftarrow$}) can be used to precise
+in which sense the equality must be rewritten. By default,
+``~\texttt{rewrite} $H$~'' corresponds to ``~\texttt{rewrite \arrow{}} $H$~''
+\begin{alltt}
+Lemma Rw : {\prodsym} x y: nat, y = y * x {\arrow} y * x * x = y.
+ intros x y e; do 2 rewrite <- e.
+\it
+1 subgoal
+
+ x : nat
+ y : nat
+ e : y = y * x
+ ============================
+ y = y
+\tt
+ reflexivity.
+Qed.
+\end{alltt}
+
+Notice that, if $H:a=b$, then the tactic ``~\texttt{rewrite $H$}~''
+ replaces \textsl{all} the
+occurrences of $a$ by $b$. However, in certain situations we could be
+interested in rewriting some of the occurrences, but not all of them.
+This can be done using the tactic \texttt{pattern} \refmancite{Section
+\ref{Pattern}}. Let us consider yet another example to
+illustrate this.
+
+Let us start with some simple theorems of arithmetic; two of them
+are already proven in the Standard Library, the last is left as an exercise.
+
+\begin{alltt}
+\it
+mult_1_l
+ : {\prodsym} n : nat, 1 * n = n
+
+mult_plus_distr_r
+ : {\prodsym} n m p : nat, (n + m) * p = n * p + m * p
+
+mult_distr_S : {\prodsym} n p : nat, n * p + p = (S n)* p.
+\end{alltt}
+
+Let us now prove a simple result:
+
+\begin{alltt}
+Lemma four_n : {\prodsym} n:nat, n+n+n+n = 4*n.
+Proof.
+ intro n;rewrite <- (mult_1_l n).
+\it
+ n : nat
+ ============================
+ 1 * n + 1 * n + 1 * n + 1 * n = 4 * (1 * n)
+\end{alltt}
+
+We can see that the \texttt{rewrite} tactic call replaced \emph{all}
+the occurrences of \texttt{n} by the term ``~\citecoq{1 * n}~''.
+If we want to do the rewriting ony on the leftmost occurrence of
+\texttt{n}, we can mark this occurrence using the \texttt{pattern}
+tactic:
+
+
+\begin{alltt}
+ Undo.
+ intro n; pattern n at 1.
+ \it
+ n : nat
+ ============================
+ (fun n0 : nat {\funarrow} n0 + n + n + n = 4 * n) n
+\end{alltt}
+Applying the tactic ``~\citecoq{pattern n at 1}~'' allowed us
+to explicitly abstract the first occurrence of \texttt{n} from the
+goal, putting this goal under the form ``~\citecoq{$Q$ n}~'',
+thus pointing to \texttt{rewrite} the particular predicate on $n$
+that we search to prove.
+
+
+\begin{alltt}
+ rewrite <- mult_1_l.
+\it
+1 subgoal
+
+ n : nat
+ ============================
+ 1 * n + n + n + n = 4 * n
+\tt
+ repeat rewrite mult_distr_S.
+\it
+ n : nat
+ ============================
+ 4 * n = 4 * n
+\tt
+ trivial.
+Qed.
+\end{alltt}
+
+\subsubsection{The Predicate $n {\leq} m$}
+
+
+The last but one instance of the elimination schema that we will illustrate is
+case analysis for the predicate $n {\leq} m$:
+
+Let $n$ and $p$ be terms of type \citecoq{nat}, and $Q$ a predicate
+of type $\citecoq{nat}\arrow{}\Prop$.
+If $H$ is a proof of ``~\texttt{n {\coqle} p}~'',
+$H_0$ a proof of ``~\texttt{$Q$ n}~'' and
+$H_S$ a proof of the statement ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'',
+then the term
+\begin{alltt}
+match H in (_ {\coqle} q) return (Q q) with
+ | le_n {\funarrow} H0
+ | le_S m Hm {\funarrow} HS m Hm
+end
+\end{alltt}
+ is a proof term of ``~\citecoq{$Q$ $p$}~''.
+
+
+The two patterns of this \texttt{match} construct describe
+all possible forms of proofs of ``~\citecoq{n {\coqle} m}~'' (notice
+again that the general parameter \texttt{n} is implicit in
+ the ``~\texttt{in \dots}~''
+clause and is absent from the match patterns.
+
+
+Notice that the choice of introducing some of the arguments of the
+predicate as being general parameters in its definition has
+consequences on the rule of case analysis that is derived. In
+particular, the type $Q$ of the object defined by the case expression
+only depends on the indexes of the predicate, and not on the general
+parameters. In the definition of the predicate $\leq$, the first
+argument of this relation is a general parameter of the
+definition. Hence, the predicate $Q$ to be proven only depends on the
+second argument of the relation. In other words, the integer $n$ is
+also a general parameter of the rule of case analysis.
+
+An example of an application of this rule is the following theorem,
+showing that any integer greater or equal than $1$ is the successor of another
+natural number:
+
+\begin{alltt}
+Lemma predecessor_of_positive :
+ {\prodsym} n, 1 {\coqle} n {\arrow} {\exsym} p:nat, n = S p.
+Proof.
+ intros n H;case H.
+\it
+ n : nat
+ H : 1 {\coqle} n
+ ============================
+ {\exsym} p : nat, 1 = S p
+\tt
+ exists 0; trivial.
+\it
+
+ n : nat
+ H : 1 {\coqle} n
+ ============================
+ {\prodsym} m : nat, 0 {\coqle} m {\arrow} {\exsym} p : nat, S m = S p
+\tt
+ intros m _ .
+ exists m.
+ trivial.
+Qed.
+\end{alltt}
+
+
+\subsubsection{Vectors}
+
+The \texttt{vector} polymorphic and dependent family of types will
+give an idea of the most general scheme of pattern-matching.
+
+For instance, let us define a function for computing the tail of
+any vector. Notice that we shall build a \emph{total} function,
+by considering that the tail of an empty vector is this vector itself.
+In that sense, it will be slightly different from the \texttt{Vtail}
+function of the Standard Library, which is defined only for vectors
+of type ``~\citecoq{vector $A$ (S $n$)}~''.
+
+The header of the function we want to build is the following:
+
+\begin{verbatim}
+Definition Vtail_total
+ (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
+\end{verbatim}
+
+Since the branches will not have the same type
+(depending on the parameter \texttt{n}),
+the body of this function is a dependent pattern matching on
+\citecoq{v}.
+So we will have :
+\begin{verbatim}
+match v in (vector _ n0) return (vector A (pred n0)) with
+\end{verbatim}
+
+The first branch deals with the constructor \texttt{Vnil} and must
+return a value in ``~\citecoq{vector A (pred 0)}~'', convertible
+to ``~\citecoq{vector A 0}~''. So, we propose:
+\begin{alltt}
+| Vnil {\funarrow} Vnil A
+\end{alltt}
+
+The second branch considers a vector in ``~\citecoq{vector A (S n0)}~''
+of the form
+``~\citecoq{Vcons A n0 v0}~'', with ``~\citecoq{v0:vector A n0}~'',
+and must return a value of type ``~\citecoq{vector A (pred (S n0))}~'',
+which is convertible to ``~\citecoq{vector A n0}~''.
+This second branch is thus :
+\begin{alltt}
+| Vcons _ n0 v0 {\funarrow} v0
+\end{alltt}
+
+Here is the full definition:
+
+\begin{alltt}
+Definition Vtail_total
+ (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
+match v in (vector _ n0) return (vector A (pred n0)) with
+| Vnil {\funarrow} Vnil A
+| Vcons _ n0 v0 {\funarrow} v0
+end.
+\end{alltt}
+
+
+\subsection{Case Analysis and Logical Paradoxes}
+
+In the previous section we have illustrated the general scheme for
+generating the rule of case analysis associated to some recursive type
+from the definition of the type. However, if the logical soundness is
+to be preserved, certain restrictions to this schema are
+necessary. This section provides a brief explanation of these
+restrictions.
+
+
+\subsubsection{The Positivity Condition}
+\label{postypes}
+
+In order to make sense of recursive types as types closed under their
+introduction rules, a constraint has to be imposed on the possible
+forms of such rules. This constraint, known as the
+\textsl{positivity condition}, is necessary to prevent the user from
+naively introducing some recursive types which would open the door to
+logical paradoxes. An example of such a dangerous type is the
+``inductive type'' \citecoq{Lambda}, whose only constructor is
+\citecoq{lambda} of type \citecoq{(Lambda\arrow False)\arrow Lambda}.
+ Following the pattern
+given in Section \ref{CaseScheme}, the rule of (non dependent) case
+analysis for \citecoq{Lambda} would be the following:
+
+\begin{center}
+\snregla {\JM{Q}{\Prop}\;\;\;\;\;
+ \JM{p}{\texttt{Lambda}}\;\;\;\;\;
+ {h : {\texttt{Lambda}}\arrow\False\; \vdash\; t\,:\,Q}}
+ {\JM{\citecoq{match $p$ return $Q$ with lambda h {\funarrow} $t$ end}}{Q}}
+\end{center}
+
+In order to avoid paradoxes, it is impossible to construct
+the type \citecoq{Lambda} in {\coq}:
+
+\begin{alltt}
+Inductive Lambda : Set :=
+ lambda : (Lambda {\arrow} False) {\arrow} Lambda.
+\it
+Error: Non strictly positive occurrence of "Lambda" in
+ "(Lambda {\arrow} False) {\arrow} Lambda"
+\end{alltt}
+
+In order to explain this danger, we
+will declare some constants for simulating the construction of
+\texttt{Lambda} as an inductive type.
+
+Let us open some section, and declare two variables, the first one for
+\texttt{Lambda}, the other for the constructor \texttt{lambda}.
+
+\begin{alltt}
+Section Paradox.
+Variable Lambda : Set.
+Variable lambda : (Lambda {\arrow} False) {\arrow}Lambda.
+\end{alltt}
+
+Since \texttt{Lambda} is not a truely inductive type, we can't use
+the \texttt{match} construct. Nevertheless, we can simulate it by a
+variable \texttt{matchL} such that the term
+``~\citecoq{matchL $l$ $Q$ (fun $h$ : Lambda {\arrow} False {\funarrow} $t$)}~''
+should be understood as
+``~\citecoq{match $l$ return $Q$ with | lambda h {\funarrow} $t$)}~''
+
+
+\begin{alltt}
+Variable matchL : Lambda {\arrow}
+ {\prodsym} Q:Prop, ((Lambda {\arrow}False) {\arrow} Q) {\arrow}
+ Q.
+\end{alltt}
+
+>From these constants, it is possible to define application by case
+analysis. Then, through auto-application, the well-known looping term
+$(\lambda x.(x\;x)\;\lambda x.(x\;x))$ provides a proof of falsehood.
+
+\begin{alltt}
+Definition application (f x: Lambda) :False :=
+ matchL f False (fun h {\funarrow} h x).
+
+Definition Delta : Lambda :=
+ lambda (fun x : Lambda {\funarrow} application x x).
+
+Definition loop : False := application Delta Delta.
+
+Theorem two_is_three : 2 = 3.
+Proof.
+ elim loop.
+Qed.
+
+End Paradox.
+\end{alltt}
+
+\noindent This example can be seen as a formulation of Russell's
+paradox in type theory associating $(\textsl{application}\;x\;x)$ to the
+formula $x\not\in x$, and \textsl{Delta} to the set $\{ x \mid
+x\not\in x\}$. If \texttt{matchL} would satisfy the reduction rule
+associated to case analysis, that is,
+$$ \citecoq{matchL (lambda $f$) $Q$ $h$} \Longrightarrow h\;f$$
+then the term \texttt{loop}
+would compute into itself. This is not actually surprising, since the
+proof of the logical soundness of {\coq} strongly lays on the property
+that any well-typed term must terminate. Hence, non-termination is
+usually a synonymous of inconsistency.
+
+%\paragraph{} In this case, the construction of a non-terminating
+%program comes from the so-called \textsl{negative occurrence} of
+%$\Lambda$ in the type of the constructor $\lambda$. In order to be
+%admissible for {\coq}, all the occurrences of the recursive type in its
+%own introduction rules must be positive, in the sense on the following
+%definition:
+%
+%\begin{enumerate}
+%\item $R$ is positive in $(R\;\vec{t})$;
+%\item $R$ is positive in $(x: A)C$ if it does not
+%occur in $A$ and $R$ is positive in $C$;
+%\item if $P\equiv (\vec{x}:\vec{T})Q$, then $R$ is positive in $(P
+%\rightarrow C)$ if $R$ does not occur in $\vec{T}$, $R$ is positive
+%in $C$, and either
+%\begin{enumerate}
+%\item $Q\equiv (R\;\vec{q})$ or
+%\item $Q\equiv (J\;\vec{t})$, \label{relax}
+% where $J$ is a recursive type, and for any term $t_i$ either :
+% \begin{enumerate}
+% \item $R$ does not occur in $t_i$, or
+% \item $t_i\equiv (z:\vec{Z})(R\;\vec{q})$, $R$ does not occur
+% in $\vec{Z}$, $t_i$ instantiates a general
+% parameter of $J$, and this parameter is positive in the
+% arguments of the constructors of $J$.
+% \end{enumerate}
+%\end{enumerate}
+%\end{enumerate}
+%\noindent Those types obtained by erasing option (\ref{relax}) in the
+%definition above are called \textsl{strictly positive} types.
+
+
+\subsubsection*{Remark} In this case, the construction of a non-terminating
+program comes from the so-called \textsl{negative occurrence} of
+\texttt{Lambda} in the argument of the constructor \texttt{lambda}.
+
+The reader will find in the Reference Manual a complete formal
+definition of the notions of \emph{positivity condition} and
+\emph{strict positivity} that an inductive definition must satisfy.
+
+
+%In order to be
+%admissible for {\coq}, the type $R$ must be positive in the types of the
+%arguments of its own introduction rules, in the sense on the following
+%definition:
+
+%\textbf{La définition du manuel de référence est plus complexe:
+%la recopier ou donner seulement des exemples?
+%}
+%\begin{enumerate}
+%\item $R$ is positive in $T$ if $R$ does not occur in $T$;
+%\item $R$ is positive in $(R\;\vec{t})$ if $R$ does not occur in $\vec{t}$;
+%\item $R$ is positive in $(x:A)C$ if it does not
+% occur in $A$ and $R$ is positive in $C$;
+%\item $R$ is positive in $(J\;\vec{t})$, \label{relax}
+% if $J$ is a recursive type, and for any term $t_i$ either :
+% \begin{enumerate}
+% \item $R$ does not occur in $t_i$, or
+% \item $R$ is positive in $t_i$, $t_i$ instantiates a general
+% parameter of $J$, and this parameter is positive in the
+% arguments of the constructors of $J$.
+% \end{enumerate}
+%\end{enumerate}
+
+%\noindent When we can show that $R$ is positive without using the item
+%(\ref{relax}) of the definition above, then we say that $R$ is
+%\textsl{strictly positive}.
+
+%\textbf{Changer le discours sur les ordinaux}
+
+Notice that the positivity condition does not forbid us to
+put functional recursive
+arguments in the constructors.
+
+For instance, let us consider the type of infinitely branching trees,
+with labels in \texttt{Z}.
+\begin{alltt}
+Require Import ZArith.
+
+Inductive itree : Set :=
+| ileaf : itree
+| inode : Z {\arrow} (nat {\arrow} itree) {\arrow} itree.
+\end{alltt}
+
+In this representation, the $i$-th child of a tree
+represented by ``~\texttt{inode $z$ $s$}~'' is obtained by applying
+the function $s$ to $i$.
+The following definitions show how to construct a tree with a single
+node, a tree of height 1 and a tree of height 2:
+
+\begin{alltt}
+Definition isingle l := inode l (fun i {\funarrow} ileaf).
+
+Definition t1 := inode 0 (fun n {\funarrow} isingle (Z_of_nat n)).
+
+Definition t2 :=
+ inode 0
+ (fun n : nat {\funarrow}
+ inode (Z_of_nat n)
+ (fun p {\funarrow} isingle (Z_of_nat (n*p)))).
+\end{alltt}
+
+
+Let us define a preorder on infinitely branching trees.
+ In order to compare two non-leaf trees,
+it is necessary to compare each of their children
+ without taking care of the order in which they
+appear:
+
+\begin{alltt}
+Inductive itree_le : itree{\arrow} itree {\arrow} Prop :=
+ | le_leaf : {\prodsym} t, itree_le ileaf t
+ | le_node : {\prodsym} l l' s s',
+ Zle l l' {\arrow}
+ ({\prodsym} i, {\exsym} j:nat, itree_le (s i) (s' j)){\arrow}
+ itree_le (inode l s) (inode l' s').
+
+\end{alltt}
+
+Notice that a call to the predicate \texttt{itree\_le} appears as
+a general parameter of the inductive type \texttt{ex} (see Sect.\ref{ex-def}).
+This kind of definition is accepted by {\coq}, but may lead to some
+difficulties, since the induction principle automatically
+generated by the system
+is not the most appropriate (see chapter 14 of~\cite{coqart} for a detailed
+explanation).
+
+
+The following definition, obtained by
+skolemising the
+proposition \linebreak $\forall\, i,\exists\, j,(\texttt{itree\_le}\;(s\;i)\;(s'\;j))$ in
+the type of \texttt{itree\_le}, does not present this problem:
+
+
+\begin{alltt}
+Inductive itree_le' : itree{\arrow} itree {\arrow} Prop :=
+ | le_leaf' : {\prodsym} t, itree_le' ileaf t
+ | le_node' : {\prodsym} l l' s s' g,
+ Zle l l' {\arrow}
+ ({\prodsym} i, itree_le' (s i) (s' (g i))) {\arrow}
+ itree_le' (inode l s) (inode l' s').
+
+\end{alltt}
+\iffalse
+\begin{alltt}
+Lemma t1_le'_t2 : itree_le' t1 t2.
+Proof.
+ unfold t1, t2.
+ constructor 2 with (fun i : nat {\funarrow} 2 * i).
+ auto with zarith.
+ unfold isingle;
+ intro i ; constructor 2 with (fun i :nat {\funarrow} i).
+ auto with zarith.
+ constructor .
+Qed.
+\end{alltt}
+\fi
+
+%In general, strictly positive definitions are preferable to only
+%positive ones. The reason is that it is sometimes difficult to derive
+%structural induction combinators for the latter ones. Such combinators
+%are automatically generated for strictly positive types, but not for
+%the only positive ones. Nevertheless, sometimes non-strictly positive
+%definitions provide a smarter or shorter way of declaring a recursive
+%type.
+
+Another example is the type of trees
+ of unbounded width, in which a recursive subterm
+\texttt{(ltree A)} instantiates the type of polymorphic lists:
+
+\begin{alltt}
+Require Import List.
+
+Inductive ltree (A:Set) : Set :=
+ lnode : A {\arrow} list (ltree A) {\arrow} ltree A.
+\end{alltt}
+
+This declaration can be transformed
+adding an extra type to the definition, as was done in Section
+\ref{MutuallyDependent}.
+
+
+\subsubsection{Impredicative Inductive Types}
+
+An inductive type $I$ inhabiting a universe $U$ is \textsl{predicative}
+if the introduction rules of $I$ do not make a universal
+quantification on a universe containing $U$. All the recursive types
+previously introduced are examples of predicative types. An example of
+an impredicative one is the following type:
+%\textsl{exT}, the dependent product
+%of a certain set (or proposition) $x$, and a proof of a property $P$
+%about $x$.
+
+%\begin{alltt}
+%Print exT.
+%\end{alltt}
+%\textbf{ttention, EXT c'est ex!}
+%\begin{alltt}
+%Check (exists P:Prop, P {\arrow} not P).
+%\end{alltt}
+
+%This type is useful for expressing existential quantification over
+%types, like ``there exists a proposition $x$ such that $(P\;x)$''
+%---written $(\textsl{EXT}\; x:Prop \mid (P\;x))$ in {\coq}. However,
+
+\begin{alltt}
+Inductive prop : Prop :=
+ prop_intro : Prop {\arrow} prop.
+\end{alltt}
+
+Notice
+that the constructor of this type can be used to inject any
+proposition --even itself!-- into the type.
+
+\begin{alltt}
+Check (prop_intro prop).\it
+prop_intro prop
+ : prop
+\end{alltt}
+
+A careless use of such a
+self-contained objects may lead to a variant of Burali-Forti's
+paradox. The construction of Burali-Forti's paradox is more
+complicated than Russel's one, so we will not describe it here, and
+point the interested reader to \cite{Bar98,Coq86}.
+
+
+Another example is the second order existential quantifier for propositions:
+
+\begin{alltt}
+Inductive ex_Prop (P : Prop {\arrow} Prop) : Prop :=
+ exP_intro : {\prodsym} X : Prop, P X {\arrow} ex_Prop P.
+\end{alltt}
+
+%\begin{alltt}
+%(*
+%Check (match prop_inject with (prop_intro p _) {\funarrow} p end).
+
+%Error: Incorrect elimination of "prop_inject" in the inductive type
+% ex
+%The elimination predicate ""fun _ : prop {\funarrow} Prop" has type
+% "prop {\arrow} Type"
+%It should be one of :
+% "Prop"
+
+%Elimination of an inductive object of sort : "Prop"
+%is not allowed on a predicate in sort : "Type"
+%because non-informative objects may not construct informative ones.
+
+%*)
+%Print prop_inject.
+
+%(*
+%prop_inject =
+%prop_inject = prop_intro prop (fun H : prop {\funarrow} H)
+% : prop
+%*)
+%\end{alltt}
+
+% \textbf{Et par ça?
+%}
+
+Notice that predicativity on sort \citecoq{Set} forbids us to build
+the following definitions.
+
+
+\begin{alltt}
+Inductive aSet : Set :=
+ aSet_intro: Set {\arrow} aSet.
+
+\it{}User error: Large non-propositional inductive types must be in Type
+\tt
+Inductive ex_Set (P : Set {\arrow} Prop) : Set :=
+ exS_intro : {\prodsym} X : Set, P X {\arrow} ex_Set P.
+
+\it{}User error: Large non-propositional inductive types must be in Type
+\end{alltt}
+
+Nevertheless, one can define types like \citecoq{aSet} and \citecoq{ex\_Set}, as inhabitants of \citecoq{Type}.
+
+\begin{alltt}
+Inductive ex_Set (P : Set {\arrow} Prop) : Type :=
+ exS_intro : {\prodsym} X : Set, P X {\arrow} ex_Set P.
+\end{alltt}
+
+In the following example, the inductive type \texttt{typ} can be defined,
+but the term associated with the interactive Definition of
+\citecoq{typ\_inject} is incompatible with {\coq}'s hierarchy of universes:
+
+
+\begin{alltt}
+Inductive typ : Type :=
+ typ_intro : Type {\arrow} typ.
+
+Definition typ_inject: typ.
+ split; exact typ.
+\it Proof completed
+
+\tt{}Defined.
+\it Error: Universe Inconsistency.
+\tt
+Abort.
+\end{alltt}
+
+One possible way of avoiding this new source of paradoxes is to
+restrict the kind of eliminations by case analysis that can be done on
+impredicative types. In particular, projections on those universes
+equal or bigger than the one inhabited by the impredicative type must
+be forbidden \cite{Coq86}. A consequence of this restriction is that it
+is not possible to define the first projection of the type
+``~\citecoq{ex\_Prop $P$}~'':
+\begin{alltt}
+Check (fun (P:Prop{\arrow}Prop)(p: ex_Prop P) {\funarrow}
+ match p with exP_intro X HX {\funarrow} X end).
+\it
+Error:
+Incorrect elimination of "p" in the inductive type
+"ex_Prop", the return type has sort "Type" while it should be
+"Prop"
+
+Elimination of an inductive object of sort "Prop"
+is not allowed on a predicate in sort "Type"
+because proofs can be eliminated only to build proofs.
+\end{alltt}
+
+%In order to explain why, let us consider for example the following
+%impredicative type \texttt{ALambda}.
+%\begin{alltt}
+%Inductive ALambda : Set :=
+% alambda : (A:Set)(A\arrow{}False)\arrow{}ALambda.
+%
+%Definition Lambda : Set := ALambda.
+%Definition lambda : (ALambda\arrow{}False)\arrow{}ALambda := (alambda ALambda).
+%Lemma CaseAL : (Q:Prop)ALambda\arrow{}((ALambda\arrow{}False)\arrow{}Q)\arrow{}Q.
+%\end{alltt}
+%
+%This type contains all the elements of the dangerous type $\Lambda$
+%described at the beginning of this section. Try to construct the
+%non-ending term $(\Delta\;\Delta)$ as an object of
+%\texttt{ALambda}. Why is it not possible?
+
+\subsubsection{Extraction Constraints}
+
+There is a final constraint on case analysis that is not motivated by
+the potential introduction of paradoxes, but for compatibility reasons
+with {\coq}'s extraction mechanism \refmancite{Appendix
+\ref{CamlHaskellExtraction}}. This mechanism is based on the
+classification of basic types into the universe $\Set$ of sets and the
+universe $\Prop$ of propositions. The objects of a type in the
+universe $\Set$ are considered as relevant for computation
+purposes. The objects of a type in $\Prop$ are considered just as
+formalised comments, not necessary for execution. The extraction
+mechanism consists in erasing such formal comments in order to obtain
+an executable program. Hence, in general, it is not possible to define
+an object in a set (that should be kept by the extraction mechanism)
+by case analysis of a proof (which will be thrown away).
+
+Nevertheless, this general rule has an exception which is important in
+practice: if the definition proceeds by case analysis on a proof of a
+\textsl{singleton proposition} or an empty type (\emph{e.g.} \texttt{False}),
+ then it is allowed. A singleton
+proposition is a non-recursive proposition with a single constructor
+$c$, all whose arguments are proofs. For example, the propositional
+equality and the conjunction of two propositions are examples of
+singleton propositions.
+
+%From the point of view of the extraction
+%mechanism, such types are isomorphic to a type containing a single
+%object $c$, so a definition $\Case{x}{c \Rightarrow b}$ is
+%directly replaced by $b$ as an extra optimisation.
+
+\subsubsection{Strong Case Analysis on Proofs}
+
+One could consider allowing
+ to define a proposition $Q$ by case
+analysis on the proofs of another recursive proposition $R$. As we
+will see in Section \ref{Discrimination}, this would enable one to prove that
+different introduction rules of $R$ construct different
+objects. However, this property would be in contradiction with the principle
+of excluded middle of classical logic, because this principle entails
+that the proofs of a proposition cannot be distinguished. This
+principle is not provable in {\coq}, but it is frequently introduced by
+the users as an axiom, for reasoning in classical logic. For this
+reason, the definition of propositions by case analysis on proofs is
+ not allowed in {\coq}.
+
+\begin{alltt}
+
+Definition comes_from_the_left (P Q:Prop)(H:P{\coqor}Q): Prop :=
+ match H with
+ | or_introl p {\funarrow} True
+ | or_intror q {\funarrow} False
+ end.
+\it
+Error:
+Incorrect elimination of "H" in the inductive type
+"or", the return type has sort "Type" while it should be
+"Prop"
+
+Elimination of an inductive object of sort "Prop"
+is not allowed on a predicate in sort "Type"
+because proofs can be eliminated only to build proofs.
+
+\end{alltt}
+
+On the other hand, if we replace the proposition $P {\coqor} Q$ with
+the informative type $\{P\}+\{Q\}$, the elimination is accepted:
+
+\begin{alltt}
+Definition comes_from_the_left_sumbool
+ (P Q:Prop)(x:\{P\} + \{Q\}): Prop :=
+ match x with
+ | left p {\funarrow} True
+ | right q {\funarrow} False
+ end.
+\end{alltt}
+
+
+\subsubsection{Summary of Constraints}
+
+To end with this section, the following table summarizes which
+universe $U_1$ may inhabit an object of type $Q$ defined by case
+analysis on $x:R$, depending on the universe $U_2$ inhabited by the
+inductive types $R$.\footnote{In the box indexed by $U_1=\citecoq{Type}$
+and $U_2=\citecoq{Set}$, the answer ``yes'' takes into account the
+predicativity of sort \citecoq{Set}. If you are working with the
+option ``impredicative-set'', you must put in this box the
+condition ``if $R$ is predicative''.}
+
+
+\begin{center}
+%%% displease hevea less by using * in multirow rather than \LL
+\renewcommand{\multirowsetup}{\centering}
+%\newlength{\LL}
+%\settowidth{\LL}{$x : R : U_2$}
+\begin{tabular}{|c|c|c|c|c|}
+\hline
+\multirow{5}*{$x : R : U_2$} &
+\multicolumn{4}{|c|}{$Q : U_1$}\\
+\hline
+& &\textsl{Set} & \textsl{Prop} & \textsl{Type}\\
+\cline{2-5}
+&\textsl{Set} & yes & yes & yes\\
+\cline{2-5}
+&\textsl{Prop} & if $R$ singleton & yes & no\\
+\cline{2-5}
+&\textsl{Type} & yes & yes & yes\\
+\hline
+\end{tabular}
+\end{center}
+
+\section{Some Proof Techniques Based on Case Analysis}
+\label{CaseTechniques}
+
+In this section we illustrate the use of case analysis as a proof
+principle, explaining the proof techniques behind three very useful
+{\coq} tactics, called \texttt{discriminate}, \texttt{injection} and
+\texttt{inversion}.
+
+\subsection{Discrimination of introduction rules}
+\label{Discrimination}
+
+In the informal semantics of recursive types described in Section
+\ref{Introduction} it was said that each of the introduction rules of a
+recursive type is considered as being different from all the others.
+It is possible to capture this fact inside the logical system using
+the propositional equality. We take as example the following theorem,
+stating that \textsl{O} constructs a natural number different
+from any of those constructed with \texttt{S}.
+
+\begin{alltt}
+Theorem S_is_not_O : {\prodsym} n, S n {\coqdiff} 0.
+\end{alltt}
+
+In order to prove this theorem, we first define a proposition by case
+analysis on natural numbers, so that the proposition is true for {\Z}
+and false for any natural number constructed with {\SUCC}. This uses
+the empty and singleton type introduced in Sections \ref{Introduction}.
+
+\begin{alltt}
+Definition Is_zero (x:nat):= match x with
+ | 0 {\funarrow} True
+ | _ {\funarrow} False
+ end.
+\end{alltt}
+
+\noindent Then, we prove the following lemma:
+
+\begin{alltt}
+Lemma O_is_zero : {\prodsym} m, m = 0 {\arrow} Is_zero m.
+Proof.
+ intros m H; subst m.
+\it{}
+================
+ Is_zero 0
+\tt{}
+simpl;trivial.
+Qed.
+\end{alltt}
+
+\noindent Finally, the proof of \texttt{S\_is\_not\_O} follows by the
+application of the previous lemma to $S\;n$.
+
+
+\begin{alltt}
+
+ red; intros n Hn.
+ \it{}
+ n : nat
+ Hn : S n = 0
+ ============================
+ False \tt
+
+ apply O_is_zero with (m := S n).
+ assumption.
+Qed.
+\end{alltt}
+
+
+The tactic \texttt{discriminate} \refmancite{Section \ref{Discriminate}} is
+a special-purpose tactic for proving disequalities between two
+elements of a recursive type introduced by different constructors. It
+generalizes the proof method described here for natural numbers to any
+[co]-inductive type. This tactic is also capable of proving disequalities
+where the difference is not in the constructors at the head of the
+terms, but deeper inside them. For example, it can be used to prove
+the following theorem:
+
+\begin{alltt}
+Theorem disc2 : {\prodsym} n, S (S n) {\coqdiff} 1.
+Proof.
+ intros n Hn; discriminate.
+Qed.
+\end{alltt}
+
+When there is an assumption $H$ in the context stating a false
+equality $t_1=t_2$, \texttt{discriminate} solves the goal by first
+proving $(t_1\not =t_2)$ and then reasoning by absurdity with respect
+to $H$:
+
+\begin{alltt}
+Theorem disc3 : {\prodsym} n, S (S n) = 0 {\arrow} {\prodsym} Q:Prop, Q.
+Proof.
+ intros n Hn Q.
+ discriminate.
+Qed.
+\end{alltt}
+
+\noindent In this case, the proof proceeds by absurdity with respect
+to the false equality assumed, whose negation is proved by
+discrimination.
+
+\subsection{Injectiveness of introduction rules}
+
+Another useful property about recursive types is the
+\textsl{injectiveness} of introduction rules, i.e., that whenever two
+objects were built using the same introduction rule, then this rule
+should have been applied to the same element. This can be stated
+formally using the propositional equality:
+
+\begin{alltt}
+Theorem inj : {\prodsym} n m, S n = S m {\arrow} n = m.
+Proof.
+\end{alltt}
+
+\noindent This theorem is just a corollary of a lemma about the
+predecessor function:
+
+\begin{alltt}
+ Lemma inj_pred : {\prodsym} n m, n = m {\arrow} pred n = pred m.
+ Proof.
+ intros n m eq_n_m.
+ rewrite eq_n_m.
+ trivial.
+ Qed.
+\end{alltt}
+\noindent Once this lemma is proven, the theorem follows directly
+from it:
+\begin{alltt}
+ intros n m eq_Sn_Sm.
+ apply inj_pred with (n:= S n) (m := S m); assumption.
+Qed.
+\end{alltt}
+
+This proof method is implemented by the tactic \texttt{injection}
+\refmancite{Section \ref{injection}}. This tactic is applied to
+a term $t$ of type ``~$c\;{t_1}\;\dots\;t_n = c\;t'_1\;\dots\;t'_n$~'', where $c$ is some constructor of
+an inductive type. The tactic \texttt{injection} is applied as deep as
+possible to derive the equality of all pairs of subterms of $t_i$ and $t'_i$
+placed in the same position. All these equalities are put as antecedents
+of the current goal.
+
+
+
+Like \texttt{discriminate}, the tactic \citecoq{injection}
+can be also applied if $x$ does not
+occur in a direct sub-term, but somewhere deeper inside it. Its
+application may leave some trivial goals that can be easily solved
+using the tactic \texttt{trivial}.
+
+\begin{alltt}
+
+ Lemma list_inject : {\prodsym} (A:Type)(a b :A)(l l':list A),
+ a :: b :: l = b :: a :: l' {\arrow} a = b {\coqand} l = l'.
+Proof.
+ intros A a b l l' e.
+
+
+\it
+ e : a :: b :: l = b :: a :: l'
+ ============================
+ a = b {\coqand} l = l'
+\tt
+ injection e.
+\it
+ ============================
+ l = l' {\arrow} b = a {\arrow} a = b {\arrow} a = b {\coqand} l = l'
+
+\tt{} auto.
+Qed.
+\end{alltt}
+
+\subsection{Inversion Techniques}\label{inversion}
+
+In section \ref{DependentCase}, we motivated the rule of dependent case
+analysis as a way of internalizing the informal equalities $n=O$ and
+$n=\SUCC\;p$ associated to each case. This internalisation
+consisted in instantiating $n$ with the corresponding term in the type
+of each branch. However, sometimes it could be better to internalise
+these equalities as extra hypotheses --for example, in order to use
+the tactics \texttt{rewrite}, \texttt{discriminate} or
+\texttt{injection} presented in the previous sections. This is
+frequently the case when the element analysed is denoted by a term
+which is not a variable, or when it is an object of a particular
+instance of a recursive family of types. Consider for example the
+following theorem:
+
+\begin{alltt}
+Theorem not_le_Sn_0 : {\prodsym} n:nat, ~ (S n {\coqle} 0).
+\end{alltt}
+
+\noindent Intuitively, this theorem should follow by case analysis on
+the hypothesis $H:(S\;n\;\leq\;\Z)$, because no introduction rule allows
+to instantiate the arguments of \citecoq{le} with respectively a successor
+and zero. However, there
+is no way of capturing this with the typing rule for case analysis
+presented in section \ref{Introduction}, because it does not take into
+account what particular instance of the family the type of $H$ is.
+Let us try it:
+\begin{alltt}
+Proof.
+ red; intros n H; case H.
+\it 2 subgoals
+
+ n : nat
+ H : S n {\coqle} 0
+ ============================
+ False
+
+subgoal 2 is:
+ {\prodsym} m : nat, S n {\coqle} m {\arrow} False
+\tt
+Undo.
+\end{alltt}
+
+\noindent What is necessary here is to make available the equalities
+``~$\SUCC\;n = \Z$~'' and ``~$\SUCC\;m = \Z$~''
+ as extra hypotheses of the
+branches, so that the goal can be solved using the
+\texttt{Discriminate} tactic. In order to obtain the desired
+equalities as hypotheses, let us prove an auxiliary lemma, that our
+theorem is a corollary of:
+
+\begin{alltt}
+ Lemma not_le_Sn_0_with_constraints :
+ {\prodsym} n p , S n {\coqle} p {\arrow} p = 0 {\arrow} False.
+ Proof.
+ intros n p H; case H .
+\it
+2 subgoals
+
+ n : nat
+ p : nat
+ H : S n {\coqle} p
+ ============================
+ S n = 0 {\arrow} False
+
+subgoal 2 is:
+ {\prodsym} m : nat, S n {\coqle} m {\arrow} S m = 0 {\arrow} False
+\tt
+ intros;discriminate.
+ intros;discriminate.
+Qed.
+\end{alltt}
+\noindent Our main theorem can now be solved by an application of this lemma:
+\begin{alltt}
+Show.
+\it
+2 subgoals
+
+ n : nat
+ p : nat
+ H : S n {\coqle} p
+ ============================
+ S n = 0 {\arrow} False
+
+subgoal 2 is:
+ {\prodsym} m : nat, S n {\coqle} m {\arrow} S m = 0 {\arrow} False
+\tt
+ eapply not_le_Sn_0_with_constraints; eauto.
+Qed.
+\end{alltt}
+
+
+The general method to address such situations consists in changing the
+goal to be proven into an implication, introducing as preconditions
+the equalities needed to eliminate the cases that make no
+sense. This proof technique is implemented by the tactic
+\texttt{inversion} \refmancite{Section \ref{Inversion}}. In order
+to prove a goal $G\;\vec{q}$ from an object of type $R\;\vec{t}$,
+this tactic automatically generates a lemma $\forall, \vec{x}.
+(R\;\vec{x}) \rightarrow \vec{x}=\vec{t}\rightarrow \vec{B}\rightarrow
+(G\;\vec{q})$, where the list of propositions $\vec{B}$ correspond to
+the subgoals that cannot be directly proven using
+\texttt{discriminate}. This lemma can either be saved for later
+use, or generated interactively. In this latter case, the subgoals
+yielded by the tactic are the hypotheses $\vec{B}$ of the lemma. If the
+lemma has been stored, then the tactic \linebreak
+ ``~\citecoq{inversion \dots using \dots}~'' can be
+used to apply it.
+
+Let us show both techniques on our previous example:
+
+\subsubsection{Interactive mode}
+
+\begin{alltt}
+Theorem not_le_Sn_0' : {\prodsym} n:nat, ~ (S n {\coqle} 0).
+Proof.
+ red; intros n H ; inversion H.
+Qed.
+\end{alltt}
+
+
+\subsubsection{Static mode}
+
+\begin{alltt}
+
+Derive Inversion le_Sn_0_inv with ({\prodsym} n :nat, S n {\coqle} 0).
+Theorem le_Sn_0'' : {\prodsym} n p : nat, ~ S n {\coqle} 0 .
+Proof.
+ intros n p H;
+ inversion H using le_Sn_0_inv.
+Qed.
+\end{alltt}
+
+
+In the example above, all the cases are solved using discriminate, so
+there remains no subgoal to be proven (i.e. the list $\vec{B}$ is
+empty). Let us present a second example, where this list is not empty:
+
+
+\begin{alltt}
+TTheorem le_reverse_rules :
+ {\prodsym} n m:nat, n {\coqle} m {\arrow}
+ n = m {\coqor}
+ {\exsym} p, n {\coqle} p {\coqand} m = S p.
+Proof.
+ intros n m H; inversion H.
+\it
+2 subgoals
+
+
+
+
+ n : nat
+ m : nat
+ H : n {\coqle} m
+ H0 : n = m
+ ============================
+ m = m {\coqor} ({\exsym} p : nat, m {\coqle} p {\coqand} m = S p)
+
+subgoal 2 is:
+ n = S m0 {\coqor} ({\exsym} p : nat, n {\coqle} p {\coqand} S m0 = S p)
+\tt
+ left;trivial.
+ right; exists m0; split; trivial.
+\it
+Proof completed
+\end{alltt}
+
+This example shows how this tactic can be used to ``reverse'' the
+introduction rules of a recursive type, deriving the possible premises
+that could lead to prove a given instance of the predicate. This is
+why these tactics are called \texttt{inversion} tactics: they go back
+from conclusions to premises.
+
+The hypotheses corresponding to the propositional equalities are not
+needed in this example, since the tactic does the necessary rewriting
+to solve the subgoals. When the equalities are no longer needed after
+the inversion, it is better to use the tactic
+\texttt{Inversion\_clear}. This variant of the tactic clears from the
+context all the equalities introduced.
+
+\begin{alltt}
+Restart.
+ intros n m H; inversion_clear H.
+\it
+\it
+
+ n : nat
+ m : nat
+ ============================
+ m = m {\coqor} ({\exsym} p : nat, m {\coqle} p {\coqand} m = S p)
+\tt
+ left;trivial.
+\it
+ n : nat
+ m : nat
+ m0 : nat
+ H0 : n {\coqle} m0
+ ============================
+ n = S m0 {\coqor} ({\exsym} p : nat, n {\coqle} p {\coqand} S m0 = S p)
+\tt
+ right; exists m0; split; trivial.
+Qed.
+\end{alltt}
+
+
+%This proof technique works in most of the cases, but not always. In
+%particular, it could not if the list $\vec{t}$ contains a term $t_j$
+%whose type $T$ depends on a previous term $t_i$, with $i<j$. Remark
+%that if this is the case, the propositional equality $x_j=t_j$ is not
+%well-typed, since $x_j:T(x_i)$ but $t_j:T(t_i)$, and both types are
+%not convertible (otherwise, the problem could be solved using the
+%tactic \texttt{Case}).
+
+
+
+\begin{exercise}
+Consider the following language of arithmetic expression, and
+its operational semantics, described by a set of rewriting rules.
+%\textbf{J'ai enlevé une règle de commutativité de l'addition qui
+%me paraissait bizarre du point de vue de la sémantique opérationnelle}
+
+\begin{alltt}
+Inductive ArithExp : Set :=
+ | Zero : ArithExp
+ | Succ : ArithExp {\arrow} ArithExp
+ | Plus : ArithExp {\arrow} ArithExp {\arrow} ArithExp.
+
+Inductive RewriteRel : ArithExp {\arrow} ArithExp {\arrow} Prop :=
+ | RewSucc : {\prodsym} e1 e2 :ArithExp,
+ RewriteRel e1 e2 {\arrow}
+ RewriteRel (Succ e1) (Succ e2)
+ | RewPlus0 : {\prodsym} e:ArithExp,
+ RewriteRel (Plus Zero e) e
+ | RewPlusS : {\prodsym} e1 e2:ArithExp,
+ RewriteRel e1 e2 {\arrow}
+ RewriteRel (Plus (Succ e1) e2)
+ (Succ (Plus e1 e2)).
+
+\end{alltt}
+\begin{enumerate}
+\item Prove that \texttt{Zero} cannot be rewritten any further.
+\item Prove that an expression of the form ``~$\texttt{Succ}\;e$~'' is always
+rewritten
+into an expression of the same form.
+\end{enumerate}
+\end{exercise}
+
+%Theorem zeroNotCompute : (e:ArithExp)~(RewriteRel Zero e).
+%Intro e.
+%Red.
+%Intro H.
+%Inversion_clear H.
+%Defined.
+%Theorem evalPlus :
+% (e1,e2:ArithExp)
+% (RewriteRel (Succ e1) e2)\arrow{}(EX e3 : ArithExp | e2=(Succ e3)).
+%Intros e1 e2 H.
+%Inversion_clear H.
+%Exists e3;Reflexivity.
+%Qed.
+
+
+\section{Inductive Types and Structural Induction}
+\label{StructuralInduction}
+
+Elements of inductive types are well-founded with
+respect to the structural order induced by the constructors of the
+type. In addition to case analysis, this extra hypothesis about
+well-foundedness justifies a stronger elimination rule for them, called
+\textsl{structural induction}. This form of elimination consists in
+defining a value ``~$f\;x$~'' from some element $x$ of the inductive type
+$I$, assuming that values have been already associated in the same way
+to the sub-parts of $x$ of type $I$.
+
+
+Definitions by structural induction are expressed through the
+\texttt{Fixpoint} command \refmancite{Section
+\ref{Fixpoint}}. This command is quite close to the
+\texttt{let-rec} construction of functional programming languages.
+For example, the following definition introduces the addition of two
+natural numbers (already defined in the Standard Library:)
+
+\begin{alltt}
+Fixpoint plus (n p:nat) \{struct n\} : nat :=
+ match n with
+ | 0 {\funarrow} p
+ | S m {\funarrow} S (plus m p)
+ end.
+\end{alltt}
+
+The definition is by structural induction on the first argument of the
+function. This is indicated by the ``~\citecoq{\{struct n\}}~''
+directive in the function's header\footnote{This directive is optional
+in the case of a function of a single argument}.
+ In
+order to be accepted, the definition must satisfy a syntactical
+condition, called the \textsl{guardedness condition}. Roughly
+speaking, this condition constrains the arguments of a recursive call
+to be pattern variables, issued from a case analysis of the formal
+argument of the function pointed by the \texttt{struct} directive.
+ In the case of the
+function \texttt{plus}, the argument \texttt{m} in the recursive call is a
+pattern variable issued from a case analysis of \texttt{n}. Therefore, the
+definition is accepted.
+
+Notice that we could have defined the addition with structural induction
+on its second argument:
+\begin{alltt}
+Fixpoint plus' (n p:nat) \{struct p\} : nat :=
+ match p with
+ | 0 {\funarrow} n
+ | S q {\funarrow} S (plus' n q)
+ end.
+\end{alltt}
+
+%This notation is useful when defining a function whose decreasing
+%argument has a dependent type. As an example, consider the following
+%recursivly defined proof of the theorem
+%$(n,m:\texttt{nat})n<m \rightarrow (S\;n)<(S\;m)$:
+%\begin{alltt}
+%Fixpoint lt_n_S [n,m:nat;p:(lt n m)] : (lt (S n) (S m)) :=
+% <[n0:nat](lt (S n) (S n0))>
+% Cases p of
+% lt_intro1 {\funarrow} (lt_intro1 (S n))
+% | (lt_intro2 m1 p2) {\funarrow} (lt_intro2 (S n) (S m1) (lt_n_S n m1 p2))
+% end.
+%\end{alltt}
+
+%The guardedness condition must be satisfied only by the last argument
+%of the enclosed list. For example, the following declaration is an
+%alternative way of defining addition:
+
+%\begin{alltt}
+%Reset add.
+%Fixpoint add [n:nat] : nat\arrow{}nat :=
+% Cases n of
+% O {\funarrow} [x:nat]x
+% | (S m) {\funarrow} [x:nat](add m (S x))
+% end.
+%\end{alltt}
+
+In the following definition of addition,
+the second argument of {\tt plus{'}{'}} grows at each
+recursive call. However, as the first one always decreases, the
+definition is sound.
+\begin{alltt}
+Fixpoint plus'' (n p:nat) \{struct n\} : nat :=
+ match n with
+ | 0 {\funarrow} p
+ | S m {\funarrow} plus'' m (S p)
+ end.
+\end{alltt}
+
+ Moreover, the argument in the recursive call
+could be a deeper component of $n$. This is the case in the following
+definition of a boolean function determining whether a number is even
+or odd:
+
+\begin{alltt}
+Fixpoint even_test (n:nat) : bool :=
+ match n
+ with 0 {\funarrow} true
+ | 1 {\funarrow} false
+ | S (S p) {\funarrow} even_test p
+ end.
+\end{alltt}
+
+Mutually dependent definitions by structural induction are also
+allowed. For example, the previous function \textsl{even} could alternatively
+be defined using an auxiliary function \textsl{odd}:
+
+\begin{alltt}
+Reset even_test.
+
+
+
+Fixpoint even_test (n:nat) : bool :=
+ match n
+ with
+ | 0 {\funarrow} true
+ | S p {\funarrow} odd_test p
+ end
+with odd_test (n:nat) : bool :=
+ match n
+ with
+ | 0 {\funarrow} false
+ | S p {\funarrow} even_test p
+ end.
+\end{alltt}
+
+%\begin{exercise}
+%Define a function by structural induction that computes the number of
+%nodes of a tree structure defined in page \pageref{Forest}.
+%\end{exercise}
+
+Definitions by structural induction are computed
+ only when they are applied, and the decreasing argument
+is a term having a constructor at the head. We can check this using
+the \texttt{Eval} command, which computes the normal form of a well
+typed term.
+
+\begin{alltt}
+Eval simpl in even_test.
+\it
+ = even_test
+ : nat {\arrow} bool
+\tt
+Eval simpl in (fun x : nat {\funarrow} even x).
+\it
+ = fun x : nat {\funarrow} even x
+ : nat {\arrow} Prop
+\tt
+Eval simpl in (fun x : nat => plus 5 x).
+\it
+ = fun x : nat {\funarrow} S (S (S (S (S x))))
+
+\tt
+Eval simpl in (fun x : nat {\funarrow} even_test (plus 5 x)).
+\it
+ = fun x : nat {\funarrow} odd_test x
+ : nat {\arrow} bool
+\tt
+Eval simpl in (fun x : nat {\funarrow} even_test (plus x 5)).
+\it
+ = fun x : nat {\funarrow} even_test (x + 5)
+ : nat {\arrow} bool
+\end{alltt}
+
+
+%\begin{exercise}
+%Prove that the second definition of even satisfies the following
+%theorem:
+%\begin{verbatim}
+%Theorem unfold_even :
+% (x:nat)
+% (even x)= (Cases x of
+% O {\funarrow} true
+% | (S O) {\funarrow} false
+% | (S (S m)) {\funarrow} (even m)
+% end).
+%\end{verbatim}
+%\end{exercise}
+
+\subsection{Proofs by Structural Induction}
+
+The principle of structural induction can be also used in order to
+define proofs, that is, to prove theorems. Let us call an
+\textsl{elimination combinator} any function that, given a predicate
+$P$, defines a proof of ``~$P\;x$~'' by structural induction on $x$. In
+{\coq}, the principle of proof by induction on natural numbers is a
+particular case of an elimination combinator. The definition of this
+combinator depends on three general parameters: the predicate to be
+proven, the base case, and the inductive step:
+
+\begin{alltt}
+Section Principle_of_Induction.
+Variable P : nat {\arrow} Prop.
+Hypothesis base_case : P 0.
+Hypothesis inductive_step : {\prodsym} n:nat, P n {\arrow} P (S n).
+Fixpoint nat_ind (n:nat) : (P n) :=
+ match n return P n with
+ | 0 {\funarrow} base_case
+ | S m {\funarrow} inductive_step m (nat_ind m)
+ end.
+
+End Principle_of_Induction.
+\end{alltt}
+
+As this proof principle is used very often, {\coq} automatically generates it
+when an inductive type is introduced. Similar principles
+\texttt{nat\_rec} and \texttt{nat\_rect} for defining objects in the
+universes $\Set$ and $\Type$ are also automatically generated
+\footnote{In fact, whenever possible, {\coq} generates the
+principle \texttt{$I$\_rect}, then derives from it the
+weaker principles \texttt{$I$\_ind} and \texttt{$I$\_rec}.
+If some principle has to be defined by hand, the user may try
+to build \texttt{$I$\_rect} (if possible). Thanks to {\coq}'s conversion
+rule, this principle can be used directly to build proofs and/or
+programs.}. The
+command \texttt{Scheme} \refmancite{Section \ref{Scheme}} can be
+used to generate an elimination combinator from certain parameters,
+like the universe that the defined objects must inhabit, whether the
+case analysis in the definitions must be dependent or not, etc. For
+example, it can be used to generate an elimination combinator for
+reasoning on even natural numbers from the mutually dependent
+predicates introduced in page \pageref{Even}. We do not display the
+combinators here by lack of space, but you can see them using the
+\texttt{Print} command.
+
+\begin{alltt}
+Scheme Even_induction := Minimality for even Sort Prop
+with Odd_induction := Minimality for odd Sort Prop.
+\end{alltt}
+
+\begin{alltt}
+Theorem even_plus_four : {\prodsym} n:nat, even n {\arrow} even (4+n).
+Proof.
+ intros n H.
+ elim H using Even_induction with (P0 := fun n {\funarrow} odd (4+n));
+ simpl;repeat constructor;assumption.
+Qed.
+\end{alltt}
+
+Another example of an elimination combinator is the principle
+of double induction on natural numbers, introduced by the following
+definition:
+
+\begin{alltt}
+Section Principle_of_Double_Induction.
+Variable P : nat {\arrow} nat {\arrow}Prop.
+Hypothesis base_case1 : {\prodsym} m:nat, P 0 m.
+Hypothesis base_case2 : {\prodsym} n:nat, P (S n) 0.
+Hypothesis inductive_step : {\prodsym} n m:nat, P n m {\arrow}
+ \,\, P (S n) (S m).
+
+Fixpoint nat_double_ind (n m:nat)\{struct n\} : P n m :=
+ match n, m return P n m with
+ | 0 , x {\funarrow} base_case1 x
+ | (S x), 0 {\funarrow} base_case2 x
+ | (S x), (S y) {\funarrow} inductive_step x y (nat_double_ind x y)
+ end.
+End Principle_of_Double_Induction.
+\end{alltt}
+
+Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Type$,
+another combinator for constructing
+(certified) programs, \texttt{nat\_double\_rect}, can be defined in exactly the same way.
+This definition is left as an exercise.\label{natdoublerect}
+
+\iffalse
+\begin{alltt}
+Section Principle_of_Double_Recursion.
+Variable P : nat {\arrow} nat {\arrow} Type.
+Hypothesis base_case1 : {\prodsym} x:nat, P 0 x.
+Hypothesis base_case2 : {\prodsym} x:nat, P (S x) 0.
+Hypothesis inductive_step : {\prodsym} n m:nat, P n m {\arrow} P (S n) (S m).
+Fixpoint nat_double_rect (n m:nat)\{struct n\} : P n m :=
+ match n, m return P n m with
+ 0 , x {\funarrow} base_case1 x
+ | (S x), 0 {\funarrow} base_case2 x
+ | (S x), (S y) {\funarrow} inductive_step x y (nat_double_rect x y)
+ end.
+End Principle_of_Double_Recursion.
+\end{alltt}
+\fi
+For instance the function computing the minimum of two natural
+numbers can be defined in the following way:
+
+\begin{alltt}
+Definition min : nat {\arrow} nat {\arrow} nat :=
+ nat_double_rect (fun (x y:nat) {\funarrow} nat)
+ (fun (x:nat) {\funarrow} 0)
+ (fun (y:nat) {\funarrow} 0)
+ (fun (x y r:nat) {\funarrow} S r).
+Eval compute in (min 5 8).
+\it
+= 5 : nat
+\end{alltt}
+
+
+%\begin{exercise}
+%
+%Define the combinator \texttt{nat\_double\_rec}, and apply it
+%to give another definition of \citecoq{le\_lt\_dec} (using the theorems
+%of the \texttt{Arith} library).
+%\end{exercise}
+
+\subsection{Using Elimination Combinators.}
+The tactic \texttt{apply} can be used to apply one of these proof
+principles during the development of a proof.
+
+\begin{alltt}
+Lemma not_circular : {\prodsym} n:nat, n {\coqdiff} S n.
+Proof.
+ intro n.
+ apply nat_ind with (P:= fun n {\funarrow} n {\coqdiff} S n).
+\it
+
+
+
+2 subgoals
+
+ n : nat
+ ============================
+ 0 {\coqdiff} 1
+
+
+subgoal 2 is:
+ {\prodsym} n0 : nat, n0 {\coqdiff} S n0 {\arrow} S n0 {\coqdiff} S (S n0)
+
+\tt
+ discriminate.
+ red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
+Qed.
+\end{alltt}
+
+The tactic \texttt{elim} \refmancite{Section \ref{Elim}} is a
+refinement of \texttt{apply}, specially designed for the application
+of elimination combinators. If $t$ is an object of an inductive type
+$I$, then ``~\citecoq{elim $t$}~'' tries to find an abstraction $P$ of the
+current goal $G$ such that $(P\;t)\equiv G$. Then it solves the goal
+applying ``~$I\texttt{\_ind}\;P$~'', where $I$\texttt{\_ind} is the
+combinator associated to $I$. The different cases of the induction
+then appear as subgoals that remain to be solved.
+In the previous proof, the tactic call ``~\citecoq{apply nat\_ind with (P:= fun n {\funarrow} n {\coqdiff} S n)}~'' can simply be replaced with ``~\citecoq{elim n}~''.
+
+The option ``~\citecoq{\texttt{elim} $t$ \texttt{using} $C$}~''
+ allows to use a
+derived combinator $C$ instead of the default one. Consider the
+following theorem, stating that equality is decidable on natural
+numbers:
+
+\label{iseqpage}
+\begin{alltt}
+Lemma eq_nat_dec : {\prodsym} n p:nat, \{n=p\}+\{n {\coqdiff} p\}.
+Proof.
+ intros n p.
+\end{alltt}
+
+Let us prove this theorem using the combinator \texttt{nat\_double\_rect}
+of section~\ref{natdoublerect}. The example also illustrates how
+\texttt{elim} may sometimes fail in finding a suitable abstraction $P$
+of the goal. Note that if ``~\texttt{elim n}~''
+ is used directly on the
+goal, the result is not the expected one.
+
+\vspace{12pt}
+
+%\pagebreak
+\begin{alltt}
+ elim n using nat_double_rect.
+\it
+4 subgoals
+
+ n : nat
+ p : nat
+ ============================
+ {\prodsym} x : nat, \{x = p\} + \{x {\coqdiff} p\}
+
+subgoal 2 is:
+ nat {\arrow} \{0 = p\} + \{0 {\coqdiff} p\}
+
+subgoal 3 is:
+ nat {\arrow} {\prodsym} m : nat, \{m = p\} + \{m {\coqdiff} p\} {\arrow} \{S m = p\} + \{S m {\coqdiff} p\}
+
+subgoal 4 is:
+ nat
+\end{alltt}
+
+The four sub-goals obtained do not correspond to the premises that
+would be expected for the principle \texttt{nat\_double\_rec}. The
+problem comes from the fact that
+this principle for eliminating $n$
+has a universally quantified formula as conclusion, which confuses
+\texttt{elim} about the right way of abstracting the goal.
+
+%In effect, let us consider the type of the goal before the call to
+%\citecoq{elim}: ``~\citecoq{\{n = p\} + \{n {\coqdiff} p\}}~''.
+
+%Among all the abstractions that can be built by ``~\citecoq{elim n}~''
+%let us consider this one
+%$P=$\citecoq{fun n :nat {\funarrow} fun q : nat {\funarrow} {\{q= p\} + \{q {\coqdiff} p\}}}.
+%It is easy to verify that
+%$P$ has type \citecoq{nat {\arrow} nat {\arrow} Set}, and that, if some
+%$q:\citecoq{nat}$ is given, then $P\;q\;$ matches the current goal.
+%Then applying \citecoq{nat\_double\_rec} with $P$ generates
+%four goals, corresponding to
+
+
+
+
+Therefore,
+in this case the abstraction must be explicited using the
+\texttt{pattern} tactic. Once the right abstraction is provided, the rest of
+the proof is immediate:
+
+\begin{alltt}
+Undo.
+ pattern p,n.
+\it
+ n : nat
+ p : nat
+ ============================
+ (fun n0 n1 : nat {\funarrow} \{n1 = n0\} + \{n1 {\coqdiff} n0\}) p n
+\tt
+ elim n using nat_double_rec.
+\it
+3 subgoals
+
+ n : nat
+ p : nat
+ ============================
+ {\prodsym} x : nat, \{x = 0\} + \{x {\coqdiff} 0\}
+
+subgoal 2 is:
+ {\prodsym} x : nat, \{0 = S x\} + \{0 {\coqdiff} S x\}
+subgoal 3 is:
+ {\prodsym} n0 m : nat, \{m = n0\} + \{m {\coqdiff} n0\} {\arrow} \{S m = S n0\} + \{S m {\coqdiff} S n0\}
+
+\tt
+ destruct x; auto.
+ destruct x; auto.
+ intros n0 m H; case H.
+ intro eq; rewrite eq ; auto.
+ intro neg; right; red ; injection 1; auto.
+Defined.
+\end{alltt}
+
+
+Notice that the tactic ``~\texttt{decide equality}~''
+\refmancite{Section\ref{DecideEquality}} generalises the proof
+above to a large class of inductive types. It can be used for proving
+a proposition of the form
+$\forall\,(x,y:R),\{x=y\}+\{x{\coqdiff}y\}$, where $R$ is an inductive datatype
+all whose constructors take informative arguments ---like for example
+the type {\nat}:
+
+\begin{alltt}
+Definition eq_nat_dec' : {\prodsym} n p:nat, \{n=p\} + \{n{\coqdiff}p\}.
+ decide equality.
+Defined.
+\end{alltt}
+
+\begin{exercise}
+\begin{enumerate}
+\item Define a recursive function of name \emph{nat2itree}
+that maps any natural number $n$ into an infinitely branching
+tree of height $n$.
+\item Provide an elimination combinator for these trees.
+\item Prove that the relation \citecoq{itree\_le} is a preorder
+(i.e. reflexive and transitive).
+\end{enumerate}
+\end{exercise}
+
+\begin{exercise} \label{zeroton}
+Define the type of lists, and a predicate ``being an ordered list''
+using an inductive family. Then, define the function
+$(from\;n)=0::1\;\ldots\; n::\texttt{nil}$ and prove that it always generates an
+ordered list.
+\end{exercise}
+
+\begin{exercise}
+Prove that \citecoq{le' n p} and \citecoq{n $\leq$ p} are logically equivalent
+for all n and p. (\citecoq{le'} is defined in section \ref{parameterstuff}).
+\end{exercise}
+
+
+\subsection{Well-founded Recursion}
+\label{WellFoundedRecursion}
+
+Structural induction is a strong elimination rule for inductive types.
+This method can be used to define any function whose termination is
+a consequence of the well-foundedness of a certain order relation $R$ decreasing
+at each recursive call. What makes this principle so strong is the
+possibility of reasoning by structural induction on the proof that
+certain $R$ is well-founded. In order to illustrate this we have
+first to introduce the predicate of accessibility.
+
+\begin{alltt}
+Print Acc.
+\it
+Inductive Acc (A : Type) (R : A {\arrow} A {\arrow} Prop) (x:A) : Prop :=
+ Acc_intro : ({\prodsym} y : A, R y x {\arrow} Acc R y) {\arrow} Acc R x
+For Acc: Argument A is implicit
+For Acc_intro: Arguments A, R are implicit
+
+\dots
+\end{alltt}
+
+\noindent This inductive predicate characterizes those elements $x$ of
+$A$ such that any descending $R$-chain $\ldots x_2\;R\;x_1\;R\;x$
+starting from $x$ is finite. A well-founded relation is a relation
+such that all the elements of $A$ are accessible.
+\emph{Notice the use of parameter $x$ (see Section~\ref{parameterstuff}, page
+\pageref{parameterstuff}).}
+
+Consider now the problem of representing in {\coq} the following ML
+function $\textsl{div}(x,y)$ on natural numbers, which computes
+$\lceil\frac{x}{y}\rceil$ if $y>0$ and yields $x$ otherwise.
+
+\begin{verbatim}
+let rec div x y =
+ if x = 0 then 0
+ else if y = 0 then x
+ else (div (x-y) y)+1;;
+\end{verbatim}
+
+
+The equality test on natural numbers can be implemented using the
+function \textsl{eq\_nat\_dec} that is defined page \pageref{iseqpage}. Giving $x$ and
+$y$, this function yields either the value $(\textsl{left}\;p)$ if
+there exists a proof $p:x=y$, or the value $(\textsl{right}\;q)$ if
+there exists $q:a\not = b$. The subtraction function is already
+defined in the library \citecoq{Minus}.
+
+Hence, direct translation of the ML function \textsl{div} would be:
+
+\begin{alltt}
+Require Import Minus.
+
+Fixpoint div (x y:nat)\{struct x\}: nat :=
+ if eq_nat_dec x 0
+ then 0
+ else if eq_nat_dec y 0
+ then x
+ else S (div (x-y) y).
+
+\it Error:
+Recursive definition of div is ill-formed.
+In environment
+div : nat {\arrow} nat {\arrow} nat
+x : nat
+y : nat
+_ : x {\coqdiff} 0
+_ : y {\coqdiff} 0
+
+Recursive call to div has principal argument equal to
+"x - y"
+instead of a subterm of x
+\end{alltt}
+
+
+The program \texttt{div} is rejected by {\coq} because it does not verify
+the syntactical condition to ensure termination. In particular, the
+argument of the recursive call is not a pattern variable issued from a
+case analysis on $x$.
+We would have the same problem if we had the directive
+``~\citecoq{\{struct y\}}~'' instead of ``~\citecoq{\{struct x\}}~''.
+However, we know that this program always
+stops. One way to justify its termination is to define it by
+structural induction on a proof that $x$ is accessible trough the
+relation $<$. Notice that any natural number $x$ is accessible
+for this relation. In order to do this, it is first necessary to prove
+some auxiliary lemmas, justifying that the first argument of
+\texttt{div} decreases at each recursive call.
+
+\begin{alltt}
+Lemma minus_smaller_S : {\prodsym} x y:nat, x - y < S x.
+Proof.
+ intros x y; pattern y, x;
+ elim x using nat_double_ind.
+ destruct x0; auto with arith.
+ simpl; auto with arith.
+ simpl; auto with arith.
+Qed.
+
+
+Lemma minus_smaller_positive :
+ {\prodsym} x y:nat, x {\coqdiff}0 {\arrow} y {\coqdiff} 0 {\arrow} x - y < x.
+Proof.
+ destruct x; destruct y;
+ ( simpl;intros; apply minus_smaller ||
+ intros; absurd (0=0); auto).
+Qed.
+\end{alltt}
+
+\noindent The last two lemmas are necessary to prove that for any pair
+of positive natural numbers $x$ and $y$, if $x$ is accessible with
+respect to \citecoq{lt}, then so is $x-y$.
+
+\begin{alltt}
+Definition minus_decrease : {\prodsym} x y:nat, Acc lt x {\arrow}
+ x {\coqdiff} 0 {\arrow}
+ y {\coqdiff} 0 {\arrow}
+ Acc lt (x-y).
+Proof.
+ intros x y H; case H.
+ intros Hz posz posy.
+ apply Hz; apply minus_smaller_positive; assumption.
+Defined.
+\end{alltt}
+
+Let us take a look at the proof of the lemma \textsl{minus\_decrease}, since
+the way in which it has been proven is crucial for what follows.
+\begin{alltt}
+Print minus_decrease.
+\it
+minus_decrease =
+fun (x y : nat) (H : Acc lt x) {\funarrow}
+match H in (Acc _ y0) return (y0 {\coqdiff} 0 {\arrow} y {\coqdiff} 0 {\arrow} Acc lt (y0 - y)) with
+| Acc_intro z Hz {\funarrow}
+ fun (posz : z {\coqdiff} 0) (posy : y {\coqdiff} 0) {\funarrow}
+ Hz (z - y) (minus_smaller_positive z y posz posy)
+end
+ : {\prodsym} x y : nat, Acc lt x {\arrow} x {\coqdiff} 0 {\arrow} y {\coqdiff} 0 {\arrow} Acc lt (x - y)
+
+\end{alltt}
+\noindent Notice that the function call
+$(\texttt{minus\_decrease}\;n\;m\;H)$
+indeed yields an accessibility proof that is \textsl{structurally
+smaller} than its argument $H$, because it is (an application of) its
+recursive component $Hz$. This enables to justify the following
+definition of \textsl{div\_aux}:
+
+\begin{alltt}
+Definition div_aux (x y:nat)(H: Acc lt x):nat.
+ fix 3.
+ intros.
+ refine (if eq_nat_dec x 0
+ then 0
+ else if eq_nat_dec y 0
+ then y
+ else div_aux (x-y) y _).
+\it
+ div_aux : {\prodsym} x : nat, nat {\arrow} Acc lt x {\arrow} nat
+ x : nat
+ y : nat
+ H : Acc lt x
+ _ : x {\coqdiff} 0
+ _0 : y {\coqdiff} 0
+ ============================
+ Acc lt (x - y)
+
+\tt
+ apply (minus_decrease x y H);auto.
+Defined.
+\end{alltt}
+
+The main division function is easily defined, using the theorem
+\citecoq{lt\_wf} of the library \citecoq{Wf\_nat}. This theorem asserts that
+\citecoq{nat} is well founded w.r.t. \citecoq{lt}, thus any natural number
+is accessible.
+\begin{alltt}
+Definition div x y := div_aux x y (lt_wf x).
+\end{alltt}
+
+Let us explain the proof above. In the definition of \citecoq{div\_aux},
+what decreases is not $x$ but the \textsl{proof} of the accessibility
+of $x$. The tactic ``~\texttt{fix 3}~'' is used to indicate that the proof
+proceeds by structural induction on the third argument of the theorem
+--that is, on the accessibility proof. It also introduces a new
+hypothesis in the context, named as the current theorem, and with the
+same type as the goal. Then, the proof is refined with an incomplete
+proof term, containing a hole \texttt{\_}. This hole corresponds to the proof
+of accessibility for $x-y$, and is filled up with the (smaller!)
+accessibility proof provided by the function \texttt{minus\_decrease}.
+
+
+\noindent Let us take a look to the term \textsl{div\_aux} defined:
+
+\pagebreak
+\begin{alltt}
+Print div_aux.
+\it
+div_aux =
+(fix div_aux (x y : nat) (H : Acc lt x) \{struct H\} : nat :=
+ match eq_nat_dec x 0 with
+ | left _ {\funarrow} 0
+ | right _ {\funarrow}
+ match eq_nat_dec y 0 with
+ | left _ {\funarrow} y
+ | right _0 {\funarrow} div_aux (x - y) y (minus_decrease x y H _ _0)
+ end
+ end)
+ : {\prodsym} x : nat, nat {\arrow} Acc lt x {\arrow} nat
+
+\end{alltt}
+
+If the non-informative parts from this proof --that is, the
+accessibility proof-- are erased, then we obtain exactly the program
+that we were looking for.
+\begin{alltt}
+
+Extraction div.
+
+\it
+let div x y =
+ div_aux x y
+\tt
+
+Extraction div_aux.
+
+\it
+let rec div_aux x y =
+ match eq_nat_dec x O with
+ | Left {\arrow} O
+ | Right {\arrow}
+ (match eq_nat_dec y O with
+ | Left {\arrow} y
+ | Right {\arrow} div_aux (minus x y) y)
+\end{alltt}
+
+This methodology enables the representation
+of any program whose termination can be proved in {\coq}. Once the
+expected properties from this program have been verified, the
+justification of its termination can be thrown away, keeping just the
+desired computational behavior for it.
+
+\section{A case study in dependent elimination}\label{CaseStudy}
+
+Dependent types are very expressive, but ignoring some useful
+techniques can cause some problems to the beginner.
+Let us consider again the type of vectors (see section~\ref{vectors}).
+We want to prove a quite trivial property: the only value of type
+``~\citecoq{vector A 0}~'' is ``~\citecoq{Vnil $A$}~''.
+
+Our first naive attempt leads to a \emph{cul-de-sac}.
+\begin{alltt}
+Lemma vector0_is_vnil :
+ {\prodsym} (A:Type)(v:vector A 0), v = Vnil A.
+Proof.
+ intros A v;inversion v.
+\it
+1 subgoal
+
+ A : Set
+ v : vector A 0
+ ============================
+ v = Vnil A
+\tt
+Abort.
+\end{alltt}
+
+Another attempt is to do a case analysis on a vector of any length
+$n$, under an explicit hypothesis $n=0$. The tactic
+\texttt{discriminate} will help us to get rid of the case
+$n=\texttt{S $p$}$.
+Unfortunately, even the statement of our lemma is refused!
+
+\begin{alltt}
+ Lemma vector0_is_vnil_aux :
+ {\prodsym} (A:Type)(n:nat)(v:vector A n), n = 0 {\arrow} v = Vnil A.
+
+\it
+Error: In environment
+A : Type
+n : nat
+v : vector A n
+e : n = 0
+The term "Vnil A" has type "vector A 0" while it is expected to have type
+ "vector A n"
+\end{alltt}
+
+In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill-typed and this is
+because the type ``~\citecoq{vector A n}~'' is not \emph{convertible}
+with ``~\citecoq{vector A 0}~''.
+
+This problem can be solved if we consider the heterogeneous
+equality \citecoq{JMeq} \cite{conor:motive}
+which allows us to consider terms of different types, even if this
+equality can only be proven for terms in the same type.
+The axiom \citecoq{JMeq\_eq}, from the library \citecoq{JMeq} allows us to convert a
+heterogeneous equality to a standard one.
+
+\begin{alltt}
+Lemma vector0_is_vnil_aux :
+ {\prodsym} (A:Type)(n:nat)(v:vector A n),
+ n= 0 {\arrow} JMeq v (Vnil A).
+Proof.
+ destruct v.
+ auto.
+ intro; discriminate.
+Qed.
+\end{alltt}
+
+Our property of vectors of null length can be easily proven:
+
+\begin{alltt}
+Lemma vector0_is_vnil : {\prodsym} (A:Type)(v:vector A 0), v = Vnil A.
+ intros a v;apply JMeq_eq.
+ apply vector0_is_vnil_aux.
+ trivial.
+Qed.
+\end{alltt}
+
+It is interesting to look at another proof of
+\citecoq{vector0\_is\_vnil}, which illustrates a technique developed
+and used by various people (consult in the \emph{Coq-club} mailing
+list archive the contributions by Yves Bertot, Pierre Letouzey, Laurent Théry,
+Jean Duprat, and Nicolas Magaud, Venanzio Capretta and Conor McBride).
+This technique is also used for unfolding infinite list definitions
+(see chapter13 of~\cite{coqart}).
+Notice that this definition does not rely on any axiom (\emph{e.g.} \texttt{JMeq\_eq}).
+
+We first give a new definition of the identity on vectors. Before that,
+we make the use of constructors and selectors lighter thanks to
+the implicit arguments feature:
+
+\begin{alltt}
+Implicit Arguments Vcons [A n].
+Implicit Arguments Vnil [A].
+Implicit Arguments Vhead [A n].
+Implicit Arguments Vtail [A n].
+
+Definition Vid : {\prodsym} (A : Type)(n:nat), vector A n {\arrow} vector A n.
+Proof.
+ destruct n; intro v.
+ exact Vnil.
+ exact (Vcons (Vhead v) (Vtail v)).
+Defined.
+\end{alltt}
+
+
+Then we prove that \citecoq{Vid} is the identity on vectors:
+
+\begin{alltt}
+Lemma Vid_eq : {\prodsym} (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Proof.
+ destruct v.
+
+\it
+ A : Type
+ ============================
+ Vnil = Vid A 0 Vnil
+
+subgoal 2 is:
+ Vcons a v = Vid A (S n) (Vcons a v)
+\tt
+ reflexivity.
+ reflexivity.
+Defined.
+\end{alltt}
+
+Why defining a new identity function on vectors? The following
+dialogue shows that \citecoq{Vid} has some interesting computational
+properties:
+
+\begin{alltt}
+Eval simpl in (fun (A:Type)(v:vector A 0) {\funarrow} (Vid _ _ v)).
+\it = fun (A : Type) (_ : vector A 0) {\funarrow} Vnil
+ : {\prodsym} A : Type, vector A 0 {\arrow} vector A 0
+
+\end{alltt}
+
+Notice that the plain identity on vectors doesn't convert \citecoq{v}
+into \citecoq{Vnil}.
+\begin{alltt}
+Eval simpl in (fun (A:Type)(v:vector A 0) {\funarrow} v).
+\it = fun (A : Type) (v : vector A 0) {\funarrow} v
+ : {\prodsym} A : Type, vector A 0 {\arrow} vector A 0
+\end{alltt}
+
+Then we prove easily that any vector of length 0 is \citecoq{Vnil}:
+
+\begin{alltt}
+Theorem zero_nil : {\prodsym} A (v:vector A 0), v = Vnil.
+Proof.
+ intros.
+ change (Vnil (A:=A)) with (Vid _ 0 v).
+\it
+1 subgoal
+
+ A : Type
+ v : vector A 0
+ ============================
+ v = Vid A 0 v
+\tt
+ apply Vid_eq.
+Defined.
+\end{alltt}
+
+A similar result can be proven about vectors of strictly positive
+length\footnote{As for \citecoq{Vid} and \citecoq{Vid\_eq}, this definition
+is from Jean Duprat.}.
+
+\begin{alltt}
+
+
+Theorem decomp :
+ {\prodsym} (A : Type) (n : nat) (v : vector A (S n)),
+ v = Vcons (Vhead v) (Vtail v).
+Proof.
+ intros.
+ change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
+\it
+ 1 subgoal
+
+ A : Type
+ n : nat
+ v : vector A (S n)
+ ============================
+ v = Vid A (S n) v
+
+\tt{} apply Vid_eq.
+Defined.
+\end{alltt}
+
+
+Both lemmas: \citecoq{zero\_nil} and \citecoq{decomp},
+can be used to easily derive a double recursion principle
+on vectors of same length:
+
+
+\begin{alltt}
+Definition vector_double_rect :
+ {\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
+ P 0 Vnil Vnil {\arrow}
+ ({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
+ P (S n) (Vcons a v1) (Vcons b v2)) {\arrow}
+ {\prodsym} n (v1 v2 : vector A n), P n v1 v2.
+ induction n.
+ intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
+ auto.
+ intros v1 v2; rewrite (decomp _ _ v1);rewrite (decomp _ _ v2).
+ apply X0; auto.
+Defined.
+\end{alltt}
+
+Notice that, due to the conversion rule of {\coq}'s type system,
+this function can be used directly with \citecoq{Prop} or \citecoq{Type}
+instead of type (thus it is useless to build
+\citecoq{vector\_double\_ind} and \citecoq{vector\_double\_rec}) from scratch.
+
+We finish this example with showing how to define the bitwise
+\emph{or} on boolean vectors of the same length,
+and proving a little property about this
+operation.
+
+\begin{alltt}
+Definition bitwise_or n v1 v2 : vector bool n :=
+ vector_double_rect
+ bool
+ (fun n v1 v2 {\funarrow} vector bool n)
+ Vnil
+ (fun n v1 v2 a b r {\funarrow} Vcons (orb a b) r) n v1 v2.
+\end{alltt}
+
+Let us define recursively the $n$-th element of a vector. Notice
+that it must be a partial function, in case $n$ is greater or equal
+than the length of the vector. Since {\coq} only considers total
+functions, the function returns a value in an \emph{option} type.
+
+\begin{alltt}
+Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p)
+ \{struct v\}
+ : option A :=
+ match n,v with
+ _ , Vnil {\funarrow} None
+ | 0 , Vcons b _ _ {\funarrow} Some b
+ | S n', Vcons _ p' v' {\funarrow} vector_nth A n' p' v'
+ end.
+Implicit Arguments vector_nth [A p].
+\end{alltt}
+
+We can now prove --- using the double induction combinator ---
+a simple property relying \citecoq{vector\_nth} and \citecoq{bitwise\_or}:
+
+\begin{alltt}
+Lemma nth_bitwise :
+ {\prodsym} (n:nat) (v1 v2: vector bool n) i a b,
+ vector_nth i v1 = Some a {\arrow}
+ vector_nth i v2 = Some b {\arrow}
+ vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
+Proof.
+ intros n v1 v2; pattern n,v1,v2.
+ apply vector_double_rect.
+ simpl.
+ destruct i; discriminate 1.
+ destruct i; simpl;auto.
+ injection 1; injection 2;intros; subst a; subst b; auto.
+Qed.
+\end{alltt}
+
+
+\section{Co-inductive Types and Non-ending Constructions}
+\label{CoInduction}
+
+The objects of an inductive type are well-founded with respect to
+the constructors of the type. In other words, these objects are built
+by applying \emph{a finite number of times} the constructors of the type.
+Co-inductive types are obtained by relaxing this condition,
+and may contain non-well-founded objects \cite{EG96,EG95a}. An
+example of a co-inductive type is the type of infinite
+sequences formed with elements of type $A$, also called streams. This
+type can be introduced through the following definition:
+
+\begin{alltt}
+ CoInductive Stream (A: Type) :Type :=
+ | Cons : A\arrow{}Stream A\arrow{}Stream A.
+\end{alltt}
+
+If we are interested in finite or infinite sequences, we consider the type
+of \emph{lazy lists}:
+
+\begin{alltt}
+CoInductive LList (A: Type) : Type :=
+ | LNil : LList A
+ | LCons : A {\arrow} LList A {\arrow} LList A.
+\end{alltt}
+
+
+It is also possible to define co-inductive types for the
+trees with infinitely-many branches (see Chapter 13 of~\cite{coqart}).
+
+Structural induction is the way of expressing that inductive types
+only contain well-founded objects. Hence, this elimination principle
+is not valid for co-inductive types, and the only elimination rule for
+streams is case analysis. This principle can be used, for example, to
+define the destructors \textsl{head} and \textsl{tail}.
+
+\begin{alltt}
+ Definition head (A:Type)(s : Stream A) :=
+ match s with Cons a s' {\funarrow} a end.
+
+ Definition tail (A : Type)(s : Stream A) :=
+ match s with Cons a s' {\funarrow} s' end.
+\end{alltt}
+
+Infinite objects are defined by means of (non-ending) methods of
+construction, like in lazy functional programming languages. Such
+methods can be defined using the \texttt{CoFixpoint} command
+\refmancite{Section \ref{CoFixpoint}}. For example, the following
+definition introduces the infinite list $[a,a,a,\ldots]$:
+
+\begin{alltt}
+ CoFixpoint repeat (A:Type)(a:A) : Stream A :=
+ Cons a (repeat a).
+\end{alltt}
+
+
+However, not every co-recursive definition is an admissible method of
+construction. Similarly to the case of structural induction, the
+definition must verify a \textsl{guardedness} condition to be
+accepted. This condition states that any recursive call in the
+definition must be protected --i.e, be an argument of-- some
+constructor, and only an argument of constructors \cite{EG94a}. The
+following definitions are examples of valid methods of construction:
+
+\begin{alltt}
+CoFixpoint iterate (A: Type)(f: A {\arrow} A)(a : A) : Stream A:=
+ Cons a (iterate f (f a)).
+
+CoFixpoint map
+ (A B:Type)(f: A {\arrow} B)(s : Stream A) : Stream B:=
+ match s with Cons a tl {\funarrow} Cons (f a) (map f tl) end.
+\end{alltt}
+
+\begin{exercise}
+Define two different methods for constructing the stream which
+infinitely alternates the values \citecoq{true} and \citecoq{false}.
+\end{exercise}
+\begin{exercise}
+Using the destructors \texttt{head} and \texttt{tail}, define a function
+which takes the n-th element of an infinite stream.
+\end{exercise}
+
+A non-ending method of construction is computed lazily. This means
+that its definition is unfolded only when the object that it
+introduces is eliminated, that is, when it appears as the argument of
+a case expression. We can check this using the command
+\texttt{Eval}.
+
+\begin{alltt}
+Eval simpl in (fun (A:Type)(a:A) {\funarrow} repeat a).
+\it = fun (A : Type) (a : A) {\funarrow} repeat a
+ : {\prodsym} A : Type, A {\arrow} Stream A
+\tt
+Eval simpl in (fun (A:Type)(a:A) {\funarrow} head (repeat a)).
+\it = fun (A : Type) (a : A) {\funarrow} a
+ : {\prodsym} A : Type, A {\arrow} A
+\end{alltt}
+
+%\begin{exercise}
+%Prove the following theorem:
+%\begin{verbatim}
+%Theorem expand_repeat : (a:A)(repeat a)=(Cons a (repeat a)).
+%\end{verbatim}
+%Hint: Prove first the streams version of the lemma in exercise
+%\ref{expand}.
+%\end{exercise}
+
+\subsection{Extensional Properties}
+
+Case analysis is also a valid proof principle for infinite
+objects. However, this principle is not sufficient to prove
+\textsl{extensional} properties, that is, properties concerning the
+whole infinite object \cite{EG95a}. A typical example of an
+extensional property is the predicate expressing that two streams have
+the same elements. In many cases, the minimal reflexive relation $a=b$
+that is used as equality for inductive types is too small to capture
+equality between streams. Consider for example the streams
+$\texttt{iterate}\;f\;(f\;x)$ and
+$(\texttt{map}\;f\;(\texttt{iterate}\;f\;x))$. Even though these two streams have
+the same elements, no finite expansion of their definitions lead to
+equal terms. In other words, in order to deal with extensional
+properties, it is necessary to construct infinite proofs. The type of
+infinite proofs of equality can be introduced as a co-inductive
+predicate, as follows:
+\begin{alltt}
+CoInductive EqSt (A: Type) : Stream A {\arrow} Stream A {\arrow} Prop :=
+ eqst : {\prodsym} s1 s2: Stream A,
+ head s1 = head s2 {\arrow}
+ EqSt (tail s1) (tail s2) {\arrow}
+ EqSt s1 s2.
+\end{alltt}
+
+It is possible to introduce proof principles for reasoning about
+infinite objects as combinators defined through
+\texttt{CoFixpoint}. However, oppositely to the case of inductive
+types, proof principles associated to co-inductive types are not
+elimination but \textsl{introduction} combinators. An example of such
+a combinator is Park's principle for proving the equality of two
+streams, usually called the \textsl{principle of co-induction}. It
+states that two streams are equal if they satisfy a
+\textit{bisimulation}. A bisimulation is a binary relation $R$ such
+that any pair of streams $s_1$ ad $s_2$ satisfying $R$ have equal
+heads, and tails also satisfying $R$. This principle is in fact a
+method for constructing an infinite proof:
+
+\begin{alltt}
+Section Parks_Principle.
+Variable A : Type.
+Variable R : Stream A {\arrow} Stream A {\arrow} Prop.
+Hypothesis bisim1 : {\prodsym} s1 s2:Stream A,
+ R s1 s2 {\arrow} head s1 = head s2.
+
+Hypothesis bisim2 : {\prodsym} s1 s2:Stream A,
+ R s1 s2 {\arrow} R (tail s1) (tail s2).
+
+CoFixpoint park_ppl :
+ {\prodsym} s1 s2:Stream A, R s1 s2 {\arrow} EqSt s1 s2 :=
+ fun s1 s2 (p : R s1 s2) {\funarrow}
+ eqst s1 s2 (bisim1 s1 s2 p)
+ (park_ppl (tail s1)
+ (tail s2)
+ (bisim2 s1 s2 p)).
+End Parks_Principle.
+\end{alltt}
+
+Let us use the principle of co-induction to prove the extensional
+equality mentioned above.
+\begin{alltt}
+Theorem map_iterate : {\prodsym} (A:Type)(f:A{\arrow}A)(x:A),
+ EqSt (iterate f (f x))
+ (map f (iterate f x)).
+Proof.
+ intros A f x.
+ apply park_ppl with
+ (R:= fun s1 s2 {\funarrow}
+ {\exsym} x: A, s1 = iterate f (f x) {\coqand}
+ s2 = map f (iterate f x)).
+
+ intros s1 s2 (x0,(eqs1,eqs2));
+ rewrite eqs1; rewrite eqs2; reflexivity.
+ intros s1 s2 (x0,(eqs1,eqs2)).
+ exists (f x0);split;
+ [rewrite eqs1|rewrite eqs2]; reflexivity.
+ exists x;split; reflexivity.
+Qed.
+\end{alltt}
+
+The use of Park's principle is sometimes annoying, because it requires
+to find an invariant relation and prove that it is indeed a
+bisimulation. In many cases, a shorter proof can be obtained trying
+to construct an ad-hoc infinite proof, defined by a guarded
+declaration. The tactic ``~``\texttt{Cofix $f$}~'' can be used to do
+that. Similarly to the tactic \texttt{fix} indicated in Section
+\ref{WellFoundedRecursion}, this tactic introduces an extra hypothesis
+$f$ into the context, whose type is the same as the current goal. Note
+that the applications of $f$ in the proof \textsl{must be guarded}. In
+order to prevent us from doing unguarded calls, we can define a tactic
+that always apply a constructor before using $f$ \refmancite{Chapter
+\ref{WritingTactics}} :
+
+\begin{alltt}
+Ltac infiniteproof f :=
+ cofix f;
+ constructor;
+ [clear f| simpl; try (apply f; clear f)].
+\end{alltt}
+
+
+In the example above, this tactic produces a much simpler proof
+that the former one:
+
+\begin{alltt}
+Theorem map_iterate' : {\prodsym} ((A:Type)f:A{\arrow}A)(x:A),
+ EqSt (iterate f (f x))
+ (map f (iterate f x)).
+Proof.
+ infiniteproof map_iterate'.
+ reflexivity.
+Qed.
+\end{alltt}
+
+\begin{exercise}
+Define a co-inductive type of name $Nat$ that contains non-standard
+natural numbers --this is, verifying
+
+$$\exists m \in \mbox{\texttt{Nat}}, \forall\, n \in \mbox{\texttt{Nat}}, n<m$$.
+\end{exercise}
+
+\begin{exercise}
+Prove that the extensional equality of streams is an equivalence relation
+using Park's co-induction principle.
+\end{exercise}
+
+
+\begin{exercise}
+Provide a suitable definition of ``being an ordered list'' for infinite lists
+and define a principle for proving that an infinite list is ordered. Apply
+this method to the list $[0,1,\ldots ]$. Compare the result with
+exercise \ref{zeroton}.
+\end{exercise}
+
+\subsection{About injection, discriminate, and inversion}
+Since co-inductive types are closed w.r.t. their constructors,
+the techniques shown in Section~\ref{CaseTechniques} work also
+with these types.
+
+Let us consider the type of lazy lists, introduced on page~\pageref{CoInduction}.
+The following lemmas are straightforward applications
+ of \texttt{discriminate} and \citecoq{injection}:
+
+\begin{alltt}
+Lemma Lnil_not_Lcons : {\prodsym} (A:Type)(a:A)(l:LList A),
+ LNil {\coqdiff} (LCons a l).
+Proof.
+ intros;discriminate.
+Qed.
+
+Lemma injection_demo : {\prodsym} (A:Type)(a b : A)(l l': LList A),
+ LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
+ a = b {\coqand} l = l'.
+Proof.
+ intros A a b l l' e; injection e; auto.
+Qed.
+
+\end{alltt}
+
+In order to show \citecoq{inversion} at work, let us define
+two predicates on lazy lists:
+
+\begin{alltt}
+Inductive Finite (A:Type) : LList A {\arrow} Prop :=
+| Lnil_fin : Finite (LNil (A:=A))
+| Lcons_fin : {\prodsym} a l, Finite l {\arrow} Finite (LCons a l).
+
+CoInductive Infinite (A:Type) : LList A {\arrow} Prop :=
+| LCons_inf : {\prodsym} a l, Infinite l {\arrow} Infinite (LCons a l).
+\end{alltt}
+
+\noindent
+First, two easy theorems:
+\begin{alltt}
+Lemma LNil_not_Infinite : {\prodsym} (A:Type), ~ Infinite (LNil (A:=A)).
+Proof.
+ intros A H;inversion H.
+Qed.
+
+Lemma Finite_not_Infinite : {\prodsym} (A:Type)(l:LList A),
+ Finite l {\arrow} ~ Infinite l.
+Proof.
+ intros A l H; elim H.
+ apply LNil_not_Infinite.
+ intros a l0 F0 I0' I1.
+ case I0'; inversion_clear I1.
+ trivial.
+Qed.
+\end{alltt}
+
+
+On the other hand, the next proof uses the \citecoq{cofix} tactic.
+Notice the destructuration of \citecoq{l}, which allows us to
+apply the constructor \texttt{LCons\_inf}, thus satisfying
+ the guard condition:
+\begin{alltt}
+Lemma Not_Finite_Infinite : {\prodsym} (A:Type)(l:LList A),
+ ~ Finite l {\arrow} Infinite l.
+Proof.
+ cofix H.
+ destruct l.
+ intro;
+ absurd (Finite (LNil (A:=A)));
+ [auto|constructor].
+\it
+
+
+
+
+1 subgoal
+
+ H : forall (A : Type) (l : LList A), ~ Finite l -> Infinite l
+ A : Type
+ a : A
+ l : LList A
+ H0 : ~ Finite (LCons a l)
+ ============================
+ Infinite l
+\end{alltt}
+At this point, one must not apply \citecoq{H}! . It would be possible
+to solve the current goal by an inversion of ``~\citecoq{Finite (LCons a l)}~'', but, since the guard condition would be violated, the user
+would get an error message after typing \citecoq{Qed}.
+In order to satisfy the guard condition, we apply the constructor of
+\citecoq{Infinite}, \emph{then} apply \citecoq{H}.
+
+\begin{alltt}
+ constructor.
+ apply H.
+ red; intro H1;case H0.
+ constructor.
+ trivial.
+Qed.
+\end{alltt}
+
+
+
+
+The reader is invited to replay this proof and understand each of its steps.
+
+
+\bibliographystyle{abbrv}
+\bibliography{manbiblio,morebib}
+
+\end{document}
+
diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
new file mode 100644
index 00000000..28aaf752
--- /dev/null
+++ b/doc/RecTutorial/RecTutorial.v
@@ -0,0 +1,1232 @@
+Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3).
+
+
+
+Inductive nat : Set :=
+ | O : nat
+ | S : nat->nat.
+Check nat.
+Check O.
+Check S.
+
+Reset nat.
+Print nat.
+
+
+Print le.
+
+Theorem zero_leq_three: 0 <= 3.
+
+Proof.
+ constructor 2.
+ constructor 2.
+ constructor 2.
+ constructor 1.
+
+Qed.
+
+Print zero_leq_three.
+
+
+Lemma zero_leq_three': 0 <= 3.
+ repeat constructor.
+Qed.
+
+
+Lemma zero_lt_three : 0 < 3.
+Proof.
+ repeat constructor.
+Qed.
+
+Print zero_lt_three.
+
+Inductive le'(n:nat):nat -> Prop :=
+ | le'_n : le' n n
+ | le'_S : forall p, le' (S n) p -> le' n p.
+
+Hint Constructors le'.
+
+
+Require Import List.
+
+Print list.
+
+Check list.
+
+Check (nil (A:=nat)).
+
+Check (nil (A:= nat -> nat)).
+
+Check (fun A: Type => (cons (A:=A))).
+
+Check (cons 3 (cons 2 nil)).
+
+Check (nat :: bool ::nil).
+
+Check ((3<=4) :: True ::nil).
+
+Check (Prop::Set::nil).
+
+Require Import Bvector.
+
+Print vector.
+
+Check (Vnil nat).
+
+Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)).
+
+Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+
+Lemma eq_3_3 : 2 + 1 = 3.
+Proof.
+ reflexivity.
+Qed.
+Print eq_3_3.
+
+Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
+Proof.
+ reflexivity.
+Qed.
+Print eq_proof_proof.
+
+Lemma eq_lt_le : ( 2 < 4) = (3 <= 4).
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_nat_nat : nat = nat.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_Set_Set : Set = Set.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_Type_Type : Type = Type.
+Proof.
+ reflexivity.
+Qed.
+
+
+Check (2 + 1 = 3).
+
+
+Check (Type = Type).
+
+Goal Type = Type.
+reflexivity.
+Qed.
+
+
+Print or.
+
+Print and.
+
+
+Print sumbool.
+
+Print ex.
+
+Require Import ZArith.
+Require Import Compare_dec.
+
+Check le_lt_dec.
+
+Definition max (n p :nat) := match le_lt_dec n p with
+ | left _ => p
+ | right _ => n
+ end.
+
+Theorem le_max : forall n p, n <= p -> max n p = p.
+Proof.
+ intros n p ; unfold max ; case (le_lt_dec n p); simpl.
+ trivial.
+ intros; absurd (p < p); eauto with arith.
+Qed.
+
+Extraction max.
+
+
+
+
+
+
+Inductive tree(A:Type) : Type :=
+ node : A -> forest A -> tree A
+with
+ forest (A: Type) : Type :=
+ nochild : forest A |
+ addchild : tree A -> forest A -> forest A.
+
+
+
+
+
+Inductive
+ even : nat->Prop :=
+ evenO : even O |
+ evenS : forall n, odd n -> even (S n)
+with
+ odd : nat->Prop :=
+ oddS : forall n, even n -> odd (S n).
+
+Lemma odd_49 : odd (7 * 7).
+ simpl; repeat constructor.
+Qed.
+
+
+
+Definition nat_case :=
+ fun (Q : Type)(g0 : Q)(g1 : nat -> Q)(n:nat) =>
+ match n return Q with
+ | 0 => g0
+ | S p => g1 p
+ end.
+
+Eval simpl in (nat_case nat 0 (fun p => p) 34).
+
+Eval simpl in (fun g0 g1 => nat_case nat g0 g1 34).
+
+Eval simpl in (fun g0 g1 => nat_case nat g0 g1 0).
+
+
+Definition pred (n:nat) := match n with O => O | S m => m end.
+
+Eval simpl in pred 56.
+
+Eval simpl in pred 0.
+
+Eval simpl in fun p => pred (S p).
+
+
+Definition xorb (b1 b2:bool) :=
+match b1, b2 with
+ | false, true => true
+ | true, false => true
+ | _ , _ => false
+end.
+
+
+ Definition pred_spec (n:nat) := {m:nat | n=0 /\ m=0 \/ n = S m}.
+
+
+ Definition predecessor : forall n:nat, pred_spec n.
+ intro n;case n.
+ unfold pred_spec;exists 0;auto.
+ unfold pred_spec; intro n0;exists n0; auto.
+ Defined.
+
+Print predecessor.
+
+Extraction predecessor.
+
+Theorem nat_expand :
+ forall n:nat, n = match n with 0 => 0 | S p => S p end.
+ intro n;case n;simpl;auto.
+Qed.
+
+Check (fun p:False => match p return 2=3 with end).
+
+Theorem fromFalse : False -> 0=1.
+ intro absurd.
+ contradiction.
+Qed.
+
+Section equality_elimination.
+ Variables (A: Type)
+ (a b : A)
+ (p : a = b)
+ (Q : A -> Type).
+ Check (fun H : Q a =>
+ match p in (eq _ y) return Q y with
+ refl_equal => H
+ end).
+
+End equality_elimination.
+
+
+Theorem trans : forall n m p:nat, n=m -> m=p -> n=p.
+Proof.
+ intros n m p eqnm.
+ case eqnm.
+ trivial.
+Qed.
+
+Lemma Rw : forall x y: nat, y = y * x -> y * x * x = y.
+ intros x y e; do 2 rewrite <- e.
+ reflexivity.
+Qed.
+
+
+Require Import Arith.
+
+Check mult_1_l.
+(*
+mult_1_l
+ : forall n : nat, 1 * n = n
+*)
+
+Check mult_plus_distr_r.
+(*
+mult_plus_distr_r
+ : forall n m p : nat, (n + m) * p = n * p + m * p
+
+*)
+
+Lemma mult_distr_S : forall n p : nat, n * p + p = (S n)* p.
+ simpl;auto with arith.
+Qed.
+
+Lemma four_n : forall n:nat, n+n+n+n = 4*n.
+ intro n;rewrite <- (mult_1_l n).
+
+ Undo.
+ intro n; pattern n at 1.
+
+
+ rewrite <- mult_1_l.
+ repeat rewrite mult_distr_S.
+ trivial.
+Qed.
+
+
+Section Le_case_analysis.
+ Variables (n p : nat)
+ (H : n <= p)
+ (Q : nat -> Prop)
+ (H0 : Q n)
+ (HS : forall m, n <= m -> Q (S m)).
+ Check (
+ match H in (_ <= q) return (Q q) with
+ | le_n => H0
+ | le_S m Hm => HS m Hm
+ end
+ ).
+
+
+End Le_case_analysis.
+
+
+Lemma predecessor_of_positive : forall n, 1 <= n -> exists p:nat, n = S p.
+Proof.
+ intros n H; case H.
+ exists 0; trivial.
+ intros m Hm; exists m;trivial.
+Qed.
+
+Definition Vtail_total
+ (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
+match v in (vector _ n0) return (vector A (pred n0)) with
+| Vnil => Vnil A
+| Vcons _ n0 v0 => v0
+end.
+
+Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n).
+ intros A n v; case v.
+ simpl.
+ exact (Vnil A).
+ simpl.
+ auto.
+Defined.
+
+(*
+Inductive Lambda : Set :=
+ lambda : (Lambda -> False) -> Lambda.
+
+
+Error: Non strictly positive occurrence of "Lambda" in
+ "(Lambda -> False) -> Lambda"
+
+*)
+
+Section Paradox.
+ Variable Lambda : Set.
+ Variable lambda : (Lambda -> False) ->Lambda.
+
+ Variable matchL : Lambda -> forall Q:Prop, ((Lambda ->False) -> Q) -> Q.
+ (*
+ understand matchL Q l (fun h : Lambda -> False => t)
+
+ as match l return Q with lambda h => t end
+ *)
+
+ Definition application (f x: Lambda) :False :=
+ matchL f False (fun h => h x).
+
+ Definition Delta : Lambda := lambda (fun x : Lambda => application x x).
+
+ Definition loop : False := application Delta Delta.
+
+ Theorem two_is_three : 2 = 3.
+ Proof.
+ elim loop.
+ Qed.
+
+End Paradox.
+
+
+Require Import ZArith.
+
+
+
+Inductive itree : Set :=
+| ileaf : itree
+| inode : Z-> (nat -> itree) -> itree.
+
+Definition isingle l := inode l (fun i => ileaf).
+
+Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
+
+Definition t2 := inode 0
+ (fun n : nat =>
+ inode (Z_of_nat n)
+ (fun p => isingle (Z_of_nat (n*p)))).
+
+
+Inductive itree_le : itree-> itree -> Prop :=
+ | le_leaf : forall t, itree_le ileaf t
+ | le_node : forall l l' s s',
+ Zle l l' ->
+ (forall i, exists j:nat, itree_le (s i) (s' j)) ->
+ itree_le (inode l s) (inode l' s').
+
+
+Theorem itree_le_trans :
+ forall t t', itree_le t t' ->
+ forall t'', itree_le t' t'' -> itree_le t t''.
+ induction t.
+ constructor 1.
+
+ intros t'; case t'.
+ inversion 1.
+ intros z0 i0 H0.
+ intro t'';case t''.
+ inversion 1.
+ intros.
+ inversion_clear H1.
+ constructor 2.
+ inversion_clear H0;eauto with zarith.
+ inversion_clear H0.
+ intro i2; case (H4 i2).
+ intros.
+ generalize (H i2 _ H0).
+ intros.
+ case (H3 x);intros.
+ generalize (H5 _ H6).
+ exists x0;auto.
+Qed.
+
+
+
+Inductive itree_le' : itree-> itree -> Prop :=
+ | le_leaf' : forall t, itree_le' ileaf t
+ | le_node' : forall l l' s s' g,
+ Zle l l' ->
+ (forall i, itree_le' (s i) (s' (g i))) ->
+ itree_le' (inode l s) (inode l' s').
+
+
+
+
+
+Lemma t1_le_t2 : itree_le t1 t2.
+ unfold t1, t2.
+ constructor.
+ auto with zarith.
+ intro i; exists (2 * i).
+ unfold isingle.
+ constructor.
+ auto with zarith.
+ exists i;constructor.
+Qed.
+
+
+
+Lemma t1_le'_t2 : itree_le' t1 t2.
+ unfold t1, t2.
+ constructor 2 with (fun i : nat => 2 * i).
+ auto with zarith.
+ unfold isingle;
+ intro i ; constructor 2 with (fun i :nat => i).
+ auto with zarith.
+ constructor .
+Qed.
+
+
+Require Import List.
+
+Inductive ltree (A:Set) : Set :=
+ lnode : A -> list (ltree A) -> ltree A.
+
+Inductive prop : Prop :=
+ prop_intro : Prop -> prop.
+
+Check (prop_intro prop).
+
+Inductive ex_Prop (P : Prop -> Prop) : Prop :=
+ exP_intro : forall X : Prop, P X -> ex_Prop P.
+
+Lemma ex_Prop_inhabitant : ex_Prop (fun P => P -> P).
+Proof.
+ exists (ex_Prop (fun P => P -> P)).
+ trivial.
+Qed.
+
+
+
+
+(*
+
+Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
+ match p with exP_intro X HX => X end).
+Error:
+Incorrect elimination of "p" in the inductive type
+"ex_Prop", the return type has sort "Type" while it should be
+"Prop"
+
+Elimination of an inductive object of sort "Prop"
+is not allowed on a predicate in sort "Type"
+because proofs can be eliminated only to build proofs
+
+*)
+
+
+Inductive typ : Type :=
+ typ_intro : Type -> typ.
+
+Definition typ_inject: typ.
+split.
+exact typ.
+(*
+Defined.
+
+Error: Universe Inconsistency.
+*)
+Abort.
+(*
+
+Inductive aSet : Set :=
+ aSet_intro: Set -> aSet.
+
+
+User error: Large non-propositional inductive types must be in Type
+
+*)
+
+Inductive ex_Set (P : Set -> Prop) : Type :=
+ exS_intro : forall X : Set, P X -> ex_Set P.
+
+
+Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
+ c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
+
+Goal (comes_from_the_left _ _ (or_introl True I)).
+split.
+Qed.
+
+Goal ~(comes_from_the_left _ _ (or_intror True I)).
+ red;inversion 1.
+ (* discriminate H0.
+ *)
+Abort.
+
+Reset comes_from_the_left.
+
+(*
+
+
+
+
+
+
+ Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
+ match H with
+ | or_introl p => True
+ | or_intror q => False
+ end.
+
+Error:
+Incorrect elimination of "H" in the inductive type
+"or", the return type has sort "Type" while it should be
+"Prop"
+
+Elimination of an inductive object of sort "Prop"
+is not allowed on a predicate in sort "Type"
+because proofs can be eliminated only to build proofs
+
+*)
+
+Definition comes_from_the_left_sumbool
+ (P Q:Prop)(x:{P}+{Q}): Prop :=
+ match x with
+ | left p => True
+ | right q => False
+ end.
+
+
+
+
+Close Scope Z_scope.
+
+
+
+
+
+Theorem S_is_not_O : forall n, S n <> 0.
+
+Definition Is_zero (x:nat):= match x with
+ | 0 => True
+ | _ => False
+ end.
+ Lemma O_is_zero : forall m, m = 0 -> Is_zero m.
+ Proof.
+ intros m H; subst m.
+ (*
+ ============================
+ Is_zero 0
+ *)
+ simpl;trivial.
+ Qed.
+
+ red; intros n Hn.
+ apply O_is_zero with (m := S n).
+ assumption.
+Qed.
+
+Theorem disc2 : forall n, S (S n) <> 1.
+Proof.
+ intros n Hn; discriminate.
+Qed.
+
+
+Theorem disc3 : forall n, S (S n) = 0 -> forall Q:Prop, Q.
+Proof.
+ intros n Hn Q.
+ discriminate.
+Qed.
+
+
+
+Theorem inj_succ : forall n m, S n = S m -> n = m.
+Proof.
+
+
+Lemma inj_pred : forall n m, n = m -> pred n = pred m.
+Proof.
+ intros n m eq_n_m.
+ rewrite eq_n_m.
+ trivial.
+Qed.
+
+ intros n m eq_Sn_Sm.
+ apply inj_pred with (n:= S n) (m := S m); assumption.
+Qed.
+
+Lemma list_inject : forall (A:Type)(a b :A)(l l':list A),
+ a :: b :: l = b :: a :: l' -> a = b /\ l = l'.
+Proof.
+ intros A a b l l' e.
+ injection e.
+ auto.
+Qed.
+
+
+Theorem not_le_Sn_0 : forall n:nat, ~ (S n <= 0).
+Proof.
+ red; intros n H.
+ case H.
+Undo.
+
+Lemma not_le_Sn_0_with_constraints :
+ forall n p , S n <= p -> p = 0 -> False.
+Proof.
+ intros n p H; case H ;
+ intros; discriminate.
+Qed.
+
+eapply not_le_Sn_0_with_constraints; eauto.
+Qed.
+
+
+Theorem not_le_Sn_0' : forall n:nat, ~ (S n <= 0).
+Proof.
+ red; intros n H ; inversion H.
+Qed.
+
+Derive Inversion le_Sn_0_inv with (forall n :nat, S n <= 0).
+Check le_Sn_0_inv.
+
+Theorem le_Sn_0'' : forall n p : nat, ~ S n <= 0 .
+Proof.
+ intros n p H;
+ inversion H using le_Sn_0_inv.
+Qed.
+
+Derive Inversion_clear le_Sn_0_inv' with (forall n :nat, S n <= 0).
+Check le_Sn_0_inv'.
+
+
+Theorem le_reverse_rules :
+ forall n m:nat, n <= m ->
+ n = m \/
+ exists p, n <= p /\ m = S p.
+Proof.
+ intros n m H; inversion H.
+ left;trivial.
+ right; exists m0; split; trivial.
+Restart.
+ intros n m H; inversion_clear H.
+ left;trivial.
+ right; exists m0; split; trivial.
+Qed.
+
+Inductive ArithExp : Set :=
+ Zero : ArithExp
+ | Succ : ArithExp -> ArithExp
+ | Plus : ArithExp -> ArithExp -> ArithExp.
+
+Inductive RewriteRel : ArithExp -> ArithExp -> Prop :=
+ RewSucc : forall e1 e2 :ArithExp,
+ RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2)
+ | RewPlus0 : forall e:ArithExp,
+ RewriteRel (Plus Zero e) e
+ | RewPlusS : forall e1 e2:ArithExp,
+ RewriteRel e1 e2 ->
+ RewriteRel (Plus (Succ e1) e2) (Succ (Plus e1 e2)).
+
+
+
+Fixpoint plus (n p:nat) {struct n} : nat :=
+ match n with
+ | 0 => p
+ | S m => S (plus m p)
+ end.
+
+Fixpoint plus' (n p:nat) {struct p} : nat :=
+ match p with
+ | 0 => n
+ | S q => S (plus' n q)
+ end.
+
+Fixpoint plus'' (n p:nat) {struct n} : nat :=
+ match n with
+ | 0 => p
+ | S m => plus'' m (S p)
+ end.
+
+
+Fixpoint even_test (n:nat) : bool :=
+ match n
+ with 0 => true
+ | 1 => false
+ | S (S p) => even_test p
+ end.
+
+
+Reset even_test.
+
+Fixpoint even_test (n:nat) : bool :=
+ match n
+ with
+ | 0 => true
+ | S p => odd_test p
+ end
+with odd_test (n:nat) : bool :=
+ match n
+ with
+ | 0 => false
+ | S p => even_test p
+ end.
+
+
+
+Eval simpl in even_test.
+
+
+
+Eval simpl in (fun x : nat => even_test x).
+
+Eval simpl in (fun x : nat => plus 5 x).
+Eval simpl in (fun x : nat => even_test (plus 5 x)).
+
+Eval simpl in (fun x : nat => even_test (plus x 5)).
+
+
+Section Principle_of_Induction.
+Variable P : nat -> Prop.
+Hypothesis base_case : P 0.
+Hypothesis inductive_step : forall n:nat, P n -> P (S n).
+Fixpoint nat_ind (n:nat) : (P n) :=
+ match n return P n with
+ | 0 => base_case
+ | S m => inductive_step m (nat_ind m)
+ end.
+
+End Principle_of_Induction.
+
+Scheme Even_induction := Minimality for even Sort Prop
+with Odd_induction := Minimality for odd Sort Prop.
+
+Theorem even_plus_four : forall n:nat, even n -> even (4+n).
+Proof.
+ intros n H.
+ elim H using Even_induction with (P0 := fun n => odd (4+n));
+ simpl;repeat constructor;assumption.
+Qed.
+
+
+Section Principle_of_Double_Induction.
+Variable P : nat -> nat ->Prop.
+Hypothesis base_case1 : forall x:nat, P 0 x.
+Hypothesis base_case2 : forall x:nat, P (S x) 0.
+Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
+Fixpoint nat_double_ind (n m:nat){struct n} : P n m :=
+ match n, m return P n m with
+ | 0 , x => base_case1 x
+ | (S x), 0 => base_case2 x
+ | (S x), (S y) => inductive_step x y (nat_double_ind x y)
+ end.
+End Principle_of_Double_Induction.
+
+Section Principle_of_Double_Recursion.
+Variable P : nat -> nat -> Type.
+Hypothesis base_case1 : forall x:nat, P 0 x.
+Hypothesis base_case2 : forall x:nat, P (S x) 0.
+Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
+Fixpoint nat_double_rect (n m:nat){struct n} : P n m :=
+ match n, m return P n m with
+ | 0 , x => base_case1 x
+ | (S x), 0 => base_case2 x
+ | (S x), (S y) => inductive_step x y (nat_double_rect x y)
+ end.
+End Principle_of_Double_Recursion.
+
+Definition min : nat -> nat -> nat :=
+ nat_double_rect (fun (x y:nat) => nat)
+ (fun (x:nat) => 0)
+ (fun (y:nat) => 0)
+ (fun (x y r:nat) => S r).
+
+Eval compute in (min 5 8).
+Eval compute in (min 8 5).
+
+
+
+Lemma not_circular : forall n:nat, n <> S n.
+Proof.
+ intro n.
+ apply nat_ind with (P:= fun n => n <> S n).
+ discriminate.
+ red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
+Qed.
+
+Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
+Proof.
+ intros n p.
+ apply nat_double_rect with (P:= fun (n q:nat) => {q=p}+{q <> p}).
+Undo.
+ pattern p,n.
+ elim n using nat_double_rect.
+ destruct x; auto.
+ destruct x; auto.
+ intros n0 m H; case H.
+ intro eq; rewrite eq ; auto.
+ intro neg; right; red ; injection 1; auto.
+Defined.
+
+Definition eq_nat_dec' : forall n p:nat, {n=p}+{n <> p}.
+ decide equality.
+Defined.
+
+
+
+Require Import Le.
+Lemma le'_le : forall n p, le' n p -> n <= p.
+Proof.
+ induction 1;auto with arith.
+Qed.
+
+Lemma le'_n_Sp : forall n p, le' n p -> le' n (S p).
+Proof.
+ induction 1;auto.
+Qed.
+
+Hint Resolve le'_n_Sp.
+
+
+Lemma le_le' : forall n p, n<=p -> le' n p.
+Proof.
+ induction 1;auto with arith.
+Qed.
+
+
+Print Acc.
+
+
+Require Import Minus.
+
+(*
+Fixpoint div (x y:nat){struct x}: nat :=
+ if eq_nat_dec x 0
+ then 0
+ else if eq_nat_dec y 0
+ then x
+ else S (div (x-y) y).
+
+Error:
+Recursive definition of div is ill-formed.
+In environment
+div : nat -> nat -> nat
+x : nat
+y : nat
+_ : x <> 0
+_ : y <> 0
+
+Recursive call to div has principal argument equal to
+"x - y"
+instead of a subterm of x
+
+*)
+
+Lemma minus_smaller_S: forall x y:nat, x - y < S x.
+Proof.
+ intros x y; pattern y, x;
+ elim x using nat_double_ind.
+ destruct x0; auto with arith.
+ simpl; auto with arith.
+ simpl; auto with arith.
+Qed.
+
+Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 ->
+ x - y < x.
+Proof.
+ destruct x; destruct y;
+ ( simpl;intros; apply minus_smaller_S ||
+ intros; absurd (0=0); auto).
+Qed.
+
+Definition minus_decrease : forall x y:nat, Acc lt x ->
+ x <> 0 ->
+ y <> 0 ->
+ Acc lt (x-y).
+Proof.
+ intros x y H; case H.
+ intros Hz posz posy.
+ apply Hz; apply minus_smaller_positive; assumption.
+Defined.
+
+Print minus_decrease.
+
+
+
+Definition div_aux (x y:nat)(H: Acc lt x):nat.
+ fix 3.
+ intros.
+ refine (if eq_nat_dec x 0
+ then 0
+ else if eq_nat_dec y 0
+ then y
+ else div_aux (x-y) y _).
+ apply (minus_decrease x y H);assumption.
+Defined.
+
+
+Print div_aux.
+(*
+div_aux =
+(fix div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
+ match eq_nat_dec x 0 with
+ | left _ => 0
+ | right _ =>
+ match eq_nat_dec y 0 with
+ | left _ => y
+ | right _0 => div_aux (x - y) y (minus_decrease x y H _ _0)
+ end
+ end)
+ : forall x : nat, nat -> Acc lt x -> nat
+*)
+
+Require Import Wf_nat.
+Definition div x y := div_aux x y (lt_wf x).
+
+Extraction div.
+(*
+let div x y =
+ div_aux x y
+*)
+
+Extraction div_aux.
+
+(*
+let rec div_aux x y =
+ match eq_nat_dec x O with
+ | Left -> O
+ | Right ->
+ (match eq_nat_dec y O with
+ | Left -> y
+ | Right -> div_aux (minus x y) y)
+*)
+
+Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Proof.
+ intros A v;inversion v.
+Abort.
+
+(*
+ Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
+ n= 0 -> v = Vnil A.
+
+Toplevel input, characters 40281-40287
+> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A.
+> ^^^^^^
+Error: In environment
+A : Set
+n : nat
+v : vector A n
+e : n = 0
+The term "Vnil A" has type "vector A 0" while it is expected to have type
+ "vector A n"
+*)
+ Require Import JMeq.
+
+
+(* On devrait changer Set en Type ? *)
+
+Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
+ n= 0 -> JMeq v (Vnil A).
+Proof.
+ destruct v.
+ auto.
+ intro; discriminate.
+Qed.
+
+Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Proof.
+ intros a v;apply JMeq_eq.
+ apply vector0_is_vnil_aux.
+ trivial.
+Qed.
+
+
+Implicit Arguments Vcons [A n].
+Implicit Arguments Vnil [A].
+Implicit Arguments Vhead [A n].
+Implicit Arguments Vtail [A n].
+
+Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Proof.
+ destruct n; intro v.
+ exact Vnil.
+ exact (Vcons (Vhead v) (Vtail v)).
+Defined.
+
+Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)).
+
+Eval simpl in (fun (A:Type)(v:vector A 0) => v).
+
+
+
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Proof.
+ destruct v.
+ reflexivity.
+ reflexivity.
+Defined.
+
+Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Proof.
+ intros.
+ change (Vnil (A:=A)) with (Vid _ 0 v).
+ apply Vid_eq.
+Defined.
+
+
+Theorem decomp :
+ forall (A : Type) (n : nat) (v : vector A (S n)),
+ v = Vcons (Vhead v) (Vtail v).
+Proof.
+ intros.
+ change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
+ apply Vid_eq.
+Defined.
+
+
+
+Definition vector_double_rect :
+ forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
+ P 0 Vnil Vnil ->
+ (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
+ P (S n) (Vcons a v1) (Vcons b v2)) ->
+ forall n (v1 v2 : vector A n), P n v1 v2.
+ induction n.
+ intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
+ auto.
+ intros v1 v2; rewrite (decomp _ _ v1);rewrite (decomp _ _ v2).
+ apply X0; auto.
+Defined.
+
+Require Import Bool.
+
+Definition bitwise_or n v1 v2 : vector bool n :=
+ vector_double_rect bool (fun n v1 v2 => vector bool n)
+ Vnil
+ (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
+
+
+Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v}
+ : option A :=
+ match n,v with
+ _ , Vnil => None
+ | 0 , Vcons b _ _ => Some b
+ | S n', Vcons _ p' v' => vector_nth A n' p' v'
+ end.
+
+Implicit Arguments vector_nth [A p].
+
+
+Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b,
+ vector_nth i v1 = Some a ->
+ vector_nth i v2 = Some b ->
+ vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
+Proof.
+ intros n v1 v2; pattern n,v1,v2.
+ apply vector_double_rect.
+ simpl.
+ destruct i; discriminate 1.
+ destruct i; simpl;auto.
+ injection 1; injection 2;intros; subst a; subst b; auto.
+Qed.
+
+ Set Implicit Arguments.
+
+ CoInductive Stream (A:Type) : Type :=
+ | Cons : A -> Stream A -> Stream A.
+
+ CoInductive LList (A: Type) : Type :=
+ | LNil : LList A
+ | LCons : A -> LList A -> LList A.
+
+
+
+
+
+ Definition head (A:Type)(s : Stream A) := match s with Cons a s' => a end.
+
+ Definition tail (A : Type)(s : Stream A) :=
+ match s with Cons a s' => s' end.
+
+ CoFixpoint repeat (A:Type)(a:A) : Stream A := Cons a (repeat a).
+
+ CoFixpoint iterate (A: Type)(f: A -> A)(a : A) : Stream A:=
+ Cons a (iterate f (f a)).
+
+ CoFixpoint map (A B:Type)(f: A -> B)(s : Stream A) : Stream B:=
+ match s with Cons a tl => Cons (f a) (map f tl) end.
+
+Eval simpl in (fun (A:Type)(a:A) => repeat a).
+
+Eval simpl in (fun (A:Type)(a:A) => head (repeat a)).
+
+
+CoInductive EqSt (A: Type) : Stream A -> Stream A -> Prop :=
+ eqst : forall s1 s2: Stream A,
+ head s1 = head s2 ->
+ EqSt (tail s1) (tail s2) ->
+ EqSt s1 s2.
+
+
+Section Parks_Principle.
+Variable A : Type.
+Variable R : Stream A -> Stream A -> Prop.
+Hypothesis bisim1 : forall s1 s2:Stream A, R s1 s2 ->
+ head s1 = head s2.
+Hypothesis bisim2 : forall s1 s2:Stream A, R s1 s2 ->
+ R (tail s1) (tail s2).
+
+CoFixpoint park_ppl : forall s1 s2:Stream A, R s1 s2 ->
+ EqSt s1 s2 :=
+ fun s1 s2 (p : R s1 s2) =>
+ eqst s1 s2 (bisim1 p)
+ (park_ppl (bisim2 p)).
+End Parks_Principle.
+
+
+Theorem map_iterate : forall (A:Type)(f:A->A)(x:A),
+ EqSt (iterate f (f x)) (map f (iterate f x)).
+Proof.
+ intros A f x.
+ apply park_ppl with
+ (R:= fun s1 s2 => exists x: A,
+ s1 = iterate f (f x) /\ s2 = map f (iterate f x)).
+
+ intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity.
+ intros s1 s2 (x0,(eqs1,eqs2)).
+ exists (f x0);split;[rewrite eqs1|rewrite eqs2]; reflexivity.
+ exists x;split; reflexivity.
+Qed.
+
+Ltac infiniteproof f :=
+ cofix f; constructor; [clear f| simpl; try (apply f; clear f)].
+
+
+Theorem map_iterate' : forall (A:Type)(f:A->A)(x:A),
+ EqSt (iterate f (f x)) (map f (iterate f x)).
+infiniteproof map_iterate'.
+ reflexivity.
+Qed.
+
+
+Implicit Arguments LNil [A].
+
+Lemma Lnil_not_Lcons : forall (A:Type)(a:A)(l:LList A),
+ LNil <> (LCons a l).
+ intros;discriminate.
+Qed.
+
+Lemma injection_demo : forall (A:Type)(a b : A)(l l': LList A),
+ LCons a (LCons b l) = LCons b (LCons a l') ->
+ a = b /\ l = l'.
+Proof.
+ intros A a b l l' e; injection e; auto.
+Qed.
+
+
+Inductive Finite (A:Type) : LList A -> Prop :=
+| Lnil_fin : Finite (LNil (A:=A))
+| Lcons_fin : forall a l, Finite l -> Finite (LCons a l).
+
+CoInductive Infinite (A:Type) : LList A -> Prop :=
+| LCons_inf : forall a l, Infinite l -> Infinite (LCons a l).
+
+Lemma LNil_not_Infinite : forall (A:Type), ~ Infinite (LNil (A:=A)).
+Proof.
+ intros A H;inversion H.
+Qed.
+
+Lemma Finite_not_Infinite : forall (A:Type)(l:LList A),
+ Finite l -> ~ Infinite l.
+Proof.
+ intros A l H; elim H.
+ apply LNil_not_Infinite.
+ intros a l0 F0 I0' I1.
+ case I0'; inversion_clear I1.
+ trivial.
+Qed.
+
+Lemma Not_Finite_Infinite : forall (A:Type)(l:LList A),
+ ~ Finite l -> Infinite l.
+Proof.
+ cofix H.
+ destruct l.
+ intro; absurd (Finite (LNil (A:=A)));[auto|constructor].
+ constructor.
+ apply H.
+ red; intro H1;case H0.
+ constructor.
+ trivial.
+Qed.
+
+
+
diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex
new file mode 100644
index 00000000..6fb7534d
--- /dev/null
+++ b/doc/RecTutorial/coqartmacros.tex
@@ -0,0 +1,180 @@
+\usepackage{url}
+
+\newcommand{\variantspringer}[1]{#1}
+\newcommand{\marginok}[1]{\marginpar{\raggedright OK:#1}}
+\newcommand{\tab}{{\null\hskip1cm}}
+\newcommand{\Ltac}{\mbox{\emph{$\cal L$}tac}}
+\newcommand{\coq}{\mbox{\emph{Coq}}}
+\newcommand{\lcf}{\mbox{\emph{LCF}}}
+\newcommand{\hol}{\mbox{\emph{HOL}}}
+\newcommand{\pvs}{\mbox{\emph{PVS}}}
+\newcommand{\isabelle}{\mbox{\emph{Isabelle}}}
+\newcommand{\prolog}{\mbox{\emph{Prolog}}}
+\newcommand{\goalbar}{\tt{}============================\it}
+\newcommand{\gallina}{\mbox{\emph{Gallina}}}
+\newcommand{\joker}{\texttt{\_}}
+\newcommand{\eprime}{\(\e^{\prime}\)}
+\newcommand{\Ztype}{\citecoq{Z}}
+\newcommand{\propsort}{\citecoq{Prop}}
+\newcommand{\setsort}{\citecoq{Set}}
+\newcommand{\typesort}{\citecoq{Type}}
+\newcommand{\ocaml}{\mbox{\emph{OCAML}}}
+\newcommand{\haskell}{\mbox{\emph{Haskell}}}
+\newcommand{\why}{\mbox{\emph{Why}}}
+\newcommand{\Pascal}{\mbox{\emph{Pascal}}}
+
+\newcommand{\ml}{\mbox{\emph{ML}}}
+
+\newcommand{\scheme}{\mbox{\emph{Scheme}}}
+\newcommand{\lisp}{\mbox{\emph{Lisp}}}
+
+\newcommand{\implarrow}{\mbox{$\Rightarrow$}}
+\newcommand{\metavar}[1]{?#1}
+\newcommand{\notincoq}[1]{#1}
+\newcommand{\coqscope}[1]{\%#1}
+\newcommand{\arrow}{\mbox{$\rightarrow$}}
+\newcommand{\fleche}{\arrow}
+\newcommand{\funarrow}{\mbox{$\Rightarrow$}}
+\newcommand{\ltacarrow}{\funarrow}
+\newcommand{\coqand}{\mbox{\(\wedge\)}}
+\newcommand{\coqor}{\mbox{\(\vee\)}}
+\newcommand{\coqnot}{\mbox{\(\neg\)}}
+\newcommand{\hide}[1]{}
+\newcommand{\hidedots}[1]{...}
+\newcommand{\sig}[3]{\texttt{\{}#1\texttt{:}#2 \texttt{|} #3\texttt{\}}}
+\renewcommand{\neg}{\sim}
+\renewcommand{\marginpar}[1]{}
+
+\addtocounter{secnumdepth}{1}
+\providecommand{\og}{«}
+\providecommand{\fg}{»}
+
+
+\newcommand{\hard}{\mbox{\small *}}
+\newcommand{\xhard}{\mbox{\small **}}
+\newcommand{\xxhard}{\mbox{\small ***}}
+
+%%% Operateurs, etc.
+\newcommand{\impl}{\mbox{$\rightarrow$}}
+\newcommand{\appli}[2]{\mbox{\tt{#1 #2}}}
+\newcommand{\applis}[1]{\mbox{\texttt{#1}}}
+\newcommand{\abst}[3]{\mbox{\tt{fun #1:#2 \funarrow #3}}}
+\newcommand{\coqle}{\mbox{$\leq$}}
+\newcommand{\coqge}{\mbox{$\geq$}}
+\newcommand{\coqdiff}{\mbox{$\neq$}}
+\newcommand{\coqiff}{\mbox{$\leftrightarrow$}}
+\newcommand{\prodsym}{\mbox{\(\forall\,\)}}
+\newcommand{\exsym}{\mbox{\(\exists\,\)}}
+
+\newcommand{\substsign}{/}
+\newcommand{\subst}[3]{\mbox{#1\{#2\substsign{}#3\}}}
+\newcommand{\anoabst}[2]{\mbox{\tt[#1]#2}}
+\newcommand{\letin}[3]{\mbox{\tt let #1:=#2 in #3}}
+\newcommand{\prodep}[3]{\mbox{\tt \(\forall\,\)#1:#2,$\,$#3}}
+\newcommand{\prodplus}[2]{\mbox{\tt\(\forall\,\)$\,$#1,$\,$#2}}
+\newcommand{\dom}[1]{\textrm{dom}(#1)} % domaine d'un contexte (log function)
+\newcommand{\norm}[1]{\textrm{n}(#1)} % forme normale (log function)
+\newcommand{\coqZ}[1]{\mbox{\tt{`#1`}}}
+\newcommand{\coqnat}[1]{\mbox{\tt{#1}}}
+\newcommand{\coqcart}[2]{\mbox{\tt{#1*#2}}}
+\newcommand{\alphacong}{\mbox{$\,\cong_{\alpha}\,$}} % alpha-congruence
+\newcommand{\betareduc}{\mbox{$\,\rightsquigarrow_{\!\beta}$}\,} % beta reduction
+%\newcommand{\betastar}{\mbox{$\,\Rightarrow_{\!\beta}^{*}\,$}} % beta reduction
+\newcommand{\deltareduc}{\mbox{$\,\rightsquigarrow_{\!\delta}$}\,} % delta reduction
+\newcommand{\dbreduc}{\mbox{$\,\rightsquigarrow_{\!\delta\beta}$}\,} % delta,beta reduction
+\newcommand{\ireduc}{\mbox{$\,\rightsquigarrow_{\!\iota}$}\,} % delta,beta reduction
+
+
+% jugement de typage
+\newcommand{\these}{\boldsymbol{\large \vdash}}
+\newcommand{\disj}{\mbox{$\backslash/$}}
+\newcommand{\conj}{\mbox{$/\backslash$}}
+%\newcommand{\juge}[3]{\mbox{$#1 \boldsymbol{\vdash} #2 : #3 $}}
+\newcommand{\juge}[4]{\mbox{$#1,#2 \these #3 \boldsymbol{:} #4 $}}
+\newcommand{\smalljuge}[3]{\mbox{$#1 \these #2 \boldsymbol{:} #3 $}}
+\newcommand{\goal}[3]{\mbox{$#1,#2 \these^{\!\!\!?} #3 $}}
+\newcommand{\sgoal}[2]{\mbox{$#1\these^{\!\!\!\!?} #2 $}}
+\newcommand{\reduc}[5]{\mbox{$#1,#2 \these #3 \rhd_{#4}#5 $}}
+\newcommand{\convert}[5]{\mbox{$#1,#2 \these #3 =_{#4}#5 $}}
+\newcommand{\convorder}[5]{\mbox{$#1,#2 \these #3\leq _{#4}#5 $}}
+\newcommand{\wouff}[2]{\mbox{$\emph{WF}(#1)[#2]$}}
+
+
+%\newcommand{\mthese}{\underset{M}{\vdash}}
+\newcommand{\mthese}{\boldsymbol{\vdash}_{\!\!M}}
+\newcommand{\type}{\boldsymbol{:}}
+
+% jugement absolu
+
+%\newcommand{\ajuge}[2]{\mbox{$ \boldsymbol{\vdash} #1 : #2 $}}
+\newcommand{\ajuge}[2]{\mbox{$\these #1 \boldsymbol{:} #2 $}}
+
+%%% logique minimale
+\newcommand{\propzero}{\mbox{$P_0$}} % types de Fzero
+
+%%% logique propositionnelle classique
+\newcommand {\ff}{\boldsymbol{f}} % faux
+\newcommand {\vv}{\boldsymbol{t}} % vrai
+
+\newcommand{\verite}{\mbox{$\cal{B}$}} % {\ff,\vv}
+\newcommand{\sequ}[2]{\mbox{$#1 \vdash #2 $}} % sequent
+\newcommand{\strip}[1]{#1^o} % enlever les variables d'un contexte
+
+
+
+%%% tactiques
+\newcommand{\decomp}{\delta} % decomposition
+\newcommand{\recomp}{\rho} % recomposition
+
+%%% divers
+\newcommand{\cqfd}{\mbox{\textbf{cqfd}}}
+\newcommand{\fail}{\mbox{\textbf{F}}}
+\newcommand{\succes}{\mbox{$\blacksquare$}}
+%%% Environnements
+
+
+%% Fzero
+\newcommand{\con}{\mbox{$\cal C$}}
+\newcommand{\var}{\mbox{$\cal V$}}
+
+\newcommand{\atomzero}{\mbox{${\cal A}_0$}} % types de base de Fzero
+\newcommand{\typezero}{\mbox{${\cal T}_0$}} % types de Fzero
+\newcommand{\termzero}{\mbox{$\Lambda_0$}} % termes de Fzero
+\newcommand{\conzero}{\mbox{$\cal C_0$}} % contextes de Fzero
+
+\newcommand{\buts}{\mbox{$\cal B$}} % buts
+
+%%% for drawing terms
+% abstraction [x:t]e
+\newcommand{\PicAbst}[3]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}\chunk{#3}%
+ \end{bundle}}
+
+% the same in DeBruijn form
+\newcommand{\PicDbj}[2]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}
+ \end{bundle}}
+
+
+% applications
+\newcommand{\PicAppl}[2]{\begin{bundle}{\bf appl}\chunk{#1}\chunk{#2}%
+ \end{bundle}}
+
+% variables
+\newcommand{\PicVar}[1]{\begin{bundle}{\bf var}\chunk{#1}
+ \end{bundle}}
+
+% constantes
+\newcommand{\PicCon}[1]{\begin{bundle}{\bf const}\chunk{#1}\end{bundle}}
+
+% arrows
+\newcommand{\PicImpl}[2]{\begin{bundle}{\impl}\chunk{#1}\chunk{#2}%
+ \end{bundle}}
+
+
+
+%%%% scripts coq
+\newcommand{\prompt}{\mbox{\sl Coq $<\;$}}
+\newcommand{\natquicksort}{\texttt{nat\_quicksort}}
+\newcommand{\citecoq}[1]{\mbox{\texttt{#1}}}
+\newcommand{\safeit}{\it}
+\newtheorem{remarque}{Remark}[section]
+%\newtheorem{definition}{Definition}[chapter]
diff --git a/doc/RecTutorial/manbiblio.bib b/doc/RecTutorial/manbiblio.bib
new file mode 100644
index 00000000..099e3bbd
--- /dev/null
+++ b/doc/RecTutorial/manbiblio.bib
@@ -0,0 +1,875 @@
+
+@STRING{toappear="To appear"}
+@STRING{lncs="Lecture Notes in Computer Science"}
+
+@TECHREPORT{RefManCoq,
+ AUTHOR = {Bruno~Barras, Samuel~Boutin,
+ Cristina~Cornes, Judicaël~Courant, Yann~Coscoy, David~Delahaye,
+ Daniel~de~Rauglaudre, Jean-Christophe~Filliâtre, Eduardo~Giménez,
+ Hugo~Herbelin, Gérard~Huet, Henri~Laulhère, César~Muñoz,
+ Chetan~Murthy, Catherine~Parent-Vigouroux, Patrick~Loiseleur,
+ Christine~Paulin-Mohring, Amokrane~Saïbi, Benjamin~Werner},
+ INSTITUTION = {INRIA},
+ TITLE = {{The Coq Proof Assistant Reference Manual -- Version V6.2}},
+ YEAR = {1998}
+}
+
+@INPROCEEDINGS{Aud91,
+ AUTHOR = {Ph. Audebaud},
+ BOOKTITLE = {Proceedings of the sixth Conf. on Logic in Computer Science.},
+ PUBLISHER = {IEEE},
+ TITLE = {Partial {Objects} in the {Calculus of Constructions}},
+ YEAR = {1991}
+}
+
+@PHDTHESIS{Aud92,
+ AUTHOR = {Ph. Audebaud},
+ SCHOOL = {{Universit\'e} Bordeaux I},
+ TITLE = {Extension du Calcul des Constructions par Points fixes},
+ YEAR = {1992}
+}
+
+@INPROCEEDINGS{Audebaud92b,
+ AUTHOR = {Ph. Audebaud},
+ BOOKTITLE = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}},
+ EDITOR = {{B. Nordstr\"om and K. Petersson and G. Plotkin}},
+ NOTE = {Also Research Report LIP-ENS-Lyon},
+ PAGES = {pp 21--34},
+ TITLE = {{CC+ : an extension of the Calculus of Constructions with fixpoints}},
+ YEAR = {1992}
+}
+
+@INPROCEEDINGS{Augustsson85,
+ AUTHOR = {L. Augustsson},
+ TITLE = {{Compiling Pattern Matching}},
+ BOOKTITLE = {Conference Functional Programming and
+Computer Architecture},
+ YEAR = {1985}
+}
+
+@INPROCEEDINGS{EG94a,
+ AUTHOR = {E. Gim\'enez},
+ EDITORS = {P. Dybjer and B. Nordstr\"om and J. Smith},
+ BOOKTITLE = {Workshop on Types for Proofs and Programs},
+ PAGES = {39-59},
+ SERIES = {LNCS},
+ NUMBER = {996},
+ TITLE = {{Codifying guarded definitions with recursive schemes}},
+ YEAR = {1994},
+ PUBLISHER = {Springer-Verlag},
+}
+
+@INPROCEEDINGS{EG95a,
+ AUTHOR = {E. Gim\'enez},
+ BOOKTITLE = {Workshop on Types for Proofs and Programs},
+ SERIES = {LNCS},
+ NUMBER = {1158},
+ PAGES = {135-152},
+ TITLE = {An application of co-Inductive types in Coq:
+ verification of the Alternating Bit Protocol},
+ EDITORS = {S. Berardi and M. Coppo},
+ PUBLISHER = {Springer-Verlag},
+ YEAR = {1995}
+}
+
+@PhdThesis{EG96,
+ author = {E. Gim\'enez},
+ title = {A Calculus of Infinite Constructions and its
+ application to the verification of communicating systems},
+ school = {Ecole Normale Sup\'erieure de Lyon},
+ year = {1996}
+}
+
+@ARTICLE{BaCo85,
+ AUTHOR = {J.L. Bates and R.L. Constable},
+ JOURNAL = {ACM transactions on Programming Languages and Systems},
+ TITLE = {Proofs as {Programs}},
+ VOLUME = {7},
+ YEAR = {1985}
+}
+
+@BOOK{Bar81,
+ AUTHOR = {H.P. Barendregt},
+ PUBLISHER = {North-Holland},
+ TITLE = {The Lambda Calculus its Syntax and Semantics},
+ YEAR = {1981}
+}
+
+@TECHREPORT{Bar91,
+ AUTHOR = {H. Barendregt},
+ INSTITUTION = {Catholic University Nijmegen},
+ NOTE = {In Handbook of Logic in Computer Science, Vol II},
+ NUMBER = {91-19},
+ TITLE = {Lambda {Calculi with Types}},
+ YEAR = {1991}
+}
+
+@BOOK{Bastad92,
+ EDITOR = {B. Nordstr\"om and K. Petersson and G. Plotkin},
+ PUBLISHER = {Available by ftp at site ftp.inria.fr},
+ TITLE = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
+ YEAR = {1992}
+}
+
+@BOOK{Bee85,
+ AUTHOR = {M.J. Beeson},
+ PUBLISHER = {Springer-Verlag},
+ TITLE = {Foundations of Constructive Mathematics, Metamathematical Studies},
+ YEAR = {1985}
+}
+
+@ARTICLE{BeKe92,
+ AUTHOR = {G. Bellin and J. Ketonen},
+ JOURNAL = {Theoretical Computer Science},
+ PAGES = {115--142},
+ TITLE = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation},
+ VOLUME = {95},
+ YEAR = {1992}
+}
+
+@BOOK{Bis67,
+ AUTHOR = {E. Bishop},
+ PUBLISHER = {McGraw-Hill},
+ TITLE = {Foundations of Constructive Analysis},
+ YEAR = {1967}
+}
+
+@BOOK{BoMo79,
+ AUTHOR = {R.S. Boyer and J.S. Moore},
+ KEY = {BoMo79},
+ PUBLISHER = {Academic Press},
+ SERIES = {ACM Monograph},
+ TITLE = {A computational logic},
+ YEAR = {1979}
+}
+
+@MASTERSTHESIS{Bou92,
+ AUTHOR = {S. Boutin},
+ MONTH = sep,
+ SCHOOL = {{Universit\'e Paris 7}},
+ TITLE = {Certification d'un compilateur {ML en Coq}},
+ YEAR = {1992}
+}
+
+@ARTICLE{Bru72,
+ AUTHOR = {N.J. de Bruijn},
+ JOURNAL = {Indag. Math.},
+ TITLE = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
+ VOLUME = {34},
+ YEAR = {1972}
+}
+
+@INCOLLECTION{Bru80,
+ AUTHOR = {N.J. de Bruijn},
+ BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
+ EDITOR = {J.P. Seldin and J.R. Hindley},
+ PUBLISHER = {Academic Press},
+ TITLE = {A survey of the project {Automath}},
+ YEAR = {1980}
+}
+
+@TECHREPORT{Leroy90,
+ AUTHOR = {X. Leroy},
+ TITLE = {The {ZINC} experiment: an economical implementation
+of the {ML} language},
+ INSTITUTION = {INRIA},
+ NUMBER = {117},
+ YEAR = {1990}
+}
+
+@BOOK{Caml,
+ AUTHOR = {P. Weis and X. Leroy},
+ PUBLISHER = {InterEditions},
+ TITLE = {Le langage Caml},
+ YEAR = {1993}
+}
+
+@TECHREPORT{CoC89,
+ AUTHOR = {Projet Formel},
+ INSTITUTION = {INRIA},
+ NUMBER = {110},
+ TITLE = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}},
+ YEAR = {1989}
+}
+
+@INPROCEEDINGS{CoHu85a,
+ AUTHOR = {Th. Coquand and G. Huet},
+ ADDRESS = {Linz},
+ BOOKTITLE = {EUROCAL'85},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}},
+ VOLUME = {203},
+ YEAR = {1985}
+}
+
+@Misc{Bar98,
+ author = {B. Barras},
+ title = {A formalisation of
+ \uppercase{B}urali-\uppercase{F}orti's paradox in Coq},
+ howpublished = {Distributed within the bunch of contribution to the
+ Coq system},
+ year = {1998},
+ month = {March},
+ note = {\texttt{http://pauillac.inria.fr/coq}}
+}
+
+
+@INPROCEEDINGS{CoHu85b,
+ AUTHOR = {Th. Coquand and G. Huet},
+ BOOKTITLE = {Logic Colloquium'85},
+ EDITOR = {The Paris Logic Group},
+ PUBLISHER = {North-Holland},
+ TITLE = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}},
+ YEAR = {1987}
+}
+
+@ARTICLE{CoHu86,
+ AUTHOR = {Th. Coquand and G. Huet},
+ JOURNAL = {Information and Computation},
+ NUMBER = {2/3},
+ TITLE = {The {Calculus of Constructions}},
+ VOLUME = {76},
+ YEAR = {1988}
+}
+
+@BOOK{Con86,
+ AUTHOR = {R.L. {Constable et al.}},
+ PUBLISHER = {Prentice-Hall},
+ TITLE = {{Implementing Mathematics with the Nuprl Proof Development System}},
+ YEAR = {1986}
+}
+
+@INPROCEEDINGS{CoPa89,
+ AUTHOR = {Th. Coquand and C. Paulin-Mohring},
+ BOOKTITLE = {Proceedings of Colog'88},
+ EDITOR = {P. Martin-L{\"o}f and G. Mints},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {Inductively defined types},
+ VOLUME = {417},
+ YEAR = {1990}
+}
+
+@PHDTHESIS{Coq85,
+ AUTHOR = {Th. Coquand},
+ MONTH = jan,
+ SCHOOL = {Universit\'e Paris~7},
+ TITLE = {Une Th\'eorie des Constructions},
+ YEAR = {1985}
+}
+
+@INPROCEEDINGS{Coq86,
+ AUTHOR = {Th. Coquand},
+ ADDRESS = {Cambridge, MA},
+ BOOKTITLE = {Symposium on Logic in Computer Science},
+ PUBLISHER = {IEEE Computer Society Press},
+ TITLE = {{An Analysis of Girard's Paradox}},
+ YEAR = {1986}
+}
+
+@INPROCEEDINGS{Coq90,
+ AUTHOR = {Th. Coquand},
+ BOOKTITLE = {Logic and Computer Science},
+ EDITOR = {P. Oddifredi},
+ NOTE = {INRIA Research Report 1088, also in~\cite{CoC89}},
+ PUBLISHER = {Academic Press},
+ TITLE = {{Metamathematical Investigations of a Calculus of Constructions}},
+ YEAR = {1990}
+}
+
+@INPROCEEDINGS{Coq92,
+ AUTHOR = {Th. Coquand},
+ BOOKTITLE = {in \cite{Bastad92}},
+ TITLE = {{Pattern Matching with Dependent Types}},
+ YEAR = {1992},
+ crossref = {Bastad92}
+}
+
+@TECHREPORT{COQ93,
+ AUTHOR = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner},
+ INSTITUTION = {INRIA},
+ MONTH = may,
+ NUMBER = {154},
+ TITLE = {{The Coq Proof Assistant User's Guide Version 5.8}},
+ YEAR = {1993}
+}
+
+@INPROCEEDINGS{Coquand93,
+ AUTHOR = {Th. Coquand},
+ BOOKTITLE = {in \cite{Nijmegen93}},
+ TITLE = {{Infinite Objects in Type Theory}},
+ YEAR = {1993},
+ crossref = {Nijmegen93}
+}
+
+@MASTERSTHESIS{Cou94a,
+ AUTHOR = {J. Courant},
+ MONTH = sep,
+ SCHOOL = {DEA d'Informatique, ENS Lyon},
+ TITLE = {Explicitation de preuves par r\'ecurrence implicite},
+ YEAR = {1994}
+}
+
+@TECHREPORT{CPar93,
+ AUTHOR = {C. Parent},
+ INSTITUTION = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
+ MONTH = oct,
+ NOTE = {Also in~\cite{Nijmegen93}},
+ NUMBER = {93-29},
+ TITLE = {Developing certified programs in the system {Coq}- {The} {Program} tactic},
+ YEAR = {1993}
+}
+
+@PHDTHESIS{CPar95,
+ AUTHOR = {C. Parent},
+ SCHOOL = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
+ TITLE = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
+ YEAR = {1995}
+}
+
+@TECHREPORT{Dow90,
+ AUTHOR = {G. Dowek},
+ INSTITUTION = {INRIA},
+ NUMBER = {1283},
+ TITLE = {{Naming and Scoping in a Mathematical Vernacular}},
+ TYPE = {Research Report},
+ YEAR = {1990}
+}
+
+@ARTICLE{Dow91a,
+ AUTHOR = {G. Dowek},
+ JOURNAL = {{Compte Rendu de l'Acad\'emie des Sciences}},
+ NOTE = {(The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors)},
+ NUMBER = {12},
+ PAGES = {951--956},
+ TITLE = {{L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}},
+ VOLUME = {I, 312},
+ YEAR = {1991}
+}
+
+@INPROCEEDINGS{Dow91b,
+ AUTHOR = {G. Dowek},
+ BOOKTITLE = {Proceedings of Mathematical Foundation of Computer Science},
+ NOTE = {Also INRIA Research Report},
+ PAGES = {151--160},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {{A Second Order Pattern Matching Algorithm in the Cube of Typed {$\lambda$}-calculi}},
+ VOLUME = {520},
+ YEAR = {1991}
+}
+
+@PHDTHESIS{Dow91c,
+ AUTHOR = {G. Dowek},
+ MONTH = dec,
+ SCHOOL = {{Universit\'e Paris 7}},
+ TITLE = {{D\'emonstration automatique dans le Calcul des Constructions}},
+ YEAR = {1991}
+}
+
+@ARTICLE{dowek93,
+ AUTHOR = {G. Dowek},
+ TITLE = {{A Complete Proof Synthesis Method for the Cube of Type Systems}},
+ JOURNAL = {Journal Logic Computation},
+ VOLUME = {3},
+ NUMBER = {3},
+ PAGES = {287--315},
+ MONTH = {June},
+ YEAR = {1993}
+}
+
+@UNPUBLISHED{Dow92a,
+ AUTHOR = {G. Dowek},
+ NOTE = {To appear in Theoretical Computer Science},
+ TITLE = {{The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}},
+ YEAR = {1992}
+}
+
+@ARTICLE{Dow94a,
+ AUTHOR = {G. Dowek},
+ JOURNAL = {Annals of Pure and Applied Logic},
+ VOLUME = {69},
+ PAGES = {135--155},
+ TITLE = {Third order matching is decidable},
+ YEAR = {1994}
+}
+
+@INPROCEEDINGS{Dow94b,
+ AUTHOR = {G. Dowek},
+ BOOKTITLE = {Proceedings of the second international conference on typed lambda calculus and applications},
+ TITLE = {{Lambda-calculus, Combinators and the Comprehension Schema}},
+ YEAR = {1995}
+}
+
+@INPROCEEDINGS{Dyb91,
+ AUTHOR = {P. Dybjer},
+ BOOKTITLE = {Logical Frameworks},
+ EDITOR = {G. Huet and G. Plotkin},
+ PAGES = {59--79},
+ PUBLISHER = {Cambridge University Press},
+ TITLE = {{Inductive sets and families in {Martin-L{\"o}f's Type Theory} and their set-theoretic semantics : An inversion principle for {Martin-L\"of's} type theory}},
+ VOLUME = {14},
+ YEAR = {1991}
+}
+
+@ARTICLE{Dyc92,
+ AUTHOR = {Roy Dyckhoff},
+ JOURNAL = {The Journal of Symbolic Logic},
+ MONTH = sep,
+ NUMBER = {3},
+ TITLE = {Contraction-free sequent calculi for intuitionistic logic},
+ VOLUME = {57},
+ YEAR = {1992}
+}
+
+@MASTERSTHESIS{Fil94,
+ AUTHOR = {J.-C. Filli\^atre},
+ MONTH = sep,
+ SCHOOL = {DEA d'Informatique, ENS Lyon},
+ TITLE = {Une proc\'edure de d\'ecision pour le {C}alcul des {P}r\'edicats {D}irect. {E}tude et impl\'ementation dans le syst\`eme {C}oq},
+ YEAR = {1994}
+}
+
+@TECHREPORT{Filliatre95,
+ AUTHOR = {J.-C. Filli\^atre},
+ INSTITUTION = {LIP-ENS-Lyon},
+ TITLE = {{A decision procedure for Direct Predicate Calculus}},
+ TYPE = {Research report},
+ NUMBER = {96--25},
+ YEAR = {1995}
+}
+
+@UNPUBLISHED{Fle90,
+ AUTHOR = {E. Fleury},
+ MONTH = jul,
+ NOTE = {Rapport de Stage},
+ TITLE = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}},
+ YEAR = {1990}
+}
+
+
+@TechReport{Gim98,
+ author = {E. Gim\'nez},
+ title = {A Tutorial on Recursive Types in Coq},
+ institution = {INRIA},
+ year = {1998}
+}
+
+@TECHREPORT{HKP97,
+ author = {G. Huet and G. Kahn and Ch. Paulin-Mohring},
+ title = {The {Coq} Proof Assistant - A tutorial, Version 6.1},
+ institution = {INRIA},
+ type = {rapport technique},
+ month = {Août},
+ year = {1997},
+ note = {Version révisée distribuée avec {Coq}},
+ number = {204},
+}
+
+<<<<<<< biblio.bib
+
+
+=======
+>>>>>>> 1.4
+@INPROCEEDINGS{Gir70,
+ AUTHOR = {J.-Y. Girard},
+ BOOKTITLE = {Proceedings of the 2nd Scandinavian Logic Symposium},
+ PUBLISHER = {North-Holland},
+ TITLE = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types},
+ YEAR = {1970}
+}
+
+@PHDTHESIS{Gir72,
+ AUTHOR = {J.-Y. Girard},
+ SCHOOL = {Universit\'e Paris~7},
+ TITLE = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
+ YEAR = {1972}
+}
+
+@BOOK{Gir89,
+ AUTHOR = {J.-Y. Girard and Y. Lafont and P. Taylor},
+ PUBLISHER = {Cambridge University Press},
+ SERIES = {Cambridge Tracts in Theoretical Computer Science 7},
+ TITLE = {Proofs and Types},
+ YEAR = {1989}
+}
+
+@MASTERSTHESIS{Hir94,
+ AUTHOR = {D. Hirschkoff},
+ MONTH = sep,
+ SCHOOL = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
+ TITLE = {{Ecriture d'une tactique arithm\'etique pour le syst\`eme Coq}},
+ YEAR = {1994}
+}
+
+@INCOLLECTION{How80,
+ AUTHOR = {W.A. Howard},
+ BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
+ EDITOR = {J.P. Seldin and J.R. Hindley},
+ NOTE = {Unpublished 1969 Manuscript},
+ PUBLISHER = {Academic Press},
+ TITLE = {The Formulae-as-Types Notion of Constructions},
+ YEAR = {1980}
+}
+
+@INCOLLECTION{HuetLevy79,
+ AUTHOR = {G. Huet and J.-J. L\'{e}vy},
+ TITLE = {Call by Need Computations in Non-Ambigous
+Linear Term Rewriting Systems},
+ NOTE = {Also research report 359, INRIA, 1979},
+ BOOKTITLE = {Computational Logic, Essays in Honor of
+Alan Robinson},
+ EDITOR = {J.-L. Lassez and G. Plotkin},
+ PUBLISHER = {The MIT press},
+ YEAR = {1991}
+}
+
+@INPROCEEDINGS{Hue87,
+ AUTHOR = {G. Huet},
+ BOOKTITLE = {Programming of Future Generation Computers},
+ EDITOR = {K. Fuchi and M. Nivat},
+ NOTE = {Also in Proceedings of TAPSOFT87, LNCS 249, Springer-Verlag, 1987, pp 276--286},
+ PUBLISHER = {Elsevier Science},
+ TITLE = {Induction Principles Formalized in the {Calculus of Constructions}},
+ YEAR = {1988}
+}
+
+@INPROCEEDINGS{Hue88,
+ AUTHOR = {G. Huet},
+ BOOKTITLE = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
+ EDITOR = {R. Narasimhan},
+ NOTE = {Also in~\cite{CoC89}},
+ PUBLISHER = {World Scientific Publishing},
+ TITLE = {{The Constructive Engine}},
+ YEAR = {1989}
+}
+
+@BOOK{Hue89,
+ EDITOR = {G. Huet},
+ PUBLISHER = {Addison-Wesley},
+ SERIES = {The UT Year of Programming Series},
+ TITLE = {Logical Foundations of Functional Programming},
+ YEAR = {1989}
+}
+
+@INPROCEEDINGS{Hue92,
+ AUTHOR = {G. Huet},
+ BOOKTITLE = {Proceedings of 12th FST/TCS Conference, New Delhi},
+ PAGES = {229--240},
+ PUBLISHER = {Springer Verlag},
+ SERIES = {LNCS},
+ TITLE = {{The Gallina Specification Language : A case study}},
+ VOLUME = {652},
+ YEAR = {1992}
+}
+
+@ARTICLE{Hue94,
+ AUTHOR = {G. Huet},
+ JOURNAL = {J. Functional Programming},
+ PAGES = {371--394},
+ PUBLISHER = {Cambridge University Press},
+ TITLE = {Residual theory in $\lambda$-calculus: a formal development},
+ VOLUME = {4,3},
+ YEAR = {1994}
+}
+
+@ARTICLE{KeWe84,
+ AUTHOR = {J. Ketonen and R. Weyhrauch},
+ JOURNAL = {Theoretical Computer Science},
+ PAGES = {297--307},
+ TITLE = {A decidable fragment of {P}redicate {C}alculus},
+ VOLUME = {32},
+ YEAR = {1984}
+}
+
+@BOOK{Kle52,
+ AUTHOR = {S.C. Kleene},
+ PUBLISHER = {North-Holland},
+ SERIES = {Bibliotheca Mathematica},
+ TITLE = {Introduction to Metamathematics},
+ YEAR = {1952}
+}
+
+@BOOK{Kri90,
+ AUTHOR = {J.-L. Krivine},
+ PUBLISHER = {Masson},
+ SERIES = {Etudes et recherche en informatique},
+ TITLE = {Lambda-calcul {types et mod\`eles}},
+ YEAR = {1990}
+}
+
+@ARTICLE{Laville91,
+ AUTHOR = {A. Laville},
+ TITLE = {Comparison of Priority Rules in Pattern
+Matching and Term Rewriting},
+ JOURNAL = {Journal of Symbolic Computation},
+ VOLUME = {11},
+ PAGES = {321--347},
+ YEAR = {1991}
+}
+
+@BOOK{LE92,
+ EDITOR = {G. Huet and G. Plotkin},
+ PUBLISHER = {Cambridge University Press},
+ TITLE = {Logical Environments},
+ YEAR = {1992}
+}
+
+@INPROCEEDINGS{LePa94,
+ AUTHOR = {F. Leclerc and C. Paulin-Mohring},
+ BOOKTITLE = {{Types for Proofs and Programs, Types' 93}},
+ EDITOR = {H. Barendregt and T. Nipkow},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}},
+ VOLUME = {806},
+ YEAR = {1994}
+}
+
+@BOOK{LF91,
+ EDITOR = {G. Huet and G. Plotkin},
+ PUBLISHER = {Cambridge University Press},
+ TITLE = {Logical Frameworks},
+ YEAR = {1991}
+}
+
+@BOOK{MaL84,
+ AUTHOR = {{P. Martin-L\"of}},
+ PUBLISHER = {Bibliopolis},
+ SERIES = {Studies in Proof Theory},
+ TITLE = {Intuitionistic Type Theory},
+ YEAR = {1984}
+}
+
+@INPROCEEDINGS{manoury94,
+ AUTHOR = {P. Manoury},
+ TITLE = {{A User's Friendly Syntax to Define
+Recursive Functions as Typed $\lambda-$Terms}},
+ BOOKTITLE = {{Types for Proofs and Programs, TYPES'94}},
+ SERIES = {LNCS},
+ VOLUME = {996},
+ MONTH = jun,
+ YEAR = {1994}
+}
+
+@ARTICLE{MaSi94,
+ AUTHOR = {P. Manoury and M. Simonot},
+ JOURNAL = {TCS},
+ TITLE = {Automatizing termination proof of recursively defined function},
+ YEAR = {To appear}
+}
+
+@TECHREPORT{maranget94,
+ AUTHOR = {L. Maranget},
+ INSTITUTION = {INRIA},
+ NUMBER = {2385},
+ TITLE = {{Two Techniques for Compiling Lazy Pattern Matching}},
+ YEAR = {1994}
+}
+
+@INPROCEEDINGS{Moh89a,
+ AUTHOR = {C. Paulin-Mohring},
+ ADDRESS = {Austin},
+ BOOKTITLE = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
+ MONTH = jan,
+ PUBLISHER = {ACM},
+ TITLE = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
+ YEAR = {1989}
+}
+
+@PHDTHESIS{Moh89b,
+ AUTHOR = {C. Paulin-Mohring},
+ MONTH = jan,
+ SCHOOL = {{Universit\'e Paris 7}},
+ TITLE = {Extraction de programmes dans le {Calcul des Constructions}},
+ YEAR = {1989}
+}
+
+@INPROCEEDINGS{Moh93,
+ AUTHOR = {C. Paulin-Mohring},
+ BOOKTITLE = {Proceedings of the conference Typed Lambda Calculi and Applications},
+ EDITOR = {M. Bezem and J.-F. Groote},
+ NOTE = {Also LIP research report 92-49, ENS Lyon},
+ NUMBER = {664},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {{Inductive Definitions in the System Coq - Rules and Properties}},
+ YEAR = {1993}
+}
+
+@MASTERSTHESIS{Mun94,
+ AUTHOR = {C. Mu\~noz},
+ MONTH = sep,
+ SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
+ TITLE = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
+ YEAR = {1994}
+}
+
+@BOOK{Nijmegen93,
+ EDITOR = {H. Barendregt and T. Nipkow},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {Types for Proofs and Programs},
+ VOLUME = {806},
+ YEAR = {1994}
+}
+
+@BOOK{NoPS90,
+ AUTHOR = {B. {Nordstr\"om} and K. Peterson and J. Smith},
+ BOOKTITLE = {Information Processing 83},
+ PUBLISHER = {Oxford Science Publications},
+ SERIES = {International Series of Monographs on Computer Science},
+ TITLE = {Programming in {Martin-L\"of's} Type Theory},
+ YEAR = {1990}
+}
+
+@ARTICLE{Nor88,
+ AUTHOR = {B. {Nordstr\"om}},
+ JOURNAL = {BIT},
+ TITLE = {Terminating General Recursion},
+ VOLUME = {28},
+ YEAR = {1988}
+}
+
+@BOOK{Odi90,
+ EDITOR = {P. Odifreddi},
+ PUBLISHER = {Academic Press},
+ TITLE = {Logic and Computer Science},
+ YEAR = {1990}
+}
+
+@INPROCEEDINGS{PaMS92,
+ AUTHOR = {M. Parigot and P. Manoury and M. Simonot},
+ ADDRESS = {St. Petersburg, Russia},
+ BOOKTITLE = {Logic Programming and automated reasoning},
+ EDITOR = {A. Voronkov},
+ MONTH = jul,
+ NUMBER = {624},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {{ProPre : A Programming language with proofs}},
+ YEAR = {1992}
+}
+
+@ARTICLE{Par92,
+ AUTHOR = {M. Parigot},
+ JOURNAL = {Theoretical Computer Science},
+ NUMBER = {2},
+ PAGES = {335--356},
+ TITLE = {{Recursive Programming with Proofs}},
+ VOLUME = {94},
+ YEAR = {1992}
+}
+
+@INPROCEEDINGS{Parent95b,
+ AUTHOR = {C. Parent},
+ BOOKTITLE = {{Mathematics of Program Construction'95}},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {{Synthesizing proofs from programs in
+the Calculus of Inductive Constructions}},
+ VOLUME = {947},
+ YEAR = {1995}
+}
+
+@ARTICLE{PaWe92,
+ AUTHOR = {C. Paulin-Mohring and B. Werner},
+ JOURNAL = {Journal of Symbolic Computation},
+ PAGES = {607--640},
+ TITLE = {{Synthesis of ML programs in the system Coq}},
+ VOLUME = {15},
+ YEAR = {1993}
+}
+
+@INPROCEEDINGS{Prasad93,
+ AUTHOR = {K.V. Prasad},
+ BOOKTITLE = {{Proceedings of CONCUR'93}},
+ PUBLISHER = {Springer-Verlag},
+ SERIES = {LNCS},
+ TITLE = {{Programming with broadcasts}},
+ VOLUME = {715},
+ YEAR = {1993}
+}
+
+@INPROCEEDINGS{puel-suarez90,
+ AUTHOR = {L.Puel and A. Su\'arez},
+ BOOKTITLE = {{Conference Lisp and Functional Programming}},
+ SERIES = {ACM},
+ PUBLISHER = {Springer-Verlag},
+ TITLE = {{Compiling Pattern Matching by Term
+Decomposition}},
+ YEAR = {1990}
+}
+
+@UNPUBLISHED{Rou92,
+ AUTHOR = {J. Rouyer},
+ MONTH = aug,
+ NOTE = {To appear as a technical report},
+ TITLE = {{D\'eveloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
+ YEAR = {1992}
+}
+
+@TECHREPORT{Saibi94,
+ AUTHOR = {A. Sa\"{\i}bi},
+ INSTITUTION = {INRIA},
+ MONTH = dec,
+ NUMBER = {2345},
+ TITLE = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}},
+ YEAR = {1994}
+}
+
+@MASTERSTHESIS{saidi94,
+ AUTHOR = {H. Saidi},
+ MONTH = sep,
+ SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
+ TITLE = {R\'esolution d'\'equations dans le syst\`eme T
+ de G\"odel},
+ YEAR = {1994}
+}
+
+@MASTERSTHESIS{Ter92,
+ AUTHOR = {D. Terrasse},
+ MONTH = sep,
+ SCHOOL = {IARFA},
+ TITLE = {{Traduction de TYPOL en COQ. Application \`a Mini ML}},
+ YEAR = {1992}
+}
+
+@TECHREPORT{ThBeKa92,
+ AUTHOR = {L. Th\'ery and Y. Bertot and G. Kahn},
+ INSTITUTION = {INRIA Sophia},
+ MONTH = may,
+ NUMBER = {1684},
+ TITLE = {Real theorem provers deserve real user-interfaces},
+ TYPE = {Research Report},
+ YEAR = {1992}
+}
+
+@BOOK{TrDa89,
+ AUTHOR = {A.S. Troelstra and D. van Dalen},
+ PUBLISHER = {North-Holland},
+ SERIES = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123},
+ TITLE = {Constructivism in Mathematics, an introduction},
+ YEAR = {1988}
+}
+
+@INCOLLECTION{wadler87,
+ AUTHOR = {P. Wadler},
+ TITLE = {Efficient Compilation of Pattern Matching},
+ BOOKTITLE = {The Implementation of Functional Programming
+Languages},
+ EDITOR = {S.L. Peyton Jones},
+ PUBLISHER = {Prentice-Hall},
+ YEAR = {1987}
+}
+
+@PHDTHESIS{Wer94,
+ AUTHOR = {B. Werner},
+ SCHOOL = {Universit\'e Paris 7},
+ TITLE = {Une th\'eorie des constructions inductives},
+ TYPE = {Th\`ese de Doctorat},
+ YEAR = {1994}
+}
+
+
diff --git a/doc/RecTutorial/morebib.bib b/doc/RecTutorial/morebib.bib
new file mode 100644
index 00000000..11dde2cd
--- /dev/null
+++ b/doc/RecTutorial/morebib.bib
@@ -0,0 +1,55 @@
+@book{coqart,
+ title = "Interactive Theorem Proving and Program Development.
+ Coq'Art: The Calculus of Inductive Constructions",
+ author = "Yves Bertot and Pierre Castéran",
+ publisher = "Springer Verlag",
+ series = "Texts in Theoretical Computer Science. An EATCS series",
+ year = 2004
+}
+
+@Article{Coquand:Huet,
+ author = {Thierry Coquand and Gérard Huet},
+ title = {The Calculus of Constructions},
+ journal = {Information and Computation},
+ year = {1988},
+ volume = {76},
+}
+
+@INcollection{Coquand:metamathematical,
+ author = "Thierry Coquand",
+ title = "Metamathematical Investigations on a Calculus of Constructions",
+ booktitle="Logic and Computer Science",
+ year = {1990},
+ editor="P. Odifreddi",
+ publisher = "Academic Press",
+}
+
+@Misc{coqrefman,
+ title = {The {C}oq reference manual},
+ author={{C}oq {D}evelopment Team},
+ note= {LogiCal Project, \texttt{http://coq.inria.fr/}}
+ }
+
+@Misc{coqsite,
+ author= {{C}oq {D}evelopment Team},
+ title = {The \emph{Coq} proof assistant},
+ note = {Documentation, system download. {C}ontact: \texttt{http://coq.inria.fr/}}
+}
+
+
+
+@Misc{Booksite,
+ author = {Yves Bertot and Pierre Cast\'eran},
+ title = {Coq'{A}rt: examples and exercises},
+ note = {\url{http://www.labri.fr/Perso/~casteran/CoqArt}}
+}
+
+
+@InProceedings{conor:motive,
+ author ="Conor McBride",
+ title = "Elimination with a motive",
+ booktitle = "Types for Proofs and Programs'2000",
+ volume = 2277,
+ pages = "197-217",
+ year = "2002",
+}
diff --git a/doc/RecTutorial/recmacros.tex b/doc/RecTutorial/recmacros.tex
new file mode 100644
index 00000000..0334553f
--- /dev/null
+++ b/doc/RecTutorial/recmacros.tex
@@ -0,0 +1,75 @@
+%===================================
+% Style of the document
+%===================================
+%\newtheorem{example}{Example}[section]
+%\newtheorem{exercise}{Exercise}[section]
+
+
+\newcommand{\comentario}[1]{\texttt{#1}}
+
+%===================================
+% Keywords
+%===================================
+
+\newcommand{\Prop}{\texttt{Prop}}
+\newcommand{\Set}{\texttt{Set}}
+\newcommand{\Type}{\texttt{Type}}
+\newcommand{\true}{\texttt{true}}
+\newcommand{\false}{\texttt{false}}
+\newcommand{\Lth}{\texttt{Lth}}
+
+\newcommand{\Nat}{\texttt{nat}}
+\newcommand{\nat}{\texttt{nat}}
+\newcommand{\Z} {\texttt{O}}
+\newcommand{\SUCC}{\texttt{S}}
+\newcommand{\pred}{\texttt{pred}}
+
+\newcommand{\False}{\texttt{False}}
+\newcommand{\True}{\texttt{True}}
+\newcommand{\I}{\texttt{I}}
+
+\newcommand{\natind}{\texttt{nat\_ind}}
+\newcommand{\natrec}{\texttt{nat\_rec}}
+\newcommand{\natrect}{\texttt{nat\_rect}}
+
+\newcommand{\eqT}{\texttt{eqT}}
+\newcommand{\identityT}{\texttt{identityT}}
+
+\newcommand{\map}{\texttt{map}}
+\newcommand{\iterates}{\texttt{iterates}}
+
+
+%===================================
+% Numbering
+%===================================
+
+
+\newtheorem{definition}{Definition}[section]
+\newtheorem{example}{Example}[section]
+
+
+%===================================
+% Judgements
+%===================================
+
+
+\newcommand{\JM}[2]{\ensuremath{#1 : #2}}
+
+%===================================
+% Expressions
+%===================================
+
+\newcommand{\Case}[3][]{\ensuremath{#1\textsf{Case}~#2~\textsf of}~#3~\textsf{end}}
+
+%=======================================
+
+\newcommand{\snreglados} [3] {\begin{tabular}{c} \ensuremath{#1} \\[2pt]
+ \ensuremath{#2}\\ \hline \ensuremath{#3} \end{tabular}}
+
+
+\newcommand{\snregla} [2] {\begin{tabular}{c}
+ \ensuremath{#1}\\ \hline \ensuremath{#2} \end{tabular}}
+
+
+%=======================================
+