Bug corrections in Function.

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

5 files changed, 57 insertions, 37 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 5654af0b3..edc01011e 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -179,10 +179,11 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
   let nochange msg  = 
     begin 
-(*       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    ); *)
+      observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    );
       failwith "NoChange"; 
     end
   in    
+  let eq_constr = Reductionops.is_conv env sigma in 
   if not (noccurn 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp t) then nochange "not an equality";
@@ -194,6 +195,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
     in 
     if not (closed0 t1) then nochange "not a closed lhs";    
     let rec compute_substitution sub t1 t2 = 
+      observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2);
       if isRel t2 
       then 
 	let t2 = destRel t2  in 
@@ -499,7 +501,7 @@ let clean_goal_with_heq ptes_infos continue_tac dyn_infos  =
     tclTHENLIST 
       [
 	tac ;
-	(continue_tac new_infos)
+	observe_tac "clean_hyp_with_heq continue" (continue_tac new_infos)
       ]
       g    
 
@@ -779,7 +781,7 @@ let build_proof
       finish_proof dyn_infos)
   in
   observe_tac "build_proof"
-    (build_proof do_finish_proof dyn_infos) 
+    (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) 
 
 
 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 9c6979ca8..f17ae6450 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -258,7 +258,7 @@ let derive_inversion fix_names =
       (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
 	  
 let generate_principle 
-    do_built fix_rec_l recdefs  interactive_proof parametrize 
+    is_general do_built fix_rec_l recdefs  interactive_proof parametrize 
     (continue_proof : int -> Names.constant array -> Term.constr array -> int -> 
       Tacmach.tactic) : unit =
   let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
@@ -308,7 +308,7 @@ let generate_principle
 	    0
 	    fix_rec_l
 	in 
-	Array.iter add_Function funs_kn;
+	Array.iter (add_Function is_general) funs_kn;
 	()
       end
   with e -> 
@@ -442,6 +442,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
       | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
+	      true
 	      register_built
 	      fixpoint_exprl 
 	      recdefs
@@ -453,6 +454,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
       | [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
+	      true
 	      register_built
 	      fixpoint_exprl 
 	      recdefs
@@ -504,6 +506,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	  let is_rec = List.exists (is_rec fix_names) recdefs in
 	  if register_built then register_struct is_rec old_fixpoint_exprl;
 	  generate_principle
+	    false
 	    register_built
 	    fixpoint_exprl
 	    recdefs 
@@ -709,7 +712,7 @@ let make_graph (f_ref:global_reference) =
 	(* We register the infos *)
 	let mp,dp,_ = repr_con c in 
 	List.iter 
-	  (fun (id,_,_,_,_) -> add_Function (make_con mp dp (label_of_id id))) 
+	  (fun (id,_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) 
 	  expr_list
 
 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 20263c188..a7f7dbf82 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -274,6 +274,7 @@ type function_info =
       rect_lemma : constant option;
       rec_lemma : constant option;
       prop_lemma : constant option;
+      is_general : bool; (* Has this function been defined using general recursive definition *)
     }
       
 
@@ -333,6 +334,7 @@ let subst_Function (_,subst,finfos) =
       rect_lemma = rect_lemma' ;
       rec_lemma = rec_lemma';
       prop_lemma = prop_lemma';
+      is_general = finfos.is_general
     }
 
 let classify_Function (_,infos) = Libobject.Substitute infos
@@ -368,6 +370,7 @@ let discharge_Function (_,finfos) =
 	   rect_lemma = rect_lemma';
 	   rec_lemma = rec_lemma';
 	   prop_lemma = prop_lemma' ;
+	   is_general = finfos.is_general
 	 }    
 
 open Term
@@ -442,7 +445,7 @@ let update_Function finfo =
   Lib.add_anonymous_leaf (in_Function finfo)
       
   
-let add_Function f = 
+let add_Function is_general f = 
   let f_id = id_of_label (con_label f) in 
   let equation_lemma = find_or_none (mk_equation_id f_id)
   and correctness_lemma = find_or_none (mk_correct_id f_id) 
@@ -462,7 +465,9 @@ let add_Function f =
       rect_lemma = rect_lemma;
       rec_lemma = rec_lemma;
       prop_lemma = prop_lemma;
-      graph_ind = graph_ind
+      graph_ind = graph_ind;
+      is_general = is_general
+      
     }
   in
   update_Function finfos
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 2142d29b3..1c8d880a2 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -92,12 +92,13 @@ type function_info =
       rect_lemma : constant option;
       rec_lemma : constant option;
       prop_lemma : constant option;
