Move FunctionalExtensionality to Logic/ (someone please check that the

doc is ok). Rework the .v files in Program accordingly, adding some
documentation and proper headers. Integrate the development of an
elimination principle for measured functions in Program/Wf by Eelis van
der Weegen.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 60 insertions, 0 deletions

diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
new file mode 100644
index 0000000000..865a465534
--- /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$ 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.