diff options
Diffstat (limited to 'doc')
22 files changed, 350 insertions, 8018 deletions
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex deleted file mode 100644 index 01369b9003..0000000000 --- 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 4a17e08182..0000000000 --- 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 72d7492690..0000000000 --- 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 caee81782c..0000000000 --- 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 438f2133d4..0000000000 --- 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 0334553f27..0000000000 --- a/doc/RecTutorial/recmacros.tex +++ /dev/null @@ -1,75 +0,0 @@ -%=================================== -% Style of the document -%=================================== -%\newtheorem{example}{Example}[section] -%\newtheorem{exercise}{Exercise}[section] - - -\newcommand{\comentario}[1]{\texttt{#1}} - -%=================================== -% Keywords -%=================================== - -\newcommand{\Prop}{\texttt{Prop}} -\newcommand{\Set}{\texttt{Set}} -\newcommand{\Type}{\texttt{Type}} -\newcommand{\true}{\texttt{true}} -\newcommand{\false}{\texttt{false}} -\newcommand{\Lth}{\texttt{Lth}} - -\newcommand{\Nat}{\texttt{nat}} -\newcommand{\nat}{\texttt{nat}} -\newcommand{\Z} {\texttt{O}} -\newcommand{\SUCC}{\texttt{S}} -\newcommand{\pred}{\texttt{pred}} - -\newcommand{\False}{\texttt{False}} -\newcommand{\True}{\texttt{True}} -\newcommand{\I}{\texttt{I}} - -\newcommand{\natind}{\texttt{nat\_ind}} -\newcommand{\natrec}{\texttt{nat\_rec}} -\newcommand{\natrect}{\texttt{nat\_rect}} - -\newcommand{\eqT}{\texttt{eqT}} -\newcommand{\identityT}{\texttt{identityT}} - -\newcommand{\map}{\texttt{map}} -\newcommand{\iterates}{\texttt{iterates}} - - -%=================================== -% Numbering -%=================================== - - -\newtheorem{definition}{Definition}[section] -\newtheorem{example}{Example}[section] - - -%=================================== -% Judgements -%=================================== - - -\newcommand{\JM}[2]{\ensuremath{#1 : #2}} - -%=================================== -% Expressions -%=================================== - -\newcommand{\Case}[3][]{\ensuremath{#1\textsf{Case}~#2~\textsf of}~#3~\textsf{end}} - -%======================================= - -\newcommand{\snreglados} [3] {\begin{tabular}{c} \ensuremath{#1} \\[2pt] - \ensuremath{#2}\\ \hline \ensuremath{#3} \end{tabular}} - - -\newcommand{\snregla} [2] {\begin{tabular}{c} - \ensuremath{#1}\\ \hline \ensuremath{#2} \end{tabular}} - - -%======================================= - diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index f5237e4fbf..e10e16c107 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -599,6 +599,7 @@ Notice that the syntax is not completely backward compatible since the identifier was not required. .. cmd:: Add Morphism f : @ident + :name: Add Morphism The latter command also is restricted to the declaration of morphisms without parameters. It is not fully backward compatible since the @@ -616,7 +617,7 @@ the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can used to replace terms in contexts that were refused by the old implementation. As discussed in the next section, the semantics of the new :tacn:`setoid_rewrite` tactic differs slightly from the old one and -tacn:`rewrite`. +:tacn:`rewrite`. Extensions diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 5f8c064840..152f4f6552 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -263,9 +263,12 @@ Activating the Printing of Coercions .. cmd:: Add Printing Coercion @qualid - This command forces coercion denoted by :n:`@qualid` to be printed. To skip - the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By - default, a coercion is never printed. + This command forces coercion denoted by :n:`@qualid` to be printed. + By default, a coercion is never printed. + +.. cmd:: Remove Printing Coercion @qualid + + Use this command, to skip the printing of coercion :n:`@qualid`. .. _coercions-classes-as-records: diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 009efd0d25..80ce016200 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -26,6 +26,11 @@ solvable. This is the restriction meant by "Presburger arithmetic". If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. +.. tacv:: romega + :name: romega + + To be documented. + Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index e80cfb6bb5..6e7ccba63c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -412,7 +412,7 @@ end of a definition or proof, we check that the only remaining universes are the ones declared. In the term and in general in proof mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one -can use :ref:`Show Universes <ShowUniverses>` to display the current context of universes. +can use :cmd:`Show Universes` to display the current context of universes. Definitions can also be instantiated explicitly, giving their full instance: diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 97231c9ecf..aeb45611e6 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -1201,15 +1201,6 @@ Decomposition}}, note = {\url{https://proofgeneral.github.io/}} } -@Book{CoqArt, - title = {Interactive Theorem Proving and Program Development. - Coq'Art: The Calculus of Inductive Constructions}, - author = {Yves Bertot and Pierre Castéran}, - publisher = {Springer Verlag}, - series = {Texts in Theoretical Computer Science. An EATCS series}, - year = 2004 -} - @InCollection{wadler87, author = {P. Wadler}, title = {Efficient Compilation of Pattern Matching}, diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 4a313df0ce..75ff72c4da 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -2,12 +2,11 @@ Introduction ------------------------ -This document is the Reference Manual of the |Coq| proof -assistant. A companion volume, the |Coq| Tutorial, is provided for the -beginners. It is advised to read the Tutorial first. A -book :cite:`CoqArt` on practical uses of the |Coq| system was -published in 2004 and is a good support for both the beginner and the -advanced user. +This document is the Reference Manual of the |Coq| proof assistant. +To start using Coq, it is advised to first read a tutorial. +Links to several tutorials can be found at +https://coq.inria.fr/documentation (see also +https://github.com/coq/coq/wiki#coq-tutorials). The |Coq| system is designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8746897e75..53b993eddc 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1175,52 +1175,53 @@ component is equal ``nat`` and hence ``M1.T`` as specified. If `qualid` denotes a valid basic module (i.e. its module type is a signature), makes its components available by their short names. -.. example:: + .. example:: - .. coqtop:: reset all + .. coqtop:: reset all - Module Mod. + Module Mod. - Definition T:=nat. + Definition T:=nat. - Check T. + Check T. - End Mod. + End Mod. - Check Mod.T. + Check Mod.T. - Fail Check T. + Fail Check T. - Import Mod. + Import Mod. - Check T. + Check T. -Some features defined in modules are activated only when a module is -imported. This is for instance the case of notations (see :ref:`Notations`). + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). -Declarations made with the Local flag are never imported by theImport -command. Such declarations are only accessible through their fully -qualified name. + Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Module A. + Module A. - Module B. + Module B. - Local Definition T := nat. + Local Definition T := nat. - End B. + End B. - End A. + End A. - Import A. + Import A. - Fail Check B.T. + Fail Check B.T. .. cmdv:: Export @qualid + :name: Export When the module containing the command Export qualid is imported, qualid is imported as well. @@ -1231,16 +1232,17 @@ qualified name. .. cmd:: Print Module @ident - Prints the module type and (optionally) the body of the module `ident`. + Prints the module type and (optionally) the body of the module :n:`@ident`. .. cmd:: Print Module Type @ident - Prints the module type corresponding to `ident`. + Prints the module type corresponding to :n:`@ident`. .. opt:: Short Module Printing - This option (off by default) disables the printing of the types of fields, - leaving only their names, for the commands ``Print Module`` and ``Print Module Type``. + This option (off by default) disables the printing of the types of fields, + leaving only their names, for the commands :cmd:`Print Module` and + :cmd:`Print Module Type`. Libraries and qualified names --------------------------------- @@ -1510,9 +1512,8 @@ implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non -maximally. This can be governed argument per argument by the command ``Implicit -Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the -:opt:`Maximal Implicit Insertion` option. +maximally. This can be governed argument per argument by the command +:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option. See also :ref:`displaying-implicit-args`. @@ -1565,7 +1566,7 @@ absent in every situation but still be able to specify it if needed: The syntax is supported in all top-level definitions: -``Definition``, ``Fixpoint``, ``Lemma`` and so on. For (co-)inductive datatype +:cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype declarations, the semantics are the following: an inductive parameter declared as an implicit argument need not be repeated in the inductive definition but will become implicit for the constructors of the diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 46e684b122..39735a6eda 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -609,6 +609,7 @@ of any section is equivalent to using ``Local Parameter``. Adds blocks of variables with different specifications. .. cmdv:: Variables {+ ( {+ @ident } : @term) } + :name: Variables .. cmdv:: Hypothesis {+ ( {+ @ident } : @term) } :name: Hypothesis @@ -672,6 +673,7 @@ Section :ref:`typing-rules`. You have to explicitly give their fully qualified name to refer to them. .. cmdv:: Example @ident := @term + :name: Example .. cmdv:: Example @ident : @term := @term diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index c5ee724caf..2b128b98fe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -245,7 +245,7 @@ focused goals with: :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested - in a tactic expression, by using the keyword :tacn:`only`: + in a tactic expression, by using the keyword ``only``: .. tacv:: only selector : expr :name: only ... : ... @@ -826,6 +826,7 @@ We can make pattern matching on goals using the following expression: .. we should provide the full grammar here .. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is matched (non-linear first-order unification) by an hypothesis of the diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index df8ef74f74..069cf8a6dc 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -8,12 +8,13 @@ In |Coq|’s proof editing mode all top-level commands documented in Chapter :ref:`vernacularcommands` remain available and the user has access to specialized commands dealing with proof development pragmas documented in this -section. He can also use some other specialized commands called +section. They can also use some other specialized commands called *tactics*. They are the very tools allowing the user to deal with logical reasoning. They are documented in Chapter :ref:`tactics`. -When switching in editing proof mode, the prompt ``Coq <`` is changed into -``ident <`` where ``ident`` is the declared name of the theorem currently -edited. + +Coq user interfaces usually have a way of marking whether the user has +switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into +:n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. At each stage of a proof development, one has a list of goals to prove. Initially, the list consists only in the theorem itself. After @@ -36,8 +37,8 @@ terms are called *proof terms*. .. exn:: No focused proof. -Coq raises this error message when one attempts to use a proof editing command -out of the proof editing mode. + Coq raises this error message when one attempts to use a proof editing command + out of the proof editing mode. .. _proof-editing-mode: @@ -46,139 +47,149 @@ Switching on/off the proof editing mode The proof editing mode is entered by asserting a statement, which typically is the assertion of a theorem using an assertion command like :cmd:`Theorem`. The -list of assertion commands is given in Section :ref:`Assertions`. The command +list of assertion commands is given in :ref:`Assertions`. The command :cmd:`Goal` can also be used. .. cmd:: Goal @form -This is intended for quick assertion of statements, without knowing in -advance which name to give to the assertion, typically for quick -testing of the provability of a statement. If the proof of the -statement is eventually completed and validated, the statement is then -bound to the name ``Unnamed_thm`` (or a variant of this name not already -used for another statement). + This is intended for quick assertion of statements, without knowing in + advance which name to give to the assertion, typically for quick + testing of the provability of a statement. If the proof of the + statement is eventually completed and validated, the statement is then + bound to the name ``Unnamed_thm`` (or a variant of this name not already + used for another statement). .. cmd:: Qed :name: Qed (interactive proof) -This command is available in interactive editing proof mode when the -proof is completed. Then ``Qed`` extracts a proof term from the proof -script, switches back to Coq top-level and attaches the extracted -proof term to the declared name of the original goal. This name is -added to the environment as an opaque constant. - + This command is available in interactive editing proof mode when the + proof is completed. Then :cmd:`Qed` extracts a proof term from the proof + script, switches back to Coq top-level and attaches the extracted + proof term to the declared name of the original goal. This name is + added to the environment as an opaque constant. -.. exn:: Attempt to save an incomplete proof. + .. exn:: Attempt to save an incomplete proof. -.. note:: + .. note:: - Sometimes an error occurs when building the proof term, because - tactics do not enforce completely the term construction - constraints. + Sometimes an error occurs when building the proof term, because + tactics do not enforce completely the term construction + constraints. -The user should also be aware of the fact that since the -proof term is completely rechecked at this point, one may have to wait -a while when the proof is large. In some exceptional cases one may -even incur a memory overflow. + The user should also be aware of the fact that since the + proof term is completely rechecked at this point, one may have to wait + a while when the proof is large. In some exceptional cases one may + even incur a memory overflow. -.. cmdv:: Defined - :name: Defined (interactive proof) + .. cmdv:: Defined + :name: Defined (interactive proof) -Defines the proved term as a transparent constant. + Defines the proved term as a transparent constant. -.. cmdv:: Save @ident + .. cmdv:: Save @ident + :name: Save -Forces the name of the original goal to be :n:`@ident`. This -command (and the following ones) can only be used if the original goal -has been opened using the ``Goal`` command. + Forces the name of the original goal to be :token:`ident`. This + command (and the following ones) can only be used if the original goal + has been opened using the :cmd:`Goal` command. .. cmd:: Admitted :name: Admitted (interactive proof) -This command is available in interactive editing mode to give up -the current proof and declare the initial goal as an axiom. - -.. cmd:: Proof @term - :name: Proof `term` - -This command applies in proof editing mode. It is equivalent to - -.. coqtop:: in + This command is available in interactive editing mode to give up + the current proof and declare the initial goal as an axiom. - exact @term. Qed. +.. cmd:: Abort -That is, you have to give the full proof in one gulp, as a -proof term (see Section :ref:`applyingtheorems`). + This command cancels the current proof development, switching back to + the previous proof development, or to the |Coq| toplevel if no other + proof was edited. -.. cmdv:: Proof - :name: Proof (interactive proof) + .. exn:: No focused proof (No proof-editing in progress). -Is a noop which is useful to delimit the sequence of tactic commands -which start a proof, after a ``Theorem`` command. It is a good practice to -use ``Proof``. as an opening parenthesis, closed in the script with a -closing ``Qed``. + .. cmdv:: Abort @ident + Aborts the editing of the proof named :token:`ident` (in case you have + nested proofs). -See also: ``Proof with tactic.`` in Section -:ref:`tactics-implicit-automation`. + .. cmdv:: Abort All + Aborts all current goals. -.. cmd:: Proof using @ident1 ... @identn +.. cmd:: Proof @term + :name: Proof `term` -This command applies in proof editing mode. It declares the set of -section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the -system will assert that the set of section variables actually used in -the proof is a subset of the declared one. + This command applies in proof editing mode. It is equivalent to + :n:`exact @term. Qed.` + That is, you have to give the full proof in one gulp, as a + proof term (see Section :ref:`applyingtheorems`). -The set of declared variables is closed under type dependency. For -example if ``T`` is variable and a is a variable of type ``T``, the commands -``Proof using a`` and ``Proof using T a``` are actually equivalent. +.. cmd:: Proof + :name: Proof (interactive proof) + Is a no-op which is useful to delimit the sequence of tactic commands + which start a proof, after a :cmd:`Theorem` command. It is a good practice to + use :cmd:`Proof` as an opening parenthesis, closed in the script with a + closing :cmd:`Qed`. -.. cmdv:: Proof using @ident1 ... @identn with @tactic + .. seealso:: :cmd:`Proof with` -in Section :ref:`tactics-implicit-automation`. +.. cmd:: Proof using {+ @ident } -.. cmdv:: Proof using All + This command applies in proof editing mode. It declares the set of + section variables (see :ref:`gallina-assumptions`) used by the proof. + At :cmd:`Qed` time, the + system will assert that the set of section variables actually used in + the proof is a subset of the declared one. -Use all section variables. + The set of declared variables is closed under type dependency. For + example if ``T`` is variable and a is a variable of type ``T``, the commands + ``Proof using a`` and ``Proof using T a`` are actually equivalent. + .. cmdv:: Proof using {+ @ident } with @tactic -.. cmdv:: Proof using Type + Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`. -.. cmdv:: Proof using + .. seealso:: :ref:`tactics-implicit-automation` -Use only section variables occurring in the statement. + .. cmdv:: Proof using All + Use all section variables. -.. cmdv:: Proof using Type* + .. cmdv:: Proof using {? Type } -The ``*`` operator computes the forward transitive closure. E.g. if the -variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type -of ``H``. ``Type*`` is the forward transitive closure of the entire set of -section variables occurring in the statement. + Use only section variables occurring in the statement. + .. cmdv:: Proof using Type* -.. cmdv:: Proof using -(@ident1 ... @identn) + The ``*`` operator computes the forward transitive closure. E.g. if the + variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type + of ``H``. ``Type*`` is the forward transitive closure of the entire set of + section variables occurring in the statement. -Use all section variables except :n:`@ident1` ... :n:`@identn`. + .. cmdv:: Proof using -({+ @ident }) + Use all section variables except the list of :token:`ident`. -.. cmdv:: Proof using @collection1 + @collection2 + .. cmdv:: Proof using @collection1 + @collection2 + Use section variables from the union of both collections. + See :ref:`nameaset` to know how to form a named collection. -.. cmdv:: Proof using @collection1 - @collection2 + .. cmdv:: Proof using @collection1 - @collection2 + Use section variables which are in the first collection but not in the + second one. -.. cmdv:: Proof using @collection - ( @ident1 ... @identn ) + .. cmdv:: Proof using @collection - ({+ @ident }) + Use section variables which are in the first collection but not in the + list of :token:`ident`. -.. cmdv:: Proof using @collection * + .. cmdv:: Proof using @collection * -Use section variables being, respectively, in the set union, set -difference, set complement, set forward transitive closure. See -Section :ref:`nameaset` to know how to form a named collection. The ``*`` operator -binds stronger than ``+`` and ``-``. + Use section variables in the forward transitive closure of the collection. + The ``*`` operator binds stronger than ``+`` and ``-``. Proof using options @@ -189,14 +200,14 @@ The following options modify the behavior of ``Proof using``. .. opt:: Default Proof Using "@expression" - Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default - Proof Using "a b"``. will complete all ``Proof`` commands not followed by a - using part with using ``a`` ``b``. + Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default + Proof Using "a b"`` will complete all ``Proof`` commands not followed by a + ``using`` part with ``using a b``. .. opt:: Suggest Proof Using - When ``Qed`` is performed, suggest a using annotation if the user did not + When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not provide one. .. _`nameaset`: @@ -204,80 +215,50 @@ The following options modify the behavior of ``Proof using``. Name a set of section hypotheses for ``Proof using`` ```````````````````````````````````````````````````` -.. cmd:: Collection @ident := @section_subset_expr - -The command ``Collection`` can be used to name a set of section -hypotheses, with the purpose of making ``Proof using`` annotations more -compact. - +.. cmd:: Collection @ident := @expression -.. cmdv:: Collection Some := x y z + This can be used to name a set of section + hypotheses, with the purpose of making ``Proof using`` annotations more + compact. -Define the collection named "Some" containing ``x``, ``y`` and ``z``. + .. example:: + Define the collection named ``Some`` containing ``x``, ``y`` and ``z``:: -.. cmdv:: Collection Fewer := Some - z + Collection Some := x y z. -Define the collection named "Fewer" containing only ``x`` and ``y``. + Define the collection named ``Fewer`` containing only ``x`` and ``y``:: + Collection Fewer := Some - z -.. cmdv:: Collection Many := Fewer + Some -.. cmdv:: Collection Many := Fewer - Some + Define the collection named ``Many`` containing the set union or set + difference of ``Fewer`` and ``Some``:: -Define the collection named "Many" containing the set union or set -difference of "Fewer" and "Some". + Collection Many := Fewer + Some + Collection Many := Fewer - Some + Define the collection named ``Many`` containing the set difference of + ``Fewer`` and the unnamed collection ``x y``:: -.. cmdv:: Collection Many := Fewer - (x y) - -Define the collection named "Many" containing the set difference of -"Fewer" and the unnamed collection ``x`` ``y`` - - -.. cmd:: Abort - -This command cancels the current proof development, switching back to -the previous proof development, or to the |Coq| toplevel if no other -proof was edited. - - -.. exn:: No focused proof (No proof-editing in progress). - - - -.. cmdv:: Abort @ident - -Aborts the editing of the proof named :n:`@ident`. - -.. cmdv:: Abort All - -Aborts all current goals, switching back to the |Coq| -toplevel. + Collection Many := Fewer - (x y) .. cmd:: Existential @num := @term -This command instantiates an existential variable. :n:`@num` is an index in -the list of uninstantiated existential variables displayed by ``Show -Existentials`` (described in Section :ref:`requestinginformation`). - -This command is intended to be used to instantiate existential -variables when the proof is completed but some uninstantiated -existential variables remain. To instantiate existential variables -during proof edition, you should use the tactic :tacn:`instantiate`. - - -See also: ``instantiate (num:= term).`` in Section -:ref:`controllingtheproofflow`. -See also: ``Grab Existential Variables.`` below. + This command instantiates an existential variable. :token:`num` is an index in + the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`. + This command is intended to be used to instantiate existential + variables when the proof is completed but some uninstantiated + existential variables remain. To instantiate existential variables + during proof edition, you should use the tactic :tacn:`instantiate`. .. cmd:: Grab Existential Variables -This command can be run when a proof has no more goal to be solved but -has remaining uninstantiated existential variables. It takes every -uninstantiated existential variable and turns it into a goal. + This command can be run when a proof has no more goal to be solved but + has remaining uninstantiated existential variables. It takes every + uninstantiated existential variable and turns it into a goal. Navigation in the proof tree @@ -290,7 +271,7 @@ Navigation in the proof tree .. cmdv:: Undo @num - Repeats Undo :n:`@num` times. + Repeats Undo :token:`num` times. .. cmdv:: Restart :name: Restart @@ -306,19 +287,22 @@ Navigation in the proof tree is solved or unfocused. This is useful when there are many current subgoals which clutter your screen. + .. deprecated:: 8.8 + + Prefer the use of bullets or focusing brackets (see below). + .. cmdv:: Focus @num - This focuses the attention on the :n:`@num` th subgoal to prove. + This focuses the attention on the :token:`num` th subgoal to prove. .. deprecated:: 8.8 - Prefer the use of bullets or - focusing brackets instead, including :n:`@num : %{` + Prefer the use of focusing brackets with a goal selector (see below). .. cmd:: Unfocus This command restores to focus the goal that were suspended by the - last ``Focus`` command. + last :cmd:`Focus` command. .. deprecated:: 8.8 @@ -332,7 +316,7 @@ Navigation in the proof tree .. cmd:: %{ %| %} The command ``{`` (without a terminating period) focuses on the first - goal, much like ``Focus.`` does, however, the subproof can only be + goal, much like :cmd:`Focus` does, however, the subproof can only be unfocused when it has been fully solved ( *i.e.* when there is no focused goal left). Unfocusing is then handled by ``}`` (again, without a terminating period). See also example in next section. @@ -341,9 +325,9 @@ Navigation in the proof tree together with a suggestion about the right bullet or ``}`` to unfocus it or focus the next one. -.. cmdv:: @num: %{ + .. cmdv:: @num: %{ - This focuses on the :n:`@num` th subgoal to prove. + This focuses on the :token:`num` th subgoal to prove. Error messages: @@ -409,19 +393,19 @@ The following example script illustrates all these features: .. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished. -Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same. + Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same. .. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here. -You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here. + You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here. .. exn:: No such goal. Focus next goal with bullet @bullet. -You tried to applied a tactic but no goal where under focus. Using :n:`@bullet` is mandatory here. + You tried to apply a tactic but no goal where under focus. Using :n:`@bullet` is mandatory here. .. exn:: No such goal. Try unfocusing with %{. -You just finished a goal focused by ``{``, you must unfocus it with ``}``. + You just finished a goal focused by ``{``, you must unfocus it with ``}``. Set Bullet Behavior ``````````````````` @@ -440,110 +424,116 @@ Requesting information .. cmd:: Show -This command displays the current goals. + This command displays the current goals. + .. exn:: No focused proof. -.. cmdv:: Show @num + .. cmdv:: Show @num -Displays only the :n:`@num`-th subgoal. + Displays only the :token:`num` th subgoal. -.. exn:: No such goal. -.. exn:: No focused proof. + .. exn:: No such goal. -.. cmdv:: Show @ident -Displays the named goal :n:`@ident`. This is useful in -particular to display a shelved goal but only works if the -corresponding existential variable has been named by the user -(see :ref:`existential-variables`) as in the following example. + .. cmdv:: Show @ident -.. example:: + Displays the named goal :token:`ident`. This is useful in + particular to display a shelved goal but only works if the + corresponding existential variable has been named by the user + (see :ref:`existential-variables`) as in the following example. - .. coqtop:: all + .. example:: - Goal exists n, n = 0. - eexists ?[n]. - Show n. + .. coqtop:: all -.. cmdv:: Show Script + Goal exists n, n = 0. + eexists ?[n]. + Show n. -Displays the whole list of tactics applied from the -beginning of the current proof. This tactics script may contain some -holes (subgoals not yet proved). They are printed under the form + .. cmdv:: Show Script + :name: Show Script -``<Your Tactic Text here>``. + Displays the whole list of tactics applied from the + beginning of the current proof. This tactics script may contain some + holes (subgoals not yet proved). They are printed under the form -.. cmdv:: Show Proof + ``<Your Tactic Text here>``. -It displays the proof term generated by the tactics -that have been applied. If the proof is not completed, this term -contain holes, which correspond to the sub-terms which are still to be -constructed. These holes appear as a question mark indexed by an -integer, and applied to the list of variables in the context, since it -may depend on them. The types obtained by abstracting away the context -from the type of each hole-placer are also printed. + .. cmdv:: Show Proof + :name: Show Proof -.. cmdv:: Show Conjectures + It displays the proof term generated by the tactics + that have been applied. If the proof is not completed, this term + contain holes, which correspond to the sub-terms which are still to be + constructed. These holes appear as a question mark indexed by an + integer, and applied to the list of variables in the context, since it + may depend on them. The types obtained by abstracting away the context + from the type of each hole-placer are also printed. -It prints the list of the names of all the -theorems that are currently being proved. As it is possible to start -proving a previous lemma during the proof of a theorem, this list may -contain several names. + .. cmdv:: Show Conjectures + :name: Show Conjectures -.. cmdv:: Show Intro + It prints the list of the names of all the + theorems that are currently being proved. As it is possible to start + proving a previous lemma during the proof of a theorem, this list may + contain several names. -If the current goal begins by at least one product, -this command prints the name of the first product, as it would be -generated by an anonymous ``intro``. The aim of this command is to ease -the writing of more robust scripts. For example, with an appropriate -Proof General macro, it is possible to transform any anonymous ``intro`` -into a qualified one such as ``intro y13``. In the case of a non-product -goal, it prints nothing. + .. cmdv:: Show Intro + :name: Show Intro -.. cmdv:: Show Intros + If the current goal begins by at least one product, + this command prints the name of the first product, as it would be + generated by an anonymous :tacn:`intro`. The aim of this command is to ease + the writing of more robust scripts. For example, with an appropriate + Proof General macro, it is possible to transform any anonymous :tacn:`intro` + into a qualified one such as ``intro y13``. In the case of a non-product + goal, it prints nothing. -This command is similar to the previous one, it -simulates the naming process of an intros. + .. cmdv:: Show Intros + :name: Show Intros -.. cmdv:: Show Existentials + This command is similar to the previous one, it + simulates the naming process of an :tacn:`intros`. -It displays the set of all uninstantiated -existential variables in the current proof tree, along with the type -and the context of each variable. + .. cmdv:: Show Existentials + :name: Show Existentials -.. cmdv:: Show Match @ident + It displays the set of all uninstantiated + existential variables in the current proof tree, along with the type + and the context of each variable. -This variant displays a template of the Gallina -``match`` construct with a branch for each constructor of the type -:n:`@ident` + .. cmdv:: Show Match @ident -.. example:: - .. coqtop:: all + This variant displays a template of the Gallina + ``match`` construct with a branch for each constructor of the type + :token:`ident` - Show Match nat. + .. example:: + .. coqtop:: all -.. exn:: Unknown inductive type. + Show Match nat. -.. _ShowUniverses: + .. exn:: Unknown inductive type. -.. cmdv:: Show Universes + .. cmdv:: Show Universes + :name: Show Universes -It displays the set of all universe constraints and -its normalized form at the current stage of the proof, useful for -debugging universe inconsistencies. + It displays the set of all universe constraints and + its normalized form at the current stage of the proof, useful for + debugging universe inconsistencies. .. cmd:: Guarded -Some tactics (e.g. :tacn:`refine`) allow to build proofs using -fixpoint or co-fixpoint constructions. Due to the incremental nature -of interactive proof construction, the check of the termination (or -guardedness) of the recursive calls in the fixpoint or cofixpoint -constructions is postponed to the time of the completion of the proof. + Some tactics (e.g. :tacn:`refine`) allow to build proofs using + fixpoint or co-fixpoint constructions. Due to the incremental nature + of interactive proof construction, the check of the termination (or + guardedness) of the recursive calls in the fixpoint or cofixpoint + constructions is postponed to the time of the completion of the proof. -The command :cmd:`Guarded` allows checking if the guard condition for -fixpoint and cofixpoint is violated at some time of the construction -of the proof without having to wait the completion of the proof. + The command :cmd:`Guarded` allows checking if the guard condition for + fixpoint and cofixpoint is violated at some time of the construction + of the proof without having to wait the completion of the proof. Controlling the effect of proof editing commands diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index b3537bad80..0318bddde4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -96,10 +96,10 @@ bindings_list`` where ``bindings_list`` may be of two different forms: + A bindings list can also be a simple list of terms :n:`{* term}`. In that case the references to which these terms correspond are - determined by the tactic. In case of ``induction``, ``destruct``, ``elim`` - and ``case`` (see :ref:`ltac`) the terms have to + determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` + and :tacn:`case`, the terms have to provide instances for all the dependent products in the type of term while in - the case of ``apply``, or of ``constructor`` and its variants, only instances + the case of :tacn:`apply`, or of :tacn:`constructor` and its variants, only instances for the dependent products that are not bound in the conclusion of the type are required. @@ -503,7 +503,7 @@ Applying theorems .. tacv:: eapply {+, @term with @bindings_list} in @ident as @intro_pattern. - This works as :tacn:`apply ... in as` but using ``eapply``. + This works as :tacn:`apply ... in ... as` but using ``eapply``. .. tacv:: simple apply @term in @ident @@ -511,15 +511,15 @@ Applying theorems on subterms that contain no variables to instantiate. For instance, if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and :g:`H0 : O = O` then ``simple apply H in H0`` does not succeed because it - would require the conversion of :g:`id ?1234` and :g:`O` where :g:`?1234` is - a variable to instantiate. Tactic :n:`simple apply @term in @ident` does not + would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is + an existential variable to instantiate. Tactic :n:`simple apply @term in @ident` does not either traverse tuples as :n:`apply @term in @ident` does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} - This summarizes the different syntactic variants of :n:`apply @term in - @ident` and :n:`eapply @term in @ident`. + This summarizes the different syntactic variants of :n:`apply @term in @ident` + and :n:`eapply @term in @ident`. .. tacn:: constructor @num :name: constructor @@ -626,22 +626,21 @@ binder. If the goal is a product, the tactic implements the "Lam" rule given in :ref:`Typing-rules` [1]_. If the goal starts with a let binder, then the tactic implements a mix of the "Let" and "Conv". -If the current goal is a dependent product :math:`\forall` :g:`x:T, U` (resp +If the current goal is a dependent product :g:`forall x:T, U` (resp :g:`let x:=t in U`) then ``intro`` puts :g:`x:T` (resp :g:`x:=t`) in the local context. The new subgoal is :g:`U`. If the goal is a non-dependent product :g:`T`:math:`\rightarrow`:g:`U`, then it puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or -:g:`Prop`) or Xn:T (if the type of :g:`T` is :g:`Type`). The optional index +:g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. If the goal is an existential variable, ``intro`` forces the resolution of the -existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +existential variable into a dependent product :math:`forall`:g:`x:?X, ?Y`, puts :g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to depend on :g:`x`. -If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. @@ -649,6 +648,7 @@ be applied or the goal is not head-reducible. .. exn:: @ident is already used. .. tacv:: intros + :name: intros This repeats ``intro`` until it meets the head-constant. It never reduces head-constants and it never fails. @@ -715,7 +715,7 @@ be applied or the goal is not head-reducible. These tactics behave as previously but naming the introduced hypothesis :n:`@ident`. It is equivalent to :n:`intro @ident` followed by the - appropriate call to move (see :tacn:`move ... after`). + appropriate call to ``move`` (see :tacn:`move ... after ...`). .. tacn:: intros @intro_pattern_list :name: intros ... @@ -760,7 +760,7 @@ be applied or the goal is not head-reducible. Assuming a goal of type :g:`Q → P` (non-dependent product), or of type - :math:`\forall`:g:`x:T, P` (dependent product), the behavior of + :g:`forall x:T, P` (dependent product), the behavior of :n:`intros p` is defined inductively over the structure of the introduction pattern :n:`p`: @@ -918,7 +918,7 @@ the inverse of :tacn:`intro`. depend on it. .. tacn:: move @ident after @ident - :name: move .. after ... + :name: move ... after ... This moves the hypothesis named :n:`@ident` in the local context after the hypothesis named :n:`@ident`, where “after” is in reference to the @@ -2149,13 +2149,13 @@ See also: :ref:`advanced-recursive-functions` :n:`dependent inversion_clear @ident`. .. tacv:: dependent inversion @ident with @term - :name: dependent inversion ... + :name: dependent inversion ... with ... This variant allows you to specify the generalization of the goal. It is useful when the system fails to generalize the goal automatically. If - :n:`@ident` has type :g:`(I t)` and :g:`I` has type :math:`\forall` - :g:`(x:T), s`, then :n:`@term` must be of type :g:`I:`:math:`\forall` - :g:`(x:T), I x -> s'` where :g:`s'` is the type of the goal. + :n:`@ident` has type :g:`(I t)` and :g:`I` has type :g:`forall (x:T), s`, + then :n:`@term` must be of type :g:`I:forall (x:T), I x -> s'` where + :g:`s'` is the type of the goal. .. tacv:: dependent inversion @ident as @intro_pattern with @term @@ -2164,7 +2164,7 @@ See also: :ref:`advanced-recursive-functions` .. tacv:: dependent inversion_clear @ident with @term - Like :tacn:`dependent inversion ...` with but clears :n:`@ident` from the + Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the local context. .. tacv:: dependent inversion_clear @ident as @intro_pattern with @term @@ -3194,7 +3194,7 @@ can solve such a goal: Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. -Note that :tacn:`ex_intro` should be declared as a hint. +Note that ``ex_intro`` should be declared as a hint. .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} @@ -3445,6 +3445,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Declares each :n:`@ident` as a transparent or opaque constant. .. cmdv:: Hint Extern @num {? @pattern} => tactic + :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a @@ -3665,6 +3666,7 @@ option which accepts three flags allowing for a fine-grained handling of non-imported hints. .. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) + :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. :cmd:`Import`: @@ -3809,14 +3811,15 @@ some incompatibilities. .. tacv:: intuition - Is equivalent to :g:`intuition auto with *`. + Is equivalent to :g:`intuition auto with *`. .. tacv:: dintuition + :name: dintuition - While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connective ``and, prod, or, sum, False, - Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive - types with one constructors and no indices, i.e. record-style connectives. + While :tacn:`intuition` recognizes inductively defined connectives + isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive + types with one constructors and no indices, i.e. record-style connectives. .. opt:: Intuition Negation Unfolding @@ -3845,11 +3848,14 @@ first- order reasoning, written by Pierre Corbineau. It is not restricted to usual logical connectives but instead may reason about any first-order class inductive definition. -.. opt:: Firstorder Solver +.. opt:: Firstorder Solver @tactic The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with *`, it can be reset locally or globally using this option and - printed using :cmd:`Print Firstorder Solver`. + :g:`auto with *`, it can be reset locally or globally using this option. + + .. cmd:: Print Firstorder Solver + + Prints the default tactic used by :tacn:`firstorder` when no rule applies. .. tacv:: firstorder @tactic @@ -4012,8 +4018,8 @@ solved by :tacn:`f_equal`. :name: reflexivity This tactic applies to a goal that has the form :g:`t=u`. It checks that `t` -and `u` are convertible and then solves the goal. It is equivalent to apply -:tacn:`refl_equal`. +and `u` are convertible and then solves the goal. It is equivalent to +``apply refl_equal``. .. exn:: The conclusion is not a substitutive equation. @@ -4105,7 +4111,7 @@ symbol :g:`=`. :n:`intro @ident; simplify_eq @ident`. .. tacn:: dependent rewrite -> @ident - :name: dependent rewrite + :name: dependent rewrite -> This tactic applies to any goal. If :n:`@ident` has type :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each @@ -4116,6 +4122,7 @@ symbol :g:`=`. :tacn:`injection` and :tacn:`inversion` tactics. .. tacv:: dependent rewrite <- @ident + :name: dependent rewrite <- Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to left. @@ -4375,19 +4382,20 @@ This tactics reverses the list of the focused goals. unification, or they can be called back into focus with the command :cmd:`Unshelve`. -.. tacv:: shelve_unifiable + .. tacv:: shelve_unifiable + :name: shelve_unifiable - Shelves only the goals under focus that are mentioned in other goals. - Goals that appear in the type of other goals can be solved by unification. + Shelves only the goals under focus that are mentioned in other goals. + Goals that appear in the type of other goals can be solved by unification. -.. example:: + .. example:: - .. coqtop:: all reset + .. coqtop:: all reset - Goal exists n, n=0. - refine (ex_intro _ _ _). - all:shelve_unifiable. - reflexivity. + Goal exists n, n=0. + refine (ex_intro _ _ _). + all: shelve_unifiable. + reflexivity. .. cmd:: Unshelve diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7ba103b222..c37233734b 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -360,6 +360,7 @@ Requests to the environment Search (?x * _ + ?x * _)%Z outside OmegaLemmas. .. cmdv:: SearchAbout + :name: SearchAbout .. deprecated:: 8.5 @@ -416,7 +417,7 @@ Requests to the environment current goal (if any) and theorems of the current context whose statement’s conclusion or last hypothesis and conclusion matches the expressionterm where holes in the latter are denoted by `_`. - It is a variant of Search @term_pattern that does not look for subterms + It is a variant of :n:`Search @term_pattern` that does not look for subterms but searches for statements whose conclusion has exactly the expected form, or whose statement finishes by the given series of hypothesis/conclusion. @@ -625,6 +626,7 @@ file is a particular case of module called *library file*. .. cmdv:: Require Import @qualid + :name: Require Import This loads and declares the module :n:`@qualid` and its dependencies then imports the contents of :n:`@qualid` as described @@ -637,10 +639,11 @@ file is a particular case of module called *library file*. :cmd:`Import` :n:`@qualid` would. .. cmdv:: Require Export @qualid + :name: Require Export - This command acts as ``Require Import`` :n:`@qualid`, - but if a further module, say `A`, contains a command ``Require Export`` `B`, - then the command ``Require Import`` `A` also imports the module `B.` + This command acts as :cmd:`Require Import` :n:`@qualid`, + but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, + then the command :cmd:`Require Import` `A` also imports the module `B.` .. cmdv:: Require [Import | Export] {+ @qualid } @@ -653,7 +656,7 @@ file is a particular case of module called *library file*. .. cmdv:: From @dirpath Require @qualid - This command acts as ``Require``, but picks + This command acts as :cmd:`Require`, but picks any library whose absolute name is of the form dirpath.dirpath’.qualid for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library comes from a given package by making explicit its absolute root. @@ -895,6 +898,7 @@ interactively, they cannot be part of a vernacular file loaded via necessary. .. cmdv:: Backtrack @num @num @num + :name: Backtrack .. deprecated:: 8.4 @@ -1022,12 +1026,14 @@ Controlling display output, printing only identifiers. .. opt:: Printing Width @num + :name: Printing Width This command sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78. .. opt:: Printing Depth @num + :name: Printing Depth This option controls the nesting depth of the formatter used for pretty- printing. Beyond this depth, display of subterms is replaced by dots. At the @@ -1208,28 +1214,29 @@ scope of their effect. There are four kinds of commands: + Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the - current section or module it occurs in. As an example, the ``Coercion`` - (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-strategy>`) - commands belong to this category. + current section or module it occurs in. As an example, the :cmd:`Coercion` + and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end of the section they occur in but to extent their effect outside the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Implicit Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support extension of their scope outside sections at all and the Global is not applicable to them. + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the Global + of the section or module they occur in. For these commands, the ``Global`` modifier extends their effect outside the sections and modules they - occurs in. The ``Transparent`` and ``Opaque`` (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands belong to this category. + occurs in. The :cmd:`Transparent` and :cmd:`Opaque` + (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + belong to this category. + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in when no section contains them.For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command - occurs in a section. The ``Set`` and ``Unset`` commands belong to this + occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index e12e4d897a..682553c31b 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -26,6 +26,7 @@ induction for objects in type `identᵢ`. natural in case of inductively defined relations. .. cmdv:: Scheme Equality for @ident + :name: Scheme Equality Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident` involves some other inductive types, their equality has to be defined first. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6958b5f265..3b95a37ed3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -916,9 +916,8 @@ Binding arguments of a constant to an interpretation scope .. seealso:: - :cmd:`About @qualid` - The command to show the scopes bound to the arguments of a - function is described in Section 2. + The command :cmd:`About` can be used to show the scopes bound to the + arguments of a function. .. note:: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index f09ed4b55c..21093bd904 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -732,14 +732,14 @@ class CoqDomain(Domain): roles = { # Each of these roles lives in a different semantic “subdomain” - 'cmd': XRefRole(), - 'tac': XRefRole(), - 'tacn': XRefRole(), - 'opt': XRefRole(), - 'thm': XRefRole(), - 'prodn' : XRefRole(), - 'exn': XRefRole(), - 'warn': XRefRole(), + 'cmd': XRefRole(warn_dangling=True), + 'tac': XRefRole(warn_dangling=True), + 'tacn': XRefRole(warn_dangling=True), + 'opt': XRefRole(warn_dangling=True), + 'thm': XRefRole(warn_dangling=True), + 'prodn' : XRefRole(warn_dangling=True), + 'exn': XRefRole(warn_dangling=True), + 'warn': XRefRole(warn_dangling=True), # This one is special 'index': IndexXRefRole(), # These are used for highlighting diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex deleted file mode 100644 index 77ce8574f2..0000000000 --- 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} - |