diff options
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. |