## Mercurial > cpdt > repo

### comparison src/GeneralRec.v @ 480:f38a3af9dd17

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Batch of changes based on proofreader feedback

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Fri, 30 Nov 2012 11:57:55 -0500 |

parents | 1fd4109f7b31 |

children | 88688402dc82 |

comparison

equal
deleted
inserted
replaced

479:40a9a36844d6 | 480:f38a3af9dd17 |
---|---|

54 match ls1 with | 54 match ls1 with |

55 | nil => ls2 | 55 | nil => ls2 |

56 | h :: ls' => insert h (merge ls' ls2) | 56 | h :: ls' => insert h (merge ls' ls2) |

57 end. | 57 end. |

58 | 58 |

59 (** 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. *) | 59 (** The last helper function for classic merge sort is the one that follows, to split a list arbitrarily into two pieces of approximately equal length. *) |

60 | 60 |

61 Fixpoint partition (ls : list A) : list A * list A := | 61 Fixpoint split (ls : list A) : list A * list A := |

62 match ls with | 62 match ls with |

63 | nil => (nil, nil) | 63 | nil => (nil, nil) |

64 | h :: nil => (h :: nil, nil) | 64 | h :: nil => (h :: nil, nil) |

65 | h1 :: h2 :: ls' => | 65 | h1 :: h2 :: ls' => |

66 let (ls1, ls2) := partition ls' in | 66 let (ls1, ls2) := split ls' in |

67 (h1 :: ls1, h2 :: ls2) | 67 (h1 :: ls1, h2 :: ls2) |

68 end. | 68 end. |

69 | 69 |

70 (** Now, let us try to write the final sorting function, using a natural number "[<=]" test [leb] from the standard library. | 70 (** Now, let us try to write the final sorting function, using a natural number "[<=]" test [leb] from the standard library. |

71 [[ | 71 [[ |

72 Fixpoint mergeSort (ls : list A) : list A := | 72 Fixpoint mergeSort (ls : list A) : list A := |

73 if leb (length ls) 1 | 73 if leb (length ls) 1 |

74 then ls | 74 then ls |

75 else let lss := partition ls in | 75 else let lss := split ls in |

76 merge (mergeSort (fst lss)) (mergeSort (snd lss)). | 76 merge (mergeSort (fst lss)) (mergeSort (snd lss)). |

77 ]] | 77 ]] |

78 | 78 |

79 << | 79 << |

80 Recursive call to mergeSort has principal argument equal to | 80 Recursive call to mergeSort has principal argument equal to |

81 "fst (partition ls)" instead of a subterm of "ls". | 81 "fst (split ls)" instead of a subterm of "ls". |

82 >> | 82 >> |

83 | 83 |

84 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. | 84 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. |

85 | 85 |

86 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. *) | 86 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. *) |

169 red; intro; eapply lengthOrder_wf'; eauto. | 169 red; intro; eapply lengthOrder_wf'; eauto. |

170 Defined. | 170 Defined. |

171 | 171 |

172 (** Notice that we end these proofs with %\index{Vernacular commands!Defined}%[Defined], not [Qed]. Recall that [Defined] marks the theorems as %\emph{transparent}%, so that the details of their proofs may be used during program execution. Why could such details possibly matter for computation? It turns out that [Fix] satisfies the primitive recursion restriction by declaring itself as _recursive in the structure of [Acc] proofs_. This is possible because [Acc] proofs follow a predictable inductive structure. We must do work, as in the last theorem's proof, to establish that all elements of a type belong to [Acc], but the automatic unwinding of those proofs during recursion is straightforward. If we ended the proof with [Qed], the proof details would be hidden from computation, in which case the unwinding process would get stuck. | 172 (** Notice that we end these proofs with %\index{Vernacular commands!Defined}%[Defined], not [Qed]. Recall that [Defined] marks the theorems as %\emph{transparent}%, so that the details of their proofs may be used during program execution. Why could such details possibly matter for computation? It turns out that [Fix] satisfies the primitive recursion restriction by declaring itself as _recursive in the structure of [Acc] proofs_. This is possible because [Acc] proofs follow a predictable inductive structure. We must do work, as in the last theorem's proof, to establish that all elements of a type belong to [Acc], but the automatic unwinding of those proofs during recursion is straightforward. If we ended the proof with [Qed], the proof details would be hidden from computation, in which case the unwinding process would get stuck. |

173 | 173 |

174 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. We use the syntax [@foo] to reference identifier [foo] with its implicit argument behavior turned off. *) | 174 To justify our two recursive [mergeSort] calls, we will also need to prove that [split] respects the [lengthOrder] relation. These proofs, too, must be kept transparent, to avoid stuckness of [Fix] evaluation. We use the syntax [@foo] to reference identifier [foo] with its implicit argument behavior turned off. (The proof details below use Ltac features not introduced yet, and they are safe to skip for now.) *) |

