Merge PR #7466: Remove tutorials from the repo

9 files changed, 5 insertions, 7691 deletions

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
deleted file mode 100644
index 01369b900..000000000
--- a/doc/RecTutorial/RecTutorial.tex
+++ /dev/null
@@ -1,3690 +0,0 @@
-\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[utf8]{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 :=  
-    eq_refl : x = x
-For eq: Argument A is implicit
-For eq_refl: Argument A is implicit
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: 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 : eq_refl (2*6) = eq_refl (3*4).
-Proof.
- reflexivity.
-Qed.
-
-Print eq_proof_proof.
-\it eq_proof_proof = 
-eq_refl (eq_refl (3 * 4))
-     : eq_refl (2 * 6) = eq_refl (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 (eq_refl 0) (eq_refl 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) (eq_refl (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
-     eq_refl {\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', 
-                Z.le 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, 
-                  Z.le 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 the use of 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 div_aux 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 div\_aux 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 ``~\texttt{div\_aux}~'', 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
deleted file mode 100644
index 4a17e0818..000000000
--- a/doc/RecTutorial/RecTutorial.v
+++ /dev/null
@@ -1,1231 +0,0 @@
-Unset Automatic Introduction.
-
-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.t.
-
-Check (Vector.nil nat).
-
-Check (fun (A:Type)(a:A)=> Vector.cons _ a _ (Vector.nil _)).
-
-Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))).
-
-Lemma eq_3_3 : 2 + 1 = 3.
-Proof.
- reflexivity.
-Qed.
-Print eq_3_3.
-
-Lemma eq_proof_proof : eq_refl (2*6) = eq_refl (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.
-
-Require Extraction.
-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
-     eq_refl => 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.t A n) : Vector.t A (pred n):=
-match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
-| Vector.nil _ => Vector.nil A
-| Vector.cons _ _ n0 v0 => v0
-end.
-
-Definition Vtail' (A:Type)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
- intros A n v; case v.
- simpl.
- exact (Vector.nil 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',
-                       Z.le 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,
-                       Z.le 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.
-Fail exact typ.
-(*
-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 div_aux 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.t A 0), v = Vector.nil A.
-Proof.
- intros A v;inversion v.
-Abort.
-
-(*
- Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n),
-                                  n= 0 -> v = Vector.nil A.
-
-Toplevel input, characters 40281-40287
-> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),                                    n= 0 -> v = Vector.nil A.
->                                                                                                                 ^^^^^^
-Error: In environment
-A : Set
-n : nat
-v : Vector.t A n
-e : n = 0
-The term "Vector.nil A" has type "Vector.t A 0" while it is expected to have type
- "Vector.t A n"
-*)
- Require Import JMeq.
-
-
-(* On devrait changer Set en Type ? *)
-
-Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n),
-                                  n= 0 -> JMeq v (Vector.nil A).
-Proof.
- destruct v.
- auto.
- intro; discriminate.
-Qed.
-
-Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A.
-Proof.
- intros a v;apply JMeq_eq.
- apply vector0_is_vnil_aux.
- trivial.
-Qed.
-
-
-Implicit Arguments Vector.cons [A n].
-Implicit Arguments Vector.nil [A].
-Implicit Arguments Vector.hd [A n].
-Implicit Arguments Vector.tl [A n].
-
-Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
-Proof.
- destruct n; intro v.
- exact Vector.nil.
- exact (Vector.cons  (Vector.hd v) (Vector.tl v)).
-Defined.
-
-Eval simpl in (fun (A:Type)(v:Vector.t A 0) => (Vid _ _ v)).
-
-Eval simpl in (fun (A:Type)(v:Vector.t A 0) => v).
-
-
-
-Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v).
-Proof.
- destruct v.
- reflexivity.
- reflexivity.
-Defined.
-
-Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil.
-Proof.
- intros.
- change (Vector.nil (A:=A)) with (Vid _ 0 v).
- apply Vid_eq.
-Defined.
-
-
-Theorem decomp :
-  forall (A : Type) (n : nat) (v : Vector.t A (S n)),
-  v = Vector.cons (Vector.hd v) (Vector.tl v).
-Proof.
- intros.
- change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _  (S n) v).
- apply Vid_eq.
-Defined.
-
-
-
-Definition vector_double_rect :
-    forall (A:Type) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type),
-        P 0 Vector.nil Vector.nil ->
-        (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 ->
-             P (S n) (Vector.cons a v1) (Vector.cons  b v2)) ->
-        forall n (v1 v2 : Vector.t 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.t bool n :=
-   vector_double_rect bool  (fun n v1 v2 => Vector.t bool n)
-                        Vector.nil
-                        (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2.
-
-Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:Vector.t A p){struct v}
-                  : option A :=
-  match n,v  with
-    _   , Vector.nil => None
-  | 0   , Vector.cons b  _ => Some b
-  | S n', @Vector.cons _  _ p' v' => vector_nth A n' p' v'
-  end.
-
-Implicit Arguments vector_nth [A p].
-
-
-Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t 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
deleted file mode 100644
index 72d749269..000000000
--- a/doc/RecTutorial/coqartmacros.tex
+++ /dev/null
@@ -1,180 +0,0 @@
-\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 de Bruijn 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
deleted file mode 100644
index caee81782..000000000
--- a/doc/RecTutorial/manbiblio.bib
+++ /dev/null
@@ -1,870 +0,0 @@
-
-@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},
-}
-
-@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
deleted file mode 100644
index 438f2133d..000000000
--- a/doc/RecTutorial/morebib.bib
+++ /dev/null
@@ -1,55 +0,0 @@
-@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
deleted file mode 100644
index 0334553f2..000000000
--- a/doc/RecTutorial/recmacros.tex
+++ /dev/null
@@ -1,75 +0,0 @@
-%===================================
-% 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}}
-
-
-%=======================================
-
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 97231c9ec..aeb45611e 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -1201,15 +1201,6 @@ Decomposition}},
   note        = {\url{https://proofgeneral.github.io/}}
 }
 
-@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
-}
-
 @InCollection{wadler87,
   author      = {P. Wadler},
   title       = {Efficient  Compilation of Pattern Matching},
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 4a313df0c..75ff72c4d 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -2,12 +2,11 @@
 Introduction
 ------------------------
 
-This document is the Reference Manual of the |Coq|  proof
-assistant. A companion volume, the |Coq| Tutorial, is provided for the
-beginners. It is advised to read the Tutorial first. A
-book :cite:`CoqArt` on practical uses of the |Coq| system was
-published in 2004 and is a good support for both the beginner and the
-advanced user.
+This document is the Reference Manual of the |Coq| proof assistant.
+To start using Coq, it is advised to first read a tutorial.
+Links to several tutorials can be found at
+https://coq.inria.fr/documentation (see also
+https://github.com/coq/coq/wiki#coq-tutorials).
 
 The |Coq| system is designed to develop mathematical proofs, and
 especially to write formal specifications, programs and to verify that
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
deleted file mode 100644
index 77ce8574f..000000000
--- a/doc/tutorial/Tutorial.tex
+++ /dev/null
@@ -1,1575 +0,0 @@
-\documentclass[11pt,a4paper]{book}
-\usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
-\usepackage{textcomp}
-\usepackage{pslatex}
-\usepackage{hyperref}
-
-\input{../common/version.tex}
-\input{../common/macros.tex}
-\input{../common/title.tex}
-
-%\makeindex
-
-\begin{document}
-\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}{}
-
-%\tableofcontents
-
-\chapter*{Getting started}
-
-\Coq{} is a Proof Assistant for a Logical Framework known as the Calculus
-of Inductive Constructions. It allows the interactive construction of
-formal proofs, and also the manipulation of functional programs 
-consistently with their specifications. It runs as a computer program
-on many architectures.
-
-It is available with a variety of user interfaces. The present
-document does not attempt to present a comprehensive view of all the
-possibilities of \Coq, but rather to present in the most elementary
-manner a tutorial on the basic specification language, called Gallina,
-in which formal axiomatisations may be developed, and on the main
-proof tools.  For more advanced information, the reader could refer to
-the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y.
-Bertot and P. Castéran on practical uses of the \Coq{} system.
-
-Instructions on installation procedures, as well as more comprehensive
-documentation, may be found in the standard distribution of \Coq,
-which may be obtained from \Coq{} web site
-\url{https://coq.inria.fr/}\footnote{You can report any bug you find
-while using \Coq{} at \url{https://coq.inria.fr/bugs}. Make sure to
-always provide a way to reproduce it and to specify the exact version
-you used. You can get this information by running \texttt{coqc -v}}.
-\Coq{} is distributed together with a graphical user interface called
-CoqIDE. Alternative interfaces exist such as
-Proof General\footnote{See \url{https://proofgeneral.github.io/}.}.
-
-In the following examples, lines preceded by the prompt \verb:Coq < :
-represent user input, terminated by a period.
-The following lines usually show \Coq's answer.
-When used from a graphical user interface such as
-CoqIDE, the prompt is not displayed: user input is given in one window
-and \Coq's answers are displayed in a different window.
-
-\chapter{Basic Predicate Calculus}
-
-\section{An overview of the specification language Gallina}
-
-A formal development in Gallina consists in a sequence of {\sl declarations}
-and {\sl definitions}.
-
-\subsection{Declarations}
-
-A declaration associates a {\sl name} with a {\sl specification}.
-A name corresponds roughly to an identifier in a programming
-language, i.e. to a string of letters, digits, and a few ASCII symbols like
-underscore (\verb"_") and prime (\verb"'"), starting with a letter. 
-We use case distinction, so that the names \verb"A" and \verb"a" are distinct.
-Certain strings are reserved as key-words of \Coq, and thus are forbidden 
-as user identifiers.
-
-A specification is a formal expression which classifies the notion which is
-being declared. There are basically three kinds of specifications: 
-{\sl logical propositions}, {\sl mathematical collections}, and
-{\sl abstract types}. They are classified by the three basic sorts
-of the system, called respectively \verb:Prop:, \verb:Set:, and
-\verb:Type:, which are themselves atomic abstract types.
-
-Every valid expression $e$ in Gallina is associated with a specification,
-itself a valid expression, called its {\sl type} $\tau(E)$. We write
-$e:\tau(E)$ for the judgment that $e$ is of type $E$. 
-You may request \Coq{} to return to you the type of a valid expression by using
-the command \verb:Check::
-
-\begin{coq_eval}
-Set Printing Width 60.
-\end{coq_eval}
-
-\begin{coq_example}
-Check O.
-\end{coq_example}
-
-Thus we know that the identifier \verb:O: (the name `O', not to be
-confused with the numeral `0' which is not a proper identifier!) is
-known in the current context, and that its type is the specification 
-\verb:nat:. This specification is itself classified as a mathematical
-collection, as we may readily check:
-
-\begin{coq_example}
-Check nat.
-\end{coq_example}
-
-The specification \verb:Set: is an abstract type, one of the basic
-sorts of the Gallina language, whereas the notions $nat$ and $O$ are
-notions which are defined in the arithmetic prelude,
-automatically loaded when running the \Coq{} system.
-
-We start by introducing a so-called section name. The role of sections
-is to structure the modelisation by limiting the scope of parameters,
-hypotheses and definitions. It will also give a convenient way to
-reset part of the development.
-
-\begin{coq_example}
-Section Declaration.
-\end{coq_example}
-With what we already know, we may now enter in the system a declaration,
-corresponding to the informal mathematics {\sl let n be a natural
-  number}. 
-
-\begin{coq_example}
-Variable n : nat.
-\end{coq_example}
-
-If we want to translate a more precise statement, such as
-{\sl let n be a positive natural number},
-we have to add another declaration, which will declare explicitly the
-hypothesis \verb:Pos_n:, with specification the proper logical
-proposition:
-\begin{coq_example}
-Hypothesis Pos_n : (gt n 0).
-\end{coq_example}
-
-Indeed we may check that the relation \verb:gt: is known with the right type
-in the current context:
-
-\begin{coq_example}
-Check gt.
-\end{coq_example}
-
-which tells us that \texttt{gt} is a function expecting two arguments of
-type \texttt{nat} in order to build a logical proposition.
-What happens here is similar to what we are used to in a functional
-programming language: we may compose the (specification) type \texttt{nat}
-with the (abstract) type \texttt{Prop} of logical propositions through the
-arrow function constructor, in order to get a functional type
-\texttt{nat -> Prop}:
-\begin{coq_example}
-Check (nat -> Prop).
-\end{coq_example}
-which may be composed once more with \verb:nat: in order to obtain the
-type \texttt{nat -> nat -> Prop} of binary relations over natural numbers.
-Actually the type \texttt{nat -> nat -> Prop} is an abbreviation for 
-\texttt{nat -> (nat -> Prop)}.
-
-Functional notions may be composed in the usual way. An expression $f$
-of type $A\ra B$ may be applied to an expression $e$ of type $A$ in order
-to form the expression $(f~e)$ of type $B$. Here we get that
-the expression \verb:(gt n): is well-formed of type \texttt{nat -> Prop},
-and thus that the expression \verb:(gt n O):, which abbreviates
-\verb:((gt n) O):, is a well-formed proposition.
-\begin{coq_example}
-Check gt n O.
-\end{coq_example}
-
-\subsection{Definitions}
-
-The initial prelude contains a few arithmetic definitions:
-\texttt{nat} is defined as a mathematical collection (type \texttt{Set}),
-constants \texttt{O}, \texttt{S}, \texttt{plus}, are defined as objects of
-types respectively \texttt{nat}, \texttt{nat -> nat}, and \texttt{nat ->
-nat -> nat}.
-You may introduce new definitions, which link a name to a well-typed value.
-For instance, we may introduce the constant \texttt{one} as being defined
-to be equal to the successor of zero:
-\begin{coq_example}
-Definition one := (S O).
-\end{coq_example}
-We may optionally indicate the required type:
-\begin{coq_example}
-Definition two : nat := S one.
-\end{coq_example}
-
-Actually \Coq{} allows several possible syntaxes:
-\begin{coq_example}
-Definition three := S two : nat.
-\end{coq_example}
-
-Here is a way to define the doubling function, which expects an
-argument \verb:m: of type \verb:nat: in order to build its result as
-\verb:(plus m m)::
-
-\begin{coq_example}
-Definition double (m : nat) := plus m m.
-\end{coq_example}
-This introduces the constant \texttt{double} defined as the
-expression \texttt{fun m : nat => plus m m}.
-The abstraction introduced by \texttt{fun} is explained as follows.
-The expression \texttt{fun x : A => e} is well formed of type
-\texttt{A -> B} in a context whenever the expression \texttt{e} is
-well-formed of type \texttt{B} in the given context to which we add the
-declaration that \texttt{x} is of type \texttt{A}. Here \texttt{x} is a
-bound, or dummy variable in the expression \texttt{fun x : A => e}.
-For instance we could as well have defined \texttt{double} as
-\texttt{fun n : nat => (plus n n)}.
-
-Bound (local) variables and free (global) variables may be mixed.
-For instance, we may define the function which adds the constant \verb:n:
-to its argument as
-\begin{coq_example}
-Definition add_n (m:nat) := plus m n.
-\end{coq_example}
-However, note that here we may not rename the formal argument $m$ into $n$
-without capturing the free occurrence of $n$, and thus changing the meaning
-of the defined notion.
-
-Binding operations are well known for instance in logic, where they
-are called quantifiers.  Thus we may universally quantify a
-proposition such as $m>0$ in order to get a universal proposition
-$\forall m\cdot m>0$. Indeed this operator is available in \Coq, with
-the following syntax: \texttt{forall m : nat, gt m O}. Similarly to the
-case of the functional abstraction binding, we are obliged to declare
-explicitly the type of the quantified variable. We check:
-\begin{coq_example}
-Check (forall m : nat, gt m 0).
-\end{coq_example}
-
-\begin{coq_eval}
-Reset Initial.
-Set Printing Width 60.
-Set Printing Compact Contexts.
-\end{coq_eval}
-
-\section{Introduction to the proof engine: Minimal Logic}
-
-In the following, we are going to consider various propositions, built
-from atomic propositions $A, B, C$. This may be done easily, by
-introducing these atoms as global variables declared of type \verb:Prop:.
-It is easy to declare several names with the same specification:
-\begin{coq_example}
-Section Minimal_Logic.
-Variables A B C : Prop.
-\end{coq_example}
-
-We shall consider simple implications, such as $A\ra B$, read as 
-``$A$ implies $B$''. Note that we overload the arrow symbol, which
-has been used above as the functionality type constructor, and which
-may be used as well as propositional connective:
-\begin{coq_example}
-Check (A -> B).
-\end{coq_example}
-
-Let us now embark on a simple proof. We want to prove the easy tautology
-$((A\ra (B\ra C))\ra (A\ra B)\ra (A\ra C)$. 
-We enter the proof engine by the command
-\verb:Goal:, followed by the conjecture we want to verify:
-\begin{coq_example}
-Goal (A -> B -> C) -> (A -> B) -> A -> C.
-\end{coq_example}
-
-The system displays the current goal below a double line, local hypotheses
-(there are none initially) being displayed above the line. We call 
-the combination of local hypotheses with a goal a {\sl judgment}.
-We are now in an inner 
-loop of the system, in proof mode. 
-New commands are available in this
-mode, such as {\sl tactics}, which are proof combining primitives.
-A tactic operates on the current goal by attempting to construct a proof
-of the corresponding judgment, possibly from proofs of some
-hypothetical judgments, which are then added to the current
-list of conjectured judgments.
-For instance, the \verb:intro: tactic is applicable to any judgment
-whose goal is an implication, by moving the proposition to the left
-of the application to the list of local hypotheses:
-\begin{coq_example}
-intro H.
-\end{coq_example}
-
-Several introductions may be done in one step:
-\begin{coq_example}
-intros H' HA.
-\end{coq_example}
-
-We notice that $C$, the current goal, may be obtained from hypothesis
-\verb:H:, provided the truth of $A$ and $B$ are established.
-The tactic \verb:apply: implements this piece of reasoning:
-\begin{coq_example}
-apply H.
-\end{coq_example}
-
-We are now in the situation where we have two judgments as conjectures
-that remain to be proved. Only the first is listed in full, for the
-others the system displays only the corresponding subgoal, without its
-local hypotheses list. Note that \verb:apply: has kept the local
-hypotheses of its father judgment, which are still available for
-the judgments it generated.
-
-In order to solve the current goal, we just have to notice that it is
-exactly available as hypothesis $HA$:
-\begin{coq_example}
-exact HA.
-\end{coq_example}
-
-Now $H'$ applies:
-\begin{coq_example}
-apply H'.
-\end{coq_example}
-
-And we may now conclude the proof as before, with \verb:exact HA.:
-Actually, we may not bother with the name \verb:HA:, and just state that
-the current goal is solvable from the current local assumptions:
-\begin{coq_example}
-assumption.
-\end{coq_example}
-
-The proof is now finished. We are now going to ask \Coq{}'s kernel
-to check and save the proof.
-\begin{coq_example}
-Qed.
-\end{coq_example}
-
-Let us redo the same proof with a few variations. First of all we may name
-the initial goal as a conjectured lemma:
-\begin{coq_example}
-Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
-\end{coq_example}
-
-Next, we may omit the names of local assumptions created by the introduction
-tactics, they can be automatically created by the proof engine as new
-non-clashing names.
-\begin{coq_example}
-intros.
-\end{coq_example}
-
-The \verb:intros: tactic, with no arguments, effects as many individual
-applications of \verb:intro: as is legal.
-
-Then, we may compose several tactics together in sequence, or in parallel,
-through {\sl tacticals}, that is tactic combinators. The main constructions
-are the following:
-\begin{itemize}
-\item $T_1 ; T_2$ (read $T_1$ then $T_2$) applies tactic $T_1$ to the current
-goal, and then tactic $T_2$ to all the subgoals generated by $T_1$.
-\item $T; [T_1 | T_2 | ... | T_n]$ applies tactic $T$ to the current
-goal, and then tactic $T_1$ to the first newly generated subgoal, 
-..., $T_n$ to the nth.
-\end{itemize}
-
-We may thus complete the proof of \verb:distr_impl: with one composite tactic:
-\begin{coq_example}
-apply H; [ assumption | apply H0; assumption ].
-\end{coq_example}
-
-You should be aware however that relying on automatically generated names is
-not robust to slight updates to this proof script. Consequently, it is
-discouraged in finished proof scripts. As for the composition of tactics with
-\texttt{:} it may hinder the readability of the proof script and it is also
-harder to see what's going on when replaying the proof because composed
-tactics are evaluated in one go.
-
-Actually, such an easy combination of tactics \verb:intro:, \verb:apply:
-and \verb:assumption: may be found completely automatically by an automatic
-tactic, called \verb:auto:, without user guidance:
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
-auto.
-\end{coq_example}
-
-Let us now save lemma \verb:distr_impl::
-\begin{coq_example}
-Qed.
-\end{coq_example}
-
-\section{Propositional Calculus}
-
-\subsection{Conjunction}
-
-We have seen how \verb:intro: and \verb:apply: tactics could be combined
-in order to prove implicational statements. More generally, \Coq{} favors a style
-of reasoning, called {\sl Natural Deduction}, which decomposes reasoning into 
-so called {\sl introduction rules}, which tell how to prove a goal whose main 
-operator is a given propositional connective, and {\sl elimination rules},
-which tell how to use an hypothesis whose main operator is the propositional 
-connective. Let us show how to use these ideas for the propositional connectives
-\verb:/\: and \verb:\/:.
-
-\begin{coq_example}
-Lemma and_commutative : A /\ B -> B /\ A.
-intro H.
-\end{coq_example}
-
-We make use of the conjunctive hypothesis \verb:H: with the \verb:elim: tactic,
-which breaks it into its components:
-\begin{coq_example}
-elim H.
-\end{coq_example}
-
-We now use the conjunction introduction tactic \verb:split:, which splits the 
-conjunctive goal into the two subgoals:
-\begin{coq_example}
-split.
-\end{coq_example}
-and the proof is now trivial. Indeed, the whole proof is obtainable as follows:
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Lemma and_commutative : A /\ B -> B /\ A.
-intro H; elim H; auto.
-Qed.
-\end{coq_example}
-
-The tactic \verb:auto: succeeded here because it knows as a hint the 
-conjunction introduction operator \verb+conj+
-\begin{coq_example}
-Check conj.
-\end{coq_example}
-
-Actually, the tactic \verb+split+ is just an abbreviation for \verb+apply conj.+
-
-What we have just seen is that the \verb:auto: tactic is more powerful than
-just a simple application of local hypotheses; it tries to apply as well 
-lemmas which have been specified as hints. A 
-\verb:Hint Resolve: command registers a
-lemma as a hint to be used from now on by the \verb:auto: tactic, whose power 
-may thus be incrementally augmented.
-
-\subsection{Disjunction}
-
-In a similar fashion, let us consider disjunction:
-
-\begin{coq_example}
-Lemma or_commutative : A \/ B -> B \/ A.
-intro H; elim H.
-\end{coq_example}
-
-Let us prove the first subgoal in detail. We use \verb:intro: in order to
-be left to prove \verb:B\/A: from \verb:A::
-
-\begin{coq_example}
-intro HA.
-\end{coq_example}
-
-Here the hypothesis \verb:H: is not needed anymore. We could choose to
-actually erase it with the tactic \verb:clear:; in this simple proof it
-does not really matter, but in bigger proof developments it is useful to
-clear away unnecessary hypotheses which may clutter your screen.
-\begin{coq_example}
-clear H.
-\end{coq_example}
-
-The tactic \verb:destruct: combines the effects of \verb:elim:, \verb:intros:,
-and \verb:clear::
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Lemma or_commutative : A \/ B -> B \/ A.
-intros H; destruct H.
-\end{coq_example}
-
-The disjunction connective has two introduction rules, since \verb:P\/Q:
-may be obtained from \verb:P: or from \verb:Q:; the two corresponding
-proof constructors are called respectively \verb:or_introl: and
-\verb:or_intror:; they are applied to the current goal by tactics
-\verb:left: and \verb:right: respectively. For instance:
-\begin{coq_example}
-right.
-trivial.
-\end{coq_example}
-The tactic \verb:trivial: works like \verb:auto: with the hints
-database, but it only tries those tactics that can solve the goal in one
-step. 
-
-As before, all these tedious elementary steps may be performed automatically,
-as shown for the second symmetric case:
-
-\begin{coq_example}
-auto.
-\end{coq_example}
-
-However, \verb:auto: alone does not succeed in proving the full lemma, because
-it does not try any elimination step.
-It is a bit disappointing that \verb:auto: is not able to prove automatically 
-such a simple tautology. The reason is that we want to keep
-\verb:auto: efficient, so that it is always effective to use. 
-
-\subsection{Tauto}
-
-A complete tactic for propositional
-tautologies is indeed available in \Coq{} as the \verb:tauto: tactic.
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Lemma or_commutative : A \/ B -> B \/ A.
-tauto.
-Qed.
-\end{coq_example}
-
-It is possible to inspect the actual proof tree constructed by \verb:tauto:,
-using a standard command of the system, which prints the value of any notion 
-currently defined in the context:
-\begin{coq_example}
-Print or_commutative.
-\end{coq_example}
-
-It is not easy to understand the notation for proof terms without some
-explanations. The \texttt{fun} prefix, such as \verb+fun H : A\/B =>+, 
-corresponds
-to \verb:intro H:, whereas a subterm such as 
-\verb:(or_intror: \verb:B H0):
-corresponds to the sequence of tactics \verb:apply or_intror; exact H0:. 
-The generic combinator \verb:or_intror: needs to be instantiated by
-the two properties \verb:B: and \verb:A:. Because \verb:A: can be
-deduced from the type of \verb:H0:, only  \verb:B: is printed.
-The two instantiations are effected automatically by the tactic
-\verb:apply: when pattern-matching a goal. The specialist will of course
-recognize our proof term as a $\lambda$-term, used as notation for the
-natural deduction proof term through the Curry-Howard isomorphism. The
-naive user of \Coq{} may safely ignore these formal details.
-
-Let us exercise the \verb:tauto: tactic on a more complex example:
-\begin{coq_example}
-Lemma distr_and : A -> B /\ C -> (A -> B) /\ (A -> C).
-tauto.
-Qed.
-\end{coq_example}
-
-\subsection{Classical reasoning}
-
-The tactic \verb:tauto: always comes back with an answer. Here is an example where it 
-fails:
-\begin{coq_example}
-Lemma Peirce : ((A -> B) -> A) -> A.
-try tauto.
-\end{coq_example}
-
-Note the use of the \verb:try: tactical, which does nothing if its tactic
-argument fails.
-
-This may come as a surprise to someone familiar with classical reasoning. 
-Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for 
-every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation
-of Peirce's law may be proved in \Coq{} using \verb:tauto::
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A).
-tauto.
-Qed.
-\end{coq_example}
-
-In classical logic, the double negation of a proposition is equivalent to this 
-proposition, but in the constructive logic of \Coq{} this is not so. If you
-want to use classical logic in \Coq, you have to import explicitly the
-\verb:Classical: module, which will declare the axiom \verb:classic:
-of excluded middle, and classical tautologies such as de Morgan's laws.
-The \verb:Require: command is used to import a module from \Coq's library:
-\begin{coq_example}
-Require Import Classical.
-Check NNPP.
-\end{coq_example}
-
-and it is now easy (although admittedly not the most direct way) to prove
-a classical law such as Peirce's:
-\begin{coq_example}
-Lemma Peirce : ((A -> B) -> A) -> A.
-apply NNPP; tauto.
-Qed.
-\end{coq_example}
-
-Here is one more example of propositional reasoning, in the shape of
-a Scottish puzzle. A private club has the following rules:
-\begin{enumerate}
-\item Every non-scottish member wears red socks
-\item Every member wears a kilt or doesn't wear red socks
-\item The married members don't go out on Sunday
-\item A member goes out on Sunday if and only if he is Scottish
-\item Every member who wears a kilt is Scottish and married
-\item Every scottish member wears a kilt
-\end{enumerate}
-Now, we show that these rules are so strict that no one can be accepted.
-\begin{coq_example}
-Section club.
-Variables Scottish RedSocks WearKilt Married GoOutSunday : Prop.
-Hypothesis rule1 : ~ Scottish -> RedSocks.
-Hypothesis rule2 : WearKilt \/ ~ RedSocks.
-Hypothesis rule3 : Married -> ~ GoOutSunday.
-Hypothesis rule4 : GoOutSunday <-> Scottish.
-Hypothesis rule5 : WearKilt -> Scottish /\ Married.
-Hypothesis rule6 : Scottish -> WearKilt.
-Lemma NoMember : False.
-tauto.
-Qed.
-\end{coq_example}
-At that point \verb:NoMember: is a proof of the absurdity depending on
-hypotheses.
-We may end the section, in that case, the variables and hypotheses
-will be discharged, and the type of \verb:NoMember: will be
-generalised.
-
-\begin{coq_example}
-End club.
-Check NoMember.
-\end{coq_example}
-
-\section{Predicate Calculus}
-
-Let us now move into predicate logic, and first of all into first-order
-predicate calculus. The essence of predicate calculus is that to try to prove 
-theorems in the most abstract possible way, without using the definitions of 
-the mathematical notions, but by formal manipulations of uninterpreted 
-function and predicate symbols. 
-
-\subsection{Sections and signatures}
-
-Usually one works in some domain of discourse, over which range the individual 
-variables and function symbols. In \Coq{}, we speak in a language with a rich
-variety of types, so we may mix several domains of discourse, in our 
-multi-sorted language. For the moment, we just do a few exercises, over a 
-domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two 
-predicate symbols  \verb:P: and \verb:R: over \verb:D:, of arities 
-1 and 2, respectively.
-
-\begin{coq_eval}
-Reset Initial.
-Set Printing Width 60.
-Set Printing Compact Contexts.
-\end{coq_eval}
-
-We start by assuming a domain of
-discourse \verb:D:, and a binary relation \verb:R:  over \verb:D:: 
-\begin{coq_example}
-Section Predicate_calculus.
-Variable D : Set.
-Variable R : D -> D -> Prop.
-\end{coq_example}
-
-As a simple example of predicate calculus reasoning, let us assume
-that relation \verb:R: is symmetric and transitive, and let us show that
-\verb:R: is reflexive in any point \verb:x: which has an \verb:R: successor.
-Since we do not want to make the assumptions about \verb:R: global axioms of 
-a theory, but rather local hypotheses to a theorem, we open a specific
-section to this effect.
-\begin{coq_example}
-Section R_sym_trans.
-Hypothesis R_symmetric : forall x y : D, R x y -> R y x.
-Hypothesis R_transitive :
-    forall x y z : D, R x y -> R y z -> R x z.
-\end{coq_example}
-
-Note the syntax \verb+forall x : D,+ which stands for universal quantification
-$\forall x : D$.
-
-\subsection{Existential quantification}
-
-We now state our lemma, and enter proof mode.
-\begin{coq_example}
-Lemma refl_if : forall x : D, (exists y, R x y) -> R x x.
-\end{coq_example}
-
-The hypotheses that are local to the currently opened sections
-are listed as local hypotheses to the current goals.
-That is because these hypotheses are going to be discharged, as
-we shall see, when we shall close the corresponding sections.
-
-Note the functional syntax for existential quantification. The existential
-quantifier is built from the operator \verb:ex:, which expects a 
-predicate as argument:
-\begin{coq_example}
-Check ex.
-\end{coq_example}
-and the notation \verb+(exists x : D, P x)+ is just concrete syntax for 
-the expression \verb+(ex D (fun x : D => P x))+. 
-Existential quantification is handled in \Coq{} in a similar
-fashion to the connectives \verb:/\: and \verb:\/:: it is introduced by
-the proof combinator \verb:ex_intro:, which is invoked by the specific 
-tactic \verb:exists:, and its elimination provides a witness \verb+a : D+ to
-\verb:P:, together with an assumption \verb+h : (P a)+ that indeed \verb+a+
-verifies \verb:P:. Let us see how this works on this simple example.
-\begin{coq_example}
-intros x x_Rlinked.
-\end{coq_example}
-
-Note that \verb:intros: treats universal quantification in the same way
-as the premises of implications. Renaming of bound variables occurs
-when it is needed; for instance, had we started with \verb:intro y:,
-we would have obtained the goal:
-\begin{coq_eval}
-Undo.
-\end{coq_eval}
-\begin{coq_example}
-intro y.
-\end{coq_example}
-\begin{coq_eval}
-Undo.
-intros x x_Rlinked.
-\end{coq_eval}
-
-Let us now use the existential hypothesis \verb:x_Rlinked: to 
-exhibit an R-successor y of x. This is done in two steps, first with
-\verb:elim:, then with \verb:intros:
-
-\begin{coq_example}
-elim x_Rlinked.
-intros y Rxy.
-\end{coq_example}
-
-Now we want to use \verb:R_transitive:. The \verb:apply: tactic will know
-how to match \verb:x: with \verb:x:, and \verb:z: with \verb:x:, but needs
-help on how to instantiate \verb:y:, which appear in the hypotheses of
-\verb:R_transitive:, but not in its conclusion. We give the proper hint
-to \verb:apply: in a \verb:with: clause, as follows:
-\begin{coq_example}
-apply R_transitive with y.
-\end{coq_example}
-
-The rest of the proof is routine:
-\begin{coq_example}
-assumption.
-apply R_symmetric; assumption.
-\end{coq_example}
-\begin{coq_example*}
-Qed.
-\end{coq_example*}
-
-Let us now close the current section.
-\begin{coq_example}
-End R_sym_trans.
-\end{coq_example}
-
-All the local hypotheses have been
-discharged in the statement of \verb:refl_if:, which now becomes a general
-theorem in the first-order language declared in section 
-\verb:Predicate_calculus:. In this particular example, section
-\verb:R_sym_trans: has not been really useful, since we could have
-instead stated theorem \verb:refl_if: in its general form, and done 
-basically the same proof, obtaining \verb:R_symmetric: and
-\verb:R_transitive: as local hypotheses by initial \verb:intros: rather
-than as global hypotheses in the context. But if we had pursued the
-theory by proving more theorems about relation \verb:R:,
-we would have obtained all general statements at the closing of the section,
-with minimal dependencies on the hypotheses of symmetry and transitivity.
-
-\subsection{Paradoxes of classical predicate calculus}
-
-Let us illustrate this feature by pursuing our \verb:Predicate_calculus:
-section with an enrichment of our language: we declare a unary predicate
-\verb:P: and a constant \verb:d::
-\begin{coq_example}
-Variable P :  D -> Prop.
-Variable d : D.
-\end{coq_example}
-
-We shall now prove a well-known fact from first-order logic: a universal 
-predicate is non-empty, or in other terms existential quantification 
-follows from universal quantification.
-\begin{coq_example}
-Lemma weird : (forall x:D, P x) ->  exists a, P a.
- intro UnivP.
-\end{coq_example}
-
-First of all, notice the pair of parentheses around
-\verb+forall x : D, P x+ in
-the statement of lemma \verb:weird:.
-If we had omitted them, \Coq's parser would have interpreted the
-statement as a truly trivial fact, since we would 
-postulate an \verb:x: verifying \verb:(P x):. Here the situation is indeed
-more problematic. If we have some element in \verb:Set: \verb:D:, we may
-apply \verb:UnivP: to it and conclude, otherwise we are stuck. Indeed
-such an element \verb:d: exists, but this is just by virtue of our
-new signature. This points out a subtle difference between standard
-predicate calculus and \Coq. In standard first-order logic,
-the equivalent of lemma \verb:weird: always holds, 
-because such a rule is wired in the inference rules for quantifiers, the
-semantic justification being that the interpretation domain is assumed to
-be non-empty. Whereas in \Coq, where types are not assumed to be 
-systematically inhabited, lemma \verb:weird: only holds in signatures
-which allow the explicit construction of an element in the domain of
-the predicate. 
-
-Let us conclude the proof, in order to show the use of the \verb:exists:
-tactic:
-\begin{coq_example}
-exists d; trivial.
-Qed.
-\end{coq_example}
-
-Another fact which illustrates the sometimes disconcerting rules of
-classical 
-predicate calculus is Smullyan's drinkers' paradox: ``In any non-empty
-bar, there is a person such that if she drinks, then everyone drinks''.
-We modelize the bar by Set \verb:D:, drinking by predicate \verb:P:.
-We shall need classical reasoning. Instead of loading the \verb:Classical:
-module as we did above, we just state the law of excluded middle as a
-local hypothesis schema at this point:
-\begin{coq_example}
-Hypothesis EM : forall A : Prop, A \/ ~ A.
-Lemma drinker :  exists x : D, P x -> forall x : D, P x.
-\end{coq_example}
-The proof goes by cases on whether or not
-there is someone who does not drink. Such reasoning by cases proceeds
-by invoking the excluded middle principle, via \verb:elim: of the
-proper instance of \verb:EM::
-\begin{coq_example}
-elim (EM (exists x, ~ P x)).
-\end{coq_example}
-
-We first look at the first case. Let Tom be the non-drinker.
-The following combines at once the effect of \verb:intros: and
-\verb:destruct::
-\begin{coq_example}
-intros (Tom, Tom_does_not_drink).
-\end{coq_example}
-
-We conclude in that case by considering Tom, since his drinking leads to
-a contradiction:
-\begin{coq_example}
-exists Tom; intro Tom_drinks.
-\end{coq_example}
-
-There are several ways in which we may eliminate a contradictory case;
-in this case, we use \verb:contradiction: to let \Coq{} find out the
-two contradictory hypotheses:
-\begin{coq_example}
-contradiction.
-\end{coq_example}
-
-We now proceed with the second case, in which actually any person will do;
-such a John Doe is given by the non-emptiness witness \verb:d::
-\begin{coq_example}
-intro No_nondrinker; exists d; intro d_drinks.
-\end{coq_example}
-
-Now we consider any Dick in the bar, and reason by cases according to its
-drinking or not:
-\begin{coq_example}
-intro Dick; elim (EM (P Dick)); trivial.
-\end{coq_example}
-
-The only non-trivial case is again treated by contradiction:
-\begin{coq_example}
-intro Dick_does_not_drink; absurd (exists x, ~ P x); trivial.
-exists Dick; trivial.
-Qed.
-\end{coq_example}
-
-Now, let us close the main section and look at the complete statements
-we proved:
-\begin{coq_example}
-End Predicate_calculus.
-Check refl_if.
-Check weird.
-Check drinker.
-\end{coq_example}
-
-Note how the three theorems are completely generic in the most general 
-fashion;
-the domain \verb:D: is discharged in all of them, \verb:R: is discharged in
-\verb:refl_if: only, \verb:P: is discharged only in \verb:weird: and
-\verb:drinker:, along with the hypothesis that \verb:D: is inhabited. 
-Finally, the excluded middle hypothesis is discharged only in 
-\verb:drinker:.
-
-Note, too, that the name \verb:d: has vanished from
-the statements of \verb:weird: and \verb:drinker:, 
-since \Coq's pretty-printer replaces
-systematically a quantification such as \texttt{forall d : D, E},
-where \texttt{d} does not occur in \texttt{E},
-by the functional notation \texttt{D -> E}.
-Similarly the name \texttt{EM} does not appear in \texttt{drinker}.
-
-Actually, universal quantification, implication, 
-as well as function formation, are
-all special cases of one general construct of type theory called
-{\sl dependent product}. This is the mathematical construction 
-corresponding to an indexed family of functions. A function 
-$f\in \Pi x:D\cdot Cx$ maps an element $x$ of its domain $D$ to its
-(indexed) codomain $Cx$. Thus a proof of $\forall x:D\cdot Px$ is
-a function mapping an element $x$ of $D$ to a proof of proposition $Px$.
-
-
-\subsection{Flexible use of local assumptions}
-
-Very often during the course of a proof we want to retrieve a local
-assumption and reintroduce it explicitly in the goal, for instance
-in order to get a more general induction hypothesis. The tactic
-\verb:generalize: is what is needed here:
-
-\begin{coq_example}
-Section Predicate_Calculus.
-Variables P Q : nat -> Prop.
-Variable R :  nat -> nat -> Prop.
-Lemma PQR :
- forall x y:nat, (R x x -> P x -> Q x) -> P x -> R x y -> Q x.
-intros.
-generalize H0.
-\end{coq_example}
-
-Sometimes it may be convenient to state an intermediate fact.
-The tactic \verb:assert: does this and introduces a new subgoal
-for this fact to be proved first. The tactic \verb:enough: does
-the same while keeping this goal for later.
-\begin{coq_example}
-enough (R x x) by auto.
-\end{coq_example}
-We clean the goal by doing an \verb:Abort: command.
-\begin{coq_example*}
-Abort.
-\end{coq_example*}
-
-
-\subsection{Equality}
-
-The basic equality provided in \Coq{} is Leibniz equality, noted infix like
-\texttt{x = y}, when \texttt{x} and \texttt{y} are two expressions of
-type the same Set. The replacement of \texttt{x} by \texttt{y} in any
-term is effected by a variety of tactics, such as \texttt{rewrite}
-and \texttt{replace}.
-
-Let us give a few examples of equality replacement. Let us assume that
-some arithmetic function \verb:f: is null in zero:
-\begin{coq_example}
-Variable f : nat -> nat.
-Hypothesis foo : f 0 = 0.
-\end{coq_example}
-
-We want to prove the following conditional equality:
-\begin{coq_example*}
-Lemma L1 : forall k:nat, k = 0 -> f k = k.
-\end{coq_example*}
-
-As usual, we first get rid of local assumptions with \verb:intro::
-\begin{coq_example}
-intros k E.
-\end{coq_example}
-
-Let us now use equation \verb:E: as a left-to-right rewriting:
-\begin{coq_example}
-rewrite E.
-\end{coq_example}
-This replaced both occurrences of \verb:k: by \verb:O:. 
-
-Now \verb:apply foo: will finish the proof:
-
-\begin{coq_example}
-apply foo.
-Qed.
-\end{coq_example}
-
-When one wants to rewrite an equality in a right to left fashion, we should
-use \verb:rewrite <- E: rather than \verb:rewrite E: or the equivalent
-\verb:rewrite -> E:. 
-Let us now illustrate the tactic \verb:replace:.
-\begin{coq_example}
-Hypothesis f10 : f 1 = f 0.
-Lemma L2 : f (f 1) = 0.
-replace (f 1) with 0.
-\end{coq_example}
-What happened here is that the replacement left the first subgoal to be
-proved, but another proof obligation was generated by the \verb:replace:
-tactic, as the second subgoal. The first subgoal is solved immediately
-by applying lemma \verb:foo:; the second one transitivity and then 
-symmetry of equality, for instance with tactics \verb:transitivity: and 
-\verb:symmetry::
-\begin{coq_example}
-apply foo.
-transitivity (f 0); symmetry; trivial.
-\end{coq_example}
-In case the equality $t=u$ generated by \verb:replace: $u$ \verb:with:
-$t$ is an assumption
-(possibly modulo symmetry), it will be automatically proved and the
-corresponding goal will not appear. For instance:
-
-\begin{coq_eval}
-Restart.
-\end{coq_eval}
-\begin{coq_example}
-Lemma L2 : f (f 1) = 0.
-replace (f 1) with (f 0).
-replace (f 0) with 0; trivial.
-Qed.
-\end{coq_example}
-
-\section{Using definitions}
-
-The development of mathematics does not simply proceed by logical 
-argumentation from first principles: definitions are used in an essential way.
-A formal development proceeds by a dual process of abstraction, where one
-proves abstract statements in predicate calculus, and use of definitions, 
-which in the contrary one instantiates general statements with particular 
-notions in order to use the structure of mathematical values for the proof of
-more specialised properties.
-
-\subsection{Unfolding definitions}
-
-Assume that we want to develop the theory of sets represented as characteristic
-predicates over some universe \verb:U:. For instance:
-\begin{coq_example}
-Variable U : Type.
-Definition set := U -> Prop.
-Definition element (x : U) (S : set) := S x.
-Definition subset (A B : set) := 
-  forall x : U, element x A -> element x B.
-\end{coq_example}
-
-Now, assume that we have loaded a module of general properties about
-relations over some abstract type \verb:T:, such as transitivity:
-
-\begin{coq_example}
-Definition transitive (T : Type) (R : T -> T -> Prop) :=
-  forall x y z : T, R x y -> R y z -> R x z.
-\end{coq_example}
-
-We want to prove that \verb:subset: is a \verb:transitive:
-relation. 
-\begin{coq_example}
-Lemma subset_transitive : transitive set subset.
-\end{coq_example}
-
-In order to make any progress, one needs to use the definition of
-\verb:transitive:. The \verb:unfold: tactic, which replaces all
-occurrences of a defined notion by its definition in the current goal,
-may be used here.
-\begin{coq_example}
-unfold transitive.
-\end{coq_example}
-
-Now, we must unfold \verb:subset::
-\begin{coq_example}
-unfold subset.
-\end{coq_example}
-Now, unfolding \verb:element: would be a mistake, because indeed a simple proof
-can be found by \verb:auto:, keeping \verb:element: an abstract predicate:
-\begin{coq_example}
-auto.
-\end{coq_example}
-
-Many variations on \verb:unfold: are provided in \Coq. For instance,
-instead of unfolding all occurrences of \verb:subset:, we may want to
-unfold only one designated occurrence:
-\begin{coq_eval}
-Undo 2.
-\end{coq_eval}
-\begin{coq_example}
-unfold subset at 2.
-\end{coq_example}
-
-One may also unfold a definition in a given local hypothesis, using the
-\verb:in: notation:
-\begin{coq_example}
-intros.
-unfold subset in H.
-\end{coq_example}
-
-Finally, the tactic \verb:red: does only unfolding of the head occurrence
-of the current goal:
-\begin{coq_example}
-red.
-auto.
-Qed.
-\end{coq_example}
-
-
-\subsection{Principle of proof irrelevance}
-
-Even though in principle the proof term associated with a verified lemma
-corresponds to a defined value of the corresponding specification, such
-definitions cannot be unfolded in \Coq: a lemma is considered an {\sl opaque}
-definition. This conforms to the mathematical tradition of {\sl proof
-irrelevance}: the proof of a logical proposition does not matter, and the
-mathematical justification of a logical development relies only on
-{\sl provability} of the lemmas used in the formal proof. 
-
-Conversely, ordinary mathematical definitions can be unfolded at will, they
-are {\sl transparent}. 
-
-\chapter{Induction}
-
-\begin{coq_eval}
-Reset Initial.
-Set Printing Width 60.
-Set Printing Compact Contexts.
-\end{coq_eval}
-
-\section{Data Types as Inductively Defined Mathematical Collections}
-
-All the notions which were studied until now pertain to traditional
-mathematical logic. Specifications of objects were abstract properties
-used in reasoning more or less constructively; we are now entering
-the realm of inductive types, which specify the existence of concrete
-mathematical constructions.
-
-\subsection{Booleans}
-
-Let us start with the collection of booleans, as they are specified
-in the \Coq's \verb:Prelude: module: 
-\begin{coq_example}
-Inductive bool :  Set := true | false.
-\end{coq_example}
-
-Such a declaration defines several objects at once. First, a new
-\verb:Set: is declared, with name \verb:bool:. Then the {\sl constructors}
-of this \verb:Set: are declared, called \verb:true: and \verb:false:.
-Those are analogous to introduction rules of the new Set \verb:bool:.
-Finally, a specific elimination rule for \verb:bool: is now available, which
-permits to reason by cases on \verb:bool: values. Three instances are
-indeed defined as new combinators in the global context: \verb:bool_ind:,
-a proof combinator corresponding to reasoning by cases,
-\verb:bool_rec:, an if-then-else programming construct,
-and \verb:bool_rect:, a similar combinator at the level of types.
-Indeed:
-\begin{coq_example}
-Check bool_ind.
-Check bool_rec.
-Check bool_rect.
-\end{coq_example}
-
-Let us for instance prove that every Boolean is true or false.
-\begin{coq_example}
-Lemma duality : forall b:bool, b = true \/ b = false.
-intro b.
-\end{coq_example}
-
-We use the knowledge that \verb:b: is a \verb:bool: by calling tactic
-\verb:elim:, which is this case will appeal to combinator \verb:bool_ind:
-in order to split the proof according to the two cases:
-\begin{coq_example}
-elim b.
-\end{coq_example}
-
-It is easy to conclude in each case:
-\begin{coq_example}
-left; trivial.
-right; trivial.
-\end{coq_example}
-
-Indeed, the whole proof can be done with the combination of the
- \verb:destruct:, which combines \verb:intro: and \verb:elim:,
-with good old \verb:auto::
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Lemma duality : forall b:bool, b = true \/ b = false.
-destruct b; auto.
-Qed.
-\end{coq_example}
-
-\subsection{Natural numbers}
-
-Similarly to Booleans, natural numbers are defined in the \verb:Prelude:
-module with constructors \verb:S: and \verb:O::
-\begin{coq_example}
-Inductive nat : Set :=
-  | O : nat
-  | S : nat -> nat.
-\end{coq_example}
-
-The elimination principles which are automatically generated are Peano's
-induction principle, and a recursion operator:
-\begin{coq_example}
-Check nat_ind.
-Check nat_rec.
-\end{coq_example}
-
-Let us start by showing how to program the standard primitive recursion
-operator \verb:prim_rec: from the more general \verb:nat_rec::
-\begin{coq_example}
-Definition prim_rec := nat_rec (fun i : nat => nat).
-\end{coq_example}
-
-That is, instead of computing for natural \verb:i: an element of the indexed
-\verb:Set: \verb:(P i):, \verb:prim_rec: computes uniformly an element of 
-\verb:nat:. Let us check the type of \verb:prim_rec::
-\begin{coq_example}
-About prim_rec.
-\end{coq_example}
-
-Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
-get an apparently more complicated expression.
-In fact, the two types are convertible and one way of having the proper
-type would be to do some computation before actually defining \verb:prim_rec:
-as such:
-
-\begin{coq_eval}
-Reset Initial.
-Set Printing Width 60.
-Set Printing Compact Contexts.
-\end{coq_eval}
-
-\begin{coq_example}
-Definition prim_rec :=
-    Eval compute in nat_rec (fun i : nat => nat).
-About prim_rec.
-\end{coq_example}
-
-Let us now show how to program addition with primitive recursion:
-\begin{coq_example}
-Definition addition (n m:nat) :=
-    prim_rec m (fun p rec : nat => S rec) n.
-\end{coq_example}
-
-That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
-according to its main constructor; when \verb:n = O:, we get \verb:m:;
- when \verb:n = S p:, we get \verb:(S rec):, where \verb:rec: is the result
-of the recursive computation \verb+(addition p m)+. Let us verify it by
-asking \Coq{} to compute for us say $2+3$:
-\begin{coq_example}
-Eval compute in (addition (S (S O)) (S (S (S O)))).
-\end{coq_example}
-
-Actually, we do not have to do all explicitly. {\Coq} provides a
-special syntax {\tt Fixpoint/match} for generic primitive recursion,
-and we could thus have defined directly addition as:
-
-\begin{coq_example}
-Fixpoint plus (n m:nat) {struct n} : nat :=
-  match n with
-  | O => m
-  | S p => S (plus p m)
-  end.
-\end{coq_example}
-
-\begin{coq_eval}
-\begin{coq_example}
-Reset Initial.
-Set Printing Width 60.
-Set Printing Compact Contexts.
-\end{coq_eval}
-
-\subsection{Simple proofs by induction}
-
-Let us now show how to do proofs by structural induction. We start with easy
-properties of the \verb:plus: function we just defined. Let us first
-show that $n=n+0$.
-\begin{coq_example}
-Lemma plus_n_O : forall n : nat, n = n + 0.
-intro n; elim n.
-\end{coq_example}
-
-What happened was that \texttt{elim n}, in order to construct a \texttt{Prop}
-(the initial goal) from a \texttt{nat} (i.e. \texttt{n}), appealed to the
-corresponding induction principle \texttt{nat\_ind} which we saw was indeed
-exactly Peano's induction scheme. Pattern-matching instantiated the 
-corresponding predicate \texttt{P} to \texttt{fun n : nat => n = n + 0},
-and we get as subgoals the corresponding instantiations of the base case
-\texttt{(P O)}, and of the inductive step
-\texttt{forall y : nat, P y -> P (S y)}.
-In each case we get an instance of function \texttt{plus} in which its second
-argument starts with a constructor, and is thus amenable to simplification
-by primitive recursion. The \Coq{} tactic \texttt{simpl} can be used for
-this purpose:
-\begin{coq_example}
-simpl.
-auto.
-\end{coq_example}
-
-We proceed in the same way for the base step:
-\begin{coq_example}
-simpl; auto.
-Qed.
-\end{coq_example}
-
-Here \verb:auto: succeeded, because it used as a hint lemma \verb:eq_S:,
-which say that successor preserves equality:
-\begin{coq_example}
-Check eq_S.
-\end{coq_example}
-
-Actually, let us see how to declare our lemma \verb:plus_n_O: as a hint
-to be used by \verb:auto::
-\begin{coq_example}
-Hint Resolve plus_n_O .
-\end{coq_example}
-
-We now proceed to the similar property concerning the other constructor
-\verb:S::
-\begin{coq_example}
-Lemma plus_n_S : forall n m:nat, S (n + m) = n + S m.
-\end{coq_example}
-
-We now go faster, using the tactic \verb:induction:, which does the
-necessary \verb:intros: before applying \verb:elim:. Factoring simplification
-and automation in both cases thanks to tactic composition, we prove this
-lemma in one line:
-\begin{coq_example}
-induction n; simpl; auto.
-Qed.
-Hint Resolve plus_n_S .
-\end{coq_example}
-
-Let us end this exercise with the commutativity of \verb:plus::
-
-\begin{coq_example}
-Lemma plus_com : forall n m:nat, n + m = m + n.
-\end{coq_example}
-
-Here we have a choice on doing an induction on \verb:n: or on \verb:m:, the
-situation being symmetric. For instance:
-\begin{coq_example}
-induction m as [ | m IHm ]; simpl; auto.
-\end{coq_example}
-
-Here \verb:auto: succeeded on the base case, thanks to our hint
-\verb:plus_n_O:, but the induction step requires rewriting, which
-\verb:auto: does not handle:
-
-\begin{coq_example}
-rewrite <- IHm; auto.
-Qed.
-\end{coq_example}
-
-\subsection{Discriminate}
-
-It is also possible to define new propositions by primitive recursion.
-Let us for instance define the predicate which discriminates between
-the constructors \verb:O: and \verb:S:: it computes to \verb:False: 
-when its argument is \verb:O:, and to \verb:True: when its argument is 
-of the form \verb:(S n)::
-\begin{coq_example}
-Definition Is_S (n : nat) := match n with
-                             | O => False
-                             | S p => True
-                             end.
-\end{coq_example}
-
-Now we may use the computational power of \verb:Is_S: to prove
-trivially that \verb:(Is_S (S n))::
-\begin{coq_example}
-Lemma S_Is_S : forall n:nat, Is_S (S n).
-simpl; trivial.
-Qed.
-\end{coq_example}
-
-But we may also use it to transform a \verb:False: goal into 
-\verb:(Is_S O):. Let us show a particularly important use of this feature;
-we want to prove that \verb:O: and \verb:S: construct different values, one
-of Peano's axioms:
-\begin{coq_example}
-Lemma no_confusion : forall n:nat, 0 <> S n.
-\end{coq_example}
-
-First of all, we replace negation by its definition, by reducing the
-goal with tactic \verb:red:; then we get contradiction by successive
-\verb:intros::
-\begin{coq_example}
-red; intros n H.
-\end{coq_example}
-
-Now we use our trick:
-\begin{coq_example}
-change (Is_S 0).
-\end{coq_example}
-
-Now we use equality in order to get a subgoal which computes out to 
-\verb:True:, which finishes the proof:
-\begin{coq_example}
-rewrite H; trivial.
-simpl; trivial.
-\end{coq_example}
-
-Actually, a specific tactic \verb:discriminate: is provided
-to produce mechanically such proofs, without the need for the user to define
-explicitly the relevant discrimination predicates:
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Lemma no_confusion : forall n:nat, 0 <> S n.
-intro n; discriminate.
-Qed.
-\end{coq_example}
-
-
-\section{Logic programming}
-
-In the same way as we defined standard data-types above, we
-may define inductive families, and for instance inductive predicates.
-Here is the definition of predicate $\le$ over type \verb:nat:, as
-given in \Coq's \verb:Prelude: module:
-\begin{coq_example*}
-Inductive le (n : nat) : nat -> Prop :=
-  | le_n : le n n
-  | le_S : forall m : nat, le n m -> le n (S m).
-\end{coq_example*}
-
-This definition introduces a new predicate
-\verb+le : nat -> nat -> Prop+,
-and the two constructors \verb:le_n: and \verb:le_S:, which are the
-defining clauses of \verb:le:. That is, we get not only the ``axioms''
-\verb:le_n: and \verb:le_S:, but also the converse property, that 
-\verb:(le n m): if and only if this statement can be obtained as a
-consequence of these defining clauses; that is, \verb:le: is the
-minimal predicate verifying clauses \verb:le_n: and \verb:le_S:. This is
-insured, as in the case of inductive data types, by an elimination principle,
-which here amounts to an induction principle \verb:le_ind:, stating this 
-minimality property:
-\begin{coq_example}
-Check le.
-Check le_ind.
-\end{coq_example}
-
-Let us show how proofs may be conducted with this principle.
-First we show that $n\le m \Rightarrow n+1\le m+1$:
-\begin{coq_example}
-Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m).
-intros n m n_le_m.
-elim n_le_m.
-\end{coq_example}
-
-What happens here is similar to the behaviour of \verb:elim: on natural
-numbers: it appeals to the relevant induction principle, here \verb:le_ind:,
-which generates the two subgoals, which may then be solved easily
-with the help of the defining clauses of \verb:le:.
-\begin{coq_example}
-apply le_n; trivial.
-intros; apply le_S; trivial.
-\end{coq_example}
-
-Now we know that it is a good idea to give the defining clauses as hints,
-so that the proof may proceed with a simple combination of 
-\verb:induction: and \verb:auto:. \verb:Hint Constructors le:
-is just an abbreviation for \verb:Hint Resolve le_n le_S:.
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Hint Constructors le.
-Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m).
-\end{coq_example}
-
-We have a slight problem however. We want to say ``Do an induction on
-hypothesis \verb:(le n m):'', but we have no explicit name for it. What we
-do in this case is to say ``Do an induction on the first unnamed hypothesis'',
-as follows.
-\begin{coq_example}
-induction 1; auto.
-Qed.
-\end{coq_example}
-
-Here is a more tricky problem. Assume we want to show that
-$n\le 0 \Rightarrow n=0$. This reasoning ought to follow simply from the
-fact that only the first defining clause of \verb:le: applies.
-\begin{coq_example} 
-Lemma tricky : forall n:nat, le n 0 -> n = 0.
-\end{coq_example}
-
-However, here trying something like \verb:induction 1: would lead
-nowhere (try it and see what happens). 
-An induction on \verb:n: would not be convenient either.
-What we must do here is analyse the definition of \verb"le" in order
-to match hypothesis \verb:(le n O): with the defining clauses, to find
-that only \verb:le_n: applies, whence the result. 
-This analysis may be performed by the ``inversion'' tactic
-\verb:inversion_clear: as follows:
-\begin{coq_example} 
-intros n H; inversion_clear H.
-trivial.
-Qed.
-\end{coq_example}
-
-\chapter{Modules}
-
-\begin{coq_eval}
-Reset Initial.
-Set Printing Width 60.
-Set Printing Compact Contexts.
-\end{coq_eval}
-
-\section{Opening library modules}
-
-When you start \Coq{} without further requirements in the command line,
-you get a bare system with few libraries loaded.  As we saw, a standard
-prelude module provides the standard logic connectives, and a few
-arithmetic notions. If you want to load and open other modules from
-the library, you have to use the \verb"Require" command, as we saw for
-classical logic above. For instance, if you want more arithmetic
-constructions, you should request:
-\begin{coq_example*}
-Require Import Arith.
-\end{coq_example*}
-
-Such a command looks for a (compiled) module file \verb:Arith.vo: in
-the libraries registered by \Coq. Libraries inherit the structure of
-the file system of the operating system and are registered with the
-command \verb:Add LoadPath:. Physical directories are mapped to
-logical directories. Especially the standard library of \Coq{} is
-pre-registered as a library of name \verb=Coq=.  Modules have absolute
-unique names denoting their place in \Coq{} libraries.  An absolute
-name is a sequence of single identifiers separated by dots.  E.g. the
-module \verb=Arith= has full name \verb=Coq.Arith.Arith= and because
-it resides in eponym subdirectory \verb=Arith= of the standard
-library, it can be as well required by the command
-
-\begin{coq_example*}
-Require Import Coq.Arith.Arith.
-\end{coq_example*}
-
-This may be useful to avoid ambiguities if somewhere, in another branch
-of the libraries known by Coq, another module is also called
-\verb=Arith=. Notice that by default, when a library is registered,
-all its contents, and all the contents of its subdirectories recursively are
-visible and accessible by a short (relative) name as \verb=Arith=.
-Notice also that modules or definitions not explicitly registered in
-a library are put in a default library called \verb=Top=.
-
-The loading of a compiled file is quick, because the corresponding
-development is not type-checked again. 
-
-\section{Creating your own modules}
-
-You may create your own module files, by writing {\Coq} commands in a file,
-say \verb:my_module.v:. Such a module may be simply loaded in the current
-context, with command \verb:Load my_module:. It may also be compiled,
-in ``batch'' mode, using the UNIX command
-\verb:coqc:. Compiling the module \verb:my_module.v: creates a 
-file \verb:my_module.vo:{} that can be reloaded with command
-\verb:Require: \verb:Import: \verb:my_module:. 
-
-If a required module depends on other modules then the latters are
-automatically required beforehand. However their contents is not
-automatically visible.  If you want a module \verb=M= required in a
-module \verb=N= to be automatically visible when \verb=N= is required,
-you should use \verb:Require Export M: in your module \verb:N:.
-
-\section{Managing the context}
-
-It is often difficult to remember the names of all lemmas and
-definitions available in the current context, especially if large
-libraries have been loaded. A convenient \verb:Search: command
-is available to lookup all known facts 
-concerning a given predicate. For instance, if you want to know all the
-known lemmas about both the successor and the less or equal relation, just ask:
-\begin{coq_eval}
-Reset Initial.
-Set Printing Width 60.
-Set Printing Compact Contexts.
-\end{coq_eval}
-\begin{coq_example}
-Search S le.
-\end{coq_example}
-Another command \verb:SearchHead: displays only lemmas where the searched
-predicate appears at the head position in the conclusion.
-\begin{coq_example}
-SearchHead le.
-\end{coq_example}
-
-The \verb:Search: commands also allows finding the theorems
-containing a given pattern, where \verb:_: can be used in
-place of an arbitrary term. As shown in this example, \Coq{}
-provides usual infix notations for arithmetic operators.
-
-\begin{coq_example}
-Search (_ + _ = _).
-\end{coq_example}
-
-\section{Now you are on your own}
-
-This tutorial is necessarily incomplete. If you wish to pursue serious
-proving in \Coq, you should now get your hands on \Coq's Reference Manual,
-which contains a complete description of all the tactics we saw, 
-plus many more.
-You also should look in the library of developed theories which is distributed
-with \Coq, in order to acquaint yourself with various proof techniques.
-
-
-\end{document}
-