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