From fbc0242a1d9c280de22da165c162ef24e4981ff1 Mon Sep 17 00:00:00 2001 From: coq Date: Mon, 9 Feb 2004 17:18:17 +0000 Subject: New version of Functional Scheme and functional induction. Deals with more functions (higher order and polymorphic functions), the principle is a bit better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5310 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 4 + contrib/funind/tacinv.ml4 | 232 ++++++++++++++++++++++++++--------- contrib/funind/tacinvutils.ml | 29 +++-- contrib/funind/tacinvutils.mli | 2 + test-suite/success/Funind.v | 266 ++++++++++++++++++++++++----------------- 5 files changed, 354 insertions(+), 179 deletions(-) diff --git a/CHANGES b/CHANGES index 3031fda33..a8dbae337 100644 --- a/CHANGES +++ b/CHANGES @@ -141,6 +141,8 @@ Vernacular commands and on substrings of the name of the lemma - "Print Implicit" displays the implicit arguments of a constant - Locate now searches for all names having a given suffix +- New command "Functional Scheme" for building an induction principle + from a function defined by case analysis and fix. Commands @@ -226,6 +228,8 @@ Tactics immediate hint), resulting in shorter proofs - Instantiate now works in hyps (syntax : Instantiate in ...) - Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists +- New tactic "functional induction" to perform case analysis and + induction following the definition of a function. - Clear now fails when trying to remove a local definition used by a constant appearing in the current goal diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index cff2dba1f..9700fa950 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -44,6 +44,8 @@ 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 +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 mkthesort = mkProp (* would like to put Type here, but with which index? *) @@ -59,18 +61,23 @@ let nthhyp = ref 1 (*debugging*) 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 *) let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c let rec collect_cases l = match l with - | [||] -> [||],[],[],[||],[||] + | [||] -> [||],[],[],[||],[||],[] | arr -> - let (a,c,d,f,e)= arr.(0) in - let aa,lc,ld,_,_ = + let (a,c,d,f,e,g)= 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 + Array.append [|a|] aa , (c@lc) , (d@ld) , f , e, g let rec collect_pred l = match l with @@ -91,6 +98,8 @@ let lift1_relleqs leq= List.map (function (r,x) -> lift 1 r,x) leq 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 @@ -137,7 +146,22 @@ let rec patternify ltypes c nme = | [] -> c | (mv,t)::ltypes' -> let c'= substitterm 0 mv (mkRel 1) c in - patternify ltypes' (mkLambda (newname_append nme "rec", t, c')) nme + 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 _ = prconstr c' in *) + let tlift = lift (List.length ltypes') t in + let res = + npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in +(* let _ = prconstr res in *) + res let rec apply_levars c lmetav = match lmetav with @@ -165,7 +189,9 @@ let rec mkAppRel c largs n = 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 ltyp = List.map fst lv in + let res = mkAppRel c ltyp (List.length ltyp) in + res let rec build_rel_map typ type_of_b = @@ -228,8 +254,11 @@ type mimickinfo = sigma: Evd.evar_map; nmefonc: constr array; fonc: int * int; - doeqs: bool (* this reference is to toggle building of equalities during + 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 *) } (* @@ -249,16 +278,32 @@ type mimickinfo = [(ev1,tev1);(ev2,tev2)..], [(i1,j1,k1);(i2,j2,k2)..], [|c1;c2..|], - [|typ1;typ2..|]] + [|typ1;typ2..|], + [(param,tparam)..]] + + *) + +(* This could be the return type of [proofPrinc], but not yet *) +type funind = + { + princ:constr; + evarlist: (constr*Term.types) list; + hypnum: (int*int*int) list; + mutfixmetas: constr array ; + conclarray: types array; + params:(constr*name*constr) list + } +(* 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[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 (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. \item[[(ev1,tev1);(ev2,tev2)...]] est l'ensemble des méta variables correspondant à des trous. [evi] est la meta variable, [tevi] est son type. @@ -270,19 +315,22 @@ type mimickinfo = \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. + \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. + + \item[[(param,tparam)..]] est la liste des paramètres (les lambda au-dessus + du fix) du fixpoint si fixpoint il y a. \end{itemize} *) -let heq_prefix = "_eq_" +let heq_prefix = "H_eq_" type kind_of_hyp = Var | Eq (*| Rec*) -let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs: +let rec proofPrinc mi lst_vars lst_eqs lst_recs: constr * (constr*Term.types) list * (int*int*int) list - * constr array * types array = + * constr array * types array * (constr*name*constr) list = match kind_of_term mi.mimick with (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to point on the name of recursive calls *) @@ -298,12 +346,11 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs: 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) mi.env in let rec collect_fix n = @@ -314,17 +361,19 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs: (* 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} in - let appel_rec,levar,lposeq,_,evarrarr = + mimick=c; fonc=(1,((Array.length iarr)));env=newenv;fix=true} in + let appel_rec,levar,lposeq,_,evarrarr,parms = proofPrinc newmi (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 + (* llevar are put outside the fix, so one level of rel must be removed *) + mkFix((iarr,i),(anme, pisarr,aappel_rec)),(pop1_levar llevar),llposeq,evararr,pisarr,[] (* Cases b of arrPt end.*) | Case(cinfo, pcase, b, arrPt) -> @@ -372,12 +421,12 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs: 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} in - let a,b,c,d,e = proofPrinc newmi lst_vars new_lsteqs new_lst_recs in - a,b,c,d,e + let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true} in + let a,b,c,d,e,p = proofPrinc newmi lst_vars new_lsteqs new_lst_recs in + a,b,c,d,e,p in - let arrPt_proof,levar,lposeq,evararr,absc = + 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 @@ -427,7 +476,7 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs: let trm = if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) else trm' in - trm,levar,lposeq,evararr,absc + trm,levar,lposeq,evararr,absc,[] (* fix parms here (fix inside case)*) | Lambda(nme, typ, cstr) -> let _, _, cconcl = destProd mi.concl in @@ -435,10 +484,20 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs: let newenv = push_rel (nme,None,typ) mi.env 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))} in - let rec_call,levar,lposeq,evararr,absc = - proofPrinc newmi ((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 + 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 lst_vars + else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars lst_vars in + let rec_call,levar,lposeq,evararr,absc,parms = + proofPrinc newmi newlst_var (lift1_leqs lst_eqs) (lift1L lst_recs) in + (* are we inside a fixpoint or a case? then this is a normal lambda *) + if mi.fix then mkLambda (nme,typ,rec_call) , levar, lposeq,evararr,absc,[] + else (* otherwise this is a parameter *) + let metav = mknewmeta() in + let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in + let newrec_call = substmeta rec_call in + let newlevar = List.map (fun ev,tev -> ev, substmeta tev) levar in + let newabsc = Array.map substmeta absc in + newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms) | LetIn(nme,cstr1, typ, cstr) -> failwith ("I don't deal with let ins yet. "^ @@ -474,7 +533,7 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs: 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],[||],mi.absconcl + ,nb_eqs],[||],mi.absconcl,[] @@ -508,14 +567,13 @@ let interp_fonc_tacarg fonctac gl = This function calls the big function proofPrinc. *) let invfun_proof fonc def_fonc gl_abstr pis env sigma = - let _ = resetmeta() in let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env; - sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true} in - let princ_proof,levar,lposeq,evararr,absc = proofPrinc mi [] [] [] in - princ_proof,levar,lposeq,evararr,absc + sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in + let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in + princ_proof,levar,lposeq,evararr,absc,parms (* Do intros [i] times, then do rewrite on all introduced hyps which are called - ["H_eq_xx"], FIX: have another filter than the name. *) + like [heq_prefix], FIX: have another filter than the name. *) let rec iterintro i = if i<=0 then tclIDTAC else tclTHEN @@ -529,7 +587,7 @@ let rec iterintro i = let hypname = (string_of_id (destVar hyp)) in let sub = try String.sub hypname 0 (String.length heq_prefix) - with _ -> "" (* different than "H_eq_"*) in + with _ -> "" (* different than [heq_prefix] *) in if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 "Cannot rewrite") )) gl) @@ -604,6 +662,12 @@ let rec applistc_iota cstr lcstr env sigma = +(* 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) *) @@ -618,24 +682,62 @@ let invfun c l dorew gl = let def_fonc'',listargs' = applistc_iota def_fonc' l (pf_env gl) (project gl) in let def_fonc = expand_letins def_fonc'' in - (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *) - let gl_abstr = (add_lambdas (pf_concl gl) gl listargs') in (* quantifies on previously generalized arguments. [(x1:T1)...g[arg1 <- x1 ...]] *) let pis = add_pis (pf_concl gl) gl listargs' in (* princ_proof builds the principle *) - let princ_proof,levar, lposeq,evararr,_ = + let _ = resetmeta() in + let princ_proof,levar, lposeq,evararr,_,parms = 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 + + (* 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 parms)) in + + (* we apply args of the fix now, the parameters will be applied later *) + let princ_proof_applied_args = + applistc princ_proof (listsuf (List.length parms) listargs') in + + (* parameters are still there so patternify must not take them -> lift *) + let princ_proof_applied_lift = + lift (List.length levar) princ_proof_applied_args in + + let princ_applied_hyps'' = patternify (List.rev levar) + 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 evararr > 0 then popn 1 princ_applied_hyps'' + else princ_applied_hyps'' in + let princ_applied_hyps = - if Array.length evararr > 0 then (* Fixpoint? *) - substit_red 0 (evararr.(0)) gl_abstr princ_applied_hyps' + if Array.length evararr > 0 then (* mutual Fixpoint not treated in the tactic *) + (substit_red 0 (evararr.(0)) gl_abstr princ_applied_hyps') else princ_applied_hyps' (* No Fixpoint *) in -(* let _ = prconstr princ_applied_hyps' in *) - let princ_applied_evars = apply_levars princ_applied_hyps levar in + let _ = prNamedConstr "princ_applied_hyps" princ_applied_hyps 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 parms listargs' princ_applied_hyps in + + +(* + (* replace params metavar by abstracted variables *) + let princ_proof_params = npatternify (List.rev parms) princ_applied_hyps in + (* we apply now the real parameters *) + let princ_proof_applied = + applistc princ_proof_params (listpref (List.length parms) listargs') in +*) + + + + let princ_applied_evars = apply_levars princ_proof_applied 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 @@ -664,32 +766,43 @@ END 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 = + let princ_proof,levar,_,evararr,absc,parms = invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in - let lst_hyps = List.map snd levar in + (* parameters are still there (unboud rel), and patternify must not take them + -> lift*) + let princ_proof_lift = lift (List.length levar) princ_proof in let princ_proof_hyps = - patternify (List.rev levar) princ_proof (Name (id_of_string "Hyp")) in + patternify (List.rev levar) 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 + else (* fix? *) princ_replace_metas ev abs (i+1) (mkLambda ( (Name (id_of_string ("Q"^(string_of_int i)))), - prod_change_concl (lift 1 abs.(i)) mkthesort, - (substitterm 0 ev.(i) (mkRel (1)) (lift 1 t)))) + 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 params in if Array.length evararr = 0 (* Is there a Fixpoint? *) then (* No Fixpoint *) - (mkLambda ((Name (id_of_string ("Q"))), + princ_replace_params parms (mkLambda ((Name (id_of_string "Q")), prod_change_concl ftyp mkthesort, (substitterm 0 gl (mkRel 1) princ_proof_hyps))) - else - princ_replace_metas evararr absc 0 princ_proof_hyps + else (* there is a fix -> add parameters + replace metas *) + let princ_rpl = princ_replace_metas evararr absc 0 princ_proof_hyps in + princ_replace_params parms princ_rpl + (* Declaration of the functional scheme. *) @@ -733,6 +846,7 @@ END *** 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: *** *) diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index b933efa36..758071bac 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -20,7 +20,8 @@ open Reductionops (*s printing of constr -- debugging *) -let msg x = () (* comment this to see debugging msgs *) +let msg x = () ;; let prterm c = str "" (* comment this to see debug msgs *) + (* uncomment this to see debugging *) let prconstr c = msg (str" " ++ prterm c ++ str"\n") let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) @@ -29,12 +30,12 @@ let prchr () = msg (str" (ret) \n") let prNamedConstr s c = begin msg(str ""); - msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n"); + msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n"); msg(str ""); end let prNamedLConstr_aux lc = - List.map (prNamedConstr "#>") lc + List.iter (prNamedConstr "#>") lc let prNamedLConstr s lc = begin @@ -137,10 +138,9 @@ let apply_eq_leqtrpl leq eq = (* [(a b c) a] -> true *) let constr_head_match u t= if isApp u - then let uhd,_= destApplication u in - begin + then + let uhd,args= destApplication u in uhd=t - end else false (* My operations on constr *) @@ -215,9 +215,16 @@ let hdMatchSub_cpl u (d,f) = let exchange_hd_prod subst_hd t = let (hd,args)= destApplication t in mkApp (subst_hd,args) +(* substitute t by by_t in head of products inside in_u, reduces each + product found *) 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) + then + let _ = prNamedConstr "in_u" in_u in + let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in + let _ = prNamedConstr "xx " x in + let _ = prstr "\n\n" in + x else map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u @@ -262,9 +269,9 @@ let name_of_const t = (*i - Local Variables: - compile-command: "make -k tacinvutils.cmo" - test-command: "../../bin/coqtop -q -batch -load-vernac-source ../../test-suite/success/Funind.v" - End: +*** Local Variables: +*** compile-command: "make -k tacinvutils.cmo" +*** test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v" +*** End: i*) diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli index b42182890..2fc37b2c9 100644 --- a/contrib/funind/tacinvutils.mli +++ b/contrib/funind/tacinvutils.mli @@ -24,6 +24,8 @@ open Evd (* printing debugging *) val prconstr: constr -> unit val prlistconstr: constr list -> unit +val prNamedConstr:string -> constr -> unit +val prNamedLConstr:string -> constr list -> unit val prstr: string -> unit diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 818267668..819da2595 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -1,15 +1,100 @@ + +Definition iszero [n:nat] : bool := Cases n of + | O => true + | _ => false + end. + +Functional Scheme iszer_ind := Induction for iszero. + +Lemma toto : (n:nat) n = 0 -> (iszero n) = true. +Intros x eg. +Functional Induction iszero x; Simpl. +Trivial. +Subst x. +Inversion H_eq_. +Qed. + +(* We can even reuse the proof as a scheme: *) + +Functional Scheme toto_ind := Induction for iszero. + + + + + +Definition ftest [n, m:nat] : nat := + Cases n of + | O => Cases m of + | O => 0 + | _ => 1 + end + | (S p) => 0 + end. + +Functional Scheme ftest_ind := Induction for ftest. + +Lemma test1 : (n,m:nat) (le (ftest n m) 2). +Intros n m. +Functional Induction ftest n m;Auto. +Save. + + +Lemma test11 : (m:nat) (le (ftest 0 m) 2). +Intros m. +Functional Induction ftest 0 m. +Auto. +Auto. +Qed. + + +Definition lamfix := +[m:nat ] +(Fix trivfun {trivfun [n:nat] : nat := Cases n of + | O => m + | (S p) => (trivfun p) + end}). + +(* Parameter v1 v2 : nat. *) + +Lemma lamfix_lem : (v1,v2:nat) (lamfix v1 v2) = v1. +Intros v1 v2. +Functional Induction lamfix v1 v2. +Trivial. +Assumption. +Defined. + + + +(* polymorphic function *) +Require PolyList. + +Functional Scheme app_ind := Induction for app. + +Lemma appnil : (A:Set)(l,l':(list A)) l'=(nil A) -> l = (app l l'). +Intros A l l'. +Functional Induction app A l l';Intuition. +Rewrite <- H1;Trivial. +Save. + + + + + Require Export Arith. -Fixpoint trivfun [n : nat] : nat := - Cases n of O => O | (S m) => (trivfun m) end. +Fixpoint trivfun [n:nat] : nat := + Cases n of + | O => 0 + | (S m) => (trivfun m) + end. (* essaie de parametre variables non locaux:*) -Parameter varessai:nat. +Parameter varessai : nat. -Lemma first_try: (trivfun varessai) = O. +Lemma first_try : (trivfun varessai) = 0. Functional Induction trivfun varessai. Trivial. Simpl. @@ -19,64 +104,84 @@ Defined. Functional Scheme triv_ind := Induction for trivfun. -Lemma bisrepetita:(n' : nat) (trivfun n') = O. +Lemma bisrepetita : (n':nat) (trivfun n') = 0. Intros n'. Functional Induction trivfun n'. Trivial. -Simpl. +Simpl . Assumption. -Save. +Qed. + + -Fixpoint iseven [n : nat] : bool := - Cases n of O => true | (S (S m)) => (iseven m) | _ => false end. + + + +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. +Fixpoint funex [n:nat] : nat := + Cases (iseven n) of + | true => n + | false => Cases n of + | O => 0 + | (S r) => (funex r) + end + end. -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. +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 Div2. -Lemma div2_inf: (n : nat) (le (div2 n) n). +Lemma div2_inf : (n:nat) (le (div2 n) n). Intros n. -(Functional Induction div2 n). -Auto with arith. -Auto with arith. +Functional Induction div2 n. +Auto. +Auto. -Simpl. Apply le_S. Apply le_n_S. Exact H. Qed. +(* reuse this lemma as a scheme:*) -Fixpoint nested_lam [n:nat] : nat -> nat := -Cases n of - O => [m:nat]O -|(S n') => [m:nat](plus m (nested_lam n' m)) -end. +Functional Scheme div2_ind := Induction for div2_inf. + +Fixpoint nested_lam [n:nat] : nat -> nat := + Cases n of + | O => [m:nat ] 0 + | (S n') => [m:nat ] (plus m (nested_lam n' m)) + end. Functional Scheme nested_lam_ind := Induction for nested_lam. -Lemma nest : (n,m:nat)(nested_lam n m)=(mult n m). +Lemma nest : (n, m:nat) (nested_lam n m) = (mult n m). Intros n m. -Functional Induction nested_lam n m;Auto. -Save. +Functional Induction nested_lam n m; Auto. +Qed. -Lemma nest2 : (n,m:nat)(nested_lam n m)=(mult n m). -Intros n m. Pattern n m. -Apply nested_lam_ind;Simpl;Intros;Auto. -Save. +Lemma nest2 : (n, m:nat) (nested_lam n m) = (mult n m). +Intros n m. Pattern n m . +Apply nested_lam_ind; Simpl ; Intros; Auto. +Qed. Fixpoint essai [x : nat] : nat * nat -> nat := @@ -98,48 +203,7 @@ Inversion H. Simpl; Try Abstract ( Auto with arith ). Simpl; Try Abstract ( Auto with arith ). Qed. - -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 @@ -174,19 +238,10 @@ 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. - Lemma inf_x_plusxy': (x, y : nat) (le x (plus x y)). Intros n m. (Functional Induction plus n m); Intros. @@ -239,25 +294,6 @@ Intros n. 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 => @@ -390,3 +426,15 @@ Unfold ftest6. (Functional Induction ftest6 n m); Simpl; Auto. Qed. + + + + + + + + + + + + -- cgit v1.2.3