(*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 -> . *) 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 = [] } (* 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: *** *)