From bcc04ed11734c90101049d12485558609df50f77 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 16 Aug 2006 12:59:07 +0000
Subject: MAJ Rectutorial (P. Castéran)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9068 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RecTutorial/RecTutorial.tex | 297 +++++++++++++++++++++++++---------------
 1 file changed, 189 insertions(+), 108 deletions(-)

(limited to 'doc/RecTutorial/RecTutorial.tex')

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index 9ee913d472..a80f6cacb3 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -49,7 +49,7 @@ Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}}
 
 \begin{abstract}
 This document\footnote{The first versions of this document were entirely written by Eduardo Gimenez.
-Pierre Cast\'eran wrote the 2004 revision.} is an introduction to the definition and
+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,
@@ -123,6 +123,7 @@ about dependent case analysis. Finally, Section
 --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.
 
@@ -142,14 +143,14 @@ respectively.  For instance, the \coq{} statement
 % inclusion numero 1
 % traduction numero 1
 \begin{alltt}
-\hide{Open Scope nat_scope. Check (}forall A:Set,(exists x : A, forall (y:A), x <> y) -> 2 = 3\hide{).}
+\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:Set,(\exsym{}x:A, {\prodsym}y:A, x {\coqdiff} y) \arrow{} 2 = 3\hide{).}
+\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
@@ -242,13 +243,17 @@ 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}:
+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 : Set) : Set :=
+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
@@ -260,7 +265,7 @@ For cons: Argument scopes are [type_scope _ _]
 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{Set}.
+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 
@@ -269,7 +274,7 @@ parameter \citecoq{A}.
 \begin{alltt}
 Check list.
 \it list
-     : Set {\arrow} Set
+     : Type {\arrow} Type
 
 \tt Check (nil (A:=nat)).
 \it nil
@@ -279,20 +284,32 @@ Check list.
 \it nil
      : list (nat {\arrow} nat)
 
-\tt Check (fun A: Set {\funarrow} (cons (A:=A))).
-\it fun A : Set {\funarrow} cons (A:=A)
-     : {\prodsym} A : Set, A {\arrow} list A {\arrow} list A
+\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 set, and $n$ a natural number, ``~\citecoq{vector $A$ $n$}~''
+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$.
 
 
@@ -301,7 +318,7 @@ Require Import  Bvector.
 
 Print vector.
 \it
-Inductive vector (A : Set) : nat {\arrow} Set :=
+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]
@@ -322,9 +339,9 @@ Check (Vnil nat).
 \it Vnil nat
      : vector nat 0
 
-\tt Check (fun (A:Set)(a:A){\funarrow} Vcons _ a _ (Vnil _)).
-\it fun (A : Set) (a : A) {\funarrow} Vcons A a 0 (Vnil A)
-     : {\prodsym} A : Set, A {\arrow} vector A 1
+\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 _))).
@@ -456,7 +473,8 @@ Qed.
 \end{alltt}
 
 Notice that the strict order on \texttt{nat}, called \citecoq{lt}
-is not inductively defined:
+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.
@@ -466,17 +484,67 @@ lt = fun n m : nat {\funarrow} S n {\coqle} m
 \tt
 Lemma zero_lt_three : 0 < 3.
 Proof.
- unfold lt.
-\it
-====================
- 1 {\coqle} 3
-\tt
  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 construtor 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
@@ -636,7 +704,9 @@ let max n p =
 \end{alltt}
 
 Another example of use of \citecoq{sumbool} is given  in Section
-\ref{WellFoundedRecursion}.
+\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
@@ -653,7 +723,7 @@ 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 universe $\Set$,
+version of existential quantification inhabiting the universes $\Type_i$,
 which is noted \texttt{sig $P$}. The syntax
 ``~\citecoq{\{$x$:$A$ | $B$\}}~'' is an abreviation for ``~\citecoq{sig (fun $x$:$A$ {\funarrow} $B$)}~''.
 
@@ -677,9 +747,9 @@ Mutually dependent definitions of recursive types are also allowed in
 introduction of the trees of unbounded (but finite) width:
 \label{Forest}
 \begin{alltt} 
