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

comparison src/Large.v @ 237:91eed1e3e3a4

More anti-patterns

author	Adam Chlipala <adamc@hcoop.net>
date	Mon, 07 Dec 2009 10:54:43 -0500
parents	c8f49f07cead
children	0a2146dafa8e

comparison

equal deleted inserted replaced

-:c8f49f07cead
+:91eed1e3e3a4
 Thus, this chapter gives some tips for structuring and maintaining large Coq developments. *)
 (** * Ltac Anti-Patterns *)
-(** In this book, I have been following an unusual style, where proofs are not considered finished until they are "fully automated," in a certain sense.  Each such theorem is proved by a single tactic.  Since Ltac is a Turing-complete programming language, it is not hard to squeeze arbitrary heuristics into single tactics, using operators like the semicolon to combine steps.  In contrast, most Ltac proofs "in the wild" consist of many steps, performed by individual tactics followed by periods.  Is it really worth drawing a distinction between proof steps terminated by semicolons and steps terminated by periods?
+(** In this book, I have been following an unusual style, where proofs are not considered finished until they are "fully automated," in a certain sense.  SEach such theorem is proved by a single tactic.  Since Ltac is a Turing-complete programming language, it is not hard to squeeze arbitrary heuristics into single tactics, using operators like the semicolon to combine steps.  In contrast, most Ltac proofs "in the wild" consist of many steps, performed by individual tactics followed by periods.  Is it really worth drawing a distinction between proof steps terminated by semicolons and steps terminated by periods?
-I argue that this is, in fact, a very important distinction, with serious consequences for a majority of important verification domains.  The more uninteresting drudge work found in a proof domain, the more important it is to work to prove theorems with single tactics.  From an automation standpoint, single-tactic proofs can be extremely effective, and automation becomes more and more critical as proofs are populated by more uninteresting detail.  In this section, I will give some examples of the consequences of more common proof styles.
+I argue that this is, in fact, a very important distinction, with serious consequences for a majority of important verification domains.  The more uninteresting drudge work a proof domain involves, the more important it is to work to prove theorems with single tactics.  From an automation standpoint, single-tactic proofs can be extremely effective, and automation becomes more and more critical as proofs are populated by more uninteresting detail.  In this section, I will give some examples of the consequences of more common proof styles.
 As a running example, consider a basic language of arithmetic expressions, an interpreter for it, and a transformation that scales up every constant in an expression. *)
 Inductive exp : Set :=
 | Const : nat -> exp
 trivial.
 Qed.
 (** We pass [induction] an %\textit{%#<i>#intro pattern#</i>#%}%, using a [|] character to separate out instructions for the different inductive cases.  Within a case, we write [?] to ask Coq to generate a name automatically, and we write an explicit name to assign that name to the corresponding new variable.  It is apparent that, to use intro patterns to avoid proof brittleness, one needs to keep track of the seemingly unimportant facts of the orders in which variables are introduced.  Thus, the script keeps working if we replace [e] by [x], but it has become more cluttered.  Arguably, neither proof is particularly easy to follow.
-That category of complaint has to do with understanding proofs as static artifacts.  As with programming in general, with serious projects, it tends to be much more important to be able to support evolution of proofs as theorems change.  Unstructured proofs like the above examples can be very hard to update in concert with theorem statements.  For instance, consider how the last proof script plays out when we modify [times] to introduce a bug. *)
+That category of complaint has to do with understanding proofs as static artifacts.  As with programming in general, with serious projects, it tends to be much more important to be able to support evolution of proofs as specifications change.  Unstructured proofs like the above examples can be very hard to update in concert with theorem statements.  For instance, consider how the last proof script plays out when we modify [times] to introduce a bug. *)
 Reset times.
 Fixpoint times (k : nat) (e : exp) : exp :=
 match e with
 ]] *)
 Abort.
