- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a side

  effect, old cut_replacing was betaiota-normalizing, new
  cut_replacing, from commit 11662, does not; turn
  betaiota-normalisation into a purer and simpler whd_beta of the
  abstracted rewriting predicate to the rewritten term).
- Made "induction in" more flexible when induction is on a goal variable
  (accept occurrences -- even if theoretically unnecessary -- so as e.g. 
   not to expand occurrences that would otherwise trigger reductions -
   see example in Peano.mult_succ_r).



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

2 files changed, 43 insertions, 66 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index eba3a119f2..1fcfb4e12f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -72,10 +72,6 @@ let general_elim_clause with_evars cls sigma c l elim =
     raise (Pretype_errors.PretypeError
 	      (env, (Pretype_errors.NoOccurrenceFound (c', cls))))
       
-let elimination_sort_of_clause = function
-  | None -> elimination_sort_of_goal
-  | Some id -> elimination_sort_of_hyp id
-
 (* The next function decides in particular whether to try a regular 
   rewrite or a setoid rewrite. 
   Approach is to break everything, if [eq] appears in head position 
@@ -94,16 +90,19 @@ let is_applied_relation t =
   | App (c, args) when Array.length args >= 2 -> true
   | _ -> false
 
-let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c l with_evars gl hdcncl =
+(* find_elim determines which elimination principle is necessary to
+   eliminate lbeq on sort_of_gl. *)
+
+let find_elim hdcncl lft2rgt gl =
   let hdcncls = string_of_inductive hdcncl in 
-  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+  let rwr_thm = if lft2rgt then hdcncls^"_rect_r" else hdcncls^"_rect" in
+  try pf_global gl (id_of_string rwr_thm)
+  with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
+
+let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c l with_evars gl hdcncl =
   let dir = if cls=None then lft2rgt else not lft2rgt in
-  let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-  let elim =
-    try pf_global gl (id_of_string rwr_thm)
-    with Not_found ->
-      error ("Cannot find rewrite principle "^rwr_thm^".")
-  in general_elim_clause with_evars cls sigma c l (elim,NoBindings) gl
+  let elim = find_elim hdcncl dir gl in
+  general_elim_clause with_evars cls sigma c l (elim,NoBindings) gl
 
 let adjust_rewriting_direction args lft2rgt =
   if List.length args = 1 then
@@ -114,8 +113,6 @@ let adjust_rewriting_direction args lft2rgt =
     (* other equality *)
     lft2rgt
 
-let leibniz_eq = Lazy.lazy_from_fun build_coq_eq
-
 let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_bindings) with_evars gl =
   if occs <> all_occurrences then (
     !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
@@ -990,26 +987,11 @@ let swapEquandsInHyp id gls =
   cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))
     (tclTHEN swapEquandsInConcl) gls
 
-(* find_elim determines which elimination principle is necessary to
-   eliminate lbeq on sort_of_gl.
-   This is somehow an artificial choice as we could take eq_rect in
-   all cases (eq_ind - and eq_rec - are instances of eq_rect) [HH 2/4/06].
-*)
-
-let find_elim sort_of_gl lbeq =
-  match kind_of_term sort_of_gl  with
-    | Sort(Prop Null)  (* Prop *)  -> lbeq.ind
-    | _ (* Set/Type *) -> 
-        (match lbeq.rect with
-           | Some eq_rect -> eq_rect
-           | None -> errorlabstrm "find_elim"
-		 (str "This type of substitution is not allowed."))
-
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim (pf_apply get_type_of gls (pf_concl gls)) lbeq in
+  let eq_elim = find_elim lbeq.eq false gls in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
@@ -1062,14 +1044,16 @@ let subst_tuple_term env sigma dep_pair b =
   let abst_B =
     List.fold_right
       (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in
-  applist(abst_B,proj_list)
-    
+  beta_applist(abst_B,proj_list)
+
 (* Comme "replace" mais decompose les egalites dependantes *)
 
+exception NothingToRewrite
+
 let cutSubstInConcl_RL eqn gls =
   let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in
   let body = pf_apply subst_tuple_term gls e2 (pf_concl gls) in
-  assert (dependent (mkRel 1) body);
+  if not (dependent (mkRel 1) body) then raise NothingToRewrite;
   bareRevSubstInConcl lbeq body eq gls
 
 (* |- (P e1)
@@ -1087,7 +1071,7 @@ let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL
 let cutSubstInHyp_LR eqn id gls =
   let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in 
   let body = pf_apply subst_tuple_term gls e1 (pf_get_hyp_typ gls id) in
-  assert (dependent (mkRel 1) body);
+  if not (dependent (mkRel 1) body) then raise NothingToRewrite;
   cut_replacing id (subst1 e2 body)
     (tclTHENFIRST (bareRevSubstInConcl lbeq body eq)) gls
 
@@ -1107,6 +1091,9 @@ let try_rewrite tac gls =
     | e when catchable_exception e -> 
 	errorlabstrm "try_rewrite"
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
+    | NothingToRewrite ->
+	errorlabstrm "try_rewrite"
+          (strbrk "Nothing to rewrite.")
 
 let cutSubstClause l2r eqn cls gls =
   match cls with
@@ -1125,33 +1112,22 @@ let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
 let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
 let rewriteInConcl l2r c = rewriteClause l2r c None
 
-(* Renaming scheme correspondence new name (old name)
+(* Naming scheme for rewrite and cutrewrite tactics
 
-      give equality                    give proof of equality
+      give equality        give proof of equality
 
-    / cutSubstClause (subst)          substClause (HypSubst on hyp)
-raw | cutSubstInHyp (substInHyp)      substInHyp (none)
-    \ cutSubstInConcl (substInConcl)  substInConcl (none) 
+    / cutSubstClause       substClause
+raw | cutSubstInHyp        substInHyp
+    \ cutSubstInConcl      substInConcl
 
-    / cutRewriteClause (none)         rewriteClause (none)
-user| cutRewriteInHyp (substHyp)      rewriteInHyp (none)
-    \ cutRewriteInConcl (substConcl)  rewriteInConcl (substHypInConcl on hyp)
+    / cutRewriteClause     rewriteClause
+user| cutRewriteInHyp      rewriteInHyp
+    \ cutRewriteInConcl    rewriteInConcl
 
 raw = raise typing error or PatternMatchingFailure
 user = raise user error specific to rewrite
 *)
 
-(* Summary of obsolete forms
-let substInConcl = cutSubstInConcl
-let substInHyp = cutSubstInHyp
-let hypSubst l2r id = substClause l2r (mkVar id)
-let hypSubst_LR = hypSubst true
-let hypSubst_RL = hypSubst false
-let substHypInConcl l2r id = rewriteInConcl l2r (mkVar id)
-let substConcl = cutRewriteInConcl
-let substHyp = cutRewriteInHyp
-*)
-
 (**********************************************************************)
 (* Substitutions tactics (JCF) *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ab65c4888a..5392fc43e3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2651,25 +2651,25 @@ let enforce_eq_name id gl = function
   | x ->
       x
 
+let has_selected_occurrences = function
+  | None -> false
+  | Some cls ->
+      cls.concl_occs <> all_occurrences_expr ||
+	cls.onhyps <> None && List.exists (fun ((occs,_),hl) ->
+          occs <> all_occurrences_expr || hl <> InHyp) (Option.get cls.onhyps)
+
+(* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls gl =
   match cls with
   | None -> tclIDTAC gl
   | Some cls ->
-      let error () =
-	error 
-	  "Selection of occurrences not supported when destructing a variable."
-      in
-      if occur_var (pf_env gl) id (pf_concl gl) then
-	if cls.concl_occs = no_occurrences_expr then
-	  errorlabstrm ""
+      if occur_var (pf_env gl) id (pf_concl gl) &&
+	 cls.concl_occs = no_occurrences_expr 
+      then errorlabstrm ""
 	    (str "Conclusion must be mentioned: it depends on " ++ pr_id id
-	     ++ str ".")
-	else if cls.concl_occs <> all_occurrences_expr then
-	  error ();
+	     ++ str ".");
       match cls.onhyps with
       | Some hyps ->
-	  List.iter (fun ((occs,id),hl) ->
-	    if occs <> all_occurrences_expr || hl <> InHyp then error ()) hyps;
 	  let to_erase (id',_,_ as d) =
 	    if List.mem id' inhyps then (* if selected, do not erase *) None
 	    else
@@ -2686,7 +2686,8 @@ let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
   | _ -> [] in
   match kind_of_term c with
     | Var id when not (mem_named_context id (Global.named_context()))
-	        & lbind = NoBindings & not with_evars & eqname = None ->
+	        & lbind = NoBindings & not with_evars & eqname = None 
+                & not (has_selected_occurrences cls) ->
 	tclTHEN
           (clear_unselected_context id inhyps cls)
 	  (induction_with_atomization_of_ind_arg