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