-(** Can you spot what went wrong, without stepping through the script step-by-step?  The problem is that [trivial] never fails.  Originally, [trivial] had been succeeding in proving an equality that follows by reflexivity.  Our change to [times] leads to a case where that equality is no longer true.  [trivial] happily leaves the false equality in place, and we continue on to the span of tactics intended for the second inductive case.  Unfortunately, those tactics end up being applied to the %\textit{%#<i>#first#</i>#%}% case instead.  This example is on a very small scale; similar consequences can be much more confusing in large developments. *)
+(** Can you spot what went wrong, without stepping through the script step-by-step?  The problem is that [trivial] never fails.  Originally, [trivial] had been succeeding in proving an equality that follows by reflexivity.  Our change to [times] leads to a case where that equality is no longer true.  [trivial] happily leaves the false equality in place, and we continue on to the span of tactics intended for the second inductive case.  Unfortunately, those tactics end up being applied to the %\textit{%#<i>#first#</i>#%}% case instead.
+The problem with [trivial] could be "solved" by writing [solve [trivial]] instead, so that an error is signaled early on if something unexpected happens.  However, the root problem is that the syntax of a tactic invocation does not imply how many subgoals it produces.  Much more confusing instances of this problem are possible.  For example, if a lemma [L] is modified to take an extra hypothesis, then uses of [apply L] will general more subgoals than before.  Old unstructured proof scripts will become hopelessly jumbled, with tactics applied to inappropriate subgoals.  Because of the lack of structure, there is usually relatively little to be gleaned from knowledge of the precise point in a proof script where an error is raised. *)
 Reset times.
 Fixpoint times (k : nat) (e : exp) : exp :=
 match e with
 | Const n => Const (k * n)
 | Plus e1 e2 => Plus (times k e1) (times k e2)
 end.
-(** Many real developments try to make essentially unstructured proofs look structured by applying careful indentation conventions, idempotent case-marker tactics included soley to serve as documentation, and so on.  All of these strategies suffer from the same kind of failure of abstraction that was just demonstrated.  I like to say that, if you find yourself caring about indentation in a proof script, it is a sign that the script is structured poorly.
+(** Many real developments try to make essentially unstructured proofs look structured by applying careful indentation conventions, idempotent case-marker tactics included soley to serve as documentation, and so on.  All of these strategies suffer from the same kind of failure of abstraction that was just demonstrated.  I like to say that if you find yourself caring about indentation in a proof script, it is a sign that the script is structured poorly.
 We can rewrite the current proof with a single tactic. *)
 Theorem eval_times : forall k e,
 eval (times k e) = k * eval e.
 eval (times k e) = k * eval e.
 Hint Rewrite mult_plus_distr_l mult_assoc : cpdt.
 induction e; crush.
 Qed.
+(** 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.
+An example should help illustrate what I mean.  Consider this function, which rewrites an expression using associativity of addition and multiplication. *)
+Fixpoint reassoc (e : exp) : exp :=
+match e with
+| Const _ => e
+| Plus e1 e2 =>
+let e1' := reassoc e1 in
+let e2' := reassoc e2 in
+match e2' with
+| Plus e21 e22 => Plus (Plus e1' e21) e22
+| _ => Plus e1' e2'
+end
+| Mult e1 e2 =>
+let e1' := reassoc e1 in
+let e2' := reassoc e2 in
+match e2' with
+| Mult e21 e22 => Mult (Mult e1' e21) e22
+| _ => Mult e1' e2'
+end
+end.
+Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
+induction e; crush;
+match goal with
+| [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
+destruct E; crush
+end.
+(** One subgoal remains:
+[[
+IHe2 : eval e3 * eval e4 = eval e2
+============================
+eval e1 * eval e3 * eval e4 = eval e1 * eval e2
+]]
+[crush] does not know how to finish this goal.  We could finish the proof manually. *)
+rewrite <- IHe2; crush.
+(** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
+Abort.
+Lemma rewr : forall a b c d, b * c = d -> a * b * c = a * d.
+crush.
+Qed.
+Hint Resolve rewr.
+Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
+induction e; crush;
+match goal with
+| [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
+destruct E; crush
+end.
+Qed.
+(** 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. *)
 (** * Modules *)
 Module Type GROUP.

Mercurial > cpdt > repo

comparison src/Large.v @ 237:91eed1e3e3a4