Mercurial > cpdt > repo
comparison src/Equality.v @ 502:7d2339cbd39c
Pass through Chapter 10
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 05 Feb 2013 17:05:09 -0500 |
parents | 31258618ef73 |
children | ed829eaa91b2 |
comparison
equal
deleted
inserted
replaced
501:28c2fa8af4eb | 502:7d2339cbd39c |
---|---|
242 Definition get := O. | 242 Definition get := O. |
243 Definition imap := O. | 243 Definition imap := O. |
244 (* end thide *) | 244 (* end thide *) |
245 (* end hide *) | 245 (* end hide *) |
246 | 246 |
247 (** 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. *) | 247 (** 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, which sets us on a collision course with the problems that are the subject of this chapter. *) |
248 | 248 |
249 Variable elm : A. | 249 Variable elm : A. |
250 | 250 |
251 Theorem fhget_fhmap : forall ls (mem : fmember elm ls) (hls : fhlist B ls), | 251 Theorem fhget_fhmap : forall ls (mem : fmember elm ls) (hls : fhlist B ls), |
252 fhget (fhmap hls) mem = f (fhget hls mem). | 252 fhget (fhmap hls) mem = f (fhget hls mem). |
268 end = f match a0 in (_ = a2) return (B a2) with | 268 end = f match a0 in (_ = a2) return (B a2) with |
269 | eq_refl => a1 | 269 | eq_refl => a1 |
270 end | 270 end |
271 ]] | 271 ]] |
272 | 272 |
273 This seems like a trivial enough obligation. The equality proof [a0] must be [eq_refl], since that is the only constructor of [eq]. Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity. | 273 This seems like a trivial enough obligation. The equality proof [a0] must be [eq_refl], the only constructor of [eq]. Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity. |
274 [[ | 274 [[ |
275 destruct a0. | 275 destruct a0. |
276 ]] | 276 ]] |
277 | 277 |
278 << | 278 << |
279 User error: Cannot solve a second-order unification problem | 279 User error: Cannot solve a second-order unification problem |
280 >> | 280 >> |
281 | 281 |
282 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. | 282 This is one of Coq's standard error messages for informing us of a failure in its heuristics for attempting an instance of an undecidable problem about dependent typing. We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial. |
283 [[ | 283 [[ |
284 assert (a0 = eq_refl _). | 284 assert (a0 = eq_refl _). |
285 ]] | 285 ]] |
286 | 286 |
287 << | 287 << |
430 *** [ eq_rect_eq : | 430 *** [ eq_rect_eq : |
431 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), | 431 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), |
432 x = eq_rect p Q x p h ] | 432 x = eq_rect p Q x p h ] |
433 ]] | 433 ]] |
434 | 434 |
435 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). *) | 435 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. *) |
436 | 436 |
437 (* begin hide *) | 437 (* begin hide *) |
438 (* begin thide *) | 438 (* begin thide *) |
439 Definition False' := False. | 439 Definition False' := False. |
440 (* end thide *) | 440 (* end thide *) |
626 match pf in (_ = ls) return (fhlist B ls) with | 626 match pf in (_ = ls) return (fhlist B ls) with |
627 | eq_refl => (a0, f) | 627 | eq_refl => (a0, f) |
628 end | 628 end |
629 ]] | 629 ]] |
630 | 630 |
631 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 contain some positions where only variables are allowed. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood. | 631 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but such a phenomenon applies to the case here and to many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations contain some positions where only variables are allowed. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood. |
632 | 632 |
633 In this case, it is helpful to generalize over our two proofs as well. *) | 633 In this case, it is helpful to generalize over our two proofs as well. *) |
634 | 634 |
635 generalize pf pf'. | 635 generalize pf pf'. |
636 (** [[ | 636 (** [[ |
644 match pf0 in (_ = ls) return (fhlist B ls) with | 644 match pf0 in (_ = ls) return (fhlist B ls) with |
645 | eq_refl => (a0, f) | 645 | eq_refl => (a0, f) |
646 end | 646 end |
647 ]] | 647 ]] |
648 | 648 |
649 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. | 649 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 so 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. |
650 | 650 |
651 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and _may be rewritten as well_. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *) | 651 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and _may be rewritten as well_. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *) |
652 | 652 |
653 rewrite app_assoc. | 653 rewrite app_assoc. |
654 (** [[ | 654 (** [[ |
901 (** * Equivalence of Equality Axioms *) | 901 (** * Equivalence of Equality Axioms *) |
902 | 902 |
903 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *) | 903 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *) |
904 | 904 |
905 (* begin thide *) | 905 (* begin thide *) |
906 (** 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. | 906 (** 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 by showing how each of the previous two sections' approaches reduces to the other logically. |
907 | 907 |
908 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. *) | 908 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. *) |
909 | 909 |
910 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x. | 910 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x. |
911 intros; rewrite (UIP_refl' pf); reflexivity. | 911 intros; rewrite (UIP_refl' pf); reflexivity. |