Nouveau Rewrite-in plus economique

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

8 files changed, 103 insertions, 86 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 674b090c39..b9d09f7173 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -217,9 +217,7 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
                   with BoundPattern -> failwith "make_apply_entry") in
-        let nmiss = 
-	  List.length 
-            (clenv_missing ce (clenv_template ce,clenv_template_type ce)) 
+        let nmiss = List.length (clenv_missing ce) 
         in 
 	if eapply & (nmiss <> 0) then begin
           if verbose then 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ca049a4547..b6131936c4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -94,6 +94,47 @@ let dyn_rewriteRL = function
   | [Constr c; Cbindings binds] -> 
       rewriteRL_bindings (c,binds)
   | _ -> assert false
+                 
+let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR
+let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)] 
+let h_rewriteLR c = h_rewriteLR_bindings (c,[])
+
+let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL
+let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)] 
+let h_rewriteRL c = h_rewriteRL_bindings (c,[])
+
+(*The Rewrite in tactic*)
+let general_rewrite_in lft2rgt id (c,l) gl =
+  let ctype = pf_type_of gl c in 
+  let env = pf_env gl in
+  let sigma = project gl in 
+  let _,t = splay_prod env sigma ctype in
+  match match_with_equation t with
+    | None -> (* Do not deal with setoids yet *) 
+        error "The term provided does not end with an equation" 
+    | Some (hdcncl,_) -> 
+        let hdcncls = string_of_inductive hdcncl in 
+	let suffix =
+          Indrec.elimination_suffix (elimination_sort_of_hyp id gl)in
+        let elim =
+	  if lft2rgt then
+            pf_global gl (id_of_string (hdcncls^suffix))
+          else
+	    pf_global gl (id_of_string (hdcncls^suffix^"_r"))
+        in 
+	general_elim_in id (c,l) (elim,[]) gl
+
+
+let dyn_rewrite_in lft2rgt = function
+  | [Identifier id;(Command com);(Bindings binds)] -> 
+      tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds)
+  | [Identifier id;(Constr c);(Cbindings binds)] -> 
+      general_rewrite_in lft2rgt id (c,binds)
+  | _ -> assert false
+
+let rewriteLR_in_tac =  hide_tactic "RewriteLRin" (dyn_rewrite_in true)
+let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false)
+
 
 (* Replacing tactics *)
 
@@ -133,14 +174,6 @@ let dyn_replace args gl =
     | [(Constr c1);(Constr c2)] -> 
        	replace c1 c2 gl
     | _ -> assert false
-                 
-let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR
-let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)] 
-let h_rewriteLR c = h_rewriteLR_bindings (c,[])
-
-let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL
-let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)] 
-let h_rewriteRL c = h_rewriteRL_bindings (c,[])
 
 let v_replace = hide_tactic "Replace" dyn_replace
 let h_replace c1 c2 = v_replace [(Constr c1);(Constr c2)]
@@ -373,12 +406,6 @@ let discriminable env sigma t1 t2 =
 
    the continuation then constructs the case-split.
  *)
-let push_rel_type sigma (na,c,t) env =
-  push_rel (na,c,t) env
-
-let push_rels vars env =
-  List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env
-
 let descend_then sigma env head dirn =
   let IndType (indf,_) as indt =
     try find_rectype env sigma (get_type_of env sigma head)
@@ -387,7 +414,7 @@ let descend_then sigma env head dirn =
   let (mib,mip) = lookup_mind_specif env ind in
   let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
-  let dirn_env = push_rels cstr.(dirn-1).cs_args env in
+  let dirn_env = push_rel_context cstr.(dirn-1).cs_args env in
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
@@ -1185,45 +1212,7 @@ let sub_term_with_unif cref ceq =
           None
         else
           Some ((plain_instance l ceq),nb)
