Mercurial > cpdt > repo

annotate src/Large.v @ 376:3b36b1e05b4e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New release
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 17:00:34 -0400
parents d1276004eec9
children d5112c099fbf
rev   line source
adam@367 1 (* Copyright (c) 2009-2011, 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
adam@314 13 Require Import CpdtTactics.
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
adam@367 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
adam@367 28 (** In this book, I have been following an unusual style, where proofs are not considered finished until they are %\index{fully automated proofs}``%#"#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?
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
adam@368 65 (* begin thide *)
adam@367 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. *)
adamc@236 67
adamc@236 68 Reset eval_times.
adamc@236 69
adam@368 70 Theorem eval_times : forall k x,
adamc@236 71 eval (times k x) = k * eval x.
adamc@236 72 induction x.
adamc@236 73
adamc@236 74 trivial.
adamc@236 75
adamc@236 76 simpl.
adam@367 77 (** %\vspace{-.15in}%[[
adamc@236 78 rewrite IHe1.
adam@367 79 ]]
adamc@236 80
adam@367 81 <<
adamc@236 82 Error: The reference IHe1 was not found in the current environment.
adam@367 83 >>
adamc@236 84
adamc@236 85 The inductive hypotheses are named [IHx1] and [IHx2] now, not [IHe1] and [IHe2]. *)
adamc@236 86
adamc@236 87 Abort.
adamc@236 88
adamc@236 89 (** 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 90
adamc@236 91 Theorem eval_times : forall k e,
adamc@236 92 eval (times k e) = k * eval e.
adamc@236 93 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 94
adamc@236 95 trivial.
adamc@236 96
adamc@236 97 simpl.
adamc@236 98 rewrite IHe1.
adamc@236 99 rewrite IHe2.
adamc@236 100 rewrite mult_plus_distr_l.
adamc@236 101 trivial.
adamc@236 102 Qed.
adamc@236 103
adam@367 104 (** We pass %\index{tactics!induction}%[induction] an %\index{intro pattern}\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 105
adamc@237 106 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 107
adamc@236 108 Reset times.
adamc@236 109
adamc@236 110 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 111 match e with
adamc@236 112 | Const n => Const (1 + k * n)
adamc@236 113 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 114 end.
adamc@236 115
adamc@236 116 Theorem eval_times : forall k e,
adamc@236 117 eval (times k e) = k * eval e.
adamc@236 118 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 119
adamc@236 120 trivial.
adamc@236 121
adamc@236 122 simpl.
adam@367 123 (** %\vspace{-.15in}%[[
adamc@236 124 rewrite IHe1.
adam@367 125 ]]
adamc@236 126
adam@367 127 <<
adamc@236 128 Error: The reference IHe1 was not found in the current environment.
adam@367 129 >>
adam@302 130 *)
adamc@236 131
adamc@236 132 Abort.
adamc@236 133
adam@367 134 (** 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. The invocation [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 135
adam@367 136 The problem with [trivial] could be %``%#"#solved#"#%''% by writing, e.g., [trivial; fail] 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 137
adamc@236 138 Reset times.
adamc@236 139
adamc@236 140 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 141 match e with
adamc@236 142 | Const n => Const (k * n)
adamc@236 143 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 144 end.
adamc@236 145
adamc@237 146 (** 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 147
adamc@236 148 We can rewrite the current proof with a single tactic. *)
adamc@236 149
adamc@236 150 Theorem eval_times : forall k e,
adamc@236 151 eval (times k e) = k * eval e.
adamc@236 152 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 153 trivial
adamc@236 154 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adamc@236 155 Qed.
adamc@236 156
adamc@236 157 (** 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 158
adamc@236 159 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 160
adamc@236 161 Reset exp.
adamc@236 162
adamc@236 163 Inductive exp : Set :=
adamc@236 164 | Const : nat -> exp
adamc@236 165 | Plus : exp -> exp -> exp
adamc@236 166 | Mult : exp -> exp -> exp.
adamc@236 167
adamc@236 168 Fixpoint eval (e : exp) : nat :=
adamc@236 169 match e with
adamc@236 170 | Const n => n
adamc@236 171 | Plus e1 e2 => eval e1 + eval e2
adamc@236 172 | Mult e1 e2 => eval e1 * eval e2
adamc@236 173 end.
adamc@236 174
adamc@236 175 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 176 match e with
adamc@236 177 | Const n => Const (k * n)
adamc@236 178 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 179 | Mult e1 e2 => Mult (times k e1) e2
adamc@236 180 end.
adamc@236 181
adamc@236 182 Theorem eval_times : forall k e,
adamc@236 183 eval (times k e) = k * eval e.
adam@367 184 (** %\vspace{-.25in}%[[
adamc@236 185 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 186 trivial
adamc@236 187 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adam@367 188 ]]
adamc@236 189
adam@367 190 <<
adamc@236 191 Error: Expects a disjunctive pattern with 3 branches.
adam@367 192 >>
adam@302 193 *)
adamc@236 194
adamc@236 195 Abort.
adamc@236 196
adamc@236 197 (** 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 198
adamc@236 199 Theorem eval_times : forall k e,
adamc@236 200 eval (times k e) = k * eval e.
adamc@236 201 induction e as [ | ? IHe1 ? IHe2 | ? IHe1 ? IHe2 ]; [
adamc@236 202 trivial
adamc@236 203 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial
adamc@236 204 | simpl; rewrite IHe1; rewrite mult_assoc; trivial ].
adamc@236 205 Qed.
adamc@236 206
adamc@236 207 (** 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 208
adamc@236 209 Reset eval_times.
adamc@236 210
adam@375 211 Hint Rewrite mult_plus_distr_l.
adamc@238 212
adamc@236 213 Theorem eval_times : forall k e,
adamc@236 214 eval (times k e) = k * eval e.
adamc@236 215 induction e; crush.
adamc@236 216 Qed.
adam@368 217 (* end thide *)
adamc@236 218
adamc@237 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.
adamc@237 220
adamc@237 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.
adamc@237 222
adamc@237 223 An example should help illustrate what I mean. Consider this function, which rewrites an expression using associativity of addition and multiplication. *)
adamc@237 224
adamc@237 225 Fixpoint reassoc (e : exp) : exp :=
adamc@237 226 match e with
adamc@237 227 | Const _ => e
adamc@237 228 | Plus 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 | Plus e21 e22 => Plus (Plus e1' e21) e22
adamc@237 233 | _ => Plus e1' e2'
adamc@237 234 end
adamc@237 235 | Mult e1 e2 =>
adamc@237 236 let e1' := reassoc e1 in
adamc@237 237 let e2' := reassoc e2 in
adamc@237 238 match e2' with
adamc@237 239 | Mult e21 e22 => Mult (Mult e1' e21) e22
adamc@237 240 | _ => Mult e1' e2'
adamc@237 241 end
adamc@237 242 end.
adamc@237 243
adamc@237 244 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adam@368 245 (* begin thide *)
adamc@237 246 induction e; crush;
adamc@237 247 match goal with
adamc@237 248 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
adamc@237 249 destruct E; crush
adamc@237 250 end.
adamc@237 251
adamc@237 252 (** One subgoal remains:
adamc@237 253 [[
adamc@237 254 IHe2 : eval e3 * eval e4 = eval e2
adamc@237 255 ============================
adamc@237 256 eval e1 * eval e3 * eval e4 = eval e1 * eval e2
adamc@237 257 ]]
adamc@237 258
adamc@237 259 [crush] does not know how to finish this goal. We could finish the proof manually. *)
adamc@237 260
adamc@237 261 rewrite <- IHe2; crush.
adamc@237 262
adamc@237 263 (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
adamc@237 264
adamc@237 265 Abort.
adamc@237 266
adamc@237 267 Lemma rewr : forall a b c d, b * c = d -> a * b * c = a * d.
adamc@237 268 crush.
adamc@237 269 Qed.
adamc@237 270
adamc@237 271 Hint Resolve rewr.
adamc@237 272
adamc@237 273 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adamc@237 274 induction e; crush;
adamc@237 275 match goal with
adamc@237 276 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
adamc@237 277 destruct E; crush
adamc@237 278 end.
adamc@237 279 Qed.
adam@368 280 (* end thide *)
adamc@237 281
adamc@237 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.
adamc@237 283
adamc@237 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. *)
adamc@237 285
adamc@235 286
adamc@238 287 (** * Debugging and Maintaining Automation *)
adamc@238 288
adam@367 289 (** Fully automated proofs are desirable because they open up possibilities for automatic adaptation to changes of specification. A well-engineered script within a narrow domain can survive many changes to the formulation of the problem it solves. Still, as we are working with higher-order logic, most theorems fall within no obvious decidable theories. It is inevitable that most long-lived automated proofs will need updating.
adamc@238 290
adam@367 291 Before we are ready to update our proofs, we need to write them in the first place. While fully automated scripts are most robust to changes of specification, it is hard to write every new proof directly in that form. Instead, it is useful to begin a theorem with exploratory proving and then gradually refine it into a suitable automated form.
adamc@238 292
adam@350 293 Consider this theorem from Chapter 8, which we begin by proving in a mostly manual way, invoking [crush] after each steop to discharge any low-hanging fruit. Our manual effort involves choosing which expressions to case-analyze on. *)
adamc@238 294
adamc@238 295 (* begin hide *)
adamc@238 296 Require Import MoreDep.
adamc@238 297 (* end hide *)
adamc@238 298
adamc@238 299 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adam@368 300 (* begin thide *)
adamc@238 301 induction e; crush.
adamc@238 302
adamc@238 303 dep_destruct (cfold e1); crush.
adamc@238 304 dep_destruct (cfold e2); crush.
adamc@238 305
adamc@238 306 dep_destruct (cfold e1); crush.
adamc@238 307 dep_destruct (cfold e2); crush.
adamc@238 308
adamc@238 309 dep_destruct (cfold e1); crush.
adamc@238 310 dep_destruct (cfold e2); crush.
adamc@238 311
adamc@238 312 dep_destruct (cfold e1); crush.
adamc@238 313 dep_destruct (expDenote e1); crush.
adamc@238 314
adamc@238 315 dep_destruct (cfold e); crush.
adamc@238 316
adamc@238 317 dep_destruct (cfold e); crush.
adamc@238 318 Qed.
adamc@238 319
adamc@238 320 (** In this complete proof, it is hard to avoid noticing a pattern. We rework the proof, abstracting over the patterns we find. *)
adamc@238 321
adamc@238 322 Reset cfold_correct.
adamc@238 323
adamc@238 324 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@238 325 induction e; crush.
adamc@238 326
adamc@238 327 (** The expression we want to destruct here turns out to be the discriminee of a [match], and we can easily enough write a tactic that destructs all such expressions. *)
adamc@238 328
adamc@238 329 Ltac t :=
adamc@238 330 repeat (match goal with
adamc@238 331 | [ |- context[match ?E with NConst _ => _ | Plus _ _ => _
adamc@238 332 | Eq _ _ => _ | BConst _ => _ | And _ _ => _
adamc@238 333 | If _ _ _ _ => _ | Pair _ _ _ _ => _
adamc@238 334 | Fst _ _ _ => _ | Snd _ _ _ => _ end] ] =>
adamc@238 335 dep_destruct E
adamc@238 336 end; crush).
adamc@238 337
adamc@238 338 t.
adamc@238 339
adamc@238 340 (** This tactic invocation discharges the whole case. It does the same on the next two cases, but it gets stuck on the fourth case. *)
adamc@238 341
adamc@238 342 t.
adamc@238 343
adamc@238 344 t.
adamc@238 345
adamc@238 346 t.
adamc@238 347
adamc@238 348 (** The subgoal's conclusion is:
adamc@238 349 [[
adamc@238 350 ============================
adamc@238 351 (if expDenote e1 then expDenote (cfold e2) else expDenote (cfold e3)) =
adamc@238 352 expDenote (if expDenote e1 then cfold e2 else cfold e3)
adamc@238 353 ]]
adamc@238 354
adamc@238 355 We need to expand our [t] tactic to handle this case. *)
adamc@238 356
adamc@238 357 Ltac t' :=
adamc@238 358 repeat (match goal with
adamc@238 359 | [ |- context[match ?E with NConst _ => _ | Plus _ _ => _
adamc@238 360 | Eq _ _ => _ | BConst _ => _ | And _ _ => _
adamc@238 361 | If _ _ _ _ => _ | Pair _ _ _ _ => _
adamc@238 362 | Fst _ _ _ => _ | Snd _ _ _ => _ end] ] =>
adamc@238 363 dep_destruct E
adamc@238 364 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@238 365 end; crush).
adamc@238 366
adamc@238 367 t'.
adamc@238 368
adamc@238 369 (** Now the goal is discharged, but [t'] has no effect on the next subgoal. *)
adamc@238 370
adamc@238 371 t'.
adamc@238 372
adamc@238 373 (** A final revision of [t] finishes the proof. *)
adamc@238 374
adamc@238 375 Ltac t'' :=
adamc@238 376 repeat (match goal with
adamc@238 377 | [ |- context[match ?E with NConst _ => _ | Plus _ _ => _
adamc@238 378 | Eq _ _ => _ | BConst _ => _ | And _ _ => _
adamc@238 379 | If _ _ _ _ => _ | Pair _ _ _ _ => _
adamc@238 380 | Fst _ _ _ => _ | Snd _ _ _ => _ end] ] =>
adamc@238 381 dep_destruct E
adamc@238 382 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@238 383 | [ |- context[match pairOut ?E with Some _ => _
adamc@238 384 | None => _ end] ] =>
adamc@238 385 dep_destruct E
adamc@238 386 end; crush).
adamc@238 387
adamc@238 388 t''.
adamc@238 389
adamc@238 390 t''.
adamc@238 391 Qed.
adamc@238 392
adam@367 393 (** We can take the final tactic and move it into the initial part of the proof script, arriving at a nicely automated proof. *)
adamc@238 394
adamc@238 395 Reset t.
adamc@238 396
adamc@238 397 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@238 398 induction e; crush;
adamc@238 399 repeat (match goal with
adamc@238 400 | [ |- context[match ?E with NConst _ => _ | Plus _ _ => _
adamc@238 401 | Eq _ _ => _ | BConst _ => _ | And _ _ => _
adamc@238 402 | If _ _ _ _ => _ | Pair _ _ _ _ => _
adamc@238 403 | Fst _ _ _ => _ | Snd _ _ _ => _ end] ] =>
adamc@238 404 dep_destruct E
adamc@238 405 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@238 406 | [ |- context[match pairOut ?E with Some _ => _
adamc@238 407 | None => _ end] ] =>
adamc@238 408 dep_destruct E
adamc@238 409 end; crush).
adamc@238 410 Qed.
adam@368 411 (* end thide *)
adamc@238 412
adam@367 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?
adamc@240 414
adamc@240 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. *)
adamc@240 416
adamc@240 417 Reset reassoc_correct.
adamc@240 418
adamc@240 419 Theorem confounder : forall e1 e2 e3,
adamc@240 420 eval e1 * eval e2 * eval e3 = eval e1 * (eval e2 + 1 - 1) * eval e3.
adamc@240 421 crush.
adamc@240 422 Qed.
adamc@240 423
adam@375 424 Hint Rewrite confounder.
adamc@240 425
adamc@240 426 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adam@368 427 (* begin thide *)
adamc@240 428 induction e; crush;
adamc@240 429 match goal with
adamc@240 430 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
adamc@240 431 destruct E; crush
adamc@240 432 end.
adamc@240 433
adamc@240 434 (** One subgoal remains:
adamc@240 435
adamc@240 436 [[
adamc@240 437 ============================
adamc@240 438 eval e1 * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2
adamc@240 439 ]]
adamc@240 440
adam@367 441 The poorly chosen rewrite rule fired, changing the goal to a form where another hint no longer applies. Imagine that we are in the middle of a large development with many hints. How would we diagnose the problem? First, we might not be sure which case of the inductive proof has gone wrong. It is useful to separate out our automation procedure and apply it manually. *)
adamc@240 442
adamc@240 443 Restart.
adamc@240 444
adamc@240 445 Ltac t := crush; match goal with
adamc@240 446 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _
adamc@240 447 | Mult _ _ => _ end] ] =>
adamc@240 448 destruct E; crush
adamc@240 449 end.
adamc@240 450
adamc@240 451 induction e.
adamc@240 452
adamc@240 453 (** Since we see the subgoals before any simplification occurs, it is clear that this is the case for constants. [t] makes short work of it. *)
adamc@240 454
adamc@240 455 t.
adamc@240 456
adamc@240 457 (** The next subgoal, for addition, is also discharged without trouble. *)
adamc@240 458
adamc@240 459 t.
adamc@240 460
adamc@240 461 (** The final subgoal is for multiplication, and it is here that we get stuck in the proof state summarized above. *)
adamc@240 462
adamc@240 463 t.
adamc@240 464
adam@367 465 (** What is [t] doing to get us to this point? The %\index{tactics!info}%[info] command can help us answer this kind of question. *)
adamc@240 466
adamc@240 467 (** remove printing * *)
adamc@240 468 Undo.
adamc@240 469 info t.
adam@367 470 (** %\vspace{-.15in}%[[
adam@375 471 == simpl in *; intuition; subst; autorewrite with core in *;
adam@375 472 simpl in *; intuition; subst; autorewrite with core in *;
adamc@240 473 simpl in *; intuition; subst; destruct (reassoc e2).
adamc@240 474 simpl in *; intuition.
adamc@240 475
adamc@240 476 simpl in *; intuition.
adamc@240 477
adam@375 478 simpl in *; intuition; subst; autorewrite with core in *;
adamc@240 479 refine (eq_ind_r
adamc@240 480 (fun n : nat =>
adamc@240 481 n * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2) _ IHe1);
adam@375 482 autorewrite with core in *; simpl in *; intuition;
adam@375 483 subst; autorewrite with core in *; simpl in *;
adamc@240 484 intuition; subst.
adamc@240 485
adamc@240 486 ]]
adamc@240 487
adamc@240 488 A detailed trace of [t]'s execution appears. Since we are using the very general [crush] tactic, many of these steps have no effect and only occur as instances of a more general strategy. We can copy-and-paste the details to see where things go wrong. *)
adamc@240 489
adamc@240 490 Undo.
adamc@240 491
adamc@240 492 (** We arbitrarily split the script into chunks. The first few seem not to do any harm. *)
adamc@240 493
adam@375 494 simpl in *; intuition; subst; autorewrite with core in *.
adam@375 495 simpl in *; intuition; subst; autorewrite with core in *.
adamc@240 496 simpl in *; intuition; subst; destruct (reassoc e2).
adamc@240 497 simpl in *; intuition.
adamc@240 498 simpl in *; intuition.
adamc@240 499
adamc@240 500 (** The next step is revealed as the culprit, bringing us to the final unproved subgoal. *)
adamc@240 501
adam@375 502 simpl in *; intuition; subst; autorewrite with core in *.
adamc@240 503
adamc@240 504 (** We can split the steps further to assign blame. *)
adamc@240 505
adamc@240 506 Undo.
adamc@240 507
adamc@240 508 simpl in *.
adamc@240 509 intuition.
adamc@240 510 subst.
adam@375 511 autorewrite with core in *.
adamc@240 512
adamc@240 513 (** It was the final of these four tactics that made the rewrite. We can find out exactly what happened. The [info] command presents hierarchical views of proof steps, and we can zoom down to a lower level of detail by applying [info] to one of the steps that appeared in the original trace. *)
adamc@240 514
adamc@240 515 Undo.
adamc@240 516
adam@375 517 info autorewrite with core in *.
adam@367 518 (** %\vspace{-.15in}%[[
adamc@240 519 == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
adamc@240 520 (confounder (reassoc e1) e3 e4)).
adamc@240 521 ]]
adamc@240 522
adamc@240 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. *)
adamc@240 524
adamc@240 525 Abort.
adam@368 526 (* end thide *)
adamc@240 527
adamc@240 528 (** printing * $\times$ *)
adamc@240 529
adamc@241 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.
adamc@241 531
adamc@241 532 Here is one example of a performance surprise. *)
adamc@241 533
adamc@239 534 Section slow.
adamc@239 535 Hint Resolve trans_eq.
adamc@239 536
adamc@241 537 (** The central element of the problem is the addition of transitivity as a hint. With transitivity available, it is easy for proof search to wind up exploring exponential search spaces. We also add a few other arbitrary variables and hypotheses, designed to lead to trouble later. *)
adamc@241 538
adamc@239 539 Variable A : Set.
adamc@239 540 Variables P Q R S : A -> A -> Prop.
adamc@239 541 Variable f : A -> A.
adamc@239 542
adamc@239 543 Hypothesis H1 : forall x y, P x y -> Q x y -> R x y -> f x = f y.
adamc@239 544 Hypothesis H2 : forall x y, S x y -> R x y.
adamc@239 545
adam@367 546 (** We prove a simple lemma very quickly, using the %\index{Vernacular commands!Time}%[Time] command to measure exactly how quickly. *)
adamc@241 547
adamc@239 548 Lemma slow : forall x y, P x y -> Q x y -> S x y -> f x = f y.
adamc@241 549 Time eauto 6.
adam@367 550 (** %\vspace{-.2in}%[[
adamc@241 551 Finished transaction in 0. secs (0.068004u,0.s)
adam@302 552 ]]
adam@302 553 *)
adamc@241 554
adamc@239 555 Qed.
adamc@239 556
adamc@241 557 (** Now we add a different hypothesis, which is innocent enough; in fact, it is even provable as a theorem. *)
adamc@241 558
adamc@239 559 Hypothesis H3 : forall x y, x = y -> f x = f y.
adamc@239 560
adamc@239 561 Lemma slow' : forall x y, P x y -> Q x y -> S x y -> f x = f y.
adamc@241 562 Time eauto 6.
adam@367 563 (** %\vspace{-.2in}%[[
adamc@241 564 Finished transaction in 2. secs (1.264079u,0.s)
adamc@241 565 ]]
adamc@241 566
adamc@241 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. *)
adamc@241 568
adam@368 569 (* begin thide *)
adamc@241 570 Restart.
adamc@241 571 info eauto 6.
adam@367 572 (** %\vspace{-.15in}%[[
adamc@241 573 == intro x; intro y; intro H; intro H0; intro H4;
adamc@241 574 simple eapply trans_eq.
adamc@241 575 simple apply refl_equal.
adamc@241 576
adamc@241 577 simple eapply trans_eq.
adamc@241 578 simple apply refl_equal.
adamc@241 579
adamc@241 580 simple eapply trans_eq.
adamc@241 581 simple apply refl_equal.
adamc@241 582
adamc@241 583 simple apply H1.
adamc@241 584 eexact H.
adamc@241 585
adamc@241 586 eexact H0.
adamc@241 587
adamc@241 588 simple apply H2; eexact H4.
adamc@241 589 ]]
adamc@241 590
adam@367 591 This output does not tell us why proof search takes so long, but it does provide a clue that would be useful if we had forgotten that we added transitivity as a hint. The [eauto] tactic is applying depth-first search, and the proof script where the real action is ends up buried inside a chain of pointless invocations of transitivity, where each invocation uses reflexivity to discharge one subgoal. Each increment to the depth argument to [eauto] adds another silly use of transitivity. This wasted proof effort only adds linear time overhead, as long as proof search never makes false steps. No false steps were made before we added the new hypothesis, but somehow the addition made possible a new faulty path. To understand which paths we enabled, we can use the %\index{tactics!debug}%[debug] command. *)
adamc@241 592
adamc@241 593 Restart.
adamc@241 594 debug eauto 6.
adamc@241 595
adamc@241 596 (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening:
adamc@241 597 [[
adamc@241 598 1 depth=6
adamc@241 599 1.1 depth=6 intro
adamc@241 600 1.1.1 depth=6 intro
adamc@241 601 1.1.1.1 depth=6 intro
adamc@241 602 1.1.1.1.1 depth=6 intro
adamc@241 603 1.1.1.1.1.1 depth=6 intro
adamc@241 604 1.1.1.1.1.1.1 depth=5 apply H3
adamc@241 605 1.1.1.1.1.1.1.1 depth=4 eapply trans_eq
adamc@241 606 1.1.1.1.1.1.1.1.1 depth=4 apply refl_equal
adamc@241 607 1.1.1.1.1.1.1.1.1.1 depth=3 eapply trans_eq
adamc@241 608 1.1.1.1.1.1.1.1.1.1.1 depth=3 apply refl_equal
adamc@241 609 1.1.1.1.1.1.1.1.1.1.1.1 depth=2 eapply trans_eq
adamc@241 610 1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply refl_equal
adamc@241 611 1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 eapply trans_eq
adamc@241 612 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply refl_equal
adamc@241 613 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=0 eapply trans_eq
adamc@241 614 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=1 apply sym_eq ; trivial
adamc@241 615 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=0 eapply trans_eq
adamc@241 616 1.1.1.1.1.1.1.1.1.1.1.1.1.1.3 depth=0 eapply trans_eq
adamc@241 617 1.1.1.1.1.1.1.1.1.1.1.1.2 depth=2 apply sym_eq ; trivial
adamc@241 618 1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=1 eapply trans_eq
adamc@241 619 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply refl_equal
adamc@241 620 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 depth=0 eapply trans_eq
adamc@241 621 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2 depth=1 apply sym_eq ; trivial
adamc@241 622 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2.1 depth=0 eapply trans_eq
adamc@241 623 1.1.1.1.1.1.1.1.1.1.1.1.2.1.3 depth=0 eapply trans_eq
adamc@241 624 ]]
adamc@241 625
adam@367 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. *)
adamc@241 627
adamc@239 628 Qed.
adam@368 629 (* end thide *)
adamc@239 630 End slow.
adamc@239 631
adam@367 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.
adamc@241 633
adam@367 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]. *)
adamc@241 635
adamc@238 636
adamc@235 637 (** * Modules *)
adamc@235 638
adam@367 639 (** Last chapter's examples of proof by reflection demonstrate opportunities for implementing abstract proof strategies with stronger formal guarantees than can be had with Ltac scripting. Coq's %\textit{%#<i>#module system#</i>#%}% provides another tool for more rigorous development of generic theorems. This feature is inspired by the module systems found in Standard ML%~\cite{modules}% and Objective Caml, and the discussion that follows assumes familiarity with the basics of one of those systems.
adamc@242 640
adam@367 641 ML modules facilitate the grouping of %\index{abstract type}%abstract types with operations over those types. Moreover, there is support for %\index{functor}\textit{%#<i>#functors#</i>#%}%, which are functions from modules to modules. A canonical example of a functor is one that builds a data structure implementation from a module that describes a domain of keys and its associated comparison operations.
adamc@242 642
adam@367 643 When we add modules to a base language with dependent types, it becomes possible to use modules and functors to formalize kinds of reasoning that are common in algebra. For instance, this module signature captures the essence of the algebraic structure known as a group. A group consists of a carrier set [G], an associative binary operation [f], a left identity element [e] for [f], and an operation [i] that is a left inverse for [f].%\index{Vernacular commands!Module Type}% *)
adamc@242 644
adamc@235 645 Module Type GROUP.
adamc@235 646 Parameter G : Set.
adamc@235 647 Parameter f : G -> G -> G.
adamc@235 648 Parameter e : G.
adamc@235 649 Parameter i : G -> G.
adamc@235 650
adamc@235 651 Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
adamc@235 652 Axiom ident : forall a, f e a = a.
adamc@235 653 Axiom inverse : forall a, f (i a) a = e.
adamc@235 654 End GROUP.
adamc@235 655
adam@367 656 (** Many useful theorems hold of arbitrary groups. We capture some such theorem statements in another module signature.%\index{Vernacular commands!Declare Module}% *)
adamc@242 657
adamc@235 658 Module Type GROUP_THEOREMS.
adamc@235 659 Declare Module M : GROUP.
adamc@235 660
adamc@235 661 Axiom ident' : forall a, M.f a M.e = a.
adamc@235 662
adamc@235 663 Axiom inverse' : forall a, M.f a (M.i a) = M.e.
adamc@235 664
adamc@235 665 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 666 End GROUP_THEOREMS.
adamc@235 667
adam@367 668 (** We implement generic proofs of these theorems with a functor, whose input is an arbitrary group [M]. The proofs are completely manual, since it would take some effort to build suitable generic automation; rather, these theorems can serve as a basis for an automated procedure for simplifying group expressions, along the lines of the procedure for monoids from the last chapter. We take the proofs from the Wikipedia page on elementary group theory.%\index{Vernacular commands!Module}% *)
adamc@242 669
adamc@239 670 Module Group (M : GROUP) : GROUP_THEOREMS with Module M := M.
adamc@235 671 Module M := M.
adamc@235 672
adamc@235 673 Import M.
adamc@235 674
adamc@235 675 Theorem inverse' : forall a, f a (i a) = e.
adamc@235 676 intro.
adamc@235 677 rewrite <- (ident (f a (i a))).
adamc@235 678 rewrite <- (inverse (f a (i a))) at 1.
adamc@235 679 rewrite assoc.
adamc@235 680 rewrite assoc.
adamc@235 681 rewrite <- (assoc (i a) a (i a)).
adamc@235 682 rewrite inverse.
adamc@235 683 rewrite ident.
adamc@235 684 apply inverse.
adamc@235 685 Qed.
adamc@235 686
adamc@235 687 Theorem ident' : forall a, f a e = a.
adamc@235 688 intro.
adamc@235 689 rewrite <- (inverse a).
adamc@235 690 rewrite <- assoc.
adamc@235 691 rewrite inverse'.
adamc@235 692 apply ident.
adamc@235 693 Qed.
adamc@235 694
adamc@235 695 Theorem unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 696 intros.
adamc@235 697 rewrite <- (H e).
adamc@235 698 symmetry.
adamc@235 699 apply ident'.
adamc@235 700 Qed.
adamc@235 701 End Group.
adamc@239 702
adamc@242 703 (** We can show that the integers with [+] form a group. *)
adamc@242 704
adamc@239 705 Require Import ZArith.
adamc@239 706 Open Scope Z_scope.
adamc@239 707
adamc@239 708 Module Int.
adamc@239 709 Definition G := Z.
adamc@239 710 Definition f x y := x + y.
adamc@239 711 Definition e := 0.
adamc@239 712 Definition i x := -x.
adamc@239 713
adamc@239 714 Theorem assoc : forall a b c, f (f a b) c = f a (f b c).
adamc@239 715 unfold f; crush.
adamc@239 716 Qed.
adamc@239 717 Theorem ident : forall a, f e a = a.
adamc@239 718 unfold f, e; crush.
adamc@239 719 Qed.
adamc@239 720 Theorem inverse : forall a, f (i a) a = e.
adamc@239 721 unfold f, i, e; crush.
adamc@239 722 Qed.
adamc@239 723 End Int.
adamc@239 724
adamc@242 725 (** Next, we can produce integer-specific versions of the generic group theorems. *)
adamc@242 726
adamc@239 727 Module IntTheorems := Group(Int).
adamc@239 728
adamc@239 729 Check IntTheorems.unique_ident.
adamc@242 730 (** %\vspace{-.15in}% [[
adamc@242 731 IntTheorems.unique_ident
adamc@242 732 : forall e' : Int.G, (forall a : Int.G, Int.f e' a = a) -> e' = Int.e
adam@302 733 ]]
adam@367 734
adam@367 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: *)
adamc@239 736
adamc@239 737 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0.
adam@368 738 (* begin thide *)
adamc@239 739 exact IntTheorems.unique_ident.
adamc@239 740 Qed.
adam@368 741 (* end thide *)
adamc@242 742
adam@367 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. *)
adamc@243 744
adamc@243 745
adamc@243 746 (** * Build Processes *)
adamc@243 747
adamc@243 748 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities.
adamc@243 749
adam@367 750 Consider a library that we will name [Lib], housed in directory %\texttt{%#<tt>#LIB#</tt>#%}% and split between files %\texttt{%#<tt>#A.v#</tt>#%}%, %\texttt{%#<tt>#B.v#</tt>#%}%, and %\texttt{%#<tt>#C.v#</tt>#%}%. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}\texttt{%#<tt>#coq_makefile#</tt>#%}% to do the hard work.
adamc@243 751
adamc@243 752 <<
adamc@243 753 MODULES := A B C
adamc@243 754 VS := $(MODULES:%=%.v)
adamc@243 755
adamc@243 756 .PHONY: coq clean
adamc@243 757
adamc@243 758 coq: Makefile.coq
adam@369 759 $(MAKE) -f Makefile.coq
adamc@243 760
adamc@243 761 Makefile.coq: Makefile $(VS)
adamc@243 762 coq_makefile -R . Lib $(VS) -o Makefile.coq
adamc@243 763
adamc@243 764 clean:: Makefile.coq
adam@369 765 $(MAKE) -f Makefile.coq clean
adamc@243 766 rm -f Makefile.coq
adamc@243 767 >>
adamc@243 768
adamc@243 769 The Makefile begins by defining a variable %\texttt{%#<tt>#VS#</tt>#%}% holding the list of filenames to be included in the project. The primary target is %\texttt{%#<tt>#coq#</tt>#%}%, which depends on the construction of an auxiliary Makefile called %\texttt{%#<tt>#Makefile.coq#</tt>#%}%. Another rule explains how to build that file. We call %\texttt{%#<tt>#coq_makefile#</tt>#%}%, using the %\texttt{%#<tt>#-R#</tt>#%}% flag to specify that files in the current directory should be considered to belong to the library [Lib]. This Makefile will build a compiled version of each module, such that %\texttt{%#<tt>#X.v#</tt>#%}% is compiled into %\texttt{%#<tt>#X.vo#</tt>#%}%.
adamc@243 770
adamc@243 771 Now code in %\texttt{%#<tt>#B.v#</tt>#%}% may refer to definitions in %\texttt{%#<tt>#A.v#</tt>#%}% after running
adamc@243 772 [[
adamc@243 773 Require Import Lib.A.
adam@367 774 ]]
adam@367 775 %\vspace{-.15in}%Library [Lib] is presented as a module, containing a submodule [A], which contains the definitions from %\texttt{%#<tt>#A.v#</tt>#%}%. These are genuine modules in the sense of Coq's module system, and they may be passed to functors and so on.
adamc@243 776
adam@367 777 The command [Require Import] is a convenient combination of two more primitive commands. The %\index{Vernacular commands!Require}%[Require] command finds the %\texttt{%#<tt>#.vo#</tt>#%}% file containing the named module, ensuring that the module is loaded into memory. The %\index{Vernacular commands!Import}%[Import] command loads all top-level definitions of the named module into the current namespace, and it may be used with local modules that do not have corresponding %\texttt{%#<tt>#.vo#</tt>#%}% files. Another command, %\index{Vernacular commands!Load}%[Load], is for inserting the contents of a named file verbatim. It is generally better to use the module-based commands, since they avoid rerunning proof scripts, and they facilitate reorganization of directory structure without the need to change code.
adamc@243 778
adamc@243 779 Now we would like to use our library from a different development, called [Client] and found in directory %\texttt{%#<tt>#CLIENT#</tt>#%}%, which has its own Makefile.
adamc@243 780
adamc@243 781 <<
adamc@243 782 MODULES := D E
adamc@243 783 VS := $(MODULES:%=%.v)
adamc@243 784
adamc@243 785 .PHONY: coq clean
adamc@243 786
adamc@243 787 coq: Makefile.coq
adam@369 788 $(MAKE) -f Makefile.coq
adamc@243 789
adamc@243 790 Makefile.coq: Makefile $(VS)
adamc@243 791 coq_makefile -R LIB Lib -R . Client $(VS) -o Makefile.coq
adamc@243 792
adamc@243 793 clean:: Makefile.coq
adam@369 794 $(MAKE) -f Makefile.coq clean
adamc@243 795 rm -f Makefile.coq
adamc@243 796 >>
adamc@243 797
adamc@243 798 We change the %\texttt{%#<tt>#coq_makefile#</tt>#%}% call to indicate where the library [Lib] is found. Now %\texttt{%#<tt>#D.v#</tt>#%}% and %\texttt{%#<tt>#E.v#</tt>#%}% can refer to definitions from [Lib] module [A] after running
adamc@243 799 [[
adamc@243 800 Require Import Lib.A.
adamc@243 801 ]]
adam@367 802 %\vspace{-.15in}\noindent{}%and %\texttt{%#<tt>#E.v#</tt>#%}% can refer to definitions from %\texttt{%#<tt>#D.v#</tt>#%}% by running
adamc@243 803 [[
adamc@243 804 Require Import Client.D.
adamc@243 805 ]]
adam@367 806 %\vspace{-.15in}%It can be useful to split a library into several files, but it is also inconvenient for client code to import library modules individually. We can get the best of both worlds by, for example, adding an extra source file %\texttt{%#<tt>#Lib.v#</tt>#%}% to [Lib]'s directory and Makefile, where that file contains just this line:%\index{Vernacular commands!Require Export}%
adamc@243 807 [[
adamc@243 808 Require Export Lib.A Lib.B Lib.C.
adamc@243 809 ]]
adam@367 810 %\vspace{-.15in}%Now client code can import all definitions from all of [Lib]'s modules simply by running
adamc@243 811 [[
adamc@243 812 Require Import Lib.
adamc@243 813 ]]
adam@367 814 %\vspace{-.15in}%The two Makefiles above share a lot of code, so, in practice, it is useful to define a common Makefile that is included by multiple library-specific Makefiles.
adamc@243 815
adamc@243 816 %\medskip%
adamc@243 817
adamc@243 818 The remaining ingredient is the proper way of editing library code files in Proof General. Recall this snippet of %\texttt{%#<tt>#.emacs#</tt>#%}% code from Chapter 2, which tells Proof General where to find the library associated with this book.
adamc@243 819
adamc@243 820 <<
adamc@243 821 (custom-set-variables
adamc@243 822 ...
adamc@243 823 '(coq-prog-args '("-I" "/path/to/cpdt/src"))
adamc@243 824 ...
adamc@243 825 )
adamc@243 826 >>
adamc@243 827
adamc@243 828 To do interactive editing of our current example, we just need to change the flags to point to the right places.
adamc@243 829
adamc@243 830 <<
adamc@243 831 (custom-set-variables
adamc@243 832 ...
adamc@243 833 ; '(coq-prog-args '("-I" "/path/to/cpdt/src"))
adamc@243 834 '(coq-prog-args '("-R" "LIB" "Lib" "-R" "CLIENT" "Client"))
adamc@243 835 ...
adamc@243 836 )
adamc@243 837 >>
adamc@243 838
adamc@243 839 When working on multiple projects, it is useful to leave multiple versions of this setting in your %\texttt{%#<tt>#.emacs#</tt>#%}% file, commenting out all but one of them at any moment in time. To switch between projects, change the commenting structure and restart Emacs. *)