175 | 175 |

176 Lemma partition_wf : forall len ls, 2 <= length ls <= len | 176 Lemma split_wf : forall len ls, 2 <= length ls <= len |

177 -> let (ls1, ls2) := partition ls in | 177 -> let (ls1, ls2) := split ls in |

178 lengthOrder ls1 ls /\ lengthOrder ls2 ls. | 178 lengthOrder ls1 ls /\ lengthOrder ls2 ls. |

179 unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush); | 179 unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush); |

180 destruct (le_lt_dec 2 (length ls)); | 180 destruct (le_lt_dec 2 (length ls)); |

181 repeat (match goal with | 181 repeat (match goal with |

182 | [ _ : length ?E < 2 |- _ ] => destruct E | 182 | [ _ : length ?E < 2 |- _ ] => destruct E |

183 | [ _ : S (length ?E) < 2 |- _ ] => destruct E | 183 | [ _ : S (length ?E) < 2 |- _ ] => destruct E |

184 | [ IH : _ |- context[partition ?L] ] => | 184 | [ IH : _ |- context[split ?L] ] => |

185 specialize (IH L); destruct (partition L); destruct IH | 185 specialize (IH L); destruct (split L); destruct IH |

186 end; crush). | 186 end; crush). |

187 Defined. | 187 Defined. |

188 | 188 |

189 Ltac partition := intros ls ?; intros; generalize (@partition_wf (length ls) ls); | 189 Ltac split_wf := intros ls ?; intros; generalize (@split_wf (length ls) ls); |

190 destruct (partition ls); destruct 1; crush. | 190 destruct (split ls); destruct 1; crush. |

191 | 191 |

192 Lemma partition_wf1 : forall ls, 2 <= length ls | 192 Lemma split_wf1 : forall ls, 2 <= length ls |

193 -> lengthOrder (fst (partition ls)) ls. | 193 -> lengthOrder (fst (split ls)) ls. |

194 partition. | 194 split_wf. |

195 Defined. | 195 Defined. |

196 | 196 |

197 Lemma partition_wf2 : forall ls, 2 <= length ls | 197 Lemma split_wf2 : forall ls, 2 <= length ls |

198 -> lengthOrder (snd (partition ls)) ls. | 198 -> lengthOrder (snd (split ls)) ls. |

199 partition. | 199 split_wf. |

200 Defined. | 200 Defined. |

201 | 201 |

202 Hint Resolve partition_wf1 partition_wf2. | 202 Hint Resolve split_wf1 split_wf2. |

203 | 203 |

204 (** To write the function definition itself, we use the %\index{tactics!refine}%[refine] tactic as a convenient way to write a program that needs to manipulate proofs, without writing out those proofs manually. We also use a replacement [le_lt_dec] for [leb] that has a more interesting dependent type. (Note that we would not be able to complete the definition without this change, since [refine] will generate subgoals for the [if] branches based only on the _type_ of the test expression, not its _value_.) *) | 204 (** To write the function definition itself, we use the %\index{tactics!refine}%[refine] tactic as a convenient way to write a program that needs to manipulate proofs, without writing out those proofs manually. We also use a replacement [le_lt_dec] for [leb] that has a more interesting dependent type. (Note that we would not be able to complete the definition without this change, since [refine] will generate subgoals for the [if] branches based only on the _type_ of the test expression, not its _value_.) *) |

205 | 205 |

206 Definition mergeSort : list A -> list A. | 206 Definition mergeSort : list A -> list A. |

207 (* begin thide *) | 207 (* begin thide *) |

208 refine (Fix lengthOrder_wf (fun _ => list A) | 208 refine (Fix lengthOrder_wf (fun _ => list A) |

209 (fun (ls : list A) | 209 (fun (ls : list A) |

210 (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) => | 210 (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) => |

211 if le_lt_dec 2 (length ls) | 211 if le_lt_dec 2 (length ls) |

212 then let lss := partition ls in | 212 then let lss := split ls in |

213 merge (mergeSort (fst lss) _) (mergeSort (snd lss) _) | 213 merge (mergeSort (fst lss) _) (mergeSort (snd lss) _) |

214 else ls)); subst lss; eauto. | 214 else ls)); subst lss; eauto. |

215 Defined. | 215 Defined. |

216 (* end thide *) | 216 (* end thide *) |

217 End mergeSort. | 217 End mergeSort. |

224 (** %\smallskip{}%Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *) | 224 (** %\smallskip{}%Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *) |

225 | 225 |

226 (* begin thide *) | 226 (* begin thide *) |

227 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls, | 227 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls, |

228 mergeSort le ls = if le_lt_dec 2 (length ls) | 228 mergeSort le ls = if le_lt_dec 2 (length ls) |

