Mercurial > cpdt > repo
comparison src/Large.v @ 350:ad315efc3b6b
Stub out new chapter
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 26 Oct 2011 11:19:52 -0400 |
| parents | d5787b70cf48 |
| children | b809d3a8a5b1 |
comparison
equal
deleted
inserted
replaced
| 349:de7db21a016c | 350:ad315efc3b6b |
|---|---|
| 282 | 282 |
| 283 (** Fully-automated proofs are desirable because they open up possibilities for automatic adaptation to changes of specification. A well-engineered script within a narrow domain can survive many changes to the formulation of the problem it solves. Still, as we are working with higher-order logic, most theorems fall within no obvious decidable theories. It is inevitable that most long-lived automated proofs will need updating. | 283 (** Fully-automated proofs are desirable because they open up possibilities for automatic adaptation to changes of specification. A well-engineered script within a narrow domain can survive many changes to the formulation of the problem it solves. Still, as we are working with higher-order logic, most theorems fall within no obvious decidable theories. It is inevitable that most long-lived automated proofs will need updating. |
| 284 | 284 |
| 285 Before we are ready to update our proofs, we need to write them in the first place. While fully-automated scripts are most robust to changes of specification, it is hard to write every new proof directly in that form. Instead, it is useful to begin a theorem with exploratory proving and then gradually refine it into a suitable automated form. | 285 Before we are ready to update our proofs, we need to write them in the first place. While fully-automated scripts are most robust to changes of specification, it is hard to write every new proof directly in that form. Instead, it is useful to begin a theorem with exploratory proving and then gradually refine it into a suitable automated form. |
| 286 | 286 |
| 287 Consider this theorem from Chapter 7, which we begin by proving in a mostly manual way, invoking [crush] after each steop to discharge any low-hanging fruit. Our manual effort involves choosing which expressions to case-analyze on. *) | 287 Consider this theorem from Chapter 8, which we begin by proving in a mostly manual way, invoking [crush] after each steop to discharge any low-hanging fruit. Our manual effort involves choosing which expressions to case-analyze on. *) |
| 288 | 288 |
| 289 (* begin hide *) | 289 (* begin hide *) |
| 290 Require Import MoreDep. | 290 Require Import MoreDep. |
| 291 (* end hide *) | 291 (* end hide *) |
| 292 | 292 |