-Inductive tree(A:Set)   : Set :=
+Inductive tree(A:Type)   : Type :=
     node : A {\arrow} forest A \arrow{} tree A 
-with  forest (A: Set)   : Set := 
+with  forest (A: Set)   : Type := 
     nochild  : forest A |
     addchild : tree A \arrow{} forest A \arrow{} forest A.
 \end{alltt}
@@ -709,7 +779,7 @@ Qed.
 \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 for an inductive type is \emph{case analysis}.
+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}.
@@ -727,7 +797,7 @@ 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$:)
+$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\\
@@ -792,7 +862,7 @@ For a pattern matching construct of the form
 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{Set}$, and $n:\citecoq{nat}$.
+$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)$.
@@ -806,7 +876,7 @@ which constraint holds on the branches of the pattern matching:
 \label{Prod-sup-rule}
 \[
 \begin{array}[t]{l}
-Q: \texttt{nat}{\arrow}\texttt{Set}\quad{t_O}:{{Q\;\texttt{O}}}  \quad
+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}}
@@ -815,7 +885,7 @@ Q: \texttt{nat}{\arrow}\texttt{Set}\quad{t_O}:{{Q\;\texttt{O}}}  \quad
 
 
 The interest of this rule of \textsl{dependent} pattern-matching is
