comparison src/Equality.v @ 436:5d5e44f905c7

Changes during more coqdoc hacking
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 15:41:06 -0400
parents a54a4a2ea6e4
children 8077352044b2
comparison
equal deleted inserted replaced
435:a54a4a2ea6e4 436:5d5e44f905c7
411 (** %\vspace{-.15in}% [[ 411 (** %\vspace{-.15in}% [[
412 UIP_refl 412 UIP_refl
413 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x 413 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
414 ]] 414 ]]
415 415
416 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an _axiom_, the term [Eq_rect_eq.eq_rect_eq] below. *) 416 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an _axiom_, the term [eq_rect_eq] below. *)
417 417
418 (* begin hide *) 418 (* begin hide *)
419 Definition ere := eq_rect_eq. 419 Import Eq_rect_eq.
420 (* end hide *) 420 (* end hide *)
421
422 Print eq_rect_eq. 421 Print eq_rect_eq.
423 (** %\vspace{-.15in}% [[ 422 (** %\vspace{-.15in}% [[
424 eq_rect_eq = 423 *** [ eq_rect_eq :
425 fun U : Type => Eq_rect_eq.eq_rect_eq U 424 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
426 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), 425 x = eq_rect p Q x p h ]
427 x = eq_rect p Q x p h
428 ]] 426 ]]
429 427
430 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). *) 428 The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. The term [eq_rect] is the automatically generated recursion principle for [eq]. Calling [eq_rect] is another way of [match]ing on an equality proof. The proof we match on is the argument [h], and [x] is the body of the [match]. The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *)
431 429
432 (* begin hide *) 430 (* begin hide *)
460 ]] 458 ]]
461 459
462 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. *) 460 This is the unfortunately named %\index{axiom K}%"Streicher's axiom K," which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
463 461
464 End fhlist_map. 462 End fhlist_map.
463
464 (* begin hide *)
465 Require Eqdep_dec.
466 (* end hide *)
465 467
466 (** 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. *) 468 (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality. The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)
467 469
468 470
469 (** * Type-Casts in Theorem Statements *) 471 (** * Type-Casts in Theorem Statements *)