Added the automatic generation of the boolean equality if possible and the

decidability of the usual equality
Major changes:
 * andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v 
 * added 2 files:
    * toplevel/ind_tables.ml* : tables where the boolean eqs and the
        decidability proofs are stored
    * toplevel/auto_ind_decl.ml* : code of the schemes that are automatically
        generated from inductives types (currently boolean eq & decidability )
 * improvement of injection: if the decidability have been correctly computed,
   injection can now break the equalities over dependant pair

How to use:
 Set Equality Scheme. to set the automatic generation of the equality when you
create a new inductive type
 Scheme Equality for I. tries to create the equality for the already declared
type I




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

1 files changed, 38 insertions, 1 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 066bf88d4..677039015 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -801,7 +801,7 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
 	let injfun = mkNamedLambda e t injbody in
 	let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in
 	let ty = simplify_args env sigma (get_type_of env sigma pf) in
-	(pf,ty))
+	  (pf,ty))
       posns in
   if injectors = [] then
     errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
@@ -809,6 +809,9 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
     (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
     injectors
 
+exception Not_dep_pair
+
+
 let injEq ipats (eq,(t,t1,t2)) id gls =
   let sigma = project gls in
   let env = pf_env gls in
@@ -825,10 +828,44 @@ let injEq ipats (eq,(t,t1,t2)) id gls =
 	let t1 = try_delta_expand env sigma t1 in
 	let t2 = try_delta_expand env sigma t2 in
 *)
+        try (
+(* fetch the informations of the  pair *)
+        let ceq = constr_of_global Coqlib.glob_eq in
+        let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
+        let eqTypeDest = fst (destApp t) in 
+        let _,ar1 = destApp t1 and
+            _,ar2 = destApp t2 in
+        let ind = destInd ar1.(0) in
+        let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
+            ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+(* check whether the equality deals with dep pairs or not *)
+(* if yes, check if the user has declared the dec principle *)
+(* and compare the fst arguments of the dep pair *)
+        let new_eq_args = [|type_of env sigma (ar1.(3));ar1.(3);ar2.(3)|] in
+        if ( (eqTypeDest = sigTconstr()) &&
+             (Ind_tables.check_dec_proof ind=true) &&
+             (is_conv env sigma (ar1.(2)) (ar2.(2)) = true))
+              then ( 
+(* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*)
+              let qidl = qualid_of_reference 
+                (Ident (dummy_loc,id_of_string "Eqdep_dec")) in
+              Library.require_library [qidl] (Some false); 
+(* cut with the good equality and prove the requested goal *)
+              tclTHENS (cut (mkApp (ceq,new_eq_args)) )
+               [tclIDTAC; tclTHEN (apply (
+                  mkApp(inj2,
+                        [|ar1.(0);Ind_tables.find_eq_dec_proof ind;
+                          ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
+                  )) (Auto.trivial [] [])
+                ] gls
+(* not a dep eq or no decidable type found *)
+            ) else (raise Not_dep_pair) 
+        ) with _ -> (
 	tclTHEN 
 	  (inject_at_positions env sigma (eq,(t,t1,t2)) id posns)
 	  (intros_pattern None ipats)
 	  gls
+        )
 
 let inj ipats = onEquality (injEq ipats)