Mercurial > cpdt > repo
comparison src/Large.v @ 368:e0c5b91e2968
Templatize Large
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 09 Nov 2011 15:26:50 -0500 |
parents | b809d3a8a5b1 |
children | 4550dedad73a |
comparison
equal
deleted
inserted
replaced
367:b809d3a8a5b1 | 368:e0c5b91e2968 |
---|---|
60 rewrite IHe2. | 60 rewrite IHe2. |
61 rewrite mult_plus_distr_l. | 61 rewrite mult_plus_distr_l. |
62 trivial. | 62 trivial. |
63 Qed. | 63 Qed. |
64 | 64 |
65 (* begin thide *) | |
65 (** We use spaces to separate the two inductive cases, but note that these spaces have no real semantic content; Coq does not enforce that our spacing matches the real case structure of a proof. The second case mentions automatically generated hypothesis names explicitly. As a result, innocuous changes to the theorem statement can invalidate the proof. *) | 66 (** We use spaces to separate the two inductive cases, but note that these spaces have no real semantic content; Coq does not enforce that our spacing matches the real case structure of a proof. The second case mentions automatically generated hypothesis names explicitly. As a result, innocuous changes to the theorem statement can invalidate the proof. *) |
66 | 67 |
67 Reset eval_times. | 68 Reset eval_times. |
68 | 69 |
69 Theorem eval_double : forall k x, | 70 Theorem eval_times : forall k x, |
70 eval (times k x) = k * eval x. | 71 eval (times k x) = k * eval x. |
71 induction x. | 72 induction x. |
72 | 73 |
73 trivial. | 74 trivial. |
74 | 75 |
211 | 212 |
212 Theorem eval_times : forall k e, | 213 Theorem eval_times : forall k e, |
213 eval (times k e) = k * eval e. | 214 eval (times k e) = k * eval e. |
214 induction e; crush. | 215 induction e; crush. |
215 Qed. | 216 Qed. |
217 (* end thide *) | |
216 | 218 |
217 (** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else. I claim that step-by-step formal proofs are a poor way of conveying information. Thus, we had might as well cut out the steps and automate as much as possible. | 219 (** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else. I claim that step-by-step formal proofs are a poor way of conveying information. Thus, we had might as well cut out the steps and automate as much as possible. |
218 | 220 |
219 What about the illustrative value of proofs? Most informal proofs are read to convey the big ideas of proofs. How can reading [induction e; crush] convey any big ideas? My position is that any ideas that standard automation can find are not very big after all, and the %\textit{%#<i>#real#</i>#%}% big ideas should be expressed through lemmas that are added as hints. | 221 What about the illustrative value of proofs? Most informal proofs are read to convey the big ideas of proofs. How can reading [induction e; crush] convey any big ideas? My position is that any ideas that standard automation can find are not very big after all, and the %\textit{%#<i>#real#</i>#%}% big ideas should be expressed through lemmas that are added as hints. |
220 | 222 |
238 | _ => Mult e1' e2' | 240 | _ => Mult e1' e2' |
239 end | 241 end |
240 end. | 242 end. |
241 | 243 |
242 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e. | 244 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e. |
245 (* begin thide *) | |
243 induction e; crush; | 246 induction e; crush; |
244 match goal with | 247 match goal with |
245 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] => | 248 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] => |
246 destruct E; crush | 249 destruct E; crush |
247 end. | 250 end. |
272 match goal with | 275 match goal with |
273 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] => | 276 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] => |
274 destruct E; crush | 277 destruct E; crush |
275 end. | 278 end. |
276 Qed. | 279 Qed. |
280 (* end thide *) | |
277 | 281 |
278 (** In the limit, a complicated inductive proof might rely on one hint for each inductive case. The lemma for each hint could restate the associated case. Compared to manual proof scripts, we arrive at more readable results. Scripts no longer need to depend on the order in which cases are generated. The lemmas are easier to digest separately than are fragments of tactic code, since lemma statements include complete proof contexts. Such contexts can only be extracted from monolithic manual proofs by stepping through scripts interactively. | 282 (** In the limit, a complicated inductive proof might rely on one hint for each inductive case. The lemma for each hint could restate the associated case. Compared to manual proof scripts, we arrive at more readable results. Scripts no longer need to depend on the order in which cases are generated. The lemmas are easier to digest separately than are fragments of tactic code, since lemma statements include complete proof contexts. Such contexts can only be extracted from monolithic manual proofs by stepping through scripts interactively. |
279 | 283 |
280 The more common situation is that a large induction has several easy cases that automation makes short work of. In the remaining cases, automation performs some standard simplification. Among these cases, some may require quite involved proofs; such a case may deserve a hint lemma of its own, where the lemma statement may copy the simplified version of the case. Alternatively, the proof script for the main theorem may be extended with some automation code targeted at the specific case. Even such targeted scripting is more desirable than manual proving, because it may be read and understood without knowledge of a proof's hierarchical structure, case ordering, or name binding structure. *) | 284 The more common situation is that a large induction has several easy cases that automation makes short work of. In the remaining cases, automation performs some standard simplification. Among these cases, some may require quite involved proofs; such a case may deserve a hint lemma of its own, where the lemma statement may copy the simplified version of the case. Alternatively, the proof script for the main theorem may be extended with some automation code targeted at the specific case. Even such targeted scripting is more desirable than manual proving, because it may be read and understood without knowledge of a proof's hierarchical structure, case ordering, or name binding structure. *) |
281 | 285 |
291 (* begin hide *) | 295 (* begin hide *) |
292 Require Import MoreDep. | 296 Require Import MoreDep. |
293 (* end hide *) | 297 (* end hide *) |
294 | 298 |
295 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e). | 299 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e). |
300 (* begin thide *) | |
296 induction e; crush. | 301 induction e; crush. |
297 | 302 |
298 dep_destruct (cfold e1); crush. | 303 dep_destruct (cfold e1); crush. |
299 dep_destruct (cfold e2); crush. | 304 dep_destruct (cfold e2); crush. |
300 | 305 |
401 | [ |- context[match pairOut ?E with Some _ => _ | 406 | [ |- context[match pairOut ?E with Some _ => _ |
402 | None => _ end] ] => | 407 | None => _ end] ] => |
403 dep_destruct E | 408 dep_destruct E |
404 end; crush). | 409 end; crush). |
405 Qed. | 410 Qed. |
411 (* end thide *) | |
406 | 412 |
407 (** Even after we put together nice automated proofs, we must deal with specification changes that can invalidate them. It is not generally possible to step through single-tactic proofs interactively. There is a command %\index{Vernacular commands!Debug On}%[Debug On] that lets us step through points in tactic execution, but the debugger tends to make counterintuitive choices of which points we would like to stop at, and per-point output is quite verbose, so most Coq users do not find this debugging mode very helpful. How are we to understand what has broken in a script that used to work? | 413 (** Even after we put together nice automated proofs, we must deal with specification changes that can invalidate them. It is not generally possible to step through single-tactic proofs interactively. There is a command %\index{Vernacular commands!Debug On}%[Debug On] that lets us step through points in tactic execution, but the debugger tends to make counterintuitive choices of which points we would like to stop at, and per-point output is quite verbose, so most Coq users do not find this debugging mode very helpful. How are we to understand what has broken in a script that used to work? |
408 | 414 |
409 An example helps demonstrate a useful approach. Consider what would have happened in our proof of [reassoc_correct] if we had first added an unfortunate rewriting hint. *) | 415 An example helps demonstrate a useful approach. Consider what would have happened in our proof of [reassoc_correct] if we had first added an unfortunate rewriting hint. *) |
410 | 416 |
416 Qed. | 422 Qed. |
417 | 423 |
418 Hint Rewrite confounder : cpdt. | 424 Hint Rewrite confounder : cpdt. |
419 | 425 |
420 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e. | 426 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e. |
427 (* begin thide *) | |
421 induction e; crush; | 428 induction e; crush; |
422 match goal with | 429 match goal with |
423 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] => | 430 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] => |
424 destruct E; crush | 431 destruct E; crush |
425 end. | 432 end. |
514 ]] | 521 ]] |
515 | 522 |
516 The way a rewrite is displayed is somewhat baroque, but we can see that theorem [confounder] is the final culprit. At this point, we could remove that hint, prove an alternate version of the key lemma [rewr], or come up with some other remedy. Fixing this kind of problem tends to be relatively easy once the problem is revealed. *) | 523 The way a rewrite is displayed is somewhat baroque, but we can see that theorem [confounder] is the final culprit. At this point, we could remove that hint, prove an alternate version of the key lemma [rewr], or come up with some other remedy. Fixing this kind of problem tends to be relatively easy once the problem is revealed. *) |
517 | 524 |
518 Abort. | 525 Abort. |
526 (* end thide *) | |
519 | 527 |
520 (** printing * $\times$ *) | 528 (** printing * $\times$ *) |
521 | 529 |
522 (** Sometimes a change to a development has undesirable performance consequences, even if it does not prevent any old proof scripts from completing. If the performance consequences are severe enough, the proof scripts can be considered broken for practical purposes. | 530 (** Sometimes a change to a development has undesirable performance consequences, even if it does not prevent any old proof scripts from completing. If the performance consequences are severe enough, the proof scripts can be considered broken for practical purposes. |
523 | 531 |
556 Finished transaction in 2. secs (1.264079u,0.s) | 564 Finished transaction in 2. secs (1.264079u,0.s) |
557 ]] | 565 ]] |
558 | 566 |
559 Why has the search time gone up so much? The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *) | 567 Why has the search time gone up so much? The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *) |
560 | 568 |
569 (* begin thide *) | |
561 Restart. | 570 Restart. |
562 info eauto 6. | 571 info eauto 6. |
563 (** %\vspace{-.15in}%[[ | 572 (** %\vspace{-.15in}%[[ |
564 == intro x; intro y; intro H; intro H0; intro H4; | 573 == intro x; intro y; intro H; intro H0; intro H4; |
565 simple eapply trans_eq. | 574 simple eapply trans_eq. |
615 ]] | 624 ]] |
616 | 625 |
617 The first choice [eauto] makes is to apply [H3], since [H3] has the fewest hypotheses of all of the hypotheses and hints that match. However, it turns out that the single hypothesis generated is unprovable. That does not stop [eauto] from trying to prove it with an exponentially sized tree of applications of transitivity, reflexivity, and symmetry of equality. It is the children of the initial [apply H3] that account for all of the noticeable time in proof execution. In a more realistic development, we might use this output of [debug] to realize that adding transitivity as a hint was a bad idea. *) | 626 The first choice [eauto] makes is to apply [H3], since [H3] has the fewest hypotheses of all of the hypotheses and hints that match. However, it turns out that the single hypothesis generated is unprovable. That does not stop [eauto] from trying to prove it with an exponentially sized tree of applications of transitivity, reflexivity, and symmetry of equality. It is the children of the initial [apply H3] that account for all of the noticeable time in proof execution. In a more realistic development, we might use this output of [debug] to realize that adding transitivity as a hint was a bad idea. *) |
618 | 627 |
619 Qed. | 628 Qed. |
629 (* end thide *) | |
620 End slow. | 630 End slow. |
621 | 631 |
622 (** It is also easy to end up with a proof script that uses too much memory. As tactics run, they avoid generating proof terms, since serious proof search will consider many possible avenues, and we do not want to build proof terms for subproofs that end up unused. Instead, tactic execution maintains %\index{thunks}\textit{%#<i>#thunks#</i>#%}% (suspended computations, represented with closures), such that a tactic's proof-producing thunk is only executed when we run [Qed]. These thunks can use up large amounts of space, such that a proof script exhausts available memory, even when we know that we could have used much less memory by forcing some thunks earlier. | 632 (** It is also easy to end up with a proof script that uses too much memory. As tactics run, they avoid generating proof terms, since serious proof search will consider many possible avenues, and we do not want to build proof terms for subproofs that end up unused. Instead, tactic execution maintains %\index{thunks}\textit{%#<i>#thunks#</i>#%}% (suspended computations, represented with closures), such that a tactic's proof-producing thunk is only executed when we run [Qed]. These thunks can use up large amounts of space, such that a proof script exhausts available memory, even when we know that we could have used much less memory by forcing some thunks earlier. |
623 | 633 |
624 The %\index{tactics!abstract}%[abstract] tactical helps us force thunks by proving some subgoals as their own lemmas. For instance, a proof [induction x; crush] can in many cases be made to use significantly less peak memory by changing it to [induction x; abstract crush]. The main limitation of [abstract] is that it can only be applied to subgoals that are proved completely, with no undetermined unification variables remaining. Still, many large automated proofs can realize vast memory savings via [abstract]. *) | 634 The %\index{tactics!abstract}%[abstract] tactical helps us force thunks by proving some subgoals as their own lemmas. For instance, a proof [induction x; crush] can in many cases be made to use significantly less peak memory by changing it to [induction x; abstract crush]. The main limitation of [abstract] is that it can only be applied to subgoals that are proved completely, with no undetermined unification variables remaining. Still, many large automated proofs can realize vast memory savings via [abstract]. *) |
723 ]] | 733 ]] |
724 | 734 |
725 Projections like [Int.G] are known to be definitionally equal to the concrete values we have assigned to them, so the above theorem yields as a trivial corollary the following more natural restatement: *) | 735 Projections like [Int.G] are known to be definitionally equal to the concrete values we have assigned to them, so the above theorem yields as a trivial corollary the following more natural restatement: *) |
726 | 736 |
727 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. | 737 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. |
738 (* begin thide *) | |
728 exact IntTheorems.unique_ident. | 739 exact IntTheorems.unique_ident. |
729 Qed. | 740 Qed. |
741 (* end thide *) | |
730 | 742 |
731 (** As in ML, the module system provides an effective way to structure large developments. Unlike in ML, Coq modules add no expressiveness; we can implement any module as an inhabitant of a dependent record type. It is the second-class nature of modules that makes them easier to use than dependent records in many case. Because modules may only be used in quite restricted ways, it is easier to support convenient module coding through special commands and editing modes, as the above example demonstrates. An isomorphic implementation with records would have suffered from lack of such conveniences as module subtyping and importation of the fields of a module. On the other hand, all module values must be determined statically, so modules may not be computed, e.g., within the defintions of normal functions, based on particular function parameters. *) | 743 (** As in ML, the module system provides an effective way to structure large developments. Unlike in ML, Coq modules add no expressiveness; we can implement any module as an inhabitant of a dependent record type. It is the second-class nature of modules that makes them easier to use than dependent records in many case. Because modules may only be used in quite restricted ways, it is easier to support convenient module coding through special commands and editing modes, as the above example demonstrates. An isomorphic implementation with records would have suffered from lack of such conveniences as module subtyping and importation of the fields of a module. On the other hand, all module values must be determined statically, so modules may not be computed, e.g., within the defintions of normal functions, based on particular function parameters. *) |
732 | 744 |
733 | 745 |
734 (** * Build Processes *) | 746 (** * Build Processes *) |