two minor bug corrections in General Recursive Functions

and one un structural Functions.


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

3 files changed, 100 insertions, 41 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index edc01011e..0bcf19dc6 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -39,12 +39,12 @@ let do_observe_tac s tac g =
 	    Cerrors.explain_exn e ++ str " on goal " ++ goal ); 
    raise e;;
 
-
-let observe_tac s tac g =
+let observe_tac_stream s tac g = 
   if do_observe ()
-  then do_observe_tac (str s) tac g
+  then do_observe_tac  s tac g
   else tac g
 
+let observe_tac s tac g = observe_tac_stream (str s) tac g
 
 let tclTRYD tac = 
   if  !Options.debug  || do_observe ()
@@ -315,9 +315,13 @@ let h_reduce_with_zeta =
 
 
 let rewrite_until_var arg_num eq_ids : tactic =
+  (* tests if the declares recursive argument is neither a Constructor nor 
+     an applied Constructor since such a form for the recursive argument 
+     will break the Guard when trying to save the Lemma. 
+  *)
   let test_var g = 
     let _,args = destApp (pf_concl g) in 
-    not (isConstruct args.(arg_num))
+    not ((isConstruct args.(arg_num)) || isAppConstruct args.(arg_num))
   in
   let rec do_rewrite eq_ids g  = 
     if test_var g 
@@ -1334,10 +1338,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
 	      h_intro hid;
 	      Elim.h_decompose_and (mkVar hid); 
 	      backtrack_eqs_until_hrec hrec eqs;
-	      tclCOMPLETE (tclTHENS  (* We must have exactly ONE subgoal !*)
-		(apply (mkVar hrec))
-		[ tclTHENSEQ 
-		    [
+	      observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" )
+		(tclTHENS  (* We must have exactly ONE subgoal !*)
+		   (apply (mkVar hrec))
+		   [ tclTHENSEQ 
+		       [
 			 thin [hrec];
 			 apply (Lazy.force acc_inv);
 			 (fun g -> 
@@ -1346,11 +1351,12 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
 			      unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g 
 			    else tclIDTAC g
 			 );
-			 tclTRY(Recdef.list_rewrite true eqs);
-			 observe_tac "finishing"  (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))
+			 observe_tac "rew_and_finish"
+			   (tclTHEN 
+			      (tclTRY(Recdef.list_rewrite true eqs))
+			      (observe_tac "finishing"  (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))))
 		       ]
-		]
-			  )
+		])
 	    ])
 	    gls
 
