adam@350
|
1 (* Copyright (c) 2006, 2011, Adam Chlipala
|
adam@350
|
2 *
|
adam@350
|
3 * This work is licensed under a
|
adam@350
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adam@350
|
5 * Unported License.
|
adam@350
|
6 * The license text is available at:
|
adam@350
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adam@350
|
8 *)
|
adam@350
|
9
|
adam@350
|
10 (* begin hide *)
|
adam@351
|
11 Require Import Arith List.
|
adam@350
|
12
|
adam@351
|
13 Require Import CpdtTactics Coinductive.
|
adam@350
|
14
|
adam@350
|
15 Set Implicit Arguments.
|
adam@350
|
16 (* end hide *)
|
adam@350
|
17
|
adam@350
|
18
|
adam@350
|
19 (** %\chapter{General Recursion}% *)
|
adam@350
|
20
|
adam@353
|
21 (** Termination of all programs is a crucial property of Gallina. Non-terminating programs introduce logical inconsistency, where any theorem can be proved with an infinite loop. Coq uses a small set of conservative, syntactic criteria to check termination of all recursive definitions. These criteria are insufficient to support the natural encodings of a variety of important programming idioms. Further, since Coq makes it so convenient to encode mathematics computationally, with functional programs, we may find ourselves wanting to employ more complicated recursion in mathematical definitions.
|
adam@351
|
22
|
adam@353
|
23 What exactly are the conservative criteria that we run up against? For %\emph{%#<i>#recursive#</i>#%}% definitions, recursive calls are only allowed on %\emph{%#<i>#syntactic subterms#</i>#%}% of the original primary argument, a restriction known as %\index{primitive recursion}\emph{%#<i>#primitive recursion#</i>#%}%. In fact, Coq's handling of reflexive inductive types (those defined in terms of functions returning the same type) gives a bit more flexibility than in traditional primitive recursion, but the term is still applied commonly. In Chapter 5, we saw how %\emph{%#<i>#co-recursive#</i>#%}% definitions are checked against a syntactic guardness condition that guarantees productivity.
|
adam@351
|
24
|
adam@353
|
25 Many natural recursion patterns satisfy neither condition. For instance, there is our simple running example in this chapter, merge sort. We will study three different approaches to more flexible recursion, and the latter two of the approaches will even support definitions that may fail to terminate on certain inputs, without any up-front characterization of which inputs those may be.
|
adam@351
|
26
|
adam@353
|
27 Before proceeding, it is important to note that the problem here is not as fundamental as it may appear. The final example of Chapter 5 demonstrated what is called a %\index{deep embedding}\emph{%#<i>#deep embedding#</i>#%}% of the syntax and semantics of a programming language. That is, we gave a mathematical definition of a language of programs and their meanings. This language clearly admitted non-termination, and we could think of writing all our sophisticated recursive functions with such explicit syntax types. However, in doing so, we forfeit our chance to take advantage of Coq's very good built-in support for reasoning about Gallina programs. We would rather use a %\index{shallow embedding}\emph{%#<i>#shallow embedding#</i>#%}%, where we model informal constructs by encoding them as normal Gallina programs. Each of the three techniques of this chapter follows that style. *)
|
adam@351
|
28
|
adam@351
|
29
|
adam@351
|
30 (** * Well-Founded Recursion *)
|
adam@351
|
31
|
adam@351
|
32 (** The essence of terminating recursion is that there are no infinite chains of nested recursive calls. This intuition is commonly mapped to the mathematical idea of a %\index{well-founded relation}\emph{%#<i>#well-founded relation#</i>#%}%, and the associated standard technique in Coq is %\index{well-founded recursion}\emph{%#<i>#well-founded recursion#</i>#%}%. The syntactic-subterm relation that Coq applies by default is well-founded, but many cases demand alternate well-founded relations. To demonstrate, let us see where we get stuck on attempting a standard merge sort implementation. *)
|
adam@351
|
33
|
adam@351
|
34 Section mergeSort.
|
adam@351
|
35 Variable A : Type.
|
adam@351
|
36 Variable le : A -> A -> bool.
|
adam@351
|
37 (** We have a set equipped with some %``%#"#less-than-or-equal-to#"#%''% test. *)
|
adam@351
|
38
|
adam@351
|
39 (** A standard function inserts an element into a sorted list, preserving sortedness. *)
|
adam@351
|
40
|
adam@351
|
41 Fixpoint insert (x : A) (ls : list A) : list A :=
|
adam@351
|
42 match ls with
|
adam@351
|
43 | nil => x :: nil
|
adam@351
|
44 | h :: ls' =>
|
adam@351
|
45 if le x h
|
adam@351
|
46 then x :: ls
|
adam@351
|
47 else h :: insert x ls'
|
adam@351
|
48 end.
|
adam@351
|
49
|
adam@351
|
50 (** We will also need a function to merge two sorted lists. (We use a less efficient implementation than usual, because the more efficient implementation already forces us to think about well-founded recursion, while here we are only interested in setting up the example of merge sort.) *)
|
adam@351
|
51
|
adam@351
|
52 Fixpoint merge (ls1 ls2 : list A) : list A :=
|
adam@351
|
53 match ls1 with
|
adam@351
|
54 | nil => ls2
|
adam@351
|
55 | h :: ls' => insert h (merge ls' ls2)
|
adam@351
|
56 end.
|
adam@351
|
57
|
adam@351
|
58 (** The last helper function for classic merge sort is the one that follows, to partition a list arbitrarily into two pieces of approximately equal length. *)
|
adam@351
|
59
|
adam@351
|
60 Fixpoint partition (ls : list A) : list A * list A :=
|
adam@351
|
61 match ls with
|
adam@351
|
62 | nil => (nil, nil)
|
adam@351
|
63 | h :: nil => (h :: nil, nil)
|
adam@351
|
64 | h1 :: h2 :: ls' =>
|
adam@351
|
65 let (ls1, ls2) := partition ls' in
|
adam@351
|
66 (h1 :: ls1, h2 :: ls2)
|
adam@351
|
67 end.
|
adam@351
|
68
|
adam@351
|
69 (** Now, let us try to write the final sorting function, using a natural number %``%#"#[<=]#"#%''% test [leb] from the standard library.
|
adam@351
|
70 [[
|
adam@351
|
71 Fixpoint mergeSort (ls : list A) : list A :=
|
adam@351
|
72 if leb (length ls) 2
|
adam@351
|
73 then ls
|
adam@351
|
74 else let lss := partition ls in
|
adam@351
|
75 merge (mergeSort (fst lss)) (mergeSort (snd lss)).
|
adam@351
|
76 ]]
|
adam@351
|
77
|
adam@351
|
78 <<
|
adam@351
|
79 Recursive call to mergeSort has principal argument equal to
|
adam@351
|
80 "fst (partition ls)" instead of a subterm of "ls".
|
adam@351
|
81 >>
|
adam@351
|
82
|
adam@351
|
83 The definition is rejected for not following the simple primitive recursion criterion. In particular, it is not apparent that recursive calls to [mergeSort] are syntactic subterms of the original argument [ls]; indeed, they are not, yet we know this is a well-founded recursive definition.
|
adam@351
|
84
|
adam@351
|
85 To produce an acceptable definition, we need to choose a well-founded relation and prove that [mergeSort] respects it. A good starting point is an examination of how well-foundedness is formalized in the Coq standard library. *)
|
adam@351
|
86
|
adam@351
|
87 Print well_founded.
|
adam@351
|
88 (** %\vspace{-.15in}% [[
|
adam@351
|
89 well_founded =
|
adam@351
|
90 fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a
|
adam@351
|
91 ]]
|
adam@351
|
92
|
adam@351
|
93 The bulk of the definitional work devolves to the %\index{accessibility relation}\index{Gallina terms!Acc}\emph{%#<i>#accessibility#</i>#%}% relation [Acc], whose definition we may also examine. *)
|
adam@351
|
94
|
adam@351
|
95 Print Acc.
|
adam@351
|
96 (** %\vspace{-.15in}% [[
|
adam@351
|
97 Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
|
adam@351
|
98 Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
|
adam@351
|
99 ]]
|
adam@351
|
100
|
adam@353
|
101 In prose, an element [x] is accessible for a relation [R] if every element %``%#"#less than#"#%''% [x] according to [R] is also accessible. Since [Acc] is defined inductively, we know that any accessibility proof involves a finite chain of invocations, in a certain sense which we can make formal. Building on Chapter 5's examples, let us define a co-inductive relation that is closer to the usual informal notion of %``%#"#absence of infinite decreasing chains.#"#%''% *)
|
adam@351
|
102
|
adam@351
|
103 CoInductive isChain A (R : A -> A -> Prop) : stream A -> Prop :=
|
adam@351
|
104 | ChainCons : forall x y s, isChain R (Cons y s)
|
adam@351
|
105 -> R y x
|
adam@351
|
106 -> isChain R (Cons x (Cons y s)).
|
adam@351
|
107
|
adam@351
|
108 (** We can now prove that any accessible element cannot be the beginning of any infinite decreasing chain. *)
|
adam@351
|
109
|
adam@351
|
110 (* begin thide *)
|
adam@351
|
111 Lemma noChains' : forall A (R : A -> A -> Prop) x, Acc R x
|
adam@351
|
112 -> forall s, ~isChain R (Cons x s).
|
adam@351
|
113 induction 1; crush;
|
adam@351
|
114 match goal with
|
adam@351
|
115 | [ H : isChain _ _ |- _ ] => inversion H; eauto
|
adam@351
|
116 end.
|
adam@351
|
117 Qed.
|
adam@351
|
118
|
adam@351
|
119 (** From here, the absence of infinite decreasing chains in well-founded sets is immediate. *)
|
adam@351
|
120
|
adam@351
|
121 Theorem noChains : forall A (R : A -> A -> Prop), well_founded R
|
adam@351
|
122 -> forall s, ~isChain R s.
|
adam@351
|
123 destruct s; apply noChains'; auto.
|
adam@351
|
124 Qed.
|
adam@351
|
125 (* end thide *)
|
adam@351
|
126
|
adam@351
|
127 (** Absence of infinite decreasing chains implies absence of infinitely nested recursive calls, for any recursive definition that respects the well-founded relation. The [Fix] combinator from the standard library formalizes that intuition: *)
|
adam@351
|
128
|
adam@351
|
129 Check Fix.
|
adam@351
|
130 (** %\vspace{-.15in}%[[
|
adam@351
|
131 Fix
|
adam@351
|
132 : forall (A : Type) (R : A -> A -> Prop),
|
adam@351
|
133 well_founded R ->
|
adam@351
|
134 forall P : A -> Type,
|
adam@351
|
135 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
|
adam@351
|
136 forall x : A, P x
|
adam@351
|
137 ]]
|
adam@351
|
138
|
adam@351
|
139 A call to %\index{Gallina terms!Fix}%[Fix] must present a relation [R] and a proof of its well-foundedness. The next argument, [P], is the possibly dependent range type of the function we build; the domain [A] of [R] is the function's domain. The following argument has this type:
|
adam@351
|
140
|
adam@351
|
141 [[
|
adam@351
|
142 forall x : A, (forall y : A, R y x -> P y) -> P x
|
adam@351
|
143 ]]
|
adam@351
|
144
|
adam@351
|
145 This is an encoding of the function body. The input [x] stands for the function argument, and the next input stands for the function we are defining. Recursive calls are encoded as calls to the second argument, whose type tells us it expects a value [y] and a proof that [y] is %``%#"#less than#"#%''% [x], according to [R]. In this way, we enforce the well-foundedness restriction on recursive calls.
|
adam@351
|
146
|
adam@353
|
147 The rest of [Fix]'s type tells us that it returns a function of exactly the type we expect, so we are now ready to use it to implement [mergeSort]. Careful readers may have noticed that [Fix] has a dependent type of the sort we met in the previous chapter.
|
adam@351
|
148
|
adam@351
|
149 Before writing [mergeSort], we need to settle on a well-founded relation. The right one for this example is based on lengths of lists. *)
|
adam@351
|
150
|
adam@351
|
151 Definition lengthOrder (ls1 ls2 : list A) :=
|
adam@351
|
152 length ls1 < length ls2.
|
adam@351
|
153
|
adam@353
|
154 (** 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
|
155
|
adam@351
|
156 Hint Constructors Acc.
|
adam@351
|
157
|
adam@351
|
158 Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
|
adam@351
|
159 unfold lengthOrder; induction len; crush.
|
adam@351
|
160 Defined.
|
adam@351
|
161
|
adam@351
|
162 Theorem lengthOrder_wf : well_founded lengthOrder.
|
adam@351
|
163 red; intro; eapply lengthOrder_wf'; eauto.
|
adam@351
|
164 Defined.
|
adam@351
|
165
|
adam@353
|
166 (** Notice that we end these proofs with %\index{Vernacular commands!Defined}%[Defined], not [Qed]. Recall that [Defined] marks the theorems as %\emph{transparent}%, so that the details of their proofs may be used during program execution. Why could such details possibly matter for computation? It turns out that [Fix] satisfies the primitive recursion restriction by declaring itself as %\emph{%#<i>#recursive in the structure of [Acc] proofs#</i>#%}%. This is possible because [Acc] proofs follow a predictable inductive structure. We must do work, as in the last theorem's proof, to establish that all elements of a type belong to [Acc], but the automatic unwinding of those proofs during recursion is straightforward. If we ended the proof with [Qed], the proof details would be hidden from computation, in which case the unwinding process would get stuck.
|
adam@351
|
167
|
adam@351
|
168 To justify our two recursive [mergeSort] calls, we will also need to prove that [partition] respects the [lengthOrder] relation. These proofs, too, must be kept transparent, to avoid stuckness of [Fix] evaluation. *)
|
adam@351
|
169
|
adam@351
|
170 Lemma partition_wf : forall len ls, 2 <= length ls <= len
|
adam@351
|
171 -> let (ls1, ls2) := partition ls in
|
adam@351
|
172 lengthOrder ls1 ls /\ lengthOrder ls2 ls.
|
adam@351
|
173 unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush);
|
adam@351
|
174 destruct (le_lt_dec 2 (length ls));
|
adam@351
|
175 repeat (match goal with
|
adam@351
|
176 | [ _ : length ?E < 2 |- _ ] => destruct E
|
adam@351
|
177 | [ _ : S (length ?E) < 2 |- _ ] => destruct E
|
adam@351
|
178 | [ IH : _ |- context[partition ?L] ] =>
|
adam@351
|
179 specialize (IH L); destruct (partition L); destruct IH
|
adam@351
|
180 end; crush).
|
adam@351
|
181 Defined.
|
adam@351
|
182
|
adam@351
|
183 Ltac partition := intros ls ?; intros; generalize (@partition_wf (length ls) ls);
|
adam@351
|
184 destruct (partition ls); destruct 1; crush.
|
adam@351
|
185
|
adam@351
|
186 Lemma partition_wf1 : forall ls, 2 <= length ls
|
adam@351
|
187 -> lengthOrder (fst (partition ls)) ls.
|
adam@351
|
188 partition.
|
adam@351
|
189 Defined.
|
adam@351
|
190
|
adam@351
|
191 Lemma partition_wf2 : forall ls, 2 <= length ls
|
adam@351
|
192 -> lengthOrder (snd (partition ls)) ls.
|
adam@351
|
193 partition.
|
adam@351
|
194 Defined.
|
adam@351
|
195
|
adam@351
|
196 Hint Resolve partition_wf1 partition_wf2.
|
adam@351
|
197
|
adam@353
|
198 (** To write the function definition itself, we use the %\index{tactics!refine}%[refine] tactic as a convenient way to write a program that needs to manipulate proofs, without writing out those proofs manually. We also use a replacement [le_lt_dec] for [leb] that has a more interesting dependent type. *)
|
adam@351
|
199
|
adam@351
|
200 Definition mergeSort : list A -> list A.
|
adam@351
|
201 (* begin thide *)
|
adam@351
|
202 refine (Fix lengthOrder_wf (fun _ => list A)
|
adam@351
|
203 (fun (ls : list A)
|
adam@351
|
204 (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) =>
|
adam@351
|
205 if le_lt_dec 2 (length ls)
|
adam@351
|
206 then let lss := partition ls in
|
adam@351
|
207 merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
|
adam@351
|
208 else ls)); subst lss; eauto.
|
adam@351
|
209 Defined.
|
adam@351
|
210 (* end thide *)
|
adam@351
|
211 End mergeSort.
|
adam@351
|
212
|
adam@351
|
213 (** The important thing is that it is now easy to evaluate calls to [mergeSort]. *)
|
adam@351
|
214
|
adam@351
|
215 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil).
|
adam@351
|
216 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *)
|
adam@351
|
217
|
adam@351
|
218 (** Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *)
|
adam@351
|
219
|
adam@351
|
220 (* begin thide *)
|
adam@351
|
221 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,
|
adam@351
|
222 mergeSort le ls = if le_lt_dec 2 (length ls)
|
adam@351
|
223 then let lss := partition ls in
|
adam@351
|
224 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
|
adam@351
|
225 else ls.
|
adam@351
|
226 intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros.
|
adam@351
|
227
|
adam@351
|
228 (** The library theorem [Fix_eq] imposes one more strange subgoal upon us. We must prove that the function body is unable to distinguish between %``%#"#self#"#%''% arguments that map equal inputs to equal outputs. One might think this should be true of any Gallina code, but in fact this general %\index{extensionality}\emph{%#<i>#function extensionality#</i>#%}% property is neither provable nor disprovable within Coq. The type of [Fix_eq] makes clear what we must show manually: *)
|
adam@351
|
229
|
adam@351
|
230 Check Fix_eq.
|
adam@351
|
231 (** %\vspace{-.15in}%[[
|
adam@351
|
232 Fix_eq
|
adam@351
|
233 : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
|
adam@351
|
234 (P : A -> Type)
|
adam@351
|
235 (F : forall x : A, (forall y : A, R y x -> P y) -> P x),
|
adam@351
|
236 (forall (x : A) (f g : forall y : A, R y x -> P y),
|
adam@351
|
237 (forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g) ->
|
adam@351
|
238 forall x : A,
|
adam@351
|
239 Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)
|
adam@351
|
240 ]]
|
adam@351
|
241
|
adam@351
|
242 Most such obligations are dischargable with straightforward proof automation, and this example is no exception. *)
|
adam@351
|
243
|
adam@351
|
244 match goal with
|
adam@351
|
245 | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E
|
adam@351
|
246 end; simpl; f_equal; auto.
|
adam@351
|
247 Qed.
|
adam@351
|
248 (* end thide *)
|
adam@351
|
249
|
adam@351
|
250 (** As a final test of our definition's suitability, we can extract to OCaml. *)
|
adam@351
|
251
|
adam@351
|
252 Extraction mergeSort.
|
adam@351
|
253
|
adam@351
|
254 (** <<
|
adam@351
|
255 let rec mergeSort le x =
|
adam@351
|
256 match le_lt_dec (S (S O)) (length x) with
|
adam@351
|
257 | Left ->
|
adam@351
|
258 let lss = partition x in
|
adam@351
|
259 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
|
adam@351
|
260 | Right -> x
|
adam@351
|
261 >>
|
adam@351
|
262
|
adam@353
|
263 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
|
264
|
adam@351
|
265 One more piece of the full picture is missing. To go on and prove correctness of [mergeSort], we would need more than a way of unfolding its definition. We also need an appropriate induction principle matched to the well-founded relation. Such a principle is available in the standard library, though we will say no more about its details here. *)
|
adam@351
|
266
|
adam@351
|
267 Check well_founded_induction.
|
adam@351
|
268 (** %\vspace{-.15in}%[[
|
adam@351
|
269 well_founded_induction
|
adam@351
|
270 : forall (A : Type) (R : A -> A -> Prop),
|
adam@351
|
271 well_founded R ->
|
adam@351
|
272 forall P : A -> Set,
|
adam@351
|
273 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
|
adam@351
|
274 forall a : A, P a
|
adam@351
|
275 ]]
|
adam@351
|
276
|
adam@351
|
277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *)
|
adam@352
|
278
|
adam@352
|
279
|
adam@354
|
280 (** * A Non-Termination Monad Inspired by Domain Theory *)
|
adam@352
|
281
|
adam@355
|
282 (** The key insights of %\index{domain theory}%domain theory%~\cite{WinskelDomains}% inspire the next approach to modeling non-termination. Domain theory is based on %\emph{%#<i>#information orders#</i>#%}% that relate values representing computatiion results, according to how much information these values convey. For instance, a simple domain might include values %``%#"#the program does not terminate#"#%''% and %``%#"#the program terminates with the answer 5.#"#%''% The former is considered to be an %\emph{%#<i>#approximation#</i>#%}% of the latter, while the latter is %\emph{%#<i>#not#</i>#%}% an approximation of %``%#"#the program terminates with the answer 6.#"#%''% The details of domain theory will not be important in what follows; we merely borrow the notion of an approximation ordering on computation results.
|
adam@355
|
283
|
adam@355
|
284 Consider this definition of a type of computations. *)
|
adam@355
|
285
|
adam@352
|
286 Section computation.
|
adam@352
|
287 Variable A : Type.
|
adam@355
|
288 (** The type [A] describes the result a computation will yield, if it terminates.
|
adam@355
|
289
|
adam@355
|
290 We give a rich dependent type to computations themselves: *)
|
adam@352
|
291
|
adam@352
|
292 Definition computation :=
|
adam@352
|
293 {f : nat -> option A
|
adam@352
|
294 | forall (n : nat) (v : A),
|
adam@352
|
295 f n = Some v
|
adam@352
|
296 -> forall (n' : nat), n' >= n
|
adam@352
|
297 -> f n' = Some v}.
|
adam@352
|
298
|
adam@355
|
299 (** A computation is fundamentally a function [f] from an %\emph{%#<i>#approximation level#</i>#%}% [n] to an optional result. Intuitively, higher [n] values enable termination in more cases than lower values. A call to [f] may return [None] to indicate that [n] was not high enough to run the computation to completion; higher [n] values may yield [Some]. Further, the proof obligation within the sigma type asserts that [f] is %\emph{%#<i>#monotone#</i>#%}% in an appropriate sense: when some [n] is sufficient to produce termination, so are all higher [n] values, and they all yield the same program result [v].
|
adam@355
|
300
|
adam@355
|
301 It is easy to define a relation characterizing when a computation runs to a particular result at a particular approximation level. *)
|
adam@355
|
302
|
adam@352
|
303 Definition runTo (m : computation) (n : nat) (v : A) :=
|
adam@352
|
304 proj1_sig m n = Some v.
|
adam@352
|
305
|
adam@355
|
306 (** On top of [runTo], we also define [run], which is the most abstract notion of when a computation runs to a value. *)
|
adam@355
|
307
|
adam@352
|
308 Definition run (m : computation) (v : A) :=
|
adam@352
|
309 exists n, runTo m n v.
|
adam@352
|
310 End computation.
|
adam@352
|
311
|
adam@355
|
312 (** 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
|
313 (* begin hide *)
|
adam@355
|
314
|
adam@352
|
315 Hint Unfold runTo.
|
adam@352
|
316
|
adam@352
|
317 Ltac run' := unfold run, runTo in *; try red; crush;
|
adam@352
|
318 repeat (match goal with
|
adam@352
|
319 | [ _ : proj1_sig ?E _ = _ |- _ ] =>
|
adam@352
|
320 match goal with
|
adam@352
|
321 | [ x : _ |- _ ] =>
|
adam@352
|
322 match x with
|
adam@352
|
323 | E => destruct E
|
adam@352
|
324 end
|
adam@352
|
325 end
|
adam@352
|
326 | [ |- context[match ?M with exist _ _ => _ end] ] => let Heq := fresh "Heq" in
|
adam@352
|
327 case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst
|
adam@352
|
328 | [ _ : context[match ?M with exist _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in
|
adam@352
|
329 case_eq M; intros ? ? Heq; try rewrite Heq in *; subst
|
adam@352
|
330 | [ H : forall n v, ?E n = Some v -> _,
|
adam@352
|
331 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] =>
|
adam@352
|
332 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
|
adam@352
|
333 | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto
|
adam@352
|
334 end; simpl in *); eauto 7.
|
adam@352
|
335
|
adam@352
|
336 Ltac run := run'; repeat (match goal with
|
adam@352
|
337 | [ H : forall n v, ?E n = Some v -> _
|
adam@352
|
338 |- context[match ?E ?N with Some _ => _ | None => _ end] ] =>
|
adam@352
|
339 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
|
adam@352
|
340 end; run').
|
adam@352
|
341
|
adam@352
|
342 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P.
|
adam@352
|
343 exists 0; auto.
|
adam@352
|
344 Qed.
|
adam@352
|
345
|
adam@352
|
346 Hint Resolve ex_irrelevant.
|
adam@352
|
347
|
adam@352
|
348 Require Import Max.
|
adam@352
|
349
|
adam@352
|
350 Ltac max := intros n m; generalize (max_spec_le n m); crush.
|
adam@352
|
351
|
adam@352
|
352 Lemma max_1 : forall n m, max n m >= n.
|
adam@352
|
353 max.
|
adam@352
|
354 Qed.
|
adam@352
|
355
|
adam@352
|
356 Lemma max_2 : forall n m, max n m >= m.
|
adam@352
|
357 max.
|
adam@352
|
358 Qed.
|
adam@352
|
359
|
adam@352
|
360 Hint Resolve max_1 max_2.
|
adam@352
|
361
|
adam@352
|
362 Lemma ge_refl : forall n, n >= n.
|
adam@352
|
363 crush.
|
adam@352
|
364 Qed.
|
adam@352
|
365
|
adam@352
|
366 Hint Resolve ge_refl.
|
adam@352
|
367
|
adam@352
|
368 Hint Extern 1 => match goal with
|
adam@352
|
369 | [ H : _ = exist _ _ _ |- _ ] => rewrite H
|
adam@352
|
370 end.
|
adam@355
|
371 (* end hide *)
|
adam@355
|
372 (** remove printing exists *)
|
adam@355
|
373
|
adam@355
|
374 (** 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, opauqe proofs are fine here, since the proof components of computations do not influence evaluation behavior. *)
|
adam@352
|
375
|
adam@352
|
376 Section Bottom.
|
adam@352
|
377 Variable A : Type.
|
adam@352
|
378
|
adam@352
|
379 Definition Bottom : computation A.
|
adam@352
|
380 exists (fun _ : nat => @None A); abstract run.
|
adam@352
|
381 Defined.
|
adam@352
|
382
|
adam@352
|
383 Theorem run_Bottom : forall v, ~run Bottom v.
|
adam@352
|
384 run.
|
adam@352
|
385 Qed.
|
adam@352
|
386 End Bottom.
|
adam@352
|
387
|
adam@355
|
388 (** A slightly more complicated example is [Return], which gives the same terminating answer at every approximation level. *)
|
adam@355
|
389
|
adam@352
|
390 Section Return.
|
adam@352
|
391 Variable A : Type.
|
adam@352
|
392 Variable v : A.
|
adam@352
|
393
|
adam@352
|
394 Definition Return : computation A.
|
adam@352
|
395 intros; exists (fun _ : nat => Some v); abstract run.
|
adam@352
|
396 Defined.
|
adam@352
|
397
|
adam@352
|
398 Theorem run_Return : run Return v.
|
adam@352
|
399 run.
|
adam@352
|
400 Qed.
|
adam@352
|
401 End Return.
|
adam@352
|
402
|
adam@355
|
403 (** The name [Return] was meant to be suggestive of the standard operations of 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
|
404
|
adam@352
|
405 Section Bind.
|
adam@352
|
406 Variables A B : Type.
|
adam@352
|
407 Variable m1 : computation A.
|
adam@352
|
408 Variable m2 : A -> computation B.
|
adam@352
|
409
|
adam@352
|
410 Definition Bind : computation B.
|
adam@352
|
411 exists (fun n =>
|
adam@352
|
412 let (f1, Hf1) := m1 in
|
adam@352
|
413 match f1 n with
|
adam@352
|
414 | None => None
|
adam@352
|
415 | Some v =>
|
adam@352
|
416 let (f2, Hf2) := m2 v in
|
adam@352
|
417 f2 n
|
adam@352
|
418 end); abstract run.
|
adam@352
|
419 Defined.
|
adam@352
|
420
|
adam@352
|
421 Theorem run_Bind : forall (v1 : A) (v2 : B),
|
adam@352
|
422 run m1 v1
|
adam@352
|
423 -> run (m2 v1) v2
|
adam@352
|
424 -> run Bind v2.
|
adam@352
|
425 run; match goal with
|
adam@352
|
426 | [ x : nat, y : nat |- _ ] => exists (max x y)
|
adam@352
|
427 end; run.
|
adam@352
|
428 Qed.
|
adam@352
|
429 End Bind.
|
adam@352
|
430
|
adam@355
|
431 (** A simple notation lets us write [Bind] calls the way they appear in Haskell. *)
|
adam@352
|
432
|
adam@352
|
433 Notation "x <- m1 ; m2" :=
|
adam@352
|
434 (Bind m1 (fun x => m2)) (right associativity, at level 70).
|
adam@352
|
435
|
adam@355
|
436 (** 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
|
437
|
adam@352
|
438 Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n.
|
adam@352
|
439
|
adam@352
|
440 Theorem left_identity : forall A B (a : A) (f : A -> computation B),
|
adam@352
|
441 meq (Bind (Return a) f) (f a).
|
adam@352
|
442 run.
|
adam@352
|
443 Qed.
|
adam@352
|
444
|
adam@352
|
445 Theorem right_identity : forall A (m : computation A),
|
adam@352
|
446 meq (Bind m (@Return _)) m.
|
adam@352
|
447 run.
|
adam@352
|
448 Qed.
|
adam@352
|
449
|
adam@352
|
450 Theorem associativity : forall A B C (m : computation A) (f : A -> computation B) (g : B -> computation C),
|
adam@352
|
451 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)).
|
adam@352
|
452 run.
|
adam@352
|
453 Qed.
|
adam@352
|
454
|
adam@355
|
455 (** Now we come to the piece most directly inspired by domain theory. We want to support general recursive function definitions, but domain theory tells us that not all definitions are reasonable; some fail to be %\emph{%#<i>#continuous#</i>#%}% and thus represent unrealizable computations. To formalize an analogous notion of continuity for our non-termination monad, we write down the approximation relation on computation results that we have had in mind all along. *)
|
adam@352
|
456
|
adam@352
|
457 Section lattice.
|
adam@352
|
458 Variable A : Type.
|
adam@352
|
459
|
adam@352
|
460 Definition leq (x y : option A) :=
|
adam@352
|
461 forall v, x = Some v -> y = Some v.
|
adam@352
|
462 End lattice.
|
adam@352
|
463
|
adam@355
|
464 (** 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
|
465
|
adam@352
|
466 Section Fix.
|
adam@355
|
467 (** First, we have the function domain and range types. *)
|
adam@355
|
468
|
adam@352
|
469 Variables A B : Type.
|
adam@355
|
470
|
adam@355
|
471 (** Next comes the function body, which is written as though it can be parameterized over itself, for recursive calls. *)
|
adam@355
|
472
|
adam@352
|
473 Variable f : (A -> computation B) -> (A -> computation B).
|
adam@352
|
474
|
adam@355
|
475 (** 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
|
476
|
adam@352
|
477 Hypothesis f_continuous : forall n v v1 x,
|
adam@352
|
478 runTo (f v1 x) n v
|
adam@352
|
479 -> forall (v2 : A -> computation B),
|
adam@352
|
480 (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n))
|
adam@352
|
481 -> runTo (f v2 x) n v.
|
adam@352
|
482
|
adam@355
|
483 (** 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
|
484
|
adam@352
|
485 Fixpoint Fix' (n : nat) (x : A) : computation B :=
|
adam@352
|
486 match n with
|
adam@352
|
487 | O => Bottom _
|
adam@352
|
488 | S n' => f (Fix' n') x
|
adam@352
|
489 end.
|
adam@352
|
490
|
adam@355
|
491 (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
|
adam@355
|
492
|
adam@352
|
493 Hint Extern 1 (_ >= _) => omega.
|
adam@352
|
494 Hint Unfold leq.
|
adam@352
|
495
|
adam@352
|
496 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
|
adam@352
|
497 -> forall n', n' >= n
|
adam@352
|
498 -> proj1_sig (Fix' n' x) steps = Some v.
|
adam@352
|
499 unfold runTo in *; induction n; crush;
|
adam@352
|
500 match goal with
|
adam@352
|
501 | [ H : _ >= _ |- _ ] => inversion H; crush; eauto
|
adam@352
|
502 end.
|
adam@352
|
503 Qed.
|
adam@352
|
504
|
adam@352
|
505 Hint Resolve Fix'_ok.
|
adam@352
|
506
|
adam@352
|
507 Hint Extern 1 (proj1_sig _ _ = _) => simpl;
|
adam@352
|
508 match goal with
|
adam@352
|
509 | [ |- proj1_sig ?E _ = _ ] => eapply (proj2_sig E)
|
adam@352
|
510 end.
|
adam@352
|
511
|
adam@352
|
512 Definition Fix : A -> computation B.
|
adam@352
|
513 intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run.
|
adam@352
|
514 Defined.
|
adam@352
|
515
|
adam@355
|
516 (** Finally, we can prove that [Fix] obeys the expected computation rule. *)
|
adam@352
|
517
|
adam@352
|
518 Theorem run_Fix : forall x v,
|
adam@352
|
519 run (f Fix x) v
|
adam@352
|
520 -> run (Fix x) v.
|
adam@352
|
521 run; match goal with
|
adam@352
|
522 | [ n : nat |- _ ] => exists (S n); eauto
|
adam@352
|
523 end.
|
adam@352
|
524 Qed.
|
adam@352
|
525 End Fix.
|
adam@352
|
526
|
adam@355
|
527 (* begin hide *)
|
adam@352
|
528 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
|
adam@352
|
529 -> x = y.
|
adam@352
|
530 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
|
adam@352
|
531 Qed.
|
adam@352
|
532
|
adam@352
|
533 Lemma leq_None : forall A (x y : A), leq (Some x) None
|
adam@352
|
534 -> False.
|
adam@352
|
535 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
|
adam@352
|
536 Qed.
|
adam@352
|
537
|
adam@355
|
538 Ltac mergeSort' := run;
|
adam@355
|
539 repeat (match goal with
|
adam@355
|
540 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
|
adam@355
|
541 end; run);
|
adam@355
|
542 repeat match goal with
|
adam@355
|
543 | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] =>
|
adam@355
|
544 match goal with
|
adam@355
|
545 | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] =>
|
adam@355
|
546 generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro
|
adam@355
|
547 end
|
adam@355
|
548 end; run; repeat match goal with
|
adam@355
|
549 | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst)
|
adam@355
|
550 end; auto.
|
adam@355
|
551 (* end hide *)
|
adam@355
|
552
|
adam@355
|
553 (** 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
|
554
|
adam@352
|
555 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A).
|
adam@352
|
556 refine (fun A le => Fix
|
adam@352
|
557 (fun (mergeSort : list A -> computation (list A))
|
adam@352
|
558 (ls : list A) =>
|
adam@352
|
559 if le_lt_dec 2 (length ls)
|
adam@352
|
560 then let lss := partition ls in
|
adam@352
|
561 ls1 <- mergeSort (fst lss);
|
adam@352
|
562 ls2 <- mergeSort (snd lss);
|
adam@352
|
563 Return (merge le ls1 ls2)
|
adam@355
|
564 else Return ls) _); abstract mergeSort'.
|
adam@352
|
565 Defined.
|
adam@352
|
566
|
adam@355
|
567 (** 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
|
568
|
adam@352
|
569 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
|
adam@352
|
570 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
|
adam@352
|
571 exists 4; reflexivity.
|
adam@352
|
572 Qed.
|
adam@352
|
573
|
adam@355
|
574 (** There is another benefit of our new [Fix] compared with one we used in the previous section: we can now write recursive functions that sometimes fail to terminate, without losing easy reasoning principles for the terminating cases. Consider this simple example, which appeals to another tactic whose definition we elide here. *)
|
adam@355
|
575
|
adam@355
|
576 (* begin hide *)
|
adam@355
|
577 Ltac looper := unfold leq in *; run;
|
adam@355
|
578 repeat match goal with
|
adam@355
|
579 | [ x : unit |- _ ] => destruct x
|
adam@355
|
580 | [ x : bool |- _ ] => destruct x
|
adam@355
|
581 end; auto.
|
adam@355
|
582 (* end hide *)
|
adam@355
|
583
|
adam@352
|
584 Definition looper : bool -> computation unit.
|
adam@352
|
585 refine (Fix (fun looper (b : bool) =>
|
adam@355
|
586 if b then Return tt else looper b) _); abstract looper.
|
adam@352
|
587 Defined.
|
adam@352
|
588
|
adam@352
|
589 Lemma test_looper : run (looper true) tt.
|
adam@352
|
590 exists 1; reflexivity.
|
adam@352
|
591 Qed.
|
adam@354
|
592
|
adam@355
|
593 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level.
|
adam@355
|
594
|
adam@355
|
595 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
|
596
|
adam@354
|
597
|
adam@354
|
598 (** * Co-Inductive Non-Termination Monads *)
|
adam@354
|
599
|
adam@354
|
600 CoInductive thunk (A : Type) : Type :=
|
adam@354
|
601 | Answer : A -> thunk A
|
adam@354
|
602 | Think : thunk A -> thunk A.
|
adam@354
|
603
|
adam@354
|
604 CoFixpoint TBind (A B : Type) (m1 : thunk A) (m2 : A -> thunk B) : thunk B :=
|
adam@354
|
605 match m1 with
|
adam@354
|
606 | Answer x => m2 x
|
adam@354
|
607 | Think m1' => Think (TBind m1' m2)
|
adam@354
|
608 end.
|
adam@354
|
609
|
adam@354
|
610 CoInductive thunk_eq A : thunk A -> thunk A -> Prop :=
|
adam@354
|
611 | EqAnswer : forall x, thunk_eq (Answer x) (Answer x)
|
adam@354
|
612 | EqThinkL : forall m1 m2, thunk_eq m1 m2 -> thunk_eq (Think m1) m2
|
adam@354
|
613 | EqThinkR : forall m1 m2, thunk_eq m1 m2 -> thunk_eq m1 (Think m2).
|
adam@354
|
614
|
adam@354
|
615 Section thunk_eq_coind.
|
adam@354
|
616 Variable A : Type.
|
adam@354
|
617 Variable P : thunk A -> thunk A -> Prop.
|
adam@354
|
618
|
adam@354
|
619 Hypothesis H : forall m1 m2, P m1 m2
|
adam@354
|
620 -> match m1, m2 with
|
adam@354
|
621 | Answer x1, Answer x2 => x1 = x2
|
adam@354
|
622 | Think m1', Think m2' => P m1' m2'
|
adam@354
|
623 | Think m1', _ => P m1' m2
|
adam@354
|
624 | _, Think m2' => P m1 m2'
|
adam@354
|
625 end.
|
adam@354
|
626
|
adam@354
|
627 Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
|
adam@354
|
628 cofix; intros;
|
adam@354
|
629 match goal with
|
adam@354
|
630 | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
|
adam@354
|
631 end; destruct m1; destruct m2; subst; repeat constructor; auto.
|
adam@354
|
632 Qed.
|
adam@354
|
633 End thunk_eq_coind.
|
adam@354
|
634
|
adam@354
|
635 Definition frob A (m : thunk A) : thunk A :=
|
adam@354
|
636 match m with
|
adam@354
|
637 | Answer x => Answer x
|
adam@354
|
638 | Think m' => Think m'
|
adam@354
|
639 end.
|
adam@354
|
640
|
adam@354
|
641 Theorem frob_eq : forall A (m : thunk A), frob m = m.
|
adam@354
|
642 destruct m; reflexivity.
|
adam@354
|
643 Qed.
|
adam@354
|
644
|
adam@354
|
645 Theorem thunk_eq_frob : forall A (m1 m2 : thunk A),
|
adam@354
|
646 thunk_eq (frob m1) (frob m2)
|
adam@354
|
647 -> thunk_eq m1 m2.
|
adam@354
|
648 intros; repeat rewrite frob_eq in *; auto.
|
adam@354
|
649 Qed.
|
adam@354
|
650
|
adam@354
|
651 Ltac findDestr := match goal with
|
adam@354
|
652 | [ |- context[match ?E with Answer _ => _ | Think _ => _ end] ] =>
|
adam@354
|
653 match E with
|
adam@354
|
654 | context[match _ with Answer _ => _ | Think _ => _ end] => fail 1
|
adam@354
|
655 | _ => destruct E
|
adam@354
|
656 end
|
adam@354
|
657 end.
|
adam@354
|
658
|
adam@354
|
659 Theorem thunk_eq_refl : forall A (m : thunk A), thunk_eq m m.
|
adam@354
|
660 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = m2)); crush; findDestr; reflexivity.
|
adam@354
|
661 Qed.
|
adam@354
|
662
|
adam@354
|
663 Hint Resolve thunk_eq_refl.
|
adam@354
|
664
|
adam@354
|
665 Theorem tleft_identity : forall A B (a : A) (f : A -> thunk B),
|
adam@354
|
666 thunk_eq (TBind (Answer a) f) (f a).
|
adam@354
|
667 intros; apply thunk_eq_frob; crush.
|
adam@354
|
668 Qed.
|
adam@354
|
669
|
adam@354
|
670 Theorem tright_identity : forall A (m : thunk A),
|
adam@354
|
671 thunk_eq (TBind m (@Answer _)) m.
|
adam@354
|
672 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = TBind m2 (@Answer _))); crush;
|
adam@354
|
673 findDestr; reflexivity.
|
adam@354
|
674 Qed.
|
adam@354
|
675
|
adam@354
|
676 Lemma TBind_Answer : forall (A B : Type) (v : A) (m2 : A -> thunk B),
|
adam@354
|
677 TBind (Answer v) m2 = m2 v.
|
adam@354
|
678 intros; rewrite <- (frob_eq (TBind (Answer v) m2));
|
adam@354
|
679 simpl; findDestr; reflexivity.
|
adam@354
|
680 Qed.
|
adam@354
|
681
|
adam@354
|
682 Hint Rewrite TBind_Answer : cpdt.
|
adam@354
|
683
|
adam@355
|
684 (** printing exists $\exists$ *)
|
adam@355
|
685
|
adam@354
|
686 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C),
|
adam@354
|
687 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)).
|
adam@354
|
688 intros; apply (thunk_eq_coind (fun m1 m2 => (exists m,
|
adam@354
|
689 m1 = TBind (TBind m f) g
|
adam@354
|
690 /\ m2 = TBind m (fun x => TBind (f x) g))
|
adam@354
|
691 \/ m1 = m2)); crush; eauto; repeat (findDestr; crush; eauto).
|
adam@354
|
692 Qed.
|
adam@354
|
693
|
adam@354
|
694 CoFixpoint fact (n acc : nat) : thunk nat :=
|
adam@354
|
695 match n with
|
adam@354
|
696 | O => Answer acc
|
adam@354
|
697 | S n' => Think (fact n' (S n' * acc))
|
adam@354
|
698 end.
|
adam@354
|
699
|
adam@354
|
700 Inductive eval A : thunk A -> A -> Prop :=
|
adam@354
|
701 | EvalAnswer : forall x, eval (Answer x) x
|
adam@354
|
702 | EvalThink : forall m x, eval m x -> eval (Think m) x.
|
adam@354
|
703
|
adam@354
|
704 Hint Rewrite frob_eq : cpdt.
|
adam@354
|
705
|
adam@354
|
706 Lemma eval_frob : forall A (c : thunk A) x,
|
adam@354
|
707 eval (frob c) x
|
adam@354
|
708 -> eval c x.
|
adam@354
|
709 crush.
|
adam@354
|
710 Qed.
|
adam@354
|
711
|
adam@354
|
712 Theorem eval_fact : eval (fact 5 1) 120.
|
adam@354
|
713 repeat (apply eval_frob; simpl; constructor).
|
adam@354
|
714 Qed.
|
adam@354
|
715
|
adam@354
|
716 (** [[
|
adam@354
|
717 CoFixpoint fib (n : nat) : thunk nat :=
|
adam@354
|
718 match n with
|
adam@354
|
719 | 0 => Answer 1
|
adam@354
|
720 | 1 => Answer 1
|
adam@354
|
721 | _ => TBind (fib (pred n)) (fun n1 =>
|
adam@354
|
722 TBind (fib (pred (pred n))) (fun n2 =>
|
adam@354
|
723 Answer (n1 + n2)))
|
adam@354
|
724 end.
|
adam@354
|
725 ]]
|
adam@354
|
726 *)
|
adam@354
|
727
|
adam@354
|
728
|
adam@354
|
729 CoInductive comp (A : Type) : Type :=
|
adam@354
|
730 | Ret : A -> comp A
|
adam@354
|
731 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.
|
adam@354
|
732
|
adam@354
|
733 Inductive exec A : comp A -> A -> Prop :=
|
adam@354
|
734 | ExecRet : forall x, exec (Ret x) x
|
adam@354
|
735 | ExecBnd : forall B (c : comp B) (f : B -> comp A) x1 x2, exec (A := B) c x1
|
adam@354
|
736 -> exec (f x1) x2
|
adam@354
|
737 -> exec (Bnd c f) x2.
|
adam@354
|
738
|
adam@354
|
739 Hint Constructors exec.
|
adam@354
|
740
|
adam@354
|
741 Definition comp_eq A (c1 c2 : comp A) := forall r, exec c1 r <-> exec c2 r.
|
adam@354
|
742
|
adam@354
|
743 Ltac inverter := repeat match goal with
|
adam@354
|
744 | [ H : exec _ _ |- _ ] => inversion H; []; crush
|
adam@354
|
745 end.
|
adam@354
|
746
|
adam@354
|
747 Theorem cleft_identity : forall A B (a : A) (f : A -> comp B),
|
adam@354
|
748 comp_eq (Bnd (Ret a) f) (f a).
|
adam@354
|
749 red; crush; inverter; eauto.
|
adam@354
|
750 Qed.
|
adam@354
|
751
|
adam@354
|
752 Theorem cright_identity : forall A (m : comp A),
|
adam@354
|
753 comp_eq (Bnd m (@Ret _)) m.
|
adam@354
|
754 red; crush; inverter; eauto.
|
adam@354
|
755 Qed.
|
adam@354
|
756
|
adam@354
|
757 Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
|
adam@354
|
758 exec c r
|
adam@354
|
759 -> forall m, c = Bnd (Bnd m f) g
|
adam@354
|
760 -> exec (Bnd m (fun x => Bnd (f x) g)) r.
|
adam@354
|
761 induction 1; crush.
|
adam@354
|
762 match goal with
|
adam@354
|
763 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
|
adam@354
|
764 end.
|
adam@354
|
765 move H3 after A.
|
adam@354
|
766 generalize dependent B0.
|
adam@354
|
767 do 2 intro.
|
adam@354
|
768 subst.
|
adam@354
|
769 crush.
|
adam@354
|
770 inversion H; clear H; crush.
|
adam@354
|
771 eauto.
|
adam@354
|
772 Qed.
|
adam@354
|
773
|
adam@354
|
774 Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
|
adam@354
|
775 exec c r
|
adam@354
|
776 -> forall m, c = Bnd m (fun x => Bnd (f x) g)
|
adam@354
|
777 -> exec (Bnd (Bnd m f) g) r.
|
adam@354
|
778 induction 1; crush.
|
adam@354
|
779 match goal with
|
adam@354
|
780 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
|
adam@354
|
781 end.
|
adam@354
|
782 move H3 after B.
|
adam@354
|
783 generalize dependent B0.
|
adam@354
|
784 do 2 intro.
|
adam@354
|
785 subst.
|
adam@354
|
786 crush.
|
adam@354
|
787 inversion H0; clear H0; crush.
|
adam@354
|
788 eauto.
|
adam@354
|
789 Qed.
|
adam@354
|
790
|
adam@354
|
791 Hint Resolve cassociativity1 cassociativity2.
|
adam@354
|
792
|
adam@354
|
793 Theorem cassociativity : forall A B C (m : comp A) (f : A -> comp B) (g : B -> comp C),
|
adam@354
|
794 comp_eq (Bnd (Bnd m f) g) (Bnd m (fun x => Bnd (f x) g)).
|
adam@354
|
795 red; crush; eauto.
|
adam@354
|
796 Qed.
|
adam@354
|
797
|
adam@354
|
798 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) :=
|
adam@354
|
799 if le_lt_dec 2 (length ls)
|
adam@354
|
800 then let lss := partition ls in
|
adam@354
|
801 Bnd (mergeSort'' le (fst lss)) (fun ls1 =>
|
adam@354
|
802 Bnd (mergeSort'' le (snd lss)) (fun ls2 =>
|
adam@354
|
803 Ret (merge le ls1 ls2)))
|
adam@354
|
804 else Ret ls.
|
adam@354
|
805
|
adam@354
|
806 Definition frob' A (c : comp A) :=
|
adam@354
|
807 match c with
|
adam@354
|
808 | Ret x => Ret x
|
adam@354
|
809 | Bnd _ c' f => Bnd c' f
|
adam@354
|
810 end.
|
adam@354
|
811
|
adam@354
|
812 Lemma frob'_eq : forall A (c : comp A), frob' c = c.
|
adam@354
|
813 destruct c; reflexivity.
|
adam@354
|
814 Qed.
|
adam@354
|
815
|
adam@354
|
816 Hint Rewrite frob'_eq : cpdt.
|
adam@354
|
817
|
adam@354
|
818 Lemma exec_frob : forall A (c : comp A) x,
|
adam@354
|
819 exec (frob' c) x
|
adam@354
|
820 -> exec c x.
|
adam@354
|
821 crush.
|
adam@354
|
822 Qed.
|
adam@354
|
823
|
adam@354
|
824 Lemma test_mergeSort'' : exec (mergeSort'' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
|
adam@354
|
825 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
|
adam@354
|
826 repeat (apply exec_frob; simpl; econstructor).
|
adam@354
|
827 Qed.
|
adam@354
|
828
|
adam@354
|
829 Definition curriedAdd (n : nat) := Ret (fun m : nat => Ret (n + m)).
|
adam@354
|
830
|
adam@354
|
831 (** [[
|
adam@354
|
832 Definition testCurriedAdd :=
|
adam@354
|
833 Bnd (curriedAdd 2) (fun f => f 3).
|
adam@354
|
834 ]]
|
adam@354
|
835
|
adam@354
|
836 <<
|
adam@354
|
837 Error: Universe inconsistency.
|
adam@354
|
838 >>
|
adam@354
|
839 *)
|
adam@354
|
840
|
adam@354
|
841
|
adam@354
|
842 (** * Comparing the Options *)
|
adam@354
|
843
|
adam@354
|
844 Definition curriedAdd' (n : nat) := Return (fun m : nat => Return (n + m)).
|
adam@354
|
845
|
adam@354
|
846 Definition testCurriedAdd :=
|
adam@354
|
847 Bind (curriedAdd' 2) (fun f => f 3).
|
adam@354
|
848
|
adam@354
|
849 Fixpoint map A B (f : A -> computation B) (ls : list A) : computation (list B) :=
|
adam@354
|
850 match ls with
|
adam@354
|
851 | nil => Return nil
|
adam@354
|
852 | x :: ls' => Bind (f x) (fun x' =>
|
adam@354
|
853 Bind (map f ls') (fun ls'' =>
|
adam@354
|
854 Return (x' :: ls'')))
|
adam@354
|
855 end.
|
adam@354
|
856
|
adam@355
|
857 (** remove printing exists *)
|
adam@354
|
858 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil)) (2 :: 3 :: 4 :: nil).
|
adam@354
|
859 exists 1; reflexivity.
|
adam@354
|
860 Qed.
|