diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/subtac/FunctionalExtensionality.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/subtac/FunctionalExtensionality.v')
-rw-r--r-- | contrib/subtac/FunctionalExtensionality.v | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v deleted file mode 100644 index 4610f346..00000000 --- a/contrib/subtac/FunctionalExtensionality.v +++ /dev/null @@ -1,47 +0,0 @@ -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. - -Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), - (forall x, f x = g x) -> f = g. - -Hint Resolve fun_extensionality fun_extensionality_dep : subtac. - -Require Import Coq.subtac.Utils. -Require Import Coq.subtac.FixSub. - -Lemma fix_sub_eq_ext : - forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) - (P : A -> Set) - (F_sub : forall x : A, (forall {y : A | R y x}, P (`y)) -> P x), - forall x : A, - Fix_sub A R Rwf P F_sub x = - F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)). -Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). - 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. |