1
\documentclass[11pt]{article}
2
\title{A Tutorial on [Co-]Inductive Types in Coq}
3
\author{Eduardo Gim\'enez\thanks{Eduardo.Gimenez@inria.fr},
4
Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}}
5
\date{May 1998 --- \today}
9
%\externaldocument{RefMan-gal.v}
10
%\externaldocument{RefMan-ext.v}
11
%\externaldocument{RefMan-tac.v}
12
%\externaldocument{RefMan-oth}
13
%\externaldocument{RefMan-tus.v}
14
%\externaldocument{RefMan-syn.v}
15
%\externaldocument{Extraction.v}
18
\newcommand{\refmancite}[1]{{}}
19
%\newcommand{\refmancite}[1]{\cite{coqrefman}}
20
%\newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}}
22
\usepackage[latin1]{inputenc}
23
\usepackage[T1]{fontenc}
31
\usepackage[dvips]{epsfig}
42
\renewcommand{\familydefault}{ptm}
43
\renewcommand{\seriesdefault}{m}
44
\renewcommand{\shapedefault}{n}
45
\newtheorem{exercise}{Exercise}[section]
51
This document\footnote{The first versions of this document were entirely written by Eduardo Gimenez.
52
Pierre Cast\'eran wrote the 2004 and 2006 revisions.} is an introduction to the definition and
53
use of inductive and co-inductive types in the {\coq} proof environment. It explains how types like natural numbers and infinite streams are defined
54
in {\coq}, and the kind of proof techniques that can be used to reason
55
about them (case analysis, induction, inversion of predicates,
56
co-induction, etc). Each technique is illustrated through an
57
executable and self-contained {\coq} script.
59
%\RRkeyword{Proof environments, recursive types.}
62
\addtocontents{toc}{\protect \thispagestyle{empty}}
63
\pagenumbering{arabic}
69
\section{About this document}
71
This document is an introduction to the definition and use of
72
inductive and co-inductive types in the {\coq} proof environment. It was born from the
73
notes written for the course about the version V5.10 of {\coq}, given
75
the Ecole Normale Sup\'erieure de Lyon in March 1996. This article is
76
a revised and improved version of these notes for the version V8.0 of
80
We assume that the reader has some familiarity with the
81
proofs-as-programs paradigm of Logic \cite{Coquand:metamathematical} and the generalities
82
of the {\coq} system \cite{coqrefman}. You would take a greater advantage of
83
this document if you first read the general tutorial about {\coq} and
84
{\coq}'s FAQ, both available on \cite{coqsite}.
85
A text book \cite{coqart}, accompanied with a lot of
86
examples and exercises \cite{Booksite}, presents a detailed description
87
of the {\coq} system and its underlying
88
formalism: the Calculus of Inductive Construction.
89
Finally, the complete description of {\coq} is given in the reference manual
90
\cite{coqrefman}. Most of the tactics and commands we describe have
91
several options, which we do not present exhaustively.
92
If some script herein uses a non described feature, please refer to
96
If you are familiar with other proof environments
97
based on type theory and the LCF style ---like PVS, LEGO, Isabelle,
98
etc--- then you will find not difficulty to guess the unexplained
101
The better way to read this document is to start up the {\coq} system,
102
type by yourself the examples and exercises, and observe the
103
behavior of the system. All the examples proposed in this tutorial
104
can be downloaded from the same site as the present document.
107
The tutorial is organised as follows. The next section describes how
108
inductive types are defined in {\coq}, and introduces some useful ones,
109
like natural numbers, the empty type, the propositional equality type,
110
and the logical connectives. Section \ref{CaseAnalysis} explains
111
definitions by pattern-matching and their connection with the
112
principle of case analysis. This principle is the most basic
113
elimination rule associated with inductive or co-inductive types
115
general scheme that we illustrate for some of the types introduced in
116
Section \ref{Introduction}. Section \ref{CaseTechniques} illustrates
117
the pragmatics of this principle, showing different proof techniques
118
based on it. Section \ref{StructuralInduction} introduces definitions
119
by structural recursion and proofs by induction.
120
Section~\ref{CaseStudy} presents some elaborate techniques
121
about dependent case analysis. Finally, Section
122
\ref{CoInduction} is a brief introduction to co-inductive types
123
--i.e., types containing infinite objects-- and the principle of
127
Thanks to Bruno Barras, Yves Bertot, Hugo Herbelin, Jean-Fran\c{c}ois Monin
128
and Michel L\'evy for their help.
130
\subsection*{Lexical conventions}
131
The \texttt{typewriter} font is used to represent text
132
input by the user, while the \textit{italic} font is used to represent
133
the text output by the system as answers.
136
Moreover, the mathematical symbols \coqle{}, \coqdiff, \(\exists\),
137
\(\forall\), \arrow{}, $\rightarrow{}$ \coqor{}, \coqand{}, and \funarrow{}
138
stand for the character strings \citecoq{<=}, \citecoq{<>},
139
\citecoq{exists}, \citecoq{forall}, \citecoq{->}, \citecoq{<-},
140
\texttt{\char'134/}, \texttt{/\char'134}, and \citecoq{=>},
141
respectively. For instance, the \coq{} statement
144
% traduction numero 1
146
\hide{Open Scope nat_scope. Check (}forall A:Type,(exists x : A, forall (y:A), x <> y) -> 2 = 3\hide{).}
148
is written as follows in this tutorial:
151
% traduction numero 2
153
\hide{Check (}{\prodsym}A:Type,(\exsym{}x:A, {\prodsym}y:A, x {\coqdiff} y) \arrow{} 2 = 3\hide{).}
156
When a fragment of \coq{} input text appears in the middle of
157
regular text, we often place this fragment between double quotes
158
``\dots.'' These double quotes do not belong to the \coq{} syntax.
161
string enclosed between \texttt{(*} and \texttt{*)} is a comment and
162
is ignored by the \coq{} system.
164
\section{Introducing Inductive Types}
167
Inductive types are types closed with respect to their introduction
168
rules. These rules explain the most basic or \textsl{canonical} ways
169
of constructing an element of the type. In this sense, they
170
characterize the recursive type. Different rules must be considered as
171
introducing different objects. In order to fix ideas, let us introduce
172
in {\coq} the most well-known example of a recursive type: the type of
177
Inductive nat : Set :=
179
| S : nat\arrow{}nat.
182
The definition of a recursive type has two main parts. First, we
183
establish what kind of recursive type we will characterize (a set, in
184
this case). Second, we present the introduction rules that define the
185
type ({\Z} and {\SUCC}), also called its {\sl constructors}. The constructors
186
{\Z} and {\SUCC} determine all the elements of this type. In other
187
words, if $n\mbox{:}\nat$, then $n$ must have been introduced either
188
by the rule {\Z} or by an application of the rule {\SUCC} to a
189
previously constructed natural number. In this sense, we can say
190
that {\nat} is \emph{closed}. On the contrary, the type
191
$\Set$ is an {\it open} type, since we do not know {\it a priori} all
192
the possible ways of introducing an object of type \texttt{Set}.
194
After entering this command, the constants {\nat}, {\Z} and {\SUCC} are
195
available in the current context. We can see their types using the
196
\texttt{Check} command \refmancite{Section \ref{Check}}:
205
\it{}S : nat {\arrow} nat
208
Moreover, {\coq} adds to the context three constants named
209
$\natind$, $\natrec$ and $\natrect$, which
210
correspond to different principles of structural induction on
211
natural numbers that {\coq} infers automatically from the definition. We
212
will come back to them in Section \ref{StructuralInduction}.
215
In fact, the type of natural numbers as well as several useful
216
theorems about them are already defined in the basic library of {\coq},
217
so there is no need to introduce them. Therefore, let us throw away
218
our (re)definition of {\nat}, using the command \texttt{Reset}.
224
\it{}Inductive nat : Set := O : nat | S : nat \arrow{} nat
225
For S: Argument scope is [nat_scope]
228
Notice that \coq{}'s \emph{interpretation scope} for natural numbers
229
(called \texttt{nat\_scope})
230
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
231
as the digit $0$, and the term ``~\texttt{S (S (S O))}~'' as $3$.
242
Let us now take a look to some other
243
recursive types contained in the standard library of {\coq}.
246
Lists are defined in library \citecoq{List}\footnote{Notice that in versions of
248
prior to 8.1, the parameter $A$ had sort \citecoq{Set} instead of \citecoq{Type};
249
the constant \citecoq{list} was thus of type \citecoq{Set\arrow{} Set}.}
256
Inductive list (A : Type) : Type:=
257
nil : list A | cons : A {\arrow} list A {\arrow} list A
258
For nil: Argument A is implicit
259
For cons: Argument A is implicit
260
For list: Argument scope is [type_scope]
261
For nil: Argument scope is [type_scope]
262
For cons: Argument scopes are [type_scope _ _]
265
In this definition, \citecoq{A} is a \emph{general parameter}, global
266
to both constructors.
267
This kind of definition allows us to build a whole family of
268
inductive types, indexed over the sort \citecoq{Type}.
269
This can be observed if we consider the type of identifiers
270
\citecoq{list}, \citecoq{cons} and \citecoq{nil}.
271
Notice the notation \citecoq{(A := \dots)} which must be used
272
when {\coq}'s type inference algorithm cannot infer the implicit
273
parameter \citecoq{A}.
279
\tt Check (nil (A:=nat)).
283
\tt Check (nil (A:= nat {\arrow} nat)).
285
: list (nat {\arrow} nat)
287
\tt Check (fun A: Type {\funarrow} (cons (A:=A))).
288
\it fun A : Type {\funarrow} cons (A:=A)
289
: {\prodsym} A : Type, A {\arrow} list A {\arrow} list A
291
\tt Check (cons 3 (cons 2 nil)).
295
\tt Check (nat :: bool ::nil).
296
\it nat :: bool :: nil
299
\tt Check ((3<=4) :: True ::nil).
300
\it (3<=4) :: True :: nil
303
\tt Check (Prop::Set::nil).
308
\subsection{Vectors.}
311
Like \texttt{list}, \citecoq{vector} is a polymorphic type:
312
if $A$ is a type, and $n$ a natural number, ``~\citecoq{vector $A$ $n$}~''
313
is the type of vectors of elements of $A$ and size $n$.
317
Require Import Bvector.
321
Inductive vector (A : Type) : nat {\arrow} Type :=
323
| Vcons : A {\arrow} {\prodsym} n : nat, vector A n {\arrow} vector A (S n)
324
For vector: Argument scopes are [type_scope nat_scope]
325
For Vnil: Argument scope is [type_scope]
326
For Vcons: Argument scopes are [type_scope _ nat_scope _]
330
Remark the difference between the two parameters $A$ and $n$:
331
The first one is a \textsl{general parameter}, global to all the
332
introduction rules,while the second one is an \textsl{index}, which is
333
instantiated differently in the introduction rules.
334
Such types parameterized by regular
335
values are called \emph{dependent types}.
342
\tt Check (fun (A:Type)(a:A){\funarrow} Vcons _ a _ (Vnil _)).
343
\it fun (A : Type) (a : A) {\funarrow} Vcons A a 0 (Vnil A)
344
: {\prodsym} A : Type, A {\arrow} vector A 1
347
\tt Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
348
\it Vcons nat 5 1 (Vcons nat 3 0 (Vnil nat))
352
\subsection{The contradictory proposition.}
353
Another example of an inductive type is the contradictory proposition.
354
This type inhabits the universe of propositions, and has no element
359
\it{} Inductive False : Prop :=
362
\noindent Notice that no constructor is given in this definition.
364
\subsection{The tautological proposition.}
366
tautological proposition {\True} is defined as an inductive type
367
with only one element {\I}:
372
\it{}Inductive True : Prop := I : True
375
\subsection{Relations as inductive types.}
376
Some relations can also be introduced in a smart way as an inductive family
377
of propositions. Let us take as example the order $n \leq m$ on natural
378
numbers, called \citecoq{le} in {\coq}.
379
This relation is introduced through
380
the following definition, quoted from the standard library\footnote{In the interpretation scope
381
for Peano arithmetic:
382
\citecoq{nat\_scope}, ``~\citecoq{n <= m}~'' is equivalent to
383
``~\citecoq{le n m}~'' .}:
391
Inductive le (n:nat) : nat\arrow{}Prop :=
393
| le_S: {\prodsym} m, n {\coqle} m \arrow{} n {\coqle} S m.
396
Notice that in this definition $n$ is a general parameter,
397
while the second argument of \citecoq{le} is an index (see section
400
introduces the binary relation $n {\leq} m$ as the family of unary predicates
401
``\textsl{to be greater or equal than a given $n$}'', parameterized by $n$.
403
The introduction rules of this type can be seen as a sort of Prolog
404
rules for proving that a given integer $n$ is less or equal than another one.
405
In fact, an object of type $n{\leq} m$ is nothing but a proof
406
built up using the constructors \textsl{le\_n} and
407
\textsl{le\_S} of this type. As an example, let us construct
408
a proof that zero is less or equal than three using {\coq}'s interactive
410
Such an object can be obtained applying three times the second
411
introduction rule of \citecoq{le}, to a proof that zero is less or equal
413
which is provided by the first constructor of \citecoq{le}:
417
Theorem zero_leq_three: 0 {\coqle} 3.
421
============================
428
============================
433
============================
438
============================
448
the current goal is an inductive type, the tactic
449
``~\citecoq{constructor $i$}~'' \refmancite{Section \ref{constructor}} applies the $i$-th constructor in the
450
definition of the type. We can take a look at the proof constructed
451
using the command \texttt{Print}:
455
Print Print zero_leq_three.
456
\it{}zero_leq_three =
457
zero_leq_three = le_S 0 2 (le_S 0 1 (le_S 0 0 (le_n 0)))
461
When the parameter $i$ is not supplied, the tactic \texttt{constructor}
462
tries to apply ``~\texttt{constructor $1$}~'', ``~\texttt{constructor $2$}~'',\dots,
463
``~\texttt{constructor $n$}~'' where $n$ is the number of constructors
464
of the inductive type (2 in our example) of the conclusion of the goal.
465
Our little proof can thus be obtained iterating the tactic
466
\texttt{constructor} until it fails:
470
Lemma zero_leq_three': 0 {\coqle} 3.
475
Notice that the strict order on \texttt{nat}, called \citecoq{lt}
476
is not inductively defined: the proposition $n<p$ (notation for \citecoq{lt $n$ $p$})
477
is reducible to \citecoq{(S $n$) $\leq$ p}.
482
lt = fun n m : nat {\funarrow} S n {\coqle} m
483
: nat {\arrow} nat {\arrow} Prop
485
Lemma zero_lt_three : 0 < 3.
491
\it zero_lt_three = le_S 1 2 (le_S 1 1 (le_n 1))
497
\subsection{About general parameters (\coq{} version $\geq$ 8.1)}
498
\label{parameterstuff}
500
Since version $8.1$, it is possible to write more compact inductive definitions
501
than in earlier versions.
503
Consider the following alternative definition of the relation $\leq$ on
507
Inductive le'(n:nat):nat -> Prop :=
509
| le'_S : forall p, le' (S n) p -> le' n p.
511
Hint Constructors le'.
514
We notice that the type of the second constructor of \citecoq{le'}
515
has an argument whose type is \citecoq{le' (S n) p}.
516
This constrasts with earlier versions
517
of {\coq}, in which a general parameter $a$ of an inductive
518
type $I$ had to appear only in applications of the form $I\,\dots\,a$.
520
Since version $8.1$, if $a$ is a general parameter of an inductive
521
type $I$, the type of an argument of a constructor of $I$ may be
522
of the form $I\,\dots\,t_a$ , where $t_a$ is any term.
523
Notice that the final type of the constructors must be of the form
524
$I\,\dots\,a$, since these constructors describe how to form
525
inhabitants of type $I\,\dots\,a$ (this is the role of parameter $a$).
527
Another example of this new feature is {\coq}'s definition of accessibility
528
(see Section~\ref{WellFoundedRecursion}), which has a general parameter
529
$x$; the constructor for the predicate
530
``$x$ is accessible'' takes an argument of type ``$y$ is accessible''.
534
In earlier versions of {\coq}, a relation like \citecoq{le'} would have to be
535
defined without $n$ being a general parameter.
540
Inductive le': nat-> nat -> Prop :=
541
| le'_n : forall n, le' n n
542
| le'_S : forall n p, le' (S n) p -> le' n p.
548
\subsection{The propositional equality type.} \label{equality}
549
In {\coq}, the propositional equality between two inhabitants $a$ and
552
noted $a=b$, is introduced as a family of recursive predicates
553
``~\textsl{to be equal to $a$}~'', parameterised by both $a$ and its type
554
$A$. This family of types has only one introduction rule, which
555
corresponds to reflexivity.
556
Notice that the syntax ``\citecoq{$a$ = $b$}~'' is an abbreviation
557
for ``\citecoq{eq $a$ $b$}~'', and that the parameter $A$ is \emph{implicit},
558
as it can be infered from $a$.
562
\it{} Inductive eq (A : Type) (x : A) : A \arrow{} Prop :=
564
For eq: Argument A is implicit
565
For refl_equal: Argument A is implicit
566
For eq: Argument scopes are [type_scope _ _]
567
For refl_equal: Argument scopes are [type_scope _]
570
Notice also that the first parameter $A$ of \texttt{eq} has type
571
\texttt{Type}. The type system of {\coq} allows us to consider equality between
572
various kinds of terms: elements of a set, proofs, propositions,
574
Look at \cite{coqrefman, coqart} to get more details on {\coq}'s type
575
system, as well as implicit arguments and argument scopes.
579
Lemma eq_3_3 : 2 + 1 = 3.
584
Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
589
Print eq_proof_proof.
591
refl_equal (refl_equal (3 * 4))
592
: refl_equal (2 * 6) = refl_equal (3 * 4)
595
Lemma eq_lt_le : ( 2 < 4) = (3 {\coqle} 4).
600
Lemma eq_nat_nat : nat = nat.
605
Lemma eq_Set_Set : Set = Set.
611
\subsection{Logical connectives.} \label{LogicalConnectives}
612
The conjunction and disjunction of two propositions are also examples
616
Inductive or (A B : Prop) : Prop :=
617
or_introl : A \arrow{} A {\coqor} B | or_intror : B \arrow{} A {\coqor} B
619
Inductive and (A B : Prop) : Prop :=
620
conj : A \arrow{} B \arrow{} A {\coqand} B
624
The propositions $A$ and $B$ are general parameters of these
625
connectives. Choosing different universes for
626
$A$ and $B$ and for the inductive type itself gives rise to different
627
type constructors. For example, the type \textsl{sumbool} is a
628
disjunction but with computational contents.
631
Inductive sumbool (A B : Prop) : Set :=
632
left : A \arrow{} \{A\} + \{B\} | right : B \arrow{} \{A\} + \{B\}
637
This type --noted \texttt{\{$A$\}+\{$B$\}} in {\coq}-- can be used in {\coq}
638
programs as a sort of boolean type, to check whether it is $A$ or $B$
639
that is true. The values ``~\citecoq{left $p$}~'' and
640
``~\citecoq{right $q$}~'' replace the boolean values \textsl{true} and
641
\textsl{false}, respectively. The advantage of this type over
642
\textsl{bool} is that it makes available the proofs $p$ of $A$ or $q$
643
of $B$, which could be necessary to construct a verification proof
645
For instance, let us consider the certified program \citecoq{le\_lt\_dec}
646
of the Standard Library.
649
Require Import Compare_dec.
653
: {\prodsym} n m : nat, \{n {\coqle} m\} + \{m < n\}
657
We use \citecoq{le\_lt\_dec} to build a function for computing
658
the max of two natural numbers:
661
Definition max (n p :nat) := match le_lt_dec n p with
662
| left _ {\funarrow} p
663
| right _ {\funarrow} n
667
In the following proof, the case analysis on the term
668
``~\citecoq{le\_lt\_dec n p}~'' gives us an access to proofs
669
of $n\leq p$ in the first case, $p<n$ in the other.
672
Theorem le_max : {\prodsym} n p, n {\coqle} p {\arrow} max n p = p.
674
intros n p ; unfold max ; case (le_lt_dec n p); simpl.
680
============================
681
n {\coqle} p {\arrow} n {\coqle} p {\arrow} p = p
684
p < n {\arrow} n {\coqle} p {\arrow} n = p
687
intros; absurd (p < p); eauto with arith.
692
Once the program verified, the proofs are
693
erased by the extraction procedure:
698
(** val max : nat {\arrow} nat {\arrow} nat **)
701
match le_lt_dec n p with
706
Another example of use of \citecoq{sumbool} is given in Section
707
\ref{WellFoundedRecursion}: the theorem \citecoq{eq\_nat\_dec} of
708
library \citecoq{Coq.Arith.Peano\_dec} is used in an euclidean division
711
\subsection{The existential quantifier.}\label{ex-def}
712
The existential quantifier is yet another example of a logical
713
connective introduced as an inductive type.
716
Inductive ex (A : Type) (P : A \arrow{} Prop) : Prop :=
717
ex_intro : {\prodsym} x : A, P x \arrow{} ex P
720
Notice that {\coq} uses the abreviation ``~\citecoq{\exsym\,$x$:$A$, $B$}~''
721
for \linebreak ``~\citecoq{ex (fun $x$:$A$ \funarrow{} $B$)}~''.
724
\noindent The former quantifier inhabits the universe of propositions.
725
As for the conjunction and disjunction connectives, there is also another
726
version of existential quantification inhabiting the universes $\Type_i$,
727
which is noted \texttt{sig $P$}. The syntax
728
``~\citecoq{\{$x$:$A$ | $B$\}}~'' is an abreviation for ``~\citecoq{sig (fun $x$:$A$ {\funarrow} $B$)}~''.
732
%\paragraph{The logical connectives.} Conjuction and disjuction are
733
%also introduced as recursive types:
742
\subsection{Mutually Dependent Definitions}
743
\label{MutuallyDependent}
745
Mutually dependent definitions of recursive types are also allowed in
746
{\coq}. A typical example of these kind of declaration is the
747
introduction of the trees of unbounded (but finite) width:
750
Inductive tree(A:Type) : Type :=
751
node : A {\arrow} forest A \arrow{} tree A
752
with forest (A: Set) : Type :=
754
addchild : tree A \arrow{} forest A \arrow{} forest A.
756
\noindent Yet another example of mutually dependent types are the
757
predicates \texttt{even} and \texttt{odd} on natural numbers:
761
even : nat\arrow{}Prop :=
763
evenS : {\prodsym} n, odd n \arrow{} even (S n)
765
odd : nat\arrow{}Prop :=
766
oddS : {\prodsym} n, even n \arrow{} odd (S n).
770
Lemma odd_49 : odd (7 * 7).
771
simpl; repeat constructor.
777
\section{Case Analysis and Pattern-matching}
779
\subsection{Non-dependent Case Analysis}
780
An \textsl{elimination rule} for the type $A$ is some way to use an
781
object $a:A$ in order to define an object in some type $B$.
782
A natural elimination rule for an inductive type is \emph{case analysis}.
785
For instance, any value of type {\nat} is built using either \texttt{O} or \texttt{S}.
786
Thus, a systematic way of building a value of type $B$ from any
787
value of type {\nat} is to associate to \texttt{O} a constant $t_O:B$ and
788
to every term of the form ``~\texttt{S $p$}~'' a term $t_S:B$. The following
789
construction has type $B$:
791
match \(n\) return \(B\) with O \funarrow \(t\sb{O}\) | S p \funarrow \(t\sb{S}\) end
795
In most of the cases, {\coq} is able to infer the type $B$ of the object
796
defined, so the ``\texttt{return $B$}'' part can be omitted.
798
The computing rules associated with this construct are the expected ones
799
(the notation $t_S\{q/\texttt{p}\}$ stands for the substitution of $p$ by
803
\texttt{match $O$ return $b$ with O {\funarrow} $t_O$ | S p {\funarrow} $t_S$ end} &\Longrightarrow& t_O\\
804
\texttt{match $S\;q$ return $b$ with O {\funarrow} $t_O$ | S p {\funarrow} $t_S$ end} &\Longrightarrow& t_S\{q/\texttt{p}\}
808
\subsubsection{Example: the predecessor function.}\label{firstpred}
809
An example of a definition by case analysis is the function which
810
computes the predecessor of any given natural number:
812
Definition pred (n:nat) := match n with
817
Eval simpl in pred 56.
821
Eval simpl in pred 0.
825
\tt{}Eval simpl in fun p {\funarrow} pred (S p).
826
\it{} = fun p : nat {\funarrow} p
830
As in functional programming, tuples and wild-cards can be used in
831
patterns \refmancite{Section \ref{ExtensionsOfCases}}. Such
832
definitions are automatically compiled by {\coq} into an expression which
833
may contain several nested case expressions. For example, the
834
exclusive \emph{or} on booleans can be defined as follows:
836
Definition xorb (b1 b2:bool) :=
838
| false, true {\funarrow} true
839
| true, false {\funarrow} true
840
| _ , _ {\funarrow} false
844
This kind of definition is compiled in {\coq} as follows\footnote{{\coq} uses
845
the conditional ``~\citecoq{if $b$ then $a$ else $b$}~'' as an abreviation to
846
``~\citecoq{match $b$ with true \funarrow{} $a$ | false \funarrow{} $b$ end}~''.}:
851
fun b1 b2 : bool {\funarrow}
852
if b1 then if b2 then false else true
853
else if b2 then true else false
854
: bool {\arrow} bool {\arrow} bool
857
\subsection{Dependent Case Analysis}
858
\label{DependentCase}
860
For a pattern matching construct of the form
861
``~\citecoq{match n with \dots end}~'' a more general typing rule
862
is obtained considering that the type of the whole expression
863
may also depend on \texttt{n}.
864
For instance, let us consider some function
865
$Q:\texttt{nat}\arrow{}\texttt{Type}$, and $n:\citecoq{nat}$.
866
In order to build a term of type $Q\;n$, we can associate
867
to the constructor \texttt{O} some term $t_O: Q\;\texttt{O}$ and to
868
the pattern ``~\texttt{S p}~'' some term $t_S : Q\;(S\;p)$.
869
Notice that the terms $t_O$ and $t_S$ do not have the same type.
871
The syntax of the \emph{dependent case analysis} and its
872
associated typing rule make precise how the resulting
873
type depends on the argument of the pattern matching, and
874
which constraint holds on the branches of the pattern matching:
876
\label{Prod-sup-rule}
879
Q: \texttt{nat}{\arrow}\texttt{Type}\quad{t_O}:{{Q\;\texttt{O}}} \quad
880
\smalljuge{p:\texttt{nat}}{t_p}{{Q\;(\texttt{S}\;p)}} \quad n:\texttt{nat} \\
882
{\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}}
887
The interest of this rule of \textsl{dependent} pattern-matching is
888
that it can also be read as the following logical principle (when $Q$ has type \citecoq{nat\arrow{}Prop}
889
by \texttt{Prop} in the type of $Q$): in order to prove
890
that a property $Q$ holds for all $n$, it is sufficient to prove that
891
$Q$ holds for {\Z} and that for all $p:\nat$, $Q$ holds for
892
$(\SUCC\;p)$. The former, non-dependent version of case analysis can
893
be obtained from this latter rule just taking $Q$ as a constant
896
Notice that destructuring $n$ into \citecoq{O} or ``~\citecoq{S p}~''
898
make appear in the goal the equalities ``~$n=\citecoq{O}$~''
899
and ``~$n=\citecoq{S p}$~''.
900
They are ``internalized'' in the rules above (see section~\ref{inversion}.)
902
\subsubsection{Example: strong specification of the predecessor function.}
904
In Section~\ref{firstpred}, the predecessor function was defined directly
905
as a function from \texttt{nat} to \texttt{nat}. It remains to prove
906
that this function has some desired properties. Another way to proceed
907
is to, first introduce a specification of what is the predecessor of a
908
natural number, under the form of a {\coq} type, then build an inhabitant
909
of this type: in other words, a realization of this specification. This way, the correctness
910
of this realization is ensured by {\coq}'s type system.
912
A reasonable specification for $\pred$ is to say that for all $n$
913
there exists another $m$ such that either $m=n=0$, or $(\SUCC\;m)$
914
is equal to $n$. The function $\pred$ should be just the way to
918
Definition pred_spec (n:nat) :=
919
\{m:nat | n=0{\coqand} m=0 {\coqor} n = S m\}.
921
Definition predecessor : {\prodsym} n:nat, pred_spec n.
925
============================
928
\tt{} unfold pred_spec;exists 0;auto.
930
=========================================
931
{\prodsym} n0 : nat, pred_spec (S n0)
933
unfold pred_spec; intro n0; exists n0; auto.
937
If we print the term built by {\coq}, we can observe its dependent pattern-matching structure:
940
predecessor = fun n : nat {\funarrow}
941
\textbf{match n as n0 return (pred_spec n0) with}
942
\textbf{| O {\funarrow}}
943
exist (fun m : nat {\funarrow} 0 = 0 {\coqand} m = 0 {\coqor} 0 = S m) 0
945
(conj (refl_equal 0) (refl_equal 0)))
946
\textbf{| S n0 {\funarrow}}
947
exist (fun m : nat {\funarrow} S n0 = 0 {\coqand} m = 0 {\coqor} S n0 = S m) n0
948
(or_intror (S n0 = 0 {\coqand} n0 = 0) (refl_equal (S n0)))
949
\textbf{end} : {\prodsym} n : nat, \textbf{pred_spec n}
953
Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at the reference manual and/or the book: tactics
954
\texttt{destruct}, ``~\texttt{intro \emph{pattern}}~'', etc.
956
\noindent The command \texttt{Extraction} \refmancite{Section
957
\ref{ExtractionIdent}} can be used to see the computational
958
contents associated to the \emph{certified} function \texttt{predecessor}:
960
Extraction predecessor.
962
(** val predecessor : nat {\arrow} pred_spec **)
964
let predecessor = function
970
\begin{exercise} \label{expand}
971
Prove the following theorem:
973
Theorem nat_expand : {\prodsym} n:nat,
976
| S p {\funarrow} S p
981
\subsection{Some Examples of Case Analysis}
983
The reader will find in the Reference manual all details about
984
typing case analysis (chapter 4: Calculus of Inductive Constructions,
985
and chapter 15: Extended Pattern-Matching).
987
The following commented examples will show the different situations to consider.
990
%\subsubsection{General Scheme}
992
%Case analysis is then the most basic elimination rule that {\coq}
993
%provides for inductive types. This rule follows a general schema,
994
%valid for any inductive type $I$. First, if $I$ has type
995
%``~$\forall\,(z_1:A_1)\ldots(z_r:A_r),S$~'', with $S$ either $\Set$, $\Prop$ or
996
%$\Type$, then a case expression on $p$ of type ``~$R\;a_1\ldots a_r$~''
997
% inhabits ``~$Q\;a_1\ldots a_r\;p$~''. The types of the branches of the case expression
998
%are obtained from the definition of the type in this way: if the type
999
%of the $i$-th constructor $c_i$ of $R$ is
1000
%``~$\forall\, (x_1:T_1)\ldots
1001
%(x_n:T_n),(R\;q_1\ldots q_r)$~'', then the $i-th$ branch must have the
1002
%form ``~$c_i\; x_1\; \ldots \;x_n\; \funarrow{}\; t_i$~'' where
1003
%$$(x_1:T_1),\ldots, (x_n:T_n) \vdash t_i : Q\;q_1\ldots q_r)$$
1004
% for non-dependent case
1005
%analysis, and $$(x_1:T_1)\ldots (x_n:T_n)\vdash t_i :Q\;q_1\ldots
1006
%q_r\;({c}_i\;x_1\;\ldots x_n)$$ for dependent one. In the
1007
%following section, we illustrate this general scheme for different
1009
%%\textbf{A v�rifier}
1011
\subsubsection{The Empty Type}
1013
In a definition by case analysis, there is one branch for each
1014
introduction rule of the type. Hence, in a definition by case analysis
1015
on $p:\False$ there are no cases to be considered. In other words, the
1016
rule of (non-dependent) case analysis for the type $\False$ is
1017
(for $s$ in \texttt{Prop}, \texttt{Set} or \texttt{Type}):
1020
\snregla {\JM{Q}{s}\;\;\;\;\;
1022
{\JM{\texttt{match $p$ return $Q$ with end}}{Q}}
1025
As a corollary, if we could construct an object in $\False$, then it
1026
could be possible to define an object in any type. The tactic
1027
\texttt{contradiction} \refmancite{Section \ref{Contradiction}}
1028
corresponds to the application of the elimination rule above. It
1029
searches in the context for an absurd hypothesis (this is, a
1030
hypothesis whose type is $\False$) and then proves the goal by a case
1034
Theorem fromFalse : False \arrow{} 0=1.
1042
In {\coq} the negation is defined as follows :
1045
Definition not (P:Prop) := P {\arrow} False
1048
The proposition ``~\citecoq{not $A$}~'' is also written ``~$\neg A$~''.
1050
If $A$ and $B$ are propositions, $a$ is a proof of $A$ and
1051
$H$ is a proof of $\neg A$,
1052
the term ``~\citecoq{match $H\;a$ return $B$ with end}~'' is a proof term of
1054
Thus, if your goal is $B$ and you have some hypothesis $H:\neg A$,
1055
the tactic ``~\citecoq{case $H$}~'' generates a new subgoal with
1056
statement $A$, as shown by the following example\footnote{Notice that
1057
$a\coqdiff b$ is just an abreviation for ``~\coqnot a= b~''}.
1060
Fact Nosense : 0 {\coqdiff} 0 {\arrow} 2 = 3.
1064
===========================
1071
The tactic ``~\texttt{absurd $A$}~'' (where $A$ is any proposition),
1072
is based on the same principle, but
1073
generates two subgoals: $A$ and $\neg A$, for solving $B$.
1075
\subsubsection{The Equality Type}
1077
Let $A:\Type$, $a$, $b$ of type $A$, and $\pi$ a proof of
1078
$a=b$. Non dependent case analysis of $\pi$ allows us to
1079
associate to any proof of ``~$Q\;a$~'' a proof of ``~$Q\;b$~'',
1080
where $Q:A\arrow{} s$ (where $s\in\{\Prop, \Set, \Type\}$).
1081
The following term is a proof of ``~$Q\;a\, \arrow{}\, Q\;b$~''.
1084
fun H : Q a {\funarrow}
1085
match \(\pi\) in (_ = y) return Q y with
1086
refl_equal {\funarrow} H
1089
Notice the header of the \texttt{match} construct.
1090
It expresses how the resulting type ``~\citecoq{Q y}~'' depends on
1091
the \emph{type} of \texttt{p}.
1092
Notice also that in the pattern introduced by the keyword \texttt{in},
1093
the parameter \texttt{a} in the type ``~\texttt{a = y}~'' must be
1094
implicit, and replaced by a wildcard '\texttt{\_}'.
1097
Therefore, case analysis on a proof of the equality $a=b$
1098
amounts to replacing all the occurrences of the term $b$ with the term
1099
$a$ in the goal to be proven. Let us illustrate this through an
1100
example: the transitivity property of this equality.
1102
Theorem trans : {\prodsym} n m p:nat, n=m \arrow{} m=p \arrow{} n=p.
1110
============================
1111
m = p {\arrow} n = p
1118
============================
1119
n = p {\arrow} n = p
1124
%\noindent The case analysis on the hypothesis $H:n=m$ yields the
1125
%tautological subgoal $n=p\rightarrow n=p$, that is directly proven by
1126
%the tactic \texttt{Trivial}.
1129
Prove the symmetry property of equality.
1132
Instead of using \texttt{case}, we can use the tactic
1133
\texttt{rewrite} \refmancite{Section \ref{Rewrite}}. If $H$ is a proof
1135
``~\citecoq{rewrite $H$}~''
1136
performs a case analysis on a proof of $b=a$, obtained by applying a
1137
symmetry theorem to $H$. This application of symmetry allows us to rewrite
1138
the equality from left to right, which looks more natural. An optional
1139
parameter (either \texttt{\arrow{}} or \texttt{$\leftarrow$}) can be used to precise
1140
in which sense the equality must be rewritten. By default,
1141
``~\texttt{rewrite} $H$~'' corresponds to ``~\texttt{rewrite \arrow{}} $H$~''
1143
Lemma Rw : {\prodsym} x y: nat, y = y * x {\arrow} y * x * x = y.
1144
intros x y e; do 2 rewrite <- e.
1151
============================
1158
Notice that, if $H:a=b$, then the tactic ``~\texttt{rewrite $H$}~''
1159
replaces \textsl{all} the
1160
occurrences of $a$ by $b$. However, in certain situations we could be
1161
interested in rewriting some of the occurrences, but not all of them.
1162
This can be done using the tactic \texttt{pattern} \refmancite{Section
1163
\ref{Pattern}}. Let us consider yet another example to
1166
Let us start with some simple theorems of arithmetic; two of them
1167
are already proven in the Standard Library, the last is left as an exercise.
1172
: {\prodsym} n : nat, 1 * n = n
1175
: {\prodsym} n m p : nat, (n + m) * p = n * p + m * p
1177
mult_distr_S : {\prodsym} n p : nat, n * p + p = (S n)* p.
1180
Let us now prove a simple result:
1183
Lemma four_n : {\prodsym} n:nat, n+n+n+n = 4*n.
1185
intro n;rewrite <- (mult_1_l n).
1188
============================
1189
1 * n + 1 * n + 1 * n + 1 * n = 4 * (1 * n)
1192
We can see that the \texttt{rewrite} tactic call replaced \emph{all}
1193
the occurrences of \texttt{n} by the term ``~\citecoq{1 * n}~''.
1194
If we want to do the rewriting ony on the leftmost occurrence of
1195
\texttt{n}, we can mark this occurrence using the \texttt{pattern}
1201
intro n; pattern n at 1.
1204
============================
1205
(fun n0 : nat {\funarrow} n0 + n + n + n = 4 * n) n
1207
Applying the tactic ``~\citecoq{pattern n at 1}~'' allowed us
1208
to explicitly abstract the first occurrence of \texttt{n} from the
1209
goal, putting this goal under the form ``~\citecoq{$Q$ n}~'',
1210
thus pointing to \texttt{rewrite} the particular predicate on $n$
1211
that we search to prove.
1215
rewrite <- mult_1_l.
1220
============================
1221
1 * n + n + n + n = 4 * n
1223
repeat rewrite mult_distr_S.
1226
============================
1233
\subsubsection{The Predicate $n {\leq} m$}
1236
The last but one instance of the elimination schema that we will illustrate is
1237
case analysis for the predicate $n {\leq} m$:
1239
Let $n$ and $p$ be terms of type \citecoq{nat}, and $Q$ a predicate
1240
of type $\citecoq{nat}\arrow{}\Prop$.
1241
If $H$ is a proof of ``~\texttt{n {\coqle} p}~'',
1242
$H_0$ a proof of ``~\texttt{$Q$ n}~'' and
1243
$H_S$ a proof of ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'',
1246
match H in (_ {\coqle} q) return (Q q) with
1247
| le_n {\funarrow} H0
1248
| le_S m Hm {\funarrow} HS m Hm
1251
is a proof term of ``~\citecoq{$Q$ $p$}~''.
1254
The two patterns of this \texttt{match} construct describe
1255
all possible forms of proofs of ``~\citecoq{n {\coqle} m}~'' (notice
1256
again that the general parameter \texttt{n} is implicit in
1257
the ``~\texttt{in \dots}~''
1258
clause and is absent from the match patterns.
1261
Notice that the choice of introducing some of the arguments of the
1262
predicate as being general parameters in its definition has
1263
consequences on the rule of case analysis that is derived. In
1264
particular, the type $Q$ of the object defined by the case expression
1265
only depends on the indexes of the predicate, and not on the general
1266
parameters. In the definition of the predicate $\leq$, the first
1267
argument of this relation is a general parameter of the
1268
definition. Hence, the predicate $Q$ to be proven only depends on the
1269
second argument of the relation. In other words, the integer $n$ is
1270
also a general parameter of the rule of case analysis.
1272
An example of an application of this rule is the following theorem,
1273
showing that any integer greater or equal than $1$ is the successor of another
1277
Lemma predecessor_of_positive :
1278
{\prodsym} n, 1 {\coqle} n {\arrow} {\exsym} p:nat, n = S p.
1284
============================
1285
{\exsym} p : nat, 1 = S p
1292
============================
1293
{\prodsym} m : nat, 0 {\coqle} m {\arrow} {\exsym} p : nat, S m = S p
1302
\subsubsection{Vectors}
1304
The \texttt{vector} polymorphic and dependent family of types will
1305
give an idea of the most general scheme of pattern-matching.
1307
For instance, let us define a function for computing the tail of
1308
any vector. Notice that we shall build a \emph{total} function,
1309
by considering that the tail of an empty vector is this vector itself.
1310
In that sense, it will be slightly different from the \texttt{Vtail}
1311
function of the Standard Library, which is defined only for vectors
1312
of type ``~\citecoq{vector $A$ (S $n$)}~''.
1314
The header of the function we want to build is the following:
1317
Definition Vtail_total
1318
(A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
1321
Since the branches will not have the same type
1322
(depending on the parameter \texttt{n}),
1323
the body of this function is a dependent pattern matching on
1327
match v in (vector _ n0) return (vector A (pred n0)) with
1330
The first branch deals with the constructor \texttt{Vnil} and must
1331
return a value in ``~\citecoq{vector A (pred 0)}~'', convertible
1332
to ``~\citecoq{vector A 0}~''. So, we propose:
1334
| Vnil {\funarrow} Vnil A
1337
The second branch considers a vector in ``~\citecoq{vector A (S n0)}~''
1339
``~\citecoq{Vcons A n0 v0}~'', with ``~\citecoq{v0:vector A n0}~'',
1340
and must return a value of type ``~\citecoq{vector A (pred (S n0))}~'',
1341
which is convertible to ``~\citecoq{vector A n0}~''.
1342
This second branch is thus :
1344
| Vcons _ n0 v0 {\funarrow} v0
1347
Here is the full definition:
1350
Definition Vtail_total
1351
(A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
1352
match v in (vector _ n0) return (vector A (pred n0)) with
1353
| Vnil {\funarrow} Vnil A
1354
| Vcons _ n0 v0 {\funarrow} v0
1359
\subsection{Case Analysis and Logical Paradoxes}
1361
In the previous section we have illustrated the general scheme for
1362
generating the rule of case analysis associated to some recursive type
1363
from the definition of the type. However, if the logical soundness is
1364
to be preserved, certain restrictions to this schema are
1365
necessary. This section provides a brief explanation of these
1369
\subsubsection{The Positivity Condition}
1372
In order to make sense of recursive types as types closed under their
1373
introduction rules, a constraint has to be imposed on the possible
1374
forms of such rules. This constraint, known as the
1375
\textsl{positivity condition}, is necessary to prevent the user from
1376
naively introducing some recursive types which would open the door to
1377
logical paradoxes. An example of such a dangerous type is the
1378
``inductive type'' \citecoq{Lambda}, whose only constructor is
1379
\citecoq{lambda} of type \citecoq{(Lambda\arrow False)\arrow Lambda}.
1380
Following the pattern
1381
given in Section \ref{CaseScheme}, the rule of (non dependent) case
1382
analysis for \citecoq{Lambda} would be the following:
1385
\snregla {\JM{Q}{\Prop}\;\;\;\;\;
1386
\JM{p}{\texttt{Lambda}}\;\;\;\;\;
1387
{h : {\texttt{Lambda}}\arrow\False\; \vdash\; t\,:\,Q}}
1388
{\JM{\citecoq{match $p$ return $Q$ with lambda h {\funarrow} $t$ end}}{Q}}
1391
In order to avoid paradoxes, it is impossible to construct
1392
the type \citecoq{Lambda} in {\coq}:
1395
Inductive Lambda : Set :=
1396
lambda : (Lambda {\arrow} False) {\arrow} Lambda.
1398
Error: Non strictly positive occurrence of "Lambda" in
1399
"(Lambda {\arrow} False) {\arrow} Lambda"
1402
In order to explain this danger, we
1403
will declare some constants for simulating the construction of
1404
\texttt{Lambda} as an inductive type.
1406
Let us open some section, and declare two variables, the first one for
1407
\texttt{Lambda}, the other for the constructor \texttt{lambda}.
1411
Variable Lambda : Set.
1412
Variable lambda : (Lambda {\arrow} False) {\arrow}Lambda.
1415
Since \texttt{Lambda} is not a truely inductive type, we can't use
1416
the \texttt{match} construct. Nevertheless, we can simulate it by a
1417
variable \texttt{matchL} such that the term
1418
``~\citecoq{matchL $l$ $Q$ (fun $h$ : Lambda {\arrow} False {\funarrow} $t$)}~''
1419
should be understood as
1420
``~\citecoq{match $l$ return $Q$ with | lambda h {\funarrow} $t$)}~''
1424
Variable matchL : Lambda {\arrow}
1425
{\prodsym} Q:Prop, ((Lambda {\arrow}False) {\arrow} Q) {\arrow}
1429
>From these constants, it is possible to define application by case
1430
analysis. Then, through auto-application, the well-known looping term
1431
$(\lambda x.(x\;x)\;\lambda x.(x\;x))$ provides a proof of falsehood.
1434
Definition application (f x: Lambda) :False :=
1435
matchL f False (fun h {\funarrow} h x).
1437
Definition Delta : Lambda :=
1438
lambda (fun x : Lambda {\funarrow} application x x).
1440
Definition loop : False := application Delta Delta.
1442
Theorem two_is_three : 2 = 3.
1450
\noindent This example can be seen as a formulation of Russell's
1451
paradox in type theory associating $(\textsl{application}\;x\;x)$ to the
1452
formula $x\not\in x$, and \textsl{Delta} to the set $\{ x \mid
1453
x\not\in x\}$. If \texttt{matchL} would satisfy the reduction rule
1454
associated to case analysis, that is,
1455
$$ \citecoq{matchL (lambda $f$) $Q$ $h$} \Longrightarrow h\;f$$
1456
then the term \texttt{loop}
1457
would compute into itself. This is not actually surprising, since the
1458
proof of the logical soundness of {\coq} strongly lays on the property
1459
that any well-typed term must terminate. Hence, non-termination is
1460
usually a synonymous of inconsistency.
1462
%\paragraph{} In this case, the construction of a non-terminating
1463
%program comes from the so-called \textsl{negative occurrence} of
1464
%$\Lambda$ in the type of the constructor $\lambda$. In order to be
1465
%admissible for {\coq}, all the occurrences of the recursive type in its
1466
%own introduction rules must be positive, in the sense on the following
1470
%\item $R$ is positive in $(R\;\vec{t})$;
1471
%\item $R$ is positive in $(x: A)C$ if it does not
1472
%occur in $A$ and $R$ is positive in $C$;
1473
%\item if $P\equiv (\vec{x}:\vec{T})Q$, then $R$ is positive in $(P
1474
%\rightarrow C)$ if $R$ does not occur in $\vec{T}$, $R$ is positive
1477
%\item $Q\equiv (R\;\vec{q})$ or
1478
%\item $Q\equiv (J\;\vec{t})$, \label{relax}
1479
% where $J$ is a recursive type, and for any term $t_i$ either :
1481
% \item $R$ does not occur in $t_i$, or
1482
% \item $t_i\equiv (z:\vec{Z})(R\;\vec{q})$, $R$ does not occur
1483
% in $\vec{Z}$, $t_i$ instantiates a general
1484
% parameter of $J$, and this parameter is positive in the
1485
% arguments of the constructors of $J$.
1489
%\noindent Those types obtained by erasing option (\ref{relax}) in the
1490
%definition above are called \textsl{strictly positive} types.
1493
\subsubsection*{Remark} In this case, the construction of a non-terminating
1494
program comes from the so-called \textsl{negative occurrence} of
1495
\texttt{Lambda} in the argument of the constructor \texttt{lambda}.
1497
The reader will find in the Reference Manual a complete formal
1498
definition of the notions of \emph{positivity condition} and
1499
\emph{strict positivity} that an inductive definition must satisfy.
1503
%admissible for {\coq}, the type $R$ must be positive in the types of the
1504
%arguments of its own introduction rules, in the sense on the following
1507
%\textbf{La d�finition du manuel de r�f�rence est plus complexe:
1508
%la recopier ou donner seulement des exemples?
1511
%\item $R$ is positive in $T$ if $R$ does not occur in $T$;
1512
%\item $R$ is positive in $(R\;\vec{t})$ if $R$ does not occur in $\vec{t}$;
1513
%\item $R$ is positive in $(x:A)C$ if it does not
1514
% occur in $A$ and $R$ is positive in $C$;
1515
%\item $R$ is positive in $(J\;\vec{t})$, \label{relax}
1516
% if $J$ is a recursive type, and for any term $t_i$ either :
1518
% \item $R$ does not occur in $t_i$, or
1519
% \item $R$ is positive in $t_i$, $t_i$ instantiates a general
1520
% parameter of $J$, and this parameter is positive in the
1521
% arguments of the constructors of $J$.
1525
%\noindent When we can show that $R$ is positive without using the item
1526
%(\ref{relax}) of the definition above, then we say that $R$ is
1527
%\textsl{strictly positive}.
1529
%\textbf{Changer le discours sur les ordinaux}
1531
Notice that the positivity condition does not forbid us to
1532
put functional recursive
1533
arguments in the constructors.
1535
For instance, let us consider the type of infinitely branching trees,
1536
with labels in \texttt{Z}.
1538
Require Import ZArith.
1540
Inductive itree : Set :=
1542
| inode : Z {\arrow} (nat {\arrow} itree) {\arrow} itree.
1545
In this representation, the $i$-th child of a tree
1546
represented by ``~\texttt{inode $z$ $s$}~'' is obtained by applying
1547
the function $s$ to $i$.
1548
The following definitions show how to construct a tree with a single
1549
node, a tree of height 1 and a tree of height 2:
1552
Definition isingle l := inode l (fun i {\funarrow} ileaf).
1554
Definition t1 := inode 0 (fun n {\funarrow} isingle (Z_of_nat n)).
1558
(fun n : nat {\funarrow}
1560
(fun p {\funarrow} isingle (Z_of_nat (n*p)))).
1564
Let us define a preorder on infinitely branching trees.
1565
In order to compare two non-leaf trees,
1566
it is necessary to compare each of their children
1567
without taking care of the order in which they
1571
Inductive itree_le : itree{\arrow} itree {\arrow} Prop :=
1572
| le_leaf : {\prodsym} t, itree_le ileaf t
1573
| le_node : {\prodsym} l l' s s',
1575
({\prodsym} i, {\exsym} j:nat, itree_le (s i) (s' j)){\arrow}
1576
itree_le (inode l s) (inode l' s').
1580
Notice that a call to the predicate \texttt{itree\_le} appears as
1581
a general parameter of the inductive type \texttt{ex} (see Sect.\ref{ex-def}).
1582
This kind of definition is accepted by {\coq}, but may lead to some
1583
difficulties, since the induction principle automatically
1584
generated by the system
1585
is not the most appropriate (see chapter 14 of~\cite{coqart} for a detailed
1589
The following definition, obtained by
1591
proposition \linebreak $\forall\, i,\exists\, j,(\texttt{itree\_le}\;(s\;i)\;(s'\;j))$ in
1592
the type of \texttt{itree\_le}, does not present this problem:
1596
Inductive itree_le' : itree{\arrow} itree {\arrow} Prop :=
1597
| le_leaf' : {\prodsym} t, itree_le' ileaf t
1598
| le_node' : {\prodsym} l l' s s' g,
1600
({\prodsym} i, itree_le' (s i) (s' (g i))) {\arrow}
1601
itree_le' (inode l s) (inode l' s').
1606
Lemma t1_le'_t2 : itree_le' t1 t2.
1609
constructor 2 with (fun i : nat {\funarrow} 2 * i).
1612
intro i ; constructor 2 with (fun i :nat {\funarrow} i).
1619
%In general, strictly positive definitions are preferable to only
1620
%positive ones. The reason is that it is sometimes difficult to derive
1621
%structural induction combinators for the latter ones. Such combinators
1622
%are automatically generated for strictly positive types, but not for
1623
%the only positive ones. Nevertheless, sometimes non-strictly positive
1624
%definitions provide a smarter or shorter way of declaring a recursive
1627
Another example is the type of trees
1628
of unbounded width, in which a recursive subterm
1629
\texttt{(ltree A)} instantiates the type of polymorphic lists:
1632
Require Import List.
1634
Inductive ltree (A:Set) : Set :=
1635
lnode : A {\arrow} list (ltree A) {\arrow} ltree A.
1638
This declaration can be transformed
1639
adding an extra type to the definition, as was done in Section
1640
\ref{MutuallyDependent}.
1643
\subsubsection{Impredicative Inductive Types}
1645
An inductive type $I$ inhabiting a universe $U$ is \textsl{predicative}
1646
if the introduction rules of $I$ do not make a universal
1647
quantification on a universe containing $U$. All the recursive types
1648
previously introduced are examples of predicative types. An example of
1649
an impredicative one is the following type:
1650
%\textsl{exT}, the dependent product
1651
%of a certain set (or proposition) $x$, and a proof of a property $P$
1657
%\textbf{ttention, EXT c'est ex!}
1659
%Check (exists P:Prop, P {\arrow} not P).
1662
%This type is useful for expressing existential quantification over
1663
%types, like ``there exists a proposition $x$ such that $(P\;x)$''
1664
%---written $(\textsl{EXT}\; x:Prop \mid (P\;x))$ in {\coq}. However,
1667
Inductive prop : Prop :=
1668
prop_intro : Prop {\arrow} prop.
1672
that the constructor of this type can be used to inject any
1673
proposition --even itself!-- into the type.
1676
Check (prop_intro prop).\it
1681
A careless use of such a
1682
self-contained objects may lead to a variant of Burali-Forti's
1683
paradox. The construction of Burali-Forti's paradox is more
1684
complicated than Russel's one, so we will not describe it here, and
1685
point the interested reader to \cite{Bar98,Coq86}.
1688
Another example is the second order existential quantifier for propositions:
1691
Inductive ex_Prop (P : Prop {\arrow} Prop) : Prop :=
1692
exP_intro : {\prodsym} X : Prop, P X {\arrow} ex_Prop P.
1697
%Check (match prop_inject with (prop_intro p _) {\funarrow} p end).
1699
%Error: Incorrect elimination of "prop_inject" in the inductive type
1701
%The elimination predicate ""fun _ : prop {\funarrow} Prop" has type
1702
% "prop {\arrow} Type"
1703
%It should be one of :
1706
%Elimination of an inductive object of sort : "Prop"
1707
%is not allowed on a predicate in sort : "Type"
1708
%because non-informative objects may not construct informative ones.
1715
%prop_inject = prop_intro prop (fun H : prop {\funarrow} H)
1720
% \textbf{Et par �a?
1723
Notice that predicativity on sort \citecoq{Set} forbids us to build
1724
the following definitions.
1728
Inductive aSet : Set :=
1729
aSet_intro: Set {\arrow} aSet.
1731
\it{}User error: Large non-propositional inductive types must be in Type
1733
Inductive ex_Set (P : Set {\arrow} Prop) : Set :=
1734
exS_intro : {\prodsym} X : Set, P X {\arrow} ex_Set P.
1736
\it{}User error: Large non-propositional inductive types must be in Type
1739
Nevertheless, one can define types like \citecoq{aSet} and \citecoq{ex\_Set}, as inhabitants of \citecoq{Type}.
1742
Inductive ex_Set (P : Set {\arrow} Prop) : Type :=
1743
exS_intro : {\prodsym} X : Set, P X {\arrow} ex_Set P.
1746
In the following example, the inductive type \texttt{typ} can be defined,
1747
but the term associated with the interactive Definition of
1748
\citecoq{typ\_inject} is incompatible with {\coq}'s hierarchy of universes:
1752
Inductive typ : Type :=
1753
typ_intro : Type {\arrow} typ.
1755
Definition typ_inject: typ.
1760
\it Error: Universe Inconsistency.
1765
One possible way of avoiding this new source of paradoxes is to
1766
restrict the kind of eliminations by case analysis that can be done on
1767
impredicative types. In particular, projections on those universes
1768
equal or bigger than the one inhabited by the impredicative type must
1769
be forbidden \cite{Coq86}. A consequence of this restriction is that it
1770
is not possible to define the first projection of the type
1771
``~\citecoq{ex\_Prop $P$}~'':
1773
Check (fun (P:Prop{\arrow}Prop)(p: ex_Prop P) {\funarrow}
1774
match p with exP_intro X HX {\funarrow} X end).
1777
Incorrect elimination of "p" in the inductive type
1778
"ex_Prop", the return type has sort "Type" while it should be
1781
Elimination of an inductive object of sort "Prop"
1782
is not allowed on a predicate in sort "Type"
1783
because proofs can be eliminated only to build proofs.
1786
%In order to explain why, let us consider for example the following
1787
%impredicative type \texttt{ALambda}.
1789
%Inductive ALambda : Set :=
1790
% alambda : (A:Set)(A\arrow{}False)\arrow{}ALambda.
1792
%Definition Lambda : Set := ALambda.
1793
%Definition lambda : (ALambda\arrow{}False)\arrow{}ALambda := (alambda ALambda).
1794
%Lemma CaseAL : (Q:Prop)ALambda\arrow{}((ALambda\arrow{}False)\arrow{}Q)\arrow{}Q.
1797
%This type contains all the elements of the dangerous type $\Lambda$
1798
%described at the beginning of this section. Try to construct the
1799
%non-ending term $(\Delta\;\Delta)$ as an object of
1800
%\texttt{ALambda}. Why is it not possible?
1802
\subsubsection{Extraction Constraints}
1804
There is a final constraint on case analysis that is not motivated by
1805
the potential introduction of paradoxes, but for compatibility reasons
1806
with {\coq}'s extraction mechanism \refmancite{Appendix
1807
\ref{CamlHaskellExtraction}}. This mechanism is based on the
1808
classification of basic types into the universe $\Set$ of sets and the
1809
universe $\Prop$ of propositions. The objects of a type in the
1810
universe $\Set$ are considered as relevant for computation
1811
purposes. The objects of a type in $\Prop$ are considered just as
1812
formalised comments, not necessary for execution. The extraction
1813
mechanism consists in erasing such formal comments in order to obtain
1814
an executable program. Hence, in general, it is not possible to define
1815
an object in a set (that should be kept by the extraction mechanism)
1816
by case analysis of a proof (which will be thrown away).
1818
Nevertheless, this general rule has an exception which is important in
1819
practice: if the definition proceeds by case analysis on a proof of a
1820
\textsl{singleton proposition} or an empty type (\emph{e.g.} \texttt{False}),
1821
then it is allowed. A singleton
1822
proposition is a non-recursive proposition with a single constructor
1823
$c$, all whose arguments are proofs. For example, the propositional
1824
equality and the conjunction of two propositions are examples of
1825
singleton propositions.
1827
%From the point of view of the extraction
1828
%mechanism, such types are isomorphic to a type containing a single
1829
%object $c$, so a definition $\Case{x}{c \Rightarrow b}$ is
1830
%directly replaced by $b$ as an extra optimisation.
1832
\subsubsection{Strong Case Analysis on Proofs}
1834
One could consider allowing
1835
to define a proposition $Q$ by case
1836
analysis on the proofs of another recursive proposition $R$. As we
1837
will see in Section \ref{Discrimination}, this would enable one to prove that
1838
different introduction rules of $R$ construct different
1839
objects. However, this property would be in contradiction with the principle
1840
of excluded middle of classical logic, because this principle entails
1841
that the proofs of a proposition cannot be distinguished. This
1842
principle is not provable in {\coq}, but it is frequently introduced by
1843
the users as an axiom, for reasoning in classical logic. For this
1844
reason, the definition of propositions by case analysis on proofs is
1845
not allowed in {\coq}.
1849
Definition comes_from_the_left (P Q:Prop)(H:P{\coqor}Q): Prop :=
1851
| or_introl p {\funarrow} True
1852
| or_intror q {\funarrow} False
1856
Incorrect elimination of "H" in the inductive type
1857
"or", the return type has sort "Type" while it should be
1860
Elimination of an inductive object of sort "Prop"
1861
is not allowed on a predicate in sort "Type"
1862
because proofs can be eliminated only to build proofs.
1866
On the other hand, if we replace the proposition $P {\coqor} Q$ with
1867
the informative type $\{P\}+\{Q\}$, the elimination is accepted:
1870
Definition comes_from_the_left_sumbool
1871
(P Q:Prop)(x:\{P\} + \{Q\}): Prop :=
1873
| left p {\funarrow} True
1874
| right q {\funarrow} False
1879
\subsubsection{Summary of Constraints}
1881
To end with this section, the following table summarizes which
1882
universe $U_1$ may inhabit an object of type $Q$ defined by case
1883
analysis on $x:R$, depending on the universe $U_2$ inhabited by the
1884
inductive types $R$.\footnote{In the box indexed by $U_1=\citecoq{Type}$
1885
and $U_2=\citecoq{Set}$, the answer ``yes'' takes into account the
1886
predicativity of sort \citecoq{Set}. If you are working with the
1887
option ``impredicative-set'', you must put in this box the
1888
condition ``if $R$ is predicative''.}
1892
\renewcommand{\multirowsetup}{\centering} \newlength{\LL}
1893
\settowidth{\LL}{$x : R : s_1$}
1894
\begin{tabular}{|c|c|c|c|c|}
1896
\multirow{5}{\LL}{$x : R : U_2$} &
1897
\multicolumn{4}{|c|}{$Q : U_1$}\\
1899
& &\textsl{Set} & \textsl{Prop} & \textsl{Type}\\
1901
&\textsl{Set} & yes & yes & yes\\
1903
&\textsl{Prop} & if $R$ singleton & yes & no\\
1905
&\textsl{Type} & yes & yes & yes\\
1910
\section{Some Proof Techniques Based on Case Analysis}
1911
\label{CaseTechniques}
1913
In this section we illustrate the use of case analysis as a proof
1914
principle, explaining the proof techniques behind three very useful
1915
{\coq} tactics, called \texttt{discriminate}, \texttt{injection} and
1918
\subsection{Discrimination of introduction rules}
1919
\label{Discrimination}
1921
In the informal semantics of recursive types described in Section
1922
\ref{Introduction} it was said that each of the introduction rules of a
1923
recursive type is considered as being different from all the others.
1924
It is possible to capture this fact inside the logical system using
1925
the propositional equality. We take as example the following theorem,
1926
stating that \textsl{O} constructs a natural number different
1927
from any of those constructed with \texttt{S}.
1930
Theorem S_is_not_O : {\prodsym} n, S n {\coqdiff} 0.
1933
In order to prove this theorem, we first define a proposition by case
1934
analysis on natural numbers, so that the proposition is true for {\Z}
1935
and false for any natural number constructed with {\SUCC}. This uses
1936
the empty and singleton type introduced in Sections \ref{Introduction}.
1939
Definition Is_zero (x:nat):= match x with
1940
| 0 {\funarrow} True
1941
| _ {\funarrow} False
1945
\noindent Then, we prove the following lemma:
1948
Lemma O_is_zero : {\prodsym} m, m = 0 {\arrow} Is_zero m.
1950
intros m H; subst m.
1959
\noindent Finally, the proof of \texttt{S\_is\_not\_O} follows by the
1960
application of the previous lemma to $S\;n$.
1969
============================
1972
apply O_is_zero with (m := S n).
1978
The tactic \texttt{discriminate} \refmancite{Section \ref{Discriminate}} is
1979
a special-purpose tactic for proving disequalities between two
1980
elements of a recursive type introduced by different constructors. It
1981
generalizes the proof method described here for natural numbers to any
1982
[co]-inductive type. This tactic is also capable of proving disequalities
1983
where the difference is not in the constructors at the head of the
1984
terms, but deeper inside them. For example, it can be used to prove
1985
the following theorem:
1988
Theorem disc2 : {\prodsym} n, S (S n) {\coqdiff} 1.
1990
intros n Hn; discriminate.
1994
When there is an assumption $H$ in the context stating a false
1995
equality $t_1=t_2$, \texttt{discriminate} solves the goal by first
1996
proving $(t_1\not =t_2)$ and then reasoning by absurdity with respect
2000
Theorem disc3 : {\prodsym} n, S (S n) = 0 {\arrow} {\prodsym} Q:Prop, Q.
2007
\noindent In this case, the proof proceeds by absurdity with respect
2008
to the false equality assumed, whose negation is proved by
2011
\subsection{Injectiveness of introduction rules}
2013
Another useful property about recursive types is the
2014
\textsl{injectiveness} of introduction rules, i.e., that whenever two
2015
objects were built using the same introduction rule, then this rule
2016
should have been applied to the same element. This can be stated
2017
formally using the propositional equality:
2020
Theorem inj : {\prodsym} n m, S n = S m {\arrow} n = m.
2024
\noindent This theorem is just a corollary of a lemma about the
2025
predecessor function:
2028
Lemma inj_pred : {\prodsym} n m, n = m {\arrow} pred n = pred m.
2035
\noindent Once this lemma is proven, the theorem follows directly
2038
intros n m eq_Sn_Sm.
2039
apply inj_pred with (n:= S n) (m := S m); assumption.
2043
This proof method is implemented by the tactic \texttt{injection}
2044
\refmancite{Section \ref{injection}}. This tactic is applied to
2045
a term $t$ of type ``~$c\;{t_1}\;\dots\;t_n = c\;t'_1\;\dots\;t'_n$~'', where $c$ is some constructor of
2046
an inductive type. The tactic \texttt{injection} is applied as deep as
2047
possible to derive the equality of all pairs of subterms of $t_i$ and $t'_i$
2048
placed in the same position. All these equalities are put as antecedents
2049
of the current goal.
2053
Like \texttt{discriminate}, the tactic \citecoq{injection}
2054
can be also applied if $x$ does not
2055
occur in a direct sub-term, but somewhere deeper inside it. Its
2056
application may leave some trivial goals that can be easily solved
2057
using the tactic \texttt{trivial}.
2061
Lemma list_inject : {\prodsym} (A:Type)(a b :A)(l l':list A),
2062
a :: b :: l = b :: a :: l' {\arrow} a = b {\coqand} l = l'.
2064
intros A a b l l' e.
2068
e : a :: b :: l = b :: a :: l'
2069
============================
2070
a = b {\coqand} l = l'
2074
============================
2075
l = l' {\arrow} b = a {\arrow} a = b {\arrow} a = b {\coqand} l = l'
2081
\subsection{Inversion Techniques}\label{inversion}
2083
In section \ref{DependentCase}, we motivated the rule of dependent case
2084
analysis as a way of internalizing the informal equalities $n=O$ and
2085
$n=\SUCC\;p$ associated to each case. This internalisation
2086
consisted in instantiating $n$ with the corresponding term in the type
2087
of each branch. However, sometimes it could be better to internalise
2088
these equalities as extra hypotheses --for example, in order to use
2089
the tactics \texttt{rewrite}, \texttt{discriminate} or
2090
\texttt{injection} presented in the previous sections. This is
2091
frequently the case when the element analysed is denoted by a term
2092
which is not a variable, or when it is an object of a particular
2093
instance of a recursive family of types. Consider for example the
2097
Theorem not_le_Sn_0 : {\prodsym} n:nat, ~ (S n {\coqle} 0).
2100
\noindent Intuitively, this theorem should follow by case analysis on
2101
the hypothesis $H:(S\;n\;\leq\;\Z)$, because no introduction rule allows
2102
to instantiate the arguments of \citecoq{le} with respectively a successor
2103
and zero. However, there
2104
is no way of capturing this with the typing rule for case analysis
2105
presented in section \ref{Introduction}, because it does not take into
2106
account what particular instance of the family the type of $H$ is.
2110
red; intros n H; case H.
2115
============================
2119
{\prodsym} m : nat, S n {\coqle} m {\arrow} False
2124
\noindent What is necessary here is to make available the equalities
2125
``~$\SUCC\;n = \Z$~'' and ``~$\SUCC\;m = \Z$~''
2126
as extra hypotheses of the
2127
branches, so that the goal can be solved using the
2128
\texttt{Discriminate} tactic. In order to obtain the desired
2129
equalities as hypotheses, let us prove an auxiliary lemma, that our
2130
theorem is a corollary of:
2133
Lemma not_le_Sn_0_with_constraints :
2134
{\prodsym} n p , S n {\coqle} p {\arrow} p = 0 {\arrow} False.
2136
intros n p H; case H .
2143
============================
2144
S n = 0 {\arrow} False
2147
{\prodsym} m : nat, S n {\coqle} m {\arrow} S m = 0 {\arrow} False
2149
intros;discriminate.
2150
intros;discriminate.
2153
\noindent Our main theorem can now be solved by an application of this lemma:
2162
============================
2163
S n = 0 {\arrow} False
2166
{\prodsym} m : nat, S n {\coqle} m {\arrow} S m = 0 {\arrow} False
2168
eapply not_le_Sn_0_with_constraints; eauto.
2173
The general method to address such situations consists in changing the
2174
goal to be proven into an implication, introducing as preconditions
2175
the equalities needed to eliminate the cases that make no
2176
sense. This proof technique is implemented by the tactic
2177
\texttt{inversion} \refmancite{Section \ref{Inversion}}. In order
2178
to prove a goal $G\;\vec{q}$ from an object of type $R\;\vec{t}$,
2179
this tactic automatically generates a lemma $\forall, \vec{x}.
2180
(R\;\vec{x}) \rightarrow \vec{x}=\vec{t}\rightarrow \vec{B}\rightarrow
2181
(G\;\vec{q})$, where the list of propositions $\vec{B}$ correspond to
2182
the subgoals that cannot be directly proven using
2183
\texttt{discriminate}. This lemma can either be saved for later
2184
use, or generated interactively. In this latter case, the subgoals
2185
yielded by the tactic are the hypotheses $\vec{B}$ of the lemma. If the
2186
lemma has been stored, then the tactic \linebreak
2187
``~\citecoq{inversion \dots using \dots}~'' can be
2190
Let us show both techniques on our previous example:
2192
\subsubsection{Interactive mode}
2195
Theorem not_le_Sn_0' : {\prodsym} n:nat, ~ (S n {\coqle} 0).
2197
red; intros n H ; inversion H.
2202
\subsubsection{Static mode}
2206
Derive Inversion le_Sn_0_inv with ({\prodsym} n :nat, S n {\coqle} 0).
2207
Theorem le_Sn_0'' : {\prodsym} n p : nat, ~ S n {\coqle} 0 .
2210
inversion H using le_Sn_0_inv.
2215
In the example above, all the cases are solved using discriminate, so
2216
there remains no subgoal to be proven (i.e. the list $\vec{B}$ is
2217
empty). Let us present a second example, where this list is not empty:
2221
TTheorem le_reverse_rules :
2222
{\prodsym} n m:nat, n {\coqle} m {\arrow}
2224
{\exsym} p, n {\coqle} p {\coqand} m = S p.
2226
intros n m H; inversion H.
2237
============================
2238
m = m {\coqor} ({\exsym} p : nat, m {\coqle} p {\coqand} m = S p)
2241
n = S m0 {\coqor} ({\exsym} p : nat, n {\coqle} p {\coqand} S m0 = S p)
2244
right; exists m0; split; trivial.
2249
This example shows how this tactic can be used to ``reverse'' the
2250
introduction rules of a recursive type, deriving the possible premises
2251
that could lead to prove a given instance of the predicate. This is
2252
why these tactics are called \texttt{inversion} tactics: they go back
2253
from conclusions to premises.
2255
The hypotheses corresponding to the propositional equalities are not
2256
needed in this example, since the tactic does the necessary rewriting
2257
to solve the subgoals. When the equalities are no longer needed after
2258
the inversion, it is better to use the tactic
2259
\texttt{Inversion\_clear}. This variant of the tactic clears from the
2260
context all the equalities introduced.
2264
intros n m H; inversion_clear H.
2270
============================
2271
m = m {\coqor} ({\exsym} p : nat, m {\coqle} p {\coqand} m = S p)
2279
============================
2280
n = S m0 {\coqor} ({\exsym} p : nat, n {\coqle} p {\coqand} S m0 = S p)
2282
right; exists m0; split; trivial.
2287
%This proof technique works in most of the cases, but not always. In
2288
%particular, it could not if the list $\vec{t}$ contains a term $t_j$
2289
%whose type $T$ depends on a previous term $t_i$, with $i<j$. Remark
2290
%that if this is the case, the propositional equality $x_j=t_j$ is not
2291
%well-typed, since $x_j:T(x_i)$ but $t_j:T(t_i)$, and both types are
2292
%not convertible (otherwise, the problem could be solved using the
2293
%tactic \texttt{Case}).
2298
Consider the following language of arithmetic expression, and
2299
its operational semantics, described by a set of rewriting rules.
2300
%\textbf{J'ai enlev� une r�gle de commutativit� de l'addition qui
2301
%me paraissait bizarre du point de vue de la s�mantique op�rationnelle}
2304
Inductive ArithExp : Set :=
2306
| Succ : ArithExp {\arrow} ArithExp
2307
| Plus : ArithExp {\arrow} ArithExp {\arrow} ArithExp.
2309
Inductive RewriteRel : ArithExp {\arrow} ArithExp {\arrow} Prop :=
2310
| RewSucc : {\prodsym} e1 e2 :ArithExp,
2311
RewriteRel e1 e2 {\arrow}
2312
RewriteRel (Succ e1) (Succ e2)
2313
| RewPlus0 : {\prodsym} e:ArithExp,
2314
RewriteRel (Plus Zero e) e
2315
| RewPlusS : {\prodsym} e1 e2:ArithExp,
2316
RewriteRel e1 e2 {\arrow}
2317
RewriteRel (Plus (Succ e1) e2)
2318
(Succ (Plus e1 e2)).
2322
\item Prove that \texttt{Zero} cannot be rewritten any further.
2323
\item Prove that an expression of the form ``~$\texttt{Succ}\;e$~'' is always
2325
into an expression of the same form.
2329
%Theorem zeroNotCompute : (e:ArithExp)~(RewriteRel Zero e).
2337
% (RewriteRel (Succ e1) e2)\arrow{}(EX e3 : ArithExp | e2=(Succ e3)).
2340
%Exists e3;Reflexivity.
2344
\section{Inductive Types and Structural Induction}
2345
\label{StructuralInduction}
2347
Elements of inductive types are well-founded with
2348
respect to the structural order induced by the constructors of the
2349
type. In addition to case analysis, this extra hypothesis about
2350
well-foundedness justifies a stronger elimination rule for them, called
2351
\textsl{structural induction}. This form of elimination consists in
2352
defining a value ``~$f\;x$~'' from some element $x$ of the inductive type
2353
$I$, assuming that values have been already associated in the same way
2354
to the sub-parts of $x$ of type $I$.
2357
Definitions by structural induction are expressed through the
2358
\texttt{Fixpoint} command \refmancite{Section
2359
\ref{Fixpoint}}. This command is quite close to the
2360
\texttt{let-rec} construction of functional programming languages.
2361
For example, the following definition introduces the addition of two
2362
natural numbers (already defined in the Standard Library:)
2365
Fixpoint plus (n p:nat) \{struct n\} : nat :=
2368
| S m {\funarrow} S (plus m p)
2372
The definition is by structural induction on the first argument of the
2373
function. This is indicated by the ``~\citecoq{\{struct n\}}~''
2374
directive in the function's header\footnote{This directive is optional
2375
in the case of a function of a single argument}.
2377
order to be accepted, the definition must satisfy a syntactical
2378
condition, called the \textsl{guardedness condition}. Roughly
2379
speaking, this condition constrains the arguments of a recursive call
2380
to be pattern variables, issued from a case analysis of the formal
2381
argument of the function pointed by the \texttt{struct} directive.
2383
function \texttt{plus}, the argument \texttt{m} in the recursive call is a
2384
pattern variable issued from a case analysis of \texttt{n}. Therefore, the
2385
definition is accepted.
2387
Notice that we could have defined the addition with structural induction
2388
on its second argument:
2390
Fixpoint plus' (n p:nat) \{struct p\} : nat :=
2393
| S q {\funarrow} S (plus' n q)
2397
%This notation is useful when defining a function whose decreasing
2398
%argument has a dependent type. As an example, consider the following
2399
%recursivly defined proof of the theorem
2400
%$(n,m:\texttt{nat})n<m \rightarrow (S\;n)<(S\;m)$:
2402
%Fixpoint lt_n_S [n,m:nat;p:(lt n m)] : (lt (S n) (S m)) :=
2403
% <[n0:nat](lt (S n) (S n0))>
2405
% lt_intro1 {\funarrow} (lt_intro1 (S n))
2406
% | (lt_intro2 m1 p2) {\funarrow} (lt_intro2 (S n) (S m1) (lt_n_S n m1 p2))
2410
%The guardedness condition must be satisfied only by the last argument
2411
%of the enclosed list. For example, the following declaration is an
2412
%alternative way of defining addition:
2416
%Fixpoint add [n:nat] : nat\arrow{}nat :=
2418
% O {\funarrow} [x:nat]x
2419
% | (S m) {\funarrow} [x:nat](add m (S x))
2423
In the following definition of addition,
2424
the second argument of \verb@plus''@ grows at each
2425
recursive call. However, as the first one always decreases, the
2426
definition is sound.
2428
Fixpoint plus'' (n p:nat) \{struct n\} : nat :=
2431
| S m {\funarrow} plus'' m (S p)
2435
Moreover, the argument in the recursive call
2436
could be a deeper component of $n$. This is the case in the following
2437
definition of a boolean function determining whether a number is even
2441
Fixpoint even_test (n:nat) : bool :=
2443
with 0 {\funarrow} true
2444
| 1 {\funarrow} false
2445
| S (S p) {\funarrow} even_test p
2449
Mutually dependent definitions by structural induction are also
2450
allowed. For example, the previous function \textsl{even} could alternatively
2451
be defined using an auxiliary function \textsl{odd}:
2458
Fixpoint even_test (n:nat) : bool :=
2461
| 0 {\funarrow} true
2462
| S p {\funarrow} odd_test p
2464
with odd_test (n:nat) : bool :=
2467
| 0 {\funarrow} false
2468
| S p {\funarrow} even_test p
2473
%Define a function by structural induction that computes the number of
2474
%nodes of a tree structure defined in page \pageref{Forest}.
2477
Definitions by structural induction are computed
2478
only when they are applied, and the decreasing argument
2479
is a term having a constructor at the head. We can check this using
2480
the \texttt{Eval} command, which computes the normal form of a well
2484
Eval simpl in even_test.
2489
Eval simpl in (fun x : nat {\funarrow} even x).
2491
= fun x : nat {\funarrow} even x
2494
Eval simpl in (fun x : nat => plus 5 x).
2496
= fun x : nat {\funarrow} S (S (S (S (S x))))
2499
Eval simpl in (fun x : nat {\funarrow} even_test (plus 5 x)).
2501
= fun x : nat {\funarrow} odd_test x
2504
Eval simpl in (fun x : nat {\funarrow} even_test (plus x 5)).
2506
= fun x : nat {\funarrow} even_test (x + 5)
2512
%Prove that the second definition of even satisfies the following
2515
%Theorem unfold_even :
2517
% (even x)= (Cases x of
2518
% O {\funarrow} true
2519
% | (S O) {\funarrow} false
2520
% | (S (S m)) {\funarrow} (even m)
2525
\subsection{Proofs by Structural Induction}
2527
The principle of structural induction can be also used in order to
2528
define proofs, that is, to prove theorems. Let us call an
2529
\textsl{elimination combinator} any function that, given a predicate
2530
$P$, defines a proof of ``~$P\;x$~'' by structural induction on $x$. In
2531
{\coq}, the principle of proof by induction on natural numbers is a
2532
particular case of an elimination combinator. The definition of this
2533
combinator depends on three general parameters: the predicate to be
2534
proven, the base case, and the inductive step:
2537
Section Principle_of_Induction.
2538
Variable P : nat {\arrow} Prop.
2539
Hypothesis base_case : P 0.
2540
Hypothesis inductive_step : {\prodsym} n:nat, P n {\arrow} P (S n).
2541
Fixpoint nat_ind (n:nat) : (P n) :=
2542
match n return P n with
2543
| 0 {\funarrow} base_case
2544
| S m {\funarrow} inductive_step m (nat_ind m)
2547
End Principle_of_Induction.
2550
As this proof principle is used very often, {\coq} automatically generates it
2551
when an inductive type is introduced. Similar principles
2552
\texttt{nat\_rec} and \texttt{nat\_rect} for defining objects in the
2553
universes $\Set$ and $\Type$ are also automatically generated
2554
\footnote{In fact, whenever possible, {\coq} generates the
2555
principle \texttt{$I$\_rect}, then derives from it the
2556
weaker principles \texttt{$I$\_ind} and \texttt{$I$\_rec}.
2557
If some principle has to be defined by hand, the user may try
2558
to build \texttt{$I$\_rect} (if possible). Thanks to {\coq}'s conversion
2559
rule, this principle can be used directly to build proofs and/or
2561
command \texttt{Scheme} \refmancite{Section \ref{Scheme}} can be
2562
used to generate an elimination combinator from certain parameters,
2563
like the universe that the defined objects must inhabit, whether the
2564
case analysis in the definitions must be dependent or not, etc. For
2565
example, it can be used to generate an elimination combinator for
2566
reasoning on even natural numbers from the mutually dependent
2567
predicates introduced in page \pageref{Even}. We do not display the
2568
combinators here by lack of space, but you can see them using the
2569
\texttt{Print} command.
2572
Scheme Even_induction := Minimality for even Sort Prop
2573
with Odd_induction := Minimality for odd Sort Prop.
2577
Theorem even_plus_four : {\prodsym} n:nat, even n {\arrow} even (4+n).
2580
elim H using Even_induction with (P0 := fun n {\funarrow} odd (4+n));
2581
simpl;repeat constructor;assumption.
2585
Another example of an elimination combinator is the principle
2586
of double induction on natural numbers, introduced by the following
2590
Section Principle_of_Double_Induction.
2591
Variable P : nat {\arrow} nat {\arrow}Prop.
2592
Hypothesis base_case1 : {\prodsym} m:nat, P 0 m.
2593
Hypothesis base_case2 : {\prodsym} n:nat, P (S n) 0.
2594
Hypothesis inductive_step : {\prodsym} n m:nat, P n m {\arrow}
2597
Fixpoint nat_double_ind (n m:nat)\{struct n\} : P n m :=
2598
match n, m return P n m with
2599
| 0 , x {\funarrow} base_case1 x
2600
| (S x), 0 {\funarrow} base_case2 x
2601
| (S x), (S y) {\funarrow} inductive_step x y (nat_double_ind x y)
2603
End Principle_of_Double_Induction.
2606
Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Type$,
2607
another combinator \texttt{nat\_double\_rect} for constructing
2608
(certified) programs can be defined in exactly the same way.
2609
This definition is left as an exercise.\label{natdoublerect}
2613
Section Principle_of_Double_Recursion.
2614
Variable P : nat {\arrow} nat {\arrow} Type.
2615
Hypothesis base_case1 : {\prodsym} x:nat, P 0 x.
2616
Hypothesis base_case2 : {\prodsym} x:nat, P (S x) 0.
2617
Hypothesis inductive_step : {\prodsym} n m:nat, P n m {\arrow} P (S n) (S m).
2618
Fixpoint nat_double_rect (n m:nat)\{struct n\} : P n m :=
2619
match n, m return P n m with
2620
0 , x {\funarrow} base_case1 x
2621
| (S x), 0 {\funarrow} base_case2 x
2622
| (S x), (S y) {\funarrow} inductive_step x y (nat_double_rect x y)
2624
End Principle_of_Double_Recursion.
2627
For instance the function computing the minimum of two natural
2628
numbers can be defined in the following way:
2631
Definition min : nat {\arrow} nat {\arrow} nat :=
2632
nat_double_rect (fun (x y:nat) {\funarrow} nat)
2633
(fun (x:nat) {\funarrow} 0)
2634
(fun (y:nat) {\funarrow} 0)
2635
(fun (x y r:nat) {\funarrow} S r).
2636
Eval compute in (min 5 8).
2644
%Define the combinator \texttt{nat\_double\_rec}, and apply it
2645
%to give another definition of \citecoq{le\_lt\_dec} (using the theorems
2646
%of the \texttt{Arith} library).
2649
\subsection{Using Elimination Combinators.}
2650
The tactic \texttt{apply} can be used to apply one of these proof
2651
principles during the development of a proof.
2654
Lemma not_circular : {\prodsym} n:nat, n {\coqdiff} S n.
2657
apply nat_ind with (P:= fun n {\funarrow} n {\coqdiff} S n).
2665
============================
2670
{\prodsym} n0 : nat, n0 {\coqdiff} S n0 {\arrow} S n0 {\coqdiff} S (S n0)
2674
red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
2678
The tactic \texttt{elim} \refmancite{Section \ref{Elim}} is a
2679
refinement of \texttt{apply}, specially designed for the application
2680
of elimination combinators. If $t$ is an object of an inductive type
2681
$I$, then ``~\citecoq{elim $t$}~'' tries to find an abstraction $P$ of the
2682
current goal $G$ such that $(P\;t)\equiv G$. Then it solves the goal
2683
applying ``~$I\texttt{\_ind}\;P$~'', where $I$\texttt{\_ind} is the
2684
combinator associated to $I$. The different cases of the induction
2685
then appear as subgoals that remain to be solved.
2686
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}~''.
2688
The option ``~\citecoq{\texttt{elim} $t$ \texttt{using} $C$}~''
2690
derived combinator $C$ instead of the default one. Consider the
2691
following theorem, stating that equality is decidable on natural
2696
Lemma eq_nat_dec : {\prodsym} n p:nat, \{n=p\}+\{n {\coqdiff} p\}.
2701
Let us prove this theorem using the combinator \texttt{nat\_double\_rect}
2702
of section~\ref{natdoublerect}. The example also illustrates how
2703
\texttt{elim} may sometimes fail in finding a suitable abstraction $P$
2704
of the goal. Note that if ``~\texttt{elim n}~''
2705
is used directly on the
2706
goal, the result is not the expected one.
2712
elim n using nat_double_rect.
2718
============================
2719
{\prodsym} x : nat, \{x = p\} + \{x {\coqdiff} p\}
2722
nat {\arrow} \{0 = p\} + \{0 {\coqdiff} p\}
2725
nat {\arrow} {\prodsym} m : nat, \{m = p\} + \{m {\coqdiff} p\} {\arrow} \{S m = p\} + \{S m {\coqdiff} p\}
2731
The four sub-goals obtained do not correspond to the premises that
2732
would be expected for the principle \texttt{nat\_double\_rec}. The
2733
problem comes from the fact that
2734
this principle for eliminating $n$
2735
has a universally quantified formula as conclusion, which confuses
2736
\texttt{elim} about the right way of abstracting the goal.
2738
%In effect, let us consider the type of the goal before the call to
2739
%\citecoq{elim}: ``~\citecoq{\{n = p\} + \{n {\coqdiff} p\}}~''.
2741
%Among all the abstractions that can be built by ``~\citecoq{elim n}~''
2742
%let us consider this one
2743
%$P=$\citecoq{fun n :nat {\funarrow} fun q : nat {\funarrow} {\{q= p\} + \{q {\coqdiff} p\}}}.
2744
%It is easy to verify that
2745
%$P$ has type \citecoq{nat {\arrow} nat {\arrow} Set}, and that, if some
2746
%$q:\citecoq{nat}$ is given, then $P\;q\;$ matches the current goal.
2747
%Then applying \citecoq{nat\_double\_rec} with $P$ generates
2748
%four goals, corresponding to
2754
in this case the abstraction must be explicited using the tactic
2755
\texttt{pattern}. Once the right abstraction is provided, the rest of
2756
the proof is immediate:
2764
============================
2765
(fun n0 n1 : nat {\funarrow} \{n1 = n0\} + \{n1 {\coqdiff} n0\}) p n
2767
elim n using nat_double_rec.
2773
============================
2774
{\prodsym} x : nat, \{x = 0\} + \{x {\coqdiff} 0\}
2777
{\prodsym} x : nat, \{0 = S x\} + \{0 {\coqdiff} S x\}
2779
{\prodsym} n0 m : nat, \{m = n0\} + \{m {\coqdiff} n0\} {\arrow} \{S m = S n0\} + \{S m {\coqdiff} S n0\}
2784
intros n0 m H; case H.
2785
intro eq; rewrite eq ; auto.
2786
intro neg; right; red ; injection 1; auto.
2791
Notice that the tactic ``~\texttt{decide equality}~''
2792
\refmancite{Section\ref{DecideEquality}} generalises the proof
2793
above to a large class of inductive types. It can be used for proving
2794
a proposition of the form
2795
$\forall\,(x,y:R),\{x=y\}+\{x{\coqdiff}y\}$, where $R$ is an inductive datatype
2796
all whose constructors take informative arguments ---like for example
2800
Definition eq_nat_dec' : {\prodsym} n p:nat, \{n=p\} + \{n{\coqdiff}p\}.
2807
\item Define a recursive function \emph{nat2itree}
2808
mapping any natural number $n$ into an infinitely branching
2810
\item Provide an elimination combinator for these trees.
2811
\item Prove that the relation \citecoq{itree\_le} is a preorder
2812
(i.e. reflexive and transitive).
2816
\begin{exercise} \label{zeroton}
2817
Define the type of lists, and a predicate ``being an ordered list''
2818
using an inductive family. Then, define the function
2819
$(from\;n)=0::1\;\ldots\; n::\texttt{nil}$ and prove that it always generates an
2824
Prove that \citecoq{le' n p} and \citecoq{n $\leq$ p} are logically equivalent
2825
for all n and p. (\citecoq{le'} is defined in section \ref{parameterstuff}).
2829
\subsection{Well-founded Recursion}
2830
\label{WellFoundedRecursion}
2832
Structural induction is a strong elimination rule for inductive types.
2833
This method can be used to define any function whose termination is
2834
based on the well-foundedness of certain order relation $R$ decreasing
2835
at each recursive call. What makes this principle so strong is the
2836
possibility of reasoning by structural induction on the proof that
2837
certain $R$ is well-founded. In order to illustrate this we have
2838
first to introduce the predicate of accessibility.
2843
Inductive Acc (A : Type) (R : A {\arrow} A {\arrow} Prop) (x:A) : Prop :=
2844
Acc_intro : ({\prodsym} y : A, R y x {\arrow} Acc R y) {\arrow} Acc R x
2845
For Acc: Argument A is implicit
2846
For Acc_intro: Arguments A, R are implicit
2851
\noindent This inductive predicate characterizes those elements $x$ of
2852
$A$ such that any descending $R$-chain $\ldots x_2\;R\;x_1\;R\;x$
2853
starting from $x$ is finite. A well-founded relation is a relation
2854
such that all the elements of $A$ are accessible.
2855
\emph{Notice the use of parameter $x$ (see Section~\ref{parameterstuff}, page
2856
\pageref{parameterstuff}).}
2858
Consider now the problem of representing in {\coq} the following ML
2859
function $\textsl{div}(x,y)$ on natural numbers, which computes
2860
$\lceil\frac{x}{y}\rceil$ if $y>0$ and yields $x$ otherwise.
2865
else if y = 0 then x
2866
else (div (x-y) y)+1;;
2870
The equality test on natural numbers can be represented as the
2871
function \textsl{eq\_nat\_dec} defined page \pageref{iseqpage}. Giving $x$ and
2872
$y$, this function yields either the value $(\textsl{left}\;p)$ if
2873
there exists a proof $p:x=y$, or the value $(\textsl{right}\;q)$ if
2874
there exists $q:a\not = b$. The subtraction function is already
2875
defined in the library \citecoq{Minus}.
2877
Hence, direct translation of the ML function \textsl{div} would be:
2880
Require Import Minus.
2882
Fixpoint div (x y:nat)\{struct x\}: nat :=
2885
else if eq_nat_dec y 0
2887
else S (div (x-y) y).
2890
Recursive definition of div is ill-formed.
2892
div : nat {\arrow} nat {\arrow} nat
2898
Recursive call to div has principal argument equal to
2900
instead of a subterm of x
2904
The program \texttt{div} is rejected by {\coq} because it does not verify
2905
the syntactical condition to ensure termination. In particular, the
2906
argument of the recursive call is not a pattern variable issued from a
2907
case analysis on $x$.
2908
We would have the same problem if we had the directive
2909
``~\citecoq{\{struct y\}}~'' instead of ``~\citecoq{\{struct x\}}~''.
2910
However, we know that this program always
2911
stops. One way to justify its termination is to define it by
2912
structural induction on a proof that $x$ is accessible trough the
2913
relation $<$. Notice that any natural number $x$ is accessible
2914
for this relation. In order to do this, it is first necessary to prove
2915
some auxiliary lemmas, justifying that the first argument of
2916
\texttt{div} decreases at each recursive call.
2919
Lemma minus_smaller_S : {\prodsym} x y:nat, x - y < S x.
2921
intros x y; pattern y, x;
2922
elim x using nat_double_ind.
2923
destruct x0; auto with arith.
2924
simpl; auto with arith.
2925
simpl; auto with arith.
2929
Lemma minus_smaller_positive :
2930
{\prodsym} x y:nat, x {\coqdiff}0 {\arrow} y {\coqdiff} 0 {\arrow} x - y < x.
2932
destruct x; destruct y;
2933
( simpl;intros; apply minus_smaller ||
2934
intros; absurd (0=0); auto).
2938
\noindent The last two lemmas are necessary to prove that for any pair
2939
of positive natural numbers $x$ and $y$, if $x$ is accessible with
2940
respect to \citecoq{lt}, then so is $x-y$.
2943
Definition minus_decrease : {\prodsym} x y:nat, Acc lt x {\arrow}
2944
x {\coqdiff} 0 {\arrow}
2945
y {\coqdiff} 0 {\arrow}
2948
intros x y H; case H.
2949
intros Hz posz posy.
2950
apply Hz; apply minus_smaller_positive; assumption.
2954
Let us take a look at the proof of the lemma \textsl{minus\_decrease}, since
2955
the way in which it has been proven is crucial for what follows.
2957
Print minus_decrease.
2960
fun (x y : nat) (H : Acc lt x) {\funarrow}
2961
match H in (Acc _ y0) return (y0 {\coqdiff} 0 {\arrow} y {\coqdiff} 0 {\arrow} Acc lt (y0 - y)) with
2962
| Acc_intro z Hz {\funarrow}
2963
fun (posz : z {\coqdiff} 0) (posy : y {\coqdiff} 0) {\funarrow}
2964
Hz (z - y) (minus_smaller_positive z y posz posy)
2966
: {\prodsym} x y : nat, Acc lt x {\arrow} x {\coqdiff} 0 {\arrow} y {\coqdiff} 0 {\arrow} Acc lt (x - y)
2969
\noindent Notice that the function call
2970
$(\texttt{minus\_decrease}\;n\;m\;H)$
2971
indeed yields an accessibility proof that is \textsl{structurally
2972
smaller} than its argument $H$, because it is (an application of) its
2973
recursive component $Hz$. This enables to justify the following
2974
definition of \textsl{div\_aux}:
2977
Definition div_aux (x y:nat)(H: Acc lt x):nat.
2980
refine (if eq_nat_dec x 0
2982
else if eq_nat_dec y 0
2984
else div_aux (x-y) y _).
2986
div_aux : {\prodsym} x : nat, nat {\arrow} Acc lt x {\arrow} nat
2992
============================
2996
apply (minus_decrease x y H);auto.
3000
The main division function is easily defined, using the theorem
3001
\citecoq{lt\_wf} of the library \citecoq{Wf\_nat}. This theorem asserts that
3002
\citecoq{nat} is well founded w.r.t. \citecoq{lt}, thus any natural number
3005
Definition div x y := div_aux x y (lt_wf x).
3008
Let us explain the proof above. In the definition of \citecoq{div\_aux},
3009
what decreases is not $x$ but the \textsl{proof} of the accessibility
3010
of $x$. The tactic ``~\texttt{fix 3}~'' is used to indicate that the proof
3011
proceeds by structural induction on the third argument of the theorem
3012
--that is, on the accessibility proof. It also introduces a new
3013
hypothesis in the context, named as the current theorem, and with the
3014
same type as the goal. Then, the proof is refined with an incomplete
3015
proof term, containing a hole \texttt{\_}. This hole corresponds to the proof
3016
of accessibility for $x-y$, and is filled up with the (smaller!)
3017
accessibility proof provided by the function \texttt{minus\_decrease}.
3020
\noindent Let us take a look to the term \textsl{div\_aux} defined:
3027
(fix div_aux (x y : nat) (H : Acc lt x) \{struct H\} : nat :=
3028
match eq_nat_dec x 0 with
3029
| left _ {\funarrow} 0
3030
| right _ {\funarrow}
3031
match eq_nat_dec y 0 with
3032
| left _ {\funarrow} y
3033
| right _0 {\funarrow} div_aux (x - y) y (minus_decrease x y H _ _0)
3036
: {\prodsym} x : nat, nat {\arrow} Acc lt x {\arrow} nat
3040
If the non-informative parts from this proof --that is, the
3041
accessibility proof-- are erased, then we obtain exactly the program
3042
that we were looking for.
3055
let rec div_aux x y =
3056
match eq_nat_dec x O with
3059
(match eq_nat_dec y O with
3061
| Right {\arrow} div_aux (minus x y) y)
3064
This methodology enables the representation
3065
of any program whose termination can be proved in {\coq}. Once the
3066
expected properties from this program have been verified, the
3067
justification of its termination can be thrown away, keeping just the
3068
desired computational behavior for it.
3070
\section{A case study in dependent elimination}\label{CaseStudy}
3072
Dependent types are very expressive, but ignoring some useful
3073
techniques can cause some problems to the beginner.
3074
Let us consider again the type of vectors (see section~\ref{vectors}).
3075
We want to prove a quite trivial property: the only value of type
3076
``~\citecoq{vector A 0}~'' is ``~\citecoq{Vnil $A$}~''.
3078
Our first naive attempt leads to a \emph{cul-de-sac}.
3080
Lemma vector0_is_vnil :
3081
{\prodsym} (A:Type)(v:vector A 0), v = Vnil A.
3083
intros A v;inversion v.
3089
============================
3095
Another attempt is to do a case analysis on a vector of any length
3096
$n$, under an explicit hypothesis $n=0$. The tactic
3097
\texttt{discriminate} will help us to get rid of the case
3099
Unfortunately, even the statement of our lemma is refused!
3102
Lemma vector0_is_vnil_aux :
3103
{\prodsym} (A:Type)(n:nat)(v:vector A n), n = 0 {\arrow} v = Vnil A.
3106
Error: In environment
3111
The term "Vnil A" has type "vector A 0" while it is expected to have type
3115
In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill typed,
3116
because the type ``~\citecoq{vector A n}~'' is not \emph{convertible}
3117
with ``~\citecoq{vector A 0}~''.
3119
This problem can be solved if we consider the heterogeneous
3120
equality \citecoq{JMeq} \cite{conor:motive}
3121
which allows us to consider terms of different types, even if this
3122
equality can only be proven for terms in the same type.
3123
The axiom \citecoq{JMeq\_eq}, from the library \citecoq{JMeq} allows us to convert a
3124
heterogeneous equality to a standard one.
3127
Lemma vector0_is_vnil_aux :
3128
{\prodsym} (A:Type)(n:nat)(v:vector A n),
3129
n= 0 {\arrow} JMeq v (Vnil A).
3133
intro; discriminate.
3137
Our property of vectors of null length can be easily proven:
3140
Lemma vector0_is_vnil : {\prodsym} (A:Type)(v:vector A 0), v = Vnil A.
3141
intros a v;apply JMeq_eq.
3142
apply vector0_is_vnil_aux.
3147
It is interesting to look at another proof of
3148
\citecoq{vector0\_is\_vnil}, which illustrates a technique developed
3149
and used by various people (consult in the \emph{Coq-club} mailing
3150
list archive the contributions by Yves Bertot, Pierre Letouzey, Laurent Th�ry,
3151
Jean Duprat, and Nicolas Magaud, Venanzio Capretta and Conor McBride).
3152
This technique is also used for unfolding infinite list definitions
3153
(see chapter13 of~\cite{coqart}).
3154
Notice that this definition does not rely on any axiom (\emph{e.g.} \texttt{JMeq\_eq}).
3156
We first give a new definition of the identity on vectors. Before that,
3157
we make the use of constructors and selectors lighter thanks to
3158
the implicit arguments feature:
3161
Implicit Arguments Vcons [A n].
3162
Implicit Arguments Vnil [A].
3163
Implicit Arguments Vhead [A n].
3164
Implicit Arguments Vtail [A n].
3166
Definition Vid : {\prodsym} (A : Type)(n:nat), vector A n {\arrow} vector A n.
3168
destruct n; intro v.
3170
exact (Vcons (Vhead v) (Vtail v)).
3175
Then we prove that \citecoq{Vid} is the identity on vectors:
3178
Lemma Vid_eq : {\prodsym} (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
3184
============================
3188
Vcons a v = Vid A (S n) (Vcons a v)
3195
Why defining a new identity function on vectors? The following
3196
dialogue shows that \citecoq{Vid} has some interesting computational
3200
Eval simpl in (fun (A:Type)(v:vector A 0) {\funarrow} (Vid _ _ v)).
3201
\it = fun (A : Type) (_ : vector A 0) {\funarrow} Vnil
3202
: {\prodsym} A : Type, vector A 0 {\arrow} vector A 0
3206
Notice that the plain identity on vectors doesn't convert \citecoq{v}
3207
into \citecoq{Vnil}.
3209
Eval simpl in (fun (A:Type)(v:vector A 0) {\funarrow} v).
3210
\it = fun (A : Type) (v : vector A 0) {\funarrow} v
3211
: {\prodsym} A : Type, vector A 0 {\arrow} vector A 0
3214
Then we prove easily that any vector of length 0 is \citecoq{Vnil}:
3217
Theorem zero_nil : {\prodsym} A (v:vector A 0), v = Vnil.
3220
change (Vnil (A:=A)) with (Vid _ 0 v).
3226
============================
3233
A similar result can be proven about vectors of strictly positive
3234
length\footnote{As for \citecoq{Vid} and \citecoq{Vid\_eq}, this definition
3235
is from Jean Duprat.}.
3241
{\prodsym} (A : Type) (n : nat) (v : vector A (S n)),
3242
v = Vcons (Vhead v) (Vtail v).
3245
change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
3252
============================
3260
Both lemmas: \citecoq{zero\_nil} and \citecoq{decomp},
3261
can be used to easily derive a double recursion principle
3262
on vectors of same length:
3266
Definition vector_double_rect :
3267
{\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
3268
P 0 Vnil Vnil {\arrow}
3269
({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
3270
P (S n) (Vcons a v1) (Vcons b v2)) {\arrow}
3271
{\prodsym} n (v1 v2 : vector A n), P n v1 v2.
3273
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
3275
intros v1 v2; rewrite (decomp _ _ v1);rewrite (decomp _ _ v2).
3280
Notice that, due to the conversion rule of {\coq}'s type system,
3281
this function can be used directly with \citecoq{Prop} or \citecoq{Type}
3282
instead of type (thus it is useless to build
3283
\citecoq{vector\_double\_ind} and \citecoq{vector\_double\_rec}) from scratch.
3285
We finish this example with showing how to define the bitwise
3286
\emph{or} on boolean vectors of the same length,
3287
and proving a little property about this
3291
Definition bitwise_or n v1 v2 : vector bool n :=
3294
(fun n v1 v2 {\funarrow} vector bool n)
3296
(fun n v1 v2 a b r {\funarrow} Vcons (orb a b) r) n v1 v2.
3299
Let us define recursively the $n$-th element of a vector. Notice
3300
that it must be a partial function, in case $n$ is greater or equal
3301
than the length of the vector. Since {\coq} only considers total
3302
functions, the function returns a value in an \emph{option} type.
3305
Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p)
3309
_ , Vnil {\funarrow} None
3310
| 0 , Vcons b _ _ {\funarrow} Some b
3311
| S n', Vcons _ p' v' {\funarrow} vector_nth A n' p' v'
3313
Implicit Arguments vector_nth [A p].
3316
We can now prove --- using the double induction combinator ---
3317
a simple property relying \citecoq{vector\_nth} and \citecoq{bitwise\_or}:
3321
{\prodsym} (n:nat) (v1 v2: vector bool n) i a b,
3322
vector_nth i v1 = Some a {\arrow}
3323
vector_nth i v2 = Some b {\arrow}
3324
vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
3326
intros n v1 v2; pattern n,v1,v2.
3327
apply vector_double_rect.
3329
destruct i; discriminate 1.
3330
destruct i; simpl;auto.
3331
injection 1; injection 2;intros; subst a; subst b; auto.
3336
\section{Co-inductive Types and Non-ending Constructions}
3339
The objects of an inductive type are well-founded with respect to
3340
the constructors of the type. In other words, these objects are built
3341
by applying \emph{a finite number of times} the constructors of the type.
3342
Co-inductive types are obtained by relaxing this condition,
3343
and may contain non-well-founded objects \cite{EG96,EG95a}. An
3344
example of a co-inductive type is the type of infinite
3345
sequences formed with elements of type $A$, also called streams. This
3346
type can be introduced through the following definition:
3349
CoInductive Stream (A: Type) :Type :=
3350
| Cons : A\arrow{}Stream A\arrow{}Stream A.
3353
If we are interested in finite or infinite sequences, we consider the type
3354
of \emph{lazy lists}:
3357
CoInductive LList (A: Type) : Type :=
3359
| LCons : A {\arrow} LList A {\arrow} LList A.
3363
It is also possible to define co-inductive types for the
3364
trees with infinite branches (see Chapter 13 of~\cite{coqart}).
3366
Structural induction is the way of expressing that inductive types
3367
only contain well-founded objects. Hence, this elimination principle
3368
is not valid for co-inductive types, and the only elimination rule for
3369
streams is case analysis. This principle can be used, for example, to
3370
define the destructors \textsl{head} and \textsl{tail}.
3373
Definition head (A:Type)(s : Stream A) :=
3374
match s with Cons a s' {\funarrow} a end.
3376
Definition tail (A : Type)(s : Stream A) :=
3377
match s with Cons a s' {\funarrow} s' end.
3380
Infinite objects are defined by means of (non-ending) methods of
3381
construction, like in lazy functional programming languages. Such
3382
methods can be defined using the \texttt{CoFixpoint} command
3383
\refmancite{Section \ref{CoFixpoint}}. For example, the following
3384
definition introduces the infinite list $[a,a,a,\ldots]$:
3387
CoFixpoint repeat (A:Type)(a:A) : Stream A :=
3392
However, not every co-recursive definition is an admissible method of
3393
construction. Similarly to the case of structural induction, the
3394
definition must verify a \textsl{guardedness} condition to be
3395
accepted. This condition states that any recursive call in the
3396
definition must be protected --i.e, be an argument of-- some
3397
constructor, and only an argument of constructors \cite{EG94a}. The
3398
following definitions are examples of valid methods of construction:
3401
CoFixpoint iterate (A: Type)(f: A {\arrow} A)(a : A) : Stream A:=
3402
Cons a (iterate f (f a)).
3405
(A B:Type)(f: A {\arrow} B)(s : Stream A) : Stream B:=
3406
match s with Cons a tl {\funarrow} Cons (f a) (map f tl) end.
3410
Define two different methods for constructing the stream which
3411
infinitely alternates the values \citecoq{true} and \citecoq{false}.
3414
Using the destructors \texttt{head} and \texttt{tail}, define a function
3415
which takes the n-th element of an infinite stream.
3418
A non-ending method of construction is computed lazily. This means
3419
that its definition is unfolded only when the object that it
3420
introduces is eliminated, that is, when it appears as the argument of
3421
a case expression. We can check this using the command
3425
Eval simpl in (fun (A:Type)(a:A) {\funarrow} repeat a).
3426
\it = fun (A : Type) (a : A) {\funarrow} repeat a
3427
: {\prodsym} A : Type, A {\arrow} Stream A
3429
Eval simpl in (fun (A:Type)(a:A) {\funarrow} head (repeat a)).
3430
\it = fun (A : Type) (a : A) {\funarrow} a
3431
: {\prodsym} A : Type, A {\arrow} A
3435
%Prove the following theorem:
3437
%Theorem expand_repeat : (a:A)(repeat a)=(Cons a (repeat a)).
3439
%Hint: Prove first the streams version of the lemma in exercise
3443
\subsection{Extensional Properties}
3445
Case analysis is also a valid proof principle for infinite
3446
objects. However, this principle is not sufficient to prove
3447
\textsl{extensional} properties, that is, properties concerning the
3448
whole infinite object \cite{EG95a}. A typical example of an
3449
extensional property is the predicate expressing that two streams have
3450
the same elements. In many cases, the minimal reflexive relation $a=b$
3451
that is used as equality for inductive types is too small to capture
3452
equality between streams. Consider for example the streams
3453
$\texttt{iterate}\;f\;(f\;x)$ and
3454
$(\texttt{map}\;f\;(\texttt{iterate}\;f\;x))$. Even though these two streams have
3455
the same elements, no finite expansion of their definitions lead to
3456
equal terms. In other words, in order to deal with extensional
3457
properties, it is necessary to construct infinite proofs. The type of
3458
infinite proofs of equality can be introduced as a co-inductive
3459
predicate, as follows:
3461
CoInductive EqSt (A: Type) : Stream A {\arrow} Stream A {\arrow} Prop :=
3462
eqst : {\prodsym} s1 s2: Stream A,
3463
head s1 = head s2 {\arrow}
3464
EqSt (tail s1) (tail s2) {\arrow}
3468
It is possible to introduce proof principles for reasoning about
3469
infinite objects as combinators defined through
3470
\texttt{CoFixpoint}. However, oppositely to the case of inductive
3471
types, proof principles associated to co-inductive types are not
3472
elimination but \textsl{introduction} combinators. An example of such
3473
a combinator is Park's principle for proving the equality of two
3474
streams, usually called the \textsl{principle of co-induction}. It
3475
states that two streams are equal if they satisfy a
3476
\textit{bisimulation}. A bisimulation is a binary relation $R$ such
3477
that any pair of streams $s_1$ ad $s_2$ satisfying $R$ have equal
3478
heads, and tails also satisfying $R$. This principle is in fact a
3479
method for constructing an infinite proof:
3482
Section Parks_Principle.
3484
Variable R : Stream A {\arrow} Stream A {\arrow} Prop.
3485
Hypothesis bisim1 : {\prodsym} s1 s2:Stream A,
3486
R s1 s2 {\arrow} head s1 = head s2.
3488
Hypothesis bisim2 : {\prodsym} s1 s2:Stream A,
3489
R s1 s2 {\arrow} R (tail s1) (tail s2).
3491
CoFixpoint park_ppl :
3492
{\prodsym} s1 s2:Stream A, R s1 s2 {\arrow} EqSt s1 s2 :=
3493
fun s1 s2 (p : R s1 s2) {\funarrow}
3494
eqst s1 s2 (bisim1 s1 s2 p)
3498
End Parks_Principle.
3501
Let us use the principle of co-induction to prove the extensional
3502
equality mentioned above.
3504
Theorem map_iterate : {\prodsym} (A:Type)(f:A{\arrow}A)(x:A),
3505
EqSt (iterate f (f x))
3506
(map f (iterate f x)).
3510
(R:= fun s1 s2 {\funarrow}
3511
{\exsym} x: A, s1 = iterate f (f x) {\coqand}
3512
s2 = map f (iterate f x)).
3514
intros s1 s2 (x0,(eqs1,eqs2));
3515
rewrite eqs1; rewrite eqs2; reflexivity.
3516
intros s1 s2 (x0,(eqs1,eqs2)).
3517
exists (f x0);split;
3518
[rewrite eqs1|rewrite eqs2]; reflexivity.
3519
exists x;split; reflexivity.
3523
The use of Park's principle is sometimes annoying, because it requires
3524
to find an invariant relation and prove that it is indeed a
3525
bisimulation. In many cases, a shorter proof can be obtained trying
3526
to construct an ad-hoc infinite proof, defined by a guarded
3527
declaration. The tactic ``~``\texttt{Cofix $f$}~'' can be used to do
3528
that. Similarly to the tactic \texttt{fix} indicated in Section
3529
\ref{WellFoundedRecursion}, this tactic introduces an extra hypothesis
3530
$f$ into the context, whose type is the same as the current goal. Note
3531
that the applications of $f$ in the proof \textsl{must be guarded}. In
3532
order to prevent us from doing unguarded calls, we can define a tactic
3533
that always apply a constructor before using $f$ \refmancite{Chapter
3534
\ref{WritingTactics}} :
3537
Ltac infiniteproof f :=
3540
[clear f| simpl; try (apply f; clear f)].
3544
In the example above, this tactic produces a much simpler proof
3545
that the former one:
3548
Theorem map_iterate' : {\prodsym} ((A:Type)f:A{\arrow}A)(x:A),
3549
EqSt (iterate f (f x))
3550
(map f (iterate f x)).
3552
infiniteproof map_iterate'.
3558
Define a co-inductive type $Nat$ containing non-standard
3559
natural numbers --this is, verifying
3561
$$\exists m \in \mbox{\texttt{Nat}}, \forall\, n \in \mbox{\texttt{Nat}}, n<m$$.
3565
Prove that the extensional equality of streams is an equivalence relation
3566
using Park's co-induction principle.
3571
Provide a suitable definition of ``being an ordered list'' for infinite lists
3572
and define a principle for proving that an infinite list is ordered. Apply
3573
this method to the list $[0,1,\ldots ]$. Compare the result with
3574
exercise \ref{zeroton}.
3577
\subsection{About injection, discriminate, and inversion}
3578
Since co-inductive types are closed w.r.t. their constructors,
3579
the techniques shown in Section~\ref{CaseTechniques} work also
3582
Let us consider the type of lazy lists, introduced on page~\pageref{CoInduction}.
3583
The following lemmas are straightforward applications
3584
of \texttt{discriminate} and \citecoq{injection}:
3587
Lemma Lnil_not_Lcons : {\prodsym} (A:Type)(a:A)(l:LList A),
3588
LNil {\coqdiff} (LCons a l).
3590
intros;discriminate.
3593
Lemma injection_demo : {\prodsym} (A:Type)(a b : A)(l l': LList A),
3594
LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
3595
a = b {\coqand} l = l'.
3597
intros A a b l l' e; injection e; auto.
3602
In order to show \citecoq{inversion} at work, let us define
3603
two predicates on lazy lists:
3606
Inductive Finite (A:Type) : LList A {\arrow} Prop :=
3607
| Lnil_fin : Finite (LNil (A:=A))
3608
| Lcons_fin : {\prodsym} a l, Finite l {\arrow} Finite (LCons a l).
3610
CoInductive Infinite (A:Type) : LList A {\arrow} Prop :=
3611
| LCons_inf : {\prodsym} a l, Infinite l {\arrow} Infinite (LCons a l).
3615
First, two easy theorems:
3617
Lemma LNil_not_Infinite : {\prodsym} (A:Type), ~ Infinite (LNil (A:=A)).
3619
intros A H;inversion H.
3622
Lemma Finite_not_Infinite : {\prodsym} (A:Type)(l:LList A),
3623
Finite l {\arrow} ~ Infinite l.
3625
intros A l H; elim H.
3626
apply LNil_not_Infinite.
3627
intros a l0 F0 I0' I1.
3628
case I0'; inversion_clear I1.
3634
On the other hand, the next proof uses the \citecoq{cofix} tactic.
3635
Notice the destructuration of \citecoq{l}, which allows us to
3636
apply the constructor \texttt{LCons\_inf}, thus satisfying
3637
the guard condition:
3639
Lemma Not_Finite_Infinite : {\prodsym} (A:Type)(l:LList A),
3640
~ Finite l {\arrow} Infinite l.
3645
absurd (Finite (LNil (A:=A)));
3654
H : forall (A : Type) (l : LList A), ~ Finite l -> Infinite l
3658
H0 : ~ Finite (LCons a l)
3659
============================
3662
At this point, one must not apply \citecoq{H}! . It would be possible
3663
to solve the current goal by an inversion of ``~\citecoq{Finite (LCons a l)}~'', but, since the guard condition would be violated, the user
3664
would get an error message after typing \citecoq{Qed}.
3665
In order to satisfy the guard condition, we apply the constructor of
3666
\citecoq{Infinite}, \emph{then} apply \citecoq{H}.
3671
red; intro H1;case H0.
3680
The reader is invited to replay this proof and understand each of its steps.
3683
\bibliographystyle{abbrv}
3684
\bibliography{manbiblio,morebib}
added
removed
RecTutorial/RecTutorial.tex
