path: root/contrib/funind/tacinv.ml4

(*i camlp4deps: "parsing/grammar.cma" i*)

(*s FunInv Tactic: inversion following the shape of a function.  *)
(* Use:
   \begin{itemize}
   \item The Tacinv directory must be in the path (-I <path> option)
   \item use the bytecode version of coqtop or coqc (-byte option), or make a coqtop
   \item Do [Require Tacinv] to be able to use it.
   \item For syntax see Tacinv.v
   \end{itemize}
*)


(*i*)
open Termops
open Equality
open Names
open Pp
open Tacmach
open Proof_type
open Tacinterp
open Tactics
open Tacticals
open Term
open Util
open Printer
open Reductionops
open Inductiveops
open Coqlib
open Refine
open Typing
open Declare
open Decl_kinds
open Safe_typing
open Vernacinterp
open Evd
open Environ
open Entries
 (*i*)
open Tacinvutils

module Smap = Map.Make(struct type t = constr let compare = compare end)
let smap_to_list m = Smap.fold (fun c cb l -> (c,cb)::l) m []
let merge_smap m1 m2 = Smap.fold (fun c cb m -> Smap.add c cb m) m1 m2

(*  this is the prefix used to name equality hypothesis generated by
    case analysis*)
let equality_hyp_string = "_eg_"

(* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur
   initiale au debut de l'appel a la fonction proofPrinc: 1. *)
let nthhyp = ref 1
 (*debugging*)
 (* let rewrules = ref [] *)
 (*debugging*)
let debug i = prstr ("DEBUG "^ string_of_int i ^"\n")
let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2)
 (*end debugging *)

let constr_of c = 
 try Constrintern.interp_constr Evd.empty (Global.env()) c
 with _ -> 
  msg (str "constr_of: error when looking for term: "); 
  raise Not_found

let rec collect_cases l =
 match l with
  | [||] -> [||],[],[],[||],[||]
  | arr -> 
     let (a,c,d,f,e)= arr.(0) in
     let aa,lc,ld,_,_ = collect_cases (Array.sub arr 1 ((Array.length arr)-1)) in
     Array.append [|a|] aa , (c@lc) , (d@ld) , f , e

let rec collect_pred l =
 match l with
  | [] -> [],[],[]
  | (e1,e2,e3)::l' -> let a,b,c = collect_pred l' in (e1::a),(e2::b),(e3::c)


(*s specific manipulations on constr *)
let lift1_leqs leq=
 List.map (function typofg,g,d -> lift 1 typofg, lift 1 g , lift 1 d) leq

(* WARNING: In the types, we don't lift the rels in the type. This is intentional. Use
  with care. *)
let lift1_lvars lvars= List.map 
 (function x,(nme,c) -> lift 1 x, (nme, (*lift 1*) c)) lvars

let rec add_n_dummy_prod t n = 
 if n<=0 then t
 else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkProp t) (n-1)

(* [add_lambdas t gl [csr1;csr2...]] returns [[x1:type of csr1]
   [x2:type of csr2] t [csr <- x1 ...]], names of abstracted variables
   are not specified *)
let rec add_lambdas t gl lcsr =
 match lcsr with
  | [] -> t
  | csr::lcsr' -> 
     let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
     lambda_id hyp_csr hyptyp (add_lambdas t gl lcsr')

(* [add_pis t gl [csr1;csr2...]] returns ([x1] :type of [csr1]
   [x2]:type of csr2) [t]*)
let rec add_pis t gl lcsr =
 match lcsr with
  | [] -> t
  | csr::lcsr' -> 
     let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
     prod_id hyp_csr hyptyp (add_pis t gl lcsr')

let mkProdEg teq eql eqr concl =
 mkProd (name_of_string "eg", mkEq teq eql eqr, lift 1 concl)

let eqs_of_beqs = List.map (function a,b,c -> (Anonymous, mkEq a b c))


let rec eqs_of_beqs_named_aux s i l =
 match l with 
  | [] -> []
  | (a,b,c)::l' -> 
     (Name(id_of_string (s^ string_of_int i)), mkEq a b c)
     ::eqs_of_beqs_named_aux s (i-1) l'


let eqs_of_beqs_named s l = eqs_of_beqs_named_aux s (List.length l) l

let rec patternify ltypes c nme =
 match ltypes with
  | [] -> c
  | (mv,t)::ltypes' -> 
     let c'= substitterm 0 mv (mkRel 1) c in
     patternify ltypes' (mkLambda (newname_append nme "rec", t, c')) nme