229 then let lss := partition ls in | 229 then let lss := split ls in |

230 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss)) | 230 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss)) |

231 else ls. | 231 else ls. |

232 intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros. | 232 intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros. |

233 | 233 |

234 (** The library theorem [Fix_eq] imposes one more strange subgoal upon us. We must prove that the function body is unable to distinguish between "self" arguments that map equal inputs to equal outputs. One might think this should be true of any Gallina code, but in fact this general%\index{extensionality}% _function extensionality_ property is neither provable nor disprovable within Coq. The type of [Fix_eq] makes clear what we must show manually: *) | 234 (** The library theorem [Fix_eq] imposes one more strange subgoal upon us. We must prove that the function body is unable to distinguish between "self" arguments that map equal inputs to equal outputs. One might think this should be true of any Gallina code, but in fact this general%\index{extensionality}% _function extensionality_ property is neither provable nor disprovable within Coq. The type of [Fix_eq] makes clear what we must show manually: *) |

259 | 259 |

260 (** << | 260 (** << |

261 let rec mergeSort le x = | 261 let rec mergeSort le x = |

262 match le_lt_dec (S (S O)) (length x) with | 262 match le_lt_dec (S (S O)) (length x) with |

263 | Left -> | 263 | Left -> |

264 let lss = partition x in | 264 let lss = split x in |

265 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss)) | 265 merge le (mergeSort le (fst lss)) (mergeSort le (snd lss)) |

266 | Right -> x | 266 | Right -> x |

267 >> | 267 >> |

268 | 268 |

269 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. | 269 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. |

380 | [ H : _ = exist _ _ _ |- _ ] => rewrite H | 380 | [ H : _ = exist _ _ _ |- _ ] => rewrite H |

381 end. | 381 end. |

382 (* end hide *) | 382 (* end hide *) |

383 (** remove printing exists *) | 383 (** remove printing exists *) |

384 | 384 |

385 (** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop. For any approximation level, it fails to terminate (returns [None]). Note the use of [abstract] to create a new opaque lemma for the proof found by the [run] tactic. In contrast to the previous section, opaque proofs are fine here, since the proof components of computations do not influence evaluation behavior. *) | 385 (** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop. For any approximation level, it fails to terminate (returns [None]). Note the use of [abstract] to create a new opaque lemma for the proof found by the #<tt>#%\coqdocvar{%run%}%#</tt># tactic. In contrast to the previous section, opaque proofs are fine here, since the proof components of computations do not influence evaluation behavior. It is generally preferable to make proofs opaque when possible, as this enforces a kind of modularity in the code to follow, preventing it from depending on any details of the proof. *) |

386 | 386 |

387 Section Bottom. | 387 Section Bottom. |

388 Variable A : Type. | 388 Variable A : Type. |

389 | 389 |

390 Definition Bottom : computation A. | 390 Definition Bottom : computation A. |

568 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A). | 568 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A). |

569 refine (fun A le => Fix | 569 refine (fun A le => Fix |

570 (fun (mergeSort : list A -> computation (list A)) | 570 (fun (mergeSort : list A -> computation (list A)) |

571 (ls : list A) => | 571 (ls : list A) => |

572 if le_lt_dec 2 (length ls) | 572 if le_lt_dec 2 (length ls) |

573 then let lss := partition ls in | 573 then let lss := split ls in |

574 ls1 <- mergeSort (fst lss); | 574 ls1 <- mergeSort (fst lss); |

575 ls2 <- mergeSort (snd lss); | 575 ls2 <- mergeSort (snd lss); |

576 Return (merge le ls1 ls2) | 576 Return (merge le ls1 ls2) |

577 else Return ls) _); abstract mergeSort'. | 577 else Return ls) _); abstract mergeSort'. |

578 Defined. | 578 Defined. |

603 exists 1; reflexivity. | 603 exists 1; reflexivity. |

604 Qed. | 604 Qed. |

605 | 605 |

606 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level. | 606 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level. |

607 | 607 |

608 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. *) | 608 There are other theorems that are important to prove about combinators like [Return], [Bind], and [Fix]. In general, for a computation [c], we sometimes have a hypothesis proving [run c v] for some [v], and we want to perform inversion to deduce what [v] must be. Each combinator should ideally have a theorem of that kind, for [c] built directly from that combinator. We have omitted such theorems here, but they are not hard to prove. In general, the domain theory-inspired approach avoids the type-theoretic "gotchas" that tend to show up in approaches that try to mix normal Coq computation with explicit syntax types. The next section of this chapter demonstrates two alternate approaches of that sort. In the final section of the chapter, we review the pros and cons of the different choices, coming to the conclusion that none of them is obviously better than any one of the others for all situations. *) |

