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 *)