let rec apply_levars c lmetav =
 match lmetav with
  | [] -> [],c
  | (i,typ) :: lmetav' -> 
     let levars,trm = apply_levars c lmetav' in
     let exkey = mknewexist() in
     ((exkey,typ)::levars),  applistc trm [mkEvar exkey]
      (* EXPERIMENT le refine est plus long si on met un cast:
         ((exkey,typ)::levars), mkCast ((applistc trm [mkEvar exkey]),typ) *)


let prod_change_concl c newconcl = let lv,_ = decompose_prod c in prod_it  newconcl lv

let lam_change_concl c newconcl = let lv,_ = decompose_prod c in lam_it newconcl lv


let rec mkAppRel c largs n =
 match largs with
  | [] -> c
  | arg::largs' -> 
     let newc = mkApp (c,[|(mkRel n)|]) in mkAppRel newc largs' (n-1)

let applFull c typofc =
 let lv,t = decompose_prod typofc in 
 let ltyp = List.map fst lv in mkAppRel c  ltyp ((List.length ltyp))


let rec build_rel_map typ type_of_b = 
 match (kind_of_term typ), (kind_of_term type_of_b) with
    Evar _ , Evar _  -> Smap.empty
  | Rel i, Rel j -> if i=j then Smap.empty 
    else Smap.add typ type_of_b Smap.empty
  | Prod (name,c1,c2), Prod (nameb,c1b,c2b) -> 
     let map1 = build_rel_map c1 c1b in
     let map2 = build_rel_map (pop c2) (pop c2b) in
     merge_smap map1 map2
  | App (f,args), App (fb,argsb) ->
     (try build_rel_map_list (Array.to_list args) (Array.to_list argsb)
     with Invalid_argument _ -> 
      failwith ("Could not generate caes annotation. "^ 
      "To application with different length"))
  | Const c1, Const c2 -> if c1=c2 then Smap.empty
    else failwith ("Could not generate caes annotation. "^ 
    "To different constants in a case annotation.")
  | Ind c1, Ind c2 -> if c1=c2 then Smap.empty
    else failwith ("Could not generate caes annotation. "^ 
    "To different constants in a case annotation.")
  | _,_ -> failwith ("Could not generate case annotation. "^
    "Incompatibility between annotation and actal type")
and build_rel_map_list ltyp ltype_of_b =
 List.fold_left2 (fun a b c -> merge_smap a (build_rel_map b c))
  Smap.empty ltyp ltype_of_b


(*s Use (and proof) of the principle *)