@@ -1545,7 +1551,7 @@ let prove_principle_for_gen
 		   let pte_info = 
 		     { proving_tac =
 			 (fun eqs -> 
-			    observe_tac "prove_with_tcc" 
+			    observe_tac "new_prove_with_tcc" 
 			      (new_prove_with_tcc is_mes acc_inv hrec  tcc_lemma_ref (List.map mkVar eqs))
 			 );
 		       is_valid = is_valid_hypothesis predicates_names 
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 7aec837d8..ec98e0df9 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -301,9 +301,18 @@ let pp_dur time time' =
   str (string_of_float (System.time_difference time time'))
 
 (* let qed () = save_named true  *)
-let defined () = Command.save_named false
-
-
+let defined () = 
+  try 
+    Command.save_named false 
+  with 
+    | UserError("extract_proof",msg) ->
+	Util.errorlabstrm
+	  "defined"
+	  ((try
+	      str "On goal : " ++ fnl () ++  pr_open_subgoals () ++ fnl ()
+	    with _ -> mt ()
+	   ) ++msg)
+    | e -> raise e
 
 
 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 16067e6f3..d780bc1c6 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -133,7 +133,17 @@ let evaluable_of_global_reference r =
       ConstRef sp -> EvalConstRef sp
     | VarRef id -> EvalVarRef id
     | _ -> assert false;;
-  
+
+
+let rank_for_arg_list h = 
+  let predicate a b = 
+      try List.for_all2 eq_constr a b with
+        Invalid_argument _ -> false in
+  let rec rank_aux i = function
+  | [] -> None
+  | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in
+  rank_aux 0;;
+
 let rec (find_call_occs:
 	   constr -> constr -> (constr list ->constr)*(constr  list list)) =
  fun f expr ->
@@ -144,19 +154,36 @@ let rec (find_call_occs:
      let (largs: constr list) = Array.to_list args in
      let rec find_aux = function
 	 []    -> (fun x -> []), []
-       | a::tl ->
-         (match find_aux tl with
-          (cf, ((arg1::args) as opt_args)) -> 
+       | a::upper_tl ->
+         (match find_aux upper_tl with
+          (cf, ((arg1::args) as args_for_upper_tl)) -> 
            (match find_call_occs f a with
              cf2, (_ :: _ as other_args) ->
-	       let len1 = List.length other_args in
-                 (fun l ->
-                   cf2 l::(cf (nthtl(l,len1)))), other_args@opt_args
-           | _, [] -> (fun x -> a::cf x), opt_args)
+               let rec avoid_duplicates args =
+                  match args with
+                  | [] -> (fun _ -> []), []
+                  | h::tl -> 
+                      let recomb_tl, args_for_tl =
+                          avoid_duplicates tl in
+                    match rank_for_arg_list h args_for_upper_tl with
+                    | None -> 
+                        (fun l -> List.hd l::recomb_tl(List.tl l)),
+                        h::args_for_tl
+                    | Some i ->
+                        (fun l -> List.nth l (i+List.length args_for_tl)::
+                            recomb_tl l),
+                        args_for_tl
+               in
+               let recombine, other_args' =
+                   avoid_duplicates other_args in
+	       let len1 = List.length other_args' in                   
+                   (fun l -> cf2 (recombine l)::cf(nthtl(l,len1))),
+                     other_args'@args_for_upper_tl
+           | _, [] -> (fun x -> a::cf x), args_for_upper_tl)
 	 | _, [] ->
 	   (match find_call_occs f a with
-	     cf, (arg1::args) -> (fun l -> cf l::tl), (arg1::args)
-	   | _, [] -> (fun x -> a::tl), [])) in
+	     cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args)
+	   | _, [] -> (fun x -> a::upper_tl), [])) in
      begin
        match (find_aux largs) with
 	   cf, [] -> (fun l -> mkApp(g, args)), []
@@ -168,7 +195,7 @@ let rec (find_call_occs:
   | Meta(_) -> error "find_call_occs : Meta"
   | Evar(_) -> error "find_call_occs : Evar"
   | Sort(_)  -> error "find_call_occs : Sort"
-  | Cast(_,_,_) -> error "find_call_occs : cast"
+  | Cast(b,_,_) -> find_call_occs f b
   | Prod(_,_,_) -> error "find_call_occs : Prod"
   | Lambda(_,_,_) -> error "find_call_occs : Lambda"
   | LetIn(_,_,_,_) -> error "find_call_occs : let in"
@@ -182,6 +209,8 @@ let rec (find_call_occs:
   | Fix(_) -> error "find_call_occs : Fix"
   | CoFix(_) -> error "find_call_occs : CoFix";;
 
+
+
 let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition" 
     (Coqlib.init_modules @ Coqlib.arith_modules) s;;
@@ -268,7 +297,9 @@ let rec  mk_intros_and_continue (extra_eqn:bool)
 	  let teq = pf_get_new_id teq_id g in
 	    tclTHENLIST
 	      [ h_intro teq;
-		tclMAP (fun eq -> tclTRY (Equality.general_rewrite_in true teq eq)) (List.rev eqs);
+		tclMAP 
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true teq eq)) 
+		  (List.rev eqs);
 	        cont_function (mkVar teq::eqs) expr
 	      ]
 	      g
@@ -285,7 +316,9 @@ let simpl_iter () =
        {rBeta=true;rIota=true;rZeta= true; rDelta=false;
         rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
     onConcl
-    
+
+(* The boolean value is_mes expresses that the termination is expressed
+  using a measure function instead of a well-founded relation. *)
 let tclUSER is_mes l g = 
   let clear_tac = 
     match l with 
@@ -473,12 +506,17 @@ let rec introduce_all_values is_mes acc_inv func context_fn
 		 (observe_tac "acc_inv" (apply (Lazy.force acc_inv)))
 		 [ observe_tac "h_assumption" h_assumption
 		 ;
-		  observe_tac "user proof"  (fun g ->  
-					       tclUSER
-						 is_mes
-						 (Some (hrec::hspec::(retrieve_acc_var g)@specs))
-						 g
-					    )
+		  tclTHENLIST
+		    [
+		      tclTRY(list_rewrite true eqs);
+		      observe_tac "user proof" 
+			(fun g ->  
+			   tclUSER
+			     is_mes
+			     (Some (hrec::hspec::(retrieve_acc_var g)@specs))
+			     g
+			)		     
+		    ]
 		 ]
 	    )
 	   ]) g)
@@ -580,7 +618,8 @@ let tclUSER_if_not_mes is_mes names_to_suppress =
     tclCOMPLETE (h_apply (delayed_force well_founded_ltof,Rawterm.NoBindings))
   else tclUSER is_mes names_to_suppress
 
-let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac wf_tac : tactic = 
+let termination_proof_header is_mes input_type ids args_id relation
+    rec_arg_num rec_arg_id tac wf_tac : tactic = 
   begin 
     fun g -> 
       let nargs = List.length args_id in
@@ -596,7 +635,8 @@ let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac wf_t
 	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
 	  (wf_thm::ids) 
       in 
-      let hrec = next_global_ident_away true hrec_id (wf_rec_arg::wf_thm::ids) in 
+      let hrec = next_global_ident_away true hrec_id
+	(wf_rec_arg::wf_thm::ids) in 
       let acc_inv = 
 	  lazy (
 	    mkApp (
@@ -630,9 +670,9 @@ let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac wf_t
 		  )
 	       )
 	       [ 
-		 (* interactive proof of the well_foundness of the relation *) 
+		 (* interactive proof that the relation is well_founded *)
 		 observe_tac "wf_tac" (wf_tac is_mes (Some args_id));
-		 (* well_foundness -> Acc for any element *)
+		 (* this gives the accessibility argument *)
 		 observe_tac 
 		   "apply wf_thm" 
 		   (h_apply ((mkApp(mkVar wf_thm,
@@ -694,7 +734,7 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
       in
       let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
       let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in 
-      start 
+      termination_proof_header 
 	is_mes
 	input_type
 	ids
@@ -805,7 +845,11 @@ let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal)   =
     Util.error "\"abstract\" cannot handle existentials";
   let hook _ _ = 
     let lemma = mkConst (Lib.make_con na) in 
-    Array.iteri (fun i _ -> by (observe_tac "tac" (prove_with_tcc lemma i))) (Array.make nb_goal ());
+    Array.iteri 
+      (fun i _ -> 
+	 by (observe_tac ("reusing lemma "^(string_of_id na)) (prove_with_tcc lemma i)))
+      (Array.make nb_goal ())
+    ;
     ref := Some lemma ;
     defined ();
   in