Mercurial > cpdt > repo
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 *) |