Mercurial > cpdt > repo

annotate src/GeneralRec.v @ 533:8921cfa2f503

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Use TeX magic to prevent -- from being displayed as an en dash
author Cl?ment Pit--Claudel <clement.pitclaudel@live.com>
date Tue, 07 Apr 2015 18:59:24 -0400
parents 8f9f1e5b2fe3
children ed829eaa91b2
rev   line source
adam@380 1 (* Copyright (c) 2006, 2011-2012, 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@353 21 (** Termination of all programs is a crucial property of Gallina. Non-terminating 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@424 23 What exactly are the conservative criteria that we run up against? For _recursive_ definitions, recursive calls are only allowed on _syntactic subterms_ of the original primary argument, a restriction known as%\index{primitive recursion}% _primitive recursion_. 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 Chapter 5, we saw how _co-recursive_ definitions are checked against a syntactic guardedness condition that guarantees productivity.
adam@351 24
adam@353 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, without any up-front characterization of which inputs those may be.
adam@351 26
adam@404 27 Before proceeding, it is important to note that the problem here is not as fundamental as it may appear. The final example of Chapter 5 demonstrated what is called a%\index{deep embedding}% _deep embedding_ 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}% _shallow embedding_, 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@404 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}% _well-founded relation_, and the associated standard technique in Coq is%\index{well-founded recursion}% _well-founded recursion_. 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@475 37
adam@424 38 (** We have a set equipped with some "less-than-or-equal-to" test. *)
adam@351 39
adam@351 40 (** A standard function inserts an element into a sorted list, preserving sortedness. *)
adam@351 41
adam@351 42 Fixpoint insert (x : A) (ls : list A) : list A :=
adam@351 43 match ls with
adam@351 44 | nil => x :: nil
adam@351 45 | h :: ls' =>
adam@351 46 if le x h
adam@351 47 then x :: ls
adam@351 48 else h :: insert x ls'
adam@351 49 end.
adam@351 50
adam@351 51 (** 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 52
adam@351 53 Fixpoint merge (ls1 ls2 : list A) : list A :=
adam@351 54 match ls1 with
adam@351 55 | nil => ls2
adam@351 56 | h :: ls' => insert h (merge ls' ls2)
adam@351 57 end.
adam@351 58
adam@480 59 (** The last helper function for classic merge sort is the one that follows, to split a list arbitrarily into two pieces of approximately equal length. *)
adam@351 60
adam@480 61 Fixpoint split (ls : list A) : list A * list A :=
adam@351 62 match ls with
adam@351 63 | nil => (nil, nil)
adam@351 64 | h :: nil => (h :: nil, nil)
adam@351 65 | h1 :: h2 :: ls' =>
adam@480 66 let (ls1, ls2) := split ls' in
adam@351 67 (h1 :: ls1, h2 :: ls2)
adam@351 68 end.
adam@351 69
adam@424 70 (** Now, let us try to write the final sorting function, using a natural number "[<=]" test [leb] from the standard library.
adam@351 71 [[
adam@351 72 Fixpoint mergeSort (ls : list A) : list A :=
adam@453 73 if leb (length ls) 1
adam@351 74 then ls
adam@480 75 else let lss := split ls in
adam@351 76 merge (mergeSort (fst lss)) (mergeSort (snd lss)).
adam@351 77 ]]
adam@351 78
adam@351 79 <<
adam@351 80 Recursive call to mergeSort has principal argument equal to
adam@480 81 "fst (split ls)" instead of a subterm of "ls".
adam@351 82 >>
adam@351 83
adam@351 84 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 85
adam@351 86 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 87
adam@351 88 Print well_founded.
adam@351 89 (** %\vspace{-.15in}% [[
adam@351 90 well_founded =
adam@351 91 fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a
adam@351 92 ]]
adam@351 93
adam@404 94 The bulk of the definitional work devolves to the%\index{accessibility relation}\index{Gallina terms!Acc}% _accessibility_ relation [Acc], whose definition we may also examine. *)
adam@351 95
adam@424 96 (* begin hide *)
adam@437 97 (* begin thide *)
adam@424 98 Definition Acc_intro' := Acc_intro.
adam@437 99 (* end thide *)
adam@424 100 (* end hide *)
adam@424 101
adam@351 102 Print Acc.
adam@351 103 (** %\vspace{-.15in}% [[
adam@351 104 Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
adam@351 105 Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
adam@351 106 ]]
adam@351 107
adam@424 108 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 that we can make formal. Building on Chapter 5'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 109
adam@474 110 CoInductive infiniteDecreasingChain A (R : A -> A -> Prop) : stream A -> Prop :=
adam@474 111 | ChainCons : forall x y s, infiniteDecreasingChain R (Cons y s)
adam@351 112 -> R y x
adam@474 113 -> infiniteDecreasingChain R (Cons x (Cons y s)).
adam@351 114
adam@351 115 (** We can now prove that any accessible element cannot be the beginning of any infinite decreasing chain. *)
adam@351 116
adam@351 117 (* begin thide *)
adam@474 118 Lemma noBadChains' : forall A (R : A -> A -> Prop) x, Acc R x
adam@474 119 -> forall s, ~infiniteDecreasingChain R (Cons x s).
adam@351 120 induction 1; crush;
adam@351 121 match goal with
adam@474 122 | [ H : infiniteDecreasingChain _ _ |- _ ] => inversion H; eauto
adam@351 123 end.
adam@351 124 Qed.
adam@351 125
adam@351 126 (** From here, the absence of infinite decreasing chains in well-founded sets is immediate. *)
adam@351 127
adam@474 128 Theorem noBadChains : forall A (R : A -> A -> Prop), well_founded R
adam@474 129 -> forall s, ~infiniteDecreasingChain R s.
adam@474 130 destruct s; apply noBadChains'; auto.
adam@351 131 Qed.
adam@351 132 (* end thide *)
adam@351 133
adam@351 134 (** 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 135
adam@351 136 Check Fix.
adam@351 137 (** %\vspace{-.15in}%[[
adam@351 138 Fix
adam@351 139 : forall (A : Type) (R : A -> A -> Prop),
adam@351 140 well_founded R ->
adam@351 141 forall P : A -> Type,
adam@351 142 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
adam@351 143 forall x : A, P x
adam@351 144 ]]
adam@351 145
adam@351 146 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 147 [[
adam@351 148 forall x : A, (forall y : A, R y x -> P y) -> P x
adam@351 149 ]]
adam@351 150
adam@424 151 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 152
adam@353 153 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 that [Fix] has a dependent type of the sort we met in the previous chapter.
adam@351 154
adam@351 155 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 156
adam@351 157 Definition lengthOrder (ls1 ls2 : list A) :=
adam@351 158 length ls1 < length ls2.
adam@351 159
adam@353 160 (** We must prove that the relation is truly well-founded. To save some space in the rest of this chapter, we skip right to nice, automated proof scripts, though we postpone introducing the principles behind such scripts to Part III of the book. Curious readers may still replace semicolons with periods and newlines to step through these scripts interactively. *)
adam@351 161
adam@351 162 Hint Constructors Acc.
adam@351 163
adam@351 164 Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
adam@351 165 unfold lengthOrder; induction len; crush.
adam@351 166 Defined.
adam@351 167
adam@351 168 Theorem lengthOrder_wf : well_founded lengthOrder.
adam@351 169 red; intro; eapply lengthOrder_wf'; eauto.
adam@351 170 Defined.
adam@351 171
adam@514 172 (** Notice that we end these proofs with %\index{Vernacular commands!Defined}%[Defined], not [Qed]. Recall that [Defined] marks the theorems as %\emph{%#<i>#transparent#</i>#%}%, 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 _recursive in the structure of [Acc] proofs_. 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 173
adam@480 174 To justify our two recursive [mergeSort] calls, we will also need to prove that [split] respects the [lengthOrder] relation. These proofs, too, must be kept transparent, to avoid stuckness of [Fix] evaluation. We use the syntax [@foo] to reference identifier [foo] with its implicit argument behavior turned off. (The proof details below use Ltac features not introduced yet, and they are safe to skip for now.) *)
adam@351 175
adam@480 176 Lemma split_wf : forall len ls, 2 <= length ls <= len
adam@480 177 -> let (ls1, ls2) := split ls in
adam@351 178 lengthOrder ls1 ls /\ lengthOrder ls2 ls.
adam@351 179 unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush);
adam@351 180 destruct (le_lt_dec 2 (length ls));
adam@351 181 repeat (match goal with
adam@351 182 | [ _ : length ?E < 2 |- _ ] => destruct E
adam@351 183 | [ _ : S (length ?E) < 2 |- _ ] => destruct E
adam@480 184 | [ IH : _ |- context[split ?L] ] =>
adam@480 185 specialize (IH L); destruct (split L); destruct IH
adam@351 186 end; crush).
adam@351 187 Defined.
adam@351 188
adam@480 189 Ltac split_wf := intros ls ?; intros; generalize (@split_wf (length ls) ls);
adam@480 190 destruct (split ls); destruct 1; crush.
adam@351 191
adam@480 192 Lemma split_wf1 : forall ls, 2 <= length ls
adam@480 193 -> lengthOrder (fst (split ls)) ls.
adam@480 194 split_wf.
adam@351 195 Defined.
adam@351 196
adam@480 197 Lemma split_wf2 : forall ls, 2 <= length ls
adam@480 198 -> lengthOrder (snd (split ls)) ls.
adam@480 199 split_wf.
adam@351 200 Defined.
adam@351 201
adam@480 202 Hint Resolve split_wf1 split_wf2.
adam@351 203
adam@453 204 (** 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. (Note that we would not be able to complete the definition without this change, since [refine] will generate subgoals for the [if] branches based only on the _type_ of the test expression, not its _value_.) *)
adam@351 205
adam@351 206 Definition mergeSort : list A -> list A.
adam@351 207 (* begin thide *)
adam@351 208 refine (Fix lengthOrder_wf (fun _ => list A)
adam@351 209 (fun (ls : list A)
adam@351 210 (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) =>
adam@351 211 if le_lt_dec 2 (length ls)
adam@480 212 then let lss := split ls in
adam@351 213 merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
adam@351 214 else ls)); subst lss; eauto.
adam@351 215 Defined.
adam@351 216 (* end thide *)
adam@351 217 End mergeSort.
adam@351 218
adam@351 219 (** The important thing is that it is now easy to evaluate calls to [mergeSort]. *)
adam@351 220
adam@351 221 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil).
adam@351 222 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *)
adam@351 223
adam@441 224 (** %\smallskip{}%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 225
adam@351 226 (* begin thide *)
adam@351 227 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,
adam@351 228 mergeSort le ls = if le_lt_dec 2 (length ls)
adam@480 229 then let lss := split ls in
adam@351 230 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 231 else ls.
adam@351 232 intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros.
adam@351 233
adam@424 234 (** 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}% _function extensionality_ property is neither provable nor disprovable within Coq. The type of [Fix_eq] makes clear what we must show manually: *)
adam@351 235
adam@351 236 Check Fix_eq.
adam@351 237 (** %\vspace{-.15in}%[[
adam@351 238 Fix_eq
adam@351 239 : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
adam@351 240 (P : A -> Type)
adam@351 241 (F : forall x : A, (forall y : A, R y x -> P y) -> P x),
adam@351 242 (forall (x : A) (f g : forall y : A, R y x -> P y),
adam@351 243 (forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g) ->
adam@351 244 forall x : A,
adam@351 245 Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)
adam@351 246 ]]
adam@351 247
adam@465 248 Most such obligations are dischargeable with straightforward proof automation, and this example is no exception. *)
adam@351 249
adam@351 250 match goal with
adam@351 251 | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E
adam@351 252 end; simpl; f_equal; auto.
adam@351 253 Qed.
adam@351 254 (* end thide *)
adam@351 255
adam@351 256 (** As a final test of our definition's suitability, we can extract to OCaml. *)
adam@351 257
adam@351 258 Extraction mergeSort.
adam@351 259
adam@351 260 (** <<
adam@351 261 let rec mergeSort le x =
adam@351 262 match le_lt_dec (S (S O)) (length x) with
adam@351 263 | Left ->
adam@480 264 let lss = split x in
adam@351 265 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 266 | Right -> x
adam@351 267 >>
adam@351 268
adam@353 269 We see almost precisely the same definition we would have written manually in OCaml! It might be a good exercise for the reader to use the commands we saw in the previous chapter to clean up some remaining differences from idiomatic OCaml.
adam@351 270
adam@351 271 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 272
adam@351 273 Check well_founded_induction.
adam@351 274 (** %\vspace{-.15in}%[[
adam@351 275 well_founded_induction
adam@351 276 : forall (A : Type) (R : A -> A -> Prop),
adam@351 277 well_founded R ->
adam@351 278 forall P : A -> Set,
adam@351 279 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
adam@351 280 forall a : A, P a
adam@351 281 ]]
adam@351 282
adam@351 283 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]. *)
adam@352 284
adam@352 285
adam@354 286 (** * A Non-Termination Monad Inspired by Domain Theory *)
adam@352 287
adam@424 288 (** The key insights of %\index{domain theory}%domain theory%~\cite{WinskelDomains}% inspire the next approach to modeling non-termination. Domain theory is based on _information orders_ that relate values representing computation results, according to how much information these values convey. For instance, a simple domain might include values "the program does not terminate" and "the program terminates with the answer 5." The former is considered to be an _approximation_ of the latter, while the latter is _not_ an approximation of "the program terminates with the answer 6." The details of domain theory will not be important in what follows; we merely borrow the notion of an approximation ordering on computation results.
adam@355 289
adam@355 290 Consider this definition of a type of computations. *)
adam@355 291
adam@352 292 Section computation.
adam@352 293 Variable A : Type.
adam@355 294 (** The type [A] describes the result a computation will yield, if it terminates.
adam@355 295
adam@355 296 We give a rich dependent type to computations themselves: *)
adam@352 297
adam@352 298 Definition computation :=
adam@352 299 {f : nat -> option A
adam@352 300 | forall (n : nat) (v : A),
adam@352 301 f n = Some v
adam@352 302 -> forall (n' : nat), n' >= n
adam@352 303 -> f n' = Some v}.
adam@352 304
adam@474 305 (** A computation is fundamentally a function [f] from an _approximation level_ [n] to an optional result. Intuitively, higher [n] values enable termination in more cases than lower values. A call to [f] may return [None] to indicate that [n] was not high enough to run the computation to completion; higher [n] values may yield [Some]. Further, the proof obligation within the subset type asserts that [f] is _monotone_ in an appropriate sense: when some [n] is sufficient to produce termination, so are all higher [n] values, and they all yield the same program result [v].
adam@355 306
adam@355 307 It is easy to define a relation characterizing when a computation runs to a particular result at a particular approximation level. *)
adam@355 308
adam@352 309 Definition runTo (m : computation) (n : nat) (v : A) :=
adam@352 310 proj1_sig m n = Some v.
adam@352 311
adam@355 312 (** On top of [runTo], we also define [run], which is the most abstract notion of when a computation runs to a value. *)
adam@355 313
adam@352 314 Definition run (m : computation) (v : A) :=
adam@352 315 exists n, runTo m n v.
adam@352 316 End computation.
adam@352 317
adam@355 318 (** The book source code contains at this point some tactics, lemma proofs, and hint commands, to be used in proving facts about computations. Since their details are orthogonal to the message of this chapter, I have omitted them in the rendered version. *)
adam@355 319 (* begin hide *)
adam@355 320
adam@352 321 Hint Unfold runTo.
adam@352 322
adam@352 323 Ltac run' := unfold run, runTo in *; try red; crush;
adam@352 324 repeat (match goal with
adam@352 325 | [ _ : proj1_sig ?E _ = _ |- _ ] =>
adam@352 326 match goal with
adam@352 327 | [ x : _ |- _ ] =>
adam@352 328 match x with
adam@352 329 | E => destruct E
adam@352 330 end
adam@352 331 end
adam@352 332 | [ |- context[match ?M with exist _ _ => _ end] ] => let Heq := fresh "Heq" in
adam@352 333 case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst
adam@352 334 | [ _ : context[match ?M with exist _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in
adam@352 335 case_eq M; intros ? ? Heq; try rewrite Heq in *; subst
adam@352 336 | [ H : forall n v, ?E n = Some v -> _,
adam@352 337 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] =>
adam@426 338 specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
adam@352 339 | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto
adam@352 340 end; simpl in *); eauto 7.
adam@352 341
adam@352 342 Ltac run := run'; repeat (match goal with
adam@352 343 | [ H : forall n v, ?E n = Some v -> _
adam@352 344 |- context[match ?E ?N with Some _ => _ | None => _ end] ] =>
adam@426 345 specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
adam@352 346 end; run').
adam@352 347
adam@352 348 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P.
adam@352 349 exists 0; auto.
adam@352 350 Qed.
adam@352 351
adam@352 352 Hint Resolve ex_irrelevant.
adam@352 353
adam@352 354 Require Import Max.
adam@352 355
adam@380 356 Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n.
adam@380 357 induction n; destruct m; simpl; intuition;
adam@380 358 specialize (IHn m); intuition.
adam@380 359 Qed.
adam@380 360
adam@352 361 Ltac max := intros n m; generalize (max_spec_le n m); crush.
adam@352 362
adam@352 363 Lemma max_1 : forall n m, max n m >= n.
adam@352 364 max.
adam@352 365 Qed.
adam@352 366
adam@352 367 Lemma max_2 : forall n m, max n m >= m.
adam@352 368 max.
adam@352 369 Qed.
adam@352 370
adam@352 371 Hint Resolve max_1 max_2.
adam@352 372
adam@352 373 Lemma ge_refl : forall n, n >= n.
adam@352 374 crush.
adam@352 375 Qed.
adam@352 376
adam@352 377 Hint Resolve ge_refl.
adam@352 378
adam@352 379 Hint Extern 1 => match goal with
adam@352 380 | [ H : _ = exist _ _ _ |- _ ] => rewrite H
adam@352 381 end.
adam@355 382 (* end hide *)
adam@355 383 (** remove printing exists *)
adam@355 384
adam@480 385 (** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop. For any approximation level, it fails to terminate (returns [None]). Note the use of [abstract] to create a new opaque lemma for the proof found by the #<tt>#%\coqdocvar{%run%}%#</tt># tactic. In contrast to the previous section, opaque proofs are fine here, since the proof components of computations do not influence evaluation behavior. It is generally preferable to make proofs opaque when possible, as this enforces a kind of modularity in the code to follow, preventing it from depending on any details of the proof. *)
adam@352 386
adam@352 387 Section Bottom.
adam@352 388 Variable A : Type.
adam@352 389
adam@352 390 Definition Bottom : computation A.
adam@352 391 exists (fun _ : nat => @None A); abstract run.
adam@352 392 Defined.
adam@352 393
adam@352 394 Theorem run_Bottom : forall v, ~run Bottom v.
adam@352 395 run.
adam@352 396 Qed.
adam@352 397 End Bottom.
adam@352 398
adam@355 399 (** A slightly more complicated example is [Return], which gives the same terminating answer at every approximation level. *)
adam@355 400
adam@352 401 Section Return.
adam@352 402 Variable A : Type.
adam@352 403 Variable v : A.
adam@352 404
adam@352 405 Definition Return : computation A.
adam@352 406 intros; exists (fun _ : nat => Some v); abstract run.
adam@352 407 Defined.
adam@352 408
adam@352 409 Theorem run_Return : run Return v.
adam@352 410 run.
adam@352 411 Qed.
adam@352 412 End Return.
adam@352 413
adam@474 414 (** The name [Return] was meant to be suggestive of the standard operations of %\index{monad}%monads%~\cite{Monads}%. The other standard operation is [Bind], which lets us run one computation and, if it terminates, pass its result off to another computation. We implement bind using the notation [let (x, y) := e1 in e2], for pulling apart the value [e1] which may be thought of as a pair. The second component of a [computation] is a proof, which we do not need to mention directly in the definition of [Bind]. *)
adam@352 415
adam@352 416 Section Bind.
adam@352 417 Variables A B : Type.
adam@352 418 Variable m1 : computation A.
adam@352 419 Variable m2 : A -> computation B.
adam@352 420
adam@352 421 Definition Bind : computation B.
adam@352 422 exists (fun n =>
adam@357 423 let (f1, _) := m1 in
adam@352 424 match f1 n with
adam@352 425 | None => None
adam@352 426 | Some v =>
adam@357 427 let (f2, _) := m2 v in
adam@352 428 f2 n
adam@352 429 end); abstract run.
adam@352 430 Defined.
adam@352 431
adam@352 432 Theorem run_Bind : forall (v1 : A) (v2 : B),
adam@352 433 run m1 v1
adam@352 434 -> run (m2 v1) v2
adam@352 435 -> run Bind v2.
adam@352 436 run; match goal with
adam@352 437 | [ x : nat, y : nat |- _ ] => exists (max x y)
adam@352 438 end; run.
adam@352 439 Qed.
adam@352 440 End Bind.
adam@352 441
adam@355 442 (** A simple notation lets us write [Bind] calls the way they appear in Haskell. *)
adam@352 443
adam@352 444 Notation "x <- m1 ; m2" :=
adam@352 445 (Bind m1 (fun x => m2)) (right associativity, at level 70).
adam@352 446
adam@424 447 (** We can verify that we have indeed defined a monad, by proving the standard monad laws. Part of the exercise is choosing an appropriate notion of equality between computations. We use "equality at all approximation levels." *)
adam@355 448
adam@352 449 Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n.
adam@352 450
adam@352 451 Theorem left_identity : forall A B (a : A) (f : A -> computation B),
adam@352 452 meq (Bind (Return a) f) (f a).
adam@352 453 run.
adam@352 454 Qed.
adam@352 455
adam@352 456 Theorem right_identity : forall A (m : computation A),
adam@352 457 meq (Bind m (@Return _)) m.
adam@352 458 run.
adam@352 459 Qed.
adam@352 460
adam@357 461 Theorem associativity : forall A B C (m : computation A)
adam@357 462 (f : A -> computation B) (g : B -> computation C),
adam@352 463 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)).
adam@352 464 run.
adam@352 465 Qed.
adam@352 466
adam@398 467 (** Now we come to the piece most directly inspired by domain theory. We want to support general recursive function definitions, but domain theory tells us that not all definitions are reasonable; some fail to be _continuous_ and thus represent unrealizable computations. To formalize an analogous notion of continuity for our non-termination monad, we write down the approximation relation on computation results that we have had in mind all along. *)
adam@352 468
adam@352 469 Section lattice.
adam@352 470 Variable A : Type.
adam@352 471
adam@352 472 Definition leq (x y : option A) :=
adam@352 473 forall v, x = Some v -> y = Some v.
adam@352 474 End lattice.
adam@352 475
adam@355 476 (** We now have the tools we need to define a new [Fix] combinator that, unlike the one we saw in the prior section, does not require a termination proof, and in fact admits recursive definition of functions that fail to terminate on some or all inputs. *)
adam@352 477
adam@352 478 Section Fix.
adam@475 479
adam@355 480 (** First, we have the function domain and range types. *)
adam@355 481
adam@352 482 Variables A B : Type.
adam@355 483
adam@355 484 (** Next comes the function body, which is written as though it can be parameterized over itself, for recursive calls. *)
adam@355 485
adam@352 486 Variable f : (A -> computation B) -> (A -> computation B).
adam@352 487
adam@355 488 (** Finally, we impose an obligation to prove that the body [f] is continuous. That is, when [f] terminates according to one recursive version of itself, it also terminates with the same result at the same approximation level when passed a recursive version that refines the original, according to [leq]. *)
adam@355 489
adam@352 490 Hypothesis f_continuous : forall n v v1 x,
adam@352 491 runTo (f v1 x) n v
adam@352 492 -> forall (v2 : A -> computation B),
adam@352 493 (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n))
adam@352 494 -> runTo (f v2 x) n v.
adam@352 495
adam@355 496 (** The computational part of the [Fix] combinator is easy to define. At approximation level 0, we diverge; at higher levels, we run the body with a functional argument drawn from the next lower level. *)
adam@355 497
adam@352 498 Fixpoint Fix' (n : nat) (x : A) : computation B :=
adam@352 499 match n with
adam@352 500 | O => Bottom _
adam@352 501 | S n' => f (Fix' n') x
adam@352 502 end.
adam@352 503
adam@355 504 (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
adam@355 505
adam@352 506 Hint Extern 1 (_ >= _) => omega.
adam@352 507 Hint Unfold leq.
adam@352 508
adam@352 509 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
adam@352 510 -> forall n', n' >= n
adam@352 511 -> proj1_sig (Fix' n' x) steps = Some v.
adam@352 512 unfold runTo in *; induction n; crush;
adam@352 513 match goal with
adam@352 514 | [ H : _ >= _ |- _ ] => inversion H; crush; eauto
adam@352 515 end.
adam@352 516 Qed.
adam@352 517
adam@352 518 Hint Resolve Fix'_ok.
adam@352 519
adam@352 520 Hint Extern 1 (proj1_sig _ _ = _) => simpl;
adam@352 521 match goal with
adam@352 522 | [ |- proj1_sig ?E _ = _ ] => eapply (proj2_sig E)
adam@352 523 end.
adam@352 524
adam@352 525 Definition Fix : A -> computation B.
adam@352 526 intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run.
adam@352 527 Defined.
adam@352 528
adam@355 529 (** Finally, we can prove that [Fix] obeys the expected computation rule. *)
adam@352 530
adam@352 531 Theorem run_Fix : forall x v,
adam@352 532 run (f Fix x) v
adam@352 533 -> run (Fix x) v.
adam@352 534 run; match goal with
adam@352 535 | [ n : nat |- _ ] => exists (S n); eauto
adam@352 536 end.
adam@352 537 Qed.
adam@352 538 End Fix.
adam@352 539
adam@355 540 (* begin hide *)
adam@352 541 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
adam@352 542 -> x = y.
adam@426 543 intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
adam@352 544 Qed.
adam@352 545
adam@352 546 Lemma leq_None : forall A (x y : A), leq (Some x) None
adam@352 547 -> False.
adam@426 548 intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
adam@352 549 Qed.
adam@352 550
adam@355 551 Ltac mergeSort' := run;
adam@355 552 repeat (match goal with
adam@355 553 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
adam@355 554 end; run);
adam@355 555 repeat match goal with
adam@355 556 | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] =>
adam@355 557 match goal with
adam@355 558 | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] =>
adam@355 559 generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro
adam@355 560 end
adam@355 561 end; run; repeat match goal with
adam@355 562 | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst)
adam@355 563 end; auto.
adam@355 564 (* end hide *)
adam@355 565
adam@355 566 (** After all that work, it is now fairly painless to define a version of [mergeSort] that requires no proof of termination. We appeal to a program-specific tactic whose definition is hidden here but present in the book source. *)
adam@355 567
adam@352 568 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A).
adam@352 569 refine (fun A le => Fix
adam@352 570 (fun (mergeSort : list A -> computation (list A))
adam@352 571 (ls : list A) =>
adam@352 572 if le_lt_dec 2 (length ls)
adam@480 573 then let lss := split ls in
adam@352 574 ls1 <- mergeSort (fst lss);
adam@352 575 ls2 <- mergeSort (snd lss);
adam@352 576 Return (merge le ls1 ls2)
adam@355 577 else Return ls) _); abstract mergeSort'.
adam@352 578 Defined.
adam@352 579
adam@424 580 (** Furthermore, "running" [mergeSort'] on concrete inputs is as easy as choosing a sufficiently high approximation level and letting Coq's computation rules do the rest. Contrast this with the proof work that goes into deriving an evaluation fact for a deeply embedded language, with one explicit proof rule application per execution step. *)
adam@352 581
adam@352 582 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
adam@352 583 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
adam@352 584 exists 4; reflexivity.
adam@352 585 Qed.
adam@352 586
adam@453 587 (** There is another benefit of our new [Fix] compared with the one we used in the previous section: we can now write recursive functions that sometimes fail to terminate, without losing easy reasoning principles for the terminating cases. Consider this simple example, which appeals to another tactic whose definition we elide here. *)
adam@355 588
adam@355 589 (* begin hide *)
adam@355 590 Ltac looper := unfold leq in *; run;
adam@355 591 repeat match goal with
adam@355 592 | [ x : unit |- _ ] => destruct x
adam@355 593 | [ x : bool |- _ ] => destruct x
adam@355 594 end; auto.
adam@355 595 (* end hide *)
adam@355 596
adam@352 597 Definition looper : bool -> computation unit.
adam@352 598 refine (Fix (fun looper (b : bool) =>
adam@355 599 if b then Return tt else looper b) _); abstract looper.
adam@352 600 Defined.
adam@352 601
adam@352 602 Lemma test_looper : run (looper true) tt.
adam@352 603 exists 1; reflexivity.
adam@352 604 Qed.
adam@354 605
adam@355 606 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level.
adam@355 607
adam@480 608 There are other theorems that are important to prove about combinators like [Return], [Bind], and [Fix]. In general, for a computation [c], we sometimes have a hypothesis proving [run c v] for some [v], and we want to perform inversion to deduce what [v] must be. Each combinator should ideally have a theorem of that kind, for [c] built directly from that combinator. We have omitted such theorems here, but they are not hard to prove. In general, the domain theory-inspired approach avoids the type-theoretic "gotchas" that tend to show up in approaches that try to mix normal Coq computation with explicit syntax types. The next section of this chapter demonstrates two alternate approaches of that sort. In the final section of the chapter, we review the pros and cons of the different choices, coming to the conclusion that none of them is obviously better than any one of the others for all situations. *)
adam@355 609
adam@354 610
adam@354 611 (** * Co-Inductive Non-Termination Monads *)
adam@354 612
adam@356 613 (** There are two key downsides to both of the previous approaches: both require unusual syntax based on explicit calls to fixpoint combinators, and both generate immediate proof obligations about the bodies of recursive definitions. In Chapter 5, we have already seen how co-inductive types support recursive definitions that exhibit certain well-behaved varieties of non-termination. It turns out that we can leverage that co-induction support for encoding of general recursive definitions, by adding layers of co-inductive syntax. In effect, we mix elements of shallow and deep embeddings.
adam@356 614
adam@356 615 Our first example of this kind, proposed by Capretta%~\cite{Capretta}%, defines a silly-looking type of thunks; that is, computations that may be forced to yield results, if they terminate. *)
adam@356 616
adam@354 617 CoInductive thunk (A : Type) : Type :=
adam@354 618 | Answer : A -> thunk A
adam@354 619 | Think : thunk A -> thunk A.
adam@354 620
adam@356 621 (** A computation is either an immediate [Answer] or another computation wrapped inside [Think]. Since [thunk] is co-inductive, every [thunk] type is inhabited by an infinite nesting of [Think]s, standing for non-termination. Terminating results are [Answer] wrapped inside some finite number of [Think]s.
adam@356 622
adam@424 623 Why bother to write such a strange definition? The definition of [thunk] is motivated by the ability it gives us to define a "bind" operation, similar to the one we defined in the previous section. *)
adam@356 624
adam@356 625 CoFixpoint TBind A B (m1 : thunk A) (m2 : A -> thunk B) : thunk B :=
adam@354 626 match m1 with
adam@354 627 | Answer x => m2 x
adam@354 628 | Think m1' => Think (TBind m1' m2)
adam@354 629 end.
adam@354 630
adam@356 631 (** Note that the definition would violate the co-recursion guardedness restriction if we left out the seemingly superfluous [Think] on the righthand side of the second [match] branch.
adam@356 632
adam@356 633 We can prove that [Answer] and [TBind] form a monad for [thunk]. The proof is omitted here but present in the book source. As usual for this sort of proof, a key element is choosing an appropriate notion of equality for [thunk]s. *)
adam@356 634
adam@356 635 (* begin hide *)
adam@354 636 CoInductive thunk_eq A : thunk A -> thunk A -> Prop :=
adam@354 637 | EqAnswer : forall x, thunk_eq (Answer x) (Answer x)
adam@354 638 | EqThinkL : forall m1 m2, thunk_eq m1 m2 -> thunk_eq (Think m1) m2
adam@354 639 | EqThinkR : forall m1 m2, thunk_eq m1 m2 -> thunk_eq m1 (Think m2).
adam@354 640
adam@354 641 Section thunk_eq_coind.
adam@354 642 Variable A : Type.
adam@354 643 Variable P : thunk A -> thunk A -> Prop.
adam@354 644
adam@354 645 Hypothesis H : forall m1 m2, P m1 m2
adam@354 646 -> match m1, m2 with
adam@354 647 | Answer x1, Answer x2 => x1 = x2
adam@354 648 | Think m1', Think m2' => P m1' m2'
adam@354 649 | Think m1', _ => P m1' m2
adam@354 650 | _, Think m2' => P m1 m2'
adam@354 651 end.
adam@354 652
adam@354 653 Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
adam@354 654 cofix; intros;
adam@354 655 match goal with
adam@354 656 | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
adam@354 657 end; destruct m1; destruct m2; subst; repeat constructor; auto.
adam@354 658 Qed.
adam@354 659 End thunk_eq_coind.
adam@356 660 (* end hide *)
adam@356 661
adam@356 662 (** In the proofs to follow, we will need a function similar to one we saw in Chapter 5, to pull apart and reassemble a [thunk] in a way that provokes reduction of co-recursive calls. *)
adam@354 663
adam@354 664 Definition frob A (m : thunk A) : thunk A :=
adam@354 665 match m with
adam@354 666 | Answer x => Answer x
adam@354 667 | Think m' => Think m'
adam@354 668 end.
adam@354 669
adam@354 670 Theorem frob_eq : forall A (m : thunk A), frob m = m.
adam@354 671 destruct m; reflexivity.
adam@354 672 Qed.
adam@354 673
adam@356 674 (* begin hide *)
adam@354 675 Theorem thunk_eq_frob : forall A (m1 m2 : thunk A),
adam@354 676 thunk_eq (frob m1) (frob m2)
adam@354 677 -> thunk_eq m1 m2.
adam@354 678 intros; repeat rewrite frob_eq in *; auto.
adam@354 679 Qed.
adam@354 680
adam@354 681 Ltac findDestr := match goal with
adam@354 682 | [ |- context[match ?E with Answer _ => _ | Think _ => _ end] ] =>
adam@354 683 match E with
adam@354 684 | context[match _ with Answer _ => _ | Think _ => _ end] => fail 1
adam@354 685 | _ => destruct E
adam@354 686 end
adam@354 687 end.
adam@354 688
adam@354 689 Theorem thunk_eq_refl : forall A (m : thunk A), thunk_eq m m.
adam@354 690 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = m2)); crush; findDestr; reflexivity.
adam@354 691 Qed.
adam@354 692
adam@354 693 Hint Resolve thunk_eq_refl.
adam@354 694
adam@354 695 Theorem tleft_identity : forall A B (a : A) (f : A -> thunk B),
adam@354 696 thunk_eq (TBind (Answer a) f) (f a).
adam@354 697 intros; apply thunk_eq_frob; crush.
adam@354 698 Qed.
adam@354 699
adam@354 700 Theorem tright_identity : forall A (m : thunk A),
adam@354 701 thunk_eq (TBind m (@Answer _)) m.
adam@354 702 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = TBind m2 (@Answer _))); crush;
adam@354 703 findDestr; reflexivity.
adam@354 704 Qed.
adam@354 705
adam@354 706 Lemma TBind_Answer : forall (A B : Type) (v : A) (m2 : A -> thunk B),
adam@354 707 TBind (Answer v) m2 = m2 v.
adam@354 708 intros; rewrite <- (frob_eq (TBind (Answer v) m2));
adam@354 709 simpl; findDestr; reflexivity.
adam@354 710 Qed.
adam@354 711
adam@375 712 Hint Rewrite TBind_Answer.
adam@354 713
adam@355 714 (** printing exists $\exists$ *)
adam@355 715
adam@354 716 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C),
adam@354 717 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)).
adam@354 718 intros; apply (thunk_eq_coind (fun m1 m2 => (exists m,
adam@354 719 m1 = TBind (TBind m f) g
adam@354 720 /\ m2 = TBind m (fun x => TBind (f x) g))
adam@354 721 \/ m1 = m2)); crush; eauto; repeat (findDestr; crush; eauto).
adam@354 722 Qed.
adam@356 723 (* end hide *)
adam@356 724
adam@356 725 (** As a simple example, here is how we might define a tail-recursive factorial function. *)
adam@354 726
adam@354 727 CoFixpoint fact (n acc : nat) : thunk nat :=
adam@354 728 match n with
adam@354 729 | O => Answer acc
adam@354 730 | S n' => Think (fact n' (S n' * acc))
adam@354 731 end.
adam@354 732
adam@356 733 (** To test our definition, we need an evaluation relation that characterizes results of evaluating [thunk]s. *)
adam@356 734
adam@354 735 Inductive eval A : thunk A -> A -> Prop :=
adam@354 736 | EvalAnswer : forall x, eval (Answer x) x
adam@354 737 | EvalThink : forall m x, eval m x -> eval (Think m) x.
adam@354 738
adam@375 739 Hint Rewrite frob_eq.
adam@354 740
adam@354 741 Lemma eval_frob : forall A (c : thunk A) x,
adam@354 742 eval (frob c) x
adam@354 743 -> eval c x.
adam@354 744 crush.
adam@354 745 Qed.
adam@354 746
adam@354 747 Theorem eval_fact : eval (fact 5 1) 120.
adam@354 748 repeat (apply eval_frob; simpl; constructor).
adam@354 749 Qed.
adam@354 750
adam@356 751 (** We need to apply constructors of [eval] explicitly, but the process is easy to automate completely for concrete input programs.
adam@356 752
adam@465 753 Now consider another very similar definition, this time of a Fibonacci number function. *)
adam@357 754
adam@357 755 Notation "x <- m1 ; m2" :=
adam@357 756 (TBind m1 (fun x => m2)) (right associativity, at level 70).
adam@357 757
adam@404 758 (* begin hide *)
adam@437 759 (* begin thide *)
adam@424 760 Definition fib := pred.
adam@437 761 (* end thide *)
adam@404 762 (* end hide *)
adam@404 763
adam@453 764 (** %\vspace{-.3in}%[[
adam@354 765 CoFixpoint fib (n : nat) : thunk nat :=
adam@354 766 match n with
adam@354 767 | 0 => Answer 1
adam@354 768 | 1 => Answer 1
adam@357 769 | _ => n1 <- fib (pred n);
adam@357 770 n2 <- fib (pred (pred n));
adam@357 771 Answer (n1 + n2)
adam@354 772 end.
adam@354 773 ]]
adam@354 774
adam@356 775 Coq complains that the guardedness condition is violated. The two recursive calls are immediate arguments to [TBind], but [TBind] is not a constructor of [thunk]. Rather, it is a defined function. This example shows a very serious limitation of [thunk] for traditional functional programming: it is not, in general, possible to make recursive calls and then make further recursive calls, depending on the first call's result. The [fact] example succeeded because it was already tail recursive, meaning no further computation is needed after a recursive call.
adam@356 776
adam@356 777 %\medskip%
adam@356 778
adam@424 779 I know no easy fix for this problem of [thunk], but we can define an alternate co-inductive monad that avoids the problem, based on a proposal by Megacz%~\cite{Megacz}%. We ran into trouble because [TBind] was not a constructor of [thunk], so let us define a new type family where "bind" is a constructor. *)
adam@354 780
adam@354 781 CoInductive comp (A : Type) : Type :=
adam@354 782 | Ret : A -> comp A
adam@354 783 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.
adam@354 784
adam@404 785 (** This example shows off Coq's support for%\index{recursively non-uniform parameters}% _recursively non-uniform parameters_, as in the case of the parameter [A] declared above, where each constructor's type ends in [comp A], but there is a recursive use of [comp] with a different parameter [B]. Beside that technical wrinkle, we see the simplest possible definition of a monad, via a type whose two constructors are precisely the monad operators.
adam@356 786
adam@356 787 It is easy to define the semantics of terminating [comp] computations. *)
adam@356 788
adam@354 789 Inductive exec A : comp A -> A -> Prop :=
adam@354 790 | ExecRet : forall x, exec (Ret x) x
adam@354 791 | ExecBnd : forall B (c : comp B) (f : B -> comp A) x1 x2, exec (A := B) c x1
adam@354 792 -> exec (f x1) x2
adam@354 793 -> exec (Bnd c f) x2.
adam@354 794
adam@356 795 (** We can also prove that [Ret] and [Bnd] form a monad according to a notion of [comp] equality based on [exec], but we omit details here; they are in the book source at this point. *)
adam@356 796
adam@356 797 (* begin hide *)
adam@354 798 Hint Constructors exec.
adam@354 799
adam@354 800 Definition comp_eq A (c1 c2 : comp A) := forall r, exec c1 r <-> exec c2 r.
adam@354 801
adam@354 802 Ltac inverter := repeat match goal with
adam@354 803 | [ H : exec _ _ |- _ ] => inversion H; []; crush
adam@354 804 end.
adam@354 805
adam@354 806 Theorem cleft_identity : forall A B (a : A) (f : A -> comp B),
adam@354 807 comp_eq (Bnd (Ret a) f) (f a).
adam@354 808 red; crush; inverter; eauto.
adam@354 809 Qed.
adam@354 810
adam@354 811 Theorem cright_identity : forall A (m : comp A),
adam@354 812 comp_eq (Bnd m (@Ret _)) m.
adam@354 813 red; crush; inverter; eauto.
adam@354 814 Qed.
adam@354 815
adam@354 816 Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
adam@354 817 exec c r
adam@354 818 -> forall m, c = Bnd (Bnd m f) g
adam@354 819 -> exec (Bnd m (fun x => Bnd (f x) g)) r.
adam@354 820 induction 1; crush.
adam@354 821 match goal with
adam@354 822 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
adam@354 823 end.
adam@354 824 move H3 after A.
adam@354 825 generalize dependent B0.
adam@354 826 do 2 intro.
adam@354 827 subst.
adam@354 828 crush.
adam@354 829 inversion H; clear H; crush.
adam@354 830 eauto.
adam@354 831 Qed.
adam@354 832
adam@354 833 Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
adam@354 834 exec c r
adam@354 835 -> forall m, c = Bnd m (fun x => Bnd (f x) g)
adam@354 836 -> exec (Bnd (Bnd m f) g) r.
adam@354 837 induction 1; crush.
adam@354 838 match goal with
adam@354 839 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
adam@354 840 end.
adam@354 841 move H3 after B.
adam@354 842 generalize dependent B0.
adam@354 843 do 2 intro.
adam@354 844 subst.
adam@354 845 crush.
adam@354 846 inversion H0; clear H0; crush.
adam@354 847 eauto.
adam@354 848 Qed.
adam@354 849
adam@354 850 Hint Resolve cassociativity1 cassociativity2.
adam@354 851
adam@354 852 Theorem cassociativity : forall A B C (m : comp A) (f : A -> comp B) (g : B -> comp C),
adam@354 853 comp_eq (Bnd (Bnd m f) g) (Bnd m (fun x => Bnd (f x) g)).
adam@354 854 red; crush; eauto.
adam@354 855 Qed.
adam@356 856 (* end hide *)
adam@356 857
adam@469 858 (** Not only can we define the Fibonacci function with the new monad, but even our running example of merge sort becomes definable. By shadowing our previous notation for "bind," we can write almost exactly the same code as in our previous [mergeSort'] definition, but with less syntactic clutter. *)
adam@356 859
adam@356 860 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)).
adam@354 861
adam@354 862 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) :=
adam@354 863 if le_lt_dec 2 (length ls)
adam@480 864 then let lss := split ls in
adam@356 865 ls1 <- mergeSort'' le (fst lss);
adam@356 866 ls2 <- mergeSort'' le (snd lss);
adam@356 867 Ret (merge le ls1 ls2)
adam@354 868 else Ret ls.
adam@354 869
adam@356 870 (** To execute this function, we go through the usual exercise of writing a function to catalyze evaluation of co-recursive calls. *)
adam@356 871
adam@354 872 Definition frob' A (c : comp A) :=
adam@354 873 match c with
adam@354 874 | Ret x => Ret x
adam@354 875 | Bnd _ c' f => Bnd c' f
adam@354 876 end.
adam@354 877
adam@354 878 Lemma exec_frob : forall A (c : comp A) x,
adam@354 879 exec (frob' c) x
adam@354 880 -> exec c x.
adam@356 881 destruct c; crush.
adam@354 882 Qed.
adam@354 883
adam@356 884 (** Now the same sort of proof script that we applied for testing [thunk]s will get the job done. *)
adam@356 885
adam@354 886 Lemma test_mergeSort'' : exec (mergeSort'' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
adam@354 887 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
adam@354 888 repeat (apply exec_frob; simpl; econstructor).
adam@354 889 Qed.
adam@354 890
adam@356 891 (** Have we finally reached the ideal solution for encoding general recursive definitions, with minimal hassle in syntax and proof obligations? Unfortunately, we have not, as [comp] has a serious expressivity weakness. Consider the following definition of a curried addition function: *)
adam@356 892
adam@354 893 Definition curriedAdd (n : nat) := Ret (fun m : nat => Ret (n + m)).
adam@354 894
adam@356 895 (** This definition works fine, but we run into trouble when we try to apply it in a trivial way.
adam@356 896 [[
adam@356 897 Definition testCurriedAdd := Bnd (curriedAdd 2) (fun f => f 3).
adam@354 898 ]]
adam@354 899
adam@354 900 <<
adam@354 901 Error: Universe inconsistency.
adam@354 902 >>
adam@356 903
adam@496 904 The problem has to do with rules for inductive definitions that we will study in more detail in Chapter 12. Briefly, recall that the type of the constructor [Bnd] quantifies over a type [B]. To make [testCurriedAdd] work, we would need to instantiate [B] as [nat -> comp nat]. However, Coq enforces a %\emph{predicativity restriction}% that (roughly) no quantifier in an inductive or co-inductive type's definition may ever be instantiated with a term that contains the type being defined. Chapter 12 presents the exact mechanism by which this restriction is enforced, but for now our conclusion is that [comp] is fatally flawed as a way of encoding interesting higher-order functional programs that use general recursion. *)
adam@354 905
adam@354 906
adam@357 907 (** * Comparing the Alternatives *)
adam@354 908
adam@453 909 (** We have seen four different approaches to encoding general recursive definitions in Coq. Among them there is no clear champion that dominates the others in every important way. Instead, we close the chapter by comparing the techniques along a number of dimensions. Every technique allows recursive definitions with termination arguments that go beyond Coq's built-in termination checking, so we must turn to subtler points to highlight differences.
adam@356 910
adam@356 911 One useful property is automatic integration with normal Coq programming. That is, we would like the type of a function to be the same, whether or not that function is defined using an interesting recursion pattern. Only the first of the four techniques, well-founded recursion, meets this criterion. It is also the only one of the four to meet the related criterion that evaluation of function calls can take place entirely inside Coq's built-in computation machinery. The monad inspired by domain theory occupies some middle ground in this dimension, since generally standard computation is enough to evaluate a term once a high enough approximation level is provided.
adam@356 912
adam@356 913 Another useful property is that a function and its termination argument may be developed separately. We may even want to define functions that fail to terminate on some or all inputs. The well-founded recursion technique does not have this property, but the other three do.
adam@356 914
adam@480 915 One minor plus is the ability to write recursive definitions in natural syntax, rather than with calls to higher-order combinators. This downside of the first two techniques is actually rather easy to get around using Coq's notation mechanism, though we leave the details as an exercise for the reader. (For this and other details of notations, see Chapter 12 of the Coq 8.4 manual.)
adam@356 916
adam@465 917 The first two techniques impose proof obligations that are more basic than termination arguments, where well-founded recursion requires a proof of extensionality and domain-theoretic recursion requires a proof of continuity. A function may not be defined, and thus may not be computed with, until these obligations are proved. The co-inductive techniques avoid this problem, as recursive definitions may be made without any proof obligations.
adam@356 918
adam@356 919 We can also consider support for common idioms in functional programming. For instance, the [thunk] monad effectively only supports recursion that is tail recursion, while the others allow arbitrary recursion schemes.
adam@356 920
adam@356 921 On the other hand, the [comp] monad does not support the effective mixing of higher-order functions and general recursion, while all the other techniques do. For instance, we can finish the failed [curriedAdd] example in the domain-theoretic monad. *)
adam@356 922
adam@354 923 Definition curriedAdd' (n : nat) := Return (fun m : nat => Return (n + m)).
adam@354 924
adam@356 925 Definition testCurriedAdd := Bind (curriedAdd' 2) (fun f => f 3).
adam@356 926
adam@357 927 (** The same techniques also apply to more interesting higher-order functions like list map, and, as in all four techniques, we can mix primitive and general recursion, preferring the former when possible to avoid proof obligations. *)
adam@354 928
adam@354 929 Fixpoint map A B (f : A -> computation B) (ls : list A) : computation (list B) :=
adam@354 930 match ls with
adam@354 931 | nil => Return nil
adam@354 932 | x :: ls' => Bind (f x) (fun x' =>
adam@354 933 Bind (map f ls') (fun ls'' =>
adam@354 934 Return (x' :: ls'')))
adam@354 935 end.
adam@354 936
adam@355 937 (** remove printing exists *)
adam@356 938 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil))
adam@356 939 (2 :: 3 :: 4 :: nil).
adam@354 940 exists 1; reflexivity.
adam@354 941 Qed.
adam@356 942
adam@524 943 (** One further disadvantage of [comp] is that we cannot prove an inversion lemma for executions of [Bind] without appealing to an _axiom_, a logical complication that we discuss at more length in Chapter 12. The other three techniques allow proof of all the important theorems within the normal logic of Coq.
adam@356 944
adam@357 945 Perhaps one theme of our comparison is that one must trade off between, on one hand, functional programming expressiveness and compatibility with normal Coq types and computation; and, on the other hand, the level of proof obligations one is willing to handle at function definition time. *)