diff options
author | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/subtac/FunctionalExtensionality.v | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/subtac/FunctionalExtensionality.v')
-rw-r--r-- | contrib/subtac/FunctionalExtensionality.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v index 1a12ac82..4610f346 100644 --- a/contrib/subtac/FunctionalExtensionality.v +++ b/contrib/subtac/FunctionalExtensionality.v @@ -1,3 +1,11 @@ +Lemma equal_f : forall A B : Type, forall (f g : A -> B), + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + Axiom fun_extensionality : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g. @@ -23,3 +31,17 @@ Proof. apply (fun_extensionality_dep _ _ _ _ H). rewrite H0 ; auto. Qed. + +Lemma fix_sub_measure_eq_ext : + forall (A : Type) (f : A -> nat) (P : A -> Type) + (F_sub : forall x : A, (forall {y : A | f y < f x}, P (`y)) -> P x), + forall x : A, + Fix_measure_sub A f P F_sub x = + F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)). +Proof. + intros ; apply Fix_measure_eq ; auto. + intros. + assert(f0 = g). + apply (fun_extensionality_dep _ _ _ _ H). + rewrite H0 ; auto. +Qed. |