Mercurial > cpdt > repo

annotate src/Large.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents f874c163f5e0
children
rev   line source
adam@534 1 (* Copyright (c) 2009-2012, 2015, 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@534 13 Require Import Cpdt.CpdtTactics.
adamc@235 14
adamc@235 15 Set Implicit Arguments.
adam@534 16 Set Asymmetric Patterns.
adamc@235 17 (* end hide *)
adamc@235 18
adamc@235 19
adam@381 20 (** %\part{The Big Picture}
adam@381 21
adam@381 22 \chapter{Proving in the Large}% *)
adamc@235 23
adam@433 24 (** 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 25
adamc@236 26 Thus, this chapter gives some tips for structuring and maintaining large Coq developments. *)
adamc@236 27
adamc@236 28
adamc@236 29 (** * Ltac Anti-Patterns *)
adamc@236 30
adam@433 31 (** 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 32
adamc@237 33 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 34
adamc@236 35 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 36
adamc@236 37 Inductive exp : Set :=
adamc@236 38 | Const : nat -> exp
adamc@236 39 | Plus : exp -> exp -> exp.
adamc@236 40
adamc@236 41 Fixpoint eval (e : exp) : nat :=
adamc@236 42 match e with
adamc@236 43 | Const n => n
adamc@236 44 | Plus e1 e2 => eval e1 + eval e2
adamc@236 45 end.
adamc@236 46
adamc@236 47 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 48 match e with
adamc@236 49 | Const n => Const (k * n)
adamc@236 50 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 51 end.
adamc@236 52
adam@452 53 (** We can write a very manual proof that [times] really implements multiplication. *)
adamc@236 54
adamc@236 55 Theorem eval_times : forall k e,
adamc@236 56 eval (times k e) = k * eval e.
adamc@236 57 induction e.
adamc@236 58
adamc@236 59 trivial.
adamc@236 60
adamc@236 61 simpl.
adamc@236 62 rewrite IHe1.
adamc@236 63 rewrite IHe2.
adamc@236 64 rewrite mult_plus_distr_l.
adamc@236 65 trivial.
adamc@236 66 Qed.
adamc@236 67
adam@368 68 (* begin thide *)
adam@367 69 (** 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 70
adamc@236 71 Reset eval_times.
adamc@236 72
adam@368 73 Theorem eval_times : forall k x,
adamc@236 74 eval (times k x) = k * eval x.
adamc@236 75 induction x.
adamc@236 76
adamc@236 77 trivial.
adamc@236 78
adamc@236 79 simpl.
adam@367 80 (** %\vspace{-.15in}%[[
adamc@236 81 rewrite IHe1.
adam@367 82 ]]
adamc@236 83
adam@367 84 <<
adamc@236 85 Error: The reference IHe1 was not found in the current environment.
adam@367 86 >>
adamc@236 87
adamc@236 88 The inductive hypotheses are named [IHx1] and [IHx2] now, not [IHe1] and [IHe2]. *)
adamc@236 89
adamc@236 90 Abort.
adamc@236 91
adamc@236 92 (** 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 93
adamc@236 94 Theorem eval_times : forall k e,
adamc@236 95 eval (times k e) = k * eval e.
adamc@236 96 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 97
adamc@236 98 trivial.
adamc@236 99
adamc@236 100 simpl.
adamc@236 101 rewrite IHe1.
adamc@236 102 rewrite IHe2.
adamc@236 103 rewrite mult_plus_distr_l.
adamc@236 104 trivial.
adamc@236 105 Qed.
adamc@236 106
adam@509 107 (** We pass %\index{tactics!induction}%[induction] an%\index{intro pattern}% _intro pattern_, using a [|] character to separate 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 108
adamc@237 109 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 110
adamc@236 111 Reset times.
adamc@236 112
adamc@236 113 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 114 match e with
adamc@236 115 | Const n => Const (1 + k * n)
adamc@236 116 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 117 end.
adamc@236 118
adamc@236 119 Theorem eval_times : forall k e,
adamc@236 120 eval (times k e) = k * eval e.
adamc@236 121 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 122
adamc@236 123 trivial.
adamc@236 124
adamc@236 125 simpl.
adam@367 126 (** %\vspace{-.15in}%[[
adamc@236 127 rewrite IHe1.
adam@367 128 ]]
adamc@236 129
adam@367 130 <<
adamc@236 131 Error: The reference IHe1 was not found in the current environment.
adam@367 132 >>
adam@302 133 *)
adamc@236 134
adamc@236 135 Abort.
adamc@236 136
adam@398 137 (** 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 _first_ case instead.
adamc@237 138
adam@433 139 The problem with [trivial] could be "solved" by writing, e.g., [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 generate 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 140
adamc@236 141 Reset times.
adamc@236 142
adamc@236 143 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 144 match e with
adamc@236 145 | Const n => Const (k * n)
adamc@236 146 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 147 end.
adamc@236 148
adam@387 149 (** Many real developments try to make essentially unstructured proofs look structured by applying careful indentation conventions, idempotent case-marker tactics included solely 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 150
adamc@236 151 We can rewrite the current proof with a single tactic. *)
adamc@236 152
adamc@236 153 Theorem eval_times : forall k e,
adamc@236 154 eval (times k e) = k * eval e.
adamc@236 155 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 156 trivial
adamc@236 157 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adamc@236 158 Qed.
adamc@236 159
adam@509 160 (** We use the form of the semicolon operator that allows a different tactic to be specified for each generated subgoal. This change improves the 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. The same could be said for scripts using the%\index{bullets}% _bullets_ or curly braces provided by Coq 8.4, which allow code like the above to be stepped through interactively, with periods in place of the semicolons, while representing proof structure in a way that is enforced by Coq. Interactive replay of scripts becomes easier, but readability is not really helped.
adamc@236 161
adamc@236 162 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 163
adamc@236 164 Reset exp.
adamc@236 165
adamc@236 166 Inductive exp : Set :=
adamc@236 167 | Const : nat -> exp
adamc@236 168 | Plus : exp -> exp -> exp
adamc@236 169 | Mult : exp -> exp -> exp.
adamc@236 170
adamc@236 171 Fixpoint eval (e : exp) : nat :=
adamc@236 172 match e with
adamc@236 173 | Const n => n
adamc@236 174 | Plus e1 e2 => eval e1 + eval e2
adamc@236 175 | Mult e1 e2 => eval e1 * eval e2
adamc@236 176 end.
adamc@236 177
adamc@236 178 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 179 match e with
adamc@236 180 | Const n => Const (k * n)
adamc@236 181 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 182 | Mult e1 e2 => Mult (times k e1) e2
adamc@236 183 end.
adamc@236 184
adamc@236 185 Theorem eval_times : forall k e,
adamc@236 186 eval (times k e) = k * eval e.
adam@367 187 (** %\vspace{-.25in}%[[
adamc@236 188 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 189 trivial
adamc@236 190 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adam@367 191 ]]
adamc@236 192
adam@367 193 <<
adamc@236 194 Error: Expects a disjunctive pattern with 3 branches.
adam@367 195 >>
adam@302 196 *)
adamc@236 197 Abort.
adamc@236 198
adamc@236 199 (** 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 200
adamc@236 201 Theorem eval_times : forall k e,
adamc@236 202 eval (times k e) = k * eval e.
adamc@236 203 induction e as [ | ? IHe1 ? IHe2 | ? IHe1 ? IHe2 ]; [
adamc@236 204 trivial
adamc@236 205 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial
adamc@236 206 | simpl; rewrite IHe1; rewrite mult_assoc; trivial ].
adamc@236 207 Qed.
adamc@236 208
adamc@236 209 (** 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 210
adamc@236 211 Reset eval_times.
adamc@236 212
adam@375 213 Hint Rewrite mult_plus_distr_l.
adamc@238 214
adamc@236 215 Theorem eval_times : forall k e,
adamc@236 216 eval (times k e) = k * eval e.
adamc@236 217 induction e; crush.
adamc@236 218 Qed.
adam@368 219 (* end thide *)
adamc@236 220
adam@491 221 (** 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 might as well cut out the steps and automate as much as possible.
adamc@237 222
adam@398 223 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 _real_ big ideas should be expressed through lemmas that are added as hints.
adamc@237 224
adamc@237 225 An example should help illustrate what I mean. Consider this function, which rewrites an expression using associativity of addition and multiplication. *)
adamc@237 226
adamc@237 227 Fixpoint reassoc (e : exp) : exp :=
adamc@237 228 match e with
adamc@237 229 | Const _ => e
adamc@237 230 | Plus e1 e2 =>
adamc@237 231 let e1' := reassoc e1 in
adamc@237 232 let e2' := reassoc e2 in
adamc@237 233 match e2' with
adamc@237 234 | Plus e21 e22 => Plus (Plus e1' e21) e22
adamc@237 235 | _ => Plus e1' e2'
adamc@237 236 end
adamc@237 237 | Mult e1 e2 =>
adamc@237 238 let e1' := reassoc e1 in
adamc@237 239 let e2' := reassoc e2 in
adamc@237 240 match e2' with
adamc@237 241 | Mult e21 e22 => Mult (Mult e1' e21) e22
adamc@237 242 | _ => Mult e1' e2'
adamc@237 243 end
adamc@237 244 end.
adamc@237 245
adamc@237 246 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adam@368 247 (* begin thide *)
adamc@237 248 induction e; crush;
adamc@237 249 match goal with
adam@413 250 | [ |- context[match ?E with Const _ => _ | _ => _ end] ] =>
adamc@237 251 destruct E; crush
adamc@237 252 end.
adamc@237 253
adamc@237 254 (** One subgoal remains:
adamc@237 255 [[
adamc@237 256 IHe2 : eval e3 * eval e4 = eval e2
adamc@237 257 ============================
adamc@237 258 eval e1 * eval e3 * eval e4 = eval e1 * eval e2
adamc@237 259 ]]
adamc@237 260
adam@574 261 The [crush] tactic does not know how to finish this goal. We could finish the proof manually. Just kidding, the standard library got smarter, and the following is now redundant! *)
adamc@237 262
adam@574 263 (*rewrite <- IHe2; crush.*)
adamc@237 264
adamc@237 265 (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
adamc@237 266
adamc@237 267 Abort.
adamc@237 268
adamc@237 269 Lemma rewr : forall a b c d, b * c = d -> a * b * c = a * d.
adamc@237 270 crush.
adamc@237 271 Qed.
adamc@237 272
adamc@237 273 Hint Resolve rewr.
adamc@237 274
adamc@237 275 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adamc@237 276 induction e; crush;
adamc@237 277 match goal with
adam@413 278 | [ |- context[match ?E with Const _ => _ | _ => _ end] ] =>
adamc@237 279 destruct E; crush
adamc@237 280 end.
adamc@237 281 Qed.
adam@368 282 (* end thide *)
adamc@237 283
adamc@237 284 (** 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 285
adam@387 286 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.
adam@387 287
adam@413 288 A competing alternative to the common style of Coq tactics is the%\index{declarative proof scripts}% _declarative_ style, most frequently associated today with the %\index{Isar}%Isar%~\cite{Isar}% language. A declarative proof script is very explicit about subgoal structure and introduction of local names, aiming for human readability. The coding of proof automation is taken to be outside the scope of the proof language, an assumption related to the idea that it is not worth building new automation for each serious theorem. I have shown in this book many examples of theorem-specific automation, which I believe is crucial for scaling to significant results. Declarative proof scripts make it easier to read scripts to modify them for theorem statement changes, but the alternate%\index{adaptive proof scripts}% _adaptive_ style from this book allows use of the _same_ scripts for many versions of a theorem.
adam@387 289
adam@387 290 Perhaps I am a pessimist for thinking that fully formal proofs will inevitably consist of details that are uninteresting to people, but it is my preference to focus on conveying proof-specific details through choice of lemmas. Additionally, adaptive Ltac scripts contain bits of automation that can be understood in isolation. For instance, in a big [repeat match] loop, each case can generally be digested separately, which is a big contrast from trying to understand the hierarchical structure of a script in a more common style. Adaptive scripts rely on variable binding, but generally only over very small scopes, whereas understanding a traditional script requires tracking the identities of local variables potentially across pages of code.
adam@387 291
adam@509 292 One might also wonder why it makes sense to prove all theorems automatically (in the sense of adaptive proof scripts) but not construct all programs automatically. My view there is that _program synthesis_ is a very useful idea that deserves broader application! In practice, there are difficult obstacles in the way of finding a program automatically from its specification. A typical specification is not exhaustive in its description of program properties. For instance, details of performance on particular machine architectures are often omitted. As a result, a synthesized program may be correct in some sense while suffering from deficiencies in other senses. Program synthesis research will continue to come up with ways of dealing with this problem, but the situation for theorem proving is fundamentally different. Following mathematical practice, the only property of a formal proof that we care about is which theorem it proves, and it is trivial to check this property automatically. In other words, with a simple criterion for what makes a proof acceptable, automatic search is straightforward. Of course, in practice we also care about understandability of proofs to facilitate long-term maintenance, which is just what motivates the techniques outlined above, and the next section gives some related advice. *)
adamc@237 293
adamc@235 294
adamc@238 295 (** * Debugging and Maintaining Automation *)
adamc@238 296
adam@367 297 (** 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 298
adam@367 299 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 300
adam@387 301 Consider this theorem from Chapter 8, which we begin by proving in a mostly manual way, invoking [crush] after each step to discharge any low-hanging fruit. Our manual effort involves choosing which expressions to case-analyze on. *)
adamc@238 302
adamc@238 303 (* begin hide *)
adamc@238 304 Require Import MoreDep.
adamc@238 305 (* end hide *)
adamc@238 306
adamc@238 307 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adam@368 308 (* begin thide *)
adamc@238 309 induction e; crush.
adamc@238 310
adamc@238 311 dep_destruct (cfold e1); crush.
adamc@238 312 dep_destruct (cfold e2); crush.
adamc@238 313
adamc@238 314 dep_destruct (cfold e1); crush.
adamc@238 315 dep_destruct (cfold e2); crush.
adamc@238 316
adamc@238 317 dep_destruct (cfold e1); crush.
adamc@238 318 dep_destruct (cfold e2); crush.
adamc@238 319
adamc@238 320 dep_destruct (cfold e1); crush.
adamc@238 321 dep_destruct (expDenote e1); crush.
adamc@238 322
adamc@238 323 dep_destruct (cfold e); crush.
adamc@238 324
adamc@238 325 dep_destruct (cfold e); crush.
adamc@238 326 Qed.
adamc@238 327
adamc@238 328 (** In this complete proof, it is hard to avoid noticing a pattern. We rework the proof, abstracting over the patterns we find. *)
adamc@238 329
adamc@238 330 Reset cfold_correct.
adamc@238 331
adamc@238 332 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@238 333 induction e; crush.
adamc@238 334
adamc@238 335 (** 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 336
adamc@238 337 Ltac t :=
adamc@238 338 repeat (match goal with
adam@413 339 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
adamc@238 340 dep_destruct E
adamc@238 341 end; crush).
adamc@238 342
adamc@238 343 t.
adamc@238 344
adamc@238 345 (** 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 346
adamc@238 347 t.
adamc@238 348
adamc@238 349 t.
adamc@238 350
adamc@238 351 t.
adamc@238 352
adamc@238 353 (** The subgoal's conclusion is:
adamc@238 354 [[
adamc@238 355 ============================
adamc@238 356 (if expDenote e1 then expDenote (cfold e2) else expDenote (cfold e3)) =
adamc@238 357 expDenote (if expDenote e1 then cfold e2 else cfold e3)
adamc@238 358 ]]
adamc@238 359
adamc@238 360 We need to expand our [t] tactic to handle this case. *)
adamc@238 361
adamc@238 362 Ltac t' :=
adamc@238 363 repeat (match goal with
adam@413 364 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
adamc@238 365 dep_destruct E
adamc@238 366 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@238 367 end; crush).
adamc@238 368
adamc@238 369 t'.
adamc@238 370
adamc@238 371 (** Now the goal is discharged, but [t'] has no effect on the next subgoal. *)
adamc@238 372
adamc@238 373 t'.
adamc@238 374
adamc@238 375 (** A final revision of [t] finishes the proof. *)
adamc@238 376
adamc@238 377 Ltac t'' :=
adamc@238 378 repeat (match goal with
adam@413 379 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
adamc@238 380 dep_destruct E
adamc@238 381 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@238 382 | [ |- context[match pairOut ?E with Some _ => _
adamc@238 383 | None => _ end] ] =>
adamc@238 384 dep_destruct E
adamc@238 385 end; crush).
adamc@238 386
adamc@238 387 t''.
adamc@238 388
adamc@238 389 t''.
adamc@238 390 Qed.
adamc@238 391
adam@367 392 (** 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 393
adam@534 394 Reset cfold_correct.
adamc@238 395
adamc@238 396 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@238 397 induction e; crush;
adamc@238 398 repeat (match goal with
adam@413 399 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
adamc@238 400 dep_destruct E
adamc@238 401 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@238 402 | [ |- context[match pairOut ?E with Some _ => _
adamc@238 403 | None => _ end] ] =>
adamc@238 404 dep_destruct E
adamc@238 405 end; crush).
adamc@238 406 Qed.
adam@368 407 (* end thide *)
adamc@238 408
adam@367 409 (** 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 410
adamc@240 411 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 412
adamc@240 413 Reset reassoc_correct.
adamc@240 414
adamc@240 415 Theorem confounder : forall e1 e2 e3,
adamc@240 416 eval e1 * eval e2 * eval e3 = eval e1 * (eval e2 + 1 - 1) * eval e3.
adamc@240 417 crush.
adamc@240 418 Qed.
adamc@240 419
adam@375 420 Hint Rewrite confounder.
adamc@240 421
adamc@240 422 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
adam@368 423 (* begin thide *)
adamc@240 424 induction e; crush;
adamc@240 425 match goal with
adam@413 426 | [ |- context[match ?E with Const _ => _ | _ => _ end] ] =>
adamc@240 427 destruct E; crush
adamc@240 428 end.
adamc@240 429
adamc@240 430 (** One subgoal remains:
adamc@240 431
adamc@240 432 [[
adamc@240 433 ============================
adamc@240 434 eval e1 * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2
adamc@240 435 ]]
adamc@240 436
adam@367 437 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 438
adamc@240 439 Restart.
adamc@240 440
adamc@240 441 Ltac t := crush; match goal with
adam@413 442 | [ |- context[match ?E with Const _ => _ | _ => _ end] ] =>
adamc@240 443 destruct E; crush
adamc@240 444 end.
adamc@240 445
adamc@240 446 induction e.
adamc@240 447
adam@509 448 (** Since we see the subgoals before any simplification occurs, it is clear that we are looking at the case for constants. Our [t] makes short work of it. *)
adamc@240 449
adamc@240 450 t.
adamc@240 451
adamc@240 452 (** The next subgoal, for addition, is also discharged without trouble. *)
adamc@240 453
adamc@240 454 t.
adamc@240 455
adamc@240 456 (** The final subgoal is for multiplication, and it is here that we get stuck in the proof state summarized above. *)
adamc@240 457
adamc@240 458 t.
adamc@240 459
adam@433 460 (** What is [t] doing to get us to this point? The %\index{tactics!info}%[info] command can help us answer this kind of question. (As of this writing, [info] is no longer functioning in the most recent Coq release, but I hope it returns.) *)
adamc@240 461
adamc@240 462 Undo.
adam@574 463 (*info*) t.
adam@574 464 (* Too bad: recent Coq versions removed [info]. *)
adam@413 465
adam@433 466 (* begin hide *)
adam@437 467 (* begin thide *)
adam@433 468 Definition eir := eq_ind_r.
adam@437 469 (* end thide *)
adam@433 470 (* end hide *)
adam@433 471
adam@367 472 (** %\vspace{-.15in}%[[
adam@375 473 == simpl in *; intuition; subst; autorewrite with core in *;
adam@375 474 simpl in *; intuition; subst; autorewrite with core in *;
adamc@240 475 simpl in *; intuition; subst; destruct (reassoc e2).
adamc@240 476 simpl in *; intuition.
adamc@240 477
adamc@240 478 simpl in *; intuition.
adamc@240 479
adam@375 480 simpl in *; intuition; subst; autorewrite with core in *;
adamc@240 481 refine (eq_ind_r
adamc@240 482 (fun n : nat =>
adamc@240 483 n * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2) _ IHe1);
adam@375 484 autorewrite with core in *; simpl in *; intuition;
adam@375 485 subst; autorewrite with core in *; simpl in *;
adamc@240 486 intuition; subst.
adamc@240 487
adamc@240 488 ]]
adamc@240 489
adamc@240 490 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 491
adamc@240 492 Undo.
adamc@240 493
adamc@240 494 (** We arbitrarily split the script into chunks. The first few seem not to do any harm. *)
adamc@240 495
adam@375 496 simpl in *; intuition; subst; autorewrite with core in *.
adam@375 497 simpl in *; intuition; subst; autorewrite with core in *.
adamc@240 498 simpl in *; intuition; subst; destruct (reassoc e2).
adamc@240 499 simpl in *; intuition.
adamc@240 500 simpl in *; intuition.
adamc@240 501
adamc@240 502 (** The next step is revealed as the culprit, bringing us to the final unproved subgoal. *)
adamc@240 503
adam@375 504 simpl in *; intuition; subst; autorewrite with core in *.
adamc@240 505
adamc@240 506 (** We can split the steps further to assign blame. *)
adamc@240 507
adamc@240 508 Undo.
adamc@240 509
adamc@240 510 simpl in *.
adamc@240 511 intuition.
adamc@240 512 subst.
adam@375 513 autorewrite with core in *.
adamc@240 514
adamc@240 515 (** 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 516
adamc@240 517 Undo.
adamc@240 518
adam@574 519 (*info*) autorewrite with core in *.
adam@367 520 (** %\vspace{-.15in}%[[
adamc@240 521 == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
adamc@240 522 (confounder (reassoc e1) e3 e4)).
adamc@240 523 ]]
adamc@240 524
adamc@240 525 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 526
adamc@240 527 Abort.
adam@368 528 (* end thide *)
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@433 550 (** <<
adamc@241 551 Finished transaction in 0. secs (0.068004u,0.s)
adam@433 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@433 563 (** <<
adamc@241 564 Finished transaction in 2. secs (1.264079u,0.s)
adam@433 565 >>
adam@445 566 %\vspace{-.15in}%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 567
adam@368 568 (* begin thide *)
adamc@241 569 Restart.
adam@574 570 (*info*) eauto 6.
adam@367 571 (** %\vspace{-.15in}%[[
adamc@241 572 == intro x; intro y; intro H; intro H0; intro H4;
adamc@241 573 simple eapply trans_eq.
adam@426 574 simple apply eq_refl.
adamc@241 575
adamc@241 576 simple eapply trans_eq.
adam@426 577 simple apply eq_refl.
adamc@241 578
adamc@241 579 simple eapply trans_eq.
adam@426 580 simple apply eq_refl.
adamc@241 581
adamc@241 582 simple apply H1.
adamc@241 583 eexact H.
adamc@241 584
adamc@241 585 eexact H0.
adamc@241 586
adamc@241 587 simple apply H2; eexact H4.
adamc@241 588 ]]
adamc@241 589
adam@367 590 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 591
adamc@241 592 Restart.
adamc@241 593 debug eauto 6.
adamc@241 594
adam@433 595 (* begin hide *)
adam@437 596 (* begin thide *)
adam@433 597 Definition deeeebug := (@eq_refl, @sym_eq).
adam@437 598 (* end thide *)
adam@433 599 (* end hide *)
adam@433 600
adamc@241 601 (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening:
adamc@241 602 [[
adamc@241 603 1 depth=6
adamc@241 604 1.1 depth=6 intro
adamc@241 605 1.1.1 depth=6 intro
adamc@241 606 1.1.1.1 depth=6 intro
adamc@241 607 1.1.1.1.1 depth=6 intro
adamc@241 608 1.1.1.1.1.1 depth=6 intro
adamc@241 609 1.1.1.1.1.1.1 depth=5 apply H3
adamc@241 610 1.1.1.1.1.1.1.1 depth=4 eapply trans_eq
adam@426 611 1.1.1.1.1.1.1.1.1 depth=4 apply eq_refl
adamc@241 612 1.1.1.1.1.1.1.1.1.1 depth=3 eapply trans_eq
adam@426 613 1.1.1.1.1.1.1.1.1.1.1 depth=3 apply eq_refl
adamc@241 614 1.1.1.1.1.1.1.1.1.1.1.1 depth=2 eapply trans_eq
adam@426 615 1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply eq_refl
adamc@241 616 1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 eapply trans_eq
adam@426 617 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply eq_refl
adamc@241 618 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=0 eapply trans_eq
adamc@241 619 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=1 apply sym_eq ; trivial
adamc@241 620 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=0 eapply trans_eq
adamc@241 621 1.1.1.1.1.1.1.1.1.1.1.1.1.1.3 depth=0 eapply trans_eq
adamc@241 622 1.1.1.1.1.1.1.1.1.1.1.1.2 depth=2 apply sym_eq ; trivial
adamc@241 623 1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=1 eapply trans_eq
adam@426 624 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply eq_refl
adamc@241 625 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 depth=0 eapply trans_eq
adamc@241 626 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2 depth=1 apply sym_eq ; trivial
adamc@241 627 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2.1 depth=0 eapply trans_eq
adamc@241 628 1.1.1.1.1.1.1.1.1.1.1.1.2.1.3 depth=0 eapply trans_eq
adamc@241 629 ]]
adamc@241 630
adam@367 631 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 632
adamc@239 633 Qed.
adam@368 634 (* end thide *)
adamc@239 635 End slow.
adamc@239 636
adam@387 637 (** As aggravating as the above situation may be, there is greater aggravation to be had from importing library modules with commands like %\index{Vernacular commands!Require Import}%[Require Import]. Such a command imports not just the Gallina terms from a module, but also all the hints for [auto], [eauto], and [autorewrite]. Some very recent versions of Coq include mechanisms for removing hints from databases, but the proper solution is to be very conservative in exporting hints from modules. Consider putting hints in named databases, so that they may be used only when called upon explicitly, as demonstrated in Chapter 13.
adam@387 638
adam@413 639 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}% _thunks_ (suspended computations, represented with closures), such that a tactic's proof-producing thunk is only executed when we run %\index{Vernacular commands!Qed}%[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 640
adam@433 641 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 in their initial states. Still, many large automated proofs can realize vast memory savings via [abstract]. *)
adamc@241 642
adamc@238 643
adamc@235 644 (** * Modules *)
adamc@235 645
adam@462 646 (** 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 _module system_ 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 OCaml, and the discussion that follows assumes familiarity with the basics of one of those systems.
adamc@242 647
adam@413 648 ML modules facilitate the grouping of %\index{abstract type}%abstract types with operations over those types. Moreover, there is support for%\index{functor}% _functors_, 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 649
adam@462 650 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, the following 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 [id] for [f], and an operation [i] that is a left inverse for [f].%\index{Vernacular commands!Module Type}% *)
adamc@242 651
adamc@235 652 Module Type GROUP.
adamc@235 653 Parameter G : Set.
adamc@235 654 Parameter f : G -> G -> G.
adam@462 655 Parameter id : G.
adamc@235 656 Parameter i : G -> G.
adamc@235 657
adamc@235 658 Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
adam@462 659 Axiom ident : forall a, f id a = a.
adam@462 660 Axiom inverse : forall a, f (i a) a = id.
adamc@235 661 End GROUP.
adamc@235 662
adam@367 663 (** Many useful theorems hold of arbitrary groups. We capture some such theorem statements in another module signature.%\index{Vernacular commands!Declare Module}% *)
adamc@242 664
adamc@235 665 Module Type GROUP_THEOREMS.
adamc@235 666 Declare Module M : GROUP.
adamc@235 667
adam@462 668 Axiom ident' : forall a, M.f a M.id = a.
adamc@235 669
adam@462 670 Axiom inverse' : forall a, M.f a (M.i a) = M.id.
adamc@235 671
adam@462 672 Axiom unique_ident : forall id', (forall a, M.f id' a = a) -> id' = M.id.
adamc@235 673 End GROUP_THEOREMS.
adamc@235 674
adam@387 675 (** We implement generic proofs of these theorems with a functor, whose input is an arbitrary group [M]. %\index{Vernacular commands!Module}% *)
adamc@242 676
adam@387 677 Module GroupProofs (M : GROUP) : GROUP_THEOREMS with Module M := M.
adam@509 678
adam@413 679 (** As in ML, Coq provides multiple options for ascribing signatures to modules. Here we use just the colon operator, which implements%\index{opaque ascription}% _opaque ascription_, hiding all details of the module not exposed by the signature. Another option is%\index{transparent ascription}% _transparent ascription_ via the [<:] operator, which checks for signature compatibility without hiding implementation details. Here we stick with opaque ascription but employ the [with] operation to add more detail to a signature, exposing just those implementation details that we need to. For instance, here we expose the underlying group representation set and operator definitions. Without such a refinement, we would get an output module proving theorems about some unknown group, which is not very useful. Also note that opaque ascription can in Coq have some undesirable consequences without analogues in ML, since not just the types but also the _definitions_ of identifiers have significance in type checking and theorem proving. *)
adam@387 680
adamc@235 681 Module M := M.
adam@387 682 (** To ensure that the module we are building meets the [GROUP_THEOREMS] signature, we add an extra local name for [M], the functor argument. *)
adamc@235 683
adamc@235 684 Import M.
adam@387 685 (** It would be inconvenient to repeat the prefix [M.] everywhere in our theorem statements and proofs, so we bring all the identifiers of [M] into the local scope unqualified.
adam@387 686
adam@387 687 Now we are ready to prove the three theorems. The proofs are completely manual, which may seem ironic given the content of the previous sections! This illustrates another lesson, which is that short proof scripts that change infrequently may be worth leaving unautomated. It would take some effort to build suitable generic automation for these theorems about groups, so I stick with manual proof scripts to avoid distracting us from the main message of the section. We take the proofs from the Wikipedia page on elementary group theory. *)
adamc@235 688
adam@462 689 Theorem inverse' : forall a, f a (i a) = id.
adamc@235 690 intro.
adamc@235 691 rewrite <- (ident (f a (i a))).
adamc@235 692 rewrite <- (inverse (f a (i a))) at 1.
adamc@235 693 rewrite assoc.
adamc@235 694 rewrite assoc.
adamc@235 695 rewrite <- (assoc (i a) a (i a)).
adamc@235 696 rewrite inverse.
adamc@235 697 rewrite ident.
adamc@235 698 apply inverse.
adamc@235 699 Qed.
adamc@235 700
adam@462 701 Theorem ident' : forall a, f a id = a.
adamc@235 702 intro.
adamc@235 703 rewrite <- (inverse a).
adamc@235 704 rewrite <- assoc.
adamc@235 705 rewrite inverse'.
adamc@235 706 apply ident.
adamc@235 707 Qed.
adamc@235 708
adam@462 709 Theorem unique_ident : forall id', (forall a, M.f id' a = a) -> id' = M.id.
adamc@235 710 intros.
adam@462 711 rewrite <- (H id).
adamc@235 712 symmetry.
adamc@235 713 apply ident'.
adamc@235 714 Qed.
adam@387 715 End GroupProofs.
adamc@239 716
adamc@242 717 (** We can show that the integers with [+] form a group. *)
adamc@242 718
adamc@239 719 Require Import ZArith.
adamc@239 720 Open Scope Z_scope.
adamc@239 721
adamc@239 722 Module Int.
adamc@239 723 Definition G := Z.
adamc@239 724 Definition f x y := x + y.
adam@462 725 Definition id := 0.
adamc@239 726 Definition i x := -x.
adamc@239 727
adamc@239 728 Theorem assoc : forall a b c, f (f a b) c = f a (f b c).
adamc@239 729 unfold f; crush.
adamc@239 730 Qed.
adam@462 731 Theorem ident : forall a, f id a = a.
adam@462 732 unfold f, id; crush.
adamc@239 733 Qed.
adam@462 734 Theorem inverse : forall a, f (i a) a = id.
adam@462 735 unfold f, i, id; crush.
adamc@239 736 Qed.
adamc@239 737 End Int.
adamc@239 738
adamc@242 739 (** Next, we can produce integer-specific versions of the generic group theorems. *)
adamc@242 740
adam@387 741 Module IntProofs := GroupProofs(Int).
adamc@239 742
adam@387 743 Check IntProofs.unique_ident.
adamc@242 744 (** %\vspace{-.15in}% [[
adam@387 745 IntProofs.unique_ident
adamc@242 746 : forall e' : Int.G, (forall a : Int.G, Int.f e' a = a) -> e' = Int.e
adam@302 747 ]]
adam@367 748
adam@367 749 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 750
adam@462 751 Theorem unique_ident : forall id', (forall a, id' + a = a) -> id' = 0.
adam@368 752 (* begin thide *)
adam@387 753 exact IntProofs.unique_ident.
adamc@239 754 Qed.
adam@368 755 (* end thide *)
adamc@242 756
adam@475 757 (** 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 cases. 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 definitions of normal functions, based on particular function parameters. *)
adamc@243 758
adamc@243 759
adamc@243 760 (** * Build Processes *)
adamc@243 761
adam@433 762 (* begin hide *)
adam@437 763 (* begin thide *)
adam@433 764 Module Lib.
adam@433 765 Module A.
adam@433 766 End A.
adam@433 767 Module B.
adam@433 768 End B.
adam@433 769 Module C.
adam@433 770 End C.
adam@433 771 End Lib.
adam@433 772 Module Client.
adam@433 773 Module D.
adam@433 774 End D.
adam@433 775 Module E.
adam@433 776 End E.
adam@433 777 End Client.
adam@437 778 (* end thide *)
adam@433 779 (* end hide *)
adam@433 780
adamc@243 781 (** 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 782
adam@435 783 Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}%<<coq_makefile>> to do the hard work.
adamc@243 784
adamc@243 785 <<
adamc@243 786 MODULES := A B C
adamc@243 787 VS := $(MODULES:%=%.v)
adamc@243 788
adamc@243 789 .PHONY: coq clean
adamc@243 790
adamc@243 791 coq: Makefile.coq
adam@369 792 $(MAKE) -f Makefile.coq
adamc@243 793
adamc@243 794 Makefile.coq: Makefile $(VS)
adamc@243 795 coq_makefile -R . Lib $(VS) -o Makefile.coq
adamc@243 796
adamc@243 797 clean:: Makefile.coq
adam@369 798 $(MAKE) -f Makefile.coq clean
adamc@243 799 rm -f Makefile.coq
adamc@243 800 >>
adamc@243 801
adam@435 802 The Makefile begins by defining a variable <<VS>> holding the list of filenames to be included in the project. The primary target is <<coq>>, which depends on the construction of an auxiliary Makefile called <<Makefile.coq>>. Another rule explains how to build that file. We call <<coq_makefile>>, using the <<-R>> 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 <<X.v>> is compiled into <<X.vo>>.
adamc@243 803
adam@433 804 Now code in <<B.v>> may refer to definitions in <<A.v>> after running
adamc@243 805 [[
adamc@243 806 Require Import Lib.A.
adam@367 807 ]]
adam@433 808 %\vspace{-.15in}%Library [Lib] is presented as a module, containing a submodule [A], which contains the definitions from <<A.v>>. These are genuine modules in the sense of Coq's module system, and they may be passed to functors and so on.
adamc@243 809
adam@433 810 The command [Require Import] is a convenient combination of two more primitive commands. The %\index{Vernacular commands!Require}%[Require] command finds the <<.vo>> 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 <<.vo>> 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 811
adam@433 812 Now we would like to use our library from a different development, called [Client] and found in directory <<CLIENT>>, which has its own Makefile.
adamc@243 813
adamc@243 814 <<
adamc@243 815 MODULES := D E
adamc@243 816 VS := $(MODULES:%=%.v)
adamc@243 817
adamc@243 818 .PHONY: coq clean
adamc@243 819
adamc@243 820 coq: Makefile.coq
adam@369 821 $(MAKE) -f Makefile.coq
adamc@243 822
adamc@243 823 Makefile.coq: Makefile $(VS)
adamc@243 824 coq_makefile -R LIB Lib -R . Client $(VS) -o Makefile.coq
adamc@243 825
adamc@243 826 clean:: Makefile.coq
adam@369 827 $(MAKE) -f Makefile.coq clean
adamc@243 828 rm -f Makefile.coq
adamc@243 829 >>
adamc@243 830
adam@435 831 We change the <<coq_makefile>> call to indicate where the library [Lib] is found. Now <<D.v>> and <<E.v>> can refer to definitions from [Lib] module [A] after running
adamc@243 832 [[
adamc@243 833 Require Import Lib.A.
adamc@243 834 ]]
adam@433 835 %\vspace{-.15in}\noindent{}%and <<E.v>> can refer to definitions from <<D.v>> by running
adamc@243 836 [[
adamc@243 837 Require Import Client.D.
adamc@243 838 ]]
adam@433 839 %\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 <<Lib.v>> to [Lib]'s directory and Makefile, where that file contains just this line:%\index{Vernacular commands!Require Export}%
adamc@243 840 [[
adamc@243 841 Require Export Lib.A Lib.B Lib.C.
adamc@243 842 ]]
adam@367 843 %\vspace{-.15in}%Now client code can import all definitions from all of [Lib]'s modules simply by running
adamc@243 844 [[
adamc@243 845 Require Import Lib.
adamc@243 846 ]]
adam@367 847 %\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 848
adamc@243 849 %\medskip%
adamc@243 850
adam@433 851 The remaining ingredient is the proper way of editing library code files in Proof General. Recall this snippet of <<.emacs>> code from Chapter 2, which tells Proof General where to find the library associated with this book.
adamc@243 852
adamc@243 853 <<
adamc@243 854 (custom-set-variables
adamc@243 855 ...
adam@535 856 '(coq-prog-args '("-R" "/path/to/cpdt/src" "Cpdt"))
adamc@243 857 ...
adamc@243 858 )
adamc@243 859 >>
adamc@243 860
adamc@243 861 To do interactive editing of our current example, we just need to change the flags to point to the right places.
adamc@243 862
adamc@243 863 <<
adamc@243 864 (custom-set-variables
adamc@243 865 ...
adam@535 866 ; '(coq-prog-args '("-R" "/path/to/cpdt/src" "Cpdt"))
adamc@243 867 '(coq-prog-args '("-R" "LIB" "Lib" "-R" "CLIENT" "Client"))
adamc@243 868 ...
adamc@243 869 )
adamc@243 870 >>
adamc@243 871
adam@433 872 When working on multiple projects, it is useful to leave multiple versions of this setting in your <<.emacs>> file, commenting out all but one of them at any moment in time. To switch between projects, change the commenting structure and restart Emacs.
adam@397 873
adam@433 874 Alternatively, we can revisit the directory-local settings approach and write the following into a file <<.dir-locals.el>> in <<CLIENT>>:
adam@397 875
adam@397 876 <<
adam@397 877 ((coq-mode . ((coq-prog-args .
adam@397 878 ("-emacs-U" "-R" "LIB" "Lib" "-R" "CLIENT" "Client")))))
adam@397 879 >>
adam@509 880
adam@509 881 A downside of this approach is that users of your code may not want to trust the arbitrary Emacs Lisp programs that you are allowed to place in such files, so that they prefer to add mappings manually.
adam@542 882
adam@542 883 Relatively recent versions of Coq support another, more principled approach to all this. A project's list of settings and source files may be saved in a single file named <<_CoqProject>>, which is processed uniformly by recent enough versions of <<coq_makefile>>, Proof General, and CoqIDE. For details, see the Coq manual.
adam@397 884 *)