Mercurial > cpdt > repo
comparison src/Equality.v @ 444:0d66f1a710b8
Vertical spacing through end of Part II
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 01 Aug 2012 17:03:39 -0400 |
parents | 8077352044b2 |
children | 848bf35f7f6c |
comparison
equal
deleted
inserted
replaced
443:97c60ffdb998 | 444:0d66f1a710b8 |
---|---|
976 (* end thide *) | 976 (* end thide *) |
977 | 977 |
978 | 978 |
979 (** * Equality of Functions *) | 979 (** * Equality of Functions *) |
980 | 980 |
981 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[ | 981 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. |
982 %\vspace{-.15in}%[[ | |
982 Theorem two_identities : (fun n => n) = (fun n => n + 0). | 983 Theorem two_identities : (fun n => n) = (fun n => n + 0). |
983 ]] | 984 ]] |
984 | 985 %\vspace{-.15in}%Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be%\index{extensionality of function equality}% _extensional_. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We _can_ assert function extensionality as an axiom, and indeed the standard library already contains that axiom. *) |
985 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be%\index{extensionality of function equality}% _extensional_. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We _can_ assert function extensionality as an axiom, and indeed the standard library already contains that axiom. *) | |
986 | 986 |
987 Require Import FunctionalExtensionality. | 987 Require Import FunctionalExtensionality. |
988 About functional_extensionality. | 988 About functional_extensionality. |
989 (** %\vspace{-.15in}%[[ | 989 (** %\vspace{-.15in}%[[ |
990 functional_extensionality : | 990 functional_extensionality : |
991 forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g | 991 forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g |
992 ]] | 992 ]] |
993 *) | 993 *) |
994 | 994 |
995 (** This axiom has been verified metatheoretically to be consistent with CIC and the two equality axioms we considered previously. With it, the proof of [S_eta] is trivial. *) | 995 (** This axiom has been verified metatheoretically to be consistent with CIC and the two equality axioms we considered previously. With it, the proof of [two_identities] is trivial. *) |
996 | 996 |
997 Theorem two_identities : (fun n => n) = (fun n => n + 0). | 997 Theorem two_identities : (fun n => n) = (fun n => n + 0). |
998 (* begin thide *) | 998 (* begin thide *) |
999 apply functional_extensionality; crush. | 999 apply functional_extensionality; crush. |
1000 Qed. | 1000 Qed. |