Certified Programming with Dependent Types: src/GeneralRec.v comparison

comparison src/GeneralRec.v @ 453:e3fa35c750ac

Proofreading pass through Chapter 7

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 23 Aug 2012 16:54:04 -0400
parents	cbfd23b4364d
children	4320c1a967c2

comparison

equal deleted inserted replaced

-:980962258b49
+:e3fa35c750ac
 end.
 (** Now, let us try to write the final sorting function, using a natural number "[<=]" test [leb] from the standard library.
 [[
 Fixpoint mergeSort (ls : list A) : list A :=
-if leb (length ls) 2
+if leb (length ls) 1
 then ls
 else let lss := partition ls in
 	merge (mergeSort (fst lss)) (mergeSort (snd lss)).
 ]]
 partition.
 Defined.
 Hint Resolve partition_wf1 partition_wf2.
-(** 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. *)
+(** 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_.) *)
 Definition mergeSort : list A -> list A.
 (* begin thide *)
 refine (Fix lengthOrder_wf (fun _ => list A)
 (fun (ls : list A)
 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
 exists 4; reflexivity.
 Qed.
-(** 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. *)
+(** There is another benefit of our new [Fix] compared with the one we used in the previous section: we can now write recursive functions that sometimes fail to terminate, without losing easy reasoning principles for the terminating cases.  Consider this simple example, which appeals to another tactic whose definition we elide here. *)
 (* begin hide *)
 Ltac looper := unfold leq in *; run;
 repeat match goal with
 | [ x : unit |- _ ] => destruct x
 (* begin thide *)
 Definition fib := pred.
 (* end thide *)
 (* end hide *)
-(** %\vspace{-.15in}%[[
+(** %\vspace{-.3in}%[[
 CoFixpoint fib (n : nat) : thunk nat :=
 match n with
 | 0 => Answer 1
 | 1 => Answer 1
 | _ => n1 <- fib (pred n);
 The problem has to do with rules for inductive definitions that we still study in more detail in Chapter 12.  Briefly, recall that the type of the constructor [Bnd] quantifies over a type [B].  To make [testCurriedAdd] work, we would need to instantiate [B] as [nat -> comp nat].  However, Coq enforces a %\emph{predicativity restriction}% that (roughly) no quantifier in an inductive or co-inductive type's definition may ever be instantiated with a term that contains the type being defined.  Chapter 12 presents the exact mechanism by which this restriction is enforced, but for now our conclusion is that [comp] is fatally flawed as a way of encoding interesting higher-order functional programs that use general recursion. *)
 (** * Comparing the Alternatives *)
-(** We have seen four different approaches to encoding general recursive definitions in Coq.  Among them there is no clear champion that dominates the others in every important way.  Instead, we close the chapter by comparing the techniques along a number of dimensions.  Every technique allows recursive definitions with terminaton arguments that go beyond Coq's built-in termination checking, so we must turn to subtler points to highlight differences.
+(** We have seen four different approaches to encoding general recursive definitions in Coq.  Among them there is no clear champion that dominates the others in every important way.  Instead, we close the chapter by comparing the techniques along a number of dimensions.  Every technique allows recursive definitions with termination arguments that go beyond Coq's built-in termination checking, so we must turn to subtler points to highlight differences.
 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.
 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.

Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 453:e3fa35c750ac