-	    
-(*The Rewrite in tactic*)
-let general_rewrite_in lft2rgt id (c,lb) gls =
-  let typ_id = pf_get_hyp_typ gls id in
-  let (wc,_) = startWalk gls
-  and (_,t) = pf_reduce_to_quantified_ind gls (pf_type_of gls c) in
-  let ctype = type_clenv_binding wc (c,t) lb in
-  match (match_with_equation ctype) with
-    | None -> error "The term provided does not end with an equation" 
-    | Some (hdcncl,l) ->
-        let mbr_eq =
-          if lft2rgt then
-            List.hd (List.tl (List.rev l))
-          else
-            List.hd (List.rev l)
-        in
-        (match sub_term_with_unif typ_id mbr_eq with
-           | None ->
-               errorlabstrm "general_rewrite_in" 
-		 (str "Nothing to rewrite in: " ++ pr_id id)
-           | Some (l2,nb_occ) ->
-               (tclTHENSI
-		  (tclTHEN
-		     (tclTHEN (generalize [(pf_global gls id)])
-			(reduce (Pattern [(list_int nb_occ 1 [],l2,
-					   pf_type_of gls l2)]) []))
-		     (general_rewrite_bindings lft2rgt (c,lb))) 
-		  [(tclTHEN (clear [id]) (introduction id))]) gls)
-
-let dyn_rewrite_in lft2rgt = function
-  | [Identifier id;(Command com);(Bindings binds)] -> 
-      tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds)
-  | [Identifier id;(Constr c);(Cbindings binds)] -> 
-      general_rewrite_in lft2rgt id (c,binds)
-  | _ -> assert false
-
-let rewriteLR_in_tac =  hide_tactic "RewriteLRin" (dyn_rewrite_in true)
-let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false)
-			 
+	 
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
   tclTHEN_i (general_rewrite_in lft2rgt id (c,bl))
     (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)
@@ -1243,26 +1232,6 @@ let v_conditional_rewriteLR_in =
 let v_conditional_rewriteRL_in = 
   hide_tactic "CondRewriteRLin" (dyn_conditional_rewrite_in false)
 
-(* Rewrite c in id. Rewrite -> c in id. Rewrite <- c in id. 
-   Does not work when c is a conditional equation *)
-
-let rewrite_in lR com id gls =
-  (try 
-     let _ = lookup_named id (pf_env gls) in () 
-   with Not_found -> 
-     errorlabstrm "rewrite_in" (str"No such hypothesis : " ++pr_id id));
-  let c = pf_interp_constr gls com in
-  let eqn = pf_type_of gls c in
-  try
-    let _ = find_eq_data_decompose eqn in
-    (try 
-       (tclTHENS 
-          ((if lR then substInHyp else revSubstInHyp) eqn id) 
-          ([tclIDTAC ; exact_no_check c])) gls
-     with UserError("SubstInHyp",_) -> tclIDTAC gls)
-  with UserError ("find_eq_data_decompose",_)->  
-    errorlabstrm "rewrite_in" (str"No equality here") 
-      
 let subst eqn cls gls =
   match cls with
     | None ->    substInConcl eqn gls
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 5c6391dc55..5ff8be0f44 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -162,6 +162,7 @@ let find_theory a =
     
 (* Add a Setoid to the database after a type verification. *)
 
+(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->(eq a c)->(eq b d) *)
 let eq_lem_proof env a eq sym trans = 
   lambda_create env
     (a, lambda_create env
@@ -178,6 +179,7 @@ let eq_lem_proof env a eq sym trans =
 					 [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]
 			      )))))))))
 
+(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->((eq a c)<->(eq b d)) *)
 let eq_lem2_proof env a eq sym trans = 
   lambda_create env
     (a, lambda_create env
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 69141302cd..238dd4b950 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -289,6 +289,15 @@ let elimination_sort_of_goal gl =
 	   | Type _ -> InType)
     | _        -> anomaly "goal should be a type"
 