-that it can also be read as the following logical principle (replacing \citecoq{Set}
+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
@@ -962,6 +1032,7 @@ analysis of it.
 
 \begin{alltt}
 Theorem fromFalse : False \arrow{} 0=1.
+Proof.
  intro H. 
  contradiction.
 Qed.
@@ -1007,7 +1078,7 @@ 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$~''.
+The following term is a proof  of ``~$Q\;a\, \arrow{}\, Q\;b$~''.
 
 \begin{alltt}
 fun H : Q a {\funarrow}
@@ -1244,7 +1315,7 @@ The header of the function we want to build is the following:
 
 \begin{verbatim}
 Definition Vtail_total 
-   (A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
+   (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
 \end{verbatim}
 
 Since the branches will not have the same type
@@ -1266,8 +1337,8 @@ to ``~\citecoq{vector A 0}~''. So, we propose:
 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 in ``~\citecoq{vector A (pred (S n0))}~'',
-convertible to ``~\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
@@ -1277,7 +1348,7 @@ Here is the full definition:
 
 \begin{alltt}
 Definition Vtail_total 
-   (A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
+   (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
@@ -1343,7 +1414,7 @@ Variable lambda : (Lambda {\arrow} False) {\arrow}Lambda.
 
 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
+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$)}~''
@@ -1355,7 +1426,7 @@ Variable matchL : Lambda {\arrow}
                   Q.
 \end{alltt}
 
-From these constants, it is possible to define application by case
+>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.
 
@@ -1419,7 +1490,7 @@ usually a synonymous of inconsistency.
 %definition above are called \textsl{strictly positive} types.
 
 
-\paragraph{} In this case, the construction of a non-terminating
+\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}. 
 
@@ -1571,9 +1642,9 @@ adding an extra type to the definition, as was done in Section
 
 \subsubsection{Impredicative Inductive Types}
 
-An inductive type $R$ inhabiting a universe $S$ is \textsl{predicative}
-if the introduction rules of $R$ do not make a universal
-quantification on a universe containing $S$. All the recursive 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
@@ -1599,18 +1670,21 @@ Inductive prop : Prop :=
 
 Notice
 that the constructor of this type can be used to inject any
-proposition --even itself!-- into the type. A careless use of such a
+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}.
 
 
-\begin{alltt}
-Lemma prop_inject: prop.
-Proof prop_intro prop.
-\end{alltt}
-
 Another example is the second order existential quantifier for propositions:
 
 \begin{alltt}
@@ -1681,9 +1755,9 @@ Inductive  typ : Type :=
 Definition typ_inject: typ.
  split; exact typ.
 \it Proof completed
+
 \tt{}Defined.
-\it
-Error: Universe Inconsistency.
+\it Error: Universe Inconsistency.
 \tt
 Abort.
 \end{alltt}
@@ -1984,7 +2058,7 @@ using the tactic \texttt{trivial}.
 
 \begin{alltt}
 
- Lemma list_inject : {\prodsym} (A:Set)(a b :A)(l l':list A),
+ 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.
@@ -2008,7 +2082,7 @@ Qed.
 
 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
+$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
@@ -2529,23 +2603,23 @@ Fixpoint nat_double_ind (n m:nat)\{struct n\} : P n m :=
 End Principle_of_Double_Induction.
 \end{alltt}
 
-Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Set$,
-another combinator \texttt{nat\_double\_rec} for constructing 
+Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Type$,
+another combinator \texttt{nat\_double\_rect} for constructing 
 (certified) programs can be defined in exactly the same way.
-This definition is left as an exercise.\label{natdoublerec}
+This definition is left as an exercise.\label{natdoublerect}
 
 \iffalse
 \begin{alltt}
 Section Principle_of_Double_Recursion.
-Variable    P               : nat {\arrow} nat {\arrow} Set.
+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_rec (n m:nat)\{struct n\} : P n 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_rec x y)
+         |  (S x), (S y) {\funarrow} inductive_step x y (nat_double_rect x y)
      end.
 End Principle_of_Double_Recursion.
 \end{alltt}
@@ -2555,7 +2629,7 @@ numbers can be defined in the following way:
 
 \begin{alltt}
 Definition min : nat {\arrow} nat {\arrow} nat  := 
-  nat_double_rec (fun (x y:nat) {\funarrow} 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).
@@ -2624,8 +2698,8 @@ Proof.
  intros n p.
 \end{alltt}
 
-Let us prove this theorem using the combinator \texttt{nat\_double\_rec}
-of section~\ref{natdoublerec}. The example also illustrates how
+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
@@ -2635,7 +2709,7 @@ goal, the result is not the expected one.
 
 %\pagebreak
 \begin{alltt}
- elim n using nat_double_rec.
+ elim n using nat_double_rect.
 \it
 4 subgoals
   
@@ -2746,6 +2820,11 @@ $(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}
@@ -2761,7 +2840,7 @@ first to introduce the predicate of accessibility.
 \begin{alltt}
 Print Acc.
 \it
-Inductive Acc (A : Set) (R : A {\arrow} A {\arrow} Prop) (x:A) : Prop :=
+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
@@ -2773,6 +2852,8 @@ For Acc_intro: Arguments A, R are implicit
 $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
@@ -2997,7 +3078,7 @@ We want to prove a quite trivial property: the only value of type
 Our first naive attempt leads to a \emph{cul-de-sac}.
 \begin{alltt}
 Lemma vector0_is_vnil : 
-  {\prodsym} (A:Set)(v:vector A 0), v = Vnil A.
+  {\prodsym} (A:Type)(v:vector A 0), v = Vnil A.
 Proof.
  intros A v;inversion v.
 \it
@@ -3019,11 +3100,11 @@ Unfortunately, even the statement of our lemma is refused!
 
 \begin{alltt}
  Lemma vector0_is_vnil_aux : 
- {\prodsym} (A:Set)(n:nat)(v:vector A n), n = 0 {\arrow} v = Vnil A.
+ {\prodsym} (A:Type)(n:nat)(v:vector A n), n = 0 {\arrow} v = Vnil A.
 
 \it
 Error: In environment
-A : Set
+A : Type
 n : nat
 v : vector A n
 e : n = 0
@@ -3040,7 +3121,7 @@ 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.
+heterogeneous equality to a standard one \footnote{At this date (July 28th 2006), the type of JMeq still uses Set instead of Type; the two following theorems are thus less generic than we can expect}.
 
 \begin{alltt}
 Lemma vector0_is_vnil_aux : 
@@ -3082,7 +3163,7 @@ Implicit Arguments Vnil [A].
 Implicit Arguments Vhead [A n].
 Implicit Arguments Vtail [A n].
 
-Definition Vid : {\prodsym} (A : Set)(n:nat), vector A n {\arrow} vector A n.
+Definition Vid : {\prodsym} (A : Type)(n:nat), vector A n {\arrow} vector A n.
 Proof.
  destruct n; intro v.
  exact Vnil.
@@ -3094,12 +3175,12 @@ Defined.
 Then we prove that \citecoq{Vid} is the identity on vectors:
 
 \begin{alltt}
-Lemma Vid_eq : {\prodsym} (n:nat) (A:Set)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : {\prodsym} (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
 Proof.
  destruct v.
 
 \it
-   A : Set
+   A : Type
   ============================
    Vnil = Vid A 0 Vnil
 
@@ -3116,18 +3197,18 @@ dialogue shows that \citecoq{Vid} has some interesting computational
 properties:
 
 \begin{alltt}
-Eval simpl in (fun (A:Set)(v:vector A 0) {\funarrow} (Vid _ _ v)).
-\it = fun (A : Set) (_ : vector A 0) {\funarrow} Vnil
-     : {\prodsym} A : Set, vector A 0 {\arrow} vector A 0
+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:Set)(v:vector A 0) {\funarrow} v).
-\it = fun (A : Set) (v : vector A 0) {\funarrow} v
-     : {\prodsym} A : Set, vector A 0 {\arrow} vector A 0
+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}:
@@ -3140,7 +3221,7 @@ Proof.
 \it
 1 subgoal
   
