Addition of more general tactics for equality. Functional extensionality and eta expansion axioms for

dependent functions. Cleanup in Utils.


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

1 files changed, 24 insertions, 7 deletions

diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 40356a9c49..22cb93d56b 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -11,16 +11,38 @@ Proof.
   auto.
 Qed.
 
+(** Eta expansion *)
+
+Axiom eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), 
+  f = fun x => f x.
+
+Lemma eta_expansion : forall A B (f : A -> B), 
+  f = fun x => f x.
+Proof.
+  intros ; apply eta_expansion_dep.
+Qed.
+
 (** Statements of functional equality for simple and dependent functions. *)
 
-Axiom fun_extensionality : forall A B (f g : A -> B), 
+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.
 
-Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), 
+Lemma fun_extensionality : forall A B (f g : A -> B), 
   (forall x, f x = g x) -> f = g.
+Proof.
+  intros ; apply fun_extensionality_dep.
+  assumption.
+Qed.
 
 Hint Resolve fun_extensionality fun_extensionality_dep : program.
 
+(** Unification needs help sometimes... *)
+Ltac apply_ext :=
+  match goal with 
+    [ |- ?x = ?y ] => apply (@fun_extensionality _ _ x y)
+  end.
+
 (** The two following lemmas allow to unfold a well-founded fixpoint definition without
    restriction using the functional extensionality axiom. *)
 
@@ -57,9 +79,4 @@ Proof.
   rewrite H0 ; auto.
 Qed.
 
-Ltac apply_ext :=
-  match goal with 
-    [ |- ?x = ?y ] => apply (@fun_extensionality _ _ x y)
-  end.
-