1 files changed, 60 insertions, 0 deletions
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
new file mode 100644
index 00000000..4445b0e1
--- /dev/null
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: FunctionalExtensionality.v 11686 2008-12-16 12:57:26Z msozeau $ 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. *)
+
+Set Manual Implicit Arguments.
+
+(** The converse of functional extensionality. *)
+
+Lemma equal_f : forall {A B : Type} {f g : A -> B}, 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+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), 
+  (forall x, f x = g x) -> f = g.
+
+Lemma functional_extensionality {A B} (f g : A -> B) : 
+  (forall x, f x = g x) -> f = g.
+Proof.
+  intros ; eauto using @functional_extensionality_dep.
+Qed.
+
+(** Apply [functional_extensionality], introducing variable x. *)
+
+Tactic Notation "extensionality" ident(x) :=
+  match goal with
+    [ |- ?X = ?Y ] => 
+    (apply (@functional_extensionality _ _ X Y) || 
+     apply (@functional_extensionality_dep _ _ X Y)) ; intro x
+  end.
+
+(** Eta expansion follows from extensionality. *)
+
+Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) :
+  f = fun x => f x.
+Proof.
+  intros.
+  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).
+Qed.