adam@398
|
1 (* Copyright (c) 2008-2012, Adam Chlipala
|
adamc@118
|
2 *
|
adamc@118
|
3 * This work is licensed under a
|
adamc@118
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@118
|
5 * Unported License.
|
adamc@118
|
6 * The license text is available at:
|
adamc@118
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@118
|
8 *)
|
adamc@118
|
9
|
adamc@118
|
10 (* begin hide *)
|
adamc@120
|
11 Require Import Eqdep JMeq List.
|
adamc@118
|
12
|
adam@314
|
13 Require Import CpdtTactics.
|
adamc@118
|
14
|
adamc@118
|
15 Set Implicit Arguments.
|
adamc@118
|
16 (* end hide *)
|
adamc@118
|
17
|
adamc@118
|
18
|
adamc@118
|
19 (** %\chapter{Reasoning About Equality Proofs}% *)
|
adamc@118
|
20
|
adam@294
|
21 (** In traditional mathematics, the concept of equality is usually taken as a given. On the other hand, in type theory, equality is a very contentious subject. There are at least three different notions of equality that are important, and researchers are actively investigating new definitions of what it means for two terms to be equal. Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly. In this chapter, I will focus on design patterns for circumventing these tricky issues, and I will introduce the different notions of equality as they are germane. *)
|
adamc@118
|
22
|
adamc@118
|
23
|
adamc@122
|
24 (** * The Definitional Equality *)
|
adamc@122
|
25
|
adam@435
|
26 (** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's%\index{definitional equality}% _definitional equality_. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion [E : T] from the premise [E : T'] and a proof that [T] and [T'] are definitionally equal.
|
adamc@122
|
27
|
adam@364
|
28 The %\index{tactics!cbv}%[cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *)
|
adamc@122
|
29
|
adamc@122
|
30 Definition pred' (x : nat) :=
|
adamc@122
|
31 match x with
|
adamc@122
|
32 | O => O
|
adamc@122
|
33 | S n' => let y := n' in y
|
adamc@122
|
34 end.
|
adamc@122
|
35
|
adamc@122
|
36 Theorem reduce_me : pred' 1 = 0.
|
adamc@218
|
37
|
adamc@124
|
38 (* begin thide *)
|
adam@364
|
39 (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters. Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation%~\cite{DeBruijn}% that encodes terms canonically.
|
adamc@122
|
40
|
adam@364
|
41 The %\index{delta reduction}%delta rule is for unfolding global definitions. We can use it here to unfold the definition of [pred']. We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules. There is an analogous tactic %\index{tactics!lazy}%[lazy] for call-by-need reduction. *)
|
adamc@122
|
42
|
adamc@122
|
43 cbv delta.
|
adam@364
|
44 (** %\vspace{-.15in}%[[
|
adamc@122
|
45 ============================
|
adamc@122
|
46 (fun x : nat => match x with
|
adamc@122
|
47 | 0 => 0
|
adamc@122
|
48 | S n' => let y := n' in y
|
adamc@122
|
49 end) 1 = 0
|
adamc@122
|
50 ]]
|
adamc@122
|
51
|
adam@364
|
52 At this point, we want to apply the famous %\index{beta reduction}%beta reduction of lambda calculus, to simplify the application of a known function abstraction. *)
|
adamc@122
|
53
|
adamc@122
|
54 cbv beta.
|
adam@364
|
55 (** %\vspace{-.15in}%[[
|
adamc@122
|
56 ============================
|
adamc@122
|
57 match 1 with
|
adamc@122
|
58 | 0 => 0
|
adamc@122
|
59 | S n' => let y := n' in y
|
adamc@122
|
60 end = 0
|
adamc@122
|
61 ]]
|
adamc@122
|
62
|
adam@364
|
63 Next on the list is the %\index{iota reduction}%iota reduction, which simplifies a single [match] term by determining which pattern matches. *)
|
adamc@122
|
64
|
adamc@122
|
65 cbv iota.
|
adam@364
|
66 (** %\vspace{-.15in}%[[
|
adamc@122
|
67 ============================
|
adamc@122
|
68 (fun n' : nat => let y := n' in y) 0 = 0
|
adamc@122
|
69 ]]
|
adamc@122
|
70
|
adamc@122
|
71 Now we need another beta reduction. *)
|
adamc@122
|
72
|
adamc@122
|
73 cbv beta.
|
adam@364
|
74 (** %\vspace{-.15in}%[[
|
adamc@122
|
75 ============================
|
adamc@122
|
76 (let y := 0 in y) = 0
|
adamc@122
|
77 ]]
|
adamc@122
|
78
|
adam@364
|
79 The final reduction rule is %\index{zeta reduction}%zeta, which replaces a [let] expression by its body with the appropriate term substituted. *)
|
adamc@122
|
80
|
adamc@122
|
81 cbv zeta.
|
adam@364
|
82 (** %\vspace{-.15in}%[[
|
adamc@122
|
83 ============================
|
adamc@122
|
84 0 = 0
|
adam@302
|
85 ]]
|
adam@302
|
86 *)
|
adamc@122
|
87
|
adamc@122
|
88 reflexivity.
|
adamc@122
|
89 Qed.
|
adamc@124
|
90 (* end thide *)
|
adamc@122
|
91
|
adam@365
|
92 (** The [beta] reduction rule applies to recursive functions as well, and its behavior may be surprising in some instances. For instance, we can run some simple tests using the reduction strategy [compute], which applies all applicable rules of the definitional equality. *)
|
adam@365
|
93
|
adam@365
|
94 Definition id (n : nat) := n.
|
adam@365
|
95
|
adam@365
|
96 Eval compute in fun x => id x.
|
adam@365
|
97 (** %\vspace{-.15in}%[[
|
adam@365
|
98 = fun x : nat => x
|
adam@365
|
99 ]]
|
adam@365
|
100 *)
|
adam@365
|
101
|
adam@365
|
102 Fixpoint id' (n : nat) := n.
|
adam@365
|
103
|
adam@365
|
104 Eval compute in fun x => id' x.
|
adam@365
|
105 (** %\vspace{-.15in}%[[
|
adam@365
|
106 = fun x : nat => (fix id' (n : nat) : nat := n) x
|
adam@365
|
107 ]]
|
adam@365
|
108
|
adam@427
|
109 By running [compute], we ask Coq to run reduction steps until no more apply, so why do we see an application of a known function, where clearly no beta reduction has been performed? The answer has to do with ensuring termination of all Gallina programs. One candidate rule would say that we apply recursive definitions wherever possible. However, this would clearly lead to nonterminating reduction sequences, since the function may appear fully applied within its own definition, and we would naively "simplify" such applications immediately. Instead, Coq only applies the beta rule for a recursive function when _the top-level structure of the recursive argument is known_. For [id'] above, we have only one argument [n], so clearly it is the recursive argument, and the top-level structure of [n] is known when the function is applied to [O] or to some [S e] term. The variable [x] is neither, so reduction is blocked.
|
adam@365
|
110
|
adam@365
|
111 What are recursive arguments in general? Every recursive function is compiled by Coq to a %\index{Gallina terms!fix}%[fix] expression, for anonymous definition of recursive functions. Further, every [fix] with multiple arguments has one designated as the recursive argument via a [struct] annotation. The recursive argument is the one that must decrease across recursive calls, to appease Coq's termination checker. Coq will generally infer which argument is recursive, though we may also specify it manually, if we want to tweak reduction behavior. For instance, consider this definition of a function to add two lists of [nat]s elementwise: *)
|
adam@365
|
112
|
adam@365
|
113 Fixpoint addLists (ls1 ls2 : list nat) : list nat :=
|
adam@365
|
114 match ls1, ls2 with
|
adam@365
|
115 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists ls1' ls2'
|
adam@365
|
116 | _, _ => nil
|
adam@365
|
117 end.
|
adam@365
|
118
|
adam@365
|
119 (** By default, Coq chooses [ls1] as the recursive argument. We can see that [ls2] would have been another valid choice. The choice has a critical effect on reduction behavior, as these two examples illustrate: *)
|
adam@365
|
120
|
adam@365
|
121 Eval compute in fun ls => addLists nil ls.
|
adam@365
|
122 (** %\vspace{-.15in}%[[
|
adam@365
|
123 = fun _ : list nat => nil
|
adam@365
|
124 ]]
|
adam@365
|
125 *)
|
adam@365
|
126
|
adam@365
|
127 Eval compute in fun ls => addLists ls nil.
|
adam@365
|
128 (** %\vspace{-.15in}%[[
|
adam@365
|
129 = fun ls : list nat =>
|
adam@365
|
130 (fix addLists (ls1 ls2 : list nat) : list nat :=
|
adam@365
|
131 match ls1 with
|
adam@365
|
132 | nil => nil
|
adam@365
|
133 | n1 :: ls1' =>
|
adam@365
|
134 match ls2 with
|
adam@365
|
135 | nil => nil
|
adam@365
|
136 | n2 :: ls2' =>
|
adam@365
|
137 (fix plus (n m : nat) : nat :=
|
adam@365
|
138 match n with
|
adam@365
|
139 | 0 => m
|
adam@365
|
140 | S p => S (plus p m)
|
adam@365
|
141 end) n1 n2 :: addLists ls1' ls2'
|
adam@365
|
142 end
|
adam@365
|
143 end) ls nil
|
adam@365
|
144 ]]
|
adam@365
|
145
|
adam@427
|
146 The outer application of the [fix] expression for [addLists] was only simplified in the first case, because in the second case the recursive argument is [ls], whose top-level structure is not known.
|
adam@365
|
147
|
adam@427
|
148 The opposite behavior pertains to a version of [addLists] with [ls2] marked as recursive. *)
|
adam@365
|
149
|
adam@365
|
150 Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat :=
|
adam@365
|
151 match ls1, ls2 with
|
adam@365
|
152 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2'
|
adam@365
|
153 | _, _ => nil
|
adam@365
|
154 end.
|
adam@365
|
155
|
adam@427
|
156 (* begin hide *)
|
adam@427
|
157 Definition foo := @eq.
|
adam@427
|
158 (* end hide *)
|
adam@427
|
159
|
adam@365
|
160 Eval compute in fun ls => addLists' ls nil.
|
adam@365
|
161 (** %\vspace{-.15in}%[[
|
adam@365
|
162 = fun ls : list nat => match ls with
|
adam@365
|
163 | nil => nil
|
adam@365
|
164 | _ :: _ => nil
|
adam@365
|
165 end
|
adam@365
|
166 ]]
|
adam@365
|
167
|
adam@365
|
168 We see that all use of recursive functions has been eliminated, though the term has not quite simplified to [nil]. We could get it to do so by switching the order of the [match] discriminees in the definition of [addLists'].
|
adam@365
|
169
|
adam@365
|
170 Recall that co-recursive definitions have a dual rule: a co-recursive call only simplifies when it is the discriminee of a [match]. This condition is built into the beta rule for %\index{Gallina terms!cofix}%[cofix], the anonymous form of [CoFixpoint].
|
adam@365
|
171
|
adam@365
|
172 %\medskip%
|
adam@365
|
173
|
adam@407
|
174 The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a%\index{propositional equality}% _propositional equality_, because it reifies definitional equality as a proposition that may or may not hold. Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity. In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina. We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use.
|
adamc@122
|
175
|
adam@427
|
176 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality "as data." *)
|
adamc@122
|
177
|
adamc@122
|
178
|
adamc@118
|
179 (** * Heterogeneous Lists Revisited *)
|
adamc@118
|
180
|
adam@427
|
181 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *)
|
adamc@118
|
182
|
adamc@118
|
183 Section fhlist.
|
adamc@118
|
184 Variable A : Type.
|
adamc@118
|
185 Variable B : A -> Type.
|
adamc@118
|
186
|
adamc@118
|
187 Fixpoint fhlist (ls : list A) : Type :=
|
adamc@118
|
188 match ls with
|
adamc@118
|
189 | nil => unit
|
adamc@118
|
190 | x :: ls' => B x * fhlist ls'
|
adamc@118
|
191 end%type.
|
adamc@118
|
192
|
adamc@118
|
193 Variable elm : A.
|
adamc@118
|
194
|
adamc@118
|
195 Fixpoint fmember (ls : list A) : Type :=
|
adamc@118
|
196 match ls with
|
adamc@118
|
197 | nil => Empty_set
|
adamc@118
|
198 | x :: ls' => (x = elm) + fmember ls'
|
adamc@118
|
199 end%type.
|
adamc@118
|
200
|
adamc@118
|
201 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
|
adamc@118
|
202 match ls return fhlist ls -> fmember ls -> B elm with
|
adamc@118
|
203 | nil => fun _ idx => match idx with end
|
adamc@118
|
204 | _ :: ls' => fun mls idx =>
|
adamc@118
|
205 match idx with
|
adamc@118
|
206 | inl pf => match pf with
|
adam@426
|
207 | eq_refl => fst mls
|
adamc@118
|
208 end
|
adamc@118
|
209 | inr idx' => fhget ls' (snd mls) idx'
|
adamc@118
|
210 end
|
adamc@118
|
211 end.
|
adamc@118
|
212 End fhlist.
|
adamc@118
|
213
|
adamc@118
|
214 Implicit Arguments fhget [A B elm ls].
|
adamc@118
|
215
|
adam@427
|
216 (* begin hide *)
|
adam@427
|
217 Definition map := O.
|
adam@427
|
218 (* end hide *)
|
adam@427
|
219
|
adamc@118
|
220 (** We can define a [map]-like function for [fhlist]s. *)
|
adamc@118
|
221
|
adamc@118
|
222 Section fhlist_map.
|
adamc@118
|
223 Variables A : Type.
|
adamc@118
|
224 Variables B C : A -> Type.
|
adamc@118
|
225 Variable f : forall x, B x -> C x.
|
adamc@118
|
226
|
adamc@118
|
227 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
|
adamc@118
|
228 match ls return fhlist B ls -> fhlist C ls with
|
adamc@118
|
229 | nil => fun _ => tt
|
adamc@118
|
230 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
|
adamc@118
|
231 end.
|
adamc@118
|
232
|
adamc@118
|
233 Implicit Arguments fhmap [ls].
|
adamc@118
|
234
|
adam@427
|
235 (* begin hide *)
|
adam@427
|
236 Definition ilist := O.
|
adam@427
|
237 Definition get := O.
|
adam@427
|
238 Definition imap := O.
|
adam@427
|
239 (* end hide *)
|
adam@427
|
240
|
adamc@118
|
241 (** For the inductive versions of the [ilist] definitions, we proved a lemma about the interaction of [get] and [imap]. It was a strategic choice not to attempt such a proof for the definitions that we just gave, because that sets us on a collision course with the problems that are the subject of this chapter. *)
|
adamc@118
|
242
|
adamc@118
|
243 Variable elm : A.
|
adamc@118
|
244
|
adamc@118
|
245 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
|
adamc@118
|
246 fhget (fhmap hls) mem = f (fhget hls mem).
|
adam@298
|
247 (* begin hide *)
|
adam@298
|
248 induction ls; crush; case a0; reflexivity.
|
adam@298
|
249 (* end hide *)
|
adam@364
|
250 (** %\vspace{-.2in}%[[
|
adamc@118
|
251 induction ls; crush.
|
adam@298
|
252 ]]
|
adamc@118
|
253
|
adam@364
|
254 %\vspace{-.15in}%In Coq 8.2, one subgoal remains at this point. Coq 8.3 has added some tactic improvements that enable [crush] to complete all of both inductive cases. To introduce the basics of reasoning about equality, it will be useful to review what was necessary in Coq 8.2.
|
adam@297
|
255
|
adam@297
|
256 Part of our single remaining subgoal is:
|
adamc@118
|
257 [[
|
adamc@118
|
258 a0 : a = elm
|
adamc@118
|
259 ============================
|
adamc@118
|
260 match a0 in (_ = a2) return (C a2) with
|
adam@426
|
261 | eq_refl => f a1
|
adamc@118
|
262 end = f match a0 in (_ = a2) return (B a2) with
|
adam@426
|
263 | eq_refl => a1
|
adamc@118
|
264 end
|
adamc@118
|
265 ]]
|
adamc@118
|
266
|
adam@426
|
267 This seems like a trivial enough obligation. The equality proof [a0] must be [eq_refl], since that is the only constructor of [eq]. Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
|
adamc@118
|
268 [[
|
adamc@118
|
269 destruct a0.
|
adamc@118
|
270 ]]
|
adamc@118
|
271
|
adam@364
|
272 <<
|
adam@364
|
273 User error: Cannot solve a second-order unification problem
|
adam@364
|
274 >>
|
adam@364
|
275
|
adamc@118
|
276 This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed. We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
|
adamc@118
|
277 [[
|
adam@426
|
278 assert (a0 = eq_refl _).
|
adam@364
|
279 ]]
|
adamc@118
|
280
|
adam@364
|
281 <<
|
adam@426
|
282 The term "eq_refl ?98" has type "?98 = ?98"
|
adamc@118
|
283 while it is expected to have type "a = elm"
|
adam@364
|
284 >>
|
adamc@118
|
285
|
adamc@118
|
286 In retrospect, the problem is not so hard to see. Reflexivity proofs only show [x = x] for particular values of [x], whereas here we are thinking in terms of a proof of [a = elm], where the two sides of the equality are not equal syntactically. Thus, the essential lemma we need does not even type-check!
|
adamc@118
|
287
|
adam@427
|
288 Is it time to throw in the towel? Luckily, the answer is "no." In this chapter, we will see several useful patterns for proving obligations like this.
|
adamc@118
|
289
|
adam@407
|
290 For this particular example, the solution is surprisingly straightforward. The [destruct] tactic has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
|
adam@297
|
291 [[
|
adamc@118
|
292 case a0.
|
adam@297
|
293
|
adamc@118
|
294 ============================
|
adamc@118
|
295 f a1 = f a1
|
adamc@118
|
296 ]]
|
adamc@118
|
297
|
adam@297
|
298 It seems that [destruct] was trying to be too smart for its own good.
|
adam@297
|
299 [[
|
adamc@118
|
300 reflexivity.
|
adam@302
|
301 ]]
|
adam@364
|
302 %\vspace{-.2in}% *)
|
adamc@118
|
303 Qed.
|
adamc@124
|
304 (* end thide *)
|
adamc@118
|
305
|
adamc@118
|
306 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *)
|
adamc@118
|
307
|
adam@426
|
308 Lemma lemma1 : forall x (pf : x = elm), O = match pf with eq_refl => O end.
|
adamc@124
|
309 (* begin thide *)
|
adamc@118
|
310 simple destruct pf; reflexivity.
|
adamc@118
|
311 Qed.
|
adamc@124
|
312 (* end thide *)
|
adamc@118
|
313
|
adam@364
|
314 (** The tactic %\index{tactics!simple destruct}%[simple destruct pf] is a convenient form for applying [case]. It runs [intro] to bring into scope all quantified variables up to its argument. *)
|
adamc@118
|
315
|
adamc@118
|
316 Print lemma1.
|
adamc@218
|
317 (** %\vspace{-.15in}% [[
|
adamc@118
|
318 lemma1 =
|
adamc@118
|
319 fun (x : A) (pf : x = elm) =>
|
adamc@118
|
320 match pf as e in (_ = y) return (0 = match e with
|
adam@426
|
321 | eq_refl => 0
|
adamc@118
|
322 end) with
|
adam@426
|
323 | eq_refl => eq_refl 0
|
adamc@118
|
324 end
|
adamc@118
|
325 : forall (x : A) (pf : x = elm), 0 = match pf with
|
adam@426
|
326 | eq_refl => 0
|
adamc@118
|
327 end
|
adamc@218
|
328
|
adamc@118
|
329 ]]
|
adamc@118
|
330
|
adamc@118
|
331 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
|
adamc@118
|
332
|
adamc@124
|
333 (* begin thide *)
|
adamc@118
|
334 Definition lemma1' :=
|
adamc@118
|
335 fun (x : A) (pf : x = elm) =>
|
adamc@118
|
336 match pf return (0 = match pf with
|
adam@426
|
337 | eq_refl => 0
|
adamc@118
|
338 end) with
|
adam@426
|
339 | eq_refl => eq_refl 0
|
adamc@118
|
340 end.
|
adamc@124
|
341 (* end thide *)
|
adamc@118
|
342
|
adam@398
|
343 (** Surprisingly, what seems at first like a _simpler_ lemma is harder to prove. *)
|
adamc@118
|
344
|
adam@426
|
345 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with eq_refl => O end.
|
adamc@124
|
346 (* begin thide *)
|
adam@364
|
347 (** %\vspace{-.25in}%[[
|
adamc@118
|
348 simple destruct pf.
|
adam@364
|
349 ]]
|
adamc@205
|
350
|
adam@364
|
351 <<
|
adamc@118
|
352 User error: Cannot solve a second-order unification problem
|
adam@364
|
353 >>
|
adam@302
|
354 *)
|
adamc@118
|
355 Abort.
|
adamc@118
|
356
|
adamc@118
|
357 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
|
adamc@118
|
358
|
adamc@124
|
359 (* begin thide *)
|
adamc@124
|
360 Definition lemma2 :=
|
adamc@118
|
361 fun (x : A) (pf : x = x) =>
|
adamc@118
|
362 match pf return (0 = match pf with
|
adam@426
|
363 | eq_refl => 0
|
adamc@118
|
364 end) with
|
adam@426
|
365 | eq_refl => eq_refl 0
|
adamc@118
|
366 end.
|
adamc@124
|
367 (* end thide *)
|
adamc@118
|
368
|
adamc@118
|
369 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
|
adamc@118
|
370
|
adam@427
|
371 (* begin hide *)
|
adam@427
|
372 Definition lemma3' := O.
|
adam@427
|
373 (* end hide *)
|
adam@427
|
374
|
adam@426
|
375 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
|
adamc@124
|
376 (* begin thide *)
|
adam@364
|
377 (** %\vspace{-.25in}%[[
|
adamc@118
|
378 simple destruct pf.
|
adam@364
|
379 ]]
|
adamc@205
|
380
|
adam@364
|
381 <<
|
adamc@118
|
382 User error: Cannot solve a second-order unification problem
|
adam@364
|
383 >>
|
adam@364
|
384 %\vspace{-.15in}%*)
|
adamc@218
|
385
|
adamc@118
|
386 Abort.
|
adamc@118
|
387
|
adamc@118
|
388 (** This time, even our manual attempt fails.
|
adamc@118
|
389 [[
|
adamc@118
|
390 Definition lemma3' :=
|
adamc@118
|
391 fun (x : A) (pf : x = x) =>
|
adam@426
|
392 match pf as pf' in (_ = x') return (pf' = eq_refl x') with
|
adam@426
|
393 | eq_refl => eq_refl _
|
adamc@118
|
394 end.
|
adam@364
|
395 ]]
|
adamc@118
|
396
|
adam@364
|
397 <<
|
adam@426
|
398 The term "eq_refl x'" has type "x' = x'" while it is expected to have type
|
adamc@118
|
399 "x = x'"
|
adam@364
|
400 >>
|
adamc@118
|
401
|
adam@427
|
402 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], referring to the [in]-bound variable [x']. To do a dependent [match], we _must_ choose a fresh name for the second argument of [eq]. We are just as constrained to use the "real" value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on _must_ equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
|
adamc@118
|
403
|
adam@398
|
404 Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
|
adamc@118
|
405
|
adam@426
|
406 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
|
adamc@118
|
407 intros; apply UIP_refl.
|
adamc@118
|
408 Qed.
|
adamc@118
|
409
|
adamc@118
|
410 Check UIP_refl.
|
adamc@218
|
411 (** %\vspace{-.15in}% [[
|
adamc@118
|
412 UIP_refl
|
adam@426
|
413 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
|
adamc@118
|
414 ]]
|
adamc@118
|
415
|
adam@436
|
416 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an _axiom_, the term [eq_rect_eq] below. *)
|
adam@427
|
417
|
adam@436
|
418 (* begin hide *)
|
adam@436
|
419 Import Eq_rect_eq.
|
adam@436
|
420 (* end hide *)
|
adamc@118
|
421 Print eq_rect_eq.
|
adamc@218
|
422 (** %\vspace{-.15in}% [[
|
adam@436
|
423 *** [ eq_rect_eq :
|
adam@436
|
424 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
|
adam@436
|
425 x = eq_rect p Q x p h ]
|
adamc@118
|
426 ]]
|
adamc@118
|
427
|
adam@427
|
428 The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. The term [eq_rect] is the automatically generated recursion principle for [eq]. Calling [eq_rect] is another way of [match]ing on an equality proof. The proof we match on is the argument [h], and [x] is the body of the [match]. The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *)
|
adam@427
|
429
|
adam@427
|
430 (* begin hide *)
|
adam@427
|
431 Definition False' := False.
|
adam@427
|
432 (* end hide *)
|
adamc@118
|
433
|
adam@364
|
434 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
|
adam@364
|
435 x = eq_rect p Q x p h).
|
adam@364
|
436 (** %\vspace{-.15in}%[[
|
adam@364
|
437 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
|
adam@364
|
438 x = match h in (_ = y) return (Q y) with
|
adam@364
|
439 | eq_refl => x
|
adam@364
|
440 end
|
adam@364
|
441 ]]
|
adam@364
|
442
|
adam@427
|
443 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axioms}%axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert _inconsistent_ sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via "informal" metatheory%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC.
|
adamc@118
|
444
|
adamc@118
|
445 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
|
adamc@118
|
446
|
adam@427
|
447 (* begin hide *)
|
adam@427
|
448 Definition Streicher_K' := (Streicher_K, UIP_refl__Streicher_K).
|
adam@427
|
449 (* end hide *)
|
adam@427
|
450
|
adamc@118
|
451 Print Streicher_K.
|
adamc@124
|
452 (* end thide *)
|
adamc@218
|
453 (** %\vspace{-.15in}% [[
|
adamc@118
|
454 Streicher_K =
|
adamc@118
|
455 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
|
adamc@118
|
456 : forall (U : Type) (x : U) (P : x = x -> Prop),
|
adam@426
|
457 P (eq_refl x) -> forall p : x = x, P p
|
adamc@118
|
458 ]]
|
adamc@118
|
459
|
adam@427
|
460 This is the unfortunately named %\index{axiom K}%"Streicher's axiom K," which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
|
adamc@118
|
461
|
adamc@118
|
462 End fhlist_map.
|
adamc@118
|
463
|
adam@436
|
464 (* begin hide *)
|
adam@436
|
465 Require Eqdep_dec.
|
adam@436
|
466 (* end hide *)
|
adam@436
|
467
|
adam@364
|
468 (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality. The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)
|
adam@364
|
469
|
adamc@119
|
470
|
adamc@119
|
471 (** * Type-Casts in Theorem Statements *)
|
adamc@119
|
472
|
adamc@119
|
473 (** Sometimes we need to use tricks with equality just to state the theorems that we care about. To illustrate, we start by defining a concatenation function for [fhlist]s. *)
|
adamc@119
|
474
|
adamc@119
|
475 Section fhapp.
|
adamc@119
|
476 Variable A : Type.
|
adamc@119
|
477 Variable B : A -> Type.
|
adamc@119
|
478
|
adamc@218
|
479 Fixpoint fhapp (ls1 ls2 : list A)
|
adamc@119
|
480 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
|
adamc@218
|
481 match ls1 with
|
adamc@119
|
482 | nil => fun _ hls2 => hls2
|
adamc@119
|
483 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
|
adamc@119
|
484 end.
|
adamc@119
|
485
|
adamc@119
|
486 Implicit Arguments fhapp [ls1 ls2].
|
adamc@119
|
487
|
adamc@124
|
488 (* EX: Prove that fhapp is associative. *)
|
adamc@124
|
489 (* begin thide *)
|
adamc@124
|
490
|
adamc@119
|
491 (** We might like to prove that [fhapp] is associative.
|
adamc@119
|
492 [[
|
adamc@119
|
493 Theorem fhapp_ass : forall ls1 ls2 ls3
|
adamc@119
|
494 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
|
adamc@119
|
495 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
|
adam@364
|
496 ]]
|
adamc@119
|
497
|
adam@364
|
498 <<
|
adamc@119
|
499 The term
|
adamc@119
|
500 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
|
adamc@119
|
501 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
|
adamc@119
|
502 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
|
adam@364
|
503 >>
|
adamc@119
|
504
|
adam@407
|
505 This first cut at the theorem statement does not even type-check. We know that the two [fhlist] types appearing in the error message are always equal, by associativity of normal list append, but this fact is not apparent to the type checker. This stems from the fact that Coq's equality is%\index{intensional type theory}% _intensional_, in the sense that type equality theorems can never be applied after the fact to get a term to type-check. Instead, we need to make use of equality explicitly in the theorem statement. *)
|
adamc@119
|
506
|
adamc@119
|
507 Theorem fhapp_ass : forall ls1 ls2 ls3
|
adamc@119
|
508 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
|
adamc@119
|
509 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
|
adamc@119
|
510 fhapp hls1 (fhapp hls2 hls3)
|
adamc@119
|
511 = match pf in (_ = ls) return fhlist _ ls with
|
adam@426
|
512 | eq_refl => fhapp (fhapp hls1 hls2) hls3
|
adamc@119
|
513 end.
|
adamc@119
|
514 induction ls1; crush.
|
adamc@119
|
515
|
adamc@119
|
516 (** The first remaining subgoal looks trivial enough:
|
adamc@119
|
517 [[
|
adamc@119
|
518 ============================
|
adamc@119
|
519 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
|
adamc@119
|
520 match pf in (_ = ls) return (fhlist B ls) with
|
adam@426
|
521 | eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
|
adamc@119
|
522 end
|
adamc@119
|
523 ]]
|
adamc@119
|
524
|
adamc@119
|
525 We can try what worked in previous examples.
|
adamc@119
|
526 [[
|
adamc@119
|
527 case pf.
|
adam@364
|
528 ]]
|
adamc@119
|
529
|
adam@364
|
530 <<
|
adamc@119
|
531 User error: Cannot solve a second-order unification problem
|
adam@364
|
532 >>
|
adamc@119
|
533
|
adamc@119
|
534 It seems we have reached another case where it is unclear how to use a dependent [match] to implement case analysis on our proof. The [UIP_refl] theorem can come to our rescue again. *)
|
adamc@119
|
535
|
adamc@119
|
536 rewrite (UIP_refl _ _ pf).
|
adamc@119
|
537 (** [[
|
adamc@119
|
538 ============================
|
adamc@119
|
539 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
|
adamc@119
|
540 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
|
adam@302
|
541 ]]
|
adam@302
|
542 *)
|
adamc@119
|
543
|
adamc@119
|
544 reflexivity.
|
adamc@119
|
545
|
adamc@119
|
546 (** Our second subgoal is trickier.
|
adamc@119
|
547 [[
|
adamc@119
|
548 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
|
adamc@119
|
549 ============================
|
adamc@119
|
550 (a0,
|
adamc@119
|
551 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
|
adamc@119
|
552 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
|
adamc@119
|
553 match pf in (_ = ls) return (fhlist B ls) with
|
adam@426
|
554 | eq_refl =>
|
adamc@119
|
555 (a0,
|
adamc@119
|
556 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
557 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
|
adamc@119
|
558 end
|
adamc@119
|
559
|
adamc@119
|
560 rewrite (UIP_refl _ _ pf).
|
adam@364
|
561 ]]
|
adamc@119
|
562
|
adam@364
|
563 <<
|
adamc@119
|
564 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
|
adamc@119
|
565 while it is expected to have type "?556 = ?556"
|
adam@364
|
566 >>
|
adamc@119
|
567
|
adamc@119
|
568 We can only apply [UIP_refl] on proofs of equality with syntactically equal operands, which is not the case of [pf] here. We will need to manipulate the form of this subgoal to get us to a point where we may use [UIP_refl]. A first step is obtaining a proof suitable to use in applying the induction hypothesis. Inversion on the structure of [pf] is sufficient for that. *)
|
adamc@119
|
569
|
adamc@119
|
570 injection pf; intro pf'.
|
adamc@119
|
571 (** [[
|
adamc@119
|
572 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
|
adamc@119
|
573 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
|
adamc@119
|
574 ============================
|
adamc@119
|
575 (a0,
|
adamc@119
|
576 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
|
adamc@119
|
577 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
|
adamc@119
|
578 match pf in (_ = ls) return (fhlist B ls) with
|
adam@426
|
579 | eq_refl =>
|
adamc@119
|
580 (a0,
|
adamc@119
|
581 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
582 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
|
adamc@119
|
583 end
|
adamc@119
|
584 ]]
|
adamc@119
|
585
|
adamc@119
|
586 Now we can rewrite using the inductive hypothesis. *)
|
adamc@119
|
587
|
adamc@119
|
588 rewrite (IHls1 _ _ pf').
|
adamc@119
|
589 (** [[
|
adamc@119
|
590 ============================
|
adamc@119
|
591 (a0,
|
adamc@119
|
592 match pf' in (_ = ls) return (fhlist B ls) with
|
adam@426
|
593 | eq_refl =>
|
adamc@119
|
594 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
595 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
|
adamc@119
|
596 end) =
|
adamc@119
|
597 match pf in (_ = ls) return (fhlist B ls) with
|
adam@426
|
598 | eq_refl =>
|
adamc@119
|
599 (a0,
|
adamc@119
|
600 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
601 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
|
adamc@119
|
602 end
|
adamc@119
|
603 ]]
|
adamc@119
|
604
|
adam@398
|
605 We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion, repeated twice. Trying case analysis on our proofs still will not work, but there is a move we can make to enable it. Not only does just one call to [fhapp] matter to us now, but it also _does not matter what the result of the call is_. In other words, the subgoal should remain true if we replace this [fhapp] call with a fresh variable. The %\index{tactics!generalize}%[generalize] tactic helps us do exactly that. *)
|
adamc@119
|
606
|
adamc@119
|
607 generalize (fhapp (fhapp b hls2) hls3).
|
adamc@119
|
608 (** [[
|
adamc@119
|
609 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
|
adamc@119
|
610 (a0,
|
adamc@119
|
611 match pf' in (_ = ls) return (fhlist B ls) with
|
adam@426
|
612 | eq_refl => f
|
adamc@119
|
613 end) =
|
adamc@119
|
614 match pf in (_ = ls) return (fhlist B ls) with
|
adam@426
|
615 | eq_refl => (a0, f)
|
adamc@119
|
616 end
|
adamc@119
|
617 ]]
|
adamc@119
|
618
|
adamc@119
|
619 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations only support variables in certain positions. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood.
|
adamc@119
|
620
|
adamc@119
|
621 In this case, it is helpful to generalize over our two proofs as well. *)
|
adamc@119
|
622
|
adamc@119
|
623 generalize pf pf'.
|
adamc@119
|
624 (** [[
|
adamc@119
|
625 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
|
adamc@119
|
626 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
|
adamc@119
|
627 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
|
adamc@119
|
628 (a0,
|
adamc@119
|
629 match pf'0 in (_ = ls) return (fhlist B ls) with
|
adam@426
|
630 | eq_refl => f
|
adamc@119
|
631 end) =
|
adamc@119
|
632 match pf0 in (_ = ls) return (fhlist B ls) with
|
adam@426
|
633 | eq_refl => (a0, f)
|
adamc@119
|
634 end
|
adamc@119
|
635 ]]
|
adamc@119
|
636
|
adamc@119
|
637 To an experienced dependent types hacker, the appearance of this goal term calls for a celebration. The formula has a critical property that indicates that our problems are over. To get our proofs into the right form to apply [UIP_refl], we need to use associativity of list append to rewrite their types. We could not do that before because other parts of the goal require the proofs to retain their original types. In particular, the call to [fhapp] that we generalized must have type [(ls1 ++ ls2) ++ ls3], for some values of the list variables. If we rewrite the type of the proof used to type-cast this value to something like [ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3], then the lefthand side of the equality would no longer match the type of the term we are trying to cast.
|
adamc@119
|
638
|
adam@398
|
639 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and _may be rewritten as well_. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *)
|
adamc@119
|
640
|
adamc@119
|
641 rewrite app_ass.
|
adamc@119
|
642 (** [[
|
adamc@119
|
643 ============================
|
adamc@119
|
644 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
|
adamc@119
|
645 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
|
adamc@119
|
646 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
|
adamc@119
|
647 (a0,
|
adamc@119
|
648 match pf'0 in (_ = ls) return (fhlist B ls) with
|
adam@426
|
649 | eq_refl => f
|
adamc@119
|
650 end) =
|
adamc@119
|
651 match pf0 in (_ = ls) return (fhlist B ls) with
|
adam@426
|
652 | eq_refl => (a0, f)
|
adamc@119
|
653 end
|
adamc@119
|
654 ]]
|
adamc@119
|
655
|
adamc@119
|
656 We can see that we have achieved the crucial property: the type of each generalized equality proof has syntactically equal operands. This makes it easy to finish the proof with [UIP_refl]. *)
|
adamc@119
|
657
|
adamc@119
|
658 intros.
|
adamc@119
|
659 rewrite (UIP_refl _ _ pf0).
|
adamc@119
|
660 rewrite (UIP_refl _ _ pf'0).
|
adamc@119
|
661 reflexivity.
|
adamc@119
|
662 Qed.
|
adamc@124
|
663 (* end thide *)
|
adamc@119
|
664 End fhapp.
|
adamc@120
|
665
|
adamc@120
|
666 Implicit Arguments fhapp [A B ls1 ls2].
|
adamc@120
|
667
|
adam@364
|
668 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics. The next section explores an alternative that leads to simpler developments in some cases. *)
|
adam@364
|
669
|
adamc@120
|
670
|
adamc@120
|
671 (** * Heterogeneous Equality *)
|
adamc@120
|
672
|
adam@407
|
673 (** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing%\index{heterogeneous equality}% _heterogeneous equality_. *)
|
adamc@120
|
674
|
adamc@120
|
675 Print JMeq.
|
adamc@218
|
676 (** %\vspace{-.15in}% [[
|
adamc@120
|
677 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
|
adamc@120
|
678 JMeq_refl : JMeq x x
|
adamc@120
|
679 ]]
|
adamc@120
|
680
|
adam@427
|
681 The identity [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as a sort of pun about British politics. The definition [JMeq] starts out looking a lot like the definition of [eq]. The crucial difference is that we may use [JMeq] _on arguments of different types_. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *)
|
adamc@120
|
682
|
adamc@120
|
683 Infix "==" := JMeq (at level 70, no associativity).
|
adamc@120
|
684
|
adam@426
|
685 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
|
adamc@124
|
686 (* begin thide *)
|
adam@426
|
687 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == eq_refl x :=
|
adam@426
|
688 match pf return (pf == eq_refl _) with
|
adam@426
|
689 | eq_refl => JMeq_refl _
|
adamc@120
|
690 end.
|
adamc@124
|
691 (* end thide *)
|
adamc@120
|
692
|
adamc@120
|
693 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
|
adamc@120
|
694
|
adamc@271
|
695 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)
|
adamc@120
|
696
|
adamc@120
|
697 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
|
adam@426
|
698 O = match pf with eq_refl => O end.
|
adamc@124
|
699 (* begin thide *)
|
adamc@121
|
700 intros; rewrite (UIP_refl' pf); reflexivity.
|
adamc@120
|
701 Qed.
|
adamc@124
|
702 (* end thide *)
|
adamc@120
|
703
|
adamc@120
|
704 (** All in all, refreshingly straightforward, but there really is no such thing as a free lunch. The use of [rewrite] is implemented in terms of an axiom: *)
|
adamc@120
|
705
|
adamc@120
|
706 Check JMeq_eq.
|
adamc@218
|
707 (** %\vspace{-.15in}% [[
|
adamc@120
|
708 JMeq_eq
|
adamc@120
|
709 : forall (A : Type) (x y : A), x == y -> x = y
|
adamc@218
|
710 ]]
|
adamc@120
|
711
|
adamc@218
|
712 It may be surprising that we cannot prove that heterogeneous equality implies normal equality. The difficulties are the same kind we have seen so far, based on limitations of [match] annotations.
|
adamc@120
|
713
|
adamc@120
|
714 We can redo our [fhapp] associativity proof based around [JMeq]. *)
|
adamc@120
|
715
|
adamc@120
|
716 Section fhapp'.
|
adamc@120
|
717 Variable A : Type.
|
adamc@120
|
718 Variable B : A -> Type.
|
adamc@120
|
719
|
adamc@120
|
720 (** This time, the naive theorem statement type-checks. *)
|
adamc@120
|
721
|
adamc@124
|
722 (* EX: Prove [fhapp] associativity using [JMeq]. *)
|
adamc@124
|
723
|
adamc@124
|
724 (* begin thide *)
|
adam@364
|
725 Theorem fhapp_ass' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
|
adam@364
|
726 (hls3 : fhlist B ls3),
|
adamc@120
|
727 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
|
adamc@120
|
728 induction ls1; crush.
|
adamc@120
|
729
|
adamc@120
|
730 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
|
adamc@120
|
731 [[
|
adamc@120
|
732 ============================
|
adam@297
|
733 (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
|
adamc@120
|
734 ]]
|
adamc@120
|
735
|
adam@297
|
736 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. Here is what happens when we try that in Coq 8.2:
|
adamc@120
|
737 [[
|
adamc@120
|
738 rewrite IHls1.
|
adam@364
|
739 ]]
|
adamc@120
|
740
|
adam@364
|
741 <<
|
adamc@120
|
742 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
|
adamc@120
|
743 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
|
adam@364
|
744 >>
|
adamc@120
|
745
|
adam@407
|
746 Coq 8.4 currently gives an error message about an uncaught exception. Perhaps that will be fixed soon. In any case, it is educational to consider a more explicit approach.
|
adam@297
|
747
|
adamc@120
|
748 We see that [JMeq] is not a silver bullet. We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts. Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type. That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument.
|
adamc@120
|
749
|
adamc@120
|
750 We can get around this problem by another multiple use of [generalize]. We want to bring into the goal the proper instance of the inductive hypothesis, and we also want to generalize the two relevant uses of [fhapp]. *)
|
adamc@120
|
751
|
adamc@120
|
752 generalize (fhapp b (fhapp hls2 hls3))
|
adamc@120
|
753 (fhapp (fhapp b hls2) hls3)
|
adamc@120
|
754 (IHls1 _ _ b hls2 hls3).
|
adam@364
|
755 (** %\vspace{-.15in}%[[
|
adamc@120
|
756 ============================
|
adamc@120
|
757 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
|
adamc@120
|
758 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
|
adamc@120
|
759 ]]
|
adamc@120
|
760
|
adamc@120
|
761 Now we can rewrite with append associativity, as before. *)
|
adamc@120
|
762
|
adamc@120
|
763 rewrite app_ass.
|
adam@364
|
764 (** %\vspace{-.15in}%[[
|
adamc@120
|
765 ============================
|
adamc@120
|
766 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
|
adamc@120
|
767 ]]
|
adamc@120
|
768
|
adamc@120
|
769 From this point, the goal is trivial. *)
|
adamc@120
|
770
|
adamc@120
|
771 intros f f0 H; rewrite H; reflexivity.
|
adamc@120
|
772 Qed.
|
adamc@124
|
773 (* end thide *)
|
adamc@121
|
774
|
adam@385
|
775 End fhapp'.
|
adam@385
|
776
|
adam@385
|
777 (** This example illustrates a general pattern: heterogeneous equality often simplifies theorem statements, but we still need to do some work to line up some dependent pattern matches that tactics will generate for us.
|
adam@385
|
778
|
adam@385
|
779 The proof we have found relies on the [JMeq_eq] axiom, which we can verify with a command%\index{Vernacular commands!Print Assumptions}% that we will discuss more in two chapters. *)
|
adam@385
|
780
|
adam@385
|
781 Print Assumptions fhapp_ass'.
|
adam@385
|
782 (** %\vspace{-.15in}%[[
|
adam@385
|
783 Axioms:
|
adam@385
|
784 JMeq_eq : forall (A : Type) (x y : A), x == y -> x = y
|
adam@385
|
785 ]]
|
adam@385
|
786
|
adam@385
|
787 It was the [rewrite H] tactic that implicitly appealed to the axiom. By restructuring the proof, we can avoid axiom dependence. A general lemma about pairs provides the key element. (Our use of [generalize] above can be thought of as reducing the proof to another, more complex and specialized lemma.) *)
|
adam@385
|
788
|
adam@385
|
789 Lemma pair_cong : forall A1 A2 B1 B2 (x1 : A1) (x2 : A2) (y1 : B1) (y2 : B2),
|
adam@385
|
790 x1 == x2
|
adam@385
|
791 -> y1 == y2
|
adam@385
|
792 -> (x1, y1) == (x2, y2).
|
adam@385
|
793 intros until y2; intros Hx Hy; rewrite Hx; rewrite Hy; reflexivity.
|
adam@385
|
794 Qed.
|
adam@385
|
795
|
adam@385
|
796 Hint Resolve pair_cong.
|
adam@385
|
797
|
adam@385
|
798 Section fhapp''.
|
adam@385
|
799 Variable A : Type.
|
adam@385
|
800 Variable B : A -> Type.
|
adam@385
|
801
|
adam@385
|
802 Theorem fhapp_ass'' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
|
adam@385
|
803 (hls3 : fhlist B ls3),
|
adam@385
|
804 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
|
adam@385
|
805 induction ls1; crush.
|
adam@385
|
806 Qed.
|
adam@385
|
807 End fhapp''.
|
adam@385
|
808
|
adam@385
|
809 Print Assumptions fhapp_ass''.
|
adam@385
|
810 (** <<
|
adam@385
|
811 Closed under the global context
|
adam@385
|
812 >>
|
adam@385
|
813
|
adam@385
|
814 One might wonder exactly which elements of a proof involving [JMeq] imply that [JMeq_eq] must be used. For instance, above we noticed that [rewrite] had brought [JMeq_eq] into the proof of [fhap_ass'], yet here we have also used [rewrite] with [JMeq] hypotheses while avoiding axioms! One illuminating exercise is comparing the types of the lemmas that [rewrite] uses under the hood to implement the rewrites. Here is the normal lemma for [eq] rewriting:%\index{Gallina terms!eq\_ind\_r}% *)
|
adam@385
|
815
|
adam@385
|
816 Check eq_ind_r.
|
adam@385
|
817 (** %\vspace{-.15in}%[[
|
adam@385
|
818 eq_ind_r
|
adam@385
|
819 : forall (A : Type) (x : A) (P : A -> Prop),
|
adam@385
|
820 P x -> forall y : A, y = x -> P y
|
adam@385
|
821 ]]
|
adam@385
|
822
|
adam@398
|
823 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is %\index{Gallina terms!internal\_JMeq\_rew\_r}%[internal_JMeq_rew_r], which, confusingly, is defined by [rewrite] as needed, so it is not available for checking until after we apply it. *)
|
adam@385
|
824
|
adam@398
|
825 Check internal_JMeq_rew_r.
|
adam@385
|
826 (** %\vspace{-.15in}%[[
|
adam@398
|
827 internal_JMeq_rew_r
|
adam@385
|
828 : forall (A : Type) (x : A) (B : Type) (b : B)
|
adam@385
|
829 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x
|
adam@385
|
830 ]]
|
adam@385
|
831
|
adam@398
|
832 The key difference is that, where the [eq] lemma is parametrized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop]. To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y]. In contrast, to apply [internal_JMeq_rew_r], it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and _its type_. In other words, the predicate must be _polymorphic_ in [y]'s type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done naively leads to a type error.
|
adam@385
|
833
|
adam@398
|
834 When [rewrite] cannot figure out how to apply [internal_JMeq_rew_r] for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *)
|
adam@385
|
835
|
adam@385
|
836 Check JMeq_ind_r.
|
adam@385
|
837 (** %\vspace{-.15in}%[[
|
adam@385
|
838 JMeq_ind_r
|
adam@385
|
839 : forall (A : Type) (x : A) (P : A -> Prop),
|
adam@385
|
840 P x -> forall y : A, y == x -> P y
|
adam@385
|
841 ]]
|
adam@385
|
842
|
adam@398
|
843 Ironically, where in the proof of [fhapp_ass'] we used [rewrite app_ass] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free [internal_JMeq_rew_r]!
|
adam@385
|
844
|
adam@385
|
845 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *)
|
adam@385
|
846
|
adam@385
|
847 Theorem out_of_luck : forall n m : nat,
|
adam@385
|
848 n == m
|
adam@385
|
849 -> S n == S m.
|
adam@385
|
850 intros n m H.
|
adam@385
|
851
|
adam@385
|
852 (** Applying [JMeq_ind_r] is easy, as the %\index{tactics!pattern}%[pattern] tactic will transform the goal into an application of an appropriate [fun] to a term that we want to abstract. *)
|
adam@385
|
853
|
adam@385
|
854 pattern n.
|
adam@385
|
855 (** %\vspace{-.15in}%[[
|
adam@385
|
856 n : nat
|
adam@385
|
857 m : nat
|
adam@385
|
858 H : n == m
|
adam@385
|
859 ============================
|
adam@385
|
860 (fun n0 : nat => S n0 == S m) n
|
adam@385
|
861 ]]
|
adam@385
|
862 *)
|
adam@385
|
863 apply JMeq_ind_r with (x := m); auto.
|
adam@385
|
864
|
adam@398
|
865 (** However, we run into trouble trying to get the goal into a form compatible with [internal_JMeq_rew_r.] *)
|
adam@427
|
866
|
adam@385
|
867 Undo 2.
|
adam@385
|
868 (** %\vspace{-.15in}%[[
|
adam@385
|
869 pattern nat, n.
|
adam@385
|
870 ]]
|
adam@385
|
871 <<
|
adam@385
|
872 Error: The abstracted term "fun (P : Set) (n0 : P) => S n0 == S m"
|
adam@385
|
873 is not well typed.
|
adam@385
|
874 Illegal application (Type Error):
|
adam@385
|
875 The term "S" of type "nat -> nat"
|
adam@385
|
876 cannot be applied to the term
|
adam@385
|
877 "n0" : "P"
|
adam@385
|
878 This term has type "P" which should be coercible to
|
adam@385
|
879 "nat".
|
adam@385
|
880 >>
|
adam@385
|
881
|
adam@385
|
882 In other words, the successor function [S] is insufficiently polymorphic. If we try to generalize over the type of [n], we find that [S] is no longer legal to apply to [n]. *)
|
adam@385
|
883
|
adam@385
|
884 Abort.
|
adam@385
|
885
|
adam@427
|
886 (** Why did we not run into this problem in our proof of [fhapp_ass'']? The reason is that the pair constructor is polymorphic in the types of the pair components, while functions like [S] are not polymorphic at all. Use of such non-polymorphic functions with [JMeq] tends to push toward use of axioms. The example with [nat] here is a bit unrealistic; more likely cases would involve functions that have _some_ polymorphism, but not enough to allow abstractions of the sort we attempted above with [pattern]. For instance, we might have an equality between two lists, where the goal only type-checks when the terms involved really are lists, though everything is polymorphic in the types of list data elements. The {{http://www.mpi-sws.org/~gil/Heq/}Heq} library builds up a slightly different foundation to help avoid such problems. *)
|
adam@364
|
887
|
adamc@121
|
888
|
adamc@121
|
889 (** * Equivalence of Equality Axioms *)
|
adamc@121
|
890
|
adamc@124
|
891 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
|
adamc@124
|
892
|
adamc@124
|
893 (* begin thide *)
|
adamc@272
|
894 (** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business. The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together. It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof. In this section, we demonstrate this by showing how each of the previous two sections' approaches reduces to the other logically.
|
adamc@121
|
895
|
adamc@121
|
896 To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section. The rest of the proof is trivial. *)
|
adamc@121
|
897
|
adam@426
|
898 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x.
|
adamc@121
|
899 intros; rewrite (UIP_refl' pf); reflexivity.
|
adamc@121
|
900 Qed.
|
adamc@121
|
901
|
adamc@121
|
902 (** The other direction is perhaps more interesting. Assume that we only have the axiom of the [Eqdep] module available. We can define [JMeq] in a way that satisfies the same interface as the combination of the [JMeq] module's inductive definition and axiom. *)
|
adamc@121
|
903
|
adamc@121
|
904 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
|
adam@426
|
905 exists pf : B = A, x = match pf with eq_refl => y end.
|
adamc@121
|
906
|
adamc@121
|
907 Infix "===" := JMeq' (at level 70, no associativity).
|
adamc@121
|
908
|
adam@427
|
909 (** remove printing exists *)
|
adam@427
|
910
|
adamc@121
|
911 (** We say that, by definition, [x] and [y] are equal if and only if there exists a proof [pf] that their types are equal, such that [x] equals the result of casting [y] with [pf]. This statement can look strange from the standpoint of classical math, where we almost never mention proofs explicitly with quantifiers in formulas, but it is perfectly legal Coq code.
|
adamc@121
|
912
|
adamc@121
|
913 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
|
adamc@121
|
914
|
adamc@121
|
915 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
|
adam@426
|
916 intros; unfold JMeq'; exists (eq_refl A); reflexivity.
|
adamc@121
|
917 Qed.
|
adamc@121
|
918
|
adamc@121
|
919 (** printing exists $\exists$ *)
|
adamc@121
|
920
|
adamc@121
|
921 (** The proof of an analogue to [JMeq_eq] is a little more interesting, but most of the action is in appealing to [UIP_refl]. *)
|
adamc@121
|
922
|
adamc@121
|
923 Theorem JMeq_eq' : forall (A : Type) (x y : A),
|
adamc@121
|
924 x === y -> x = y.
|
adamc@121
|
925 unfold JMeq'; intros.
|
adamc@121
|
926 (** [[
|
adamc@121
|
927 H : exists pf : A = A,
|
adamc@121
|
928 x = match pf in (_ = T) return T with
|
adam@426
|
929 | eq_refl => y
|
adamc@121
|
930 end
|
adamc@121
|
931 ============================
|
adamc@121
|
932 x = y
|
adam@302
|
933 ]]
|
adam@302
|
934 *)
|
adamc@121
|
935
|
adamc@121
|
936 destruct H.
|
adamc@121
|
937 (** [[
|
adamc@121
|
938 x0 : A = A
|
adamc@121
|
939 H : x = match x0 in (_ = T) return T with
|
adam@426
|
940 | eq_refl => y
|
adamc@121
|
941 end
|
adamc@121
|
942 ============================
|
adamc@121
|
943 x = y
|
adam@302
|
944 ]]
|
adam@302
|
945 *)
|
adamc@121
|
946
|
adamc@121
|
947 rewrite H.
|
adamc@121
|
948 (** [[
|
adamc@121
|
949 x0 : A = A
|
adamc@121
|
950 ============================
|
adamc@121
|
951 match x0 in (_ = T) return T with
|
adam@426
|
952 | eq_refl => y
|
adamc@121
|
953 end = y
|
adam@302
|
954 ]]
|
adam@302
|
955 *)
|
adamc@121
|
956
|
adamc@121
|
957 rewrite (UIP_refl _ _ x0); reflexivity.
|
adamc@121
|
958 Qed.
|
adamc@121
|
959
|
adam@427
|
960 (** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always interconvert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements. *)
|
adamc@123
|
961
|
adamc@124
|
962 (* end thide *)
|
adamc@123
|
963
|
adamc@123
|
964
|
adamc@123
|
965 (** * Equality of Functions *)
|
adamc@123
|
966
|
adamc@123
|
967 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
|
adam@407
|
968 Theorem two_identities : (fun n => n) = (fun n => n + 0).
|
adamc@205
|
969 ]]
|
adamc@205
|
970
|
adam@407
|
971 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be%\index{extensionality of function equality}% _extensional_. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We _can_ assert function extensionality as an axiom, and indeed the standard library already contains that axiom. *)
|
adamc@123
|
972
|
adam@407
|
973 Require Import FunctionalExtensionality.
|
adam@407
|
974 About functional_extensionality.
|
adam@407
|
975 (** %\vspace{-.15in}%[[
|
adam@407
|
976 functional_extensionality :
|
adam@407
|
977 forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g
|
adam@407
|
978 ]]
|
adam@407
|
979 *)
|
adamc@123
|
980
|
adamc@123
|
981 (** This axiom has been verified metatheoretically to be consistent with CIC and the two equality axioms we considered previously. With it, the proof of [S_eta] is trivial. *)
|
adamc@123
|
982
|
adam@407
|
983 Theorem two_identities : (fun n => n) = (fun n => n + 0).
|
adamc@124
|
984 (* begin thide *)
|
adam@407
|
985 apply functional_extensionality; crush.
|
adamc@123
|
986 Qed.
|
adamc@124
|
987 (* end thide *)
|
adamc@123
|
988
|
adam@427
|
989 (** The same axiom can help us prove equality of types, where we need to "reason under quantifiers." *)
|
adamc@123
|
990
|
adamc@123
|
991 Theorem forall_eq : (forall x : nat, match x with
|
adamc@123
|
992 | O => True
|
adamc@123
|
993 | S _ => True
|
adamc@123
|
994 end)
|
adamc@123
|
995 = (forall _ : nat, True).
|
adamc@123
|
996
|
adam@364
|
997 (** There are no immediate opportunities to apply [ext_eq], but we can use %\index{tactics!change}%[change] to fix that. *)
|
adamc@123
|
998
|
adamc@124
|
999 (* begin thide *)
|
adamc@123
|
1000 change ((forall x : nat, (fun x => match x with
|
adamc@123
|
1001 | 0 => True
|
adamc@123
|
1002 | S _ => True
|
adamc@123
|
1003 end) x) = (nat -> True)).
|
adam@407
|
1004 rewrite (functional_extensionality (fun x => match x with
|
adam@407
|
1005 | 0 => True
|
adam@407
|
1006 | S _ => True
|
adam@407
|
1007 end) (fun _ => True)).
|
adamc@123
|
1008 (** [[
|
adamc@123
|
1009 2 subgoals
|
adamc@123
|
1010
|
adamc@123
|
1011 ============================
|
adamc@123
|
1012 (nat -> True) = (nat -> True)
|
adamc@123
|
1013
|
adamc@123
|
1014 subgoal 2 is:
|
adamc@123
|
1015 forall x : nat, match x with
|
adamc@123
|
1016 | 0 => True
|
adamc@123
|
1017 | S _ => True
|
adamc@123
|
1018 end = True
|
adam@302
|
1019 ]]
|
adam@302
|
1020 *)
|
adamc@123
|
1021
|
adamc@123
|
1022 reflexivity.
|
adamc@123
|
1023
|
adamc@123
|
1024 destruct x; constructor.
|
adamc@123
|
1025 Qed.
|
adamc@124
|
1026 (* end thide *)
|
adamc@127
|
1027
|
adam@407
|
1028 (** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of%\index{functional extensionality}% _functional extensionality_ for types with decidable equality. To allow equality reasoning without axioms, it may be worth rewriting a development to replace functions with alternate representations, such as finite map types for which extensionality is derivable in CIC. *)
|