- Another bug in get_sort_family_of (sort-polymorphism of constants and

  inductive types was not taken into account).
- Virtually extended tauto to 
  - support arbitrary-length disjunctions and conjunctions,
  - support arbitrary complex forms of disjunctions and
    conjunctions when in the contravariant of an implicative hypothesis,
  - stick with the purely propositional fragment and not apply reflexivity.
  This is virtual in the sense that it is not activated since it breaks 
  compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a 
  way that is closer to the intuitive meaning (forbid dependencies 
  between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
  definition; modified tauto.ml4 so that it works with the current and
  the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.



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

1 files changed, 86 insertions, 49 deletions

diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index c796eda90..769681155 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -15,6 +15,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Sign
 open Termops
 open Reductionops
 open Inductiveops
@@ -64,48 +65,83 @@ let match_with_non_recursive_type t =
 
 let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
 
-(* A general conjunction type is a non-recursive inductive type with
-   only one constructor. *)
+(* Test dependencies *)
 
-let match_with_conjunction_size t =
-  let (hdapp,args) = decompose_app t in 
-  match kind_of_term hdapp with
-    | Ind ind -> 
-	let (mib,mip) = Global.lookup_inductive ind in
-	if (Array.length mip.mind_consnames = 1)
-	  && (not (mis_is_recursive (ind,mib,mip)))
-          && (mip.mind_nrealargs = 0)
-        then 
-	  Some (hdapp,args,mip.mind_consnrealdecls.(0))
-        else 
-	  None
-    | _ -> None
-
-let match_with_conjunction t =
-  match match_with_conjunction_size t with
-  | Some (hd,args,n) -> Some (hd,args)
-  | None -> None
+let rec has_nodep_prod_after n c =
+  match kind_of_term c with
+    | Prod (_,_,b) -> 
+	( n>0 || not (dependent (mkRel 1) b)) 
+	&& (has_nodep_prod_after (n-1) b)
+    | _            -> true
+	  
+let has_nodep_prod = has_nodep_prod_after 0
 
-let is_conjunction t = op2bool (match_with_conjunction t)
-    
-(* A general disjunction type is a non-recursive inductive type all
-   whose constructors have a single argument. *)
+(* A general conjunctive type is a non-recursive with-no-indices inductive 
+   type with only one constructor and no dependencies between argument;
+   it is strict if it has the form 
+   "Inductive I A1 ... An := C (_:A1) ... (_:An)" *)
 
-let match_with_disjunction t =
+let match_with_conjunction ?(strict=false) t =
   let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
-    | Ind ind  ->
-        let car = mis_constr_nargs ind in
-	if array_for_all (fun ar -> ar = 1) car &&
-	   (let (mib,mip) = Global.lookup_inductive ind in
-            not (mis_is_recursive (ind,mib,mip)))
-        then 
+  | Ind ind -> 
+      let (mib,mip) = Global.lookup_inductive ind in
+      if (Array.length mip.mind_consnames = 1)
+	&& (not (mis_is_recursive (ind,mib,mip)))
+        && (mip.mind_nrealargs = 0)
+      then
+	let is_nth_argument n (_,b,c) = b=None && c=mkRel(n+mib.mind_nparams) in
+	if strict &&
+	  list_for_all_i is_nth_argument 1 
+	    (fst (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))
+	then
 	  Some (hdapp,args)
-        else 
-	  None
-    | _ -> None
+	else
+	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
+	  let cargs = List.map pi3 (fst (decompose_prod_assum ctyp)) in
+	  if has_nodep_prod ctyp then
+	    Some (hdapp,List.rev cargs)
+	  else None
+      else None
+  | _ -> None
+
+let is_conjunction ?(strict=false) t =
+  op2bool (match_with_conjunction ~strict t)
+
+(* A general disjunction type is a non-recursive with-no-indices inductive 
+   type with of which all constructors have a single argument;
+   it is strict if it has the form 
+   "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
+
+let match_with_disjunction ?(strict=false) t =
+  let (hdapp,args) = decompose_app t in 
+  match kind_of_term hdapp with
+  | Ind ind  ->
+      let car = mis_constr_nargs ind in
+      let (mib,mip) = Global.lookup_inductive ind in
+      if array_for_all (fun ar -> ar = 1) car &&
+	not (mis_is_recursive (ind,mib,mip))
+      then
+	if strict &
+	  array_for_all_i (fun i c -> 
+	    snd (decompose_prod_n_assum mib.mind_nparams c) = mkRel i) 1
+	  mip.mind_nf_lc
+	then
+	  Some (hdapp,args)
+	else
+	  let cargs =
+	    Array.map (fun ar -> pi2 (destProd (prod_applist ar args)))
+	      mip.mind_nf_lc in
+	  Some (hdapp,Array.to_list cargs)
+      else 
+	None
+  | _ -> None
 
-let is_disjunction t = op2bool (match_with_disjunction t)
+let is_disjunction ?(strict=false) t =
+  op2bool (match_with_disjunction ~strict t)
+
+(* An empty type is an inductive type, possible with indices, that has no
+   constructors *)
 
 let match_with_empty_type t =
   let (hdapp,args) = decompose_app t in
@@ -118,22 +154,32 @@ let match_with_empty_type t =
 	  
 let is_empty_type t = op2bool (match_with_empty_type t)
 
-let match_with_unit_type t =
+(* This filters inductive types with one constructor with no arguments;
+   Parameters and indices are allowed *)
+
+let match_with_unit_or_eq_type t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
     | Ind ind  -> 
         let (mib,mip) = Global.lookup_inductive ind in
         let constr_types = mip.mind_nf_lc in 
         let nconstr = Array.length mip.mind_consnames in
-        let zero_args c =
-	  nb_prod c = mib.mind_nparams in  
+        let zero_args c = nb_prod c = mib.mind_nparams in  
 	if nconstr = 1 && zero_args constr_types.(0) then 
 	  Some hdapp
-        else 
+	else 
 	  None
     | _ -> None
 
-let is_unit_type t = op2bool (match_with_unit_type t)
+let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
+
+(* A unit type is an inductive type with no indices but possibly
+   (useless) parameters, and that has no constructors *)
+
+let is_unit_type t =
+  match match_with_conjunction t with
+  | Some (_,t) when List.length t = 0 -> true
+  | _ -> false
 
 (* Checks if a given term is an application of an
    inductive binary relation R, so that R has only one constructor
@@ -204,15 +250,6 @@ let match_with_imp_term c=
 
 let is_imp_term c = op2bool (match_with_imp_term c) 
 
-let rec has_nodep_prod_after n c =
-  match kind_of_term c with
-    | Prod (_,_,b) -> 
-	( n>0 || not (dependent (mkRel 1) b)) 
-	&& (has_nodep_prod_after (n-1) b)
-    | _            -> true
-	  
-let has_nodep_prod = has_nodep_prod_after 0
-	
 let match_with_nodep_ind t =
   let (hdapp,args) = decompose_app t in
     match (kind_of_term hdapp) with