Certified Programming with Dependent Types: src/Large.v comparison

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

-:b809d3a8a5b1
+:e0c5b91e2968
 rewrite IHe2.
 rewrite mult_plus_distr_l.
 trivial.
 Qed.
+(* begin thide *)
 (** 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. *)
 Reset eval_times.
-Theorem eval_double : forall k x,
+Theorem eval_times : forall k x,
 eval (times k x) = k * eval x.
 induction x.
 trivial.
 Theorem eval_times : forall k e,
 eval (times k e) = k * eval e.
 induction e; crush.
 Qed.
+(* end thide *)
 (** 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.
 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.
 | _ => Mult e1' e2'
 end
 end.
 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
+(* begin thide *)
 induction e; crush;
 match goal with
 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
 destruct E; crush
 end.
 match goal with
 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
 destruct E; crush
 end.
 Qed.
+(* end thide *)
 (** 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.
 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. *)
 (* begin hide *)
 Require Import MoreDep.
 (* end hide *)
 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
+(* begin thide *)
 induction e; crush.
 dep_destruct (cfold e1); crush.
 dep_destruct (cfold e2); crush.
 | [ |- context[match pairOut ?E with Some _ => _
 | None => _ end] ] =>
 dep_destruct E
 end; crush).
 Qed.
+(* end thide *)
 (** 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?
 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. *)
 Qed.
 Hint Rewrite confounder : cpdt.
 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
+(* begin thide *)
 induction e; crush;
 match goal with
 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
 destruct E; crush
 end.
 ]]
 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. *)
 Abort.
+(* end thide *)
 (** printing * $\times$ *)
 (** 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.
 Finished transaction in 2. secs (1.264079u,0.s)
 ]]
 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. *)
+(* begin thide *)
 Restart.
 info eauto 6.
 (** %\vspace{-.15in}%[[
 == intro x; intro y; intro H; intro H0; intro H4;
 simple eapply trans_eq.
 ]]
 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. *)
 Qed.
+(* end thide *)
 End slow.
 (** 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.
 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]. *)
 ]]
 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: *)
 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0.
+(* begin thide *)
 exact IntTheorems.unique_ident.
 Qed.
+(* end thide *)
 (** 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. *)
 (** * Build Processes *)

Mercurial > cpdt > repo

comparison src/Large.v @ 368:e0c5b91e2968