Mercurial > cpdt > repo

annotate src/GeneralRec.v @ 351:bb1a470c1757

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Well-founded recursion
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 15:12:21 -0400
parents ad315efc3b6b
children ab60b10890ed
rev   line source
adam@350 1 (* Copyright (c) 2006, 2011, Adam Chlipala
adam@350 2 *
adam@350 3 * This work is licensed under a
adam@350 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adam@350 5 * Unported License.
adam@350 6 * The license text is available at:
adam@350 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adam@350 8 *)
adam@350 9
adam@350 10 (* begin hide *)
adam@351 11 Require Import Arith List.
adam@350 12
adam@351 13 Require Import CpdtTactics Coinductive.
adam@350 14
adam@350 15 Set Implicit Arguments.
adam@350 16 (* end hide *)
adam@350 17
adam@350 18
adam@350 19 (** %\chapter{General Recursion}% *)
adam@350 20
adam@351 21 (** Termination of all programs is a crucial property of Gallina. Nonterminating programs introduce logical inconsistency, where any theorem can be proved with an infinite loop. Coq uses a small set of conservative, syntactic criteria to check termination of all recursive definitions. These criteria are insufficient to support the natural encodings of a variety of important programming idioms. Further, since Coq makes it so convenient to encode mathematics computationally, with functional programs, we may find ourselves wanting to employ more complicated recursion in mathematical definitions.
adam@351 22
adam@351 23 What exactly are the conservative criteria that we run up against? For %\emph{%#<i>#recursive#</i>#%}% definitions, recursive calls are only allowed on %\emph{%#<i>#syntactic subterms#</i>#%}% of the original primary argument, a restriction known as %\index{primitive recursion}\emph{%#<i>#primitive recursion#</i>#%}%. In fact, Coq's handling of reflexive inductive types (those defined in terms of functions returning the same type) gives a bit more flexibility than in traditional primitive recursion, but the term is still applied commonly. In the previous chapter, we saw how %\emph{%#<i>#co-recursive#</i>#%}% definitions are checked against a syntactic guardness condition that guarantees productivity.
adam@351 24
adam@351 25 Many natural recursion patterns satisfy neither condition. For instance, there is our simple running example in this chapter, merge sort. We will study three different approaches to more flexible recursion, and the latter two of the approaches will even support definitions that may fail to terminate on certain inputs.
adam@351 26
adam@351 27 Before proceeding, it is important to note that the problem here is not as fundamental as it may appear. The final example of the previous chapter demonstrated what is called a %\index{deep embedding}\emph{%#<i>#deep embedding#</i>#%}% of the syntax and semantics of a programming language. That is, we gave a mathematical definition of a language of programs and their meanings. This language clearly admitted non-termination, and we could think of writing all our sophisticated recursive functions with such explicit syntax types. However, in doing so, we forfeit our chance to take advantage of Coq's very good built-in support for reasoning about Gallina programs. We would rather use a %\index{shallow embedding}\emph{%#<i>#shallow embedding#</i>#%}%, where we model informal constructs by encoding them as normal Gallina programs. Each of the three techniques of this chapter follows that style. *)
adam@351 28
adam@351 29
adam@351 30 (** * Well-Founded Recursion *)
adam@351 31
adam@351 32 (** The essence of terminating recursion is that there are no infinite chains of nested recursive calls. This intuition is commonly mapped to the mathematical idea of a %\index{well-founded relation}\emph{%#<i>#well-founded relation#</i>#%}%, and the associated standard technique in Coq is %\index{well-founded recursion}\emph{%#<i>#well-founded recursion#</i>#%}%. The syntactic-subterm relation that Coq applies by default is well-founded, but many cases demand alternate well-founded relations. To demonstrate, let us see where we get stuck on attempting a standard merge sort implementation. *)
adam@351 33
adam@351 34 Section mergeSort.
adam@351 35 Variable A : Type.
adam@351 36 Variable le : A -> A -> bool.
adam@351 37 (** We have a set equipped with some %``%#"#less-than-or-equal-to#"#%''% test. *)
adam@351 38
adam@351 39 (** A standard function inserts an element into a sorted list, preserving sortedness. *)
adam@351 40
adam@351 41 Fixpoint insert (x : A) (ls : list A) : list A :=
adam@351 42 match ls with
adam@351 43 | nil => x :: nil
adam@351 44 | h :: ls' =>
adam@351 45 if le x h
adam@351 46 then x :: ls
adam@351 47 else h :: insert x ls'
adam@351 48 end.
adam@351 49
adam@351 50 (** We will also need a function to merge two sorted lists. (We use a less efficient implementation than usual, because the more efficient implementation already forces us to think about well-founded recursion, while here we are only interested in setting up the example of merge sort.) *)
adam@351 51
adam@351 52 Fixpoint merge (ls1 ls2 : list A) : list A :=
adam@351 53 match ls1 with
adam@351 54 | nil => ls2
adam@351 55 | h :: ls' => insert h (merge ls' ls2)
adam@351 56 end.
adam@351 57
adam@351 58 (** The last helper function for classic merge sort is the one that follows, to partition a list arbitrarily into two pieces of approximately equal length. *)
adam@351 59
adam@351 60 Fixpoint partition (ls : list A) : list A * list A :=
adam@351 61 match ls with
adam@351 62 | nil => (nil, nil)
adam@351 63 | h :: nil => (h :: nil, nil)
adam@351 64 | h1 :: h2 :: ls' =>
adam@351 65 let (ls1, ls2) := partition ls' in
adam@351 66 (h1 :: ls1, h2 :: ls2)
adam@351 67 end.
adam@351 68
adam@351 69 (** Now, let us try to write the final sorting function, using a natural number %``%#"#[<=]#"#%''% test [leb] from the standard library.
adam@351 70 [[
adam@351 71 Fixpoint mergeSort (ls : list A) : list A :=
adam@351 72 if leb (length ls) 2
adam@351 73 then ls
adam@351 74 else let lss := partition ls in
adam@351 75 merge (mergeSort (fst lss)) (mergeSort (snd lss)).
adam@351 76 ]]
adam@351 77
adam@351 78 <<
adam@351 79 Recursive call to mergeSort has principal argument equal to
adam@351 80 "fst (partition ls)" instead of a subterm of "ls".
adam@351 81 >>
adam@351 82
adam@351 83 The definition is rejected for not following the simple primitive recursion criterion. In particular, it is not apparent that recursive calls to [mergeSort] are syntactic subterms of the original argument [ls]; indeed, they are not, yet we know this is a well-founded recursive definition.
adam@351 84
adam@351 85 To produce an acceptable definition, we need to choose a well-founded relation and prove that [mergeSort] respects it. A good starting point is an examination of how well-foundedness is formalized in the Coq standard library. *)
adam@351 86
adam@351 87 Print well_founded.
adam@351 88 (** %\vspace{-.15in}% [[
adam@351 89 well_founded =
adam@351 90 fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a
adam@351 91 ]]
adam@351 92
adam@351 93 The bulk of the definitional work devolves to the %\index{accessibility relation}\index{Gallina terms!Acc}\emph{%#<i>#accessibility#</i>#%}% relation [Acc], whose definition we may also examine. *)
adam@351 94
adam@351 95 Print Acc.
adam@351 96 (** %\vspace{-.15in}% [[
adam@351 97 Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
adam@351 98 Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
adam@351 99 ]]
adam@351 100
adam@351 101 In prose, an element [x] is accessible for a relation [R] if every element %``%#"#less than#"#%''% [x] according to [R] is also accessible. Since [Acc] is defined inductively, we know that any accessibility proof involves a finite chain of invocations, in a certain sense which we can make formal. Building on last chapter's examples, let us define a co-inductive relation that is closer to the usual informal notion of %``%#"#absence of infinite decreasing chains.#"#%''% *)
adam@351 102
adam@351 103 CoInductive isChain A (R : A -> A -> Prop) : stream A -> Prop :=
adam@351 104 | ChainCons : forall x y s, isChain R (Cons y s)
adam@351 105 -> R y x
adam@351 106 -> isChain R (Cons x (Cons y s)).
adam@351 107
adam@351 108 (** We can now prove that any accessible element cannot be the beginning of any infinite decreasing chain. *)
adam@351 109
adam@351 110 (* begin thide *)
adam@351 111 Lemma noChains' : forall A (R : A -> A -> Prop) x, Acc R x
adam@351 112 -> forall s, ~isChain R (Cons x s).
adam@351 113 induction 1; crush;
adam@351 114 match goal with
adam@351 115 | [ H : isChain _ _ |- _ ] => inversion H; eauto
adam@351 116 end.
adam@351 117 Qed.
adam@351 118
adam@351 119 (** From here, the absence of infinite decreasing chains in well-founded sets is immediate. *)
adam@351 120
adam@351 121 Theorem noChains : forall A (R : A -> A -> Prop), well_founded R
adam@351 122 -> forall s, ~isChain R s.
adam@351 123 destruct s; apply noChains'; auto.
adam@351 124 Qed.
adam@351 125 (* end thide *)
adam@351 126
adam@351 127 (** Absence of infinite decreasing chains implies absence of infinitely nested recursive calls, for any recursive definition that respects the well-founded relation. The [Fix] combinator from the standard library formalizes that intuition: *)
adam@351 128
adam@351 129 Check Fix.
adam@351 130 (** %\vspace{-.15in}%[[
adam@351 131 Fix
adam@351 132 : forall (A : Type) (R : A -> A -> Prop),
adam@351 133 well_founded R ->
adam@351 134 forall P : A -> Type,
adam@351 135 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
adam@351 136 forall x : A, P x
adam@351 137 ]]
adam@351 138
adam@351 139 A call to %\index{Gallina terms!Fix}%[Fix] must present a relation [R] and a proof of its well-foundedness. The next argument, [P], is the possibly dependent range type of the function we build; the domain [A] of [R] is the function's domain. The following argument has this type:
adam@351 140
adam@351 141 [[
adam@351 142 forall x : A, (forall y : A, R y x -> P y) -> P x
adam@351 143 ]]
adam@351 144
adam@351 145 This is an encoding of the function body. The input [x] stands for the function argument, and the next input stands for the function we are defining. Recursive calls are encoded as calls to the second argument, whose type tells us it expects a value [y] and a proof that [y] is %``%#"#less than#"#%''% [x], according to [R]. In this way, we enforce the well-foundedness restriction on recursive calls.
adam@351 146
adam@351 147 The rest of [Fix]'s type tells us that it returns a function of exactly the type we expect, so we are now ready to use it to implement [mergeSort]. Careful readers may have noticed something unusual going on in the type of [Fix], where a program function takes a proof as an argument. Chapter 7 will include much more detail on that style of programming; here we will merely give a taste of what is to come.
adam@351 148
adam@351 149 Before writing [mergeSort], we need to settle on a well-founded relation. The right one for this example is based on lengths of lists. *)
adam@351 150
adam@351 151 Definition lengthOrder (ls1 ls2 : list A) :=
adam@351 152 length ls1 < length ls2.
adam@351 153
adam@351 154 (** We must prove that the relation is truly well-founded. To save some space here, we skip right to nice, automated proof scripts, though we postpone introducing the principles behind such scripts into Part III of the book. Curious readers may still replace semicolons with periods and newlines to step through these scripts interactively. *)
adam@351 155
adam@351 156 Hint Constructors Acc.
adam@351 157
adam@351 158 Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
adam@351 159 unfold lengthOrder; induction len; crush.
adam@351 160 Defined.
adam@351 161
adam@351 162 Theorem lengthOrder_wf : well_founded lengthOrder.
adam@351 163 red; intro; eapply lengthOrder_wf'; eauto.
adam@351 164 Defined.
adam@351 165
adam@351 166 (** Notice that we end these proofs with %\index{Vernacular commands!Defined}%[Defined], not [Qed]. The alternate command marks the theorems as %\emph{transparent}%, so that the details of their proofs may be used during program execution. Why could such details possibly matter for computation? It turns out that [Fix] satisfies the primitive recursion restriction by declaring itself as %\emph{%#<i>#recursive in the structure of [Acc] proofs#</i>#%}%. This is possible because [Acc] proofs follow a predictable inductive structure. We must do work, as in the last theorem's proof, to establish that all elements of a type belong to [Acc], but the automatic unwinding of those proofs during recursion is straightforward. If we ended the proof with [Qed], the proof details would be hidden from computation, in which case the unwinding process would get stuck.
adam@351 167
adam@351 168 To justify our two recursive [mergeSort] calls, we will also need to prove that [partition] respects the [lengthOrder] relation. These proofs, too, must be kept transparent, to avoid stuckness of [Fix] evaluation. *)
adam@351 169
adam@351 170 Lemma partition_wf : forall len ls, 2 <= length ls <= len
adam@351 171 -> let (ls1, ls2) := partition ls in
adam@351 172 lengthOrder ls1 ls /\ lengthOrder ls2 ls.
adam@351 173 unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush);
adam@351 174 destruct (le_lt_dec 2 (length ls));
adam@351 175 repeat (match goal with
adam@351 176 | [ _ : length ?E < 2 |- _ ] => destruct E
adam@351 177 | [ _ : S (length ?E) < 2 |- _ ] => destruct E
adam@351 178 | [ IH : _ |- context[partition ?L] ] =>
adam@351 179 specialize (IH L); destruct (partition L); destruct IH
adam@351 180 end; crush).
adam@351 181 Defined.
adam@351 182
adam@351 183 Ltac partition := intros ls ?; intros; generalize (@partition_wf (length ls) ls);
adam@351 184 destruct (partition ls); destruct 1; crush.
adam@351 185
adam@351 186 Lemma partition_wf1 : forall ls, 2 <= length ls
adam@351 187 -> lengthOrder (fst (partition ls)) ls.
adam@351 188 partition.
adam@351 189 Defined.
adam@351 190
adam@351 191 Lemma partition_wf2 : forall ls, 2 <= length ls
adam@351 192 -> lengthOrder (snd (partition ls)) ls.
adam@351 193 partition.
adam@351 194 Defined.
adam@351 195
adam@351 196 Hint Resolve partition_wf1 partition_wf2.
adam@351 197
adam@351 198 (** To write the function definition itself, we use the %\index{tactics!refine}%[refine] tactic as a convenient way to write a program that needs to manipulate proofs, without writing out those proofs manually. We also use a replacement [le_lt_dec] for [leb] that has a more interesting dependent type. Again, more detail on these points will come in Chapter 7. *)
adam@351 199
adam@351 200 Definition mergeSort : list A -> list A.
adam@351 201 (* begin thide *)
adam@351 202 refine (Fix lengthOrder_wf (fun _ => list A)
adam@351 203 (fun (ls : list A)
adam@351 204 (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) =>
adam@351 205 if le_lt_dec 2 (length ls)
adam@351 206 then let lss := partition ls in
adam@351 207 merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
adam@351 208 else ls)); subst lss; eauto.
adam@351 209 Defined.
adam@351 210 (* end thide *)
adam@351 211 End mergeSort.
adam@351 212
adam@351 213 (** The important thing is that it is now easy to evaluate calls to [mergeSort]. *)
adam@351 214
adam@351 215 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil).
adam@351 216 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *)
adam@351 217
adam@351 218 (** Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *)
adam@351 219
adam@351 220 (* begin thide *)
adam@351 221 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,
adam@351 222 mergeSort le ls = if le_lt_dec 2 (length ls)
adam@351 223 then let lss := partition ls in
adam@351 224 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 225 else ls.
adam@351 226 intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros.
adam@351 227
adam@351 228 (** The library theorem [Fix_eq] imposes one more strange subgoal upon us. We must prove that the function body is unable to distinguish between %``%#"#self#"#%''% arguments that map equal inputs to equal outputs. One might think this should be true of any Gallina code, but in fact this general %\index{extensionality}\emph{%#<i>#function extensionality#</i>#%}% property is neither provable nor disprovable within Coq. The type of [Fix_eq] makes clear what we must show manually: *)
adam@351 229
adam@351 230 Check Fix_eq.
adam@351 231 (** %\vspace{-.15in}%[[
adam@351 232 Fix_eq
adam@351 233 : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
adam@351 234 (P : A -> Type)
adam@351 235 (F : forall x : A, (forall y : A, R y x -> P y) -> P x),
adam@351 236 (forall (x : A) (f g : forall y : A, R y x -> P y),
adam@351 237 (forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g) ->
adam@351 238 forall x : A,
adam@351 239 Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)
adam@351 240 ]]
adam@351 241
adam@351 242 Most such obligations are dischargable with straightforward proof automation, and this example is no exception. *)
adam@351 243
adam@351 244 match goal with
adam@351 245 | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E
adam@351 246 end; simpl; f_equal; auto.
adam@351 247 Qed.
adam@351 248 (* end thide *)
adam@351 249
adam@351 250 (** As a final test of our definition's suitability, we can extract to OCaml. *)
adam@351 251
adam@351 252 Extraction mergeSort.
adam@351 253
adam@351 254 (** <<
adam@351 255 let rec mergeSort le x =
adam@351 256 match le_lt_dec (S (S O)) (length x) with
adam@351 257 | Left ->
adam@351 258 let lss = partition x in
adam@351 259 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 260 | Right -> x
adam@351 261 >>
adam@351 262
adam@351 263 We see almost precisely the same definition we would have written manually in OCaml! Chapter 7 shows how we can clean up a few of the remaining warts, like use of the mysterious constructors [Left] and [Right].
adam@351 264
adam@351 265 One more piece of the full picture is missing. To go on and prove correctness of [mergeSort], we would need more than a way of unfolding its definition. We also need an appropriate induction principle matched to the well-founded relation. Such a principle is available in the standard library, though we will say no more about its details here. *)
adam@351 266
adam@351 267 Check well_founded_induction.
adam@351 268 (** %\vspace{-.15in}%[[
adam@351 269 well_founded_induction
adam@351 270 : forall (A : Type) (R : A -> A -> Prop),
adam@351 271 well_founded R ->
adam@351 272 forall P : A -> Set,
adam@351 273 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
adam@351 274 forall a : A, P a
adam@351 275 ]]
adam@351 276
adam@351 277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *)