Replacing the old version of "functional induction" with the new one.

The old version is, for now, still available by prefixing any command/tactic with Old/old (eg. old functional induction ...).


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

6 files changed, 92 insertions, 38 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 2dbf1d107a..119b155d06 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -322,7 +322,7 @@ let h_reduce_with_zeta =
 let rewrite_until_var arg_num eq_ids : tactic =
   let test_var g = 
     let _,args = destApp (pf_concl g) in 
-    isVar args.(arg_num)
+    not (isConstruct args.(arg_num))
   in
   let rec do_rewrite eq_ids g  = 
     if test_var g 
@@ -532,9 +532,9 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	     match kind_of_term new_term_value_eq with
 	       | App(f,[| _;_;args2 |]) -> args2
 	       | _ ->
-(* 		   observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++ *)
-(* 			      pr_lconstr_env (pf_env g') new_term_value_eq *)
-(* 			   ); *)
+		   observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
+			      pr_lconstr_env (pf_env g') new_term_value_eq
+			   );
 		   anomaly "cannot compute new term value"
 	   in
 	 let fun_body =
@@ -622,9 +622,9 @@ let build_proof
 	      let term_eq =
 		make_refl_eq type_of_term t
 	      in
-  	      tclTHENSEQ
+	      tclTHENSEQ
 		[
-		  h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps);
+		  h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
 		  thin dyn_infos.rec_hyps;
 		  pattern_option [[-1],t] None;
 		  h_simplest_case t;
@@ -744,7 +744,7 @@ let build_proof
 		] g
 	  | Rel _ -> anomaly "Free var in goal conclusion !" 
   and build_proof do_finalize dyn_infos g =
-(*     observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *)
+(*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
      (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
@@ -813,8 +813,9 @@ type static_fix_info =
       nb_realargs : int
     }
 
-let prove_rec_hyp fix_info  =
-  { proving_tac = 
+
+
+let prove_rec_hyp_for_struct fix_info = 
       (fun  eq_hyps -> tclTHEN 
 	(rewrite_until_var (fix_info.idx - 1) eq_hyps)
 	(fun g -> 
@@ -824,6 +825,9 @@ let prove_rec_hyp fix_info  =
 	   in
 	   refine rec_hyp_proof g
 	))
+
+let prove_rec_hyp fix_info  =
+  { proving_tac = prove_rec_hyp_for_struct fix_info
   ;
     is_valid = fun _ -> true 
   }
@@ -831,7 +835,26 @@ let prove_rec_hyp fix_info  =
 
 exception Not_Rec
     
-
+let generalize_non_dep hyp g = 
+  let hyps = [hyp] in 
+  let env = Global.env () in 
+  let hyp_typ = pf_type_of g (mkVar hyp) in 
+  let to_revert,_ = 
+    Environ.    fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
+      if List.mem hyp hyps
+	or List.exists (occur_var_in_decl env hyp) keep
+	or occur_var env hyp hyp_typ
+	or Termops.is_section_variable hyp (* should be dangerous *) 
+      then (clear,decl::keep)
+      else (hyp::clear,keep))
+      ~init:([],[]) (pf_env g)
+  in
+  observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert);
+  tclTHEN 
+    (observe_tac "h_generalize" (h_generalize (List.map mkVar to_revert)))
+    (observe_tac "thin" (thin to_revert))
+    g
+  
 let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic =
    fun goal ->
 (*      observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++  *)
@@ -974,7 +997,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams :
 		      try
 			if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec;
 			let nparams = List.length !params in
-			let args_as_constr = List.map mkVar  args in
+			let args_as_constr = List.map mkVar args in
 			let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in 
 			let other_args_as_constr = List.map mkVar  other_args in 
 			let rec_num,new_body =
@@ -982,7 +1005,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams :
 			  let f = fnames.(idx') in
 			  let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly ""
 			  in
-			  let name_of_f = Name ( id_of_label (con_label f)) in
+			  let name_of_f = Name (id_of_label (con_label f)) in
 			  let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in
 			  let idx'' = list_index name_of_f (Array.to_list na) - 1 in
 			  let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in
@@ -1002,11 +1025,11 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams :
 (* 			observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body); *)
 			let do_prove branches applied_body =
 			  build_proof
-			    interactive_proof
-			    (Array.to_list fnames)
-			    (Idmap.map prove_rec_hyp ptes_to_fixes)
-			    branches
-			    applied_body
+			       interactive_proof
+			       (Array.to_list fnames)
+			       (Idmap.map prove_rec_hyp ptes_to_fixes)
+			       branches
+			       applied_body
 			in
 			let replace_and_prove =
 			  tclTHENS
@@ -1025,11 +1048,18 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams :
 				      info = applied_body_with_real_args;
 				      eq_hyps = [];
 				    } ];
-			      let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in
-			      let id_as_induction_constr = Tacexpr.ElimOnConstr id in 
+			      let id = 
+				try
+				  List.nth (List.rev args_as_constr) (rec_num) 
+				with _ -> anomaly ("Cannot find recursive argument of function ! ") 
+			      in
 			      (tclTHENSEQ
-				 [new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *)
-				  intros_reflexivity
+				 [ 
+				   keep (!params@(List.map destVar args_as_constr));
+				   observe_tac "generalizing" (generalize_non_dep (destVar id));
+				   observe_tac "new_destruct" 
+				    (h_case (id,Rawterm.NoBindings));
+				  observe_tac "intros_reflexivity" intros_reflexivity
 				 ])
 			    ]
 			in