+      is_general : bool;
     }
 
 val find_Function_infos : constant -> function_info
 val find_Function_of_graph : inductive -> function_info
 (* WARNING: To be used just after the graph definition !!! *)
-val add_Function : constant -> unit
+val add_Function : bool -> constant -> unit
 
 val update_Function : function_info -> unit 
 
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 084ec7e01..74db6a54b 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -44,25 +44,6 @@ let pr_with_bindings prc prlc (c,bl) =
 let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds = 
   pr_with_bindings prc prc  (c,bl)
 
-let pr_elim_scheme el = 
-  let env = Global.env () in 
-  let msg = str "params := " ++ Printer.pr_rel_context env el.params in 
-  let env = Environ.push_rel_context el.params env in 
-  let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in 
-  let env = Environ.push_rel_context el.predicates env in 
-  let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in 
-  let env = Environ.push_rel_context el.branches env in 
-  let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in 
-  let env = Environ.push_rel_context el.args env in 
-  let msg = 
-    Util.option_fold_right
-      (fun o msg -> msg ++ fnl () ++ str "indarg := " ++ Printer.pr_rel_context env [o]) 
-      el.indarg
-      msg
-  in 
-  let env = Util.option_fold_right (fun o env -> Environ.push_rel_context [o] env) el.indarg env in 
-  msg ++ fnl () ++ str "concl := " ++ Printer.pr_lconstr_env env el.concl
-
 (* The local debuging mechanism *)
 let msgnl = Pp.msgnl
 
@@ -443,7 +424,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+	     let id = (* Termops.next_global_ident_away false (Nameops.out_name x) avoid *) 
+	       Nameops.next_ident_away (Nameops.out_name x) avoid in
 	     (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
 	  )
 	  ([],[])
@@ -453,7 +435,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in 
+(* Termops.next_global_ident_away false (Nameops.out_name x) avoid in *)
 	     (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
@@ -471,7 +454,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	  (observe_tac "functional_induction" (
 	     fun g -> 
 	       observe
-		 (str "princ" ++ pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g))  (mkVar principle_id,bindings));
+		 (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g))  (mkVar principle_id,bindings));
 	       functional_induction  false (applist(funs_constr.(i),List.map mkVar args_names))
 		 (Some (mkVar principle_id,bindings))
 		 pat g
@@ -493,6 +476,31 @@ let generalize_depedent_of x hyp g =
     (pf_hyps g)
     g
 
+
+
+
+
+
+let rec reflexivity_with_destruct_cases g = 
+  let destruct_case () = 
+    try 
+      match kind_of_term (snd (destApp (pf_concl g))).(2) with 
+	| Case(_,_,v,_) -> 
+	    tclTHENSEQ[
+	      h_case (v,Rawterm.NoBindings);
+	      intros;
+	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases 
+	    ]
+	| _ -> reflexivity
+    with _ -> reflexivity
+  in
+  tclFIRST
+    [ reflexivity;
+      destruct_case ()
+    ]
+    g
+
+
 (* [prove_fun_complete funs graphs schemes lemmas_types_infos i] 
    is the tactic used to prove completness lemma. 
    
@@ -567,11 +575,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let rewrite_tac j ids : tactic = 
       let graph_def = graphs.(j) in 
-      if Rtree.is_infinite graph_def.mind_recargs
+      let infos =  try find_Function_infos (destConst funcs.(j)) with Not_found ->  error "No graph found" in 
+      if infos.is_general ||  Rtree.is_infinite graph_def.mind_recargs
       then 
 	let eq_lemma = 
-	  try out_some (find_Function_infos (destConst funcs.(j))).equation_lemma
-	  with Failure "out_some" | Not_found -> anomaly "Cannot find equation lemma"
+	  try out_some (infos).equation_lemma
+	  with Failure "out_some"  -> anomaly "Cannot find equation lemma"
 	in 
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
@@ -677,8 +686,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
         observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
 	(* introduce hypothesis with some rewrite *)
         (intros_with_rewrite);
-	(* The proof is complete *)
-        observe_tac "reflexivity" (reflexivity)
+	(* The proof is (almost) complete *)
+        observe_tac "reflexivity" (reflexivity_with_destruct_cases)
       ]
 	g
     in
@@ -758,7 +767,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
-	 Pfedit.by (observe_tac ("procve correctness ("^(string_of_id f_id)^")") (proving_tac i));
+	 Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in 
 	 update_Function