(*
  \begin {itemize}
  \item [concl] ([constr]): conclusions, cad (xi:ti)gl, ou gl  est le but a prouver, et
  xi:ti correspondent aux  arguments donn�s � la tactique.  On enl�ve un produit �
  chaque fois qu'on rencontre un binder, sans lift ou pop.  Initialement: une
  seule conclusion, puis specifique a  chaque branche. 
  \item[absconcl] ([constr array]): les conclusions (un predicat pour chaque
  fixp. mutuel) patternis�es pour  pouvoir �tre appliqu�es.
  \item [mimick] ([constr]): le terme qu'on imite. On plonge  dedans au fur et � mesure,
  sans lift ni pop. 
  \item [nmefonc] ([constr array]): la constante correspondant � la fonction appel�e,
  permet de remplacer les appels recursifs par des appels � la constante
  correspondante (non pertinent (et inutile) si on permet l'appel de la tactique
  sur une terme donn� directement (au lieu d'une constante comme pour l'instant)).
  \item [fonc] ([int array]) : indices des variable correspondant aux appels r�cursifs
  (plusieurs car fixp.  mutuels), utile pour reconna�tre les appels r�cursifs
  (ATTENTION: initialement vide, reste vide tant qu'on n'est pas dans un fix.).
  
  \item [lst_vars] ([(constr*(name*constr)) list]): liste des variables rencontr�es
  jusqu'� maintenant.
  \item [lst_eqs] ([constr list]): liste d'�quations engendr�es au cours du parcours,
  cette liste grandit �  chaque case, et il faut lifter le tout � chaque binder.
  \item [lst_recs] ([constr list]): listes des appels  r�cursifs rencontr�s jusque
  l�.
  \end{itemize}
  
  le Compteur nthhyp est utilis� pour contourner un comportement bizarre de refine en
  beta expansant lesmutual fixpt. On mets une variable � la place d'un ?, dont le
  debruijn pointe sur la nieme hypoth�se (nthhyp). nthhyp vaut donc initialement 1.

  Cette fonction rends un nuplet de la forme:

  [t,[(ev1,tev1);(ev2,tev2)..],[(i1,j1,k1);(i2,j2,k2)..],[|c1;c2..|],[|typ1;typ2..|]]

  o�:
  \begin{itemize}
  \item[t] est le principe demand�, il contient des meta variables repr�sentant soit des
  trous � prouver plus tard, soit les conclusions � compl�ter avant de rendre le terme
  (plusieurs conclusions si plusieurs fonction mutuellement r�cursives) voir la suite.
  \item[[(ev1,tev1);(ev2,tev2)...]] est l'ensemble des m�ta variables correspondant �
  des trous. [evi] est la meta variable, [tevi] est son type.
  \item[(in,jn,kn)] sont les nombres respectivement de variables, d'�quations, et
  d'hypoth�ses de r�currence pour le but n. Permet de faire le bon nombre d'intros et
  des rewrite au bons endroits dans la suite.
  \item[[|c1;c2...|]] est un tableau de meta variables correspondant � chacun des
  pr�dicats mutuellement r�cursifs construits.
  \item[|typ1;typ2...|] est un tableau contenant les conclusions respectives de chacun
  des pr�dicats mutuellement r�cursifs. Permet de finir la construction du principe.
  \end{itemize}

  TODO: mettre tout �a dans un record bien propre.

  proofPrinc G=concl absG=absconcl t=mimick X=fonc Gamma1=lst_vars Gamma2=lst_eq
  Gamma3=lst_recs *) 
