Mercurial > cpdt > repo

comparison src/Equality.v @ 444:0d66f1a710b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.