diff options
Diffstat (limited to 'contrib/funind/tacinv.ml4')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 872 |
1 files changed, 0 insertions, 872 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 deleted file mode 100644 index 5d19079b..00000000 --- a/contrib/funind/tacinv.ml4 +++ /dev/null @@ -1,872 +0,0 @@ -(*i camlp4deps: "parsing/grammar.cma" i*) - -(*s FunInv Tactic: inversion following the shape of a function. *) - -(* Deprecated: see indfun_main.ml4 instead *) - -(* Don't delete this file yet, it may be used for other purposes *) - -(*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 -open Setoid_replace -open Tacinvutils -(*i*) - -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 -let rec listsuf i l = if i<=0 then l else listsuf (i-1) (List.tl l) -let rec listpref i l = if i<=0 then [] else List.hd l :: listpref (i-1) (List.tl l) -let rec split3 l = - List.fold_right (fun (e1,e2,e3) (a,b,c) -> (e1::a),(e2::b),(e3::c)) l ([],[],[]) - -let mkthesort = mkProp (* would like to put Type here, but with which index? *) - -(* this is the prefix used to name equality hypothesis generated by - case analysis*) -let equality_hyp_string = "_eg_" - -(* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur - initiale au debut de l'appel a la fonction proofPrinc: 1. *) -let nthhyp = ref 1 - -let debug i = prstr ("DEBUG "^ string_of_int i ^"\n") -let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2) -(* 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) - (*end debugging *) - -(* Interpretation of constr's *) -let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c - -(*s specific manipulations on constr *) -let lift1_leqs leq= - List.map - (function (r,(typofg,g,d)) - -> lift 1 r, (lift 1 typofg, lift 1 g , lift 1 d)) leq - -let lift1_relleqs leq= List.map (function (r,x) -> lift 1 r,x) 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 pop1_levar levars = List.map (function ev,tev -> ev, popn 1 tev) levars - - -let rec add_n_dummy_prod t n = - if n<=0 then t - else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkthesort 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 x = - List.map (function (_,(a,b,c)) -> (Anonymous, mkEq a b c)) x - - -let rec eqs_of_beqs_named_aux s i l = - match l with - | [] -> [] - | (r,(a,b,c))::l' -> - (Name(id_of_string (s^ string_of_int i)), mkEq a b c) - ::eqs_of_beqs_named_aux s (i-1) l' - - -let eqs_of_beqs_named s l = eqs_of_beqs_named_aux s (List.length l) l - -let rec patternify ltypes c nme = - match ltypes with - | [] -> c - | (mv,t)::ltypes' -> - let c'= substitterm 0 mv (mkRel 1) c in - let tlift = lift (List.length ltypes') t in - let res = - patternify ltypes' (mkLambda (newname_append nme "rec", tlift, c')) nme in - res - -let rec npatternify ltypes c = - match ltypes with - | [] -> c - | (mv,nme,t)::ltypes' -> - let c'= substitterm 0 mv (mkRel 1) c in - let tlift = lift (List.length ltypes') t in - let res = - npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in - res - -(* fait une application (c m1 m2...mn, où mi est une evar, on rend également - la liste des evar munies de leur type) *) -let rec apply_levars c lmetav = - match lmetav with - | [] -> [],c - | (i,typ) :: lmetav' -> - let levars,trm = apply_levars c lmetav' in - let exkey = mknewexist() in - ((exkey,typ)::levars), applistc trm [mkEvar exkey] - (* EXPERIMENT le refine est plus long si on met un cast: - ((exkey,typ)::levars), mkCast ((applistc trm [mkEvar exkey]),typ) *) - - -let prod_change_concl c newconcl = - let lv,_ = decompose_prod c in prod_it newconcl lv - -let lam_change_concl c newconcl = - let lv,_ = decompose_prod c in lam_it newconcl lv - - -let rec mkAppRel c largs n = - match largs with - | [] -> c - | arg::largs' -> - let newc = mkApp (c,[|(mkRel n)|]) in mkAppRel newc largs' (n-1) - -let applFull c typofc = - let lv,t = decompose_prod typofc in - let ltyp = List.map fst lv in - let res = mkAppRel c ltyp (List.length ltyp) in - res - -(* Take two terms with same structure and return a map of deBruijn from the - first to the second. Only DeBruijn should be different between the two - terms. *) -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 - | Const c1, Const c2 when c1=c2 -> Smap.empty - | Ind c1, Ind c2 when c1=c2 -> Smap.empty - | Rel i, Rel j when i=j -> Smap.empty - | Rel i, Rel j -> 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) when Array.length args = Array.length argsb -> - build_rel_map_list (Array.to_list args) (Array.to_list argsb) - | _,_ -> failwith ("Could not generate case annotation. "^ - "Incompatibility between annotation and actual 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 *) - -(* This is the type of the argument of [proofPrinc] *) - -type mimickinfo = - { - concl: constr; (* conclusion voulue, cad (xi:ti)gl, ou gl est le but a - prouver, et xi:ti correspondent aux arguments donnés à - la tactique. On enlèvera un produit à chaque fois - qu'on rencontrera un binder, sans lift ou pop. - Initialement: une seule conclusion, puis specifique à - chaque branche. *) - absconcl: constr array; (* conclusions patternisées pour pouvoir être - appliquées = un predicat pour chaque fixpt - mutuel. *) - mimick: constr; (* le terme qu'on imite. On plongera dedans au fur et - à mesure, sans lift ni pop. *) - env: env; (* The global typing environment, we will add thing in it when - going inside the term (push_rel, push_rec_types) *) - sigma: Evd.evar_map; - 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)). *) - fonc: int * int; (* bornes des 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). *) - doeqs: bool; (* this reference is to toggle building of equalities during - the building of the principle (default is true) *) - fix: bool; (* did I already went through a fix or case constr? lambdas - found before a case or a fix are treated as parameters of - the induction principle *) - lst_vars: (constr*(name*constr)) list ; (* Variables rencontrées jusque là *) - lst_eqs: (Term.constr * (Term.constr * Term.constr * Term.constr)) list ; - (* liste d'équations engendrées au cours du - parcours, cette liste grandit à chaque - case, et il faut lifter le tout à chaque - binder *) - lst_recs: constr list ; (* appels récursifs rencontrés jusque là *) - } - -(* This is the return type of [proofPrinc] *) -type 'a funind = (* 'A = CONTR OU CONSTR ARRAY *) - { - - princ:'a; (* le (ou les) principe(s) demandé(s), il contient des meta - variables représentant soit des trous à prouver plus tard, - soit les conclusions à compléter avant de rendre le terme - (suivant qu'on utilise le principe pour faire refine ou - functional scheme). Il y plusieurs conclusions si plusieurs - fonction mutuellement récursives) voir la suite. *) - evarlist: (constr*Term.types) list; (* [(ev1,tev1);(ev2,tev2)...]] - l'ensemble des meta variables - correspondant à des trous. [evi] - est la meta variable, [tevi] est - son type. *) - hypnum: (int*int*int) list; (* [[(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. *) - mutfixmetas: constr array ; (* un tableau de meta variables correspondant - à chacun des prédicats mutuellement - récursifs construits. *) - conclarray: types array; (* un tableau contenant les conclusions - respectives de chacun des prédicats - mutuellement récursifs. Permet de finir la - construction du principe. *) - params:(constr*name*constr) list; (* [[(metavar,param,tparam)..]] la - liste des paramètres (les lambdas - au-dessus du fix) du fixpoint si - fixpoint il y a, le paramètre est - une meta var, dont on stocke le nom - et le type. TODO: utiliser la - structure adequat? *) - } - - - -let empty_funind_constr = - { - princ = mkProp; - evarlist = []; - hypnum = []; - mutfixmetas = [||]; - conclarray = [||]; - params = [] - } - -let empty_funind_array = - { empty_funind_constr with - princ = [||]; - } - -(* Replace the calls to the function (recursive calls) by calls to the - corresponding constant *) -let replace_reccalls mi b = - let d,f = mi.fonc in - let res = ref b in - let _ = for i = d to f do - res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in - !res - - - -(* collects all information of match branches stored in [l] *) -let rec collect_cases l = - match l with - | [||] -> empty_funind_array - | arr -> - let x = arr.(0) in - let resrec = collect_cases (Array.sub arr 1 (Array.length arr - 1)) in - { x with - princ= Array.append [|x.princ|] resrec.princ; - evarlist = x.evarlist@resrec.evarlist; - hypnum = x.hypnum@resrec.hypnum; - } - -let collect_pred l = - let l1,l2,l3 = split3 l in - Array.of_list l1 , Array.of_list l2 , Array.of_list l3 - - -(* [build_pred n tarr] builds the right predicates for each element of [tarr] - (of type: [type array] of size [n]). Return the list of triples: - (?i , - fun (x1:t1) ... (xn:tn) => (?i x1...xn) , - forall (x1:t1) ... (xn:tn), (?i x1...xn)), - where ti's are deduced from elements of tarr, which are of the form: - t1 -> t2 -> ... -> tn -> <nevermind>. *) -let rec build_pred n tarr = - if n >= Array.length tarr (* 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) tarr - - -let heq_prefix = "H_eq_" - -type kind_of_hyp = Var | Eq (*| Rec*) - -(* the main function, build the principle by exploring the term and reproduce - the same structure. *) -let rec proofPrinc mi: constr funind = - match kind_of_term mi.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 evararr,newabsconcl,pisarr = collect_pred (build_pred 0 tarr) in - let newenv = push_rec_types (narr,tarr,carr) mi.env in - let anme',aappel_rec,llevar,llposeq = - collect_fix mi 0 iarr narr carr pisarr newabsconcl newenv in - let anme = Array.map (fun nme -> newname_append nme "_ind") anme' in - { - princ = mkFix((iarr,i),(anme, pisarr,aappel_rec)); - evarlist= pop1_levar llevar; (* llevar are put outside the fix, so we pop 1 *) - hypnum = llposeq; - mutfixmetas = evararr; - conclarray = pisarr; - params = [] - } - (* <pcase> Cases b of arrPt end.*) - | Case (cinfo, pcase, b, arrPt) -> - let prod_pcase,_ = decompose_lam pcase in - let _nmeb,_ = List.hd prod_pcase in - let newb'= apply_leqtrpl_t b mi.lst_eqs in - let type_of_b = Typing.type_of mi.env mi.sigma b in - (* Replace the recursive calls to the function by calls to the constant *) - let newb = replace_reccalls mi newb' in - let cases = collect_cases (Array.mapi (fold_proof mi b type_of_b newb) arrPt) in - (* the match (case) annotation must be transformed, see [build_pcase] below *) - let newpcase = build_pcase mi pcase b type_of_b newb in - let trm' = mkCase (cinfo,newpcase,newb, cases.princ) in - { cases with - princ = if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) else trm'; - params = [] (* FIX: fix parms here (fixpt inside a match)*) - } - - - | Lambda(nme, typ, cstr) -> - let _, _, cconcl = destProd mi.concl in - let d,f=mi.fonc in - let newenv = push_rel (nme,None,typ) mi.env in - let newlst_var = (* if this lambda is a param, then don't add it here *) - if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars mi.lst_vars - else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars mi.lst_vars in - let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv; - fonc = (if d > 0 then d+1 else 0) , (if f > 0 then f+1 else 0); - lst_vars = newlst_var ; lst_eqs = lift1_leqs mi.lst_eqs; - lst_recs = lift1L mi.lst_recs} in - let resrec = proofPrinc newmi in - (* are we inside a fixpoint or a case? then this is a normal lambda *) - if mi.fix - then { resrec with princ = mkLambda (nme,typ,resrec.princ) ; params = [] } - else (* otherwise this is a parameter *) - let metav = mknewmeta() in - let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in - { resrec with - princ = substmeta resrec.princ; - evarlist = List.map (fun (ev,tev) -> ev, substmeta tev) resrec.evarlist; - conclarray = Array.map substmeta resrec.conclarray; - params = (metav,nme,typ) :: resrec.params - } - - - | 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 mi.lst_vars) in - let varnames = List.map snd mi.lst_vars in - let nb_vars = List.length varnames in - let nb_eqs = List.length mi.lst_eqs in - let _eqrels = List.map fst mi.lst_eqs in - (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs - trouvés dans les let in et les Cases avec ceux trouves dans u (ie - mi.mimick). *) - (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *) - let terms_recs = mi.lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in - (*c construction du terme: application successive des variables, des - egalites et des appels rec, 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 mi.absconcl mi.fonc terms_recs in - let typeofhole'' = prod_it_anonym_lift mi.concl 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 - { empty_funind_constr with - princ = conclrecs; - evarlist = [ newmeta , typeofhole ]; - hypnum = [ nb_vars , List.length terms_recs , nb_eqs ]; - conclarray = mi.absconcl; - } - - -(* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant - l'annotation de type du case [pcase] contient des lambdas supplémentaires - en tête. Je les récupère dans la variable [suppllam_pcase]. Le problème est - que la conclusion de l'annotation du nouveauacse doit faire référence à ces - variables plutôt qu'à celle de l'exterieur. Ce qui suit permet de changer - les reference de newpcase' pour pointer vers les lambda du piquant. On - procède comme suit: on repère les rels qui pointent à l'interieur de - l'annotation dans la fonction initiale et on les relie à celle du type - voulu pour le case, pour ça ([build_rel_map]) on parcourt en même temps le - dernier lambda du piquant ([typ]) (qui contient le type de l'argument du - case) et le type attendu pour le case ([type_of_b]) et on construit un - map. Ensuite on remplace les rels correspondant dans la preuve construite - en suivant le map. *) - -and build_pcase mi pcase b type_of_b newb = - let prod_pcase,_ = decompose_lam pcase in - let nme,typ = List.hd 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 typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 mi.concl) in - let suppllam_pcase = List.tl prod_pcase in - let suppllam_pcasel = List.length suppllam_pcase in - let rel_smap = - if suppllam_pcasel=0 then Smap.empty else (* FIX: is this test necessary ? *) - build_rel_map (lift suppllam_pcasel type_of_b) typ in - let newpcase''' = - Smap.fold (fun e e' acc -> substitterm 0 e (lift 1 e') acc) - rel_smap typeof_case'' in - let neweq = mkEq (lift (suppllam_pcasel + 1) type_of_b) - (lift (suppllam_pcasel + 1) newb) (mkRel 1) in - let newpcase'' = - if mi.doeqs - then mkProd (name_of_string "eg", neweq, lift 1 newpcase''') - else newpcase''' in - (* construction du dernier lambda du piquant. *) - let newpcase' = mkLambda (newname_append nme "_ind" ,typ, newpcase'') in - (* ajout des lambdas supplémentaires (type dépendant) du piquant. *) - lamn suppllam_pcasel suppllam_pcase newpcase' - - -(* [fold_proof mi b typeofb newb l n] rend le resultat de l'appel recursif sur - cstr (correpsondant au ième elt de [arrPt] ci-dessus et donc au ième - constructeur de [typeofb]), appele avec les bons arguments: [mi.concl] - devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments - du constructeur considéré, et [concl'] est [mi.concl] ou l'on a réécrit [b] - en ($c_n$ [rel1]...). *) -and fold_proof mi b type_of_b newb i cstr = - let new_lst_recs = mi.lst_recs @ hdMatchSub_cpl b mi.fonc in - (* 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 i in - let concl'' = - substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in - let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in - let concl_dummy = add_n_dummy_prod concl'' nargs in - let lsteqs_rew = apply_eq_leqtrpl mi.lst_eqs neweq in - let new_lsteqs = (mkRel (-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in - let a',a'' = decompose_lam_n nargs cstr in - let newa'' = - if mi.doeqs - then mkLambda (name_of_string heq_prefix,lift nargs neweq,lift 1 a'') - else a'' in - let newmimick = lamn nargs a' newa'' in - let b',b'' = decompose_prod_n nargs concl_dummy in - let newb'' = - if mi.doeqs - then mkProd (name_of_string heq_prefix,lift nargs neweq,lift 1 b'') - else b'' in - let newconcl = prodn nargs b' newb'' in - let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true; - lst_eqs= new_lsteqs; lst_recs = new_lst_recs} in - proofPrinc newmi - - -and collect_fix mi n iarr narr carr pisarr newabsconcl newenv = - 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 newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl; - mimick=c; fonc=(1,((Array.length iarr)));env=newenv;fix=true; - lst_vars=lift1_lvars mi.lst_vars; lst_eqs=lift1_leqs mi.lst_eqs; - lst_recs= lift1L mi.lst_recs;} in - let resrec = proofPrinc newmi in - let lnme,lappel_rec,llevar,llposeq = - collect_fix mi (n+1) iarr narr carr pisarr newabsconcl newenv in - Array.append [|nme|] lnme , Array.append [|resrec.princ|] lappel_rec - , (resrec.evarlist@llevar) , (resrec.hypnum@llposeq) - -let mkevarmap_aux ex = let x,y = ex in (mkevarmap_from_listex x),y - - -(* 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 = - let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env; - sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false ; - lst_vars = []; lst_eqs = []; lst_recs = []} in - proofPrinc mi - -(* Do intros [i] times, then do rewrite on all introduced hyps which are called - like [heq_prefix], FIX: have another filter than the name. *) -let rec iterintro i = - if i<=0 then tclIDTAC else - tclTHEN - (tclTHEN - intro - (iterintro (i-1))) - (fun gl -> - (tclREPEAT - (tclNTH_HYP i - (fun hyp -> - let hypname = (string_of_id (destVar hyp)) in - let sub = - try String.sub hypname 0 (String.length heq_prefix) - with _ -> "" (* different than [heq_prefix] *) in - if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite")) - )) gl) - - -(* - (fun hyp gl -> - let _ = prstr ("nthhyp= "^ string_of_int i) in - if isConst hyp && ((name_of_const hyp)==heq_prefix) then - let _ = prstr "YES\n" in - rewriteLR hyp gl - else - let _ = prstr "NO\n" in - tclIDTAC gl) - *) - -(* [invfun_basic C listargs_ids gl dorew lposeq] builds the tactic - which: - \begin{itemize} - \item Do refine on C (the induction principle), - \item try to Clear listargs_ids - \item if boolean dorew is true, then intro all new hypothesis, and - try rewrite on those hypothesis that are equalities. - \end{itemize} -*) - -let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq = - (tclTHEN_i - (tclTHEN - (tclTHEN - (* Refine on the right term (following the sheme of the - given function) *) - (fun gl -> refine open_princ_proof_applied gl) - (* Clear the hypothesis given as arguments of the tactic - (because they are generalized) *) - (tclTHEN simpl_in_concl (tclTRY (clear listargs_ids)))) - (* Now we introduce the created hypothesis, and try rewrite on - equalities due to case analysis *) - (fun gl -> (tclIDTAC gl))) - (fun i gl -> - if not dorew then tclIDTAC gl - else - (* d,m,f correspond respectively to vars, induction hyps and - equalities*) - let d,m,f = List.nth lposeq (i-1) in - tclTHEN (iterintro (d)) (tclDO m (tclTRY intro)) 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,_ = destApp 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*) - - - -(* TODO: ne plus mettre les sous-but à l'exterieur, mais à l'intérieur (le bug - de refine est normalement resolu). Ca permettra 2 choses: d'une part que - les preuves soient plus simple, et d'autre part de fabriquer un terme de - refine qui pourra s'aapliquer SANS FAIRE LES INTROS AVANT, ce qui est bcp - mieux car fonctionne comme induction et plus comme inversion (pas de perte - de connexion entre les hypothèse et les variables). *) - -(*s Tactic that makes induction and case analysis following the shape - of a function (idf) given with arguments (listargs) *) -let invfun c l dorew gl = -(* \begin{itemize} - \item [fonc] = the constant corresponding to the function - (necessary for equalities of the form [(f x1 x2 ...)=...] where - [f] is the recursive function). - \item [def_fonc] = body of the function, where let ins have - been expanded. *) - let fonc, def_fonc' = interp_fonc_tacarg c gl in - let def_fonc'',listargs' = - applistc_iota def_fonc' l (pf_env gl) (project gl) in - let def_fonc = expand_letins def_fonc'' in - (* 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 _ = resetmeta() in - let pr = invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in - (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *) - let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in - (* apply parameters immediately *) - let gl_abstr = - applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev pr.params)) in - (* we apply args of the fix now, the parameters will be applied later *) - let princ_proof_applied_args = - applistc pr.princ (listsuf (List.length pr.params) listargs') in - (* parameters are still there so patternify must not take them -> lift *) - let princ_proof_applied_lift = - lift (List.length pr.evarlist) princ_proof_applied_args in - let princ_applied_hyps'' = patternify (List.rev pr.evarlist) - princ_proof_applied_lift (Name (id_of_string "Hyp")) in - (* if there was a fix, we will not add "Q" as in funscheme, so we make a pop, - TODO: find were we made the lift in proofPrinc instead and supress it here, - and add lift in funscheme. *) - let princ_applied_hyps' = - if Array.length pr.mutfixmetas > 0 then popn 1 princ_applied_hyps'' - else princ_applied_hyps'' in - (* if there is was fix, we have to replace the meta representing the - predicate of the goal by the abstracted goal itself. *) - let princ_applied_hyps = - if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) - (substit_red 0 (pr.mutfixmetas.(0)) gl_abstr princ_applied_hyps') - else princ_applied_hyps' (* No Fixpoint *) in - let _ = prNamedConstr "princ_applied_hyps" princ_applied_hyps in - (* Same thing inside levar *) - let newlevar' = - if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) - List.map (fun (x,y) -> x,substit_red 0 (pr.mutfixmetas.(0)) gl_abstr y) pr.evarlist - else pr.evarlist - in - (* replace params metavar by real args *) - let rec replace_parms lparms largs t = - match lparms, largs with - [], _ -> t - | ((p,_,_)::lp), (a::la) -> let t'= substitterm 0 p a t in replace_parms lp la t' - | _, _ -> error "problem with number of args." in - let princ_proof_applied = replace_parms pr.params listargs' princ_applied_hyps in - let _ = prNamedLConstr "levar:" (List.map fst newlevar') in - let _ = prNamedLConstr "levar types:" (List.map snd newlevar') in - let _ = prNamedConstr "princ_proof_applied" princ_proof_applied in - (* replace also in levar *) - let newlevar = - List.rev (List.map (fun (x,y) -> x, replace_parms pr.params listargs' y) newlevar') in -(* - (* replace params metavar by abstracted variables *) - let princ_proof_params = npatternify (List.rev pr.params) princ_applied_hyps in - (* we apply now the real parameters *) - let princ_proof_applied = - applistc princ_proof_params (listpref (List.length pr.params) listargs') in -*) - let princ_applied_evars = apply_levars princ_proof_applied newlevar in - let open_princ_proof_applied = princ_applied_evars in - let _ = prNamedConstr "princ_applied_evars" (snd princ_applied_evars) in - let _ = prNamedLConstr "evars" (List.map snd (fst princ_applied_evars)) in - let listargs_ids = List.map destVar (List.filter isVar listargs') in - (* debug: impression du but*) - let lgl = Evd.to_list (sig_sig gl) in - let _ = prNamedLConstr "\ngl= " (List.map (fun x -> (snd x).evar_concl) lgl) in - let _ = prstr "fin gl \n\n" in - invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids - gl dorew pr.hypnum - -(* function must be a constant, all arguments must be given. *) -let invfun_verif c l dorew gl = - if not (isConst c) then error "given function is not a constant" - else - let x,_ = decompose_prod (pf_type_of gl c) in - if List.length x = List.length l then - try invfun c l dorew gl - with UserError (x,y) -> raise (UserError (x,y)) - else error "wrong number of arguments for the function" - - - - -(* 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 _ = resetmeta() in - let gl = mknewmeta() in - let gl_app = applFull gl ftyp in - let pis = prod_change_concl ftyp gl_app in - (* Here we call the function invfun_proof, that effectively - builds the scheme *) -(* let princ_proof,levar,_,evararr,absc,parms = *) - let _ = prstr "Recherche du principe... lancement de invfun_proof\n" in - let pr = invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in - (* parameters are still there (unboud rel), and patternify must not take them - -> lift*) - let princ_proof_lift = lift (List.length pr.evarlist) pr.princ in - let princ_proof_hyps = - patternify (List.rev pr.evarlist) princ_proof_lift (Name (id_of_string "Hyp")) in - let rec princ_replace_metas ev abs i t = - if i>= Array.length ev then t - else (* fix? *) - princ_replace_metas ev abs (i+1) - (mkLambda ( - (Name (id_of_string ("Q"^(string_of_int i)))), - prod_change_concl (lift 0 abs.(i)) mkthesort, - (substitterm 0 ev.(i) (mkRel 1) (lift 0 t)))) - in - let rec princ_replace_params params t = - List.fold_left ( - fun acc (ev,nam,typ) -> - mkLambda (Name (id_of_name nam) , typ, - substitterm 0 ev (mkRel 1) (lift 0 acc))) - t (List.rev params) in - if Array.length pr.mutfixmetas = 0 (* Is there a Fixpoint? *) - then (* No Fixpoint *) - princ_replace_params pr.params (mkLambda ((Name (id_of_string "Q")), - prod_change_concl ftyp mkthesort, - (substitterm 0 gl (mkRel 1) princ_proof_hyps))) - else (* there is a fix -> add parameters + replace metas *) - let princ_rpl = - princ_replace_metas pr.mutfixmetas pr.conclarray 0 princ_proof_hyps in - princ_replace_params pr.params princ_rpl - - - -(* Declaration of the functional scheme. *) -let declareFunScheme f fname mutflist = - let _ = prstr "Recherche du perincipe...\n" in - let id_to_cstr id = - try constr_of_id (Global.env()) id - with - Not_found -> error (string_of_id id ^ " not found in the environment") in - let flist = if mutflist=[] then [f] else mutflist in - let fcstrlist = Array.of_list (List.map id_to_cstr flist) in - let idf = id_to_cstr f in - let scheme = buildFunscheme idf fcstrlist in - let _ = prstr "Principe:" in - let _ = prconstr scheme in - let ce = { - const_entry_body = scheme; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true } in - let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in - () - - - -TACTIC EXTEND functional_induction - [ "old" "functional" "induction" constr(c) ne_constr_list(l) ] - -> [ invfun_verif c l true ] -END - -VERNAC COMMAND EXTEND FunctionalScheme - [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" - ident(c) "with" ne_ident_list(l) ] - -> [ declareFunScheme c na l ] -| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ] - -> [ declareFunScheme c na [] ] -END - - - - - -(* -*** Local Variables: *** -*** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" *** -*** 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: 78 *** -*** indent-tabs-mode: nil *** -*** test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v" *** -*** End: *** -*) - - |