-  A : Set
+  A : Type
   v : vector A 0
   ============================
    v = Vid A 0 v
@@ -3150,14 +3231,14 @@ Defined.
 \end{alltt}
 
 A similar result can be proven about vectors of strictly positive
-lenght\footnote{As for \citecoq{Vid} and \citecoq{Vid\_eq}, this definition 
+length\footnote{As for \citecoq{Vid} and \citecoq{Vid\_eq}, this definition 
 is from Jean Duprat.}.
 
 \begin{alltt}
 
 
 Theorem decomp :
-  {\prodsym} (A : Set) (n : nat) (v : vector A (S n)),
+  {\prodsym} (A : Type) (n : nat) (v : vector A (S n)),
   v = Vcons (Vhead v) (Vtail v).
 Proof.
  intros.
@@ -3165,7 +3246,7 @@ Proof.
 \it
  1 subgoal
   
-  A : Set
+  A : Type
   n : nat
   v : vector A (S n)
   ============================
@@ -3183,7 +3264,7 @@ on vectors of same length:
 
 \begin{alltt}
 Definition vector_double_rect : 
-    {\prodsym} (A:Set) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
+    {\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}
@@ -3197,7 +3278,7 @@ 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{Set}
+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.
 
@@ -3221,7 +3302,7 @@ 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:Set)(n:nat)(p:nat)(v:vector A p)
+Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p)
                   \{struct v\}
                   : option A :=
   match n,v  with
@@ -3265,7 +3346,7 @@ sequences formed with elements of type $A$, also called streams.  This
 type can be introduced through the following definition:
 
 \begin{alltt}
- CoInductive Stream (A: Set) :Set   := 
+ CoInductive Stream (A: Type) :Type   := 
  | Cons : A\arrow{}Stream A\arrow{}Stream A.
 \end{alltt}
 
@@ -3273,7 +3354,7 @@ If we are interested in finite or infinite sequences, we consider the type
 of \emph{lazy lists}:
 
 \begin{alltt}
-CoInductive LList (A: Set) : Set :=
+CoInductive LList (A: Type) : Type :=
  |  LNil : LList A
  |  LCons : A {\arrow} LList A {\arrow} LList A.
 \end{alltt}
@@ -3289,10 +3370,10 @@ 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:Set)(s : Stream A) := 
+ Definition head (A:Type)(s : Stream A) := 
    match s with Cons a s' {\funarrow} a end.
 
- Definition tail (A : Set)(s : Stream A) :=
+ Definition tail (A : Type)(s : Stream A) :=
       match s with Cons a s' {\funarrow} s' end.
 \end{alltt}
 
@@ -3303,7 +3384,7 @@ methods can be defined using the \texttt{CoFixpoint} command
 definition introduces the infinite list $[a,a,a,\ldots]$:
 
 \begin{alltt}
- CoFixpoint repeat (A:Set)(a:A) : Stream A := 
+ CoFixpoint repeat (A:Type)(a:A) : Stream A := 
    Cons a (repeat a).
 \end{alltt}
 
