adam@297
|
1 (* Copyright (c) 2008-2011, 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@364
|
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}\textit{%#<i>#definitional equality#</i>#%}%. 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@364
|
92 (** The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a %\index{propositional equality}\textit{%#<i>#propositional equality#</i>#%}%, 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
|
93
|
adam@294
|
94 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
|
95
|
adamc@122
|
96
|
adamc@118
|
97 (** * Heterogeneous Lists Revisited *)
|
adamc@118
|
98
|
adam@292
|
99 (** 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 [member] types. *)
|
adamc@118
|
100
|
adamc@118
|
101 Section fhlist.
|
adamc@118
|
102 Variable A : Type.
|
adamc@118
|
103 Variable B : A -> Type.
|
adamc@118
|
104
|
adamc@118
|
105 Fixpoint fhlist (ls : list A) : Type :=
|
adamc@118
|
106 match ls with
|
adamc@118
|
107 | nil => unit
|
adamc@118
|
108 | x :: ls' => B x * fhlist ls'
|
adamc@118
|
109 end%type.
|
adamc@118
|
110
|
adamc@118
|
111 Variable elm : A.
|
adamc@118
|
112
|
adamc@118
|
113 Fixpoint fmember (ls : list A) : Type :=
|
adamc@118
|
114 match ls with
|
adamc@118
|
115 | nil => Empty_set
|
adamc@118
|
116 | x :: ls' => (x = elm) + fmember ls'
|
adamc@118
|
117 end%type.
|
adamc@118
|
118
|
adamc@118
|
119 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
|
adamc@118
|
120 match ls return fhlist ls -> fmember ls -> B elm with
|
adamc@118
|
121 | nil => fun _ idx => match idx with end
|
adamc@118
|
122 | _ :: ls' => fun mls idx =>
|
adamc@118
|
123 match idx with
|
adamc@118
|
124 | inl pf => match pf with
|
adamc@118
|
125 | refl_equal => fst mls
|
adamc@118
|
126 end
|
adamc@118
|
127 | inr idx' => fhget ls' (snd mls) idx'
|
adamc@118
|
128 end
|
adamc@118
|
129 end.
|
adamc@118
|
130 End fhlist.
|
adamc@118
|
131
|
adamc@118
|
132 Implicit Arguments fhget [A B elm ls].
|
adamc@118
|
133
|
adamc@118
|
134 (** We can define a [map]-like function for [fhlist]s. *)
|
adamc@118
|
135
|
adamc@118
|
136 Section fhlist_map.
|
adamc@118
|
137 Variables A : Type.
|
adamc@118
|
138 Variables B C : A -> Type.
|
adamc@118
|
139 Variable f : forall x, B x -> C x.
|
adamc@118
|
140
|
adamc@118
|
141 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
|
adamc@118
|
142 match ls return fhlist B ls -> fhlist C ls with
|
adamc@118
|
143 | nil => fun _ => tt
|
adamc@118
|
144 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
|
adamc@118
|
145 end.
|
adamc@118
|
146
|
adamc@118
|
147 Implicit Arguments fhmap [ls].
|
adamc@118
|
148
|
adamc@118
|
149 (** 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
|
150
|
adamc@118
|
151 Variable elm : A.
|
adamc@118
|
152
|
adamc@118
|
153 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
|
adamc@118
|
154 fhget (fhmap hls) mem = f (fhget hls mem).
|
adam@298
|
155 (* begin hide *)
|
adam@298
|
156 induction ls; crush; case a0; reflexivity.
|
adam@298
|
157 (* end hide *)
|
adam@364
|
158 (** %\vspace{-.2in}%[[
|
adamc@118
|
159 induction ls; crush.
|
adam@298
|
160 ]]
|
adamc@118
|
161
|
adam@364
|
162 %\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
|
163
|
adam@297
|
164 Part of our single remaining subgoal is:
|
adamc@118
|
165 [[
|
adamc@118
|
166 a0 : a = elm
|
adamc@118
|
167 ============================
|
adamc@118
|
168 match a0 in (_ = a2) return (C a2) with
|
adamc@118
|
169 | refl_equal => f a1
|
adamc@118
|
170 end = f match a0 in (_ = a2) return (B a2) with
|
adamc@118
|
171 | refl_equal => a1
|
adamc@118
|
172 end
|
adamc@118
|
173 ]]
|
adamc@118
|
174
|
adamc@118
|
175 This seems like a trivial enough obligation. The equality proof [a0] must be [refl_equal], 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
|
176 [[
|
adamc@118
|
177 destruct a0.
|
adamc@118
|
178 ]]
|
adamc@118
|
179
|
adam@364
|
180 <<
|
adam@364
|
181 User error: Cannot solve a second-order unification problem
|
adam@364
|
182 >>
|
adam@364
|
183
|
adamc@118
|
184 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
|
185 [[
|
adamc@118
|
186 assert (a0 = refl_equal _).
|
adam@364
|
187 ]]
|
adamc@118
|
188
|
adam@364
|
189 <<
|
adamc@118
|
190 The term "refl_equal ?98" has type "?98 = ?98"
|
adamc@118
|
191 while it is expected to have type "a = elm"
|
adam@364
|
192 >>
|
adamc@118
|
193
|
adamc@118
|
194 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
|
195
|
adam@292
|
196 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
|
197
|
adam@297
|
198 For this particular example, the solution is surprisingly straightforward. [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
|
adam@297
|
199 [[
|
adamc@118
|
200 case a0.
|
adam@297
|
201
|
adamc@118
|
202 ============================
|
adamc@118
|
203 f a1 = f a1
|
adamc@118
|
204 ]]
|
adamc@118
|
205
|
adam@297
|
206 It seems that [destruct] was trying to be too smart for its own good.
|
adam@297
|
207 [[
|
adamc@118
|
208 reflexivity.
|
adam@302
|
209 ]]
|
adam@364
|
210 %\vspace{-.2in}% *)
|
adamc@118
|
211 Qed.
|
adamc@124
|
212 (* end thide *)
|
adamc@118
|
213
|
adamc@118
|
214 (** 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
|
215
|
adamc@118
|
216 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
|
adamc@124
|
217 (* begin thide *)
|
adamc@118
|
218 simple destruct pf; reflexivity.
|
adamc@118
|
219 Qed.
|
adamc@124
|
220 (* end thide *)
|
adamc@118
|
221
|
adam@364
|
222 (** 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
|
223
|
adamc@118
|
224 Print lemma1.
|
adamc@218
|
225 (** %\vspace{-.15in}% [[
|
adamc@118
|
226 lemma1 =
|
adamc@118
|
227 fun (x : A) (pf : x = elm) =>
|
adamc@118
|
228 match pf as e in (_ = y) return (0 = match e with
|
adamc@118
|
229 | refl_equal => 0
|
adamc@118
|
230 end) with
|
adamc@118
|
231 | refl_equal => refl_equal 0
|
adamc@118
|
232 end
|
adamc@118
|
233 : forall (x : A) (pf : x = elm), 0 = match pf with
|
adamc@118
|
234 | refl_equal => 0
|
adamc@118
|
235 end
|
adamc@218
|
236
|
adamc@118
|
237 ]]
|
adamc@118
|
238
|
adamc@118
|
239 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
|
adamc@118
|
240
|
adamc@124
|
241 (* begin thide *)
|
adamc@118
|
242 Definition lemma1' :=
|
adamc@118
|
243 fun (x : A) (pf : x = elm) =>
|
adamc@118
|
244 match pf return (0 = match pf with
|
adamc@118
|
245 | refl_equal => 0
|
adamc@118
|
246 end) with
|
adamc@118
|
247 | refl_equal => refl_equal 0
|
adamc@118
|
248 end.
|
adamc@124
|
249 (* end thide *)
|
adamc@118
|
250
|
adamc@118
|
251 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
|
adamc@118
|
252
|
adamc@118
|
253 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
|
adamc@124
|
254 (* begin thide *)
|
adam@364
|
255 (** %\vspace{-.25in}%[[
|
adamc@118
|
256 simple destruct pf.
|
adam@364
|
257 ]]
|
adamc@205
|
258
|
adam@364
|
259 <<
|
adamc@118
|
260 User error: Cannot solve a second-order unification problem
|
adam@364
|
261 >>
|
adam@302
|
262 *)
|
adamc@118
|
263 Abort.
|
adamc@118
|
264
|
adamc@118
|
265 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
|
adamc@118
|
266
|
adamc@124
|
267 (* begin thide *)
|
adamc@124
|
268 Definition lemma2 :=
|
adamc@118
|
269 fun (x : A) (pf : x = x) =>
|
adamc@118
|
270 match pf return (0 = match pf with
|
adamc@118
|
271 | refl_equal => 0
|
adamc@118
|
272 end) with
|
adamc@118
|
273 | refl_equal => refl_equal 0
|
adamc@118
|
274 end.
|
adamc@124
|
275 (* end thide *)
|
adamc@118
|
276
|
adamc@118
|
277 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
|
adamc@118
|
278
|
adamc@118
|
279 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
|
adamc@124
|
280 (* begin thide *)
|
adam@364
|
281 (** %\vspace{-.25in}%[[
|
adamc@118
|
282 simple destruct pf.
|
adam@364
|
283 ]]
|
adamc@205
|
284
|
adam@364
|
285 <<
|
adamc@118
|
286 User error: Cannot solve a second-order unification problem
|
adam@364
|
287 >>
|
adam@364
|
288 %\vspace{-.15in}%*)
|
adamc@218
|
289
|
adamc@118
|
290 Abort.
|
adamc@118
|
291
|
adamc@118
|
292 (** This time, even our manual attempt fails.
|
adamc@118
|
293 [[
|
adamc@118
|
294 Definition lemma3' :=
|
adamc@118
|
295 fun (x : A) (pf : x = x) =>
|
adamc@118
|
296 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
|
adamc@118
|
297 | refl_equal => refl_equal _
|
adamc@118
|
298 end.
|
adam@364
|
299 ]]
|
adamc@118
|
300
|
adam@364
|
301 <<
|
adamc@118
|
302 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
|
adamc@118
|
303 "x = x'"
|
adam@364
|
304 >>
|
adamc@118
|
305
|
adam@296
|
306 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 %\textit{%#<i>#must#</i>#%}% 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 %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
|
adamc@118
|
307
|
adamc@118
|
308 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)
|
adamc@118
|
309
|
adamc@118
|
310 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
|
adamc@118
|
311 intros; apply UIP_refl.
|
adamc@118
|
312 Qed.
|
adamc@118
|
313
|
adamc@118
|
314 Check UIP_refl.
|
adamc@218
|
315 (** %\vspace{-.15in}% [[
|
adamc@118
|
316 UIP_refl
|
adamc@118
|
317 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
|
adamc@118
|
318 ]]
|
adamc@118
|
319
|
adam@364
|
320 The theorem %\index{Gallina terms!UIF\_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 %\textit{%#<i>#axiom#</i>#%}%. *)
|
adamc@118
|
321
|
adamc@118
|
322 Print eq_rect_eq.
|
adamc@218
|
323 (** %\vspace{-.15in}% [[
|
adamc@118
|
324 eq_rect_eq =
|
adamc@118
|
325 fun U : Type => Eq_rect_eq.eq_rect_eq U
|
adamc@118
|
326 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
|
adamc@118
|
327 x = eq_rect p Q x p h
|
adamc@118
|
328 ]]
|
adamc@118
|
329
|
adam@364
|
330 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). *)
|
adamc@118
|
331
|
adam@364
|
332 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
|
adam@364
|
333 x = eq_rect p Q x p h).
|
adam@364
|
334 (** %\vspace{-.15in}%[[
|
adam@364
|
335 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
|
adam@364
|
336 x = match h in (_ = y) return (Q y) with
|
adam@364
|
337 | eq_refl => x
|
adam@364
|
338 end
|
adam@364
|
339 ]]
|
adam@364
|
340
|
adam@364
|
341 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axiom}%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 %\textit{%#<i>#inconsistent#</i>#%}% 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
|
342
|
adamc@118
|
343 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
|
adamc@118
|
344
|
adamc@118
|
345 Print Streicher_K.
|
adamc@124
|
346 (* end thide *)
|
adamc@218
|
347 (** %\vspace{-.15in}% [[
|
adamc@118
|
348 Streicher_K =
|
adamc@118
|
349 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
|
adamc@118
|
350 : forall (U : Type) (x : U) (P : x = x -> Prop),
|
adamc@118
|
351 P (refl_equal x) -> forall p : x = x, P p
|
adamc@118
|
352 ]]
|
adamc@118
|
353
|
adam@364
|
354 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
|
355
|
adamc@118
|
356 End fhlist_map.
|
adamc@118
|
357
|
adam@364
|
358 (** 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
|
359
|
adamc@119
|
360
|
adamc@119
|
361 (** * Type-Casts in Theorem Statements *)
|
adamc@119
|
362
|
adamc@119
|
363 (** 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
|
364
|
adamc@119
|
365 Section fhapp.
|
adamc@119
|
366 Variable A : Type.
|
adamc@119
|
367 Variable B : A -> Type.
|
adamc@119
|
368
|
adamc@218
|
369 Fixpoint fhapp (ls1 ls2 : list A)
|
adamc@119
|
370 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
|
adamc@218
|
371 match ls1 with
|
adamc@119
|
372 | nil => fun _ hls2 => hls2
|
adamc@119
|
373 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
|
adamc@119
|
374 end.
|
adamc@119
|
375
|
adamc@119
|
376 Implicit Arguments fhapp [ls1 ls2].
|
adamc@119
|
377
|
adamc@124
|
378 (* EX: Prove that fhapp is associative. *)
|
adamc@124
|
379 (* begin thide *)
|
adamc@124
|
380
|
adamc@119
|
381 (** We might like to prove that [fhapp] is associative.
|
adamc@119
|
382 [[
|
adamc@119
|
383 Theorem fhapp_ass : forall ls1 ls2 ls3
|
adamc@119
|
384 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
|
adamc@119
|
385 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
|
adam@364
|
386 ]]
|
adamc@119
|
387
|
adam@364
|
388 <<
|
adamc@119
|
389 The term
|
adamc@119
|
390 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
|
adamc@119
|
391 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
|
adamc@119
|
392 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
|
adam@364
|
393 >>
|
adamc@119
|
394
|
adam@364
|
395 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}\textit{%#<i>#intensional#</i>#%}%, 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
|
396
|
adamc@119
|
397 Theorem fhapp_ass : forall ls1 ls2 ls3
|
adamc@119
|
398 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
|
adamc@119
|
399 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
|
adamc@119
|
400 fhapp hls1 (fhapp hls2 hls3)
|
adamc@119
|
401 = match pf in (_ = ls) return fhlist _ ls with
|
adamc@119
|
402 | refl_equal => fhapp (fhapp hls1 hls2) hls3
|
adamc@119
|
403 end.
|
adamc@119
|
404 induction ls1; crush.
|
adamc@119
|
405
|
adamc@119
|
406 (** The first remaining subgoal looks trivial enough:
|
adamc@119
|
407 [[
|
adamc@119
|
408 ============================
|
adamc@119
|
409 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
|
adamc@119
|
410 match pf in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
411 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
|
adamc@119
|
412 end
|
adamc@119
|
413 ]]
|
adamc@119
|
414
|
adamc@119
|
415 We can try what worked in previous examples.
|
adamc@119
|
416 [[
|
adamc@119
|
417 case pf.
|
adam@364
|
418 ]]
|
adamc@119
|
419
|
adam@364
|
420 <<
|
adamc@119
|
421 User error: Cannot solve a second-order unification problem
|
adam@364
|
422 >>
|
adamc@119
|
423
|
adamc@119
|
424 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
|
425
|
adamc@119
|
426 rewrite (UIP_refl _ _ pf).
|
adamc@119
|
427 (** [[
|
adamc@119
|
428 ============================
|
adamc@119
|
429 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
|
adamc@119
|
430 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
|
adam@302
|
431 ]]
|
adam@302
|
432 *)
|
adamc@119
|
433
|
adamc@119
|
434 reflexivity.
|
adamc@119
|
435
|
adamc@119
|
436 (** Our second subgoal is trickier.
|
adamc@119
|
437 [[
|
adamc@119
|
438 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
|
adamc@119
|
439 ============================
|
adamc@119
|
440 (a0,
|
adamc@119
|
441 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
|
adamc@119
|
442 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
|
adamc@119
|
443 match pf in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
444 | refl_equal =>
|
adamc@119
|
445 (a0,
|
adamc@119
|
446 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
447 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
|
adamc@119
|
448 end
|
adamc@119
|
449
|
adamc@119
|
450 rewrite (UIP_refl _ _ pf).
|
adam@364
|
451 ]]
|
adamc@119
|
452
|
adam@364
|
453 <<
|
adamc@119
|
454 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
|
adamc@119
|
455 while it is expected to have type "?556 = ?556"
|
adam@364
|
456 >>
|
adamc@119
|
457
|
adamc@119
|
458 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
|
459
|
adamc@119
|
460 injection pf; intro pf'.
|
adamc@119
|
461 (** [[
|
adamc@119
|
462 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
|
adamc@119
|
463 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
|
adamc@119
|
464 ============================
|
adamc@119
|
465 (a0,
|
adamc@119
|
466 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
|
adamc@119
|
467 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
|
adamc@119
|
468 match pf in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
469 | refl_equal =>
|
adamc@119
|
470 (a0,
|
adamc@119
|
471 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
472 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
|
adamc@119
|
473 end
|
adamc@119
|
474 ]]
|
adamc@119
|
475
|
adamc@119
|
476 Now we can rewrite using the inductive hypothesis. *)
|
adamc@119
|
477
|
adamc@119
|
478 rewrite (IHls1 _ _ pf').
|
adamc@119
|
479 (** [[
|
adamc@119
|
480 ============================
|
adamc@119
|
481 (a0,
|
adamc@119
|
482 match pf' in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
483 | refl_equal =>
|
adamc@119
|
484 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
485 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
|
adamc@119
|
486 end) =
|
adamc@119
|
487 match pf in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
488 | refl_equal =>
|
adamc@119
|
489 (a0,
|
adamc@119
|
490 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
|
adamc@119
|
491 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
|
adamc@119
|
492 end
|
adamc@119
|
493 ]]
|
adamc@119
|
494
|
adam@364
|
495 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 %\textit{%#<i>#does not matter what the result of the call is#</i>#%}%. 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
|
496
|
adamc@119
|
497 generalize (fhapp (fhapp b hls2) hls3).
|
adamc@119
|
498 (** [[
|
adamc@119
|
499 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
|
adamc@119
|
500 (a0,
|
adamc@119
|
501 match pf' in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
502 | refl_equal => f
|
adamc@119
|
503 end) =
|
adamc@119
|
504 match pf in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
505 | refl_equal => (a0, f)
|
adamc@119
|
506 end
|
adamc@119
|
507 ]]
|
adamc@119
|
508
|
adamc@119
|
509 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
|
510
|
adamc@119
|
511 In this case, it is helpful to generalize over our two proofs as well. *)
|
adamc@119
|
512
|
adamc@119
|
513 generalize pf pf'.
|
adamc@119
|
514 (** [[
|
adamc@119
|
515 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
|
adamc@119
|
516 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
|
adamc@119
|
517 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
|
adamc@119
|
518 (a0,
|
adamc@119
|
519 match pf'0 in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
520 | refl_equal => f
|
adamc@119
|
521 end) =
|
adamc@119
|
522 match pf0 in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
523 | refl_equal => (a0, f)
|
adamc@119
|
524 end
|
adamc@119
|
525 ]]
|
adamc@119
|
526
|
adamc@119
|
527 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
|
528
|
adamc@119
|
529 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and %\textit{%#<i>#may be rewritten as well#</i>#%}%. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *)
|
adamc@119
|
530
|
adamc@119
|
531 rewrite app_ass.
|
adamc@119
|
532 (** [[
|
adamc@119
|
533 ============================
|
adamc@119
|
534 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
|
adamc@119
|
535 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
|
adamc@119
|
536 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
|
adamc@119
|
537 (a0,
|
adamc@119
|
538 match pf'0 in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
539 | refl_equal => f
|
adamc@119
|
540 end) =
|
adamc@119
|
541 match pf0 in (_ = ls) return (fhlist B ls) with
|
adamc@119
|
542 | refl_equal => (a0, f)
|
adamc@119
|
543 end
|
adamc@119
|
544 ]]
|
adamc@119
|
545
|
adamc@119
|
546 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
|
547
|
adamc@119
|
548 intros.
|
adamc@119
|
549 rewrite (UIP_refl _ _ pf0).
|
adamc@119
|
550 rewrite (UIP_refl _ _ pf'0).
|
adamc@119
|
551 reflexivity.
|
adamc@119
|
552 Qed.
|
adamc@124
|
553 (* end thide *)
|
adamc@119
|
554 End fhapp.
|
adamc@120
|
555
|
adamc@120
|
556 Implicit Arguments fhapp [A B ls1 ls2].
|
adamc@120
|
557
|
adam@364
|
558 (** 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
|
559
|
adamc@120
|
560
|
adamc@120
|
561 (** * Heterogeneous Equality *)
|
adamc@120
|
562
|
adam@364
|
563 (** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing %\index{heterogeneous equality}\textit{%#<i>#heterogeneous equality#</i>#%}%. *)
|
adamc@120
|
564
|
adamc@120
|
565 Print JMeq.
|
adamc@218
|
566 (** %\vspace{-.15in}% [[
|
adamc@120
|
567 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
|
adamc@120
|
568 JMeq_refl : JMeq x x
|
adamc@120
|
569 ]]
|
adamc@120
|
570
|
adam@364
|
571 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. [JMeq] starts out looking a lot like [eq]. The crucial difference is that we may use [JMeq] %\textit{%#<i>#on arguments of different types#</i>#%}%. 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
|
572
|
adamc@120
|
573 Infix "==" := JMeq (at level 70, no associativity).
|
adamc@120
|
574
|
adamc@124
|
575 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
|
adamc@124
|
576 (* begin thide *)
|
adamc@121
|
577 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
|
adamc@120
|
578 match pf return (pf == refl_equal _) with
|
adamc@120
|
579 | refl_equal => JMeq_refl _
|
adamc@120
|
580 end.
|
adamc@124
|
581 (* end thide *)
|
adamc@120
|
582
|
adamc@120
|
583 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
|
adamc@120
|
584
|
adamc@271
|
585 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
|
586
|
adamc@120
|
587 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
|
adamc@120
|
588 O = match pf with refl_equal => O end.
|
adamc@124
|
589 (* begin thide *)
|
adamc@121
|
590 intros; rewrite (UIP_refl' pf); reflexivity.
|
adamc@120
|
591 Qed.
|
adamc@124
|
592 (* end thide *)
|
adamc@120
|
593
|
adamc@120
|
594 (** 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
|
595
|
adamc@120
|
596 Check JMeq_eq.
|
adamc@218
|
597 (** %\vspace{-.15in}% [[
|
adamc@120
|
598 JMeq_eq
|
adamc@120
|
599 : forall (A : Type) (x y : A), x == y -> x = y
|
adamc@218
|
600 ]]
|
adamc@120
|
601
|
adamc@218
|
602 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
|
603
|
adamc@120
|
604 We can redo our [fhapp] associativity proof based around [JMeq]. *)
|
adamc@120
|
605
|
adamc@120
|
606 Section fhapp'.
|
adamc@120
|
607 Variable A : Type.
|
adamc@120
|
608 Variable B : A -> Type.
|
adamc@120
|
609
|
adamc@120
|
610 (** This time, the naive theorem statement type-checks. *)
|
adamc@120
|
611
|
adamc@124
|
612 (* EX: Prove [fhapp] associativity using [JMeq]. *)
|
adamc@124
|
613
|
adamc@124
|
614 (* begin thide *)
|
adam@364
|
615 Theorem fhapp_ass' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
|
adam@364
|
616 (hls3 : fhlist B ls3),
|
adamc@120
|
617 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
|
adamc@120
|
618 induction ls1; crush.
|
adamc@120
|
619
|
adamc@120
|
620 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
|
adamc@120
|
621 [[
|
adamc@120
|
622 ============================
|
adam@297
|
623 (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
|
adamc@120
|
624 ]]
|
adamc@120
|
625
|
adam@297
|
626 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
|
627 [[
|
adamc@120
|
628 rewrite IHls1.
|
adam@364
|
629 ]]
|
adamc@120
|
630
|
adam@364
|
631 <<
|
adamc@120
|
632 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
|
adamc@120
|
633 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
|
adam@364
|
634 >>
|
adamc@120
|
635
|
adam@297
|
636 Coq 8.3 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
|
637
|
adamc@120
|
638 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
|
639
|
adamc@120
|
640 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
|
641
|
adamc@120
|
642 generalize (fhapp b (fhapp hls2 hls3))
|
adamc@120
|
643 (fhapp (fhapp b hls2) hls3)
|
adamc@120
|
644 (IHls1 _ _ b hls2 hls3).
|
adam@364
|
645 (** %\vspace{-.15in}%[[
|
adamc@120
|
646 ============================
|
adamc@120
|
647 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
|
adamc@120
|
648 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
|
adamc@120
|
649 ]]
|
adamc@120
|
650
|
adamc@120
|
651 Now we can rewrite with append associativity, as before. *)
|
adamc@120
|
652
|
adamc@120
|
653 rewrite app_ass.
|
adam@364
|
654 (** %\vspace{-.15in}%[[
|
adamc@120
|
655 ============================
|
adamc@120
|
656 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
|
adamc@120
|
657 ]]
|
adamc@120
|
658
|
adamc@120
|
659 From this point, the goal is trivial. *)
|
adamc@120
|
660
|
adamc@120
|
661 intros f f0 H; rewrite H; reflexivity.
|
adamc@120
|
662 Qed.
|
adamc@124
|
663 (* end thide *)
|
adamc@120
|
664 End fhapp'.
|
adamc@121
|
665
|
adam@364
|
666 (** 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@364
|
667
|
adamc@121
|
668
|
adamc@121
|
669 (** * Equivalence of Equality Axioms *)
|
adamc@121
|
670
|
adamc@124
|
671 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
|
adamc@124
|
672
|
adamc@124
|
673 (* begin thide *)
|
adamc@272
|
674 (** 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
|
675
|
adamc@121
|
676 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
|
677
|
adamc@121
|
678 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
|
adamc@121
|
679 intros; rewrite (UIP_refl' pf); reflexivity.
|
adamc@121
|
680 Qed.
|
adamc@121
|
681
|
adamc@121
|
682 (** 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
|
683
|
adamc@121
|
684 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
|
adamc@121
|
685 exists pf : B = A, x = match pf with refl_equal => y end.
|
adamc@121
|
686
|
adamc@121
|
687 Infix "===" := JMeq' (at level 70, no associativity).
|
adamc@121
|
688
|
adamc@121
|
689 (** 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
|
690
|
adamc@121
|
691 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
|
adamc@121
|
692
|
adamc@121
|
693 (** remove printing exists *)
|
adamc@121
|
694 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
|
adamc@121
|
695 intros; unfold JMeq'; exists (refl_equal A); reflexivity.
|
adamc@121
|
696 Qed.
|
adamc@121
|
697
|
adamc@121
|
698 (** printing exists $\exists$ *)
|
adamc@121
|
699
|
adamc@121
|
700 (** 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
|
701
|
adamc@121
|
702 Theorem JMeq_eq' : forall (A : Type) (x y : A),
|
adamc@121
|
703 x === y -> x = y.
|
adamc@121
|
704 unfold JMeq'; intros.
|
adamc@121
|
705 (** [[
|
adamc@121
|
706 H : exists pf : A = A,
|
adamc@121
|
707 x = match pf in (_ = T) return T with
|
adamc@121
|
708 | refl_equal => y
|
adamc@121
|
709 end
|
adamc@121
|
710 ============================
|
adamc@121
|
711 x = y
|
adam@302
|
712 ]]
|
adam@302
|
713 *)
|
adamc@121
|
714
|
adamc@121
|
715 destruct H.
|
adamc@121
|
716 (** [[
|
adamc@121
|
717 x0 : A = A
|
adamc@121
|
718 H : x = match x0 in (_ = T) return T with
|
adamc@121
|
719 | refl_equal => y
|
adamc@121
|
720 end
|
adamc@121
|
721 ============================
|
adamc@121
|
722 x = y
|
adam@302
|
723 ]]
|
adam@302
|
724 *)
|
adamc@121
|
725
|
adamc@121
|
726 rewrite H.
|
adamc@121
|
727 (** [[
|
adamc@121
|
728 x0 : A = A
|
adamc@121
|
729 ============================
|
adamc@121
|
730 match x0 in (_ = T) return T with
|
adamc@121
|
731 | refl_equal => y
|
adamc@121
|
732 end = y
|
adam@302
|
733 ]]
|
adam@302
|
734 *)
|
adamc@121
|
735
|
adamc@121
|
736 rewrite (UIP_refl _ _ x0); reflexivity.
|
adamc@121
|
737 Qed.
|
adamc@121
|
738
|
adam@364
|
739 (** 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
|
740
|
adamc@124
|
741 (* end thide *)
|
adamc@123
|
742
|
adamc@123
|
743
|
adamc@123
|
744 (** * Equality of Functions *)
|
adamc@123
|
745
|
adamc@123
|
746 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
|
adamc@123
|
747 Theorem S_eta : S = (fun n => S n).
|
adamc@205
|
748 ]]
|
adamc@205
|
749
|
adam@364
|
750 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}\textit{%#<i>#extensional#</i>#%}%. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *)
|
adamc@123
|
751
|
adamc@124
|
752 (* begin thide *)
|
adamc@123
|
753 Axiom ext_eq : forall A B (f g : A -> B),
|
adamc@123
|
754 (forall x, f x = g x)
|
adamc@123
|
755 -> f = g.
|
adamc@124
|
756 (* end thide *)
|
adamc@123
|
757
|
adamc@123
|
758 (** 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
|
759
|
adamc@123
|
760 Theorem S_eta : S = (fun n => S n).
|
adamc@124
|
761 (* begin thide *)
|
adamc@123
|
762 apply ext_eq; reflexivity.
|
adamc@123
|
763 Qed.
|
adamc@124
|
764 (* end thide *)
|
adamc@123
|
765
|
adam@292
|
766 (** The same axiom can help us prove equality of types, where we need to %``%#"#reason under quantifiers.#"#%''% *)
|
adamc@123
|
767
|
adamc@123
|
768 Theorem forall_eq : (forall x : nat, match x with
|
adamc@123
|
769 | O => True
|
adamc@123
|
770 | S _ => True
|
adamc@123
|
771 end)
|
adamc@123
|
772 = (forall _ : nat, True).
|
adamc@123
|
773
|
adam@364
|
774 (** There are no immediate opportunities to apply [ext_eq], but we can use %\index{tactics!change}%[change] to fix that. *)
|
adamc@123
|
775
|
adamc@124
|
776 (* begin thide *)
|
adamc@123
|
777 change ((forall x : nat, (fun x => match x with
|
adamc@123
|
778 | 0 => True
|
adamc@123
|
779 | S _ => True
|
adamc@123
|
780 end) x) = (nat -> True)).
|
adamc@123
|
781 rewrite (ext_eq (fun x => match x with
|
adamc@123
|
782 | 0 => True
|
adamc@123
|
783 | S _ => True
|
adamc@123
|
784 end) (fun _ => True)).
|
adamc@123
|
785 (** [[
|
adamc@123
|
786 2 subgoals
|
adamc@123
|
787
|
adamc@123
|
788 ============================
|
adamc@123
|
789 (nat -> True) = (nat -> True)
|
adamc@123
|
790
|
adamc@123
|
791 subgoal 2 is:
|
adamc@123
|
792 forall x : nat, match x with
|
adamc@123
|
793 | 0 => True
|
adamc@123
|
794 | S _ => True
|
adamc@123
|
795 end = True
|
adam@302
|
796 ]]
|
adam@302
|
797 *)
|
adamc@123
|
798
|
adamc@123
|
799 reflexivity.
|
adamc@123
|
800
|
adamc@123
|
801 destruct x; constructor.
|
adamc@123
|
802 Qed.
|
adamc@124
|
803 (* end thide *)
|
adamc@127
|
804
|
adam@364
|
805 (** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of %\index{functional extensionality}\emph{%#<i>#functional extensionality#</i>#%}% 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. *)
|
adam@364
|
806
|
adamc@127
|
807
|
adamc@127
|
808 (** * Exercises *)
|
adamc@127
|
809
|
adamc@127
|
810 (** %\begin{enumerate}%#<ol>#
|
adamc@127
|
811
|
adam@364
|
812 %\item%#<li># Implement and prove correct a substitution function for simply typed lambda calculus. In particular:
|
adamc@127
|
813 %\begin{enumerate}%#<ol>#
|
adamc@127
|
814 %\item%#<li># Define a datatype [type] of lambda types, including just booleans and function types.#</li>#
|
adamc@127
|
815 %\item%#<li># Define a type family [exp : list type -> type -> Type] of lambda expressions, including boolean constants, variables, and function application and abstraction.#</li>#
|
adamc@127
|
816 %\item%#<li># Implement a definitional interpreter for [exp]s, by way of a recursive function over expressions and substitutions for free variables, like in the related example from the last chapter.#</li>#
|
adam@292
|
817 %\item%#<li># Implement a function [subst : forall t' ts t, exp (t' :: ts) t -> exp ts t' -> exp ts t]. The type of the first expression indicates that its most recently bound free variable has type [t']. The second expression also has type [t'], and the job of [subst] is to substitute the second expression for every occurrence of the %``%#"#first#"#%''% variable of the first expression.#</li>#
|
adamc@127
|
818 %\item%#<li># Prove that [subst] preserves program meanings. That is, prove
|
adamc@127
|
819 [[
|
adamc@127
|
820 forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts),
|
adamc@127
|
821 expDenote (subst e e') s = expDenote e (expDenote e' s ::: s)
|
adamc@127
|
822 ]]
|
adam@292
|
823 where [:::] is an infix operator for heterogeneous %``%#"#cons#"#%''% that is defined in the book's [DepList] module.#</li>#
|
adamc@127
|
824 #</ol>#%\end{enumerate}%
|
adamc@127
|
825 The material presented up to this point should be sufficient to enable a good solution of this exercise, with enough ingenuity. If you get stuck, it may be helpful to use the following structure. None of these elements need to appear in your solution, but we can at least guarantee that there is a reasonable solution based on them.
|
adamc@127
|
826 %\begin{enumerate}%#<ol>#
|
adamc@127
|
827 %\item%#<li># The [DepList] module will be useful. You can get the standard dependent list definitions there, instead of copying-and-pasting from the last chapter. It is worth reading the source for that module over, since it defines some new helpful functions and notations that we did not use last chapter.#</li>#
|
adam@292
|
828 %\item%#<li># Define a recursive function [liftVar : forall ts1 ts2 t t', member t (ts1 ++ ts2) -> member t (ts1 ++ t' :: ts2)]. This function should %``%#"#lift#"#%''% a de Bruijn variable so that its type refers to a new variable inserted somewhere in the index list.#</li>#
|
adam@292
|
829 %\item%#<li># Define a recursive function [lift' : forall ts t (e : exp ts t) ts1 ts2 t', ts = ts1 ++ ts2 -> exp (ts1 ++ t' :: ts2) t] which performs a similar lifting on an [exp]. The convoluted type is to get around restrictions on [match] annotations. We delay %``%#"#realizing#"#%''% that the first index of [e] is built with list concatenation until after a dependent [match], and the new explicit proof argument must be used to cast some terms that come up in the [match] body.#</li>#
|
adamc@127
|
830 %\item%#<li># Define a function [lift : forall ts t t', exp ts t -> exp (t' :: ts) t], which handles simpler top-level lifts. This should be an easy one-liner based on [lift'].#</li>#
|
adamc@127
|
831 %\item%#<li># Define a recursive function [substVar : forall ts1 ts2 t t', member t (ts1 ++ t' :: ts2) -> (t' = t) + member t (ts1 ++ ts2)]. This function is the workhorse behind substitution applied to a variable. It returns [inl] to indicate that the variable we pass to it is the variable that we are substituting for, and it returns [inr] to indicate that the variable we are examining is %\textit{%#<i>#not#</i>#%}% the one we are substituting for. In the first case, we get a proof that the necessary typing relationship holds, and, in the second case, we get the original variable modified to reflect the removal of the substitutee from the typing context.#</li>#
|
adamc@127
|
832 %\item%#<li># Define a recursive function [subst' : forall ts t (e : exp ts t) ts1 t' ts2, ts = ts1 ++ t' :: ts2 -> exp (ts1 ++ ts2) t' -> exp (ts1 ++ ts2) t]. This is the workhorse of substitution in expressions, employing the same proof-passing trick as for [lift']. You will probably want to use [lift] somewhere in the definition of [subst'].#</li>#
|
adamc@127
|
833 %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li>#
|
adamc@127
|
834 %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li>#
|
adam@292
|
835 %\item%#<li># All of the reasoning about equality proofs in these theorems follows a regular pattern. If you have an equality proof that you want to replace with [refl_equal] somehow, run [generalize] on that proof variable. Your goal is to get to the point where you can [rewrite] with the original proof to change the type of the generalized version. To avoid type errors (the infamous %``%#"#second-order unification#"#%''% failure messages), it will be helpful to run [generalize] on other pieces of the proof context that mention the equality's lefthand side. You might also want to use [generalize dependent], which generalizes not just one variable but also all variables whose types depend on it. [generalize dependent] has the sometimes-helpful property of removing from the context all variables that it generalizes. Once you do manage the mind-bending trick of using the equality proof to rewrite its own type, you will be able to rewrite with [UIP_refl].#</li>#
|
adam@364
|
836 %\item%#<li># The [ext_eq] axiom from the end of this chapter is available in the Coq standard library as [functional_extensionality] in module [FunctionalExtensionality], and you will probably want to use it in the [lift'] and [subst'] correctness proofs.#</li>#
|
adam@292
|
837 %\item%#<li># The [change] tactic should come in handy in the proofs about [lift] and [subst], where you want to introduce %``%#"#extraneous#"#%''% list concatenations with [nil] to match the forms of earlier theorems.#</li>#
|
adam@292
|
838 %\item%#<li># Be careful about [destruct]ing a term %``%#"#too early.#"#%''% You can use [generalize] on proof terms to bring into the proof context any important propositions about the term. Then, when you [destruct] the term, it is updated in the extra propositions, too. The [case_eq] tactic is another alternative to this approach, based on saving an equality between the original term and its new form.#</li>#
|
adamc@127
|
839 #</ol>#%\end{enumerate}%
|
adamc@127
|
840 #</li>#
|
adamc@127
|
841
|
adamc@127
|
842 #</ol>#%\end{enumerate}% *)
|