Mercurial > cpdt > repo

annotate src/GeneralRec.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents a913f19955e2
children
rev   line source
adam@534 1 (* Copyright (c) 2006, 2011-2012, 2015, 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@574 11 Require Import Arith List Lia.
adam@350 12
adam@534 13 Require Import Cpdt.CpdtTactics Cpdt.Coinductive.
adam@350 14
adam@563 15 Require Extraction.
adam@563 16
adam@350 17 Set Implicit Arguments.
adam@534 18 Set Asymmetric Patterns.
adam@350 19 (* end hide *)
adam@350 20
adam@350 21
adam@350 22 (** %\chapter{General Recursion}% *)
adam@350 23
adam@353 24 (** 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 25
adam@424 26 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 27
adam@353 28 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 29
adam@404 30 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 31
adam@351 32
adam@351 33 (** * Well-Founded Recursion *)
adam@351 34
adam@404 35 (** 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 36
adam@351 37 Section mergeSort.
adam@351 38 Variable A : Type.
adam@351 39 Variable le : A -> A -> bool.
adam@475 40
adam@424 41 (** We have a set equipped with some "less-than-or-equal-to" test. *)
adam@351 42
adam@351 43 (** A standard function inserts an element into a sorted list, preserving sortedness. *)
adam@351 44
adam@351 45 Fixpoint insert (x : A) (ls : list A) : list A :=
adam@351 46 match ls with
adam@351 47 | nil => x :: nil
adam@351 48 | h :: ls' =>
adam@351 49 if le x h
adam@351 50 then x :: ls
adam@351 51 else h :: insert x ls'
adam@351 52 end.
adam@351 53
adam@351 54 (** 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 55
adam@351 56 Fixpoint merge (ls1 ls2 : list A) : list A :=
adam@351 57 match ls1 with
adam@351 58 | nil => ls2
adam@351 59 | h :: ls' => insert h (merge ls' ls2)
adam@351 60 end.
adam@351 61
adam@480 62 (** 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 63
adam@480 64 Fixpoint split (ls : list A) : list A * list A :=
adam@351 65 match ls with
adam@351 66 | nil => (nil, nil)
adam@351 67 | h :: nil => (h :: nil, nil)
adam@351 68 | h1 :: h2 :: ls' =>
adam@480 69 let (ls1, ls2) := split ls' in
adam@351 70 (h1 :: ls1, h2 :: ls2)
adam@351 71 end.
adam@351 72
adam@424 73 (** Now, let us try to write the final sorting function, using a natural number "[<=]" test [leb] from the standard library.
adam@351 74 [[
adam@351 75 Fixpoint mergeSort (ls : list A) : list A :=
adam@453 76 if leb (length ls) 1
adam@351 77 then ls
adam@480 78 else let lss := split ls in
adam@351 79 merge (mergeSort (fst lss)) (mergeSort (snd lss)).
adam@351 80 ]]
adam@351 81
adam@351 82 <<
adam@351 83 Recursive call to mergeSort has principal argument equal to
adam@480 84 "fst (split ls)" instead of a subterm of "ls".
adam@351 85 >>
adam@351 86
adam@351 87 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 88
adam@351 89 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 90
adam@351 91 Print well_founded.
adam@351 92 (** %\vspace{-.15in}% [[
adam@351 93 well_founded =
adam@351 94 fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a
adam@351 95 ]]
adam@351 96
adam@404 97 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 98
adam@424 99 (* begin hide *)
adam@437 100 (* begin thide *)
adam@424 101 Definition Acc_intro' := Acc_intro.
adam@437 102 (* end thide *)
adam@424 103 (* end hide *)
adam@424 104
adam@351 105 Print Acc.
adam@351 106 (** %\vspace{-.15in}% [[
adam@351 107 Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
adam@351 108 Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
adam@351 109 ]]
adam@351 110
adam@424 111 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 112
adam@474 113 CoInductive infiniteDecreasingChain A (R : A -> A -> Prop) : stream A -> Prop :=
adam@474 114 | ChainCons : forall x y s, infiniteDecreasingChain R (Cons y s)
adam@351 115 -> R y x
adam@474 116 -> infiniteDecreasingChain R (Cons x (Cons y s)).
adam@351 117
adam@351 118 (** We can now prove that any accessible element cannot be the beginning of any infinite decreasing chain. *)
adam@351 119
adam@351 120 (* begin thide *)
adam@474 121 Lemma noBadChains' : forall A (R : A -> A -> Prop) x, Acc R x
adam@474 122 -> forall s, ~infiniteDecreasingChain R (Cons x s).
adam@351 123 induction 1; crush;
adam@351 124 match goal with
adam@474 125 | [ H : infiniteDecreasingChain _ _ |- _ ] => inversion H; eauto
adam@351 126 end.
adam@351 127 Qed.
adam@351 128
adam@351 129 (** From here, the absence of infinite decreasing chains in well-founded sets is immediate. *)
adam@351 130
adam@474 131 Theorem noBadChains : forall A (R : A -> A -> Prop), well_founded R
adam@474 132 -> forall s, ~infiniteDecreasingChain R s.
adam@474 133 destruct s; apply noBadChains'; auto.
adam@351 134 Qed.
adam@351 135 (* end thide *)
adam@351 136
adam@351 137 (** 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 138
adam@351 139 Check Fix.
adam@351 140 (** %\vspace{-.15in}%[[
adam@351 141 Fix
adam@351 142 : forall (A : Type) (R : A -> A -> Prop),
adam@351 143 well_founded R ->
adam@351 144 forall P : A -> Type,
adam@351 145 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
adam@351 146 forall x : A, P x
adam@351 147 ]]
adam@351 148
adam@351 149 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 150 [[
adam@351 151 forall x : A, (forall y : A, R y x -> P y) -> P x
adam@351 152 ]]
adam@351 153
adam@424 154 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 155
adam@353 156 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 157
adam@351 158 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 159
adam@351 160 Definition lengthOrder (ls1 ls2 : list A) :=
adam@351 161 length ls1 < length ls2.
adam@351 162
adam@353 163 (** 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 164
adam@351 165 Hint Constructors Acc.
adam@574 166 Hint Extern 2 (Acc _ _) => lia.
adam@574 167 Hint Extern 2 (_ <= _) => lia.
adam@574 168
adam@351 169 Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
adam@351 170 unfold lengthOrder; induction len; crush.
adam@351 171 Defined.
adam@351 172
adam@351 173 Theorem lengthOrder_wf : well_founded lengthOrder.
adam@351 174 red; intro; eapply lengthOrder_wf'; eauto.
adam@351 175 Defined.
adam@351 176
adam@514 177 (** 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 178
adam@480 179 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 180
adam@480 181 Lemma split_wf : forall len ls, 2 <= length ls <= len
adam@480 182 -> let (ls1, ls2) := split ls in
adam@351 183 lengthOrder ls1 ls /\ lengthOrder ls2 ls.
adam@351 184 unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush);
adam@351 185 destruct (le_lt_dec 2 (length ls));
adam@351 186 repeat (match goal with
adam@351 187 | [ _ : length ?E < 2 |- _ ] => destruct E
adam@351 188 | [ _ : S (length ?E) < 2 |- _ ] => destruct E
adam@480 189 | [ IH : _ |- context[split ?L] ] =>
adam@480 190 specialize (IH L); destruct (split L); destruct IH
adam@351 191 end; crush).
adam@351 192 Defined.
adam@351 193
adam@480 194 Ltac split_wf := intros ls ?; intros; generalize (@split_wf (length ls) ls);
adam@480 195 destruct (split ls); destruct 1; crush.
adam@351 196
adam@480 197 Lemma split_wf1 : forall ls, 2 <= length ls
adam@480 198 -> lengthOrder (fst (split ls)) ls.
adam@480 199 split_wf.
adam@351 200 Defined.
adam@351 201
adam@480 202 Lemma split_wf2 : forall ls, 2 <= length ls
adam@480 203 -> lengthOrder (snd (split ls)) ls.
adam@480 204 split_wf.
adam@351 205 Defined.
adam@351 206
adam@480 207 Hint Resolve split_wf1 split_wf2.
adam@351 208
adam@453 209 (** 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 210
adam@351 211 Definition mergeSort : list A -> list A.
adam@351 212 (* begin thide *)
adam@351 213 refine (Fix lengthOrder_wf (fun _ => list A)
adam@351 214 (fun (ls : list A)
adam@351 215 (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) =>
adam@351 216 if le_lt_dec 2 (length ls)
adam@480 217 then let lss := split ls in
adam@351 218 merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
adam@351 219 else ls)); subst lss; eauto.
adam@351 220 Defined.
adam@351 221 (* end thide *)
adam@351 222 End mergeSort.
adam@351 223
adam@351 224 (** The important thing is that it is now easy to evaluate calls to [mergeSort]. *)
adam@351 225
adam@351 226 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil).
adam@351 227 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *)
adam@351 228
adam@441 229 (** %\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 230
adam@351 231 (* begin thide *)
adam@351 232 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,
adam@351 233 mergeSort le ls = if le_lt_dec 2 (length ls)
adam@480 234 then let lss := split ls in
adam@351 235 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 236 else ls.
adam@351 237 intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros.
adam@351 238
adam@424 239 (** 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 240
adam@351 241 Check Fix_eq.
adam@351 242 (** %\vspace{-.15in}%[[
adam@351 243 Fix_eq
adam@351 244 : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
adam@351 245 (P : A -> Type)
adam@351 246 (F : forall x : A, (forall y : A, R y x -> P y) -> P x),
adam@351 247 (forall (x : A) (f g : forall y : A, R y x -> P y),
adam@351 248 (forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g) ->
adam@351 249 forall x : A,
adam@351 250 Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)
adam@351 251 ]]
adam@351 252
adam@465 253 Most such obligations are dischargeable with straightforward proof automation, and this example is no exception. *)
adam@351 254
adam@351 255 match goal with
adam@351 256 | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E
adam@351 257 end; simpl; f_equal; auto.
adam@351 258 Qed.
adam@351 259 (* end thide *)
adam@351 260
adam@351 261 (** As a final test of our definition's suitability, we can extract to OCaml. *)
adam@351 262
adam@351 263 Extraction mergeSort.
adam@351 264
adam@351 265 (** <<
adam@351 266 let rec mergeSort le x =
adam@351 267 match le_lt_dec (S (S O)) (length x) with
adam@351 268 | Left ->
adam@480 269 let lss = split x in
adam@351 270 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
adam@351 271 | Right -> x
adam@351 272 >>
adam@351 273
adam@353 274 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 275
adam@351 276 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 277
adam@351 278 Check well_founded_induction.
adam@351 279 (** %\vspace{-.15in}%[[
adam@351 280 well_founded_induction
adam@351 281 : forall (A : Type) (R : A -> A -> Prop),
adam@351 282 well_founded R ->
adam@351 283 forall P : A -> Set,
adam@351 284 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
adam@351 285 forall a : A, P a
adam@351 286 ]]
adam@351 287
adam@351 288 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 289
adam@352 290
adam@354 291 (** * A Non-Termination Monad Inspired by Domain Theory *)
adam@352 292
adam@424 293 (** 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 294
adam@355 295 Consider this definition of a type of computations. *)
adam@355 296
adam@352 297 Section computation.
adam@352 298 Variable A : Type.
adam@355 299 (** The type [A] describes the result a computation will yield, if it terminates.
adam@355 300
adam@355 301 We give a rich dependent type to computations themselves: *)
adam@352 302
adam@352 303 Definition computation :=
adam@352 304 {f : nat -> option A
adam@352 305 | forall (n : nat) (v : A),
adam@352 306 f n = Some v
adam@352 307 -> forall (n' : nat), n' >= n
adam@352 308 -> f n' = Some v}.
adam@352 309
adam@474 310 (** 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 311
adam@355 312 It is easy to define a relation characterizing when a computation runs to a particular result at a particular approximation level. *)
adam@355 313
adam@352 314 Definition runTo (m : computation) (n : nat) (v : A) :=
adam@352 315 proj1_sig m n = Some v.
adam@352 316
adam@355 317 (** On top of [runTo], we also define [run], which is the most abstract notion of when a computation runs to a value. *)
adam@355 318
adam@352 319 Definition run (m : computation) (v : A) :=
adam@352 320 exists n, runTo m n v.
adam@352 321 End computation.
adam@352 322
adam@355 323 (** 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 324 (* begin hide *)
adam@355 325
adam@352 326 Hint Unfold runTo.
adam@352 327
adam@352 328 Ltac run' := unfold run, runTo in *; try red; crush;
adam@352 329 repeat (match goal with
adam@352 330 | [ _ : proj1_sig ?E _ = _ |- _ ] =>
adam@352 331 match goal with
adam@352 332 | [ x : _ |- _ ] =>
adam@352 333 match x with
adam@352 334 | E => destruct E
adam@352 335 end
adam@352 336 end
adam@352 337 | [ |- context[match ?M with exist _ _ => _ end] ] => let Heq := fresh "Heq" in
adam@352 338 case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst
adam@352 339 | [ _ : context[match ?M with exist _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in
adam@352 340 case_eq M; intros ? ? Heq; try rewrite Heq in *; subst
adam@352 341 | [ H : forall n v, ?E n = Some v -> _,
adam@352 342 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] =>
adam@426 343 specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
adam@352 344 | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto
adam@352 345 end; simpl in *); eauto 7.
adam@352 346
adam@352 347 Ltac run := run'; repeat (match goal with
adam@352 348 | [ H : forall n v, ?E n = Some v -> _
adam@352 349 |- context[match ?E ?N with Some _ => _ | None => _ end] ] =>
adam@426 350 specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
adam@352 351 end; run').
adam@352 352
adam@352 353 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P.
adam@352 354 exists 0; auto.
adam@352 355 Qed.
adam@352 356
adam@352 357 Hint Resolve ex_irrelevant.
adam@352 358
adam@352 359 Require Import Max.
adam@352 360
adam@380 361 Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n.
adam@380 362 induction n; destruct m; simpl; intuition;
adam@380 363 specialize (IHn m); intuition.
adam@380 364 Qed.
adam@380 365
adam@352 366 Ltac max := intros n m; generalize (max_spec_le n m); crush.
adam@352 367
adam@352 368 Lemma max_1 : forall n m, max n m >= n.
adam@352 369 max.
adam@352 370 Qed.
adam@352 371
adam@352 372 Lemma max_2 : forall n m, max n m >= m.
adam@352 373 max.
adam@352 374 Qed.
adam@352 375
adam@352 376 Hint Resolve max_1 max_2.
adam@352 377
adam@352 378 Lemma ge_refl : forall n, n >= n.
adam@352 379 crush.
adam@352 380 Qed.
adam@352 381
adam@352 382 Hint Resolve ge_refl.
adam@352 383
adam@352 384 Hint Extern 1 => match goal with
adam@352 385 | [ H : _ = exist _ _ _ |- _ ] => rewrite H
adam@352 386 end.
adam@355 387 (* end hide *)
adam@355 388 (** remove printing exists *)
adam@355 389
adam@480 390 (** 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 391
adam@352 392 Section Bottom.
adam@352 393 Variable A : Type.
adam@352 394
adam@352 395 Definition Bottom : computation A.
adam@352 396 exists (fun _ : nat => @None A); abstract run.
adam@352 397 Defined.
adam@352 398
adam@352 399 Theorem run_Bottom : forall v, ~run Bottom v.
adam@352 400 run.
adam@352 401 Qed.
adam@352 402 End Bottom.
adam@352 403
adam@355 404 (** A slightly more complicated example is [Return], which gives the same terminating answer at every approximation level. *)
adam@355 405
adam@352 406 Section Return.
adam@352 407 Variable A : Type.
adam@352 408 Variable v : A.
adam@352 409
adam@352 410 Definition Return : computation A.
adam@352 411 intros; exists (fun _ : nat => Some v); abstract run.
adam@352 412 Defined.
adam@352 413
adam@352 414 Theorem run_Return : run Return v.
adam@352 415 run.
adam@352 416 Qed.
adam@352 417 End Return.
adam@352 418
adam@474 419 (** 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 420
adam@352 421 Section Bind.
adam@352 422 Variables A B : Type.
adam@352 423 Variable m1 : computation A.
adam@352 424 Variable m2 : A -> computation B.
adam@352 425
adam@352 426 Definition Bind : computation B.
adam@352 427 exists (fun n =>
adam@357 428 let (f1, _) := m1 in
adam@352 429 match f1 n with
adam@352 430 | None => None
adam@352 431 | Some v =>
adam@357 432 let (f2, _) := m2 v in
adam@352 433 f2 n
adam@352 434 end); abstract run.
adam@352 435 Defined.
adam@352 436
adam@352 437 Theorem run_Bind : forall (v1 : A) (v2 : B),
adam@352 438 run m1 v1
adam@352 439 -> run (m2 v1) v2
adam@352 440 -> run Bind v2.
adam@352 441 run; match goal with
adam@352 442 | [ x : nat, y : nat |- _ ] => exists (max x y)
adam@352 443 end; run.
adam@352 444 Qed.
adam@352 445 End Bind.
adam@352 446
adam@355 447 (** A simple notation lets us write [Bind] calls the way they appear in Haskell. *)
adam@352 448
adam@352 449 Notation "x <- m1 ; m2" :=
adam@352 450 (Bind m1 (fun x => m2)) (right associativity, at level 70).
adam@352 451
adam@424 452 (** 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 453
adam@352 454 Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n.
adam@352 455
adam@352 456 Theorem left_identity : forall A B (a : A) (f : A -> computation B),
adam@352 457 meq (Bind (Return a) f) (f a).
adam@352 458 run.
adam@352 459 Qed.
adam@352 460
adam@352 461 Theorem right_identity : forall A (m : computation A),
adam@352 462 meq (Bind m (@Return _)) m.
adam@352 463 run.
adam@352 464 Qed.
adam@352 465
adam@357 466 Theorem associativity : forall A B C (m : computation A)
adam@357 467 (f : A -> computation B) (g : B -> computation C),
adam@352 468 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)).
adam@352 469 run.
adam@352 470 Qed.
adam@352 471
adam@398 472 (** 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 473
adam@352 474 Section lattice.
adam@352 475 Variable A : Type.
adam@352 476
adam@352 477 Definition leq (x y : option A) :=
adam@352 478 forall v, x = Some v -> y = Some v.
adam@352 479 End lattice.
adam@352 480
adam@355 481 (** 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 482
adam@352 483 Section Fix.
adam@475 484
adam@355 485 (** First, we have the function domain and range types. *)
adam@355 486
adam@352 487 Variables A B : Type.
adam@355 488
adam@355 489 (** Next comes the function body, which is written as though it can be parameterized over itself, for recursive calls. *)
adam@355 490
adam@352 491 Variable f : (A -> computation B) -> (A -> computation B).
adam@352 492
adam@355 493 (** 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 494
adam@352 495 Hypothesis f_continuous : forall n v v1 x,
adam@352 496 runTo (f v1 x) n v
adam@352 497 -> forall (v2 : A -> computation B),
adam@352 498 (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n))
adam@352 499 -> runTo (f v2 x) n v.
adam@352 500
adam@355 501 (** 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 502
adam@352 503 Fixpoint Fix' (n : nat) (x : A) : computation B :=
adam@352 504 match n with
adam@352 505 | O => Bottom _
adam@352 506 | S n' => f (Fix' n') x
adam@352 507 end.
adam@352 508
adam@355 509 (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
adam@355 510
adam@574 511 Hint Extern 1 (_ >= _) => lia.
adam@352 512 Hint Unfold leq.
adam@352 513
adam@352 514 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
adam@352 515 -> forall n', n' >= n
adam@352 516 -> proj1_sig (Fix' n' x) steps = Some v.
adam@352 517 unfold runTo in *; induction n; crush;
adam@352 518 match goal with
adam@352 519 | [ H : _ >= _ |- _ ] => inversion H; crush; eauto
adam@352 520 end.
adam@352 521 Qed.
adam@352 522
adam@352 523 Hint Resolve Fix'_ok.
adam@352 524
adam@352 525 Hint Extern 1 (proj1_sig _ _ = _) => simpl;
adam@352 526 match goal with
adam@352 527 | [ |- proj1_sig ?E _ = _ ] => eapply (proj2_sig E)
adam@352 528 end.
adam@352 529
adam@352 530 Definition Fix : A -> computation B.
adam@352 531 intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run.
adam@352 532 Defined.
adam@352 533
adam@355 534 (** Finally, we can prove that [Fix] obeys the expected computation rule. *)
adam@352 535
adam@352 536 Theorem run_Fix : forall x v,
adam@352 537 run (f Fix x) v
adam@352 538 -> run (Fix x) v.
adam@352 539 run; match goal with
adam@352 540 | [ n : nat |- _ ] => exists (S n); eauto
adam@352 541 end.
adam@352 542 Qed.
adam@352 543 End Fix.
adam@352 544
adam@355 545 (* begin hide *)
adam@352 546 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
adam@352 547 -> x = y.
adam@426 548 intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
adam@352 549 Qed.
adam@352 550
adam@352 551 Lemma leq_None : forall A (x y : A), leq (Some x) None
adam@352 552 -> False.
adam@426 553 intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
adam@352 554 Qed.
adam@352 555
adam@355 556 Ltac mergeSort' := run;
adam@355 557 repeat (match goal with
adam@355 558 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
adam@355 559 end; run);
adam@355 560 repeat match goal with
adam@355 561 | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] =>
adam@355 562 match goal with
adam@355 563 | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] =>
adam@355 564 generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro
adam@355 565 end
adam@355 566 end; run; repeat match goal with
adam@355 567 | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst)
adam@355 568 end; auto.
adam@355 569 (* end hide *)
adam@355 570
adam@355 571 (** 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 572
adam@352 573 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A).
adam@352 574 refine (fun A le => Fix
adam@352 575 (fun (mergeSort : list A -> computation (list A))
adam@352 576 (ls : list A) =>
adam@352 577 if le_lt_dec 2 (length ls)
adam@480 578 then let lss := split ls in
adam@352 579 ls1 <- mergeSort (fst lss);
adam@352 580 ls2 <- mergeSort (snd lss);
adam@352 581 Return (merge le ls1 ls2)
adam@355 582 else Return ls) _); abstract mergeSort'.
adam@352 583 Defined.
adam@352 584
adam@424 585 (** 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 586
adam@352 587 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
adam@352 588 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
adam@352 589 exists 4; reflexivity.
adam@352 590 Qed.
adam@352 591
adam@453 592 (** 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 593
adam@355 594 (* begin hide *)
adam@355 595 Ltac looper := unfold leq in *; run;
adam@355 596 repeat match goal with
adam@355 597 | [ x : unit |- _ ] => destruct x
adam@355 598 | [ x : bool |- _ ] => destruct x
adam@355 599 end; auto.
adam@355 600 (* end hide *)
adam@355 601
adam@352 602 Definition looper : bool -> computation unit.
adam@352 603 refine (Fix (fun looper (b : bool) =>
adam@355 604 if b then Return tt else looper b) _); abstract looper.
adam@352 605 Defined.
adam@352 606
adam@352 607 Lemma test_looper : run (looper true) tt.
adam@352 608 exists 1; reflexivity.
adam@352 609 Qed.
adam@354 610
adam@355 611 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level.
adam@355 612
adam@480 613 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 614
adam@354 615
adam@354 616 (** * Co-Inductive Non-Termination Monads *)
adam@354 617
adam@356 618 (** 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 619
adam@356 620 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 621
adam@354 622 CoInductive thunk (A : Type) : Type :=
adam@354 623 | Answer : A -> thunk A
adam@354 624 | Think : thunk A -> thunk A.
adam@354 625
adam@356 626 (** 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 627
adam@424 628 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 629
adam@356 630 CoFixpoint TBind A B (m1 : thunk A) (m2 : A -> thunk B) : thunk B :=
adam@354 631 match m1 with
adam@354 632 | Answer x => m2 x
adam@354 633 | Think m1' => Think (TBind m1' m2)
adam@354 634 end.
adam@354 635
adam@356 636 (** 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 637
adam@356 638 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 639
adam@356 640 (* begin hide *)
adam@354 641 CoInductive thunk_eq A : thunk A -> thunk A -> Prop :=
adam@354 642 | EqAnswer : forall x, thunk_eq (Answer x) (Answer x)
adam@354 643 | EqThinkL : forall m1 m2, thunk_eq m1 m2 -> thunk_eq (Think m1) m2
adam@354 644 | EqThinkR : forall m1 m2, thunk_eq m1 m2 -> thunk_eq m1 (Think m2).
adam@354 645
adam@354 646 Section thunk_eq_coind.
adam@354 647 Variable A : Type.
adam@354 648 Variable P : thunk A -> thunk A -> Prop.
adam@354 649
adam@354 650 Hypothesis H : forall m1 m2, P m1 m2
adam@354 651 -> match m1, m2 with
adam@354 652 | Answer x1, Answer x2 => x1 = x2
adam@354 653 | Think m1', Think m2' => P m1' m2'
adam@354 654 | Think m1', _ => P m1' m2
adam@354 655 | _, Think m2' => P m1 m2'
adam@354 656 end.
adam@354 657
adam@354 658 Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
adam@568 659 cofix thunk_eq_coind; intros;
adam@354 660 match goal with
adam@354 661 | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
adam@354 662 end; destruct m1; destruct m2; subst; repeat constructor; auto.
adam@354 663 Qed.
adam@354 664 End thunk_eq_coind.
adam@356 665 (* end hide *)
adam@356 666
adam@356 667 (** 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 668
adam@354 669 Definition frob A (m : thunk A) : thunk A :=
adam@354 670 match m with
adam@354 671 | Answer x => Answer x
adam@354 672 | Think m' => Think m'
adam@354 673 end.
adam@354 674
adam@354 675 Theorem frob_eq : forall A (m : thunk A), frob m = m.
adam@354 676 destruct m; reflexivity.
adam@354 677 Qed.
adam@354 678
adam@356 679 (* begin hide *)
adam@354 680 Theorem thunk_eq_frob : forall A (m1 m2 : thunk A),
adam@354 681 thunk_eq (frob m1) (frob m2)
adam@354 682 -> thunk_eq m1 m2.
adam@354 683 intros; repeat rewrite frob_eq in *; auto.
adam@354 684 Qed.
adam@354 685
adam@354 686 Ltac findDestr := match goal with
adam@354 687 | [ |- context[match ?E with Answer _ => _ | Think _ => _ end] ] =>
adam@354 688 match E with
adam@354 689 | context[match _ with Answer _ => _ | Think _ => _ end] => fail 1
adam@354 690 | _ => destruct E
adam@354 691 end
adam@354 692 end.
adam@354 693
adam@354 694 Theorem thunk_eq_refl : forall A (m : thunk A), thunk_eq m m.
adam@354 695 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = m2)); crush; findDestr; reflexivity.
adam@354 696 Qed.
adam@354 697
adam@354 698 Hint Resolve thunk_eq_refl.
adam@354 699
adam@354 700 Theorem tleft_identity : forall A B (a : A) (f : A -> thunk B),
adam@354 701 thunk_eq (TBind (Answer a) f) (f a).
adam@354 702 intros; apply thunk_eq_frob; crush.
adam@354 703 Qed.
adam@354 704
adam@354 705 Theorem tright_identity : forall A (m : thunk A),
adam@354 706 thunk_eq (TBind m (@Answer _)) m.
adam@354 707 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = TBind m2 (@Answer _))); crush;
adam@354 708 findDestr; reflexivity.
adam@354 709 Qed.
adam@354 710
adam@354 711 Lemma TBind_Answer : forall (A B : Type) (v : A) (m2 : A -> thunk B),
adam@354 712 TBind (Answer v) m2 = m2 v.
adam@354 713 intros; rewrite <- (frob_eq (TBind (Answer v) m2));
adam@354 714 simpl; findDestr; reflexivity.
adam@354 715 Qed.
adam@354 716
adam@375 717 Hint Rewrite TBind_Answer.
adam@354 718
adam@355 719 (** printing exists $\exists$ *)
adam@355 720
adam@354 721 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C),
adam@354 722 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)).
adam@354 723 intros; apply (thunk_eq_coind (fun m1 m2 => (exists m,
adam@354 724 m1 = TBind (TBind m f) g
adam@354 725 /\ m2 = TBind m (fun x => TBind (f x) g))
adam@354 726 \/ m1 = m2)); crush; eauto; repeat (findDestr; crush; eauto).
adam@354 727 Qed.
adam@356 728 (* end hide *)
adam@356 729
adam@356 730 (** As a simple example, here is how we might define a tail-recursive factorial function. *)
adam@354 731
adam@354 732 CoFixpoint fact (n acc : nat) : thunk nat :=
adam@354 733 match n with
adam@354 734 | O => Answer acc
adam@354 735 | S n' => Think (fact n' (S n' * acc))
adam@354 736 end.
adam@354 737
adam@356 738 (** To test our definition, we need an evaluation relation that characterizes results of evaluating [thunk]s. *)
adam@356 739
adam@354 740 Inductive eval A : thunk A -> A -> Prop :=
adam@354 741 | EvalAnswer : forall x, eval (Answer x) x
adam@354 742 | EvalThink : forall m x, eval m x -> eval (Think m) x.
adam@354 743
adam@375 744 Hint Rewrite frob_eq.
adam@354 745
adam@354 746 Lemma eval_frob : forall A (c : thunk A) x,
adam@354 747 eval (frob c) x
adam@354 748 -> eval c x.
adam@354 749 crush.
adam@354 750 Qed.
adam@354 751
adam@354 752 Theorem eval_fact : eval (fact 5 1) 120.
adam@354 753 repeat (apply eval_frob; simpl; constructor).
adam@354 754 Qed.
adam@354 755
adam@356 756 (** We need to apply constructors of [eval] explicitly, but the process is easy to automate completely for concrete input programs.
adam@356 757
adam@465 758 Now consider another very similar definition, this time of a Fibonacci number function. *)
adam@357 759
adam@357 760 Notation "x <- m1 ; m2" :=
adam@357 761 (TBind m1 (fun x => m2)) (right associativity, at level 70).
adam@357 762
adam@404 763 (* begin hide *)
adam@437 764 (* begin thide *)
adam@424 765 Definition fib := pred.
adam@437 766 (* end thide *)
adam@404 767 (* end hide *)
adam@404 768
adam@453 769 (** %\vspace{-.3in}%[[
adam@354 770 CoFixpoint fib (n : nat) : thunk nat :=
adam@354 771 match n with
adam@354 772 | 0 => Answer 1
adam@354 773 | 1 => Answer 1
adam@357 774 | _ => n1 <- fib (pred n);
adam@357 775 n2 <- fib (pred (pred n));
adam@357 776 Answer (n1 + n2)
adam@354 777 end.
adam@354 778 ]]
adam@354 779
adam@356 780 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 781
adam@356 782 %\medskip%
adam@356 783
adam@424 784 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 785
adam@572 786 Set Universe Polymorphism.
adam@572 787
adam@354 788 CoInductive comp (A : Type) : Type :=
adam@354 789 | Ret : A -> comp A
adam@354 790 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.
adam@354 791
adam@404 792 (** 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 793
adam@356 794 It is easy to define the semantics of terminating [comp] computations. *)
adam@356 795
adam@354 796 Inductive exec A : comp A -> A -> Prop :=
adam@354 797 | ExecRet : forall x, exec (Ret x) x
adam@354 798 | ExecBnd : forall B (c : comp B) (f : B -> comp A) x1 x2, exec (A := B) c x1
adam@354 799 -> exec (f x1) x2
adam@354 800 -> exec (Bnd c f) x2.
adam@354 801
adam@356 802 (** 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 803
adam@356 804 (* begin hide *)
adam@354 805 Hint Constructors exec.
adam@354 806
adam@354 807 Definition comp_eq A (c1 c2 : comp A) := forall r, exec c1 r <-> exec c2 r.
adam@354 808
adam@354 809 Ltac inverter := repeat match goal with
adam@354 810 | [ H : exec _ _ |- _ ] => inversion H; []; crush
adam@354 811 end.
adam@354 812
adam@354 813 Theorem cleft_identity : forall A B (a : A) (f : A -> comp B),
adam@354 814 comp_eq (Bnd (Ret a) f) (f a).
adam@354 815 red; crush; inverter; eauto.
adam@354 816 Qed.
adam@354 817
adam@354 818 Theorem cright_identity : forall A (m : comp A),
adam@354 819 comp_eq (Bnd m (@Ret _)) m.
adam@354 820 red; crush; inverter; eauto.
adam@354 821 Qed.
adam@354 822
adam@354 823 Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
adam@354 824 exec c r
adam@354 825 -> forall m, c = Bnd (Bnd m f) g
adam@354 826 -> exec (Bnd m (fun x => Bnd (f x) g)) r.
adam@354 827 induction 1; crush.
adam@354 828 match goal with
adam@354 829 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
adam@354 830 end.
adam@549 831 try subst B. (* This line expected to fail in Coq 8.4 and succeed in Coq 8.6. *)
adam@354 832 crush.
adam@354 833 inversion H; clear H; crush.
adam@354 834 eauto.
adam@354 835 Qed.
adam@354 836
adam@354 837 Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
adam@354 838 exec c r
adam@354 839 -> forall m, c = Bnd m (fun x => Bnd (f x) g)
adam@354 840 -> exec (Bnd (Bnd m f) g) r.
adam@354 841 induction 1; crush.
adam@354 842 match goal with
adam@354 843 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
adam@354 844 end.
adam@549 845 try subst A. (* Same as above *)
adam@354 846 crush.
adam@354 847 inversion H0; clear H0; crush.
adam@354 848 eauto.
adam@354 849 Qed.
adam@354 850
adam@354 851 Hint Resolve cassociativity1 cassociativity2.
adam@354 852
adam@354 853 Theorem cassociativity : forall A B C (m : comp A) (f : A -> comp B) (g : B -> comp C),
adam@354 854 comp_eq (Bnd (Bnd m f) g) (Bnd m (fun x => Bnd (f x) g)).
adam@354 855 red; crush; eauto.
adam@354 856 Qed.
adam@356 857 (* end hide *)
adam@356 858
adam@469 859 (** 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 860
adam@356 861 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)).
adam@354 862
adam@354 863 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) :=
adam@354 864 if le_lt_dec 2 (length ls)
adam@480 865 then let lss := split ls in
adam@356 866 ls1 <- mergeSort'' le (fst lss);
adam@356 867 ls2 <- mergeSort'' le (snd lss);
adam@356 868 Ret (merge le ls1 ls2)
adam@354 869 else Ret ls.
adam@354 870
adam@356 871 (** To execute this function, we go through the usual exercise of writing a function to catalyze evaluation of co-recursive calls. *)
adam@356 872
adam@354 873 Definition frob' A (c : comp A) :=
adam@354 874 match c with
adam@354 875 | Ret x => Ret x
adam@354 876 | Bnd _ c' f => Bnd c' f
adam@354 877 end.
adam@354 878
adam@354 879 Lemma exec_frob : forall A (c : comp A) x,
adam@354 880 exec (frob' c) x
adam@354 881 -> exec c x.
adam@356 882 destruct c; crush.
adam@354 883 Qed.
adam@354 884
adam@356 885 (** Now the same sort of proof script that we applied for testing [thunk]s will get the job done. *)
adam@356 886
adam@354 887 Lemma test_mergeSort'' : exec (mergeSort'' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
adam@354 888 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
adam@354 889 repeat (apply exec_frob; simpl; econstructor).
adam@354 890 Qed.
adam@354 891
adam@356 892 (** 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 893
adam@354 894 Definition curriedAdd (n : nat) := Ret (fun m : nat => Ret (n + m)).
adam@354 895
adam@356 896 (** This definition works fine, but we run into trouble when we try to apply it in a trivial way.
adam@356 897 [[
adam@356 898 Definition testCurriedAdd := Bnd (curriedAdd 2) (fun f => f 3).
adam@354 899 ]]
adam@354 900
adam@354 901 <<
adam@354 902 Error: Universe inconsistency.
adam@354 903 >>
adam@356 904
adam@496 905 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 906
adam@354 907
adam@357 908 (** * Comparing the Alternatives *)
adam@354 909
adam@453 910 (** 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 911
adam@356 912 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 913
adam@356 914 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 915
adam@480 916 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 917
adam@465 918 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 919
adam@356 920 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 921
adam@356 922 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 923
adam@354 924 Definition curriedAdd' (n : nat) := Return (fun m : nat => Return (n + m)).
adam@354 925
adam@356 926 Definition testCurriedAdd := Bind (curriedAdd' 2) (fun f => f 3).
adam@356 927
adam@357 928 (** 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 929
adam@354 930 Fixpoint map A B (f : A -> computation B) (ls : list A) : computation (list B) :=
adam@354 931 match ls with
adam@354 932 | nil => Return nil
adam@354 933 | x :: ls' => Bind (f x) (fun x' =>
adam@354 934 Bind (map f ls') (fun ls'' =>
adam@354 935 Return (x' :: ls'')))
adam@354 936 end.
adam@354 937
adam@355 938 (** remove printing exists *)
adam@356 939 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil))
adam@356 940 (2 :: 3 :: 4 :: nil).
adam@354 941 exists 1; reflexivity.
adam@354 942 Qed.
adam@356 943
adam@524 944 (** 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 945
adam@357 946 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. *)