Mercurial > cpdt > repo
comparison src/GeneralRec.v @ 514:3b21f4395178
Fix a word that was only included in LaTeX version
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Thu, 26 Sep 2013 15:26:12 -0400 |
| parents | 88688402dc82 |
| children | 8f9f1e5b2fe3 |
comparison
equal
deleted
inserted
replaced
| 513:a4b3386ae140 | 514:3b21f4395178 |
|---|---|
| 167 | 167 |
| 168 Theorem lengthOrder_wf : well_founded lengthOrder. | 168 Theorem lengthOrder_wf : well_founded lengthOrder. |
| 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{%#<i>#transparent#</i>#%}%, 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 [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.) *) | 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 split_wf : forall len ls, 2 <= length ls <= len | 176 Lemma split_wf : forall len ls, 2 <= length ls <= len |
| 177 -> let (ls1, ls2) := split ls in | 177 -> let (ls1, ls2) := split ls in |