### comparison src/Equality.v @ 502:7d2339cbd39c

Pass through Chapter 10
author Adam Chlipala Tue, 05 Feb 2013 17:05:09 -0500 31258618ef73 ed829eaa91b2
comparison
equal 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.