Mercurial > cpdt > repo

annotate src/Large.v @ 236:c8f49f07cead

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
First part of 'Ltac Anti-Patterns'
author Adam Chlipala <adamc@hcoop.net>
date Fri, 04 Dec 2009 16:58:30 -0500
parents 52b9e43be069
children 91eed1e3e3a4
rev   line source
adamc@235 1 (* Copyright (c) 2009, Adam Chlipala
adamc@235 2 *
adamc@235 3 * This work is licensed under a
adamc@235 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@235 5 * Unported License.
adamc@235 6 * The license text is available at:
adamc@235 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@235 8 *)
adamc@235 9
adamc@235 10 (* begin hide *)
adamc@236 11 Require Import Arith.
adamc@236 12
adamc@235 13 Require Import Tactics.
adamc@235 14
adamc@235 15 Set Implicit Arguments.
adamc@235 16 (* end hide *)
adamc@235 17
adamc@235 18
adamc@235 19 (** %\chapter{Proving in the Large}% *)
adamc@235 20
adamc@236 21 (** It is somewhat unfortunate that the term "theorem-proving" looks so much like the word "theory." Most researchers and practitioners in software assume that mechanized theorem-proving is profoundly impractical. Indeed, until recently, most advances in theorem-proving for higher-order logics have been largely theoretical. However, starting around the beginning of the 21st century, there was a surge in the use of proof assistants in serious verification efforts. That line of work is still quite new, but I believe it is not too soon to distill some lessons on how to work effectively with large formal proofs.
adamc@236 22
adamc@236 23 Thus, this chapter gives some tips for structuring and maintaining large Coq developments. *)
adamc@236 24
adamc@236 25
adamc@236 26 (** * Ltac Anti-Patterns *)
adamc@236 27
adamc@236 28 (** In this book, I have been following an unusual style, where proofs are not considered finished until they are "fully automated," in a certain sense. 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@236 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 found in a proof domain, the more important it is to work to prove theorems with single tactics. From an automation standpoint, single-tactic proofs can be extremely effective, and automation becomes more and more critical as proofs are populated by more uninteresting detail. In this section, I will give some examples of the consequences of more common proof styles.
adamc@236 31
adamc@236 32 As a running example, consider a basic language of arithmetic expressions, an interpreter for it, and a transformation that scales up every constant in an expression. *)
adamc@236 33
adamc@236 34 Inductive exp : Set :=
adamc@236 35 | Const : nat -> exp
adamc@236 36 | Plus : exp -> exp -> exp.
adamc@236 37
adamc@236 38 Fixpoint eval (e : exp) : nat :=
adamc@236 39 match e with
adamc@236 40 | Const n => n
adamc@236 41 | Plus e1 e2 => eval e1 + eval e2
adamc@236 42 end.
adamc@236 43
adamc@236 44 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 45 match e with
adamc@236 46 | Const n => Const (k * n)
adamc@236 47 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 48 end.
adamc@236 49
adamc@236 50 (** We can write a very manual proof that [double] really doubles an expression's value. *)
adamc@236 51
adamc@236 52 Theorem eval_times : forall k e,
adamc@236 53 eval (times k e) = k * eval e.
adamc@236 54 induction e.
adamc@236 55
adamc@236 56 trivial.
adamc@236 57
adamc@236 58 simpl.
adamc@236 59 rewrite IHe1.
adamc@236 60 rewrite IHe2.
adamc@236 61 rewrite mult_plus_distr_l.
adamc@236 62 trivial.
adamc@236 63 Qed.
adamc@236 64
adamc@236 65 (** We use spaces to separate the two inductive cases. The second case mentions automatically-generated hypothesis names explicitly. As a result, innocuous changes to the theorem statement can invalidate the proof. *)
adamc@236 66
adamc@236 67 Reset eval_times.
adamc@236 68
adamc@236 69 Theorem eval_double : forall k x,
adamc@236 70 eval (times k x) = k * eval x.
adamc@236 71 induction x.
adamc@236 72
adamc@236 73 trivial.
adamc@236 74
adamc@236 75 simpl.
adamc@236 76 (** [[
adamc@236 77 rewrite IHe1.
adamc@236 78
adamc@236 79 Error: The reference IHe1 was not found in the current environment.
adamc@236 80
adamc@236 81 ]]
adamc@236 82
adamc@236 83 The inductive hypotheses are named [IHx1] and [IHx2] now, not [IHe1] and [IHe2]. *)
adamc@236 84
adamc@236 85 Abort.
adamc@236 86
adamc@236 87 (** We might decide to use a more explicit invocation of [induction] to give explicit binders for all of the names that we will reference later in the proof. *)
adamc@236 88
adamc@236 89 Theorem eval_times : forall k e,
adamc@236 90 eval (times k e) = k * eval e.
adamc@236 91 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 92
adamc@236 93 trivial.
adamc@236 94
adamc@236 95 simpl.
adamc@236 96 rewrite IHe1.
adamc@236 97 rewrite IHe2.
adamc@236 98 rewrite mult_plus_distr_l.
adamc@236 99 trivial.
adamc@236 100 Qed.
adamc@236 101
adamc@236 102 (** We pass [induction] an %\textit{%#<i>#intro pattern#</i>#%}%, using a [|] character to separate out instructions for the different inductive cases. Within a case, we write [?] to ask Coq to generate a name automatically, and we write an explicit name to assign that name to the corresponding new variable. It is apparent that, to use intro patterns to avoid proof brittleness, one needs to keep track of the seemingly unimportant facts of the orders in which variables are introduced. Thus, the script keeps working if we replace [e] by [x], but it has become more cluttered. Arguably, neither proof is particularly easy to follow.
adamc@236 103
adamc@236 104 That category of complaint has to do with understanding proofs as static artifacts. As with programming in general, with serious projects, it tends to be much more important to be able to support evolution of proofs as theorems change. Unstructured proofs like the above examples can be very hard to update in concert with theorem statements. For instance, consider how the last proof script plays out when we modify [times] to introduce a bug. *)
adamc@236 105
adamc@236 106 Reset times.
adamc@236 107
adamc@236 108 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 109 match e with
adamc@236 110 | Const n => Const (1 + k * n)
adamc@236 111 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 112 end.
adamc@236 113
adamc@236 114 Theorem eval_times : forall k e,
adamc@236 115 eval (times k e) = k * eval e.
adamc@236 116 induction e as [ | ? IHe1 ? IHe2 ].
adamc@236 117
adamc@236 118 trivial.
adamc@236 119
adamc@236 120 simpl.
adamc@236 121 (** [[
adamc@236 122 rewrite IHe1.
adamc@236 123
adamc@236 124 Error: The reference IHe1 was not found in the current environment.
adamc@236 125
adamc@236 126 ]] *)
adamc@236 127
adamc@236 128 Abort.
adamc@236 129
adamc@236 130 (** Can you spot what went wrong, without stepping through the script step-by-step? The problem is that [trivial] never fails. Originally, [trivial] had been succeeding in proving an equality that follows by reflexivity. Our change to [times] leads to a case where that equality is no longer true. [trivial] happily leaves the false equality in place, and we continue on to the span of tactics intended for the second inductive case. Unfortunately, those tactics end up being applied to the %\textit{%#<i>#first#</i>#%}% case instead. This example is on a very small scale; similar consequences can be much more confusing in large developments. *)
adamc@236 131
adamc@236 132 Reset times.
adamc@236 133
adamc@236 134 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 135 match e with
adamc@236 136 | Const n => Const (k * n)
adamc@236 137 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 138 end.
adamc@236 139
adamc@236 140 (** 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 141
adamc@236 142 We can rewrite the current proof with a single tactic. *)
adamc@236 143
adamc@236 144 Theorem eval_times : forall k e,
adamc@236 145 eval (times k e) = k * eval e.
adamc@236 146 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 147 trivial
adamc@236 148 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adamc@236 149 Qed.
adamc@236 150
adamc@236 151 (** 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 152
adamc@236 153 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 154
adamc@236 155 Reset exp.
adamc@236 156
adamc@236 157 Inductive exp : Set :=
adamc@236 158 | Const : nat -> exp
adamc@236 159 | Plus : exp -> exp -> exp
adamc@236 160 | Mult : exp -> exp -> exp.
adamc@236 161
adamc@236 162 Fixpoint eval (e : exp) : nat :=
adamc@236 163 match e with
adamc@236 164 | Const n => n
adamc@236 165 | Plus e1 e2 => eval e1 + eval e2
adamc@236 166 | Mult e1 e2 => eval e1 * eval e2
adamc@236 167 end.
adamc@236 168
adamc@236 169 Fixpoint times (k : nat) (e : exp) : exp :=
adamc@236 170 match e with
adamc@236 171 | Const n => Const (k * n)
adamc@236 172 | Plus e1 e2 => Plus (times k e1) (times k e2)
adamc@236 173 | Mult e1 e2 => Mult (times k e1) e2
adamc@236 174 end.
adamc@236 175
adamc@236 176 Theorem eval_times : forall k e,
adamc@236 177 eval (times k e) = k * eval e.
adamc@236 178 (** [[
adamc@236 179 induction e as [ | ? IHe1 ? IHe2 ]; [
adamc@236 180 trivial
adamc@236 181 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
adamc@236 182
adamc@236 183 Error: Expects a disjunctive pattern with 3 branches.
adamc@236 184
adamc@236 185 ]] *)
adamc@236 186
adamc@236 187 Abort.
adamc@236 188
adamc@236 189 (** 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 190
adamc@236 191 Theorem eval_times : forall k e,
adamc@236 192 eval (times k e) = k * eval e.
adamc@236 193 induction e as [ | ? IHe1 ? IHe2 | ? IHe1 ? IHe2 ]; [
adamc@236 194 trivial
adamc@236 195 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial
adamc@236 196 | simpl; rewrite IHe1; rewrite mult_assoc; trivial ].
adamc@236 197 Qed.
adamc@236 198
adamc@236 199 (** 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 200
adamc@236 201 Reset eval_times.
adamc@236 202
adamc@236 203 Theorem eval_times : forall k e,
adamc@236 204 eval (times k e) = k * eval e.
adamc@236 205 Hint Rewrite mult_plus_distr_l mult_assoc : cpdt.
adamc@236 206
adamc@236 207 induction e; crush.
adamc@236 208 Qed.
adamc@236 209
adamc@235 210
adamc@235 211 (** * Modules *)
adamc@235 212
adamc@235 213 Module Type GROUP.
adamc@235 214 Parameter G : Set.
adamc@235 215 Parameter f : G -> G -> G.
adamc@235 216 Parameter e : G.
adamc@235 217 Parameter i : G -> G.
adamc@235 218
adamc@235 219 Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
adamc@235 220 Axiom ident : forall a, f e a = a.
adamc@235 221 Axiom inverse : forall a, f (i a) a = e.
adamc@235 222 End GROUP.
adamc@235 223
adamc@235 224 Module Type GROUP_THEOREMS.
adamc@235 225 Declare Module M : GROUP.
adamc@235 226
adamc@235 227 Axiom ident' : forall a, M.f a M.e = a.
adamc@235 228
adamc@235 229 Axiom inverse' : forall a, M.f a (M.i a) = M.e.
adamc@235 230
adamc@235 231 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 232 End GROUP_THEOREMS.
adamc@235 233
adamc@235 234 Module Group (M : GROUP) : GROUP_THEOREMS.
adamc@235 235 Module M := M.
adamc@235 236
adamc@235 237 Import M.
adamc@235 238
adamc@235 239 Theorem inverse' : forall a, f a (i a) = e.
adamc@235 240 intro.
adamc@235 241 rewrite <- (ident (f a (i a))).
adamc@235 242 rewrite <- (inverse (f a (i a))) at 1.
adamc@235 243 rewrite assoc.
adamc@235 244 rewrite assoc.
adamc@235 245 rewrite <- (assoc (i a) a (i a)).
adamc@235 246 rewrite inverse.
adamc@235 247 rewrite ident.
adamc@235 248 apply inverse.
adamc@235 249 Qed.
adamc@235 250
adamc@235 251 Theorem ident' : forall a, f a e = a.
adamc@235 252 intro.
adamc@235 253 rewrite <- (inverse a).
adamc@235 254 rewrite <- assoc.
adamc@235 255 rewrite inverse'.
adamc@235 256 apply ident.
adamc@235 257 Qed.
adamc@235 258
adamc@235 259 Theorem unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 260 intros.
adamc@235 261 rewrite <- (H e).
adamc@235 262 symmetry.
adamc@235 263 apply ident'.
adamc@235 264 Qed.
adamc@235 265 End Group.