Mercurial > cpdt > repo

annotate src/GeneralRec.v @ 355:62fdf0993e05

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prose for domain-theoretic approach
author Adam Chlipala <adam@chlipala.net>
date Fri, 28 Oct 2011 15:38:41 -0400
parents dc99dffdf20a
children 50e1d338728c
rev   line source
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.