Mercurial > cpdt > repo
comparison src/Equality.v @ 218:c8508d277a00
Ported Equality
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 11 Nov 2009 15:12:40 -0500 |
parents | f05514cc6c0d |
children | aa3c054afce0 |
comparison
equal
deleted
inserted
replaced
217:6601384e7e14 | 218:c8508d277a00 |
---|---|
32 | O => O | 32 | O => O |
33 | S n' => let y := n' in y | 33 | S n' => let y := n' in y |
34 end. | 34 end. |
35 | 35 |
36 Theorem reduce_me : pred' 1 = 0. | 36 Theorem reduce_me : pred' 1 = 0. |
37 | |
37 (* begin thide *) | 38 (* begin thide *) |
38 (** 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 that encodes terms canonically. | 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 that encodes terms canonically. |
39 | 40 |
40 The 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 [lazy] for call-by-need reduction. *) | 41 The 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 [lazy] for call-by-need reduction. *) |
41 | 42 |
42 cbv delta. | 43 cbv delta. |
43 (** [[ | 44 (** [[ |
44 | |
45 ============================ | 45 ============================ |
46 (fun x : nat => match x with | 46 (fun x : nat => match x with |
47 | 0 => 0 | 47 | 0 => 0 |
48 | S n' => let y := n' in y | 48 | S n' => let y := n' in y |
49 end) 1 = 0 | 49 end) 1 = 0 |
50 | |
50 ]] | 51 ]] |
51 | 52 |
52 At this point, we want to apply the famous beta reduction of lambda calculus, to simplify the application of a known function abstraction. *) | 53 At this point, we want to apply the famous beta reduction of lambda calculus, to simplify the application of a known function abstraction. *) |
53 | 54 |
54 cbv beta. | 55 cbv beta. |
55 (** [[ | 56 (** [[ |
56 | |
57 ============================ | 57 ============================ |
58 match 1 with | 58 match 1 with |
59 | 0 => 0 | 59 | 0 => 0 |
60 | S n' => let y := n' in y | 60 | S n' => let y := n' in y |
61 end = 0 | 61 end = 0 |
62 | |
62 ]] | 63 ]] |
63 | 64 |
64 Next on the list is the iota reduction, which simplifies a single [match] term by determining which pattern matches. *) | 65 Next on the list is the iota reduction, which simplifies a single [match] term by determining which pattern matches. *) |
65 | 66 |
66 cbv iota. | 67 cbv iota. |
67 (** [[ | 68 (** [[ |
68 | |
69 ============================ | 69 ============================ |
70 (fun n' : nat => let y := n' in y) 0 = 0 | 70 (fun n' : nat => let y := n' in y) 0 = 0 |
71 | |
71 ]] | 72 ]] |
72 | 73 |
73 Now we need another beta reduction. *) | 74 Now we need another beta reduction. *) |
74 | 75 |
75 cbv beta. | 76 cbv beta. |
76 (** [[ | 77 (** [[ |
77 | |
78 ============================ | 78 ============================ |
79 (let y := 0 in y) = 0 | 79 (let y := 0 in y) = 0 |
80 | |
80 ]] | 81 ]] |
81 | 82 |
82 The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *) | 83 The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *) |
83 | 84 |
84 cbv zeta. | 85 cbv zeta. |
85 (** [[ | 86 (** [[ |
86 | |
87 ============================ | 87 ============================ |
88 0 = 0 | 88 0 = 0 |
89 | |
89 ]] *) | 90 ]] *) |
90 | 91 |
91 reflexivity. | 92 reflexivity. |
92 Qed. | 93 Qed. |
93 (* end thide *) | 94 (* end thide *) |
97 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, we will introduce effective proof methods for goals that use proofs of the standard propositional equality "as data." *) | 98 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, we will introduce effective proof methods for goals that use proofs of the standard propositional equality "as data." *) |
98 | 99 |
99 | 100 |
100 (** * Heterogeneous Lists Revisited *) | 101 (** * Heterogeneous Lists Revisited *) |
101 | 102 |
102 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. *) | 103 (** 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. *) |
103 | 104 |
104 Section fhlist. | 105 Section fhlist. |
105 Variable A : Type. | 106 Variable A : Type. |
106 Variable B : A -> Type. | 107 Variable B : A -> Type. |
107 | 108 |
159 induction ls; crush. | 160 induction ls; crush. |
160 | 161 |
161 (** Part of our single remaining subgoal is: | 162 (** Part of our single remaining subgoal is: |
162 | 163 |
163 [[ | 164 [[ |
164 | |
165 a0 : a = elm | 165 a0 : a = elm |
166 ============================ | 166 ============================ |
167 match a0 in (_ = a2) return (C a2) with | 167 match a0 in (_ = a2) return (C a2) with |
168 | refl_equal => f a1 | 168 | refl_equal => f a1 |
169 end = f match a0 in (_ = a2) return (B a2) with | 169 end = f match a0 in (_ = a2) return (B a2) with |
170 | refl_equal => a1 | 170 | refl_equal => a1 |
171 end | 171 end |
172 | |
172 ]] | 173 ]] |
173 | 174 |
174 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. | 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. |
175 | 176 |
176 [[ | 177 [[ |
177 | |
178 destruct a0. | 178 destruct a0. |
179 | 179 |
180 ]] | 180 User error: Cannot solve a second-order unification problem |
181 | |
182 ]] | |
183 | |
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. | |
181 | 185 |
182 [[ | 186 [[ |
183 User error: Cannot solve a second-order unification problem | |
184 ]] | |
185 | |
186 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. | |
187 | |
188 [[ | |
189 | |
190 assert (a0 = refl_equal _). | 187 assert (a0 = refl_equal _). |
191 | 188 |
192 ]] | |
193 | |
194 [[ | |
195 The term "refl_equal ?98" has type "?98 = ?98" | 189 The term "refl_equal ?98" has type "?98 = ?98" |
196 while it is expected to have type "a = elm" | 190 while it is expected to have type "a = elm" |
191 | |
197 ]] | 192 ]] |
198 | 193 |
199 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! | 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! |
200 | 195 |
201 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. | 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. |
202 | 197 |
203 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. *) | 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. *) |
204 | 199 |
205 case a0. | 200 case a0. |
206 (** [[ | 201 (** [[ |
207 | |
208 ============================ | 202 ============================ |
209 f a1 = f a1 | 203 f a1 = f a1 |
204 | |
210 ]] | 205 ]] |
211 | 206 |
212 It seems that [destruct] was trying to be too smart for its own good. *) | 207 It seems that [destruct] was trying to be too smart for its own good. *) |
213 | 208 |
214 reflexivity. | 209 reflexivity. |
224 (* end thide *) | 219 (* end thide *) |
225 | 220 |
226 (** [simple destruct pf] is a convenient form for applying [case]. It runs [intro] to bring into scope all quantified variables up to its argument. *) | 221 (** [simple destruct pf] is a convenient form for applying [case]. It runs [intro] to bring into scope all quantified variables up to its argument. *) |
227 | 222 |
228 Print lemma1. | 223 Print lemma1. |
229 | 224 (** %\vspace{-.15in}% [[ |
230 (** [[ | |
231 | |
232 lemma1 = | 225 lemma1 = |
233 fun (x : A) (pf : x = elm) => | 226 fun (x : A) (pf : x = elm) => |
234 match pf as e in (_ = y) return (0 = match e with | 227 match pf as e in (_ = y) return (0 = match e with |
235 | refl_equal => 0 | 228 | refl_equal => 0 |
236 end) with | 229 end) with |
237 | refl_equal => refl_equal 0 | 230 | refl_equal => refl_equal 0 |
238 end | 231 end |
239 : forall (x : A) (pf : x = elm), 0 = match pf with | 232 : forall (x : A) (pf : x = elm), 0 = match pf with |
240 | refl_equal => 0 | 233 | refl_equal => 0 |
241 end | 234 end |
235 | |
242 ]] | 236 ]] |
243 | 237 |
244 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *) | 238 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *) |
245 | 239 |
246 (* begin thide *) | 240 (* begin thide *) |
256 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *) | 250 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *) |
257 | 251 |
258 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end. | 252 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end. |
259 (* begin thide *) | 253 (* begin thide *) |
260 (** [[ | 254 (** [[ |
261 | |
262 simple destruct pf. | 255 simple destruct pf. |
263 | 256 |
264 ]] | |
265 | |
266 [[ | |
267 | |
268 User error: Cannot solve a second-order unification problem | 257 User error: Cannot solve a second-order unification problem |
258 | |
269 ]] *) | 259 ]] *) |
270 Abort. | 260 Abort. |
271 | 261 |
272 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *) | 262 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *) |
273 | 263 |
284 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *) | 274 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *) |
285 | 275 |
286 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. | 276 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. |
287 (* begin thide *) | 277 (* begin thide *) |
288 (** [[ | 278 (** [[ |
289 | |
290 simple destruct pf. | 279 simple destruct pf. |
291 | |
292 ]] | |
293 | |
294 [[ | |
295 | 280 |
296 User error: Cannot solve a second-order unification problem | 281 User error: Cannot solve a second-order unification problem |
297 ]] *) | 282 ]] *) |
283 | |
298 Abort. | 284 Abort. |
299 | 285 |
300 (** This time, even our manual attempt fails. | 286 (** This time, even our manual attempt fails. |
301 | 287 |
302 [[ | 288 [[ |
303 | |
304 Definition lemma3' := | 289 Definition lemma3' := |
305 fun (x : A) (pf : x = x) => | 290 fun (x : A) (pf : x = x) => |
306 match pf as pf' in (_ = x') return (pf' = refl_equal x') with | 291 match pf as pf' in (_ = x') return (pf' = refl_equal x') with |
307 | refl_equal => refl_equal _ | 292 | refl_equal => refl_equal _ |
308 end. | 293 end. |
309 | 294 |
310 ]] | |
311 | |
312 [[ | |
313 | |
314 The term "refl_equal x'" has type "x' = x'" while it is expected to have type | 295 The term "refl_equal x'" has type "x' = x'" while it is expected to have type |
315 "x = x'" | 296 "x = x'" |
297 | |
316 ]] | 298 ]] |
317 | 299 |
318 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], refering 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. | 300 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], refering 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. |
319 | 301 |
320 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *) | 302 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *) |
322 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. | 304 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. |
323 intros; apply UIP_refl. | 305 intros; apply UIP_refl. |
324 Qed. | 306 Qed. |
325 | 307 |
326 Check UIP_refl. | 308 Check UIP_refl. |
327 (** [[ | 309 (** %\vspace{-.15in}% [[ |
328 | |
329 UIP_refl | 310 UIP_refl |
330 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x | 311 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x |
312 | |
331 ]] | 313 ]] |
332 | 314 |
333 [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>#%}%. *) | 315 [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>#%}%. *) |
334 | 316 |
335 Print eq_rect_eq. | 317 Print eq_rect_eq. |
336 (** [[ | 318 (** %\vspace{-.15in}% [[ |
337 | |
338 eq_rect_eq = | 319 eq_rect_eq = |
339 fun U : Type => Eq_rect_eq.eq_rect_eq U | 320 fun U : Type => Eq_rect_eq.eq_rect_eq U |
340 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), | 321 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), |
341 x = eq_rect p Q x p h | 322 x = eq_rect p Q x p h |
323 | |
342 ]] | 324 ]] |
343 | 325 |
344 [eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. [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]. [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. | 326 [eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. [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]. [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. |
345 | 327 |
346 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an 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. | 328 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an 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. |
347 | 329 |
348 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *) | 330 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *) |
349 | 331 |
350 Print Streicher_K. | 332 Print Streicher_K. |
351 (* end thide *) | 333 (* end thide *) |
352 (** [[ | 334 (** %\vspace{-.15in}% [[ |
353 | |
354 Streicher_K = | 335 Streicher_K = |
355 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U) | 336 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U) |
356 : forall (U : Type) (x : U) (P : x = x -> Prop), | 337 : forall (U : Type) (x : U) (P : x = x -> Prop), |
357 P (refl_equal x) -> forall p : x = x, P p | 338 P (refl_equal x) -> forall p : x = x, P p |
339 | |
358 ]] | 340 ]] |
359 | 341 |
360 This is the unfortunately-named "Streicher's axiom K," which says that a predicate on properly-typed equality proofs holds of all such proofs if it holds of reflexivity. *) | 342 This is the unfortunately-named "Streicher's axiom K," which says that a predicate on properly-typed equality proofs holds of all such proofs if it holds of reflexivity. *) |
361 | 343 |
362 End fhlist_map. | 344 End fhlist_map. |
368 | 350 |
369 Section fhapp. | 351 Section fhapp. |
370 Variable A : Type. | 352 Variable A : Type. |
371 Variable B : A -> Type. | 353 Variable B : A -> Type. |
372 | 354 |
373 Fixpoint fhapp (ls1 ls2 : list A) {struct ls1} | 355 Fixpoint fhapp (ls1 ls2 : list A) |
374 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) := | 356 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) := |
375 match ls1 return fhlist _ ls1 -> _ -> fhlist _ (ls1 ++ ls2) with | 357 match ls1 with |
376 | nil => fun _ hls2 => hls2 | 358 | nil => fun _ hls2 => hls2 |
377 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2) | 359 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2) |
378 end. | 360 end. |
379 | 361 |
380 Implicit Arguments fhapp [ls1 ls2]. | 362 Implicit Arguments fhapp [ls1 ls2]. |
383 (* begin thide *) | 365 (* begin thide *) |
384 | 366 |
385 (** We might like to prove that [fhapp] is associative. | 367 (** We might like to prove that [fhapp] is associative. |
386 | 368 |
387 [[ | 369 [[ |
388 | |
389 Theorem fhapp_ass : forall ls1 ls2 ls3 | 370 Theorem fhapp_ass : forall ls1 ls2 ls3 |
390 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3), | 371 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3), |
391 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3. | 372 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3. |
392 | |
393 ]] | |
394 | |
395 [[ | |
396 | 373 |
397 The term | 374 The term |
398 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2) | 375 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2) |
399 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)" | 376 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)" |
400 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)" | 377 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)" |
378 | |
401 ]] | 379 ]] |
402 | 380 |
403 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 %\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. *) | 381 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 %\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. *) |
404 | 382 |
405 Theorem fhapp_ass : forall ls1 ls2 ls3 | 383 Theorem fhapp_ass : forall ls1 ls2 ls3 |
412 induction ls1; crush. | 390 induction ls1; crush. |
413 | 391 |
414 (** The first remaining subgoal looks trivial enough: | 392 (** The first remaining subgoal looks trivial enough: |
415 | 393 |
416 [[ | 394 [[ |
417 | |
418 ============================ | 395 ============================ |
419 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 = | 396 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 = |
420 match pf in (_ = ls) return (fhlist B ls) with | 397 match pf in (_ = ls) return (fhlist B ls) with |
421 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 | 398 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 |
422 end | 399 end |
400 | |
423 ]] | 401 ]] |
424 | 402 |
425 We can try what worked in previous examples. | 403 We can try what worked in previous examples. |
426 | 404 |
427 [[ | 405 [[ |
428 case pf. | 406 case pf. |
429 | 407 |
430 ]] | |
431 | |
432 [[ | |
433 | |
434 User error: Cannot solve a second-order unification problem | 408 User error: Cannot solve a second-order unification problem |
409 | |
435 ]] | 410 ]] |
436 | 411 |
437 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. *) | 412 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. *) |
438 | 413 |
439 rewrite (UIP_refl _ _ pf). | 414 rewrite (UIP_refl _ _ pf). |
440 (** [[ | 415 (** [[ |
441 | |
442 ============================ | 416 ============================ |
443 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 = | 417 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 = |
444 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 | 418 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 |
419 | |
445 ]] *) | 420 ]] *) |
446 | 421 |
447 reflexivity. | 422 reflexivity. |
448 | 423 |
449 (** Our second subgoal is trickier. | 424 (** Our second subgoal is trickier. |
450 | 425 |
451 [[ | 426 [[ |
452 | |
453 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3 | 427 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3 |
454 ============================ | 428 ============================ |
455 (a0, | 429 (a0, |
456 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b | 430 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b |
457 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) = | 431 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) = |
459 | refl_equal => | 433 | refl_equal => |
460 (a0, | 434 (a0, |
461 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) | 435 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) |
462 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) | 436 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) |
463 end | 437 end |
464 ]] | |
465 | |
466 | |
467 [[ | |
468 | 438 |
469 rewrite (UIP_refl _ _ pf). | 439 rewrite (UIP_refl _ _ pf). |
470 | 440 |
471 ]] | |
472 | |
473 [[ | |
474 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3" | 441 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3" |
475 while it is expected to have type "?556 = ?556" | 442 while it is expected to have type "?556 = ?556" |
443 | |
476 ]] | 444 ]] |
477 | 445 |
478 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. *) | 446 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. *) |
479 | 447 |
480 injection pf; intro pf'. | 448 injection pf; intro pf'. |
481 (** [[ | 449 (** [[ |
482 | |
483 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3 | 450 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3 |
484 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3 | 451 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3 |
485 ============================ | 452 ============================ |
486 (a0, | 453 (a0, |
487 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b | 454 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b |
490 | refl_equal => | 457 | refl_equal => |
491 (a0, | 458 (a0, |
492 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) | 459 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) |
493 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) | 460 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) |
494 end | 461 end |
462 | |
495 ]] | 463 ]] |
496 | 464 |
497 Now we can rewrite using the inductive hypothesis. *) | 465 Now we can rewrite using the inductive hypothesis. *) |
498 | 466 |
499 rewrite (IHls1 _ _ pf'). | 467 rewrite (IHls1 _ _ pf'). |
500 (** [[ | 468 (** [[ |
501 | |
502 ============================ | 469 ============================ |
503 (a0, | 470 (a0, |
504 match pf' in (_ = ls) return (fhlist B ls) with | 471 match pf' in (_ = ls) return (fhlist B ls) with |
505 | refl_equal => | 472 | refl_equal => |
506 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) | 473 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) |
510 | refl_equal => | 477 | refl_equal => |
511 (a0, | 478 (a0, |
512 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) | 479 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) |
513 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) | 480 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) |
514 end | 481 end |
482 | |
515 ]] | 483 ]] |
516 | 484 |
517 We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion. 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 [generalize] tactic helps us do exactly that. *) | 485 We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion. 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 [generalize] tactic helps us do exactly that. *) |
518 | 486 |
519 generalize (fhapp (fhapp b hls2) hls3). | 487 generalize (fhapp (fhapp b hls2) hls3). |
520 (** [[ | 488 (** [[ |
521 | |
522 forall f : fhlist B ((ls1 ++ ls2) ++ ls3), | 489 forall f : fhlist B ((ls1 ++ ls2) ++ ls3), |
523 (a0, | 490 (a0, |
524 match pf' in (_ = ls) return (fhlist B ls) with | 491 match pf' in (_ = ls) return (fhlist B ls) with |
525 | refl_equal => f | 492 | refl_equal => f |
526 end) = | 493 end) = |
527 match pf in (_ = ls) return (fhlist B ls) with | 494 match pf in (_ = ls) return (fhlist B ls) with |
528 | refl_equal => (a0, f) | 495 | refl_equal => (a0, f) |
529 end | 496 end |
497 | |
530 ]] | 498 ]] |
531 | 499 |
532 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. | 500 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. |
533 | 501 |
534 In this case, it is helpful to generalize over our two proofs as well. *) | 502 In this case, it is helpful to generalize over our two proofs as well. *) |
535 | 503 |
536 generalize pf pf'. | 504 generalize pf pf'. |
537 (** [[ | 505 (** [[ |
538 | |
539 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3) | 506 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3) |
540 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3) | 507 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3) |
541 (f : fhlist B ((ls1 ++ ls2) ++ ls3)), | 508 (f : fhlist B ((ls1 ++ ls2) ++ ls3)), |
542 (a0, | 509 (a0, |
543 match pf'0 in (_ = ls) return (fhlist B ls) with | 510 match pf'0 in (_ = ls) return (fhlist B ls) with |
544 | refl_equal => f | 511 | refl_equal => f |
545 end) = | 512 end) = |
546 match pf0 in (_ = ls) return (fhlist B ls) with | 513 match pf0 in (_ = ls) return (fhlist B ls) with |
547 | refl_equal => (a0, f) | 514 | refl_equal => (a0, f) |
548 end | 515 end |
516 | |
549 ]] | 517 ]] |
550 | 518 |
551 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. | 519 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. |
552 | 520 |
553 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. *) | 521 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. *) |
554 | 522 |
555 rewrite app_ass. | 523 rewrite app_ass. |
556 (** [[ | 524 (** [[ |
557 | |
558 ============================ | 525 ============================ |
559 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3) | 526 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3) |
560 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3) | 527 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3) |
561 (f : fhlist B (ls1 ++ ls2 ++ ls3)), | 528 (f : fhlist B (ls1 ++ ls2 ++ ls3)), |
562 (a0, | 529 (a0, |
564 | refl_equal => f | 531 | refl_equal => f |
565 end) = | 532 end) = |
566 match pf0 in (_ = ls) return (fhlist B ls) with | 533 match pf0 in (_ = ls) return (fhlist B ls) with |
567 | refl_equal => (a0, f) | 534 | refl_equal => (a0, f) |
568 end | 535 end |
536 | |
569 ]] | 537 ]] |
570 | 538 |
571 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]. *) | 539 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]. *) |
572 | 540 |
573 intros. | 541 intros. |
584 (** * Heterogeneous Equality *) | 552 (** * Heterogeneous Equality *) |
585 | 553 |
586 (** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *) | 554 (** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *) |
587 | 555 |
588 Print JMeq. | 556 Print JMeq. |
589 (** [[ | 557 (** %\vspace{-.15in}% [[ |
590 | |
591 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := | 558 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := |
592 JMeq_refl : JMeq x x | 559 JMeq_refl : JMeq x x |
560 | |
593 ]] | 561 ]] |
594 | 562 |
595 [JMeq] stands for "John Major equality," a name coined by Conor McBride 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. *) | 563 [JMeq] stands for "John Major equality," a name coined by Conor McBride 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. *) |
596 | 564 |
597 Infix "==" := JMeq (at level 70, no associativity). | 565 Infix "==" := JMeq (at level 70, no associativity). |
616 (* end thide *) | 584 (* end thide *) |
617 | 585 |
618 (** 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: *) | 586 (** 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: *) |
619 | 587 |
620 Check JMeq_eq. | 588 Check JMeq_eq. |
621 (** [[ | 589 (** %\vspace{-.15in}% [[ |
622 | |
623 JMeq_eq | 590 JMeq_eq |
624 : forall (A : Type) (x y : A), x == y -> x = y | 591 : forall (A : Type) (x y : A), x == y -> x = y |
625 ]] *) | 592 |
626 | 593 ]] |
627 (** 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. | 594 |
595 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. | |
628 | 596 |
629 We can redo our [fhapp] associativity proof based around [JMeq]. *) | 597 We can redo our [fhapp] associativity proof based around [JMeq]. *) |
630 | 598 |
631 Section fhapp'. | 599 Section fhapp'. |
632 Variable A : Type. | 600 Variable A : Type. |
643 induction ls1; crush. | 611 induction ls1; crush. |
644 | 612 |
645 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is: | 613 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is: |
646 | 614 |
647 [[ | 615 [[ |
648 | |
649 ============================ | 616 ============================ |
650 (a0, | 617 (a0, |
651 fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b | 618 fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b |
652 (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) == | 619 (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) == |
653 (a0, | 620 (a0, |
654 fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3) | 621 fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3) |
655 (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3) | 622 (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3) |
623 | |
656 ]] | 624 ]] |
657 | 625 |
658 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. | 626 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. |
659 | 627 |
660 [[ | 628 [[ |
661 | |
662 rewrite IHls1. | 629 rewrite IHls1. |
663 | |
664 ]] | |
665 | |
666 [[ | |
667 | 630 |
668 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with | 631 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with |
669 "fhlist B (ls1 ++ ?1572 ++ ?1573)" | 632 "fhlist B (ls1 ++ ?1572 ++ ?1573)" |
633 | |
670 ]] | 634 ]] |
671 | 635 |
672 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. | 636 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. |
673 | 637 |
674 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]. *) | 638 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]. *) |
675 | 639 |
676 generalize (fhapp b (fhapp hls2 hls3)) | 640 generalize (fhapp b (fhapp hls2 hls3)) |
677 (fhapp (fhapp b hls2) hls3) | 641 (fhapp (fhapp b hls2) hls3) |
678 (IHls1 _ _ b hls2 hls3). | 642 (IHls1 _ _ b hls2 hls3). |
679 (** [[ | 643 (** [[ |
680 | |
681 ============================ | 644 ============================ |
682 forall (f : fhlist B (ls1 ++ ls2 ++ ls3)) | 645 forall (f : fhlist B (ls1 ++ ls2 ++ ls3)) |
683 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0) | 646 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0) |
647 | |
684 ]] | 648 ]] |
685 | 649 |
686 Now we can rewrite with append associativity, as before. *) | 650 Now we can rewrite with append associativity, as before. *) |
687 | 651 |
688 rewrite app_ass. | 652 rewrite app_ass. |
689 (** [[ | 653 (** [[ |
690 | |
691 ============================ | 654 ============================ |
692 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0) | 655 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0) |
656 | |
693 ]] | 657 ]] |
694 | 658 |
695 From this point, the goal is trivial. *) | 659 From this point, the goal is trivial. *) |
696 | 660 |
697 intros f f0 H; rewrite H; reflexivity. | 661 intros f f0 H; rewrite H; reflexivity. |
735 | 699 |
736 Theorem JMeq_eq' : forall (A : Type) (x y : A), | 700 Theorem JMeq_eq' : forall (A : Type) (x y : A), |
737 x === y -> x = y. | 701 x === y -> x = y. |
738 unfold JMeq'; intros. | 702 unfold JMeq'; intros. |
739 (** [[ | 703 (** [[ |
740 | |
741 H : exists pf : A = A, | 704 H : exists pf : A = A, |
742 x = match pf in (_ = T) return T with | 705 x = match pf in (_ = T) return T with |
743 | refl_equal => y | 706 | refl_equal => y |
744 end | 707 end |
745 ============================ | 708 ============================ |
746 x = y | 709 x = y |
710 | |
747 ]] *) | 711 ]] *) |
748 | 712 |
749 destruct H. | 713 destruct H. |
750 (** [[ | 714 (** [[ |
751 | |
752 x0 : A = A | 715 x0 : A = A |
753 H : x = match x0 in (_ = T) return T with | 716 H : x = match x0 in (_ = T) return T with |
754 | refl_equal => y | 717 | refl_equal => y |
755 end | 718 end |
756 ============================ | 719 ============================ |
757 x = y | 720 x = y |
721 | |
758 ]] *) | 722 ]] *) |
759 | 723 |
760 rewrite H. | 724 rewrite H. |
761 (** [[ | 725 (** [[ |
762 | |
763 x0 : A = A | 726 x0 : A = A |
764 ============================ | 727 ============================ |
765 match x0 in (_ = T) return T with | 728 match x0 in (_ = T) return T with |
766 | refl_equal => y | 729 | refl_equal => y |
767 end = y | 730 end = y |
731 | |
768 ]] *) | 732 ]] *) |
769 | 733 |
770 rewrite (UIP_refl _ _ x0); reflexivity. | 734 rewrite (UIP_refl _ _ x0); reflexivity. |
771 Qed. | 735 Qed. |
772 | 736 |
777 | 741 |
778 | 742 |
779 (** * Equality of Functions *) | 743 (** * Equality of Functions *) |
780 | 744 |
781 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[ | 745 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[ |
782 | |
783 Theorem S_eta : S = (fun n => S n). | 746 Theorem S_eta : S = (fun n => S n). |
784 | 747 |
785 ]] | 748 ]] |
786 | 749 |
787 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be %\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. *) | 750 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be %\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. *) |
788 | 751 |
789 (* begin thide *) | 752 (* begin thide *) |
818 rewrite (ext_eq (fun x => match x with | 781 rewrite (ext_eq (fun x => match x with |
819 | 0 => True | 782 | 0 => True |
820 | S _ => True | 783 | S _ => True |
821 end) (fun _ => True)). | 784 end) (fun _ => True)). |
822 (** [[ | 785 (** [[ |
823 | |
824 2 subgoals | 786 2 subgoals |
825 | 787 |
826 ============================ | 788 ============================ |
827 (nat -> True) = (nat -> True) | 789 (nat -> True) = (nat -> True) |
828 | 790 |
830 forall x : nat, match x with | 792 forall x : nat, match x with |
831 | 0 => True | 793 | 0 => True |
832 | S _ => True | 794 | S _ => True |
833 end = True | 795 end = True |
834 ]] *) | 796 ]] *) |
835 | |
836 | 797 |
837 reflexivity. | 798 reflexivity. |
838 | 799 |
839 destruct x; constructor. | 800 destruct x; constructor. |
840 Qed. | 801 Qed. |
853 %\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># | 814 %\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># |
854 %\item%#<li># Prove that [subst] preserves program meanings. That is, prove | 815 %\item%#<li># Prove that [subst] preserves program meanings. That is, prove |
855 [[ | 816 [[ |
856 forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts), | 817 forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts), |
857 expDenote (subst e e') s = expDenote e (expDenote e' s ::: s) | 818 expDenote (subst e e') s = expDenote e (expDenote e' s ::: s) |
819 | |
858 ]] | 820 ]] |
859 where [:::] is an infix operator for heterogeneous "cons" that is defined in the book's [DepList] module.#</li># | 821 where [:::] is an infix operator for heterogeneous "cons" that is defined in the book's [DepList] module.#</li># |
860 #</ol>#%\end{enumerate}% | 822 #</ol>#%\end{enumerate}% |
861 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. | 823 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. |
862 %\begin{enumerate}%#<ol># | 824 %\begin{enumerate}%#<ol># |