Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 475:1fd4109f7b31

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 Mon, 22 Oct 2012 14:23:52 -0400
parents d9e1fb184672
children f38a3af9dd17
comparison
equal deleted inserted replaced
474:d9e1fb184672 475:1fd4109f7b31
32 (** The essence of terminating recursion is that there are no infinite chains of nested recursive calls. This intuition is commonly mapped to the mathematical idea of a%\index{well-founded relation}% _well-founded relation_, and the associated standard technique in Coq is%\index{well-founded recursion}% _well-founded recursion_. The syntactic-subterm relation that Coq applies by default is well-founded, but many cases demand alternate well-founded relations. To demonstrate, let us see where we get stuck on attempting a standard merge sort implementation. *) 32 (** The essence of terminating recursion is that there are no infinite chains of nested recursive calls. This intuition is commonly mapped to the mathematical idea of a%\index{well-founded relation}% _well-founded relation_, and the associated standard technique in Coq is%\index{well-founded recursion}% _well-founded recursion_. The syntactic-subterm relation that Coq applies by default is well-founded, but many cases demand alternate well-founded relations. To demonstrate, let us see where we get stuck on attempting a standard merge sort implementation. *)
33 33
34 Section mergeSort. 34 Section mergeSort.
35 Variable A : Type. 35 Variable A : Type.
36 Variable le : A -> A -> bool. 36 Variable le : A -> A -> bool.
37
37 (** We have a set equipped with some "less-than-or-equal-to" test. *) 38 (** We have a set equipped with some "less-than-or-equal-to" test. *)
38 39
39 (** A standard function inserts an element into a sorted list, preserving sortedness. *) 40 (** A standard function inserts an element into a sorted list, preserving sortedness. *)
40 41
41 Fixpoint insert (x : A) (ls : list A) : list A := 42 Fixpoint insert (x : A) (ls : list A) : list A :=
473 End lattice. 474 End lattice.
474 475
475 (** We now have the tools we need to define a new [Fix] combinator that, unlike the one we saw in the prior section, does not require a termination proof, and in fact admits recursive definition of functions that fail to terminate on some or all inputs. *) 476 (** 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. *)
476 477
477 Section Fix. 478 Section Fix.
479
478 (** First, we have the function domain and range types. *) 480 (** First, we have the function domain and range types. *)
479 481
480 Variables A B : Type. 482 Variables A B : Type.
481 483
482 (** Next comes the function body, which is written as though it can be parameterized over itself, for recursive calls. *) 484 (** Next comes the function body, which is written as though it can be parameterized over itself, for recursive calls. *)