Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Equality.v Wed Aug 01 16:32:04 2012 -0400 +++ b/src/Equality.v Wed Aug 01 17:03:39 2012 -0400 @@ -978,11 +978,11 @@ (** * Equality of Functions *) -(** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[ +(** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. + %\vspace{-.15in}%[[ Theorem two_identities : (fun n => n) = (fun n => n + 0). ]] - - 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. *) + %\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. *) Require Import FunctionalExtensionality. About functional_extensionality. @@ -992,7 +992,7 @@ ]] *) -(** 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. *) +(** 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. *) Theorem two_identities : (fun n => n) = (fun n => n + 0). (* begin thide *)