The contribution of Pierre Courtieu on generating specialized induction schemes

for recursive functions.


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

7 files changed, 1575 insertions, 15 deletions

diff --git a/.depend b/.depend
index b016111d9..f2c3841dc 100644
--- a/.depend
+++ b/.depend
@@ -391,6 +391,12 @@ contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     lib/pp.cmi 
 contrib/extraction/table.cmi: kernel/environ.cmi library/libnames.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi 
+contrib/funind/tacinvutils.cmi: interp/coqlib.cmi tactics/equality.cmi \
+    pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
+    tactics/refine.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi 
 contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
     proofs/tacmach.cmi 
 contrib/interface/dad.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
@@ -981,17 +987,17 @@ parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx library/decl_kinds.cmx \
     library/libnames.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
     interp/ppextend.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \
     interp/topconstr.cmx lib/util.cmx parsing/pcoq.cmi 
-parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
-    lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    interp/ppextend.cmi pretyping/rawterm.cmi interp/symbols.cmi \
-    kernel/term.cmi parsing/termast.cmi interp/topconstr.cmi lib/util.cmi \
+parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi interp/constrextern.cmi \
+    parsing/coqast.cmi lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi \
+    library/libnames.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi interp/ppextend.cmi pretyping/rawterm.cmi \
+    interp/symbols.cmi kernel/term.cmi interp/topconstr.cmi lib/util.cmi \
     parsing/ppconstr.cmi 
-parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
-    lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    interp/ppextend.cmx pretyping/rawterm.cmx interp/symbols.cmx \
-    kernel/term.cmx parsing/termast.cmx interp/topconstr.cmx lib/util.cmx \
+parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx interp/constrextern.cmx \
+    parsing/coqast.cmx lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx \
+    library/libnames.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx interp/ppextend.cmx pretyping/rawterm.cmx \
+    interp/symbols.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
     parsing/ppconstr.cmi 
 parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
@@ -2575,6 +2581,18 @@ contrib/fourier/g_fourier.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
 contrib/fourier/g_fourier.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     contrib/fourier/fourierR.cmx parsing/pcoq.cmx lib/pp.cmx \
     parsing/pptactic.cmx proofs/refiner.cmx 
+contrib/funind/tacinvutils.cmo: interp/coqlib.cmi kernel/declarations.cmi \
+    library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
+    library/global.cmi pretyping/inductiveops.cmi library/libnames.cmi \
+    library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
+    pretyping/reductionops.cmi kernel/sign.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi contrib/funind/tacinvutils.cmi 
+contrib/funind/tacinvutils.cmx: interp/coqlib.cmx kernel/declarations.cmx \
+    library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \
+    library/global.cmx pretyping/inductiveops.cmx library/libnames.cmx \
+    library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
+    pretyping/reductionops.cmx kernel/sign.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx contrib/funind/tacinvutils.cmi 
 contrib/interface/blast.cmo: tactics/auto.cmi proofs/clenv.cmi \
     toplevel/command.cmi contrib/interface/ctast.cmo kernel/declarations.cmi \
     library/declare.cmi tactics/eauto.cmo kernel/environ.cmi \
@@ -3135,6 +3153,8 @@ contrib/linear/ccidpc.cmo: parsing/grammar.cma
 contrib/linear/ccidpc.cmx: parsing/grammar.cma
 contrib/linear/dpc.cmo: parsing/grammar.cma
 contrib/linear/dpc.cmx: parsing/grammar.cma
+contrib/funind/tacinv.cmo: 
+contrib/funind/tacinv.cmx: 
 parsing/lexer.cmo: 
 parsing/lexer.cmx: 
 parsing/q_util.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index 9fc97cdd1..7ff30566a 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -19,6 +19,7 @@ contrib/jprover/jprover.ml: parsing/grammar.cma
 contrib/cc/cctac.ml: parsing/grammar.cma
 contrib/linear/ccidpc.ml: parsing/grammar.cma
 contrib/linear/dpc.ml: parsing/grammar.cma
+contrib/funind/tacinv.ml: 
 parsing/lexer.ml: 
 parsing/q_util.ml: 
 parsing/q_coqast.ml: 
diff --git a/Makefile b/Makefile
index 41b613d30..5a1227ff6 100644
--- a/Makefile
+++ b/Makefile
@@ -44,7 +44,8 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
 	      -I contrib/ring -I contrib/xml \
 	      -I contrib/extraction -I contrib/correctness \
               -I contrib/interface -I contrib/fourier \
-	      -I contrib/jprover -I contrib/cc -I contrib/linear
+	      -I contrib/jprover -I contrib/cc -I contrib/linear \
+	      -I contrib/funind
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
@@ -281,7 +282,8 @@ PARSERREQUIRES=\
   contrib/correctness/ptyping.cmo contrib/correctness/pwp.cmo \
   contrib/correctness/pmlize.cmo contrib/correctness/ptactic.cmo \
   contrib/correctness/psyntax.cmo contrib/cc/ccalgo.cmo \