609 | 609 |

610 | 610 |

611 (** * Co-Inductive Non-Termination Monads *) | 611 (** * Co-Inductive Non-Termination Monads *) |

612 | 612 |

613 (** There are two key downsides to both of the previous approaches: both require unusual syntax based on explicit calls to fixpoint combinators, and both generate immediate proof obligations about the bodies of recursive definitions. In Chapter 5, we have already seen how co-inductive types support recursive definitions that exhibit certain well-behaved varieties of non-termination. It turns out that we can leverage that co-induction support for encoding of general recursive definitions, by adding layers of co-inductive syntax. In effect, we mix elements of shallow and deep embeddings. | 613 (** There are two key downsides to both of the previous approaches: both require unusual syntax based on explicit calls to fixpoint combinators, and both generate immediate proof obligations about the bodies of recursive definitions. In Chapter 5, we have already seen how co-inductive types support recursive definitions that exhibit certain well-behaved varieties of non-termination. It turns out that we can leverage that co-induction support for encoding of general recursive definitions, by adding layers of co-inductive syntax. In effect, we mix elements of shallow and deep embeddings. |

859 | 859 |

860 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)). | 860 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)). |

861 | 861 |

862 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) := | 862 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) := |

863 if le_lt_dec 2 (length ls) | 863 if le_lt_dec 2 (length ls) |

864 then let lss := partition ls in | 864 then let lss := split ls in |

865 ls1 <- mergeSort'' le (fst lss); | 865 ls1 <- mergeSort'' le (fst lss); |

866 ls2 <- mergeSort'' le (snd lss); | 866 ls2 <- mergeSort'' le (snd lss); |

867 Ret (merge le ls1 ls2) | 867 Ret (merge le ls1 ls2) |

868 else Ret ls. | 868 else Ret ls. |

869 | 869 |

910 | 910 |

911 One useful property is automatic integration with normal Coq programming. That is, we would like the type of a function to be the same, whether or not that function is defined using an interesting recursion pattern. Only the first of the four techniques, well-founded recursion, meets this criterion. It is also the only one of the four to meet the related criterion that evaluation of function calls can take place entirely inside Coq's built-in computation machinery. The monad inspired by domain theory occupies some middle ground in this dimension, since generally standard computation is enough to evaluate a term once a high enough approximation level is provided. | 911 One useful property is automatic integration with normal Coq programming. That is, we would like the type of a function to be the same, whether or not that function is defined using an interesting recursion pattern. Only the first of the four techniques, well-founded recursion, meets this criterion. It is also the only one of the four to meet the related criterion that evaluation of function calls can take place entirely inside Coq's built-in computation machinery. The monad inspired by domain theory occupies some middle ground in this dimension, since generally standard computation is enough to evaluate a term once a high enough approximation level is provided. |

912 | 912 |

913 Another useful property is that a function and its termination argument may be developed separately. We may even want to define functions that fail to terminate on some or all inputs. The well-founded recursion technique does not have this property, but the other three do. | 913 Another useful property is that a function and its termination argument may be developed separately. We may even want to define functions that fail to terminate on some or all inputs. The well-founded recursion technique does not have this property, but the other three do. |

914 | 914 |

915 One minor plus is the ability to write recursive definitions in natural syntax, rather than with calls to higher-order combinators. This downside of the first two techniques is actually rather easy to get around using Coq's notation mechanism, though we leave the details as an exercise for the reader. | 915 One minor plus is the ability to write recursive definitions in natural syntax, rather than with calls to higher-order combinators. This downside of the first two techniques is actually rather easy to get around using Coq's notation mechanism, though we leave the details as an exercise for the reader. (For this and other details of notations, see Chapter 12 of the Coq 8.4 manual.) |

916 | 916 |

917 The first two techniques impose proof obligations that are more basic than termination arguments, where well-founded recursion requires a proof of extensionality and domain-theoretic recursion requires a proof of continuity. A function may not be defined, and thus may not be computed with, until these obligations are proved. The co-inductive techniques avoid this problem, as recursive definitions may be made without any proof obligations. | 917 The first two techniques impose proof obligations that are more basic than termination arguments, where well-founded recursion requires a proof of extensionality and domain-theoretic recursion requires a proof of continuity. A function may not be defined, and thus may not be computed with, until these obligations are proved. The co-inductive techniques avoid this problem, as recursive definitions may be made without any proof obligations. |

918 | 918 |

919 We can also consider support for common idioms in functional programming. For instance, the [thunk] monad effectively only supports recursion that is tail recursion, while the others allow arbitrary recursion schemes. | 919 We can also consider support for common idioms in functional programming. For instance, the [thunk] monad effectively only supports recursion that is tail recursion, while the others allow arbitrary recursion schemes. |

920 | 920 |