From 97ad592fc2b52d6d2fc3ec3f6196b96380830457 Mon Sep 17 00:00:00 2001 From: bertot Date: Thu, 27 Feb 2003 15:03:27 +0000 Subject: 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 --- .depend | 40 ++- .depend.camlp4 | 1 + Makefile | 18 +- contrib/funind/tacinv.ml4 | 751 +++++++++++++++++++++++++++++++++++++++++ contrib/funind/tacinvutils.ml | 276 +++++++++++++++ contrib/funind/tacinvutils.mli | 75 ++++ contrib/funind/test.v | 429 +++++++++++++++++++++++ 7 files changed, 1575 insertions(+), 15 deletions(-) create mode 100644 contrib/funind/tacinv.ml4 create mode 100644 contrib/funind/tacinvutils.ml create mode 100644 contrib/funind/tacinvutils.mli create mode 100644 contrib/funind/test.v 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 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 + + (* 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 .vo" + End: +*) -- cgit v1.2.3