@@ -1077,7 +1107,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams :
 		let fix_info = Idmap.find (destVar pte) !pte_to_fix in
 		fix_info.nb_realargs
 	      with Not_found -> (* Not a recursive function *) 
-		nb_prod (pf_concl g)
+		nb_lam (Util.out_some !fbody_with_params)
+(* 		nb_prod (pf_concl g) *)
 	    in 
 	    observe_tac "" (tclTHEN
 	      (tclDO nb_real_args (observe_tac "intro" intro)) 
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 072c3d518d..fc5200202a 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -439,6 +439,8 @@ let get_funs_constant mp dp =
       with Not_Rec -> ()
     in
     l_const
+
+exception No_graph_found 
 	
 let make_scheme fas = 
   let env = Global.env () 
@@ -451,8 +453,10 @@ let make_scheme fas =
   let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in 
   let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in 
   let first_fun_kn = 
-    (* Fixme: take into accour funs_mp and funs_dp *)
+    try 
+    (* Fixme: take into account funs_mp and funs_dp *)
     fst (destInd (id_to_constr first_fun_rel_id))
+    with Not_found -> raise No_graph_found
   in
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
   let this_block_funs = Array.map fst this_block_funs_indexes in 
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
index 929c3db510..8b4faaf448 100644
--- a/contrib/funind/functional_principles_types.mli
+++ b/contrib/funind/functional_principles_types.mli
@@ -24,5 +24,8 @@ val generate_functional_principle :
 val compute_new_princ_type_from_rel : constr array -> sorts array -> 
   types -> types
 
+
+exception No_graph_found
+
 val make_scheme : (identifier*identifier*Rawterm.rawsort) list ->  unit
 val make_case_scheme : (identifier*identifier*Rawterm.rawsort)  ->  unit
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 2bad9bb504..bd48266a4f 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -82,8 +82,13 @@ let choose_dest_or_ind scheme_info =
 
 
 TACTIC EXTEND newfunind
-   ["new" "functional" "induction" constr(c) fun_ind_using(princl) with_names(pat)] -> 
+   ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
      [
+       let c = match cl with 
+	 | [] -> assert false
+	 | [c] -> c 
+	 | c::cl -> applist(c,cl)
+       in 
        let f,args = decompose_app c in 
        fun g -> 
 	 let princ = 
@@ -192,15 +197,26 @@ VERNAC ARGUMENT EXTEND fun_scheme_args
 END 
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-   ["New" "Functional" "Scheme" fun_scheme_args(fas) ] ->
+   ["Functional" "Scheme" fun_scheme_args(fas) ] ->
     [
-      Functional_principles_types.make_scheme fas
+      try 
+	Functional_principles_types.make_scheme fas
+      with Functional_principles_types.No_graph_found -> 
+	match fas with 
+	  | (_,fun_name,_)::_ -> 
+	      begin
+		make_graph fun_name;
+		try Functional_principles_types.make_scheme fas
+		with Functional_principles_types.No_graph_found -> 
+		  Util.error ("Cannot generate induction principle(s)")
+	      end
+	  | _ -> assert false (* we can only have non empty  list *)
     ]
 END
 
 
 VERNAC COMMAND EXTEND NewFunctionalCase
-   ["New" "Functional" "Case" fun_scheme_arg(fas) ] ->
+   ["Functional" "Case" fun_scheme_arg(fas) ] ->
     [
       Functional_principles_types.make_case_scheme fas
     ]
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index a12f1f01f3..2c7e4d33c3 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -772,11 +772,6 @@ let invfun_verif c l dorew gl =
    else error "wrong number of arguments for the function"
 
 
-TACTIC EXTEND functional_induction
-  [ "functional" "induction" constr(c)  ne_constr_list(l) ] 
-     -> [ invfun_verif c l true ]
-END
-
 
 
 (* Construction of the functional scheme. *)
@@ -847,15 +842,20 @@ let declareFunScheme f fname mutflist =
 
 
 
+TACTIC EXTEND functional_induction
+  [ "old" "functional" "induction" constr(c)  ne_constr_list(l) ] 
+     -> [ invfun_verif c l true ]
+END
+
 VERNAC COMMAND EXTEND FunctionalScheme
- [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
+ [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
     ident(c) "with" ne_ident_list(l) ] 
   -> [ declareFunScheme c na l ]
-| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
+| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
   -> [ declareFunScheme c na [] ]
 END
 
- 
+
 
 
 
diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v
index ee66f02a91..8827da1004 100644
--- a/contrib/rtauto/Bintree.v
+++ b/contrib/rtauto/Bintree.v
@@ -18,7 +18,7 @@ Open Scope positive_scope.
 Ltac clean := try (simpl; congruence). 
 Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 
-Functional Scheme Pcompare_ind := Induction for Pcompare.
+Functional Scheme Pcompare_ind := Induction for Pcompare Sort Prop.
 
 Lemma Prect : forall P : positive -> Type,
        P 1 ->
@@ -31,13 +31,13 @@ Qed.
 
 Lemma Gt_Eq_Gt : forall p q cmp,
        (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt.
-apply (Pcompare_ind (fun p q cmp => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt));
+apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt));
 simpl;auto;congruence.
 Qed.
 
 Lemma Gt_Lt_Gt : forall p q cmp,
        (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt.
-apply (Pcompare_ind (fun p q cmp => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt));
+apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt));
 simpl;auto;congruence.
 Qed.