diff options
Diffstat (limited to 'doc/RecTutorial/RecTutorial.tex')
| -rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 301 |
1 files changed, 191 insertions, 110 deletions
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex index 9ee913d4..df8bc9f1 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 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 @@ -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 @@ -2769,10 +2848,12 @@ For Acc_intro: Arguments A, R are implicit \dots \end{alltt} -\noindent This inductive predicate characterize those elements $x$ of +\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 @@ -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 @@ -3044,7 +3125,7 @@ heterogeneous equality to a standard one. \begin{alltt} Lemma vector0_is_vnil_aux : - {\prodsym} (A:Set)(n:nat)(v:vector A n), + {\prodsym} (A:Type)(n:nat)(v:vector A n), n= 0 {\arrow} JMeq v (Vnil A). Proof. destruct v. @@ -3056,7 +3137,7 @@ Qed. Our property of vectors of null length can be easily proven: \begin{alltt} -Lemma vector0_is_vnil : {\prodsym} (A:Set)(v:vector A 0), v = Vnil A. +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. @@ -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) |