annotate src/GeneralRec.v @ 388:057a29f9c773

Baffling unification messages explained
author Adam Chlipala <adam@chlipala.net>
date Thu, 12 Apr 2012 16:27:28 -0400
parents 31fa03bc0f18
children 05efde66559d
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@353 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 Chapter 5, we saw how %\emph{%#<i>#co-recursive#</i>#%}% definitions are checked against a syntactic guardness 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@353 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}\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@357 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 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 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 forall x : A, (forall y : A, R y x -> P y) -> P x
adam@351 142 ]]
adam@351 143
adam@351 144 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 145
adam@353 146 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 147
adam@351 148 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 149
adam@351 150 Definition lengthOrder (ls1 ls2 : list A) :=
adam@351 151 length ls1 < length ls2.
adam@351 152
adam@353 153 (** 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 154
adam@351 155 Hint Constructors Acc.
adam@351 156
adam@351 157 Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
adam@351 158 unfold lengthOrder; induction len; crush.
adam@351 159 Defined.
adam@351 160
adam@351 161 Theorem lengthOrder_wf : well_founded lengthOrder.
adam@351 162 red; intro; eapply lengthOrder_wf'; eauto.
adam@351 163 Defined.
adam@351 164
adam@353 165 (** Notice that we end these proofs with %\index{Vernacular commands!Defined}%[Defined], not [Qed]. Recall that [Defined] 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 166
adam@351 167 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 168
adam@351 169 Lemma partition_wf : forall len ls, 2 <= length ls <= len
adam@351 170 -> let (ls1, ls2) := partition ls in
adam@351 171 lengthOrder ls1 ls /\ lengthOrder ls2 ls.
adam@351 172 unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush);
adam@351 173 destruct (le_lt_dec 2 (length ls));
adam@351 174 repeat (match goal with
adam@351 175 | [ _ : length ?E < 2 |- _ ] => destruct E
adam@351 176 | [ _ : S (length ?E) < 2 |- _ ] => destruct E
adam@351 177 | [ IH : _ |- context[partition ?L] ] =>
adam@351 178 specialize (IH L); destruct (partition L); destruct IH
adam@351 179 end; crush).
adam@351 180 Defined.
adam@351 181
adam@351 182 Ltac partition := intros ls ?; intros; generalize (@partition_wf (length ls) ls);
adam@351 183 destruct (partition ls); destruct 1; crush.
adam@351 184
adam@351 185 Lemma partition_wf1 : forall ls, 2 <= length ls
adam@351 186 -> lengthOrder (fst (partition ls)) ls.
adam@351 187 partition.
adam@351 188 Defined.
adam@351 189
adam@351 190 Lemma partition_wf2 : forall ls, 2 <= length ls
adam@351 191 -> lengthOrder (snd (partition ls)) ls.
adam@351 192 partition.
adam@351 193 Defined.
adam@351 194
adam@351 195 Hint Resolve partition_wf1 partition_wf2.
adam@351 196
adam@353 197 (** 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. *)
adam@351 198
adam@351 199 Definition mergeSort : list A -> list A.
adam@351 200 (* begin thide *)
adam@351 201 refine (Fix lengthOrder_wf (fun _ => list A)
adam@351 202 (fun (ls : list A)
adam@351 203 (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) =>
adam@351 204 if le_lt_dec 2 (length ls)
adam@351 205 then let lss := partition ls in
adam@351 206 merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
adam@351 207 else ls)); subst lss; eauto.
adam@351 208 Defined.
adam@351 209 (* end thide *)
adam@351 210 End mergeSort.
adam@351 211
adam@351 212 (** The important thing is that it is now easy to evaluate calls to [mergeSort]. *)
adam@351 213
adam@351 214 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil).
adam@351 215 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *)
adam@351 216
adam@351 217 (** 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 218
adam@351 219 (* begin thide *)
adam@351 220 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,
adam@351 221 mergeSort le ls = if le_lt_dec 2 (length ls)
adam@351 222 then let lss := partition ls in
adam@351 223 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 224 else ls.
adam@351 225 intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros.
adam@351 226
adam@351 227 (** 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 228
adam@351 229 Check Fix_eq.
adam@351 230 (** %\vspace{-.15in}%[[
adam@351 231 Fix_eq
adam@351 232 : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
adam@351 233 (P : A -> Type)
adam@351 234 (F : forall x : A, (forall y : A, R y x -> P y) -> P x),
adam@351 235 (forall (x : A) (f g : forall y : A, R y x -> P y),
adam@351 236 (forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g) ->
adam@351 237 forall x : A,
adam@351 238 Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)
adam@351 239 ]]
adam@351 240
adam@351 241 Most such obligations are dischargable with straightforward proof automation, and this example is no exception. *)
adam@351 242
adam@351 243 match goal with
adam@351 244 | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E
adam@351 245 end; simpl; f_equal; auto.
adam@351 246 Qed.
adam@351 247 (* end thide *)
adam@351 248
adam@351 249 (** As a final test of our definition's suitability, we can extract to OCaml. *)
adam@351 250
adam@351 251 Extraction mergeSort.
adam@351 252
adam@351 253 (** <<
adam@351 254 let rec mergeSort le x =
adam@351 255 match le_lt_dec (S (S O)) (length x) with
adam@351 256 | Left ->
adam@351 257 let lss = partition x in
adam@351 258 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 259 | Right -> x
adam@351 260 >>
adam@351 261
adam@353 262 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 263
adam@351 264 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 265
adam@351 266 Check well_founded_induction.
adam@351 267 (** %\vspace{-.15in}%[[
adam@351 268 well_founded_induction
adam@351 269 : forall (A : Type) (R : A -> A -> Prop),
adam@351 270 well_founded R ->
adam@351 271 forall P : A -> Set,
adam@351 272 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
adam@351 273 forall a : A, P a
adam@351 274 ]]
adam@351 275
adam@351 276 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 277
adam@352 278
adam@354 279 (** * A Non-Termination Monad Inspired by Domain Theory *)
adam@352 280
adam@357 281 (** The key insights of %\index{domain theory}%domain theory%~\cite{WinskelDomains}% inspire the next approach to modeling non-termination. Domain theory is based on %\emph{%#<i>#information orders#</i>#%}% 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 %\emph{%#<i>#approximation#</i>#%}% of the latter, while the latter is %\emph{%#<i>#not#</i>#%}% 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 282
adam@355 283 Consider this definition of a type of computations. *)
adam@355 284
adam@352 285 Section computation.
adam@352 286 Variable A : Type.
adam@355 287 (** The type [A] describes the result a computation will yield, if it terminates.
adam@355 288
adam@355 289 We give a rich dependent type to computations themselves: *)
adam@352 290
adam@352 291 Definition computation :=
adam@352 292 {f : nat -> option A
adam@352 293 | forall (n : nat) (v : A),
adam@352 294 f n = Some v
adam@352 295 -> forall (n' : nat), n' >= n
adam@352 296 -> f n' = Some v}.
adam@352 297
adam@355 298 (** A computation is fundamentally a function [f] from an %\emph{%#<i>#approximation level#</i>#%}% [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 sigma type asserts that [f] is %\emph{%#<i>#monotone#</i>#%}% 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 299
adam@355 300 It is easy to define a relation characterizing when a computation runs to a particular result at a particular approximation level. *)
adam@355 301
adam@352 302 Definition runTo (m : computation) (n : nat) (v : A) :=
adam@352 303 proj1_sig m n = Some v.
adam@352 304
adam@355 305 (** On top of [runTo], we also define [run], which is the most abstract notion of when a computation runs to a value. *)
adam@355 306
adam@352 307 Definition run (m : computation) (v : A) :=
adam@352 308 exists n, runTo m n v.
adam@352 309 End computation.
adam@352 310
adam@355 311 (** 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 312 (* begin hide *)
adam@355 313
adam@352 314 Hint Unfold runTo.
adam@352 315
adam@352 316 Ltac run' := unfold run, runTo in *; try red; crush;
adam@352 317 repeat (match goal with
adam@352 318 | [ _ : proj1_sig ?E _ = _ |- _ ] =>
adam@352 319 match goal with
adam@352 320 | [ x : _ |- _ ] =>
adam@352 321 match x with
adam@352 322 | E => destruct E
adam@352 323 end
adam@352 324 end
adam@352 325 | [ |- context[match ?M with exist _ _ => _ end] ] => let Heq := fresh "Heq" in
adam@352 326 case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst
adam@352 327 | [ _ : context[match ?M with exist _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in
adam@352 328 case_eq M; intros ? ? Heq; try rewrite Heq in *; subst
adam@352 329 | [ H : forall n v, ?E n = Some v -> _,
adam@352 330 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] =>
adam@352 331 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
adam@352 332 | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto
adam@352 333 end; simpl in *); eauto 7.
adam@352 334
adam@352 335 Ltac run := run'; repeat (match goal with
adam@352 336 | [ H : forall n v, ?E n = Some v -> _
adam@352 337 |- context[match ?E ?N with Some _ => _ | None => _ end] ] =>
adam@352 338 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
adam@352 339 end; run').
adam@352 340
adam@352 341 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P.
adam@352 342 exists 0; auto.
adam@352 343 Qed.
adam@352 344
adam@352 345 Hint Resolve ex_irrelevant.
adam@352 346
adam@352 347 Require Import Max.
adam@352 348
adam@380 349 Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n.
adam@380 350 induction n; destruct m; simpl; intuition;
adam@380 351 specialize (IHn m); intuition.
adam@380 352 Qed.
adam@380 353
adam@352 354 Ltac max := intros n m; generalize (max_spec_le n m); crush.
adam@352 355
adam@352 356 Lemma max_1 : forall n m, max n m >= n.
adam@352 357 max.
adam@352 358 Qed.
adam@352 359
adam@352 360 Lemma max_2 : forall n m, max n m >= m.
adam@352 361 max.
adam@352 362 Qed.
adam@352 363
adam@352 364 Hint Resolve max_1 max_2.
adam@352 365
adam@352 366 Lemma ge_refl : forall n, n >= n.
adam@352 367 crush.
adam@352 368 Qed.
adam@352 369
adam@352 370 Hint Resolve ge_refl.
adam@352 371
adam@352 372 Hint Extern 1 => match goal with
adam@352 373 | [ H : _ = exist _ _ _ |- _ ] => rewrite H
adam@352 374 end.
adam@355 375 (* end hide *)
adam@355 376 (** remove printing exists *)
adam@355 377
adam@357 378 (** 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 [run] tactic. In contrast to the previous section, opaque proofs are fine here, since the proof components of computations do not influence evaluation behavior. *)
adam@352 379
adam@352 380 Section Bottom.
adam@352 381 Variable A : Type.
adam@352 382
adam@352 383 Definition Bottom : computation A.
adam@352 384 exists (fun _ : nat => @None A); abstract run.
adam@352 385 Defined.
adam@352 386
adam@352 387 Theorem run_Bottom : forall v, ~run Bottom v.
adam@352 388 run.
adam@352 389 Qed.
adam@352 390 End Bottom.
adam@352 391
adam@355 392 (** A slightly more complicated example is [Return], which gives the same terminating answer at every approximation level. *)
adam@355 393
adam@352 394 Section Return.
adam@352 395 Variable A : Type.
adam@352 396 Variable v : A.
adam@352 397
adam@352 398 Definition Return : computation A.
adam@352 399 intros; exists (fun _ : nat => Some v); abstract run.
adam@352 400 Defined.
adam@352 401
adam@352 402 Theorem run_Return : run Return v.
adam@352 403 run.
adam@352 404 Qed.
adam@352 405 End Return.
adam@352 406
adam@356 407 (** 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. *)
adam@352 408
adam@352 409 Section Bind.
adam@352 410 Variables A B : Type.
adam@352 411 Variable m1 : computation A.
adam@352 412 Variable m2 : A -> computation B.
adam@352 413
adam@352 414 Definition Bind : computation B.
adam@352 415 exists (fun n =>
adam@357 416 let (f1, _) := m1 in
adam@352 417 match f1 n with
adam@352 418 | None => None
adam@352 419 | Some v =>
adam@357 420 let (f2, _) := m2 v in
adam@352 421 f2 n
adam@352 422 end); abstract run.
adam@352 423 Defined.
adam@352 424
adam@352 425 Theorem run_Bind : forall (v1 : A) (v2 : B),
adam@352 426 run m1 v1
adam@352 427 -> run (m2 v1) v2
adam@352 428 -> run Bind v2.
adam@352 429 run; match goal with
adam@352 430 | [ x : nat, y : nat |- _ ] => exists (max x y)
adam@352 431 end; run.
adam@352 432 Qed.
adam@352 433 End Bind.
adam@352 434
adam@355 435 (** A simple notation lets us write [Bind] calls the way they appear in Haskell. *)
adam@352 436
adam@352 437 Notation "x <- m1 ; m2" :=
adam@352 438 (Bind m1 (fun x => m2)) (right associativity, at level 70).
adam@352 439
adam@355 440 (** 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 441
adam@352 442 Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n.
adam@352 443
adam@352 444 Theorem left_identity : forall A B (a : A) (f : A -> computation B),
adam@352 445 meq (Bind (Return a) f) (f a).
adam@352 446 run.
adam@352 447 Qed.
adam@352 448
adam@352 449 Theorem right_identity : forall A (m : computation A),
adam@352 450 meq (Bind m (@Return _)) m.
adam@352 451 run.
adam@352 452 Qed.
adam@352 453
adam@357 454 Theorem associativity : forall A B C (m : computation A)
adam@357 455 (f : A -> computation B) (g : B -> computation C),
adam@352 456 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)).
adam@352 457 run.
adam@352 458 Qed.
adam@352 459
adam@355 460 (** 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 %\emph{%#<i>#continuous#</i>#%}% 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 461
adam@352 462 Section lattice.
adam@352 463 Variable A : Type.
adam@352 464
adam@352 465 Definition leq (x y : option A) :=
adam@352 466 forall v, x = Some v -> y = Some v.
adam@352 467 End lattice.
adam@352 468
adam@355 469 (** 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 470
adam@352 471 Section Fix.
adam@355 472 (** First, we have the function domain and range types. *)
adam@355 473
adam@352 474 Variables A B : Type.
adam@355 475
adam@355 476 (** Next comes the function body, which is written as though it can be parameterized over itself, for recursive calls. *)
adam@355 477
adam@352 478 Variable f : (A -> computation B) -> (A -> computation B).
adam@352 479
adam@355 480 (** 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 481
adam@352 482 Hypothesis f_continuous : forall n v v1 x,
adam@352 483 runTo (f v1 x) n v
adam@352 484 -> forall (v2 : A -> computation B),
adam@352 485 (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n))
adam@352 486 -> runTo (f v2 x) n v.
adam@352 487
adam@355 488 (** 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 489
adam@352 490 Fixpoint Fix' (n : nat) (x : A) : computation B :=
adam@352 491 match n with
adam@352 492 | O => Bottom _
adam@352 493 | S n' => f (Fix' n') x
adam@352 494 end.
adam@352 495
adam@355 496 (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
adam@355 497
adam@352 498 Hint Extern 1 (_ >= _) => omega.
adam@352 499 Hint Unfold leq.
adam@352 500
adam@352 501 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
adam@352 502 -> forall n', n' >= n
adam@352 503 -> proj1_sig (Fix' n' x) steps = Some v.
adam@352 504 unfold runTo in *; induction n; crush;
adam@352 505 match goal with
adam@352 506 | [ H : _ >= _ |- _ ] => inversion H; crush; eauto
adam@352 507 end.
adam@352 508 Qed.
adam@352 509
adam@352 510 Hint Resolve Fix'_ok.
adam@352 511
adam@352 512 Hint Extern 1 (proj1_sig _ _ = _) => simpl;
adam@352 513 match goal with
adam@352 514 | [ |- proj1_sig ?E _ = _ ] => eapply (proj2_sig E)
adam@352 515 end.
adam@352 516
adam@352 517 Definition Fix : A -> computation B.
adam@352 518 intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run.
adam@352 519 Defined.
adam@352 520
adam@355 521 (** Finally, we can prove that [Fix] obeys the expected computation rule. *)
adam@352 522
adam@352 523 Theorem run_Fix : forall x v,
adam@352 524 run (f Fix x) v
adam@352 525 -> run (Fix x) v.
adam@352 526 run; match goal with
adam@352 527 | [ n : nat |- _ ] => exists (S n); eauto
adam@352 528 end.
adam@352 529 Qed.
adam@352 530 End Fix.
adam@352 531
adam@355 532 (* begin hide *)
adam@352 533 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
adam@352 534 -> x = y.
adam@352 535 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
adam@352 536 Qed.
adam@352 537
adam@352 538 Lemma leq_None : forall A (x y : A), leq (Some x) None
adam@352 539 -> False.
adam@352 540 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
adam@352 541 Qed.
adam@352 542
adam@355 543 Ltac mergeSort' := run;
adam@355 544 repeat (match goal with
adam@355 545 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
adam@355 546 end; run);
adam@355 547 repeat match goal with
adam@355 548 | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] =>
adam@355 549 match goal with
adam@355 550 | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] =>
adam@355 551 generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro
adam@355 552 end
adam@355 553 end; run; repeat match goal with
adam@355 554 | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst)
adam@355 555 end; auto.
adam@355 556 (* end hide *)
adam@355 557
adam@355 558 (** 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 559
adam@352 560 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A).
adam@352 561 refine (fun A le => Fix
adam@352 562 (fun (mergeSort : list A -> computation (list A))
adam@352 563 (ls : list A) =>
adam@352 564 if le_lt_dec 2 (length ls)
adam@352 565 then let lss := partition ls in
adam@352 566 ls1 <- mergeSort (fst lss);
adam@352 567 ls2 <- mergeSort (snd lss);
adam@352 568 Return (merge le ls1 ls2)
adam@355 569 else Return ls) _); abstract mergeSort'.
adam@352 570 Defined.
adam@352 571
adam@355 572 (** 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 573
adam@352 574 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
adam@352 575 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
adam@352 576 exists 4; reflexivity.
adam@352 577 Qed.
adam@352 578
adam@355 579 (** There is another benefit of our new [Fix] compared with 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 580
adam@355 581 (* begin hide *)
adam@355 582 Ltac looper := unfold leq in *; run;
adam@355 583 repeat match goal with
adam@355 584 | [ x : unit |- _ ] => destruct x
adam@355 585 | [ x : bool |- _ ] => destruct x
adam@355 586 end; auto.
adam@355 587 (* end hide *)
adam@355 588
adam@352 589 Definition looper : bool -> computation unit.
adam@352 590 refine (Fix (fun looper (b : bool) =>
adam@355 591 if b then Return tt else looper b) _); abstract looper.
adam@352 592 Defined.
adam@352 593
adam@352 594 Lemma test_looper : run (looper true) tt.
adam@352 595 exists 1; reflexivity.
adam@352 596 Qed.
adam@354 597
adam@355 598 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level.
adam@355 599
adam@355 600 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. *)
adam@355 601
adam@354 602
adam@354 603 (** * Co-Inductive Non-Termination Monads *)
adam@354 604
adam@356 605 (** 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 606
adam@356 607 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 608
adam@354 609 CoInductive thunk (A : Type) : Type :=
adam@354 610 | Answer : A -> thunk A
adam@354 611 | Think : thunk A -> thunk A.
adam@354 612
adam@356 613 (** 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 614
adam@356 615 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 616
adam@356 617 CoFixpoint TBind A B (m1 : thunk A) (m2 : A -> thunk B) : thunk B :=
adam@354 618 match m1 with
adam@354 619 | Answer x => m2 x
adam@354 620 | Think m1' => Think (TBind m1' m2)
adam@354 621 end.
adam@354 622
adam@356 623 (** 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 624
adam@356 625 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 626
adam@356 627 (* begin hide *)
adam@354 628 CoInductive thunk_eq A : thunk A -> thunk A -> Prop :=
adam@354 629 | EqAnswer : forall x, thunk_eq (Answer x) (Answer x)
adam@354 630 | EqThinkL : forall m1 m2, thunk_eq m1 m2 -> thunk_eq (Think m1) m2
adam@354 631 | EqThinkR : forall m1 m2, thunk_eq m1 m2 -> thunk_eq m1 (Think m2).
adam@354 632
adam@354 633 Section thunk_eq_coind.
adam@354 634 Variable A : Type.
adam@354 635 Variable P : thunk A -> thunk A -> Prop.
adam@354 636
adam@354 637 Hypothesis H : forall m1 m2, P m1 m2
adam@354 638 -> match m1, m2 with
adam@354 639 | Answer x1, Answer x2 => x1 = x2
adam@354 640 | Think m1', Think m2' => P m1' m2'
adam@354 641 | Think m1', _ => P m1' m2
adam@354 642 | _, Think m2' => P m1 m2'
adam@354 643 end.
adam@354 644
adam@354 645 Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
adam@354 646 cofix; intros;
adam@354 647 match goal with
adam@354 648 | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
adam@354 649 end; destruct m1; destruct m2; subst; repeat constructor; auto.
adam@354 650 Qed.
adam@354 651 End thunk_eq_coind.
adam@356 652 (* end hide *)
adam@356 653
adam@356 654 (** 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 655
adam@354 656 Definition frob A (m : thunk A) : thunk A :=
adam@354 657 match m with
adam@354 658 | Answer x => Answer x
adam@354 659 | Think m' => Think m'
adam@354 660 end.
adam@354 661
adam@354 662 Theorem frob_eq : forall A (m : thunk A), frob m = m.
adam@354 663 destruct m; reflexivity.
adam@354 664 Qed.
adam@354 665
adam@356 666 (* begin hide *)
adam@354 667 Theorem thunk_eq_frob : forall A (m1 m2 : thunk A),
adam@354 668 thunk_eq (frob m1) (frob m2)
adam@354 669 -> thunk_eq m1 m2.
adam@354 670 intros; repeat rewrite frob_eq in *; auto.
adam@354 671 Qed.
adam@354 672
adam@354 673 Ltac findDestr := match goal with
adam@354 674 | [ |- context[match ?E with Answer _ => _ | Think _ => _ end] ] =>
adam@354 675 match E with
adam@354 676 | context[match _ with Answer _ => _ | Think _ => _ end] => fail 1
adam@354 677 | _ => destruct E
adam@354 678 end
adam@354 679 end.
adam@354 680
adam@354 681 Theorem thunk_eq_refl : forall A (m : thunk A), thunk_eq m m.
adam@354 682 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = m2)); crush; findDestr; reflexivity.
adam@354 683 Qed.
adam@354 684
adam@354 685 Hint Resolve thunk_eq_refl.
adam@354 686
adam@354 687 Theorem tleft_identity : forall A B (a : A) (f : A -> thunk B),
adam@354 688 thunk_eq (TBind (Answer a) f) (f a).
adam@354 689 intros; apply thunk_eq_frob; crush.
adam@354 690 Qed.
adam@354 691
adam@354 692 Theorem tright_identity : forall A (m : thunk A),
adam@354 693 thunk_eq (TBind m (@Answer _)) m.
adam@354 694 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = TBind m2 (@Answer _))); crush;
adam@354 695 findDestr; reflexivity.
adam@354 696 Qed.
adam@354 697
adam@354 698 Lemma TBind_Answer : forall (A B : Type) (v : A) (m2 : A -> thunk B),
adam@354 699 TBind (Answer v) m2 = m2 v.
adam@354 700 intros; rewrite <- (frob_eq (TBind (Answer v) m2));
adam@354 701 simpl; findDestr; reflexivity.
adam@354 702 Qed.
adam@354 703
adam@375 704 Hint Rewrite TBind_Answer.
adam@354 705
adam@355 706 (** printing exists $\exists$ *)
adam@355 707
adam@354 708 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C),
adam@354 709 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)).
adam@354 710 intros; apply (thunk_eq_coind (fun m1 m2 => (exists m,
adam@354 711 m1 = TBind (TBind m f) g
adam@354 712 /\ m2 = TBind m (fun x => TBind (f x) g))
adam@354 713 \/ m1 = m2)); crush; eauto; repeat (findDestr; crush; eauto).
adam@354 714 Qed.
adam@356 715 (* end hide *)
adam@356 716
adam@356 717 (** As a simple example, here is how we might define a tail-recursive factorial function. *)
adam@354 718
adam@354 719 CoFixpoint fact (n acc : nat) : thunk nat :=
adam@354 720 match n with
adam@354 721 | O => Answer acc
adam@354 722 | S n' => Think (fact n' (S n' * acc))
adam@354 723 end.
adam@354 724
adam@356 725 (** To test our definition, we need an evaluation relation that characterizes results of evaluating [thunk]s. *)
adam@356 726
adam@354 727 Inductive eval A : thunk A -> A -> Prop :=
adam@354 728 | EvalAnswer : forall x, eval (Answer x) x
adam@354 729 | EvalThink : forall m x, eval m x -> eval (Think m) x.
adam@354 730
adam@375 731 Hint Rewrite frob_eq.
adam@354 732
adam@354 733 Lemma eval_frob : forall A (c : thunk A) x,
adam@354 734 eval (frob c) x
adam@354 735 -> eval c x.
adam@354 736 crush.
adam@354 737 Qed.
adam@354 738
adam@354 739 Theorem eval_fact : eval (fact 5 1) 120.
adam@354 740 repeat (apply eval_frob; simpl; constructor).
adam@354 741 Qed.
adam@354 742
adam@356 743 (** We need to apply constructors of [eval] explicitly, but the process is easy to automate completely for concrete input programs.
adam@356 744
adam@357 745 Now consider another very similar definition, this time of a Fibonacci number funtion. *)
adam@357 746
adam@357 747 Notation "x <- m1 ; m2" :=
adam@357 748 (TBind m1 (fun x => m2)) (right associativity, at level 70).
adam@357 749
adam@357 750 (** %\vspace{-.15in}%[[
adam@354 751 CoFixpoint fib (n : nat) : thunk nat :=
adam@354 752 match n with
adam@354 753 | 0 => Answer 1
adam@354 754 | 1 => Answer 1
adam@357 755 | _ => n1 <- fib (pred n);
adam@357 756 n2 <- fib (pred (pred n));
adam@357 757 Answer (n1 + n2)
adam@354 758 end.
adam@354 759 ]]
adam@354 760
adam@356 761 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 762
adam@356 763 %\medskip%
adam@356 764
adam@356 765 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 766
adam@354 767 CoInductive comp (A : Type) : Type :=
adam@354 768 | Ret : A -> comp A
adam@354 769 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.
adam@354 770
adam@356 771 (** This example shows off Coq's support for %\index{recursively non-uniform parameters}\emph{%#<i>#recursively non-uniform parameters#</i>#%}%, 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 772
adam@356 773 It is easy to define the semantics of terminating [comp] computations. *)
adam@356 774
adam@354 775 Inductive exec A : comp A -> A -> Prop :=
adam@354 776 | ExecRet : forall x, exec (Ret x) x
adam@354 777 | ExecBnd : forall B (c : comp B) (f : B -> comp A) x1 x2, exec (A := B) c x1
adam@354 778 -> exec (f x1) x2
adam@354 779 -> exec (Bnd c f) x2.
adam@354 780
adam@356 781 (** 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 782
adam@356 783 (* begin hide *)
adam@354 784 Hint Constructors exec.
adam@354 785
adam@354 786 Definition comp_eq A (c1 c2 : comp A) := forall r, exec c1 r <-> exec c2 r.
adam@354 787
adam@354 788 Ltac inverter := repeat match goal with
adam@354 789 | [ H : exec _ _ |- _ ] => inversion H; []; crush
adam@354 790 end.
adam@354 791
adam@354 792 Theorem cleft_identity : forall A B (a : A) (f : A -> comp B),
adam@354 793 comp_eq (Bnd (Ret a) f) (f a).
adam@354 794 red; crush; inverter; eauto.
adam@354 795 Qed.
adam@354 796
adam@354 797 Theorem cright_identity : forall A (m : comp A),
adam@354 798 comp_eq (Bnd m (@Ret _)) m.
adam@354 799 red; crush; inverter; eauto.
adam@354 800 Qed.
adam@354 801
adam@354 802 Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
adam@354 803 exec c r
adam@354 804 -> forall m, c = Bnd (Bnd m f) g
adam@354 805 -> exec (Bnd m (fun x => Bnd (f x) g)) r.
adam@354 806 induction 1; crush.
adam@354 807 match goal with
adam@354 808 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
adam@354 809 end.
adam@354 810 move H3 after A.
adam@354 811 generalize dependent B0.
adam@354 812 do 2 intro.
adam@354 813 subst.
adam@354 814 crush.
adam@354 815 inversion H; clear H; crush.
adam@354 816 eauto.
adam@354 817 Qed.
adam@354 818
adam@354 819 Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
adam@354 820 exec c r
adam@354 821 -> forall m, c = Bnd m (fun x => Bnd (f x) g)
adam@354 822 -> exec (Bnd (Bnd m f) g) r.
adam@354 823 induction 1; crush.
adam@354 824 match goal with
adam@354 825 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
adam@354 826 end.
adam@354 827 move H3 after B.
adam@354 828 generalize dependent B0.
adam@354 829 do 2 intro.
adam@354 830 subst.
adam@354 831 crush.
adam@354 832 inversion H0; clear H0; crush.
adam@354 833 eauto.
adam@354 834 Qed.
adam@354 835
adam@354 836 Hint Resolve cassociativity1 cassociativity2.
adam@354 837
adam@354 838 Theorem cassociativity : forall A B C (m : comp A) (f : A -> comp B) (g : B -> comp C),
adam@354 839 comp_eq (Bnd (Bnd m f) g) (Bnd m (fun x => Bnd (f x) g)).
adam@354 840 red; crush; eauto.
adam@354 841 Qed.
adam@356 842 (* end hide *)
adam@356 843
adam@356 844 (** 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 845
adam@356 846 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)).
adam@354 847
adam@354 848 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) :=
adam@354 849 if le_lt_dec 2 (length ls)
adam@354 850 then let lss := partition ls in
adam@356 851 ls1 <- mergeSort'' le (fst lss);
adam@356 852 ls2 <- mergeSort'' le (snd lss);
adam@356 853 Ret (merge le ls1 ls2)
adam@354 854 else Ret ls.
adam@354 855
adam@356 856 (** To execute this function, we go through the usual exercise of writing a function to catalyze evaluation of co-recursive calls. *)
adam@356 857
adam@354 858 Definition frob' A (c : comp A) :=
adam@354 859 match c with
adam@354 860 | Ret x => Ret x
adam@354 861 | Bnd _ c' f => Bnd c' f
adam@354 862 end.
adam@354 863
adam@354 864 Lemma exec_frob : forall A (c : comp A) x,
adam@354 865 exec (frob' c) x
adam@354 866 -> exec c x.
adam@356 867 destruct c; crush.
adam@354 868 Qed.
adam@354 869
adam@356 870 (** Now the same sort of proof script that we applied for testing [thunk]s will get the job done. *)
adam@356 871
adam@354 872 Lemma test_mergeSort'' : exec (mergeSort'' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
adam@354 873 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
adam@354 874 repeat (apply exec_frob; simpl; econstructor).
adam@354 875 Qed.
adam@354 876
adam@356 877 (** 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 878
adam@354 879 Definition curriedAdd (n : nat) := Ret (fun m : nat => Ret (n + m)).
adam@354 880
adam@356 881 (** This definition works fine, but we run into trouble when we try to apply it in a trivial way.
adam@356 882 [[
adam@356 883 Definition testCurriedAdd := Bnd (curriedAdd 2) (fun f => f 3).
adam@354 884 ]]
adam@354 885
adam@354 886 <<
adam@354 887 Error: Universe inconsistency.
adam@354 888 >>
adam@356 889
adam@356 890 The problem has to do with rules for inductive definitions that we still 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 891
adam@354 892
adam@357 893 (** * Comparing the Alternatives *)
adam@354 894
adam@356 895 (** 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 terminaton arguments that go beyond Coq's built-in termination checking, so we must turn to subtler points to highlight differences.
adam@356 896
adam@356 897 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 898
adam@356 899 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 900
adam@356 901 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.
adam@356 902
adam@356 903 The first two techniques impose proof obligations that are more basic than terminaton 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 904
adam@356 905 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 906
adam@356 907 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 908
adam@354 909 Definition curriedAdd' (n : nat) := Return (fun m : nat => Return (n + m)).
adam@354 910
adam@356 911 Definition testCurriedAdd := Bind (curriedAdd' 2) (fun f => f 3).
adam@356 912
adam@357 913 (** 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 914
adam@354 915 Fixpoint map A B (f : A -> computation B) (ls : list A) : computation (list B) :=
adam@354 916 match ls with
adam@354 917 | nil => Return nil
adam@354 918 | x :: ls' => Bind (f x) (fun x' =>
adam@354 919 Bind (map f ls') (fun ls'' =>
adam@354 920 Return (x' :: ls'')))
adam@354 921 end.
adam@354 922
adam@355 923 (** remove printing exists *)
adam@356 924 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil))
adam@356 925 (2 :: 3 :: 4 :: nil).
adam@354 926 exists 1; reflexivity.
adam@354 927 Qed.
adam@356 928
adam@356 929 (** One further disadvantage of [comp] is that we cannot prove an inversion lemma for executions of [Bind] without appealing to an %\emph{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 930
adam@357 931 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. *)