-  contrib/cc/ccproof.cmo contrib/cc/cctac.cmo 
+  contrib/cc/ccproof.cmo contrib/cc/cctac.cmo contrib/funind/tacinvutils.cmo \
+  contrib/funind/tacinv.cmo
 
 PARSERREQUIRESCMX=$(PARSERREQUIRES:.cmo=.cmx)
 
@@ -345,6 +347,9 @@ JPROVERCMO=\
   contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \
   contrib/jprover/jprover.cmo
 
+FUNINDCMO=\
+  contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo 
+
 CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
 
 LINEARCMO=\
@@ -360,11 +365,11 @@ LINEARCMO=\
   contrib/linear/dpc.cmo
 
 ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \
-  contrib/linear/ccidpc.ml4 contrib/linear/dpc.ml4
+  contrib/linear/ccidpc.ml4 contrib/linear/dpc.ml4 contrib/funind/tacinv.ml4
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(USERCMO)
+	$(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(FUNINDCMO) $(USERCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
@@ -765,6 +770,8 @@ INTERFACERC = contrib/interface/vernacrc
 
 FOURIERVO = contrib/fourier/Fourier_util.vo    contrib/fourier/Fourier.vo
 
+FUNINDVO = 
+
 JPROVERVO = 
 
 CCVO = contrib/cc/CC.vo
@@ -777,7 +784,7 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init
 
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(CORRECTNESSVO) $(FOURIERVO) \
-	    $(JPROVERVO) $(INTERFACEV0) $(CCVO)
+	    $(JPROVERVO) $(INTERFACEV0) $(CCVO) $(FUNINDVO)
 
 $(CONTRIBVO): states/initial.coq
 
@@ -791,6 +798,7 @@ correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO)
 field: $(FIELDVO) $(FIELDCMO)
 fourier: $(FOURIERVO) $(FOURIERCMO)
 jprover: $(JPROVERVO) $(JPROVERCMO)
+funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
 
 ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) $(EXTRACTIONVO)
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
new file mode 100644
index 000000000..81071ad1e
--- /dev/null
+++ b/contrib/funind/tacinv.ml4
@@ -0,0 +1,751 @@
+(*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 par
+   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 _ -> failwith "constr_of: error when looking for a term.\n"
+
+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'
+
+
+(* List.map (function a,b,c -> ((id_of_string s), (mkEq a b c))) *)
+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 je 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à (dans les let in).
+  \end{itemize}
+  
+  le Compteur nthhyp est utilisé pour contourner un bug de refine en beta expansant
+  lesmutual fixpt.  trous. 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}
+
+  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
+ (*   prconstr princ_proof; *)
+ 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 -> 
+     (* 				let _ = prstr "avant refine \n" in *)
+				 refine open_princ_proof_applied  gl)
+    (* Clear the hypothesis given as arguments of the tactic
+       (because they are generalized) *)
+    (tclTHEN (fun gl -> 
+     (* let _ = prstr "apres refine \n" in *) (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 -> (*let _ = prstr "avant rewrite \n" in*) (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 = 
+ (* match l with
+    | fonctac::listargs ->*)
+ let listargs'' = l in
+
+(* try List.map constr_of_Constr l with _ -> failwith " constr_of_Constr " in *)
+ 
+ (* \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' listargs'' (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
+
+(*         | _ ->  failwith "invfun_proof _ " *)
+
+
+(* new syntax, with or without parenthesis *)
+TACTIC EXTEND FunctionalInduction
+  [ "Functional" "Induction" constr(c)  ne_constr_list(l) ] -> [ invfun 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
+ (*   let gl_abstr = lam_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 _ = prconstr princ_proof 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
+ (*   let _ = prconstr (princ_replace_metas evararr absc 0 princ_proof_hyps) 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
+(*   let _ = prstr "principe:\n" in
+   let _ = prconstr (princ_replace_metas evararr absc 0 princ_proof_hyps) in *)
+   princ_replace_metas evararr absc 0 princ_proof_hyps
+
+    
+(* Declaration of the functional scheme. *)
+let declareFunScheme f fname mutflist =
+ let ce = { 
+  const_entry_body = buildFunscheme (constr_of f)
+                      (Array.of_list (List.map constr_of (f::mutflist)));
+  const_entry_type = None;
+  const_entry_opaque = false } in
+ let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in
+ ()
+
+(* Commands and tactic declarations *)
+
+
+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
+
+
+(*s Command that generates the generic principle. *)
+(* FIXME:
+
+let _ = vinterp_add "FunctionElim"
+ (function
+   | VARG_CONSTR f::VARG_IDENTIFIER fname:: l  -> 
+      let mutflist =
+       List.map
+        (function VARG_CONSTR i -> i
+          | _ -> bad_vernac_args "FunctionElim") l in
+      (fun _ -> (declareFunScheme f fname mutflist))
+   | _  -> bad_vernac_args "FunctionElim")
+
+
+
+
+let _ = add_tactic "Invfunproofsimpl" dyn_invfun_proof
+let _ = hide_tactic "Invfunproof" dyn_invfun_proofR
+*)
+
+(* iter a tactic *)
+let rec iter_tac_on_hyps tac l =
+ match l with
+  | [] -> tclIDTAC
+  | h::l' -> 
+     tclTHEN (tac h) (iter_tac_on_hyps tac l')
+
+(* iter on all tactics for which filter is true *)
+let rec iter_tac_on_hyps_filter filter tac l =
+ match l with
+  | [] -> tclIDTAC
+  | h::l' -> 
+     tclTHEN 
+     (if filter h then tac h 
+     else tclIDTAC)
+     (iter_tac_on_hyps_filter filter tac l')
+
+(* Definition of a filter (see above) that matches the prefix of hypothesis *)
+exception String_diff
+
+let string_match s1 s2 =
+ let res = true in
+ try 
+  for i = 0 to (String.length s1) - 1  do
+    if String.get s1 i <> String.get s2 i then raise String_diff
+  done;
+  true
+ with Invalid_argument _ -> false
+  | String_diff -> false
+
+(* a simple filter: true if an hyp name prefix matches [s] *)
+let hyp_named s namedecl =
+ let id,_,_ = namedecl in
+ string_match s (string_of_id id)
+ 
+(* Rewrite Matching *)
+let rew_list id = 
+ match id with 
+  | s,None,x -> tclTRY (rewriteLR (mkVar s))
+  | _ -> failwith "something went wrong during automatic rewriting."
+
+let iter_rew_on_matching_name_hyps s gl =
+ let hypslist = pf_hyps gl in
+ iter_tac_on_hyps_filter (hyp_named s) rew_list hypslist gl
+
+TACTIC EXTEND RewriteMatching
+  [ "Rewrite" "Matching" ident(s) ] 
+ ->[iter_rew_on_matching_name_hyps (string_of_id s)]
+END
+(* End Rewrite Matching *)
+
+(* Clear (Try to) all matching hyps *)
+let clear_list id = 
+ match id with
+  | (s,None,x) -> tclTRY (clear [s])
+  | _ -> failwith "something went wrong during automatic clear."
+
+let iter_clear_on_matching_name_hyps s gl =
+ let hypslist = pf_hyps gl in
+ iter_tac_on_hyps_filter (hyp_named s) clear_list hypslist gl
+
+TACTIC EXTEND ClearMatching
+  [ "Clear" "Matching" ident(s) ] 
+ ->[iter_clear_on_matching_name_hyps (string_of_id s)]
+END
+(* end of clear matching*)
+
+
+
+(* 
+*** Local Variables: ***
+*** compile-command: "make" ***
+*** 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: ***
+*)
+          
+
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
new file mode 100644
index 000000000..f99b548ee
--- /dev/null
+++ b/contrib/funind/tacinvutils.ml
@@ -0,0 +1,276 @@
+(* tacinvutils.ml *)
+(*s utilities *)
+
+(*i*)
+open Names
+open Util
+open Term
+open Termops
+open Coqlib
+open Pp
+open Printer
+open Inductiveops
+open Environ
+open Declarations
+open Nameops
+open Evd
+open Sign
+open Reductionops
+(*i*)
+
+(* FIXME: ref 1, pas bon, si? *)
+let evarcpt = ref 0
+let metacpt = ref 0
+let mknewexist ()= 
+  begin
+    evarcpt := !evarcpt+1;
+    !evarcpt,[||]
+  end
+
+let mknewmeta ()= 
+  begin
+    metacpt := !metacpt+1;
+    mkMeta !metacpt
+  end
+
+let  rec mkevarmap_from_listex lex =
+  match lex with
+	 | [] -> Evd.empty
+	 | ((ex,_),typ)::lex' -> 
+		  let info ={
+			 evar_concl = typ;
+			 evar_hyps = empty_named_context;
+			 evar_body = Evar_empty} in
+		  Evd.add (mkevarmap_from_listex lex') ex info
+
+(*s printing of constr *)
+
+let prconstr c =  msg(str"  " ++ prterm c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+
+let prchr () = msg (str" (ret) \n")
+let prNamedConstr s c = 
+  begin
+    msg(str "");
+    msg(str(s^"==>\n  ") ++ prterm c ++ str "\n<==\n");
+    msg(str "");
+  end
+
+let prNamedLConstr_aux lc = 
+  List.map (prNamedConstr "#>") lc
+
+let prNamedLConstr s lc = 
+  begin
+    prstr s;
+    prNamedLConstr_aux lc
+  end
+
+
+(* tire de const\_omega.ml *)
+let constant dir s =
+  try
+    Declare.global_absolute_reference
+      (Libnames.make_path
+        (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
+        (Names.id_of_string s))
+  with e -> print_endline (String.concat "." dir); print_endline s; 
+            raise e
+(* fin const\_omega.ml *)
+
+let mkEq typ c1 c2 = 
+  mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|])
+let mkRefl typ c1 = 
+  mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"),
+         [| typ; c1|])
+
+let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
+
+
+(* Operations on names *)
+let id_of_name = function
+    Anonymous -> id_of_string "H"
+  | Name id   -> id;;
+let string_of_name nme = string_of_id (id_of_name nme)
+let name_of_string str = Name (id_of_string str)
+let newname_append nme str = 
+  Name(id_of_string ((string_of_id (id_of_name nme))^str))
+
+(* Substitutions in constr *)
+
+let compare_constr_nosub t1 t2 =
+  if compare_constr (fun _ _ -> false) t1 t2 
+  then true
+  else false
+
+let rec compare_constr' t1 t2 =
+  if compare_constr_nosub t1 t2 
+  then true
+  else (compare_constr (compare_constr') t1 t2)
+
+let rec substitterm prof t by_t in_u =
+  if (compare_constr' (lift prof t) in_u)
+  then (lift prof by_t)
+  else map_constr_with_binders succ 
+    (fun i -> substitterm i t by_t) prof in_u
+
+
+let apply_eqtrpl eq t =
+  let tb,b,by_t = eq in
+  substitterm 0 b by_t t
+
+let apply_eqtrpl_lt lt eq =  List.map (apply_eqtrpl eq) lt
+
+let apply_leqtrpl_t t leq =
+  List.fold_left (fun x y -> apply_eqtrpl y x) t leq
+
+
+let apply_refl_term eq t =
+  let _,arr = destApplication eq in
+  let reli= (Array.get arr 1) in
+  let by_t= (Array.get arr 2) in
+  substitterm 0 reli by_t t
+
+let apply_eq_leqtrpl leq eq =
+  List.map 
+    (function (tb,b,t) 
+	-> tb,
+	(if isRel b then b else (apply_refl_term eq b)),
+	apply_refl_term eq t) leq
+
+
+
+(* [(a b c) a] -> true *)
+let constr_head_match u t=
+  if isApp u 
+  then let uhd,_= destApplication u in
+  begin
+    uhd=t
+  end
+  else false
+
+(* My operations on constr *)
+let lift1L l = (List.map (lift 1) l)
+let mkArrow_lift t1 t2 = mkArrow t1 (lift 1 t2)
+let mkProd_liftc nme c1 c2 = mkProd (nme,c1,(lift 1 c2))
+(* prod_it_lift x [a1 a2 ...] *)
+let prod_it_lift ini lcpl =
+  List.fold_right (function a,b -> (fun c -> mkProd_liftc a b c)) ini lcpl;;
+
+let prod_it_anonym_lift trm lst = List.fold_right mkArrow_lift lst trm
+
+let lam_it_anonymous trm lst =
+  List.fold_right (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm
+
+let lambda_id id typeofid cstr =
+  let cstr' = mkNamedLambda (id_of_string "FUNX") typeofid cstr in
+  substitterm 0 id (mkRel 0) cstr'
+
+let prod_id id typeofid cstr =
+  let cstr' = mkNamedProd (id_of_string "FUNX") typeofid cstr in
+  substitterm 0 id (mkRel 0) cstr'
+
+
+
+
+
+let nth_dep_constructor indtype n =
+  let sigma = Evd.empty and env = Global.env() in
+  let indtypedef = find_rectype env sigma indtype in
+  let indfam,_ = dest_ind_type indtypedef in
+  let arr_cstr_summary = get_constructors env indfam in
+  let cstr_sum = Array.get arr_cstr_summary n in
+  build_dependent_constructor cstr_sum,  cstr_sum.cs_nargs
+
+
+let coq_refl_equal = lazy(constant ["Coq"; "Init"; "Logic"] "refl_equal")
+
+let rec buildrefl_from_eqs eqs = 
+  match eqs with 
+    | []  ->  []
+    | cstr::eqs' -> 
+        let eq,args = destApplication cstr in        
+        (mkApp (Lazy.force coq_refl_equal,
+          [| 
+          (Array.get args 0);
+          (Array.get args 2)|]))
+        ::(buildrefl_from_eqs eqs')
+
+
+
+
+(* list of occurrences of a term inside another, no imbricated
+   occurrence are considered (ie we stop looking inside a termthat is
+   an occurrence). *)
+let rec hdMatchSub u t=
+  if constr_head_match u t then 
+	 u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
+      [] 
+      u)
+  else
+    fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
+      [] 
+      u
+
+(* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
+let hdMatchSub_cpl u (d,f) = 
+	 let res = ref [] in
+	 begin
+	 	for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done;
+		  !res
+	 end
+
+
+(* destApplication raises an exception if [t] is not an application *)      
+let exchange_hd_prod subst_hd t =
+    let (hd,args)= destApplication t in mkApp (subst_hd,args)
+
+let rec substit_red prof t by_t in_u =
+  if constr_head_match in_u (lift prof t) 
+  then whd_beta (exchange_hd_prod (lift prof by_t) in_u)
+  else
+    map_constr_with_binders succ (fun i u -> substit_red i t by_t u)
+    	prof in_u
+
+(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each reli by tarr.(f-i). *)
+let exchange_reli_arrayi tarr (d,f) t =
+  let hd,args= destApplication t in 
+  let i = destRel hd in
+  whd_beta (mkApp (tarr.(f-i) ,args))
+
+let exchange_reli_arrayi_L tarr (d,f) = List.map (exchange_reli_arrayi tarr (d,f))
+
+
+let rec expand_letins mimick =
+  match kind_of_term mimick with
+    | LetIn(nme,cstr1, typ, cstr) ->
+        let cstr' = substitterm 0 (mkRel 1) (lift 1 cstr1) cstr in
+        expand_letins (pop cstr')
+    | x -> map_constr expand_letins mimick
+	  
+
+(* From Antonia: Valeur d'une constante *)
+let def_of_const t =
+  match kind_of_term t with
+    | Const sp -> 
+		  (try 
+			 match Global.lookup_constant sp with
+              {const_body=Some c} -> force c
+ 				|_ -> assert false
+			 with _ -> assert false)
+    | _ -> t
+
+(* nom d'une constante.*)
+let name_of_const t =
+    match (kind_of_term t) with
+      Const cst -> string_of_kn cst
+     |_ -> assert false
+ ;;
+
+
+(*i
+ Local Variables:
+ compile-command: "make -k tacinvutils.cmo"
+ End:
+i*)
+
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
new file mode 100644
index 000000000..21e351371
--- /dev/null
+++ b/contrib/funind/tacinvutils.mli
@@ -0,0 +1,75 @@
+(* tacinvutils.ml *)
+(*s utilities *)
+
+(*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 Evd
+(*i*)
+
+(* printing *)
+val prconstr: constr -> unit
+val prlistconstr: constr list  -> unit
+val prstr: string -> unit 
+
+
+val mknewmeta: unit -> constr
+val mknewexist: unit -> existential
+val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map
+val mkEq: types -> constr -> constr -> constr
+(* let mkEq typ c1 c2 =   mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *)
+val mkRefl: types -> constr -> constr
+val buildrefl_from_eqs: constr list -> constr list
+(* typ c1 =  mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *)
+
+val nth_dep_constructor: constr -> int -> (constr*int)
+
+val prod_it_lift:  (name*constr) list -> constr -> constr
+val prod_it_anonym_lift: constr -> constr list -> constr
+val lam_it_anonymous: constr -> constr list -> constr
+val lift1L: (constr list) -> constr list
+val popn: int -> constr -> constr
+val lambda_id: constr -> constr -> constr -> constr
+val prod_id: constr -> constr -> constr -> constr
+
+
+val name_of_string : string -> name
+val newname_append: name -> string -> name
+
+val apply_eqtrpl: (constr*constr*constr) -> constr -> constr
+val substitterm: int -> constr -> constr -> constr -> constr
+val apply_leqtrpl_t: 
+  constr -> (constr*constr*constr) list -> constr
+val apply_eq_leqtrpl: 
+  (constr*constr*constr) list -> constr -> (constr*constr*constr) list
+(* val apply_leq_lt: constr list -> constr list -> constr list *)
+
+val hdMatchSub: constr -> constr -> constr list
+val hdMatchSub_cpl: constr -> int*int -> constr list
+val exchange_hd_prod: constr -> constr -> constr
+val exchange_reli_arrayi_L: constr array  -> int*int -> constr list -> constr list
+val substit_red: int -> constr -> constr -> constr -> constr
+val expand_letins: constr -> constr
+
+val def_of_const: constr -> constr
+val name_of_const: constr -> string
+(*i
+ Local Variables:
+ compile-command: "make -k tacinvutils.cmi"
+ End:
+i*)
+
diff --git a/contrib/funind/test.v b/contrib/funind/test.v
new file mode 100644
index 000000000..eb794dde6
--- /dev/null
+++ b/contrib/funind/test.v
@@ -0,0 +1,429 @@
+(* Declare ML Module "csimpl" "tacinvutils" "tacinv-new". *)
+Require Import Arith.
+(* Require Export Tacinvnew. *)
+ 
+Fixpoint trivfun [n : nat] : nat :=
+ Cases n of O => O | (S m) => (trivfun m) end.
+(*Parameter P: nat -> Prop.
+  Goal  (n:nat)(P n).
+  Intro n.
+  Invfunproof trivfun params n.
+  Show Proof.
+*)
+
+(* essaie de parametre variables non locaux:*) 
+
+Variables varessai:nat.
+Goal(trivfun varessai) = O.
+Functional Induction trivfun varessai.
+Trivial.
+Simpl.
+Assumption.
+Defined.
+ 
+
+Functional Scheme triv_ind := Induction for trivfun.
+
+Lemma bisrepetita:(n' : nat)  (trivfun n') = O.
+Intros n'.
+Functional Induction trivfun n'.
+Trivial.
+Simpl.
+Assumption.
+Save.
+
+
+Fixpoint iseven [n : nat] : bool :=
+ Cases n of O => true | (S (S m)) => (iseven m) | _ => false end.
+ 
+Fixpoint funex [n : nat] : nat :=
+ Cases (iseven n) of
+   true => n
+  | false =>
+      Cases n of O => O | (S r) => (funex r) end
+ end.
+(*Goal (n:nat) (funex n) = O -> (iseven n)=true.
+  Intro n.
+  Invfunproof funex params n.
+  Show Proof.
+   *)
+ 
+Fixpoint nat_equal_bool [n : nat] : nat ->  bool :=
+ [m : nat]  Cases n of
+              O =>
+                Cases m of O => true | _ => false end
+             | (S p) =>
+                 Cases m of O => false | (S q) => (nat_equal_bool p q) end
+            end.
+Require Export Arith.
+Require Export Div2.
+ 
+Lemma div2_inf: (n : nat)  (le (div2 n) n).
+Intros n.
+(Functional Induction div2 n).
+Auto with arith.
+Auto with arith.
+
+Simpl.
+Apply le_S.
+Apply le_n_S.
+Exact H.
+Qed.
+(* 
+  Functional Scheme plus_ind := Induction plus.
+  Print plus_ind.
+   *)
+ 
+Fixpoint essai [x : nat] : nat * nat ->  nat :=
+ [p : nat * nat]  ( Case p of [n, m : ?]  Cases n of
+                                            O => O
+                                           | (S q) =>
+                                               Cases x of
+                                                 O => (S O)
+                                                | (S r) => (S (essai r (q, m)))
+                                               end
+                                          end end ).
+ 
+Lemma essai_essai:
+ (x : nat)
+ (p : nat * nat)  ( Case p of [n, m : ?] (lt O n) ->  (lt O (essai x p)) end ).
+Intros x p.
+(Functional Induction essai x p); Intros.
+Inversion H.
+Simpl; Try Abstract ( Auto with arith ).
+Simpl; Try Abstract ( Auto with arith ).
+Qed.
+(* 
+  Lemma dep_dep:(x:nat)(le x (S x)).
+  Intro x.
+  Invfunproof essai_essai_trans params x.
+   
+   
+  Fixpoint  essaidep[x:nat]: () :=
+  [p:nat*nat]
+  let (n,m)=p in
+  Cases n of
+   | O => O
+   |(S q) =>  
+  Cases x of
+  | O => (S O)
+  | (S r) => (S (essai r (q,m)))
+  end
+  end.
+   *)
+ 
+Fixpoint plus_x_not_five' [n : nat] : nat ->  nat :=
+ [m : nat]  Cases n of
+              O => O
+             | (S q) =>
+                 Cases m of
+                   O => (S (plus_x_not_five' q O))
+                  | (S r) => (S (plus_x_not_five' q (S r)))
+                 end
+            end.
+ 
+Lemma notplusfive':
+ (x, y : nat) y = (S (S (S (S (S O))))) ->  (plus_x_not_five' x y) = x.
+Intros x y.
+(Functional Induction plus_x_not_five' x y); Intros hyp.
+Auto.
+Inversion hyp.
+Intros.
+Simpl.
+Auto.
+Qed.
+ 
+Fixpoint plus_x_not_five [n : nat] : nat ->  nat :=
+ [m : nat]
+  Cases n of
+    O => O
+   | (S q) =>
+       Cases (nat_equal_bool m (S q)) of   true => (S (plus_x_not_five q m))
+                                          | false => (S (plus_x_not_five q m))
+       end
+  end.
+ 
+Lemma notplusfive:
+ (x, y : nat) y = (S (S (S (S (S O))))) ->  (plus_x_not_five x y) = x.
+Intros x y.
+Unfold plus_x_not_five.
+(Functional Induction plus_x_not_five x y) ; Simpl; Intros hyp;
+ Fold plus_x_not_five.
+Auto.
+Auto.
+Auto.
+Qed.
+ 
+Fixpoint plus_x_not_five'' [n : nat] : nat ->  nat :=
+ [m : nat]  let x = (nat_equal_bool m (S (S (S (S (S O)))))) in
+              let y = O in
+                Cases n of
+                  O => y
+                 | (S q) =>
+                     let recapp = (plus_x_not_five'' q m) in
+                       Cases x of true => (S recapp) | false => (S recapp) end
+                end.
+(* let in pas encore traites *)
+ 
+Lemma notplusfive'':
+ (x, y : nat) y = (S (S (S (S (S O))))) ->  (plus_x_not_five'' x y) = x.
+Intros a b.
+Unfold plus_x_not_five''.
+(Functional Induction plus_x_not_five'' a b); Intros hyp; Simpl; Auto.
+Qed.
+ 
+Lemma iseq_eq: (n, m : nat) n = m ->  (nat_equal_bool n m) = true.
+Intros n m.
+Unfold nat_equal_bool.
+(Functional Induction nat_equal_bool n m); Simpl; Intros hyp; Auto.
+Inversion hyp.
+Inversion hyp.
+Qed.
+ 
+Lemma iseq_eq': (n, m : nat) (nat_equal_bool n m) = true ->  n = m.
+Intros n m.
+Unfold nat_equal_bool.
+(Functional Induction nat_equal_bool n m); Simpl; Intros eg; Auto.
+Inversion eg.
+Inversion eg.
+Qed.
+ 
+Definition iszero : nat ->  bool :=
+   [n : nat]  Cases n of O => true | _ => false end.
+ 
+Inductive istrue : bool ->  Prop :=
+  istrue0: (istrue true) .
+ 
+Lemma toto: (n : nat) n = O ->  (istrue (iszero n)).
+Intros x.
+(Functional Induction iszero x); Intros eg; Simpl.
+Apply istrue0.
+Inversion eg.
+Qed.
+(* 
+  plus = 
+  Fix plus
+  {plus [n:nat] : nat->nat :=
+     [m:nat]Cases n of
+              O => m
+            | (S p) => (S (plus p m))
+            end}
+     : nat->nat->nat
+   *)
+ 
+Lemma inf_x_plusxy': (x, y : nat)  (le x (plus x y)).
+Intros n m.
+(Functional Induction plus n m); Intros.
+Auto with arith.
+Auto with arith.
+Qed.
+(* *****essais *)
+ 
+Lemma inf_x_plusxy'': (x : nat)  (le x (plus x O)).
+Intros n.
+Unfold plus.
+(Functional Induction plus n O); Intros.
+Auto with arith.
+Apply le_n_S.
+Assumption.
+Qed.
+ 
+Lemma inf_x_plusxy''': (x : nat)  (le x (plus O x)).
+Intros n.
+(Functional Induction plus O n); Intros;Auto with arith.
+Qed.
+
+(*Lemma inf_x_plusxy''':(x,y:nat)(le x (plus (S x) (S y))).
+  Intros n m.
+  Invfunproof plus params (S n) (S m);Intros.
+  Auto with arith.
+  Assumption.
+  Save.*)
+ 
+Fixpoint mod2 [n : nat] : nat :=
+ Cases n of   O => O
+             | (S (S m)) => (S (mod2 m))
+             | _ => O end.
+ 
+Lemma princ_mod2: (n : nat)  (le (mod2 n) n).
+Intros n.
+(Functional Induction mod2 n); Simpl; Auto with arith.
+Qed.
+ 
+Definition isfour : nat ->  bool :=
+   [n : nat]  Cases n of (S (S (S (S O)))) => true | _ => false end.
+ 
+Definition isononeorfour : nat ->  bool :=
+   [n : nat]  Cases n of   (S O) => true
+                          | (S (S (S (S O)))) => true
+                          | _ => false end.
+(* Inductive istrue : bool -> Prop := istrue0 : (istrue true). *)
+ 
+Lemma toto'': (n : nat) (istrue (isfour n)) ->  (istrue (isononeorfour n)).
+Intros n.
+(Functional Induction isononeorfour n); Intros istr; Simpl; Inversion istr.
+Apply istrue0.
+Qed.
+ 
+Lemma toto': (n, m : nat) n = (S (S (S (S O)))) ->  (istrue (isononeorfour n)).
+Intros n.
+(Functional Induction isononeorfour n); Intros m istr; Inversion istr.
+Apply istrue0.
+Qed.
+ 
+Definition ftest : nat -> nat ->  nat :=
+   [n, m : nat]  Cases n of
+                   O =>
+                     Cases m of O => O | _ => (S O) end
+                  | (S p) => O
+                 end.
+ 
+Lemma test1: (n, m : nat)  (le (ftest n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest n m); Auto with arith.
+Qed.
+ 
+Lemma test11: (m : nat)  (le (ftest O m) (S (S O))).
+Intros m.
+(Functional Induction ftest O m).
+Auto with arith.
+Auto with arith.
+Qed.
+ 
+Definition ftest4 : nat -> nat ->  nat :=
+   [n, m : nat]  Cases n of
+                   O =>
+                     Cases m of O => O | (S q) => (S O) end
+                  | (S p) =>
+                      Cases m of O => O | (S r) => (S O) end
+                 end.
+ 
+Lemma test4: (n, m : nat)  (le (ftest n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest n m); Auto with arith.
+Qed.
+ 
+Lemma test4': (n, m : nat)  (le (ftest4 (S n) m) (S (S O))).
+Intros n m.
+(Functional Induction ftest4 (S n) m).
+Auto with arith.
+Auto with arith.
+Qed.
+ 
+Definition ftest44 : nat * nat -> nat -> nat ->  nat :=
+   [x : nat * nat]
+   [n, m : nat]
+    ( Case x of [p, q : ?]  Cases n of
+                              O =>
+                                Cases m of O => O | (S q) => (S O) end
+                             | (S p) =>
+                                 Cases m of O => O | (S r) => (S O) end
+                            end end ).
+ 
+Lemma test44:
+ (pq : nat * nat) (n, m, o, r, s : nat)  (le (ftest44 pq n (S m)) (S (S O))).
+Intros pq n m o r s.
+(Functional Induction ftest44 pq n (S m)).
+Auto with arith.
+Auto with arith.
+Auto with arith.
+Auto with arith.
+Qed.
+ 
+Fixpoint ftest2 [n : nat] : nat ->  nat :=
+ [m : nat]  Cases n of
+              O =>
+                Cases m of O => O | (S q) => O end
+             | (S p) => (ftest2 p m)
+            end.
+ 
+Lemma test2: (n, m : nat)  (le (ftest2 n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest2 n m) ; Simpl; Intros; Auto.
+Qed.
+ 
+Fixpoint ftest3 [n : nat] : nat ->  nat :=
+ [m : nat]  Cases n of
+              O => O
+             | (S p) =>
+                 Cases m of O => (ftest3 p O) | (S r) => O end
+            end.
+ 
+Lemma test3: (n, m : nat)  (le (ftest3 n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest3 n m).
+Intros.
+Auto.
+Intros.
+Auto.
+Intros.
+Simpl.
+Auto.
+Qed.
+ 
+Fixpoint ftest5 [n : nat] : nat ->  nat :=
+ [m : nat]  Cases n of
+              O => O
+             | (S p) =>
+                 Cases m of O => (ftest5 p O) | (S r) => (ftest5 p r) end
+            end.
+ 
+Lemma test5: (n, m : nat)  (le (ftest5 n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest5 n m).
+Intros.
+Auto.
+Intros.
+Auto.
+Intros.
+Simpl.
+Auto.
+Qed.
+ 
+Definition ftest7 : (n : nat)  nat :=
+   [n : nat]  Cases (ftest5 n O) of O => O | (S r) => O end.
+ 
+Lemma essai7:
+ (Hrec : (n : nat) (ftest5 n O) = O ->  (le (ftest7 n) (S (S O))))
+ (Hrec0 : (n, r : nat) (ftest5 n O) = (S r) ->  (le (ftest7 n) (S (S O))))
+ (n : nat)  (le (ftest7 n) (S (S O))).
+Intros hyp1 hyp2 n.
+Unfold ftest7.
+(Functional Induction ftest7 n); Auto.
+Qed.
+ 
+Fixpoint ftest6 [n : nat] : nat ->  nat :=
+ [m : nat]
+  Cases n of
+    O => O
+   | (S p) =>
+       Cases (ftest5 p O) of O => (ftest6 p O) | (S r) => (ftest6 p r) end
+  end.
+
+ 
+Lemma princ6:
+ ((n, m : nat) n = O ->  (le (ftest6 O m) (S (S O)))) ->
+ ((n, m, p : nat)
+  (le (ftest6 p O) (S (S O))) ->
+  (ftest5 p O) = O -> n = (S p) ->  (le (ftest6 (S p) m) (S (S O)))) ->
+ ((n, m, p, r : nat)
+  (le (ftest6 p r) (S (S O))) ->
+  (ftest5 p O) = (S r) -> n = (S p) ->  (le (ftest6 (S p) m) (S (S O)))) ->
+ (x, y : nat)  (le (ftest6 x y) (S (S O))).
+Intros hyp1 hyp2 hyp3 n m.
+Generalize hyp1 hyp2 hyp3.
+Clear hyp1 hyp2 hyp3.
+(Functional Induction ftest6 n m);Auto.
+Qed.
+ 
+Lemma essai6: (n, m : nat)  (le (ftest6 n m) (S (S O))).
+Intros n m.
+Unfold ftest6.
+(Functional Induction ftest6 n m); Simpl; Auto.
+Qed.
+  (* 
+   Local Variables: 
+   coq-prog-name: "../mytop.out  -I . -emacs"
+   compile-command: "make -C <chemin du makefile> <chemin du makefile au fichier>.vo"
+   End:
+*)