Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 1538 insertions, 0 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
new file mode 100644
index 00000000..f0e986fb
--- /dev/null
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -0,0 +1,1538 @@
+open Printer
+open Util
+open Term
+open Termops 
+open Names 
+open Declarations
+open Pp
+open Entries
+open Hiddentac
+open Evd
+open Tacmach
+open Proof_type
+open Tacticals
+open Tactics
+open Indfun_common
+open Libnames
+
+let msgnl = Pp.msgnl
+
+let do_observe () = 
+  Tacinterp.get_debug () <> Tactic_debug.DebugOff  
+
+
+let observe strm =
+  if do_observe ()
+  then Pp.msgnl strm
+  else ()
+
+let observennl strm =
+  if do_observe ()
+  then begin Pp.msg strm;Pp.pp_flush () end
+  else ()
+
+
+
+
+let do_observe_tac s tac g =
+ try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
+ with e ->
+   let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+   msgnl (str "observation "++ s++str " raised exception " ++ 
+	    Cerrors.explain_exn e ++ str " on goal " ++ goal ); 
+   raise e;;
+
+
+let observe_tac s tac g =
+  if do_observe ()
+  then do_observe_tac (str s) tac g
+  else tac g
+
+
+let tclTRYD tac = 
+  if  !Options.debug  || do_observe ()
+  then (fun g -> try (* do_observe_tac ""  *)tac g with _ -> tclIDTAC g)
+  else tac
+
+
+let list_chop ?(msg="") n l = 
+  try 
+    list_chop n l 
+  with Failure (msg') -> 
+    failwith (msg ^ msg')
+  
+
+let make_refl_eq type_of_t t  =
+  let refl_equal_term = Lazy.force refl_equal in
+  mkApp(refl_equal_term,[|type_of_t;t|])
+
+
+type pte_info = 
+    { 
+      proving_tac : (identifier list ->  Tacmach.tactic);
+      is_valid : constr -> bool
+    }
+
+type ptes_info = pte_info Idmap.t
+
+type 'a dynamic_info = 
+    { 
+      nb_rec_hyps : int;
+      rec_hyps : identifier list ; 
+      eq_hyps : identifier list;
+      info : 'a
+    }
+
+type body_info = constr dynamic_info 
+      
+
+let finish_proof dynamic_infos g = 
+  observe_tac "finish" 
+    ( h_assumption)
+    g
+	  
+
+let refine c = 
+  Tacmach.refine_no_check c
+
+let thin l = 
+  Tacmach.thin_no_check l
+  
+
+let cut_replacing id t tac :tactic= 
+  tclTHENS (cut t)
+    [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
+      tac 
+    ]
+
+let intro_erasing id = tclTHEN (thin [id]) (introduction id)
+
+
+
+let rec_hyp_id = id_of_string "rec_hyp"
+
+let is_trivial_eq t = 
+  match kind_of_term t with 
+    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+	eq_constr t1 t2
+    | _ -> false 
+
+
+let rec incompatible_constructor_terms t1 t2 = 
+  let c1,arg1 = decompose_app t1 
+  and c2,arg2 = decompose_app t2 
+  in 
+  (not (eq_constr t1 t2)) &&
+    isConstruct c1 && isConstruct c2 && 
+    (
+      not (eq_constr c1 c2) || 
+	List.exists2 incompatible_constructor_terms arg1 arg2
+    )
+
+let is_incompatible_eq t = 
+  match kind_of_term t with 
+    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+	incompatible_constructor_terms t1 t2
+    | _ -> false 
+
+let change_hyp_with_using msg hyp_id t tac : tactic = 
+  fun g -> 
+    let prov_id = pf_get_new_id hyp_id g in 
+    tclTHENS
+      (observe_tac msg (forward (Some  (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
+      [tclTHENLIST 
+      [	
+	observe_tac "change_hyp_with_using thin" (thin [hyp_id]);
+	observe_tac "change_hyp_with_using rename " (h_rename prov_id hyp_id)
+      ]] g
+
+exception TOREMOVE
+
+
+let prove_trivial_eq h_id context (type_of_term,term) = 
+  let nb_intros = List.length context in 
+  tclTHENLIST
+    [
+      tclDO nb_intros intro; (* introducing context *)
+      (fun g -> 
+	 let context_hyps =  
+	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) 
+	 in
+	 let context_hyps' = 
+	   (mkApp(Lazy.force refl_equal,[|type_of_term;term|]))::
+	     (List.map mkVar context_hyps)
+	 in
+	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in 
+	 refine to_refine g
+      )
+    ]
+
+
+let isAppConstruct t = 
+  if isApp t 
+  then isConstruct (fst (destApp t))
+  else false 
+
+
+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    ); *)
+      failwith "NoChange"; 
+    end
+  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";
+    let f_eq,args = destApp t in
+    if not (eq_constr f_eq (Lazy.force eq)) then nochange "not an equality";
+    let t1 = args.(1) 
+    and t2 = args.(2) 
+    and t1_typ = args.(0)
+    in 
+    if not (closed0 t1) then nochange "not a closed lhs";    
+    let rec compute_substitution sub t1 t2 = 
+      if isRel t2 
+      then 
+	let t2 = destRel t2  in 
+	begin 
+	  try 
+	    let t1' = Intmap.find t2 sub in 
+	    if not (eq_constr t1 t1') then nochange "twice bound variable";
+	    sub
+	  with Not_found -> 
+	    assert (closed0 t1);
+	    Intmap.add t2 t1 sub
+	end
+      else if isAppConstruct t1 && isAppConstruct t2 
+      then 
+	begin
+	  let c1,args1 = destApp t1 
+	  and c2,args2 = destApp t2 
+	  in 
+	  if not (eq_constr c1 c2) then anomaly "deconstructing equation";
+	  array_fold_left2 compute_substitution sub args1 args2
+	end
+      else 
+	if (eq_constr t1 t2) then sub else nochange "cannot solve"
+    in
+    let sub = compute_substitution Intmap.empty t1 t2 in 
+    let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) 
+    let new_end_of_type = 
+      (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 
+	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
+      *)
+      let sub' = Intmap.fold (fun i t acc -> (i,t)::acc) sub [] in 
+      let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in 
+      List.fold_left (fun end_of_type (i,t)  -> lift 1 (substnl  [t] (i-1) end_of_type))
+	end_of_type_with_pop
+	sub''
+    in
+    (* let new_end_of_type =  *)
+    (*  Intmap.fold *)
+    (* 	(fun i t end_of_type -> lift 1 (substnl  [t] (i-1) end_of_type)) *)
+    (* 	sub *)
+    (* 	end_of_type_with_pop *)
+    (*     in *)
+    let old_context_length = List.length context + 1 in
+    let witness_fun = 
+      mkLetIn(Anonymous,make_refl_eq t1_typ t1,t,
+	       mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
+	      )
+    in
+    let new_type_of_hyp,ctxt_size,witness_fun = 
+      list_fold_left_i 
+	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> 
+	   try 
+	     let witness = Intmap.find i sub in 
+	     if b' <> None then anomaly "can not redefine a rel!";
+	     (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
+	   with Not_found  -> 
+	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
+	)
+	1 
+	(new_end_of_type,0,witness_fun)
+	context
+    in
+    let new_type_of_hyp = Reductionops.nf_betaiota  new_type_of_hyp in 
+    let new_ctxt,new_end_of_type = 
+      Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp 
+    in 
+    let prove_new_hyp : tactic = 
+      tclTHEN
+	(tclDO ctxt_size intro)
+	(fun g ->
+	   let all_ids = pf_ids_of_hyps g in 
+	   let new_ids,_  = list_chop ctxt_size all_ids in 
+	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in 
+	   refine to_refine g
+	)
+    in
+    let simpl_eq_tac = 
+      change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp prove_new_hyp
+    in
+(*     observe (str "In " ++ Ppconstr.pr_id hyp_id ++  *)
+(* 	       str "removing an equation " ++ fnl ()++  *)
+(* 	       str "old_typ_of_hyp :=" ++ *)
+(* 	       Printer.pr_lconstr_env *)
+(* 	       env *)
+(* 	       (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) *)
+(* 	     ++ fnl () ++ *)
+(* 	       str "new_typ_of_hyp := "++  *)
+(* 	       Printer.pr_lconstr_env env new_type_of_hyp ++ fnl () *)
+(* 	     ++ str "old context := " ++ pr_rel_context env context ++ fnl ()  *)
+(* 	     ++ str "new context := " ++ pr_rel_context env new_ctxt ++ fnl ()  *)
+(* 	     ++ str "old type  := " ++ pr_lconstr end_of_type ++ fnl ()  *)
+(* 	     ++ str "new type := " ++ pr_lconstr new_end_of_type ++ fnl ()  *)
+(* ); *)
+    new_ctxt,new_end_of_type,simpl_eq_tac
+
+
+let is_property ptes_info t_x full_type_of_hyp = 
+  if isApp t_x 
+  then 
+    let pte,args = destApp t_x in 
+    if isVar pte && array_for_all closed0 args 
+    then 
+      try 
+	let info = Idmap.find (destVar pte) ptes_info in 
+	info.is_valid full_type_of_hyp	  
+      with Not_found -> false 
+    else false 
+  else false 
+
+let isLetIn t = 
+  match kind_of_term t with 
+    | LetIn _ -> true 
+    | _ -> false 
+
+
+let h_reduce_with_zeta = 	 
+  h_reduce 
+    (Rawterm.Cbv
+       {Rawterm.all_flags 
+	with Rawterm.rDelta = false; 		 
+       })
+  
+
+
+let rewrite_until_var arg_num eq_ids : tactic =
+  let test_var g = 
+    let _,args = destApp (pf_concl g) in 
+    not (isConstruct args.(arg_num))
+  in
+  let rec do_rewrite eq_ids g  = 
+    if test_var g 
+    then tclIDTAC g
+    else
+      match eq_ids with 
+	| [] -> anomaly "Cannot find a way to prove recursive property";
+	| eq_id::eq_ids -> 
+	    tclTHEN 
+	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+	      (do_rewrite eq_ids)
+	      g
+  in
+  do_rewrite eq_ids
+
+
+let rec_pte_id = id_of_string "Hrec" 
+let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = 
+  let coq_False = Coqlib.build_coq_False () in 
+  let coq_True = Coqlib.build_coq_True () in 
+  let coq_I = Coqlib.build_coq_I () in 
+  let rec scan_type  context type_of_hyp : tactic = 
+    if isLetIn type_of_hyp then 
+      let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
+      let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in 
+      (* length of context didn't change ? *)
+      let new_context,new_typ_of_hyp = 
+	 Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
+      in
+        tclTHENLIST 
+	[
+	  h_reduce_with_zeta
+	    (Tacticals.onHyp hyp_id)
+	  ;
+	  scan_type new_context new_typ_of_hyp 
+	  
+	]
+    else if isProd type_of_hyp 
+    then 
+      begin 
+	let (x,t_x,t') = destProd type_of_hyp in	
+	let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in 
+	if is_property ptes_infos t_x actual_real_type_of_hyp then
+	  begin
+	    let pte,pte_args =  (destApp t_x) in 
+	    let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in 
+	    let popped_t' = pop t' in 
+	    let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in 
+	    let prove_new_type_of_hyp = 
+	      let context_length = List.length context in 
+	      tclTHENLIST
+		[ 
+		  tclDO context_length intro; 
+		  (fun g ->  
+		     let context_hyps_ids = 
+		       fst (list_chop ~msg:"rec hyp : context_hyps"
+			      context_length (pf_ids_of_hyps g))
+		     in
+		     let rec_pte_id = pf_get_new_id rec_pte_id g in 
+		     let to_refine = 
+		       applist(mkVar hyp_id,
+			       List.rev_map mkVar (rec_pte_id::context_hyps_ids)
+			      )
+		     in
+		     observe_tac "rec hyp "
+		       (tclTHENS
+		       (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x)
+		       [observe_tac "prove rec hyp" (prove_rec_hyp eq_hyps);
+			observe_tac "prove rec hyp"
+			  (refine to_refine)
+		       ])
+		       g
+		  )
+		]
+	    in
+	    tclTHENLIST 
+	      [
+		observe_tac "hyp rec" 
+		  (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp);
+		scan_type context popped_t'
+	      ]
+	  end
+	else if eq_constr t_x coq_False then 
+	  begin
+(* 	    observe (str "Removing : "++ Ppconstr.pr_id hyp_id++  *)
+(* 		       str " since it has False in its preconds " *)
+(* 		    ); *)
+	    raise TOREMOVE;  (* False -> .. useless *)
+	  end
+	else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *) 
+	else if eq_constr t_x coq_True  (* Trivial => we remove this precons *)
+	then 
+(* 	    observe (str "In "++Ppconstr.pr_id hyp_id++  *)
+(* 		       str " removing useless precond True" *)
+(* 		    );  *)
+	  let popped_t' = pop t' in
+	  let real_type_of_hyp = 
+	    it_mkProd_or_LetIn ~init:popped_t' context 
+	  in 
+	  let prove_trivial =  
+	    let nb_intro = List.length context in 
+	    tclTHENLIST [
+	      tclDO nb_intro intro;
+	      (fun g -> 
+		 let context_hyps = 
+		   fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
+		 in
+		 let to_refine = 
+		   applist (mkVar hyp_id,
+			    List.rev (coq_I::List.map mkVar context_hyps)
+			   )
+		 in
+		 refine to_refine g
+	      )
+	    ]
+	  in
+	  tclTHENLIST[
+	    change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp 
+	      (observe_tac "prove_trivial" prove_trivial);
+	    scan_type context popped_t'
+	  ]
+	else if is_trivial_eq t_x 
+	then (*  t_x :=  t = t   => we remove this precond *) 
+	  let popped_t' = pop t' in
+	  let real_type_of_hyp =
+	    it_mkProd_or_LetIn ~init:popped_t' context
+	  in
+	  let _,args = destApp t_x in
+	  tclTHENLIST
+	    [
+	      change_hyp_with_using
+		"prove_trivial_eq"
+		hyp_id
+		real_type_of_hyp
+		(observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1))));
+	      scan_type context popped_t'
+	    ] 
+	else 
+	  begin
+	    try 
+	      let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in 
+	      tclTHEN
+		tac 
+		(scan_type new_context new_t')
+	    with Failure "NoChange" -> 
+	      (* Last thing todo : push the rel in the context and continue *) 
+	      scan_type ((x,None,t_x)::context) t'
+	  end
+      end
+    else
+      tclIDTAC
+  in 
+  try 
+    scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
+  with TOREMOVE -> 
+    thin [hyp_id],[]
+
+
+let clean_goal_with_heq ptes_infos continue_tac dyn_infos  = 
+  fun g -> 
+    let env = pf_env g 
+    and sigma = project g 
+    in
+    let tac,new_hyps = 
+      List.fold_left ( 
+	fun (hyps_tac,new_hyps) hyp_id ->
+	  let hyp_tac,new_hyp = 
+	    clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma 
+	  in
+	  (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps
+      )
+	(tclIDTAC,[])
+	dyn_infos.rec_hyps
+    in
+    let new_infos = 
+      { dyn_infos with 
+	  rec_hyps = new_hyps; 
+	  nb_rec_hyps  = List.length new_hyps
+      }
+    in
+    tclTHENLIST 
+      [
+	tac ;
+	(continue_tac new_infos)
+      ]
+      g    
+
+let heq_id = id_of_string "Heq"
+
+let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = 
+  fun g -> 
+    let heq_id = pf_get_new_id heq_id g in 
+    let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
+    tclTHENLIST
+      [ 
+	(* We first introduce the variables *) 
+	tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
+	(* Then the equation itself *)
+	introduction_no_check heq_id;
+	(* Then the new hypothesis *) 
+	tclMAP introduction_no_check dyn_infos.rec_hyps;
+	observe_tac "after_introduction" (fun g' -> 
+	   (* We get infos on the equations introduced*)
+	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in 
+	   (* compute the new value of the body *)
+	   let new_term_value =
+	     match kind_of_term new_term_value_eq with
+	       | App(f,[| _;_;args2 |]) -> args2
+	       | _ ->
+		   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 =
+	   mkLambda(Anonymous,
+		    pf_type_of g' term,
+		    replace_term term (mkRel 1) dyn_infos.info
+		   )
+	 in
+	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
+	 let new_infos = 
+	   {dyn_infos with 
+	      info = new_body;
+	      eq_hyps = heq_id::dyn_infos.eq_hyps
+	   }
+	 in 
+	 clean_goal_with_heq ptes_infos continue_tac new_infos  g'
+      )
+    ]
+      g
+
+
+let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = 
+  let args = Array.of_list (List.map mkVar  args_id) in 
+  let instanciate_one_hyp hid = 
+    tclORELSE
+      ( (* we instanciate the hyp if possible  *)
+	fun g -> 
+	  let prov_hid = pf_get_new_id hid g in
+	  tclTHENLIST[
+	    forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+	    thin [hid];
+	    h_rename prov_hid hid
+	  ] g
+      )
+      ( (*
+	  if not then we are in a mutual function block 
+	  and this hyp is a recursive hyp on an other function.
+	  
+	  We are not supposed to use it while proving this 
+	  principle so that we can trash it 
+	  
+	*)
+	(fun g -> 
+(* 	   observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *)
+	   thin [hid] g
+	)
+      )
+  in
+  if args_id = []  
+  then 
+    tclTHENLIST [
+      tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+      do_prove hyps
+    ]
+  else
+    tclTHENLIST
+      [
+	tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+	tclMAP instanciate_one_hyp hyps;
+	(fun g ->  
+	   let all_g_hyps_id = 
+	     List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
+	   in 
+	   let remaining_hyps = 
+	     List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
+	   in
+	   do_prove remaining_hyps g
+	  )
+      ]
+
+let build_proof 
+    (interactive_proof:bool)
+    (fnames:constant list)
+    ptes_infos
+    dyn_infos
+    : tactic =
+  let rec build_proof_aux do_finalize dyn_infos : tactic = 
+    fun g -> 
+      
+(*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
+	match kind_of_term dyn_infos.info with 
+	  | Case(_,_,t,_) -> 
+	      let g_nb_prod = nb_prod (pf_concl g) in
+	      let type_of_term = pf_type_of g t in
+	      let term_eq =
+		make_refl_eq type_of_term t
+	      in
+	      tclTHENSEQ
+		[
+		  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;
+		  (fun g' -> 
+		     let g'_nb_prod = nb_prod (pf_concl g') in 
+		     let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
+		     observe_tac "treat_new_case" 
+		       (treat_new_case  
+		       ptes_infos
+		       nb_instanciate_partial 
+		       (build_proof do_finalize) 
+		       t 
+		       dyn_infos)
+		       g'
+		  )
+		  
+		] g
+	  | Lambda(n,t,b) ->
+	      begin
+		match kind_of_term( pf_concl g) with
+		  | Prod _ ->
+		      tclTHEN
+			intro
+			(fun g' ->
+			   let (id,_,_) = pf_last_hyp g' in
+			   let new_term = 
+			     pf_nf_betaiota g' 
+			       (mkApp(dyn_infos.info,[|mkVar id|])) 
+			   in
+			   let new_infos = {dyn_infos with info = new_term} in
+			   let do_prove new_hyps = 
+			     build_proof do_finalize 
+			       {new_infos with
+			       	  rec_hyps = new_hyps; 
+				  nb_rec_hyps  = List.length new_hyps
+			       }
+			   in 
+			   observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
+			     (* 			   build_proof do_finalize new_infos g' *)
+			) g
+		  | _ ->
+		      do_finalize dyn_infos g 
+	      end
+	  | Cast(t,_,_) -> 
+	      build_proof do_finalize {dyn_infos with info = t} g
+	  | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+	      do_finalize dyn_infos g
+	  | App(_,_) ->
+	      let f,args = decompose_app dyn_infos.info in
+	      begin
+		match kind_of_term f with
+		  | App _ -> assert false (* we have collected all the app in decompose_app *)
+		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
+		      let new_infos = 
+			{ dyn_infos with 
+			    info = (f,args)
+			}
+		      in
+		      build_proof_args do_finalize new_infos  g
+		  | Const c when not (List.mem c fnames) ->
+		      let new_infos = 
+			{ dyn_infos with 
+			    info = (f,args)
+			}
+		      in
+(* 		      Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
+		      build_proof_args do_finalize new_infos g
+		  | Const _ ->
+		      do_finalize dyn_infos  g
+		  | Lambda _ -> 
+		      let new_term = Reductionops.nf_beta dyn_infos.info in 
+		      build_proof do_finalize {dyn_infos with info = new_term} 
+			g
+		  | LetIn _ -> 
+		      let new_infos = 
+			{ dyn_infos with info = nf_betaiotazeta dyn_infos.info } 
+		      in 
+
+		      tclTHENLIST 
+			[tclMAP 
+			   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
+			   dyn_infos.rec_hyps;
+			 h_reduce_with_zeta Tacticals.onConcl;
+			 build_proof do_finalize new_infos
+			] 
+			g
+		  | Cast(b,_,_) -> 
+		      build_proof do_finalize {dyn_infos with info = b } g
+		  | Case _ | Fix _ | CoFix _ ->
+		      let new_finalize dyn_infos = 
+			let new_infos = 
+			  { dyn_infos with 
+			      info = dyn_infos.info,args
+			  }
+			in 
+			build_proof_args do_finalize new_infos 
+		      in 
+		      build_proof new_finalize {dyn_infos  with info = f } g
+	      end
+	  | Fix _ | CoFix _ ->
+	      error ( "Anonymous local (co)fixpoints are not handled yet")
+
+	  | Prod _ -> error "Prod" 
+	  | LetIn _ -> 
+	      let new_infos = 
+		{ dyn_infos with 
+		    info = nf_betaiotazeta dyn_infos.info 
+		}
+	      in 
+
+	      tclTHENLIST 
+		[tclMAP 
+		   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
+		   dyn_infos.rec_hyps;
+		 h_reduce_with_zeta Tacticals.onConcl;
+		 build_proof do_finalize new_infos
+		] g
+	  | Rel _ -> anomaly "Free var in goal conclusion !" 
+  and build_proof do_finalize dyn_infos 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 ->
+(*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
+(*      then msgnl (str "build_proof_args with "  ++  *)
+(* 		   pr_lconstr_env (pf_env g) f_args' *)
+(* 		); *)
+      let (f_args',args) = dyn_infos.info in 
+      let tac : tactic =
+	fun g -> 
+	match args with
+	  | []  ->
+	      do_finalize {dyn_infos with info = f_args'} g 
+	  | arg::args ->
+(* 		observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
+(* 			fnl () ++  *)
+(* 			pr_goal (Tacmach.sig_it g) *)
+(* 			); *)
+	      let do_finalize dyn_infos =
+		let new_arg = dyn_infos.info in 
+		(* 		tclTRYD *)
+		(build_proof_args
+		   do_finalize
+		   {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
+		)
+	      in
+	      build_proof do_finalize 
+		{dyn_infos with info = arg }
+		g
+      in
+      observe_tac "build_proof_args" (tac ) g
+   in
+   let do_finish_proof dyn_infos = 
+     (* tclTRYD *) (clean_goal_with_heq 
+      ptes_infos
+      finish_proof dyn_infos)
+  in
+  observe_tac "build_proof"
+    (build_proof do_finish_proof dyn_infos) 
+
+
+
+
+
+
+
+
+
+
+
+
+(* Proof of principles from structural functions *) 
+let is_pte_type t =
+  isSort (snd (decompose_prod t))
+    
+let is_pte (_,_,t) = is_pte_type t
+
+
+
+
+type static_fix_info = 
+    {
+      idx : int;
+      name : identifier;
+      types : types;
+      offset : int;
+      nb_realargs : int;
+      body_with_param : constr 
+    }
+
+
+
+let prove_rec_hyp_for_struct fix_info = 
+      (fun  eq_hyps -> tclTHEN 
+	(rewrite_until_var (fix_info.idx) eq_hyps)
+	(fun g -> 
+	   let _,pte_args = destApp (pf_concl g) in 
+	   let rec_hyp_proof = 
+	     mkApp(mkVar fix_info.name,array_get_start pte_args) 
+	   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 
+  }
+
+
+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 id_of_decl (na,_,_) =  (Nameops.out_name na)
+let var_of_decl decl = mkVar (id_of_decl decl)
+let revert idl = 
+  tclTHEN 
+    (generalize (List.map mkVar idl)) 
+    (thin idl)
+
+
+let do_replace params rec_arg_num rev_args_id fun_to_replace body = 
+  fun g ->
+    let nb_intro_to_do = nb_prod (pf_concl g) in
+    tclTHEN
+      (tclDO nb_intro_to_do intro)
+      (
+	fun g' -> 
+	  let just_introduced = nLastHyps nb_intro_to_do g' in 
+	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in 
+	  let old_rev_args_id = rev_args_id in 
+	  let rev_args_id = just_introduced_id@rev_args_id in 
+	  let to_replace = 
+	    Reductionops.nf_betaiota (substl (List.map mkVar rev_args_id) fun_to_replace )
+	  and by = 
+	    Reductionops.nf_betaiota (applist(body,List.rev_map mkVar rev_args_id)) 
+	  in 
+(* 	  observe (str "to_replace := " ++ pr_lconstr_env (pf_env g') to_replace); *)
+(* 	  observe (str "by := " ++ pr_lconstr_env (pf_env g') by); *)
+	  let prove_replacement = 
+	    let rec_id = List.nth (List.rev old_rev_args_id) (rec_arg_num) in 
+	    observe_tac "prove_replacement"
+	      (tclTHENSEQ
+		 [ 
+		   revert just_introduced_id;
+		   keep ((List.map id_of_decl params)@ old_rev_args_id);
+		   generalize_non_dep rec_id;
+		   observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings)); 
+		   intros_reflexivity
+		 ]
+	      )
+	  in
+	  tclTHENS
+	    (observe_tac "replacement" (Equality.replace to_replace by))
+	    [ revert just_introduced_id;
+	     tclSOLVE [prove_replacement]]
+	    g'
+      )
+      g
+    
+
+
+let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
+  fun g -> 
+    let princ_type = pf_concl g in 
+    let princ_info = compute_elim_sig princ_type in 
+    let fresh_id = 
+      let avoid = ref (pf_ids_of_hyps g) in 
+      (fun na -> 
+	 let new_id = 
+	   match na with 
+	       Name id -> fresh_id !avoid (string_of_id id) 
+	     | Anonymous -> fresh_id !avoid "H"
+	 in
+	 avoid := new_id :: !avoid; 
+	 (Name new_id)
+      )
+    in
+    let fresh_decl = 
+      (fun (na,b,t) -> 
+	 (fresh_id na,b,t)
+      )
+    in
+    let princ_info : elim_scheme = 
+      { princ_info with 
+	  params = List.map fresh_decl princ_info.params;
+	  predicates = List.map fresh_decl princ_info.predicates; 
+	  branches = List.map fresh_decl princ_info.branches; 
+	  args = List.map fresh_decl princ_info.args
+      }
+    in
+    let get_body const =
+      match (Global.lookup_constant const ).const_body with
+	| Some b ->
+	     let body = force b in
+	     Tacred.cbv_norm_flags
+	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+	       (Global.env ())
+	       (Evd.empty)
+	       body
+	| None -> error ( "Cannot define a principle over an axiom ")
+    in
+    let fbody = get_body fnames.(fun_num) in
+    let f_ctxt,f_body = decompose_lam fbody in 
+    let f_ctxt_length = List.length f_ctxt in 
+    let diff_params = princ_info.nparams - f_ctxt_length in 
+    let full_params,princ_params,fbody_with_full_params = 
+      if diff_params > 0
+      then 
+	let princ_params,full_params = 
+	  list_chop  diff_params princ_info.params 
+	in 
+	(full_params, (* real params *)
+	 princ_params, (* the params of the principle which are not params of the function *)
+	 substl (* function instanciated with real params *)
+	   (List.map var_of_decl full_params)
+	   f_body
+	)
+      else
+	let f_ctxt_other,f_ctxt_params = 
+	  list_chop (- diff_params) f_ctxt in 
+	let f_body = compose_lam f_ctxt_other f_body in 
+	(princ_info.params, (* real params *)
+	 [],(* all params are full params *)
+	 substl (* function instanciated with real params *)
+	   (List.map var_of_decl princ_info.params)
+	   f_body
+	)
+    in
+(*     observe (str "full_params := " ++  *)
+(* 	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
+(* 	       full_params *)
+(* 	    );  *)
+(*     observe (str "princ_params := " ++  *)
+(* 	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
+(* 	       princ_params *)
+(* 	    );  *)
+(*     observe (str "fbody_with_full_params := " ++  *)
+(* 	       pr_lconstr fbody_with_full_params *)
+(* 	    );  *)
+    let all_funs_with_full_params = 
+      Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
+    in
+    let fix_offset = List.length princ_params in 
+    let ptes_to_fix,infos = 
+      match kind_of_term fbody_with_full_params with 
+	| Fix((idxs,i),(names,typess,bodies)) -> 
+	    let bodies_with_all_params = 
+	      Array.map 
+		(fun body -> 
+		   Reductionops.nf_betaiota 
+		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
+			      List.rev_map var_of_decl princ_params))
+		)
+		bodies
+	    in
+	    let info_array = 
+	      Array.mapi 
+		(fun i types -> 
+		   let types = prod_applist types (List.rev_map var_of_decl princ_params) in
+		   { idx = idxs.(i)  - fix_offset;
+		     name = Nameops.out_name (fresh_id names.(i));
+		     types = types; 
+		     offset = fix_offset;
+		     nb_realargs = 
+		       List.length 
+			 (fst (decompose_lam bodies.(i))) - fix_offset;
+		     body_with_param = bodies_with_all_params.(i)
+		   }
+		)
+		typess
+	    in
+	    let pte_to_fix,rev_info = 
+	      list_fold_left_i 
+		(fun i (acc_map,acc_info) (pte,_,_) -> 
+		   let infos = info_array.(i) in 
+		   let type_args,_ = decompose_prod infos.types in 
+		   let nargs = List.length type_args in 
+		   let f = applist(mkConst fnames.(i), List.rev_map var_of_decl princ_info.params) in
+		   let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
+		   let app_f = mkApp(f,first_args) in
+		   let pte_args = (Array.to_list first_args)@[app_f] in 
+		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in 
+		   let body_with_param = 
+		     let body = get_body fnames.(i) in 
+		     let body_with_full_params = 
+		       Reductionops.nf_betaiota (
+			 applist(body,List.rev_map var_of_decl full_params))
+		     in
+		     match kind_of_term body_with_full_params with 
+		       | Fix((_,num),(_,_,bs)) -> 
+			       Reductionops.nf_betaiota
+				 (
+				   (applist
+				      (substl 
+					 (List.rev 
+					    (Array.to_list all_funs_with_full_params)) 
+					 bs.(num),
+				       List.rev_map var_of_decl princ_params))
+				 )
+			 | _ -> error "Not a mutual block"
+		   in
+		   let info = 
+		     {infos with 
+			types = compose_prod type_args app_pte;
+			 body_with_param = body_with_param
+		     }
+		   in 
+(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
+(* 			      str " to " ++ Ppconstr.pr_id info.name); *)
+		   (Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info)
+		   )
+		0 
+		(Idmap.empty,[]) 
+		(List.rev princ_info.predicates)
+	    in
+	    pte_to_fix,List.rev rev_info
+	| _ -> Idmap.empty,[]
+    in
+    let mk_fixes : tactic = 
+      let pre_info,infos = list_chop fun_num infos in 
+      match pre_info,infos with 
+	| [],[] -> tclIDTAC
+	| _, this_fix_info::others_infos -> 
+	    let other_fix_infos =
+	      List.map
+		(fun fi -> fi.name,fi.idx + 1 ,fi.types) 
+		(pre_info@others_infos)
+	    in 
+	    if other_fix_infos = [] 
+	    then
+	      observe_tac ("h_fix") (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
+	    else
+	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+		other_fix_infos
+	| _ -> anomaly "Not a valid information"
+    in
+    let first_tac : tactic = (* every operations until fix creations *)
+      tclTHENSEQ 
+	[ observe_tac "introducing params" (intros_using (List.rev_map id_of_decl princ_info.params)); 
+	  observe_tac "introducing predictes" (intros_using (List.rev_map id_of_decl princ_info.predicates)); 
+	  observe_tac "introducing branches" (intros_using (List.rev_map id_of_decl princ_info.branches)); 
+	  observe_tac "building fixes" mk_fixes;
+	]
+    in
+    let intros_after_fixes : tactic = 
+      fun gl -> 
+	let ctxt,pte_app =  (Sign.decompose_prod_assum (pf_concl gl)) in
+	let pte,pte_args = (decompose_app pte_app) in
+	try
+	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in 
+	  let fix_info = Idmap.find  pte ptes_to_fix in
+	  let nb_args = fix_info.nb_realargs in 
+	  tclTHENSEQ
+	    [
+	      observe_tac ("introducing args") (tclDO nb_args intro);
+	      (fun g -> (* replacement of the function by its body *)
+		 let args = nLastHyps nb_args g in 
+		 let fix_body = fix_info.body_with_param in
+(* 		 observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
+		 let args_id = List.map (fun (id,_,_) -> id) args in
+		 let dyn_infos = 
+		   {
+		     nb_rec_hyps = -100;
+		     rec_hyps = [];
+		     info = 
+		       Reductionops.nf_betaiota 
+			 (applist(fix_body,List.rev_map mkVar args_id));
+		     eq_hyps = []
+		   }
+		 in
+		 tclTHENSEQ
+		   [
+		     observe_tac "do_replace" 
+		       (do_replace princ_info.params fix_info.idx args_id
+			  (List.hd (List.rev pte_args)) fix_body);
+		     let do_prove = 
+		       build_proof 
+			 interactive_proof
+			 (Array.to_list fnames) 
+			 (Idmap.map prove_rec_hyp ptes_to_fix)
+		     in
+		     let prove_tac branches  = 
+		       let dyn_infos = 
+			 {dyn_infos with 
+			    rec_hyps = branches;
+			    nb_rec_hyps = List.length branches
+			 }
+		       in
+		       clean_goal_with_heq
+			 (Idmap.map prove_rec_hyp ptes_to_fix) 
+			 do_prove 
+			 dyn_infos
+		     in
+(* 		     observe (str "branches := " ++  *)
+(* 				prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches); *)
+		     observe_tac "instancing" (instanciate_hyps_with_args prove_tac 
+		       (List.rev_map id_of_decl princ_info.branches) 
+		       (List.rev args_id))
+		   ]
+		   g
+	      );
+	    ] gl
+	with Not_found ->
+	  let nb_args = min (princ_info.nargs) (List.length ctxt) in
+	  tclTHENSEQ
+	    [
+	      tclDO nb_args intro;
+	      (fun g -> (* replacement of the function by its body *)
+		 let args = nLastHyps nb_args g in 
+		 let args_id = List.map (fun (id,_,_) -> id) args in
+		 let dyn_infos = 
+		   {
+		     nb_rec_hyps = -100;
+		     rec_hyps = [];
+		     info = 
+		       Reductionops.nf_betaiota 
+			 (applist(fbody_with_full_params,
+				  (List.rev_map var_of_decl princ_params)@
+				    (List.rev_map mkVar args_id)
+				 ));
+		     eq_hyps = []
+		   }
+		 in
+		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
+		 tclTHENSEQ
+		   [unfold_in_concl [([],Names.EvalConstRef fname)];
+		    let do_prove = 
+		      build_proof 
+			interactive_proof
+			(Array.to_list fnames) 
+			 (Idmap.map prove_rec_hyp ptes_to_fix)
+		    in
+		    let prove_tac branches  = 
+		      let dyn_infos = 
+			 {dyn_infos with 
+			    rec_hyps = branches;
+			    nb_rec_hyps = List.length branches
+			 }
+		      in
+		       clean_goal_with_heq
+			 (Idmap.map prove_rec_hyp ptes_to_fix) 
+			 do_prove 
+			 dyn_infos
+		    in
+		    instanciate_hyps_with_args prove_tac 
+		       (List.rev_map id_of_decl princ_info.branches) 
+		      (List.rev args_id)
+		   ]
+		   g
+	      )
+	    ] 
+	  gl
+    in
+    tclTHEN 
+      first_tac
+      intros_after_fixes
+      g
+	    
+
+
+
+
+
+(* Proof of principles of general functions *) 
+let h_id = Recdef.h_id
+and hrec_id = Recdef.hrec_id
+and acc_inv_id = Recdef.acc_inv_id
+and ltof_ref = Recdef.ltof_ref
+and acc_rel = Recdef.acc_rel
+and well_founded = Recdef.well_founded
+and delayed_force = Recdef.delayed_force
+and h_intros = Recdef.h_intros
+and list_rewrite = Recdef.list_rewrite
+and evaluable_of_global_reference = Recdef.evaluable_of_global_reference
+
+let prove_with_tcc tcc_lemma_constr eqs : tactic =
+  match !tcc_lemma_constr with
+    | None -> anomaly "No tcc proof !!"
+    | Some lemma ->
+	fun gls ->
+	  let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+	  tclTHENSEQ
+	    [
+	      generalize [lemma];
+	      h_intro hid;
+	      Elim.h_decompose_and (mkVar hid);
+	      tclTRY(list_rewrite true eqs);
+	      Eauto.gen_eauto false (false,5) [] (Some [])
+	    ]
+	    gls
+
+
+let backtrack_eqs_until_hrec hrec eqs : tactic = 
+  fun gls -> 
+    let rewrite = 
+      tclFIRST (List.map Equality.rewriteRL eqs )
+    in 
+    let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in 
+    let f_app = array_last (snd (destApp hrec_concl)) in 
+    let f =  (fst (destApp f_app)) in 
+    let rec backtrack : tactic = 
+      fun g -> 
+	let f_app = array_last (snd (destApp (pf_concl g))) in 
+	match kind_of_term f_app with 
+	  | App(f',_) when eq_constr f' f -> tclIDTAC g
+	  | _ -> tclTHEN rewrite backtrack g
+    in
+    backtrack gls
+
+    
+    
+  
+
+let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic = 
+  match !tcc_lemma_constr with 
+    | None -> tclIDTAC_MESSAGE (str "No tcc proof !!")
+    | Some lemma -> 
+	fun gls ->
+	  let hid = next_global_ident_away true Recdef.h_id (pf_ids_of_hyps gls) in 
+	    (tclTHENSEQ 
+	    [
+	      generalize [lemma];
+	      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 
+		    [
+			 thin [hrec];
+			 apply (Lazy.force acc_inv);
+			 (fun g -> 
+			    if is_mes 
+			    then 
+			      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 [])))
+		       ]
+		]
+			  )
+	    ])
+	    gls
+
+
+let is_valid_hypothesis predicates_name =
+  let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in
+  let is_pte typ =
+    if isApp typ
+    then
+      let pte,_ = destApp typ in
+      if isVar pte
+      then Idset.mem (destVar pte) predicates_name
+      else false
+    else false
+  in
+  let rec is_valid_hypothesis typ =
+    is_pte typ ||
+      match kind_of_term typ with 
+	| Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
+	| _ -> false 
+  in
+  is_valid_hypothesis 
+
+let fresh_id avoid na = 
+  let id =  
+    match na with 
+      | Name id -> id 
+      | Anonymous -> h_id 
+  in 
+  next_global_ident_away true id avoid
+
+
+let prove_principle_for_gen
+    (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
+    rec_arg_num rec_arg_type relation = 
+  fun g -> 
+    let type_of_goal = pf_concl g in 
+    let goal_ids = pf_ids_of_hyps g in 
+    let goal_elim_infos = compute_elim_sig type_of_goal in 
+    let params_names,ids = List.fold_left 
+      (fun (params_names,avoid) (na,_,_) -> 
+	 let new_id = fresh_id avoid na in 
+	 (new_id::params_names,new_id::avoid)
+      )
+      ([],goal_ids)
+      goal_elim_infos.params
+    in
+    let predicates_names,ids = 
+      List.fold_left 
+	(fun (predicates_names,avoid) (na,_,_) -> 
+	   let new_id = fresh_id avoid na in 
+	   (new_id::predicates_names,new_id::avoid)
+	)
+	([],ids)
+	goal_elim_infos.predicates
+    in
+    let branches_names,ids = 
+      List.fold_left 
+	(fun (branches_names,avoid) (na,_,_) -> 
+	   let new_id = fresh_id avoid na in 
+	   (new_id::branches_names,new_id::avoid)
+	)
+	([],ids)
+	goal_elim_infos.branches
+    in
+    let to_intro = params_names@predicates_names@branches_names in 
+    let nparams = List.length params_names in 
+    let rec_arg_num = rec_arg_num - nparams in 
+    let tac_intro_static = h_intros to_intro in 
+    let args_info = ref None in 
+    let arg_tac g =  (* introducing args *)
+      let ids = pf_ids_of_hyps g in 
+      let func_body = def_of_const (mkConst functional_ref) in
+      (* 	      let _ = Pp.msgnl (Printer.pr_lconstr func_body) in  *)
+      let (f_name, _, body1) = destLambda func_body in
+      let f_id =
+	match f_name with
+	  | Name f_id -> next_global_ident_away true f_id ids
+	  | Anonymous -> anomaly "anonymous function"
+      in
+      let n_names_types,_ = decompose_lam body1 in 
+      let n_ids,ids = 
+	List.fold_left 
+	  (fun (n_ids,ids) (n_name,_) -> 
+	     match n_name with 
+	       | Name id -> 
+		   let n_id = next_global_ident_away true id ids in 
+		   n_id::n_ids,n_id::ids
+	       | _ -> anomaly "anonymous argument"
+	  )
+	  ([],(f_id::ids))
+	  n_names_types
+      in
+      let rec_arg_id = List.nth n_ids (rec_arg_num - 1 ) in
+      let args_ids = snd (list_chop nparams n_ids) in
+      args_info := Some (ids,args_ids,rec_arg_id);
+      h_intros args_ids g
+    in
+    let wf_tac = 
+      if is_mes 
+      then 
+	Recdef.tclUSER_if_not_mes 
+      else fun _ -> prove_with_tcc tcc_lemma_ref []
+    in
+    let start_tac g = 
+      let ids,args_ids,rec_arg_id = out_some !args_info in
+      let nargs = List.length args_ids in 
+      let pre_rec_arg = 
+	List.rev_map 
+	  mkVar 
+	  (fst (list_chop (rec_arg_num - 1) args_ids))
+      in
+      let args_before_rec = pre_rec_arg@(List.map mkVar params_names) in
+      let relation = substl args_before_rec relation in 
+      let input_type = substl args_before_rec rec_arg_type in 
+      let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in 
+      let wf_rec_arg = 
+	next_global_ident_away true 
+	  (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 acc_inv = 
+	lazy (
+	  mkApp (
+	    delayed_force acc_inv_id,
+	    [|input_type;relation;mkVar rec_arg_id|]
+	  )
+	)
+      in
+      (tclTHENS
+	   (observe_tac 
+	      "first assert" 
+	      (assert_tac 
+		 true (* the assert thm is in first subgoal *)
+		 (Name wf_rec_arg) 
+		 (mkApp (delayed_force acc_rel,
+			 [|input_type;relation;mkVar rec_arg_id|])
+		 )
+	      )
+	   )
+	   [
+	     (* accesibility proof *) 
+	     tclTHENS 
+	       (observe_tac 
+		  "second assert" 
+		  (assert_tac 
+		     true 
+		     (Name wf_thm)
+		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
+		  )
+	       )
+	       [ 
+		 (* interactive proof of the well_foundness of the relation *) 
+		 wf_tac is_mes;
+		 (* well_foundness -> Acc for any element *)
+		 observe_tac 
+		   "apply wf_thm" 
+		   (h_apply ((mkApp(mkVar wf_thm,
+				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+		   )
+	       ]
+	     ;
+	     (* rest of the proof *)
+	     tclTHENSEQ
+	       [
+		 observe_tac "generalize" (fun g -> 
+		    let to_thin = 
+		      fst (list_chop ( nargs + 1) (pf_ids_of_hyps g))
+		    in
+		    let to_thin_c = List.rev_map mkVar to_thin in 
+		    tclTHEN (generalize to_thin_c) (observe_tac "thin" (h_clear false to_thin)) g
+		 );
+		 observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
+		h_intros args_ids;
+		h_intro wf_rec_arg;
+		Equality.rewriteLR (mkConst eq_ref);
+		(fun g' -> 
+		   let body = 
+		     let _,args = destApp (pf_concl g') in 
+		     array_last args
+		   in
+		   let body_info rec_hyps = 
+		     {
+		       nb_rec_hyps = List.length rec_hyps;
+		       rec_hyps = rec_hyps;
+		       eq_hyps = [];
+		       info = body
+		     }
+		   in 
+		   let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  wf_rec_arg|]) )  in
+		   let pte_info = 
+		     { proving_tac =
+			 (fun eqs -> 
+			    observe_tac "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 
+		     }
+		   in
+		   let ptes_info : pte_info Idmap.t = 
+		     List.fold_left
+		       (fun map pte_id -> 
+			  Idmap.add pte_id 
+			    pte_info			       
+			    map
+		       )
+		       Idmap.empty
+		       predicates_names
+		   in
+		   let make_proof rec_hyps = 
+		     build_proof 
+		       false 
+		       [f_ref]
+		       ptes_info
+		       (body_info rec_hyps)
+		   in
+		   instanciate_hyps_with_args 
+		     make_proof
+		     branches_names
+		     args_ids
+		     g'
+		     
+		) 
+	       ]
+	   ]
+	   g
+      )
+      in
+      tclTHENSEQ 
+	[tac_intro_static;
+	 arg_tac;
+	 start_tac
+	] g
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+