Better resolution of implicit parameters in typeclass binders, add extensionality tactic to apply the axiom properly and fix test-suite.

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

3 files changed, 33 insertions, 11 deletions

diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 382252ce2a..81bb5390b1 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -1,6 +1,25 @@
+(************************************************************************)
+(*  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: Tactics.v 10410 2007-12-31 13:11:55Z 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. 
+
+   It also defines two lemmas for expansion of fixpoint defs using extensionnality and proof-irrelevance
+   to avoid a side condition on the functionals. *)
+   
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Wf.
 
+Set Implicit Arguments.
+Unset Strict Implicit.
+
 (** The converse of functional equality. *)
 
 Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
@@ -37,10 +56,11 @@ 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)
+(** Apply [fun_extensionality], introducing variable x. *)
+
+Tactic Notation "extensionality" ident(x) :=
+  match goal with
+    [ |- ?X = ?Y ] => apply (@fun_extensionality _ _ X Y) || apply (@fun_extensionality_dep _ _ X Y) ; intro x
   end.
 
 (** The two following lemmas allow to unfold a well-founded fixpoint definition without
@@ -59,7 +79,7 @@ Proof.
   intros ; apply Fix_eq ; auto.
   intros.
   assert(f = g).
-  apply (fun_extensionality_dep _ _ _ _ H).
+  extensionality y ; apply H.
   rewrite H0 ; auto.
 Qed.
 
@@ -75,7 +95,7 @@ Proof.
   intros ; apply Fix_measure_eq ; auto.
   intros.
   assert(f0 = g).
-  apply (fun_extensionality_dep _ _ _ _ H).
+  extensionality y ; apply H.
   rewrite H0 ; auto.
 Qed.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index ac0f5cf717..b7b62f394a 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -134,6 +134,8 @@ Ltac autoinjection :=
       | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
     end.
 
+Ltac autoinjections := repeat autoinjection.
+
 (** Destruct an hypothesis by first copying it to avoid dependencies. *)
 
 Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.
@@ -157,7 +159,7 @@ Tactic Notation "contradiction" "by" constr(t) :=
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
 Ltac program_simplify :=
-  simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; 
-    try (solve [ red ; intros ; destruct_conjs ; discriminate ]).
+  simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; try autoinjection ; try discriminates ;
+    try (solve [ red ; intros ; destruct_conjs ; try autoinjection ; discriminates ]).
 
 Ltac program_simpl := program_simplify ; auto with *.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 6af81a4105..16e8de9707 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -18,9 +18,9 @@ Notation " {{ x }} " := (tt : { y : unit | x }).
 
 (** A simpler notation for subsets defined on a cartesian product. *)
 
-(* Notation "{ ( x , y )  :  A  |  P }" :=  *)
-(*   (sig (fun anonymous : A => let (x,y) := anonymous in P)) *)
-(*   (x ident, y ident, at level 10) : type_scope. *)
+Notation "{ ( x , y )  :  A  |  P }" :=
+  (sig (fun anonymous : A => let (x,y) := anonymous in P))
+  (x ident, y ident, at level 10) : type_scope.
 
 (** Generates an obligation to prove False. *)