Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
235:52b9e43be069 236:c8f49f07cead
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith.
12
11 Require Import Tactics. 13 Require Import Tactics.
12 14
13 Set Implicit Arguments. 15 Set Implicit Arguments.
14 (* end hide *) 16 (* end hide *)
15 17
16 18
17 (** %\chapter{Proving in the Large}% *) 19 (** %\chapter{Proving in the Large}% *)
20
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.
22
23 Thus, this chapter gives some tips for structuring and maintaining large Coq developments. *)
24
25
26 (** * Ltac Anti-Patterns *)
27
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?
29
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.
31
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. *)
33
34 Inductive exp : Set :=
35 | Const : nat -> exp
36 | Plus : exp -> exp -> exp.
37
38 Fixpoint eval (e : exp) : nat :=
39 match e with
40 | Const n => n
41 | Plus e1 e2 => eval e1 + eval e2
42 end.
43
44 Fixpoint times (k : nat) (e : exp) : exp :=
45 match e with
46 | Const n => Const (k * n)
47 | Plus e1 e2 => Plus (times k e1) (times k e2)
48 end.
49
50 (** We can write a very manual proof that [double] really doubles an expression's value. *)
51
52 Theorem eval_times : forall k e,
53 eval (times k e) = k * eval e.
54 induction e.
55
56 trivial.
57
58 simpl.
59 rewrite IHe1.
60 rewrite IHe2.
61 rewrite mult_plus_distr_l.
62 trivial.
63 Qed.
64
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. *)
66
67 Reset eval_times.
68
69 Theorem eval_double : forall k x,
70 eval (times k x) = k * eval x.
71 induction x.
72
73 trivial.
74
75 simpl.
76 (** [[
77 rewrite IHe1.
78
79 Error: The reference IHe1 was not found in the current environment.
80
81 ]]
82
83 The inductive hypotheses are named [IHx1] and [IHx2] now, not [IHe1] and [IHe2]. *)
84
85 Abort.
86
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. *)
88
89 Theorem eval_times : forall k e,
90 eval (times k e) = k * eval e.
91 induction e as [ | ? IHe1 ? IHe2 ].
92
93 trivial.
94
95 simpl.
96 rewrite IHe1.
97 rewrite IHe2.
98 rewrite mult_plus_distr_l.
99 trivial.
100 Qed.
101
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.
103
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. *)
105
106 Reset times.
107
108 Fixpoint times (k : nat) (e : exp) : exp :=
109 match e with
110 | Const n => Const (1 + k * n)
111 | Plus e1 e2 => Plus (times k e1) (times k e2)
112 end.
113
114 Theorem eval_times : forall k e,
115 eval (times k e) = k * eval e.
116 induction e as [ | ? IHe1 ? IHe2 ].
117
118 trivial.
119
120 simpl.
121 (** [[
122 rewrite IHe1.
123
124 Error: The reference IHe1 was not found in the current environment.
125
126 ]] *)
127
128 Abort.
129
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. *)
131
132 Reset times.
133
134 Fixpoint times (k : nat) (e : exp) : exp :=
135 match e with
136 | Const n => Const (k * n)
137 | Plus e1 e2 => Plus (times k e1) (times k e2)
138 end.
139
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.
141
142 We can rewrite the current proof with a single tactic. *)
143
144 Theorem eval_times : forall k e,
145 eval (times k e) = k * eval e.
146 induction e as [ | ? IHe1 ? IHe2 ]; [
147 trivial
148 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
149 Qed.
150
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.
152
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. *)
154
155 Reset exp.
156
157 Inductive exp : Set :=
158 | Const : nat -> exp
159 | Plus : exp -> exp -> exp
160 | Mult : exp -> exp -> exp.
161
162 Fixpoint eval (e : exp) : nat :=
163 match e with
164 | Const n => n
165 | Plus e1 e2 => eval e1 + eval e2
166 | Mult e1 e2 => eval e1 * eval e2
167 end.
168
169 Fixpoint times (k : nat) (e : exp) : exp :=
170 match e with
171 | Const n => Const (k * n)
172 | Plus e1 e2 => Plus (times k e1) (times k e2)
173 | Mult e1 e2 => Mult (times k e1) e2
174 end.
175
176 Theorem eval_times : forall k e,
177 eval (times k e) = k * eval e.
178 (** [[
179 induction e as [ | ? IHe1 ? IHe2 ]; [
180 trivial
181 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
182
183 Error: Expects a disjunctive pattern with 3 branches.
184
185 ]] *)
186
187 Abort.
188
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. *)
190
191 Theorem eval_times : forall k e,
192 eval (times k e) = k * eval e.
193 induction e as [ | ? IHe1 ? IHe2 | ? IHe1 ? IHe2 ]; [
194 trivial
195 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial
196 | simpl; rewrite IHe1; rewrite mult_assoc; trivial ].
197 Qed.
198
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. *)
200
201 Reset eval_times.
202
203 Theorem eval_times : forall k e,
204 eval (times k e) = k * eval e.
205 Hint Rewrite mult_plus_distr_l mult_assoc : cpdt.
206
207 induction e; crush.
208 Qed.
18 209
19 210
20 (** * Modules *) 211 (** * Modules *)
21 212
22 Module Type GROUP. 213 Module Type GROUP.