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 |