+let elimination_sort_of_hyp id gl = 
+  match kind_of_term (hnf_type_of gl (pf_get_hyp_typ gl id)) with 
+    | Sort s ->
+	(match s with
+	   | Prop Null -> InProp
+	   | Prop Pos -> InSet
+	   | Type _ -> InType)
+    | _        -> anomaly "goal should be a type"
+
 
 (* Find the right elimination suffix corresponding to the sort of the goal *)
 (* c should be of type A1->.. An->B with B an inductive definition *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index af0ea2a66b..7693e7f777 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -121,7 +121,7 @@ type branch_assumptions = {
   indargs   : identifier list} (* the inductive arguments *)
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
-(*i val suff              : goal sigma -> constr -> string i*)
+val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
 
 val general_elim_then_using :
   constr ->  (inductive -> bool list array) -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2fb555d884..a300258480 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1077,7 +1077,7 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
-let elimination_clause_scheme kONT wc elimclause indclause gl = 
+let elimination_clause_scheme kONT elimclause indclause gl = 
   let indmv = 
     (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
        | Meta mv -> mv
@@ -1108,7 +1108,7 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl =
   let indclause  = make_clenv_binding wc (c,t) lbindc  in
   let elimt      = w_type_of wc elimc in
   let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
-  elimination_clause_scheme kONT wc elimclause indclause gl
+  elimination_clause_scheme kONT elimclause indclause gl
 
 (* Elimination tactic with bindings but using the default elimination 
  * constant associated with the type. *)
@@ -1125,6 +1125,43 @@ let default_elim (c,lbindc)  gl =
 
 let simplest_elim c = default_elim (c,[])
 
+(* Elimination in hypothesis *)
+
+let elimination_in_clause_scheme kONT id elimclause indclause =
+  let (hypmv,indmv) = 
+    match clenv_independent elimclause with
+        [k1;k2] -> (k1,k2)
+      | _  -> errorlabstrm "elimination_clause"
+          (str "The type of elimination clause is not well-formed") in
+  let elimclause'  = clenv_fchain indmv elimclause indclause in 
+  let hyp = mkVar id in
+  let hyp_typ = clenv_type_of elimclause' hyp in
+  let hypclause =
+    mk_clenv_from_n elimclause'.hook 0 (hyp, hyp_typ) in
+  let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
+  let new_hyp_prf  = clenv_instance_template elimclause'' in
+  let new_hyp_typ  = clenv_instance_template_type elimclause'' in
+  if eq_constr hyp_typ new_hyp_typ then
+    errorlabstrm "general_rewrite_in" 
+      (str "Nothing to rewrite in " ++ pr_id id);
+  tclTHEN
+    (kONT elimclause''.hook)
+    (tclTHENS
+      (cut new_hyp_typ)
+      [ (* Try to insert the new hyp at the same place *)
+        tclORELSE (intro_replacing id)
+          (tclTHEN (clear [id]) (introduction id));
+        refine new_hyp_prf])
+
+let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = 
+  let (wc,kONT)  = startWalk gl in
+  let ct = pf_type_of gl c in
+  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
+  let indclause  = make_clenv_binding wc (c,t) lbindc  in
+  let elimt      = w_type_of wc elimc in
+  let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
+  elimination_in_clause_scheme kONT id elimclause indclause gl
+
 (*
  * A "natural" induction tactic
  * 
@@ -1440,7 +1477,7 @@ let induction_tac varname typ (elimc,elimt) gl =
   let (wc,kONT)  = startWalk gl                    in
   let indclause  = make_clenv_binding wc (c,typ) []  in
   let elimclause = make_clenv_binding wc (mkCast (elimc,elimt),elimt) [] in
-  elimination_clause_scheme kONT wc elimclause indclause gl
+  elimination_clause_scheme kONT elimclause indclause gl
 
 let is_indhyp p n t =
   let c,_ = decompose_app t in 
@@ -1648,7 +1685,7 @@ let elim_scheme_type elim t gl =
     | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
-	  clenv_unify CUMUL t (clenv_instance_type clause mv) clause in
+	  clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in
 	elim_res_pf kONT clause' gl
     | _ -> anomaly "elim_scheme_type"
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 28a17ea517..19cd032b0c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -188,6 +188,9 @@ val default_elim   : constr * constr substitution -> tactic
 val simplest_elim  : constr -> tactic
 val dyn_elim       : tactic_arg list -> tactic
 
+val general_elim_in : identifier -> constr * constr substitution ->
+                      constr * constr substitution -> tactic
+
 val old_induct       : identifier -> tactic
 val old_induct_nodep : int        -> tactic
 val dyn_old_induct : tactic_arg list -> tactic
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index a233aef2d0..007a3aa997 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -51,9 +51,7 @@ let clenv_constrain_with_bindings bl clause =
     clause 
   else 
     let all_mvs = collect_metas (clenv_template clause).rebus
-    and ind_mvs = clenv_independent clause
-		    (clenv_template clause,
-                     clenv_template_type clause) in
+    and ind_mvs = clenv_independent clause in
     let nb_indep = List.length ind_mvs in
     let rec matchrec clause = function
       | []       -> clause
@@ -95,7 +93,8 @@ let clenv_constrain_with_bindings bl clause =
 	  let sigma = Evd.empty in
 	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
 	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
-	  matchrec (clenv_assign k c (clenv_unify CUMUL c_typ k_typ clause)) t
+	  matchrec
+            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
     in 
     matchrec clause bl