Mercurial > cpdt > repo

annotate src/Large.v @ 237:91eed1e3e3a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More anti-patterns
author Adam Chlipala <adamc@hcoop.net>
date Mon, 07 Dec 2009 10:54:43 -0500
parents c8f49f07cead
children 0a2146dafa8e
rev   line source
adamc@235 1 (* Copyright (c) 2009, Adam Chlipala
adamc@235 2 *
adamc@235 3 * This work is licensed under a
adamc@235 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@235 5 * Unported License.
adamc@235 6 * The license text is available at:
adamc@235 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@235 8 *)
adamc@235 9
adamc@235 10 (* begin hide *)
adamc@236 11 Require Import Arith.
adamc@236 12
adamc@235 13 Require Import Tactics.
adamc@235 14
adamc@235 15 Set Implicit Arguments.
adamc@235 16 (* end hide *)
adamc@235 17
adamc@235 18
adamc@235 19 (** %\chapter{Proving in the Large}% *)
adamc@235 20
adamc@236 21 (** It is somewhat unfortunate that the term "theorem-proving" looks so much like the word "theory." Most researchers and practitioners in software assume that mechanized theorem-proving is profoundly impractical. Indeed, until recently, most advances in theorem-proving for higher-order logics have been largely theoretical. However, starting around the beginning of the 21st century, there was a surge in the use of proof assistants in serious verification efforts. That line of work is still quite new, but I believe it is not too soon to distill some lessons on how to work effectively with large formal proofs.
adamc@236 22
adamc@236 23 Thus, this chapter gives some tips for structuring and maintaining large Coq developments. *)
adamc@236 24
adamc@236 25
adamc@236 26 (** * Ltac Anti-Patterns *)
adamc@236 27
adamc@237 28 (** 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?
adamc@236 29
adamc@237 30 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.
adamc@236 31
adamc@236 32 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. *)
adamc@236 33
adamc@236 34 Inductive exp : Set :=
adamc@236 35 | Const : nat -> exp
adamc@236 36 | Plus : exp -> exp -> exp.
adamc@236 37
adamc@236 38 Fixpoint eval (e : exp) : nat :=
adamc@236 39 match e with
adamc@236 40 | Const n => n
adamc@236 41 | Plus e1 e2 => eval e1 + eval e2
adamc@236 42 end.
adamc@236 43
adamc@236 44 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 45 match e with
adamc@236 46 | Const n => Const (k * n)
adamc@236 47 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 48 end.
adamc@236 49
adamc@236 50 (** We can write a very manual proof that [double] really doubles an expression's value. *)
adamc@236 51
adamc@236 52 Theorem eval_times : forall k e,
adamc@236 53 eval (times k e) = k * eval e.
adamc@236 54 induction e.
adamc@236 55
adamc@236 56 trivial.
adamc@236 57
adamc@236 58 simpl.
adamc@236 59 rewrite IHe1.
adamc@236 60 rewrite IHe2.
adamc@236 61 rewrite mult_plus_distr_l.
adamc@236 62 trivial.
adamc@236 63 Qed.
adamc@236 64
adamc@236 65 (** We use spaces to separate the two inductive cases. The second case mentions automatically-generated hypothesis names explicitly. As a result, innocuous changes to the theorem statement can invalidate the proof. *)
adamc@236 66
adamc@236 67 Reset eval_times.
adamc@236 68
adamc@236 69 Theorem eval_double : forall k x,
adamc@236 70 eval (times k x) = k * eval x.
adamc@236 71 induction x.
adamc@236 72
adamc@236 73 trivial.
adamc@236 74
adamc@236 75 simpl.
adamc@236 76 (** [[
adamc@236 77 rewrite IHe1.
adamc@236 78
adamc@236 79 Error: The reference IHe1 was not found in the current environment.
adamc@236 80
adamc@236 81 ]]
adamc@236 82
adamc@236 83 The inductive hypotheses are named [IHx1] and [IHx2] now, not [IHe1] and [IHe2]. *)
adamc@236 84
adamc@236 85 Abort.
adamc@236 86
adamc@236 87 (** We might decide to use a more explicit invocation of [induction] to give explicit binders for all of the names that we will reference later in the proof. *)
adamc@236 88
adamc@236 89 Theorem eval_times : forall k e,
adamc@236 90 eval (times k e) = k * eval e.
adamc@236 91 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 92
adamc@236 93 trivial.
adamc@236 94
adamc@236 95 simpl.
adamc@236 96 rewrite IHe1.
adamc@236 97 rewrite IHe2.
adamc@236 98 rewrite mult_plus_distr_l.
adamc@236 99 trivial.
adamc@236 100 Qed.
adamc@236 101
adamc@236 102 (** 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.
adamc@236 103
adamc@237 104 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. *)
adamc@236 105
adamc@236 106 Reset times.
adamc@236 107
adamc@236 108 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 109 match e with
adamc@236 110 | Const n => Const (1 + k * n)
adamc@236 111 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 112 end.
adamc@236 113
adamc@236 114 Theorem eval_times : forall k e,
adamc@236 115 eval (times k e) = k * eval e.
adamc@236 116 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 117
adamc@236 118 trivial.
adamc@236 119
adamc@236 120 simpl.
adamc@236 121 (** [[
adamc@236 122 rewrite IHe1.
adamc@236 123
adamc@236 124 Error: The reference IHe1 was not found in the current environment.
adamc@236 125
adamc@236 126 ]] *)
adamc@236 127
adamc@236 128 Abort.
adamc@236 129
adamc@237 130 (** 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.
adamc@237 131
adamc@237 132 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. *)
adamc@236 133
adamc@236 134 Reset times.
adamc@236 135
adamc@236 136 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 137 match e with
adamc@236 138 | Const n => Const (k * n)
adamc@236 139 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 140 end.
adamc@236 141
adamc@237 142 (** 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.
adamc@236 143
adamc@236 144 We can rewrite the current proof with a single tactic. *)
adamc@236 145
adamc@236 146 Theorem eval_times : forall k e,
adamc@236 147 eval (times k e) = k * eval e.
adamc@236 148 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 149 trivial
adamc@236 150 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adamc@236 151 Qed.
adamc@236 152
adamc@236 153 (** This is an improvement in robustness of the script. We no longer need to worry about tactics from one case being applied to a different case. Still, the proof script is not especially readable. Probably most readers would not find it helpful in explaining why the theorem is true.
adamc@236 154
adamc@236 155 The situation gets worse in considering extensions to the theorem we want to prove. Let us add multiplication nodes to our [exp] type and see how the proof fares. *)
adamc@236 156
adamc@236 157 Reset exp.
adamc@236 158
adamc@236 159 Inductive exp : Set :=
adamc@236 160 | Const : nat -> exp
adamc@236 161 | Plus : exp -> exp -> exp
adamc@236 162 | Mult : exp -> exp -> exp.
adamc@236 163
adamc@236 164 Fixpoint eval (e : exp) : nat :=
adamc@236 165 match e with
adamc@236 166 | Const n => n
adamc@236 167 | Plus e1 e2 => eval e1 + eval e2
adamc@236 168 | Mult e1 e2 => eval e1 * eval e2
adamc@236 169 end.
adamc@236 170
adamc@236 171 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 172 match e with
adamc@236 173 | Const n => Const (k * n)
adamc@236 174 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 175 | Mult e1 e2 => Mult (times k e1) e2
adamc@236 176 end.
adamc@236 177
adamc@236 178 Theorem eval_times : forall k e,
adamc@236 179 eval (times k e) = k * eval e.
adamc@236 180 (** [[
adamc@236 181 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 182 trivial
adamc@236 183 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adamc@236 184
adamc@236 185 Error: Expects a disjunctive pattern with 3 branches.
adamc@236 186
adamc@236 187 ]] *)
adamc@236 188
adamc@236 189 Abort.
adamc@236 190
adamc@236 191 (** Unsurprisingly, the old proof fails, because it explicitly says that there are two inductive cases. To update the script, we must, at a minimum, remember the order in which the inductive cases are generated, so that we can insert the new case in the appropriate place. Even then, it will be painful to add the case, because we cannot walk through proof steps interactively when they occur inside an explicit set of cases. *)
adamc@236 192
adamc@236 193 Theorem eval_times : forall k e,
adamc@236 194 eval (times k e) = k * eval e.
adamc@236 195 induction e as [ | ? IHe1 ? IHe2 | ? IHe1 ? IHe2 ]; [
adamc@236 196 trivial
adamc@236 197 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial
adamc@236 198 | simpl; rewrite IHe1; rewrite mult_assoc; trivial ].
adamc@236 199 Qed.
adamc@236 200
adamc@236 201 (** Now we are in a position to see how much nicer is the style of proof that we have followed in most of this book. *)
adamc@236 202
adamc@236 203 Reset eval_times.
adamc@236 204
adamc@236 205 Theorem eval_times : forall k e,
adamc@236 206 eval (times k e) = k * eval e.
adamc@236 207 Hint Rewrite mult_plus_distr_l mult_assoc : cpdt.
adamc@236 208
adamc@236 209 induction e; crush.
adamc@236 210 Qed.
adamc@236 211
adamc@237 212 (** 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.
adamc@237 213
adamc@237 214 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.
adamc@237 215
adamc@237 216 An example should help illustrate what I mean. Consider this function, which rewrites an expression using associativity of addition and multiplication. *)
adamc@237 217
adamc@237 218 Fixpoint reassoc (e : exp) : exp :=
adamc@237 219 match e with
adamc@237 220 | Const _ => e
adamc@237 221 | Plus e1 e2 =>
adamc@237 222 let e1' := reassoc e1 in
adamc@237 223 let e2' := reassoc e2 in
adamc@237 224 match e2' with
adamc@237 225 | Plus e21 e22 => Plus (Plus e1' e21) e22
adamc@237 226 | _ => Plus e1' e2'
adamc@237 227 end
adamc@237 228 | Mult e1 e2 =>
adamc@237 229 let e1' := reassoc e1 in
adamc@237 230 let e2' := reassoc e2 in
adamc@237 231 match e2' with
adamc@237 232 | Mult e21 e22 => Mult (Mult e1' e21) e22
adamc@237 233 | _ => Mult e1' e2'
adamc@237 234 end
adamc@237 235 end.
adamc@237 236
adamc@237 237 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adamc@237 238 induction e; crush;
adamc@237 239 match goal with
adamc@237 240 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
adamc@237 241 destruct E; crush
adamc@237 242 end.
adamc@237 243
adamc@237 244 (** One subgoal remains:
adamc@237 245 [[
adamc@237 246 IHe2 : eval e3 * eval e4 = eval e2
adamc@237 247 ============================
adamc@237 248 eval e1 * eval e3 * eval e4 = eval e1 * eval e2
adamc@237 249
adamc@237 250 ]]
adamc@237 251
adamc@237 252 [crush] does not know how to finish this goal. We could finish the proof manually. *)
adamc@237 253
adamc@237 254 rewrite <- IHe2; crush.
adamc@237 255
adamc@237 256 (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
adamc@237 257
adamc@237 258 Abort.
adamc@237 259
adamc@237 260 Lemma rewr : forall a b c d, b * c = d -> a * b * c = a * d.
adamc@237 261 crush.
adamc@237 262 Qed.
adamc@237 263
adamc@237 264 Hint Resolve rewr.
adamc@237 265
adamc@237 266 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adamc@237 267 induction e; crush;
adamc@237 268 match goal with
adamc@237 269 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
adamc@237 270 destruct E; crush
adamc@237 271 end.
adamc@237 272 Qed.
adamc@237 273
adamc@237 274 (** 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.
adamc@237 275
adamc@237 276 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. *)
adamc@237 277
adamc@235 278
adamc@235 279 (** * Modules *)
adamc@235 280
adamc@235 281 Module Type GROUP.
adamc@235 282 Parameter G : Set.
adamc@235 283 Parameter f : G -> G -> G.
adamc@235 284 Parameter e : G.
adamc@235 285 Parameter i : G -> G.
adamc@235 286
adamc@235 287 Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
adamc@235 288 Axiom ident : forall a, f e a = a.
adamc@235 289 Axiom inverse : forall a, f (i a) a = e.
adamc@235 290 End GROUP.
adamc@235 291
adamc@235 292 Module Type GROUP_THEOREMS.
adamc@235 293 Declare Module M : GROUP.
adamc@235 294
adamc@235 295 Axiom ident' : forall a, M.f a M.e = a.
adamc@235 296
adamc@235 297 Axiom inverse' : forall a, M.f a (M.i a) = M.e.
adamc@235 298
adamc@235 299 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 300 End GROUP_THEOREMS.
adamc@235 301
adamc@235 302 Module Group (M : GROUP) : GROUP_THEOREMS.
adamc@235 303 Module M := M.
adamc@235 304
adamc@235 305 Import M.
adamc@235 306
adamc@235 307 Theorem inverse' : forall a, f a (i a) = e.
adamc@235 308 intro.
adamc@235 309 rewrite <- (ident (f a (i a))).
adamc@235 310 rewrite <- (inverse (f a (i a))) at 1.
adamc@235 311 rewrite assoc.
adamc@235 312 rewrite assoc.
adamc@235 313 rewrite <- (assoc (i a) a (i a)).
adamc@235 314 rewrite inverse.
adamc@235 315 rewrite ident.
adamc@235 316 apply inverse.
adamc@235 317 Qed.
adamc@235 318
adamc@235 319 Theorem ident' : forall a, f a e = a.
adamc@235 320 intro.
adamc@235 321 rewrite <- (inverse a).
adamc@235 322 rewrite <- assoc.
adamc@235 323 rewrite inverse'.
adamc@235 324 apply ident.
adamc@235 325 Qed.
adamc@235 326
adamc@235 327 Theorem unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 328 intros.
adamc@235 329 rewrite <- (H e).
adamc@235 330 symmetry.
adamc@235 331 apply ident'.
adamc@235 332 Qed.
adamc@235 333 End Group.