let rec 
 proofPrinc ~concl ~absconcl ~mimick ~env ~sigma nmefonc fonc lst_vars lst_eqs lst_recs
 : constr* (constr*Term.types) list * (int*int*int) list * constr array * types array =
 match kind_of_term mimick with
    (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to
      	point on the name of recursive calls *)
  | Fix((iarr,i),(narr,tarr,carr)) -> 

     (* We construct the right predicates for each mutual fixpt *)     
     let rec build_pred n =
      if n >= Array.length iarr then []
      else
        let ftyp = Array.get tarr n in
        let gl = mknewmeta() in
        let gl_app = applFull gl ftyp in
        let pis = prod_change_concl ftyp gl_app in
        let gl_abstr = lam_change_concl ftyp gl_app in
        (gl,gl_abstr,pis):: build_pred (n+1) in
     
     let evarl,predl,pisl = collect_pred (build_pred 0) in
     let newabsconcl = Array.of_list predl in
     let evararr = Array.of_list evarl in
     let pisarr = Array.of_list pisl in
     
     let newenv = push_rec_types (narr,tarr,carr) env in

     let rec collect_fix n =
      if n >= Array.length iarr then [],[],[],[]
      else
        let nme = Array.get narr n in
        let c = Array.get carr n in
        (* rappelle sur le sous-terme, on ajoute un niveau de
           profondeur (lift) parce que Fix est un binder. *)
        let appel_rec,levar,lposeq,_,evarrarr =
         proofPrinc ~concl:(pisarr.(n)) ~absconcl:newabsconcl ~mimick:c nmefonc
         (1,((Array.length iarr))) ~env:newenv ~sigma:sigma (lift1_lvars lst_vars)
         (lift1_leqs lst_eqs) (lift1L lst_recs) in
        let lnme,lappel_rec,llevar,llposeq = collect_fix (n+1) in
        (nme::lnme),(appel_rec::lappel_rec),(levar@llevar), (lposeq@llposeq) in
     let lnme,lappel_rec,llevar,llposeq =collect_fix  0 in
     let lnme' = List.map (fun nme -> newname_append nme   "_ind") lnme in
     let anme = Array.of_list lnme' in
     let aappel_rec = Array.of_list lappel_rec in
     mkFix((iarr,i), ( anme, pisarr ,aappel_rec)), llevar,llposeq,evararr,pisarr

  (* <pcase> Cases b of arrPt end.*)
  | Case(cinfo, pcase, b, arrPt) -> 

     let prod_pcase,_ = decompose_lam pcase in
     let nmeb,lastprod_pcase = List.hd prod_pcase in
     let b'= apply_leqtrpl_t b lst_eqs in
     let type_of_b = Typing.type_of env sigma b in
     let new_lst_recs = lst_recs @ hdMatchSub_cpl b fonc in
     (* Replace the calls to the function (recursive calls) by calls to the
        corresponding constant:  *)
     let d,f = fonc in 
     let res = ref b' in
     let _ = for i = d to f do 
       res := substitterm 0 (mkRel i) nmefonc.(f-i) !res done in
     let newb = !res in

     (* [fold_proof t l n] rend le resultat de l'appel recursif sur les elements de la
        liste l (correpsondant a arrPt), appele avec les bons arguments: [concl] devient
        [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments du
        constructeur consid�r� (FIX: Hormis les parametres!!), et [concl'] est concl ou
        l'on a r��crit [b] en ($c_n$ [rel1]...).*)

     let rec fold_proof nth_construct eltPt' =  
      (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3
         x2 x1... ], sans quoi les annotations ne sont plus coherentes *)
      let cstr_appl,nargs = nth_dep_constructor type_of_b nth_construct in
      let concl'' = substitterm 0 (lift nargs b) cstr_appl (lift nargs concl) in
      let concl_dummy = add_n_dummy_prod concl'' nargs in
      let lsteqs_rew =
       apply_eq_leqtrpl lst_eqs (mkEq type_of_b newb (popn nargs cstr_appl)) in
      let new_lsteqs = (type_of_b,newb, popn nargs cstr_appl)::lsteqs_rew in
      proofPrinc ~concl:concl_dummy ~absconcl:absconcl ~mimick:eltPt' ~env:env
       ~sigma:sigma nmefonc fonc lst_vars new_lsteqs new_lst_recs in
     
     let arrPt_proof,levar,lposeq,evararr,absc = 
      collect_cases (Array.mapi fold_proof arrPt) in
     let prod_pcase,concl_pcase = decompose_lam pcase in
     let nme,typ = List.hd prod_pcase in
     let suppllam_pcase = List.tl prod_pcase in
     (* je remplace b par rel1 (apres avoir lifte un coup) dans la
        future annotation du futur case: ensuite je mettrai un lambda devant *)
     let typesofeqs' = eqs_of_beqs_named equality_hyp_string lst_eqs in
     let typesofeqs = prod_it_lift  typesofeqs' concl in
     let typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 typesofeqs) in
     
     (* C'est un peu compliqu� ici: en cas de type inductif vraiment d�pendant le
        piquant du case [pcase] contient des lambdas suppl�mentaires en t�te je les
        ai dans la variable [suppllam_pcase]. Le probl�me est que la conclusion du
        piquant doit faire r�f�rence � ces variables plut�t qu'� celle de
        l'exterieur. Ce qui suit permet de changer les reference de newpacse' pour
        pointer vers les lambda du piquant. On proc�de comme suit: on rep�re les rels
        qui pointent � l'interieur du piquant dans la fonction imit�e, pour �a on
        parcourt le dernier lambda du piquant (qui contient le type de l'argument du
        case), et on remplace les rels correspondant dans la preuve construite. *)
     
     (* typ vient du piquant, type_of_b vient du typage de b.*)
     
     let rel_smap = 
      if List.length suppllam_pcase=0 then Smap.empty else
        build_rel_map (lift (List.length suppllam_pcase) type_of_b) typ in
     let rel_map = smap_to_list rel_smap in
     let rec substL l c =
      match l with
         [] -> c
       | ((e,e') ::l') -> substL l' (substitterm 0 e (lift 1 e') c) in
     let newpcase' = substL rel_map typeof_case'' in
     let newpcase = 
      mkProdEg (lift (List.length suppllam_pcase + 1) type_of_b) 
       (lift (List.length suppllam_pcase + 1) newb) (mkRel 1) 
       newpcase' in
     (* construction du dernier lambda du piquant. *)
     let typeof_case' = mkLambda (newname_append nme "_ind" ,typ, newpcase) in
     (* ajout des lambdas suppl�mentaires (type d�pendant) du piquant. *)
     let typeof_case = lamn (List.length suppllam_pcase) suppllam_pcase typeof_case' in
     let trm' = mkCase (cinfo,typeof_case,newb, arrPt_proof) in
     let trm = mkApp (trm',[|(mkRefl type_of_b newb)|]) in
     trm,levar,lposeq,evararr,absc
      
  | Lambda(nme, typ, cstr) ->
     let _, _, cconcl = destProd concl in
     let d,f=fonc in
     let newenv = push_rel (nme,None,typ) env in

     let rec_call,levar,lposeq,evararr,absc =
      proofPrinc ~concl:cconcl ~absconcl:absconcl ~mimick:cstr ~env:newenv ~sigma:sigma
      nmefonc ((if d > 0 then d+1 else 0),(if f > 0 then f+1 else 0))
       ((mkRel 1,(nme,typ)):: lift1_lvars lst_vars)
       (lift1_leqs lst_eqs) (lift1L lst_recs) in
     mkLambda (nme,typ,rec_call) , levar, lposeq,evararr,absc

  | LetIn(nme,cstr1, typ, cstr) ->
     failwith ("I don't deal with let ins yet. "^
				 "Please expand them before applying this function.")

  | u -> 
     let varrels = List.rev (List.map fst lst_vars) in
     let varnames = List.map snd lst_vars in
     let nb_vars = (List.length varnames) in
     let nb_eqs = (List.length lst_eqs) in

     (* [terms_recs]: appel rec du fixpoint, On concat�ne les appels recs trouv�s
        dans les let in et les Cases. *)
     (* TODO: il faudra g�rer plusieurs pt fixes imbriqu�s ? *)
     let terms_recs = lst_recs @ (hdMatchSub_cpl mimick fonc)  in
     
     (*c construction du terme: application successive des variables, des appels
       rec (mais pas des egalites), a la variable existentielle correspondant a
       l'hypothese de recurrence en cours. *)
     (* d'abord, on fabrique les types des appels recursifs en replacant le nom de
        des fonctions par les predicats dans [terms_recs]: [(f_i t u v)] devient
        [(P_i t u v)] *)
     (* TODO optimiser ici: *)
     let appsrecpred = exchange_reli_arrayi_L absconcl fonc terms_recs in
     let typesofeqs    = eqs_of_beqs_named equality_hyp_string lst_eqs in
     let typeofhole''' = prod_it_lift typesofeqs concl  in
     let typeofhole''  = prod_it_anonym_lift  typeofhole''' appsrecpred in
     let typeofhole    = prodn nb_vars varnames typeofhole'' in
		   
     (* Un bug de refine m'oblige � mettre ici un H (meta variable � ce point,
        mais remplac� par H avant le refine) au lieu d'un '?', je mettrai les '?'  �
        la fin comme �a [(([H1,H2,H3...] ...) ? ? ?)]*)

     let newmeta = (mknewmeta()) in
     let concl_with_var = applistc newmeta varrels in
     let conclrecs = applistc concl_with_var terms_recs in
     conclrecs,[newmeta,typeofhole], [nb_vars,(List.length terms_recs)
      ,nb_eqs],[||],absconcl



let mkevarmap_aux ex = let x,y = ex in	(mkevarmap_from_listex x),y

(* Interpretation of constr's *)
let constr_of_Constr c = Constrintern.interp_constr Evd.empty (Global.env()) c


(* TODO: deal with any term, not only a constant. *)
let interp_fonc_tacarg fonctac gl =
 (* [fonc] is the constr corresponding to fontact not unfolded,
    if [fonctac] is a (qualified) name then this is a [const] ?. *)
(*  let fonc = constr_of_Constr fonctac in *)
 (* TODO: replace the [with _ -> ] by something more precise in
    the following. *)
 (* [def_fonc] is the definition of fonc. TODO: We should do this only
    if [fonc] is a const, and take [fonc] otherwise.*)
 try fonctac, pf_const_value gl (destConst fonctac)
 with _ -> failwith ("don't know how to deal with this function "
 ^"(DEBUG:is it a constante?)")




(* [invfun_proof fonc  def_fonc  gl_abstr pis]  builds  the principle,
   following  the shape  of   [def_fonc],    [fonc]  is the      constant
   corresponding to [def_func] (or a reduced form of  it ?), gl_abstr and
   pis are the goal to be proved, of the form [x,y...]g and (x.y...)g.

   This function calls the big function proofPrinc. *)

let invfun_proof fonc def_fonc gl_abstr pis env sigma =
 (* this counter only because of the bug of refine. [nthhyp] is
    the number of the current hypothesis (corresponding to a ?), it
    is used in the main  function. *)
 let _ = nthhyp := 1 in
 let princ_proof,levar,lposeq,evararr,absc =
  proofPrinc ~concl:pis ~absconcl:gl_abstr ~mimick:def_fonc ~env:env
   ~sigma:sigma fonc (0,0) [] [] []
 in
 princ_proof,levar,lposeq,evararr,absc
  
let rec iterintro i = 
 if i<=0 then tclIDTAC else 
   tclTHEN
    (tclTHEN 
     intro
     (iterintro (i-1)))
    (fun gl -> 
     (tclREPEAT (tclNTH_HYP i rewriteLR)) gl)

    
(* [invfun_basic C listargs_ids gl dorew lposeq] builds the tactic
   which:
   \begin{itemize}
   \item Do refine on C (the induction principle),
   \item try to Clear listargs_ids
   \item if boolean dorew is true, then intro all new hypothesis, and
   try rewrite on those hypothesis that are equalities.
   \end{itemize}
*)


let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq =
 (tclTHEN_i
  (tclTHEN
   (tclTHEN
    (* Refine on the right term (following the sheme of the
       given function) *)
    (fun gl -> 
				 refine open_princ_proof_applied  gl)
    (* Clear the hypothesis given as arguments of the tactic
       (because they are generalized) *)
    (tclTHEN (fun gl -> (simpl_in_concl gl)) (tclTRY (clear listargs_ids))))
   (* Now we introduce the created hypothesis, and try rewrite on
      equalities due to case analysis *)
   (fun gl ->  (tclIDTAC gl)))
		(fun i gl -> 
   if not dorew then tclIDTAC gl
   else
     (* d,m,f correspond respectivelyto vars, induction hyps and
        equalities*)
     let d,m,f=(List.nth lposeq (i-1)) in
     tclTHEN 
      (tclDO d intro)
      (tclTHEN (tclDO m intro) (iterintro f))
      gl)
 )
 gl




(* This function trys to reduce instanciated arguments, provided they
   are of the form [(C t u v...)] where [C] is a constructor, and
   provided that the argument is not the argument of a fixpoint (i.e. the
   argument corresponds to a simple lambda) . *)
let rec applistc_iota cstr lcstr env sigma = 
 match lcstr with
  | [] -> cstr,[]
  | arg::lcstr' -> 
     let arghd = 
      if isApp arg then let x,_ = destApplication arg in x else arg in
     if isConstruct arghd (* of the form [(C ...)]*)
     then 
        applistc_iota (Tacred.nf env sigma (nf_beta (applistc cstr [arg])))
         lcstr' env sigma
     else 
       try 
        let nme,typ,suite = destLambda cstr in
        let c, l = applistc_iota suite lcstr' env sigma in
        mkLambda (nme,typ,c), arg::l
       with _ -> cstr,arg::lcstr' (* the arg does not correspond to a lambda*)




(*s Tactic that makes induction and case analysis following the shape
  of a function (idf) given with arguments (listargs) *)
let invfun c l dorew gl = 
(* \begin{itemize}
    \item [fonc] = the constant corresponding to the function
    (necessary for equalities of the form [(f x1 x2 ...)=...] where
    [f] is the recursive function).
    \item [def_fonc] = body of the function, where let ins have
    been expanded. *)
 let fonc, def_fonc' = interp_fonc_tacarg c gl in
 let def_fonc'',listargs' =  
  applistc_iota def_fonc' l (pf_env gl) (project gl)  in
 let def_fonc = expand_letins def_fonc'' in
 (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
 let gl_abstr = (add_lambdas (pf_concl gl) gl listargs') in
 (* quantifies on previously generalized arguments. 
    [(x1:T1)...g[arg1 <- x1 ...]] *)
 let pis = add_pis (pf_concl gl) gl listargs' in
 (* princ_proof builds the principle *)
 let princ_proof,levar, lposeq,evararr,_ = 
  invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
 (* We do not consider mutual fixpt here *)
 let princ_proof_applied = applistc princ_proof listargs' in
 let princ_applied_hyps' = 
  patternify (List.rev levar) 
   princ_proof_applied (Name (id_of_string "Hyp"))  in
 let princ_applied_hyps = 
  if Array.length evararr > 0 then (* Fixpoint? *)
    substit_red 0 (evararr.(0)) gl_abstr princ_applied_hyps'
  else princ_applied_hyps' (* No Fixpoint *) in
 let princ_applied_evars = apply_levars princ_applied_hyps levar in
 let open_princ_proof_applied = princ_applied_evars in
 let listargs_ids = List.map destVar (List.filter isVar listargs') in
 invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids gl dorew lposeq

(* function must be a constant, all arguments must be given. *)
let invfun_verif c l dorew gl =
 if not (isConst c) then error "given function is not a constant"
 else 
   let x,_ = decompose_prod (pf_type_of gl c) in
   if List.length x = List.length l then 
     try invfun c l dorew gl
     with _ -> 
      error 
      ( "Tactic went wrong for some reason. If the function you used to define\n"
      ^ "the induction principle do not deal with dependent typed, please report.")
   else error "wrong number of arguments for the function"


TACTIC EXTEND FunctionalInduction
  [ "Functional" "Induction" constr(c)  ne_constr_list(l) ] -> [ invfun_verif c l true ]
END



(* Construction of the functional scheme. *)
let buildFunscheme fonc mutflist =
 let def_fonc = expand_letins (def_of_const fonc) in
 let ftyp = type_of (Global.env ()) Evd.empty fonc in
 let gl = mknewmeta() in
 let gl_app = applFull gl ftyp in
 let pis = prod_change_concl ftyp gl_app in
 (* Here we call the function invfun_proof, that effectively 
    builds the scheme *)
 let princ_proof,levar,_,evararr,absc = 
  invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in
 let lst_hyps = List.map snd levar in
 let princ_proof_hyps = 
  patternify (List.rev levar) princ_proof (Name (id_of_string "Hyp"))  in
 let rec princ_replace_metas ev abs i t = 
  if i>= Array.length ev then t
  else
    princ_replace_metas ev abs (i+1)
     (mkLambda (
      (Name (id_of_string ("Q"^(string_of_int i)))),
      prod_change_concl (lift 1 abs.(i)) mkProp,
      (substitterm 0 ev.(i) (mkRel (1)) (lift 1 t))))
 in
 if Array.length evararr = 0 (* Is there a Fixpoint? *)
	then (* No Fixpoint *)
		 (mkLambda ((Name (id_of_string ("Q"))), 
		 prod_change_concl ftyp mkProp,
   (substitterm 0 gl (mkRel 1) princ_proof_hyps)))
	else
   princ_replace_metas evararr absc 0 princ_proof_hyps

    
(* Declaration of the functional scheme. *)
let declareFunScheme f fname mutflist =
 let scheme = buildFunscheme (constr_of f) 
  (Array.of_list (List.map constr_of (f::mutflist))) in
 let ce = { 
  const_entry_body = scheme;
  const_entry_type = None;
  const_entry_opaque = false } in
 let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in
 ()



VERNAC COMMAND EXTEND FunctionalScheme
 [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
    constr(c) "with" constr_list(l) ]
  -> [ declareFunScheme c na l ]
| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" constr(c) ]
  -> [ declareFunScheme c na [] ]
END

 



(* 
*** Local Variables: ***
*** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" ***
*** tab-width: 1 ***
*** tuareg-default-indent:1 ***
*** tuareg-begin-indent:1 ***
*** tuareg-let-indent:1 ***
*** tuareg-match-indent:-1 ***
*** tuareg-try-indent:1 ***
*** tuareg-with-indent:1 ***
*** tuareg-if-then-else-inden:1 ***
*** fill-column: 88 ***
*** indent-tabs-mode: nil ***
*** End: ***
*)