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