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

7 files changed, 68 insertions, 34 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7be0b015e8..2de7945ee4 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,14 +92,17 @@ let ids_of_named_context_avoiding avoid l =
     ([], avoid) (Termops.ids_of_named_context l)
     
 let combine_params avoid applied needed =
-  let rec aux ids app need =
+  let rec aux ids avoid app need =
     match app, need with
 	[], need -> 
-	  let need', avoid = ids_of_named_context_avoiding avoid need in
+	  let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in
 	    List.rev ids @ (List.map mkIdentC need'), avoid
-      | x :: app, _ :: need -> aux (x :: ids) app need    
+      | _, (true, (id, _, _)) :: need -> 
+	  let id' = next_ident_away_from id avoid in
+	    aux (CRef (Ident (dummy_loc, id')) :: ids) (Idset.add id' avoid) app need
+      | x :: app, (false, _) :: need -> aux (x :: ids) avoid app need    
       | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
-  in aux [] applied needed
+  in aux [] avoid applied needed
 
 let compute_context_vars env l =
   List.fold_left (fun avoid (iid, _, c) -> 
@@ -123,7 +126,9 @@ let full_class_binders env l =
 	    let (id, l) = destClassApp cl in
 	      (try
 		  let c = class_info (snd id) in
-		  let args, avoid = combine_params avoid l (List.rev c.cl_context @ List.rev c.cl_super @ List.rev c.cl_params) in
+		  let args, avoid = combine_params avoid l 
+		    (List.rev_map (fun x -> false, x) c.cl_context @ List.rev_map (fun x -> true, x) c.cl_super @ List.rev_map (fun x -> false, x) c.cl_params) 
+		  in
 		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
 		with Not_found -> unbound_class (Global.env ()) id)
 	| Implicit -> (x :: l', avoid))
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index fbe48e06a2..f53ea7beac 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -24,8 +24,8 @@ open Util
 (* This module defines type-classes *)
 type typeclass = {
   cl_name : identifier; (* Name of the class *)
-  cl_context : named_context; (* Context in which superclasses and params are typed (usually types) *)
-  cl_super : named_context; (* Superclasses applied to some of the params *)
+  cl_context : named_context; (* Context in which superclasses and params are typed (usually types and indirect superclasses) *)
+  cl_super : named_context; (* Direct superclasses applied to some of the params *)
   cl_params : named_context; (* Context of the real parameters (types and operations) *)
 (*   cl_defs : rel_context; (\* Context of the definitions (usually functions), which may be shared *\) *)
   cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
index 11eb69b5d3..bb475bdc2a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -18,7 +18,7 @@ intros.
 destruct H.
 Defined.
 
-Program Fixpoint fetch t p (x:Exact t p) {struct x} :=
+Program Fixpoint fetch t p (x:Exact t p) {struct t} :=
    match t, p with
    | No p' , nil      => p'
    | No p' , _::_     => unreachable nat _
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index c1f8194124..d81589fc47 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,4 +1,4 @@
-Require Import Coq.Program.Tactics.
+Require Import Coq.Program.Program.
 
 Variable A : Set.
 
@@ -17,7 +17,7 @@ Require Import ProofIrrelevance.
 Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a n v'.
 Proof.
   intros n H.
-  dependent induction H.
+  dependent induction H generalizing n.
   inversion H0 ; subst.
   rewrite (UIP_refl _ _ H0).
   simpl.
@@ -52,20 +52,27 @@ Proof with simpl in * ; auto.
   dependent induction H generalizing G D.
 
   destruct D...
-  subst.
-  apply weak ; apply ax.
-  inversion H ; subst.
-  apply ax.
-
-  induction D...
-  subst.
-  do 2 apply weak.
-  assumption.
+    subst.
+    apply weak ; apply ax.
 
-  apply weak.
-  apply IHterm.
-  inversion H0 ; subst ; reflexivity.
+    inversion H ; subst.
+    apply ax.
+    
+  destruct D...
+    subst.
+    do 2 apply weak.
+    assumption.
 
-  apply abs.
+    apply weak.
+    apply IHterm.
+    inversion H0 ; subst ; reflexivity.
+
+  cut(term (snoc (app G0 D) tau'0) (arrow tau tau') -> term (app (snoc G0 tau'0) D) (arrow tau tau')).
+  intros.
+  apply H0.
   apply weak.
+  apply abs.
+  assumption.
+
+  intros.
 Admitted.
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. *)