diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Logic/FunctionalExtensionality.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Logic/FunctionalExtensionality.v')
-rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 0dc82907..1678a287 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: FunctionalExtensionality.v 11686 2008-12-16 12:57:26Z msozeau $ i*) +(*i $Id$ i*) (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) (** The converse of functional extensionality. *) -Lemma equal_f : forall {A B : Type} {f g : A -> B}, +Lemma equal_f : forall {A B : Type} {f g : A -> B}, f = g -> forall x, f x = g x. Proof. intros. @@ -23,11 +23,11 @@ Qed. (** Statements of functional extensionality for simple and dependent functions. *) -Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, - forall (f g : forall x : A, B x), +Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, + forall (f g : forall x : A, B x), (forall x, f x = g x) -> f = g. -Lemma functional_extensionality {A B} (f g : A -> B) : +Lemma functional_extensionality {A B} (f g : A -> B) : (forall x, f x = g x) -> f = g. Proof. intros ; eauto using @functional_extensionality_dep. @@ -37,8 +37,8 @@ Qed. Tactic Notation "extensionality" ident(x) := match goal with - [ |- ?X = ?Y ] => - (apply (@functional_extensionality _ _ X Y) || + [ |- ?X = ?Y ] => + (apply (@functional_extensionality _ _ X Y) || apply (@functional_extensionality_dep _ _ X Y)) ; intro x end. @@ -51,8 +51,8 @@ Proof. extensionality x. reflexivity. Qed. - + Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x. Proof. - intros A B f. apply (eta_expansion_dep f). + apply (eta_expansion_dep f). Qed. |