@@ -3317,11 +3398,11 @@ constructor, and only an argument of constructors \cite{EG94a}. The
 following definitions are examples of valid methods of construction:
 
 \begin{alltt}
-CoFixpoint iterate (A: Set)(f: A {\arrow} A)(a : A) : Stream A:=
+CoFixpoint iterate (A: Type)(f: A {\arrow} A)(a : A) : Stream A:=
     Cons a (iterate f (f a)).
 
 CoFixpoint map 
-  (A B:Set)(f: A {\arrow} B)(s : Stream A) : Stream B:=
+  (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}
 
@@ -3341,13 +3422,13 @@ a case expression. We can check this using the command
 \texttt{Eval}.
 
 \begin{alltt}
-Eval simpl in (fun (A:Set)(a:A) {\funarrow} repeat a).
-\it  = fun (A : Set) (a : A) {\funarrow} repeat a
-     : {\prodsym} A : Set, A {\arrow} Stream A
+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:Set)(a:A) {\funarrow} head (repeat a)).
-\it  = fun (A : Set) (a : A) {\funarrow} a
-     : {\prodsym} A : Set, A {\arrow} A
+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}
@@ -3377,7 +3458,7 @@ 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: Set) : Stream A {\arrow} Stream A {\arrow} Prop :=
+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}
@@ -3399,7 +3480,7 @@ method for constructing an infinite proof:
 
 \begin{alltt}
 Section Parks_Principle.
-Variable A : Set.
+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.
@@ -3420,7 +3501,7 @@ End Parks_Principle.
 Let us use the principle of co-induction to prove the extensional
 equality mentioned above. 
 \begin{alltt}
-Theorem map_iterate : {\prodsym} (a:Set)(f:A{\arrow}A)(x:A),
+Theorem map_iterate : {\prodsym} (A:Type)(f:A{\arrow}A)(x:A),
                        EqSt (iterate f (f x)) 
                             (map f (iterate f x)).
 Proof.
@@ -3464,7 +3545,7 @@ In the example above, this tactic produces a much simpler proof
 that the former one:
 
 \begin{alltt}
-Theorem map_iterate' : {\prodsym} ((A:Set)f:A{\arrow}A)(x:A),
+Theorem map_iterate' : {\prodsym} ((A:Type)f:A{\arrow}A)(x:A),
                        EqSt (iterate f (f x))
                             (map f (iterate f x)).
 Proof.
@@ -3503,13 +3584,13 @@ The following lemmas are straightforward applications
  of \texttt{discriminate} and \citecoq{injection}:
 
 \begin{alltt}
-Lemma Lnil_not_Lcons : {\prodsym} (A:Set)(a:A)(l:LList A),
+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:Set)(a b : A)(l l': LList A),
+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.
@@ -3522,23 +3603,23 @@ In order to show \citecoq{inversion} at work, let us define
 two predicates on lazy lists:
 
 \begin{alltt}
-Inductive Finite (A:Set) : LList A {\arrow} Prop :=
+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:Set) : LList A {\arrow} Prop :=
+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:Set), ~ Infinite (LNil (A:=A)).
+Lemma LNil_not_Infinite : {\prodsym} (A:Type), ~ Infinite (LNil (A:=A)).
 Proof.
   intros A H;inversion H.
 Qed.
 
-Lemma Finite_not_Infinite : {\prodsym} (A:Set)(l:LList A),
+Lemma Finite_not_Infinite : {\prodsym} (A:Type)(l:LList A),
                                 Finite l {\arrow} ~ Infinite l.
 Proof.
  intros A l H; elim H.
@@ -3555,7 +3636,7 @@ 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:Set)(l:LList A),
+Lemma Not_Finite_Infinite : {\prodsym} (A:Type)(l:LList A),
                             ~ Finite l {\arrow} Infinite l.
 Proof.
  cofix H.
@@ -3570,8 +3651,8 @@ Proof.
 
 1 subgoal
   
-  H : forall (A : Set) (l : LList A), ~ Finite l -> Infinite l
-  A : Set
+  H : forall (A : Type) (l : LList A), ~ Finite l -> Infinite l
+  A : Type
   a : A
   l : LList A
   H0 : ~ Finite (LCons a l)
-- 
cgit v1.2.3

