From db3a9e3e16d6d7c6bc66b90a0f2eaf72ea28f81e Mon Sep 17 00:00:00 2001 From: jforest Date: Mon, 28 Apr 2008 12:17:22 +0000 Subject: menage dans funind + deplaceemnt de recdef dans funind git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10865 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 10 +- contrib/funind/Recdef.v | 48 ++ contrib/funind/g_indfun.ml4 | 485 ++++++++++++++ contrib/funind/indfun_main.ml4 | 485 -------------- contrib/funind/recdef.ml | 1430 +++++++++++++++++++++++++++++++++++++++ contrib/funind/tacinv.ml4 | 869 ------------------------ contrib/funind/tacinvutils.ml | 284 -------- contrib/funind/tacinvutils.mli | 80 --- contrib/recdef/Recdef.v | 48 -- contrib/recdef/recdef.ml4 | 1448 ---------------------------------------- 10 files changed, 1967 insertions(+), 3220 deletions(-) create mode 100644 contrib/funind/Recdef.v create mode 100644 contrib/funind/g_indfun.ml4 delete mode 100644 contrib/funind/indfun_main.ml4 create mode 100644 contrib/funind/recdef.ml delete mode 100644 contrib/funind/tacinv.ml4 delete mode 100644 contrib/funind/tacinvutils.ml delete mode 100644 contrib/funind/tacinvutils.mli delete mode 100644 contrib/recdef/Recdef.v delete mode 100644 contrib/recdef/recdef.ml4 diff --git a/Makefile.common b/Makefile.common index e45d70b996..315ed912aa 100644 --- a/Makefile.common +++ b/Makefile.common @@ -274,14 +274,12 @@ JPROVERCMO:=\ FUNINDCMO:=\ contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \ + contrib/funind/recdef.cmo \ contrib/funind/rawterm_to_relation.cmo \ contrib/funind/functional_principles_proofs.cmo \ contrib/funind/functional_principles_types.cmo \ contrib/funind/invfun.cmo contrib/funind/indfun.cmo \ - contrib/funind/merge.cmo contrib/funind/indfun_main.cmo - -RECDEFCMO:=\ - contrib/recdef/recdef.cmo + contrib/funind/merge.cmo contrib/funind/g_indfun.cmo FOCMO:=\ contrib/firstorder/formula.cmo contrib/firstorder/unify.cmo \ @@ -307,7 +305,7 @@ RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ - $(RECDEFCMO) $(FUNINDCMO) + $(FUNINDCMO) CMA:=$(CLIBS) $(CAMLP4OBJS) CMXA:=$(CMA:.cma=.cmxa) @@ -797,7 +795,7 @@ FOURIERVO:=\ FUNINDVO:= -RECDEFVO:=contrib/recdef/Recdef.vo +RECDEFVO:=contrib/funind/Recdef.vo JPROVERVO:= diff --git a/contrib/funind/Recdef.v b/contrib/funind/Recdef.v new file mode 100644 index 0000000000..2d206220e4 --- /dev/null +++ b/contrib/funind/Recdef.v @@ -0,0 +1,48 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* A) -> A -> A := + fun (fl : A -> A) (def : A) => + match n with + | O => def + | S m => fl (iter m fl def) + end. +End Iter. + +Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')). + intro p; intro p'; change (S p <= S (S (p + p'))); + apply le_S; apply Gt.gt_le_S; change (p < S (p + p')); + apply Lt.le_lt_n_Sm; apply Plus.le_plus_l. +Qed. + + +Theorem Splus_lt : forall p p' : nat, p' < S (p + p'). + intro p; intro p'; change (S p' <= S (p + p')); + apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm; + apply Plus.le_plus_r. +Qed. + +Theorem le_lt_SS : forall x y, x <= y -> x < S (S y). +intro x; intro y; intro H; change (S x <= S (S y)); + apply le_S; apply Gt.gt_le_S; change (x < S y); + apply Lt.le_lt_n_Sm; exact H. +Qed. + +Inductive max_type (m n:nat) : Set := + cmt : forall v, m <= v -> n <= v -> max_type m n. + +Definition max : forall m n:nat, max_type m n. +intros m n; case (Compare_dec.le_gt_dec m n). +intros h; exists n; [exact h | apply le_n]. +intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h]. +Defined. diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 new file mode 100644 index 0000000000..4b3492b125 --- /dev/null +++ b/contrib/funind/g_indfun.ml4 @@ -0,0 +1,485 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + +let pr_bindings prc prlc = function + | Rawterm.ImplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + Util.prlist_with_sep spc prc l + | Rawterm.ExplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | Rawterm.NoBindings -> mt () + +let pr_with_bindings prc prlc (c,bl) = + prc c ++ hv 0 (pr_bindings prc prlc bl) + +let pr_fun_ind_using prc prlc _ opt_c = + match opt_c with + | None -> mt () + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) + +(* Duplication of printing functions because "'a with_bindings" is + (internally) not uniform in 'a: indeed constr_with_bindings at the + "typed" level has type "open_constr with_bindings" instead of + "constr with_bindings"; hence, its printer cannot be polymorphic in + (prc,prlc)... *) + +let pr_with_bindings_typed prc prlc (c,bl) = + prc c ++ + hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) + +let pr_fun_ind_using_typed prc prlc _ opt_c = + match opt_c with + | None -> mt () + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) + + +ARGUMENT EXTEND fun_ind_using + TYPED AS constr_with_bindings_opt + PRINTED BY pr_fun_ind_using_typed + RAW_TYPED AS constr_with_bindings_opt + RAW_PRINTED BY pr_fun_ind_using + GLOB_TYPED AS constr_with_bindings_opt + GLOB_PRINTED BY pr_fun_ind_using +| [ "using" constr_with_bindings(c) ] -> [ Some c ] +| [ ] -> [ None ] +END + + +TACTIC EXTEND newfuninv + [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> + [ + Invfun.invfun hyp fname + ] +END + + +let pr_intro_as_pat prc _ _ pat = + match pat with + | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat + | None -> mt () + + +ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat +| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] +| [] ->[ None ] +END + + + + +TACTIC EXTEND newfunind + ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + [ + let pat = + match pat with + | None -> IntroAnonymous + | Some pat -> pat + in + let c = match cl with + | [] -> assert false + | [c] -> c + | c::cl -> applist(c,cl) + in + functional_induction true c princl pat ] +END +(***** debug only ***) +TACTIC EXTEND snewfunind + ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + [ + let pat = + match pat with + | None -> IntroAnonymous + | Some pat -> pat + in + let c = match cl with + | [] -> assert false + | [c] -> c + | c::cl -> applist(c,cl) + in + functional_induction false c princl pat ] +END + + +let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc + +ARGUMENT EXTEND constr_coma_sequence' + TYPED AS constr_list + PRINTED BY pr_constr_coma_sequence +| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] +| [ constr(c) ] -> [ [c] ] +END + +let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc + +ARGUMENT EXTEND auto_using' + TYPED AS constr_list + PRINTED BY pr_auto_using +| [ "using" constr_coma_sequence'(l) ] -> [ l ] +| [ ] -> [ [] ] +END + +VERNAC ARGUMENT EXTEND rec_annotation2 + [ "{" "struct" ident(id) "}"] -> [ Struct id ] +| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ] +| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] +END + + +VERNAC ARGUMENT EXTEND binder2 + [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> + [ + LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ] +END + + +VERNAC ARGUMENT EXTEND rec_definition2 + [ ident(id) binder2_list( bl) + rec_annotation2_opt(annot) ":" lconstr( type_) + ":=" lconstr(def)] -> + [let names = List.map snd (Topconstr.names_of_local_assums bl) in + let check_one_name () = + if List.length names > 1 then + Util.user_err_loc + (Util.dummy_loc,"Function", + Pp.str "the recursive argument needs to be specified"); + in + let check_exists_args an = + try + let id = match an with + | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id + | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" + in + (try ignore(Util.list_index0 (Name id) names); annot + with Not_found -> Util.user_err_loc + (Util.dummy_loc,"Function", + Pp.str "No argument named " ++ Nameops.pr_id id) + ) + with Failure "check_exists_args" -> check_one_name ();annot + in + let ni = + match annot with + | None -> + annot + | Some an -> + check_exists_args an + in + (id, ni, bl, type_, def) ] + END + + +VERNAC ARGUMENT EXTEND rec_definitions2 +| [ rec_definition2(rd) ] -> [ [rd] ] +| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ] +END + + +VERNAC COMMAND EXTEND Function + ["Function" rec_definitions2(recsl)] -> + [ + do_generate_principle false recsl; + + ] +END + + +VERNAC ARGUMENT EXTEND fun_scheme_arg +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] +END + +VERNAC ARGUMENT EXTEND fun_scheme_args +| [ fun_scheme_arg(fa) ] -> [ [fa] ] +| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas] +END + +VERNAC COMMAND EXTEND NewFunctionalScheme + ["Functional" "Scheme" fun_scheme_args(fas) ] -> + [ + try + Functional_principles_types.build_scheme fas + with Functional_principles_types.No_graph_found -> + match fas with + | (_,fun_name,_)::_ -> + begin + begin + make_graph (Nametab.global fun_name) + end + ; + try Functional_principles_types.build_scheme fas + with Functional_principles_types.No_graph_found -> + Util.error ("Cannot generate induction principle(s)") + end + | _ -> assert false (* we can only have non empty list *) + ] +END +(***** debug only ***) + +VERNAC COMMAND EXTEND NewFunctionalCase + ["Functional" "Case" fun_scheme_arg(fas) ] -> + [ + Functional_principles_types.build_case_scheme fas + ] +END + +(***** debug only ***) +VERNAC COMMAND EXTEND GenerateGraph +["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] +END + + + + + +(* FINDUCTION *) + +(* comment this line to see debug msgs *) +let msg x = () ;; let pr_lconstr c = str "" + (* uncomment this to see debugging *) +let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prlistconstr lc = List.iter prconstr lc +let prstr s = msg(str s) +let prNamedConstr s c = + begin + msg(str ""); + msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n"); + msg(str ""); + end + + + +(** Information about an occurrence of a function call (application) + inside a term. *) +type fapp_info = { + fname: constr; (** The function applied *) + largs: constr list; (** List of arguments *) + free: bool; (** [true] if all arguments are debruijn free *) + max_rel: int; (** max debruijn index in the funcall *) + onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *) +} + + +(** [constr_head_match(a b c) a] returns true, false otherwise. *) +let constr_head_match u t= + if isApp u + then + let uhd,args= destApp u in + uhd=t + else false + +(** [hdMatchSub inu t] returns the list of occurrences of [t] in + [inu]. DeBruijn are not pushed, so some of them may be unbound in + the result. *) +let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = + let subres = + match kind_of_term inu with + | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> + hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test + | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *) + Array.fold_left + (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) + [] bl + | _ -> (* Cofix will be wrong *) + fold_constr + (fun l cstr -> + l @ hdMatchSub cstr test) [] inu in + if not (test inu) then subres + else + let f,args = decompose_app inu in + let freeset = Termops.free_rels inu in + let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in + {fname = f; largs = args; free = Util.Intset.is_empty freeset; + max_rel = max_rel; onlyvars = List.for_all isVar args } + ::subres + +let mkEq typ c1 c2 = + mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|]) + + +let poseq_unsafe idunsafe cstr gl = + let typ = Tacmach.pf_type_of gl cstr in + tclTHEN + (Tactics.letin_tac true (Name idunsafe) cstr allClauses) + (tclTHENFIRST + (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) + Tactics.reflexivity) + gl + + +let poseq id cstr gl = + let x = Tactics.fresh_id [] id gl in + poseq_unsafe x cstr gl + +(* dirty? *) + +let list_constr_largs = ref [] + +let rec poseq_list_ids_rec lcstr gl = + match lcstr with + | [] -> tclIDTAC gl + | c::lcstr' -> + match kind_of_term c with + | Var _ -> + (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl) + | _ -> + let _ = prstr "c = " in + let _ = prconstr c in + let _ = prstr "\n" in + let typ = Tacmach.pf_type_of gl c in + let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in + let x = Tactics.fresh_id [] cname gl in + let _ = list_constr_largs:=mkVar x :: !list_constr_largs in + let _ = prstr " list_constr_largs = " in + let _ = prlistconstr !list_constr_largs in + let _ = prstr "\n" in + + tclTHEN + (poseq_unsafe x c) + (poseq_list_ids_rec lcstr') + gl + +let poseq_list_ids lcstr gl = + let _ = list_constr_largs := [] in + poseq_list_ids_rec lcstr gl + +(** [find_fapp test g] returns the list of [app_info] of all calls to + functions that satisfy [test] in the conclusion of goal g. Trivial + repetition (not modulo conversion) are deleted. *) +let find_fapp (test:constr -> bool) g : fapp_info list = + let pre_res = hdMatchSub (Tacmach.pf_concl g) test in + let res = + List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in + (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); + res) + + + +(** [finduction id filter g] tries to apply functional induction on + an occurence of function [id] in the conclusion of goal [g]. If + [id]=[None] then calls to any function are selected. In any case + [heuristic] is used to select the most pertinent occurrence. *) +let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list) + (nexttac:Proof_type.tactic) g = + let test = match oid with + | Some id -> + let idconstr = mkConst (const_of_id id) in + (fun u -> constr_head_match u idconstr) (* select only id *) + | None -> (fun u -> isApp u) in (* select calls to any function *) + let info_list = find_fapp test g in + let ordered_info_list = heuristic info_list in + prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); + if List.length ordered_info_list = 0 then Util.error "function not found in goal\n"; + let taclist: Proof_type.tactic list = + List.map + (fun info -> + (tclTHEN + (tclTHEN (poseq_list_ids info.largs) + ( + fun gl -> + (functional_induction + true (applist (info.fname, List.rev !list_constr_largs)) + None IntroAnonymous) gl)) + nexttac)) ordered_info_list in + (* we try each (f t u v) until one does not fail *) + (* TODO: try also to mix functional schemes *) + tclFIRST taclist g + + + + +(** [chose_heuristic oi x] returns the heuristic for reordering + (and/or forgetting some elts of) a list of occurrences of + function calls infos to chose first with functional induction. *) +let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = + match oi with + | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *) + | None -> + (* Default heuristic: put first occurrences where all arguments + are *bound* (meaning already introduced) variables *) + let ordering x y = + if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *) + else if x.free && x.onlyvars then -1 + else if y.free && y.onlyvars then 1 + else 0 (* both not pertinent *) + in + List.sort ordering + + + +TACTIC EXTEND finduction + ["finduction" ident(id) natural_opt(oi)] -> + [ + match oi with + | Some(n) when n<=0 -> Util.error "numerical argument must be > 0" + | _ -> + let heuristic = chose_heuristic oi in + finduction (Some id) heuristic tclIDTAC + ] +END + + + +TACTIC EXTEND fauto + [ "fauto" tactic(tac)] -> + [ + let heuristic = chose_heuristic None in + finduction None heuristic (snd tac) + ] + | + [ "fauto" ] -> + [ + let heuristic = chose_heuristic None in + finduction None heuristic tclIDTAC + ] + +END + + +TACTIC EXTEND poseq + [ "poseq" ident(x) constr(c) ] -> + [ poseq x c ] +END + +VERNAC COMMAND EXTEND Showindinfo + [ "showindinfo" ident(x) ] -> [ Merge.showind x ] +END + +VERNAC COMMAND EXTEND MergeFunind + [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" + "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> + [ + let f1 = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Util.dummy_loc,id1))) in + let f2 = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Util.dummy_loc,id2))) in + let f1type = Typing.type_of (Global.env()) Evd.empty f1 in + let f2type = Typing.type_of (Global.env()) Evd.empty f2 in + let ar1 = List.length (fst (decompose_prod f1type)) in + let ar2 = List.length (fst (decompose_prod f2type)) in + let _ = + if ar1 <> List.length cl1 then + Util.error ("not the right number of arguments for " ^ string_of_id id1) in + let _ = + if ar2 <> List.length cl2 then + Util.error ("not the right number of arguments for " ^ string_of_id id2) in + Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id + ] +END diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 deleted file mode 100644 index 4b3492b125..0000000000 --- a/contrib/funind/indfun_main.ml4 +++ /dev/null @@ -1,485 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - -let pr_bindings prc prlc = function - | Rawterm.ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l - | Rawterm.ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Rawterm.NoBindings -> mt () - -let pr_with_bindings prc prlc (c,bl) = - prc c ++ hv 0 (pr_bindings prc prlc bl) - -let pr_fun_ind_using prc prlc _ opt_c = - match opt_c with - | None -> mt () - | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) - -(* Duplication of printing functions because "'a with_bindings" is - (internally) not uniform in 'a: indeed constr_with_bindings at the - "typed" level has type "open_constr with_bindings" instead of - "constr with_bindings"; hence, its printer cannot be polymorphic in - (prc,prlc)... *) - -let pr_with_bindings_typed prc prlc (c,bl) = - prc c ++ - hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) - -let pr_fun_ind_using_typed prc prlc _ opt_c = - match opt_c with - | None -> mt () - | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) - - -ARGUMENT EXTEND fun_ind_using - TYPED AS constr_with_bindings_opt - PRINTED BY pr_fun_ind_using_typed - RAW_TYPED AS constr_with_bindings_opt - RAW_PRINTED BY pr_fun_ind_using - GLOB_TYPED AS constr_with_bindings_opt - GLOB_PRINTED BY pr_fun_ind_using -| [ "using" constr_with_bindings(c) ] -> [ Some c ] -| [ ] -> [ None ] -END - - -TACTIC EXTEND newfuninv - [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> - [ - Invfun.invfun hyp fname - ] -END - - -let pr_intro_as_pat prc _ _ pat = - match pat with - | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat - | None -> mt () - - -ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat -| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] -| [] ->[ None ] -END - - - - -TACTIC EXTEND newfunind - ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in - let c = match cl with - | [] -> assert false - | [c] -> c - | c::cl -> applist(c,cl) - in - functional_induction true c princl pat ] -END -(***** debug only ***) -TACTIC EXTEND snewfunind - ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in - let c = match cl with - | [] -> assert false - | [c] -> c - | c::cl -> applist(c,cl) - in - functional_induction false c princl pat ] -END - - -let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc - -ARGUMENT EXTEND constr_coma_sequence' - TYPED AS constr_list - PRINTED BY pr_constr_coma_sequence -| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] -| [ constr(c) ] -> [ [c] ] -END - -let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc - -ARGUMENT EXTEND auto_using' - TYPED AS constr_list - PRINTED BY pr_auto_using -| [ "using" constr_coma_sequence'(l) ] -> [ l ] -| [ ] -> [ [] ] -END - -VERNAC ARGUMENT EXTEND rec_annotation2 - [ "{" "struct" ident(id) "}"] -> [ Struct id ] -| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ] -| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] -END - - -VERNAC ARGUMENT EXTEND binder2 - [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> - [ - LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ] -END - - -VERNAC ARGUMENT EXTEND rec_definition2 - [ ident(id) binder2_list( bl) - rec_annotation2_opt(annot) ":" lconstr( type_) - ":=" lconstr(def)] -> - [let names = List.map snd (Topconstr.names_of_local_assums bl) in - let check_one_name () = - if List.length names > 1 then - Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified"); - in - let check_exists_args an = - try - let id = match an with - | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id - | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" - in - (try ignore(Util.list_index0 (Name id) names); annot - with Not_found -> Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "No argument named " ++ Nameops.pr_id id) - ) - with Failure "check_exists_args" -> check_one_name ();annot - in - let ni = - match annot with - | None -> - annot - | Some an -> - check_exists_args an - in - (id, ni, bl, type_, def) ] - END - - -VERNAC ARGUMENT EXTEND rec_definitions2 -| [ rec_definition2(rd) ] -> [ [rd] ] -| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ] -END - - -VERNAC COMMAND EXTEND Function - ["Function" rec_definitions2(recsl)] -> - [ - do_generate_principle false recsl; - - ] -END - - -VERNAC ARGUMENT EXTEND fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] -END - -VERNAC ARGUMENT EXTEND fun_scheme_args -| [ fun_scheme_arg(fa) ] -> [ [fa] ] -| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas] -END - -VERNAC COMMAND EXTEND NewFunctionalScheme - ["Functional" "Scheme" fun_scheme_args(fas) ] -> - [ - try - Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - match fas with - | (_,fun_name,_)::_ -> - begin - begin - make_graph (Nametab.global fun_name) - end - ; - try Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - Util.error ("Cannot generate induction principle(s)") - end - | _ -> assert false (* we can only have non empty list *) - ] -END -(***** debug only ***) - -VERNAC COMMAND EXTEND NewFunctionalCase - ["Functional" "Case" fun_scheme_arg(fas) ] -> - [ - Functional_principles_types.build_case_scheme fas - ] -END - -(***** debug only ***) -VERNAC COMMAND EXTEND GenerateGraph -["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] -END - - - - - -(* FINDUCTION *) - -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" - (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) -let prNamedConstr s c = - begin - msg(str ""); - msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n"); - msg(str ""); - end - - - -(** Information about an occurrence of a function call (application) - inside a term. *) -type fapp_info = { - fname: constr; (** The function applied *) - largs: constr list; (** List of arguments *) - free: bool; (** [true] if all arguments are debruijn free *) - max_rel: int; (** max debruijn index in the funcall *) - onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *) -} - - -(** [constr_head_match(a b c) a] returns true, false otherwise. *) -let constr_head_match u t= - if isApp u - then - let uhd,args= destApp u in - uhd=t - else false - -(** [hdMatchSub inu t] returns the list of occurrences of [t] in - [inu]. DeBruijn are not pushed, so some of them may be unbound in - the result. *) -let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = - let subres = - match kind_of_term inu with - | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> - hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test - | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *) - Array.fold_left - (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) - [] bl - | _ -> (* Cofix will be wrong *) - fold_constr - (fun l cstr -> - l @ hdMatchSub cstr test) [] inu in - if not (test inu) then subres - else - let f,args = decompose_app inu in - let freeset = Termops.free_rels inu in - let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in - {fname = f; largs = args; free = Util.Intset.is_empty freeset; - max_rel = max_rel; onlyvars = List.for_all isVar args } - ::subres - -let mkEq typ c1 c2 = - mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|]) - - -let poseq_unsafe idunsafe cstr gl = - let typ = Tacmach.pf_type_of gl cstr in - tclTHEN - (Tactics.letin_tac true (Name idunsafe) cstr allClauses) - (tclTHENFIRST - (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) - Tactics.reflexivity) - gl - - -let poseq id cstr gl = - let x = Tactics.fresh_id [] id gl in - poseq_unsafe x cstr gl - -(* dirty? *) - -let list_constr_largs = ref [] - -let rec poseq_list_ids_rec lcstr gl = - match lcstr with - | [] -> tclIDTAC gl - | c::lcstr' -> - match kind_of_term c with - | Var _ -> - (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl) - | _ -> - let _ = prstr "c = " in - let _ = prconstr c in - let _ = prstr "\n" in - let typ = Tacmach.pf_type_of gl c in - let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in - let x = Tactics.fresh_id [] cname gl in - let _ = list_constr_largs:=mkVar x :: !list_constr_largs in - let _ = prstr " list_constr_largs = " in - let _ = prlistconstr !list_constr_largs in - let _ = prstr "\n" in - - tclTHEN - (poseq_unsafe x c) - (poseq_list_ids_rec lcstr') - gl - -let poseq_list_ids lcstr gl = - let _ = list_constr_largs := [] in - poseq_list_ids_rec lcstr gl - -(** [find_fapp test g] returns the list of [app_info] of all calls to - functions that satisfy [test] in the conclusion of goal g. Trivial - repetition (not modulo conversion) are deleted. *) -let find_fapp (test:constr -> bool) g : fapp_info list = - let pre_res = hdMatchSub (Tacmach.pf_concl g) test in - let res = - List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in - (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); - res) - - - -(** [finduction id filter g] tries to apply functional induction on - an occurence of function [id] in the conclusion of goal [g]. If - [id]=[None] then calls to any function are selected. In any case - [heuristic] is used to select the most pertinent occurrence. *) -let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list) - (nexttac:Proof_type.tactic) g = - let test = match oid with - | Some id -> - let idconstr = mkConst (const_of_id id) in - (fun u -> constr_head_match u idconstr) (* select only id *) - | None -> (fun u -> isApp u) in (* select calls to any function *) - let info_list = find_fapp test g in - let ordered_info_list = heuristic info_list in - prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); - if List.length ordered_info_list = 0 then Util.error "function not found in goal\n"; - let taclist: Proof_type.tactic list = - List.map - (fun info -> - (tclTHEN - (tclTHEN (poseq_list_ids info.largs) - ( - fun gl -> - (functional_induction - true (applist (info.fname, List.rev !list_constr_largs)) - None IntroAnonymous) gl)) - nexttac)) ordered_info_list in - (* we try each (f t u v) until one does not fail *) - (* TODO: try also to mix functional schemes *) - tclFIRST taclist g - - - - -(** [chose_heuristic oi x] returns the heuristic for reordering - (and/or forgetting some elts of) a list of occurrences of - function calls infos to chose first with functional induction. *) -let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = - match oi with - | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *) - | None -> - (* Default heuristic: put first occurrences where all arguments - are *bound* (meaning already introduced) variables *) - let ordering x y = - if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *) - else if x.free && x.onlyvars then -1 - else if y.free && y.onlyvars then 1 - else 0 (* both not pertinent *) - in - List.sort ordering - - - -TACTIC EXTEND finduction - ["finduction" ident(id) natural_opt(oi)] -> - [ - match oi with - | Some(n) when n<=0 -> Util.error "numerical argument must be > 0" - | _ -> - let heuristic = chose_heuristic oi in - finduction (Some id) heuristic tclIDTAC - ] -END - - - -TACTIC EXTEND fauto - [ "fauto" tactic(tac)] -> - [ - let heuristic = chose_heuristic None in - finduction None heuristic (snd tac) - ] - | - [ "fauto" ] -> - [ - let heuristic = chose_heuristic None in - finduction None heuristic tclIDTAC - ] - -END - - -TACTIC EXTEND poseq - [ "poseq" ident(x) constr(c) ] -> - [ poseq x c ] -END - -VERNAC COMMAND EXTEND Showindinfo - [ "showindinfo" ident(x) ] -> [ Merge.showind x ] -END - -VERNAC COMMAND EXTEND MergeFunind - [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" - "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> - [ - let f1 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Util.dummy_loc,id1))) in - let f2 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Util.dummy_loc,id2))) in - let f1type = Typing.type_of (Global.env()) Evd.empty f1 in - let f2type = Typing.type_of (Global.env()) Evd.empty f2 in - let ar1 = List.length (fst (decompose_prod f1type)) in - let ar2 = List.length (fst (decompose_prod f2type)) in - let _ = - if ar1 <> List.length cl1 then - Util.error ("not the right number of arguments for " ^ string_of_id id1) in - let _ = - if ar2 <> List.length cl2 then - Util.error ("not the right number of arguments for " ^ string_of_id id2) in - Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id - ] -END diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml new file mode 100644 index 0000000000..49c07ff72e --- /dev/null +++ b/contrib/funind/recdef.ml @@ -0,0 +1,1430 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* next_global_ident_away false id (acc@ids)::acc) + idl + [] + +let pf_get_new_id id g = + List.hd (pf_get_new_ids [id] g) + +let h_intros l = + tclMAP h_intro l + +let do_observe_tac s tac g = + let goal = begin (Printer.pr_goal (sig_it g)) end in + try let v = tac g in msgnl (goal ++ fnl () ++ (str "recdef ") ++ + (str s)++(str " ")++(str "finished")); v + with e -> + msgnl (str "observation "++str s++str " raised exception " ++ + Cerrors.explain_exn e ++ str " on goal " ++ goal ); + raise e;; + + +let observe_tac s tac g = + if Tacinterp.get_debug () <> Tactic_debug.DebugOff + then do_observe_tac s tac g + else tac g + +let hyp_ids = List.map id_of_string + ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res"; + "hspec";"heq"; "hrec"; "hex"; "teq"; "pmax";"hle"];; + +let rec nthtl = function + l, 0 -> l | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];; + +let hyp_id n l = List.nth l n;; + +let (x_id:identifier) = hyp_id 0 hyp_ids;; +let (v_id:identifier) = hyp_id 1 hyp_ids;; +let (k_id:identifier) = hyp_id 2 hyp_ids;; +let (def_id:identifier) = hyp_id 3 hyp_ids;; +let (p_id:identifier) = hyp_id 4 hyp_ids;; +let (h_id:identifier) = hyp_id 5 hyp_ids;; +let (n_id:identifier) = hyp_id 6 hyp_ids;; +let (h'_id:identifier) = hyp_id 7 hyp_ids;; +let (ano_id:identifier) = hyp_id 8 hyp_ids;; +let (rec_res_id:identifier) = hyp_id 10 hyp_ids;; +let (hspec_id:identifier) = hyp_id 11 hyp_ids;; +let (heq_id:identifier) = hyp_id 12 hyp_ids;; +let (hrec_id:identifier) = hyp_id 13 hyp_ids;; +let (hex_id:identifier) = hyp_id 14 hyp_ids;; +let (teq_id:identifier) = hyp_id 15 hyp_ids;; +let (pmax_id:identifier) = hyp_id 16 hyp_ids;; +let (hle_id:identifier) = hyp_id 17 hyp_ids;; + +let message s = if Flags.is_verbose () then msgnl(str s);; + +let def_of_const t = + match (kind_of_term t) with + Const sp -> + (try (match (Global.lookup_constant sp) with + {const_body=Some c} -> Declarations.force c + |_ -> assert false) + with _ -> + anomaly ("Cannot find definition of constant "^ + (string_of_id (id_of_label (con_label sp)))) + ) + |_ -> assert false + +let type_of_const t = + match (kind_of_term t) with + Const sp -> Typeops.type_of_constant (Global.env()) sp + |_ -> assert false + +let arg_type t = + match kind_of_term (def_of_const t) with + Lambda(a,b,c) -> b + | _ -> assert false;; + +let evaluable_of_global_reference r = + match r with + ConstRef sp -> EvalConstRef sp + | VarRef id -> EvalVarRef id + | _ -> assert false;; + + +let rank_for_arg_list h = + let predicate a b = + try List.for_all2 eq_constr a b with + Invalid_argument _ -> false in + let rec rank_aux i = function + | [] -> None + | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in + rank_aux 0;; + +let rec (find_call_occs : int -> constr -> constr -> + (constr list -> constr) * constr list list) = + fun nb_lam f expr -> + match (kind_of_term expr) with + App (g, args) when g = f -> + (fun l -> List.hd l), [Array.to_list args] + | App (g, args) -> + let (largs: constr list) = Array.to_list args in + let rec find_aux = function + [] -> (fun x -> []), [] + | a::upper_tl -> + (match find_aux upper_tl with + (cf, ((arg1::args) as args_for_upper_tl)) -> + (match find_call_occs nb_lam f a with + cf2, (_ :: _ as other_args) -> + let rec avoid_duplicates args = + match args with + | [] -> (fun _ -> []), [] + | h::tl -> + let recomb_tl, args_for_tl = + avoid_duplicates tl in + match rank_for_arg_list h args_for_upper_tl with + | None -> + (fun l -> List.hd l::recomb_tl(List.tl l)), + h::args_for_tl + | Some i -> + (fun l -> List.nth l (i+List.length args_for_tl):: + recomb_tl l), + args_for_tl + in + let recombine, other_args' = + avoid_duplicates other_args in + let len1 = List.length other_args' in + (fun l -> cf2 (recombine l)::cf(nthtl(l,len1))), + other_args'@args_for_upper_tl + | _, [] -> (fun x -> a::cf x), args_for_upper_tl) + | _, [] -> + (match find_call_occs nb_lam f a with + cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args) + | _, [] -> (fun x -> a::upper_tl), [])) in + begin + match (find_aux largs) with + cf, [] -> (fun l -> mkApp(g, args)), [] + | cf, args -> + (fun l -> mkApp (g, Array.of_list (cf l))), args + end + | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[]) + | Var(id) -> (fun l -> expr), [] + | Meta(_) -> error "find_call_occs : Meta" + | Evar(_) -> error "find_call_occs : Evar" + | Sort(_) -> (fun l -> expr), [] + | Cast(b,_,_) -> find_call_occs nb_lam f b + | Prod(_,_,_) -> error "find_call_occs : Prod" + | Lambda(na,t,b) -> + begin + match find_call_occs (succ nb_lam) f b with + | _, [] -> (* Lambda are authorized as long as they do not contain + recursives calls *) + (fun l -> expr),[] + | _ -> error "find_call_occs : Lambda" + end + | LetIn(na,v,t,b) -> + begin + match find_call_occs nb_lam f v, find_call_occs (succ nb_lam) f b with + | (_,[]),(_,[]) -> + ((fun l -> expr), []) + | (_,[]),(cf,(_::_ as l)) -> + ((fun l -> mkLetIn(na,v,t,cf l)),l) + | (cf,(_::_ as l)),(_,[]) -> + ((fun l -> mkLetIn(na,cf l,t,b)), l) + | _ -> error "find_call_occs : LetIn" + end + | Const(_) -> (fun l -> expr), [] + | Ind(_) -> (fun l -> expr), [] + | Construct (_, _) -> (fun l -> expr), [] + | Case(i,t,a,r) -> + (match find_call_occs nb_lam f a with + cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args) + | _ -> (fun l -> expr),[]) + | Fix(_) -> error "find_call_occs : Fix" + | CoFix(_) -> error "find_call_occs : CoFix";; + +let coq_constant s = + Coqlib.gen_constant_in_modules "RecursiveDefinition" + (Coqlib.init_modules @ Coqlib.arith_modules) s;; + +let constant sl s = + constr_of_global + (locate (make_qualid(Names.make_dirpath + (List.map id_of_string (List.rev sl))) + (id_of_string s)));; + +let find_reference sl s = + (locate (make_qualid(Names.make_dirpath + (List.map id_of_string (List.rev sl))) + (id_of_string s)));; + +let delayed_force f = f () + +let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") +let le_lt_n_Sm = function () -> (coq_constant "le_lt_n_Sm") + +let le_trans = function () -> (coq_constant "le_trans") +let le_lt_trans = function () -> (coq_constant "le_lt_trans") +let lt_S_n = function () -> (coq_constant "lt_S_n") +let le_n = function () -> (coq_constant "le_n") +let refl_equal = function () -> (coq_constant "refl_equal") +let eq = function () -> (coq_constant "eq") +let ex = function () -> (coq_constant "ex") +let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") +let coq_sig = function () -> (coq_constant "sig") +let coq_O = function () -> (coq_constant "O") +let coq_S = function () -> (coq_constant "S") + +let gt_antirefl = function () -> (coq_constant "gt_irrefl") +let lt_n_O = function () -> (coq_constant "lt_n_O") +let lt_n_Sn = function () -> (coq_constant "lt_n_Sn") + +let f_equal = function () -> (coq_constant "f_equal") +let well_founded_induction = function () -> (coq_constant "well_founded_induction") +let well_founded = function () -> (coq_constant "well_founded") +let acc_rel = function () -> (coq_constant "Acc") +let acc_inv_id = function () -> (coq_constant "Acc_inv") +let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof") +let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded") +let max_ref = function () -> (find_reference ["Recdef"] "max") +let iter = function () -> (constr_of_global (delayed_force iter_ref)) +let max_constr = function () -> (constr_of_global (delayed_force max_ref)) + +let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") +let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" + +(* These are specific to experiments in nat with lt as well_founded_relation, *) +(* but this should be made more general. *) +let nat = function () -> (coq_constant "nat") +let lt = function () -> (coq_constant "lt") + +(* This is simply an implementation of the case_eq tactic. this code + should be replaced with the tactic defined in Ltac in Init/Tactics.v *) +let mkCaseEq a : tactic = + (fun g -> + let type_of_a = pf_type_of g a in + tclTHENLIST + [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; + (fun g2 -> + change_in_concl None + (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2)) + g2); + simplest_case a] g);; + +(* This is like the previous one except that it also rewrite on all + hypotheses except the ones given in the first argument. All the + modified hypotheses are generalized in the process and should be + introduced back later; the result is the pair of the tactic and the + list of hypotheses that have been generalized and cleared. *) +let mkDestructEq : + identifier list -> constr -> goal sigma -> tactic * identifier list = + fun not_on_hyp expr g -> + let hyps = pf_hyps g in + let to_revert = + Util.map_succeed + (fun (id,_,t) -> + if List.mem id not_on_hyp || not (Termops.occur_term expr t) + then failwith "is_expr_context"; + id) hyps in + let to_revert_constr = List.rev_map mkVar to_revert in + let type_of_expr = pf_type_of g expr in + let new_hyps = mkApp(delayed_force refl_equal, [|type_of_expr; expr|]):: + to_revert_constr in + tclTHENLIST + [h_generalize new_hyps; + (fun g2 -> + change_in_concl None + (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); + simplest_case expr], to_revert + +let rec mk_intros_and_continue thin_intros (extra_eqn:bool) + cont_function (eqs:constr list) nb_lam (expr:constr) g = + let finalize () = if extra_eqn then + let teq = pf_get_new_id teq_id g in + tclTHENLIST + [ h_intro teq; + thin thin_intros; + h_intros thin_intros; + + tclMAP + (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false)) + (List.rev eqs); + (fun g1 -> + let ty_teq = pf_type_of g1 (mkVar teq) in + let teq_lhs,teq_rhs = + let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in + args.(1),args.(2) + in + cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1 + ) + ] + g + else + tclTHENSEQ[ + thin thin_intros; + h_intros thin_intros; + cont_function eqs expr + ] g + in + if nb_lam = 0 + then finalize () + else + match kind_of_term expr with + | Lambda (n, _, b) -> + let n1 = + match n with + Name x -> x + | Anonymous -> ano_id + in + let new_n = pf_get_new_id n1 g in + tclTHEN (h_intro new_n) + (mk_intros_and_continue thin_intros extra_eqn cont_function eqs + (pred nb_lam) (subst1 (mkVar new_n) b)) g + | _ -> + assert false +(* finalize () *) +let const_of_ref = function + ConstRef kn -> kn + | _ -> anomaly "ConstRef expected" + +let simpl_iter clause = + reduce + (Lazy + {rBeta=true;rIota=true;rZeta= true; rDelta=false; + rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]}) +(* (Simpl (Some ([],mkConst (const_of_ref (delayed_force iter_ref))))) *) + clause + +(* The boolean value is_mes expresses that the termination is expressed + using a measure function instead of a well-founded relation. *) +let tclUSER tac is_mes l g = + let clear_tac = + match l with + | None -> h_clear true [] + | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l) + in + tclTHENSEQ + [ + clear_tac; + if is_mes + then tclTHEN + (unfold_in_concl [([], evaluable_of_global_reference + (delayed_force ltof_ref))]) + tac + else tac + ] + g + + +let list_rewrite (rev:bool) (eqs: constr list) = + tclREPEAT + (List.fold_right + (fun eq i -> tclORELSE (rewriteLR eq) i) + (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; + +let base_leaf_terminate (func:global_reference) eqs expr = +(* let _ = msgnl (str "entering base_leaf") in *) + (fun g -> + let k',h = + match pf_get_new_ids [k_id;h_id] g with + [k';h] -> k',h + | _ -> assert false + in + tclTHENLIST + [observe_tac "first split" (split (ImplicitBindings [expr])); + observe_tac "second split" + (split (ImplicitBindings [delayed_force coq_O])); + observe_tac "intro k" (h_intro k'); + observe_tac "case on k" + (tclTHENS (simplest_case (mkVar k')) + [(tclTHEN (h_intro h) + (tclTHEN (simplest_elim (mkApp (delayed_force gt_antirefl, + [| delayed_force coq_O |]))) + default_auto)); tclIDTAC ]); + intros; + simpl_iter onConcl; + unfold_constr func; + list_rewrite true eqs; + default_auto] g);; + +(* La fonction est donnee en premier argument a la + fonctionnelle suivie d'autres Lambdas et de Case ... + Pour recuperer la fonction f a partir de la + fonctionnelle *) + +let get_f foncl = + match (kind_of_term (def_of_const foncl)) with + Lambda (Name f, _, _) -> f + |_ -> error "la fonctionnelle est mal definie";; + + +let rec compute_le_proofs = function + [] -> assumption + | a::tl -> + tclORELSE assumption + (tclTHENS + (fun g -> + let le_trans = delayed_force le_trans in + let t_le_trans = compute_renamed_type g le_trans in + let m_id = + let _,_,t = destProd t_le_trans in + let na,_,_ = destProd t in + Nameops.out_name na + in + apply_with_bindings + (le_trans, + ExplicitBindings[dummy_loc,NamedHyp m_id,a]) + g) + [compute_le_proofs tl; + tclORELSE (apply (delayed_force le_n)) assumption]) + +let make_lt_proof pmax le_proof = + tclTHENS + (fun g -> + let le_lt_trans = delayed_force le_lt_trans in + let t_le_lt_trans = compute_renamed_type g le_lt_trans in + let m_id = + let _,_,t = destProd t_le_lt_trans in + let na,_,_ = destProd t in + Nameops.out_name na + in + apply_with_bindings + (le_lt_trans, + ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g) + [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); + tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];; + +let rec list_cond_rewrite k def pmax cond_eqs le_proofs = + match cond_eqs with + [] -> tclIDTAC + | eq::eqs -> + (fun g -> + let t_eq = compute_renamed_type g (mkVar eq) in + let k_id,def_id = + let k_na,_,t = destProd t_eq in + let _,_,t = destProd t in + let def_na,_,_ = destProd t in + Nameops.out_name k_na,Nameops.out_name def_na + in + tclTHENS + (general_rewrite_bindings false [] + (mkVar eq, + ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; + dummy_loc, NamedHyp def_id, mkVar def]) false) + [list_cond_rewrite k def pmax eqs le_proofs; + observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g + ) + +let rec introduce_all_equalities func eqs values specs bound le_proofs + cond_eqs = + match specs with + [] -> + fun g -> + let ids = pf_ids_of_hyps g in + let s_max = mkApp(delayed_force coq_S, [|bound|]) in + let k = next_global_ident_away true k_id ids in + let ids = k::ids in + let h' = next_global_ident_away true (h'_id) ids in + let ids = h'::ids in + let def = next_global_ident_away true def_id ids in + tclTHENLIST + [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max])); + observe_tac "introduce_all_equalities_final intro k" (h_intro k); + tclTHENS + (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k))) + [ + tclTHENLIST[h_intro h'; + simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])); + default_full_auto]; + tclIDTAC + ]; + observe_tac "clearing k " (clear [k]); + observe_tac "intros k h' def" (h_intros [k;h';def]); + observe_tac "simple_iter" (simpl_iter onConcl); + observe_tac "unfold functional" + (unfold_in_concl[([1],evaluable_of_global_reference func)]); + observe_tac "rewriting equations" + (list_rewrite true eqs); + observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs); + observe_tac "refl equal" (apply (delayed_force refl_equal))] g + | spec1::specs -> + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + let p = next_global_ident_away true p_id ids in + let ids = p::ids in + let pmax = next_global_ident_away true pmax_id ids in + let ids = pmax::ids in + let hle1 = next_global_ident_away true hle_id ids in + let ids = hle1::ids in + let hle2 = next_global_ident_away true hle_id ids in + let ids = hle2::ids in + let heq = next_global_ident_away true heq_id ids in + tclTHENLIST + [simplest_elim (mkVar spec1); + list_rewrite true eqs; + h_intros [p; heq]; + simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|])); + h_intros [pmax; hle1; hle2]; + introduce_all_equalities func eqs values specs + (mkVar pmax) ((mkVar pmax)::le_proofs) + (heq::cond_eqs)] g;; + +let string_match s = + if String.length s < 3 then failwith "string_match"; + try + for i = 0 to 3 do + if String.get s i <> String.get "Acc_" i then failwith "string_match" + done; + with Invalid_argument _ -> failwith "string_match" + +let retrieve_acc_var g = + (* Julien: I don't like this version .... *) + let hyps = pf_ids_of_hyps g in + map_succeed + (fun id -> string_match (string_of_id id);id) + hyps + +let rec introduce_all_values concl_tac is_mes acc_inv func context_fn + eqs hrec args values specs = + (match args with + [] -> + tclTHENLIST + [observe_tac "split" (split(ImplicitBindings + [context_fn (List.map mkVar (List.rev values))])); + observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs + (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])] + | arg::args -> + (fun g -> + let ids = ids_of_named_context (pf_hyps g) in + let rec_res = next_global_ident_away true rec_res_id ids in + let ids = rec_res::ids in + let hspec = next_global_ident_away true hspec_id ids in + let tac = + observe_tac "introduce_all_values" ( + introduce_all_values concl_tac is_mes acc_inv func context_fn eqs + hrec args + (rec_res::values)(hspec::specs)) in + (tclTHENS + (observe_tac "elim h_rec" + (simplest_elim (mkApp(mkVar hrec, Array.of_list arg))) + ) + [tclTHENLIST [h_intros [rec_res; hspec]; + tac]; + (tclTHENS + (observe_tac "acc_inv" (apply (Lazy.force acc_inv))) + [(* tclTHEN (tclTRY(list_rewrite true eqs)) *) + (observe_tac "h_assumption" h_assumption) + ; + tclTHENLIST + [ + tclTRY(list_rewrite true eqs); + observe_tac "user proof" + (fun g -> + tclUSER + concl_tac + is_mes + (Some (hrec::hspec::(retrieve_acc_var g)@specs)) + g + ) + ] + ] + ) + ]) g) + + ) + + +let rec_leaf_terminate concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = + match find_call_occs 0 (mkVar (get_f (constr_of_global func))) expr with + | context_fn, args -> + observe_tac "introduce_all_values" + (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] []) + +let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier) + (f_constr:constr) (func:global_reference) base_leaf rec_leaf = + let rec proveterminate (eqs:constr list) (expr:constr) = + try + (* let _ = msgnl (str "entering proveterminate") in *) + let v = + match (kind_of_term expr) with + Case (ci, t, a, l) -> + (match find_call_occs 0 f_constr a with + _,[] -> + (fun g -> + let destruct_tac, rev_to_thin_intro = + mkDestructEq rec_arg_id a g in + tclTHENS destruct_tac + (list_map_i + (fun i -> mk_intros_and_continue + (List.rev rev_to_thin_intro) + true + proveterminate + eqs + ci.ci_cstr_nargs.(i)) + 0 (Array.to_list l)) g) + | _, _::_ -> + (match find_call_occs 0 f_constr expr with + _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr) + | _, _:: _ -> + observe_tac "rec_leaf" + (rec_leaf is_mes acc_inv hrec func eqs expr))) + | _ -> + (match find_call_occs 0 f_constr expr with + _,[] -> + (try observe_tac "base_leaf" (base_leaf func eqs expr) + with e -> (msgerrnl (str "failure in base case");raise e )) + | _, _::_ -> + observe_tac "rec_leaf" + (rec_leaf is_mes acc_inv hrec func eqs expr)) in + v + with e -> begin msgerrnl(str "failure in proveterminate"); raise e end + in + proveterminate + +let hyp_terminates nb_args func = + let a_arrow_b = arg_type (constr_of_global func) in + let rev_args,b = decompose_prod_n nb_args a_arrow_b in + let left = + mkApp(delayed_force iter, + Array.of_list + (lift 5 a_arrow_b:: mkRel 3:: + constr_of_global func::mkRel 1:: + List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args) + ) + ) + in + let right = mkRel 5 in + let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in + let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in + let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in + let nb_iter = + mkApp(delayed_force ex, + [|delayed_force nat; + (mkLambda + (Name + p_id, + delayed_force nat, + (mkProd (Name k_id, delayed_force nat, + mkArrow cond result))))|])in + let value = mkApp(delayed_force coq_sig, + [|b; + (mkLambda (Name v_id, b, nb_iter))|]) in + compose_prod rev_args value + + + +let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = + if is_mes + then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof)) + else tclUSER concl_tac is_mes names_to_suppress + +let termination_proof_header is_mes input_type ids args_id relation + rec_arg_num rec_arg_id tac wf_tac : tactic = + begin + fun g -> + let nargs = List.length args_id in + let pre_rec_args = + List.rev_map + mkVar (fst (list_chop (rec_arg_num - 1) args_id)) + in + let relation = substl pre_rec_args relation in + let input_type = substl pre_rec_args input_type in + let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in + let wf_rec_arg = + next_global_ident_away true + (id_of_string ("Acc_"^(string_of_id rec_arg_id))) + (wf_thm::ids) + in + let hrec = next_global_ident_away true hrec_id + (wf_rec_arg::wf_thm::ids) in + let acc_inv = + lazy ( + mkApp ( + delayed_force acc_inv_id, + [|input_type;relation;mkVar rec_arg_id|] + ) + ) + in + tclTHEN + (h_intros args_id) + (tclTHENS + (observe_tac + "first assert" + (assert_tac + true (* the assert thm is in first subgoal *) + (Name wf_rec_arg) + (mkApp (delayed_force acc_rel, + [|input_type;relation;mkVar rec_arg_id|]) + ) + ) + ) + [ + (* accesibility proof *) + tclTHENS + (observe_tac + "second assert" + (assert_tac + true + (Name wf_thm) + (mkApp (delayed_force well_founded,[|input_type;relation|])) + ) + ) + [ + (* interactive proof that the relation is well_founded *) + observe_tac "wf_tac" (wf_tac is_mes (Some args_id)); + (* this gives the accessibility argument *) + observe_tac + "apply wf_thm" + (h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])) + ) + ] + ; + (* rest of the proof *) + tclTHENSEQ + [observe_tac "generalize" + (onNLastHyps (nargs+1) + (fun (id,_,_) -> + tclTHEN (h_generalize [mkVar id]) (h_clear false [id]) + )) + ; + observe_tac "h_fix" (h_fix (Some hrec) (nargs+1)); + h_intros args_id; + h_intro wf_rec_arg; + observe_tac "tac" (tac wf_rec_arg hrec acc_inv) + ] + ] + ) g + end + + + +let rec instantiate_lambda t l = + match l with + | [] -> t + | a::l -> + let (bound_name, _, body) = destLambda t in + instantiate_lambda (subst1 a body) l +;; + + +let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic = + begin + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + let func_body = (def_of_const (constr_of_global func)) in + let (f_name, _, body1) = destLambda func_body in + let f_id = + match f_name with + | Name f_id -> next_global_ident_away true f_id ids + | Anonymous -> anomaly "Anonymous function" + in + let n_names_types,_ = decompose_lam_n nb_args body1 in + let n_ids,ids = + List.fold_left + (fun (n_ids,ids) (n_name,_) -> + match n_name with + | Name id -> + let n_id = next_global_ident_away true id ids in + n_id::n_ids,n_id::ids + | _ -> anomaly "anonymous argument" + ) + ([],(f_id::ids)) + n_names_types + in + let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in + let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in + termination_proof_header + is_mes + input_type + ids + n_ids + relation + rec_arg_num + rec_arg_id + (fun rec_arg_id hrec acc_inv g -> + (proveterminate + [rec_arg_id] + is_mes + acc_inv + hrec + (mkVar f_id) + func + base_leaf_terminate + (rec_leaf_terminate concl_tac) + [] + expr + ) + g + ) + (tclUSER_if_not_mes concl_tac) + g + end + +let get_current_subgoals_types () = + let pts = get_pftreestate () in + let _,subs = extract_open_pftreestate pts in + List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs ) + +let build_and_l l = + let and_constr = Coqlib.build_coq_and () in + let conj_constr = coq_conj () in + let mk_and p1 p2 = + Term.mkApp(and_constr,[|p1;p2|]) in + let rec f = function + | [] -> failwith "empty list of subgoals!" + | [p] -> p,tclIDTAC,1 + | p1::pl -> + let c,tac,nb = f pl in + mk_and p1 c, + tclTHENS + (apply (constr_of_global conj_constr)) + [tclIDTAC; + tac + ],nb+1 + in f l + + +let is_rec_res id = + let rec_res_name = string_of_id rec_res_id in + let id_name = string_of_id id in + try + String.sub id_name 0 (String.length rec_res_name) = rec_res_name + with _ -> false + +let clear_goals = + let rec clear_goal t = + match kind_of_term t with + | Prod(Name id as na,t,b) -> + let b' = clear_goal b in + if noccurn 1 b' && (is_rec_res id) + then pop b' + else if b' == b then t + else mkProd(na,t,b') + | _ -> map_constr clear_goal t + in + List.map clear_goal + + +let build_new_goal_type () = + let sub_gls_types = get_current_subgoals_types () in + let sub_gls_types = clear_goals sub_gls_types in + let res = build_and_l sub_gls_types in + res + + + (* +let prove_with_tcc lemma _ : tactic = + fun gls -> + let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in + tclTHENSEQ + [ + h_generalize [lemma]; + h_intro hid; + Elim.h_decompose_and (mkVar hid); + gen_eauto(* default_eauto *) false (false,5) [] (Some []) + (* default_auto *) + ] + gls + *) + + + +let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = + let current_proof_name = get_current_proof_name () in + let name = match goal_name with + | Some s -> s + | None -> + try (add_suffix current_proof_name "_subproof") + with _ -> anomaly "open_new_goal with an unamed theorem" + in + let sign = Global.named_context () in + let sign = clear_proofs sign in + let na = next_global_ident_away false name [] in + if occur_existential gls_type then + Util.error "\"abstract\" cannot handle existentials"; + let hook _ _ = + let opacity = + let na_ref = Libnames.Ident (dummy_loc,na) in + let na_global = Nametab.global na_ref in + match na_global with + ConstRef c -> + let cb = Global.lookup_constant c in + if cb.Declarations.const_opaque then true + else begin match cb.const_body with None -> true | _ -> false end + | _ -> anomaly "equation_lemma: not a constant" + in + let lemma = mkConst (Lib.make_con na) in + ref_ := Some lemma ; + let lid = ref [] in + let h_num = ref (-1) in + Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None); + build_proof + ( fun gls -> + let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in + tclTHENSEQ + [ + h_generalize [lemma]; + h_intro hid; + (fun g -> + let ids = pf_ids_of_hyps g in + tclTHEN + (Elim.h_decompose_and (mkVar hid)) + (fun g -> + let ids' = pf_ids_of_hyps g in + lid := List.rev (list_subtract ids' ids); + if !lid = [] then lid := [hid]; +(* list_iter_i *) +(* (fun i v -> *) +(* msgnl (str "hyp" ++ int i ++ str " " ++ *) +(* Nameops.pr_id v ++ fnl () ++ fnl())) *) +(* !lid; *) + tclIDTAC g + ) + g + ); + ] gls) + (fun g -> + match kind_of_term (pf_concl g) with + | App(f,_) when eq_constr f (well_founded ()) -> + Auto.h_auto None [] (Some []) g + | _ -> + incr h_num; + tclTHEN + (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) + e_assumption + g) +; + Command.save_named opacity; + in + start_proof + na + (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) + sign + gls_type + hook ; + by ( + fun g -> + tclTHEN + (decompose_and_tac) + (tclORELSE + (tclFIRST + (List.map + (fun c -> + tclTHENSEQ + [intros; + h_simplest_apply (interp_constr Evd.empty (Global.env()) c); + tclCOMPLETE Auto.default_auto + ] + ) + using_lemmas) + ) tclIDTAC) + g); + try + by tclIDTAC; (* raises UserError _ if the proof is complete *) + if Flags.is_verbose () then (pp (Printer.pr_open_subgoals())) + with UserError _ -> + defined () + +;; + + +let com_terminate + tcc_lemma_name + tcc_lemma_ref + is_mes + fonctional_ref + input_type + relation + rec_arg_num + thm_name using_lemmas + nb_args + hook = + let start_proof (tac_start:tactic) (tac_end:tactic) = + let (evmap, env) = Command.get_current_context() in + start_proof thm_name + (Global, Proof Lemma) (Environ.named_context_val env) + (hyp_terminates nb_args fonctional_ref) hook; + by (observe_tac "starting_tac" tac_start); + by (observe_tac "whole_start" (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num )) + + in + start_proof tclIDTAC tclIDTAC; + try + let new_goal_type = build_new_goal_type () in + open_new_goal start_proof using_lemmas tcc_lemma_ref + (Some tcc_lemma_name) + (new_goal_type) + with Failure "empty list of subgoals!" -> + (* a non recursive function declared with measure ! *) + defined () + + + + +let ind_of_ref = function + | IndRef (ind,i) -> (ind,i) + | _ -> anomaly "IndRef expected" + +let (value_f:constr list -> global_reference -> constr) = + fun al fterm -> + let d0 = dummy_loc in + let rev_x_id_l = + ( + List.fold_left + (fun x_id_l _ -> + let x_id = next_global_ident_away true x_id x_id_l in + x_id::x_id_l + ) + [] + al + ) + in + let fun_body = + RCases + (d0,RegularStyle,None, + [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l), + (Anonymous,None)], + [d0, [v_id], [PatCstr(d0,(ind_of_ref + (delayed_force coq_sig_ref),1), + [PatVar(d0, Name v_id); + PatVar(d0, Anonymous)], + Anonymous)], + RVar(d0,v_id)]) + in + let value = + List.fold_left2 + (fun acc x_id a -> + RLambda + (d0, Name x_id, Explicit, RDynamic(d0, constr_in a), + acc + ) + ) + fun_body + rev_x_id_l + (List.rev al) + in + understand Evd.empty (Global.env()) value;; + +let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = + fun f_id kind value -> + let ce = {const_entry_body = value; + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = true} in + ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; + +let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) = + fun f_id kind input_type fterm_ref -> + declare_fun f_id kind (value_f input_type fterm_ref);; + +let rec n_x_id ids n = + if n = 0 then [] + else let x = next_global_ident_away true x_id ids in + x::n_x_id (x::ids) (n-1);; + +let start_equation (f:global_reference) (term_f:global_reference) + (cont_tactic:identifier list -> tactic) g = + let ids = pf_ids_of_hyps g in + let terminate_constr = constr_of_global term_f in + let nargs = nb_prod (type_of_const terminate_constr) in + let x = n_x_id ids nargs in + tclTHENLIST [ + h_intros x; + unfold_in_concl [([], evaluable_of_global_reference f)]; + observe_tac "simplest_case" + (simplest_case (mkApp (terminate_constr, + Array.of_list (List.map mkVar x)))); + observe_tac "prove_eq" (cont_tactic x)] g;; + +let base_leaf_eq func eqs f_id g = + let ids = pf_ids_of_hyps g in + let k = next_global_ident_away true k_id ids in + let p = next_global_ident_away true p_id (k::ids) in + let v = next_global_ident_away true v_id (p::k::ids) in + let heq = next_global_ident_away true heq_id (v::p::k::ids) in + let heq1 = next_global_ident_away true heq_id (heq::v::p::k::ids) in + let hex = next_global_ident_away true hex_id (heq1::heq::v::p::k::ids) in + tclTHENLIST [ + h_intros [v; hex]; + simplest_elim (mkVar hex); + h_intros [p;heq1]; + tclTRY + (rewriteRL + (mkApp(mkVar heq1, + [|mkApp (delayed_force coq_S, [|mkVar p|]); + mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|]))); + simpl_iter onConcl; + tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]); + list_rewrite true eqs; + apply (delayed_force refl_equal)] g;; + +let f_S t = mkApp(delayed_force coq_S, [|t|]);; + + +let rec introduce_all_values_eq cont_tac functional termine + f p heq1 pmax bounds le_proofs eqs ids = + function + [] -> + let heq2 = next_global_ident_away true heq_id ids in + tclTHENLIST + [forward None (IntroIdentifier heq2) + (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); + simpl_iter (onHyp heq2); + unfold_in_hyp [([1], evaluable_of_global_reference + (global_of_constr functional))] + (([], heq2), Tacexpr.InHyp); + tclTHENS + (fun gls -> + let t_eq = compute_renamed_type gls (mkVar heq2) in + let def_id = + let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in + Nameops.out_name def_na + in + observe_tac "rewrite heq" (general_rewrite_bindings false [] + (mkVar heq2, + ExplicitBindings[dummy_loc,NamedHyp def_id, + f]) false) gls) + [tclTHENLIST + [observe_tac "list_rewrite" (list_rewrite true eqs); + cont_tac pmax le_proofs]; + tclTHENLIST[apply (delayed_force le_lt_SS); + compute_le_proofs le_proofs]]] + | arg::args -> + let v' = next_global_ident_away true v_id ids in + let ids = v'::ids in + let hex' = next_global_ident_away true hex_id ids in + let ids = hex'::ids in + let p' = next_global_ident_away true p_id ids in + let ids = p'::ids in + let new_pmax = next_global_ident_away true pmax_id ids in + let ids = pmax::ids in + let hle1 = next_global_ident_away true hle_id ids in + let ids = hle1::ids in + let hle2 = next_global_ident_away true hle_id ids in + let ids = hle2::ids in + let heq = next_global_ident_away true heq_id ids in + let ids = heq::ids in + let heq2 = next_global_ident_away true heq_id ids in + let ids = heq2::ids in + tclTHENLIST + [mkCaseEq(mkApp(termine, Array.of_list arg)); + h_intros [v'; hex']; + simplest_elim(mkVar hex'); + h_intros [p']; + simplest_elim(mkApp(delayed_force max_constr, [|mkVar pmax; + mkVar p'|])); + h_intros [new_pmax;hle1;hle2]; + introduce_all_values_eq + (fun pmax' le_proofs'-> + tclTHENLIST + [cont_tac pmax' le_proofs'; + h_intros [heq;heq2]; + observe_tac ("rewriteRL " ^ (string_of_id heq2)) + (tclTRY (rewriteLR (mkVar heq2))); + tclTRY (tclTHENS + ( fun g -> + let t_eq = compute_renamed_type g (mkVar heq) in + let k_id,def_id = + let k_na,_,t = destProd t_eq in + let _,_,t = destProd t in + let def_na,_,_ = destProd t in + Nameops.out_name k_na,Nameops.out_name def_na + in + let c_b = (mkVar heq, + ExplicitBindings + [dummy_loc, NamedHyp k_id, + f_S(mkVar pmax'); + dummy_loc, NamedHyp def_id, f]) + in + observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false [] + c_b false)) + g + ) + [tclIDTAC; + tclTHENLIST + [apply (delayed_force le_lt_n_Sm); + compute_le_proofs le_proofs']])]) + functional termine f p heq1 new_pmax + (p'::bounds)((mkVar pmax)::le_proofs) eqs + (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args] + + +let rec_leaf_eq termine f ids functional eqs expr fn args = + let p = next_global_ident_away true p_id ids in + let ids = p::ids in + let v = next_global_ident_away true v_id ids in + let ids = v::ids in + let hex = next_global_ident_away true hex_id ids in + let ids = hex::ids in + let heq1 = next_global_ident_away true heq_id ids in + let ids = heq1::ids in + let hle1 = next_global_ident_away true hle_id ids in + let ids = hle1::ids in + tclTHENLIST + [observe_tac "intros v hex" (h_intros [v;hex]); + simplest_elim (mkVar hex); + h_intros [p;heq1]; + h_generalize [mkApp(delayed_force le_n,[|mkVar p|])]; + h_intros [hle1]; + observe_tac "introduce_all_values_eq" (introduce_all_values_eq + (fun _ _ -> tclIDTAC) + functional termine f p heq1 p [] [] eqs ids args); + observe_tac "failing here" (apply (delayed_force refl_equal))] + +let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) + (eqs:constr list) (expr:constr) = +(* tclTRY *) + (match kind_of_term expr with + Case(ci,t,a,l) -> + (match find_call_occs 0 f a with + _,[] -> + (fun g -> + let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in + tclTHENS + destruct_tac + (list_map_i + (fun i -> mk_intros_and_continue + (List.rev rev_to_thin_intro) true + (prove_eq termine f functional) + eqs ci.ci_cstr_nargs.(i)) + 0 (Array.to_list l)) g) + | _,_::_ -> + (match find_call_occs 0 f expr with + _,[] -> base_leaf_eq functional eqs f + | fn,args -> + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + rec_leaf_eq termine f ids + (constr_of_global functional) + eqs expr fn args g)) + | _ -> + (match find_call_occs 0 f expr with + _,[] -> base_leaf_eq functional eqs f + | fn,args -> + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + observe_tac "rec_leaf_eq" (rec_leaf_eq + termine f ids (constr_of_global functional) + eqs expr fn args) g));; + +let (com_eqn : identifier -> + global_reference -> global_reference -> global_reference + -> constr -> unit) = + fun eq_name functional_ref f_ref terminate_ref equation_lemma_type -> + let opacity = + match terminate_ref with + | ConstRef c -> + let cb = Global.lookup_constant c in + if cb.Declarations.const_opaque then true + else begin match cb.const_body with None -> true | _ -> false end + | _ -> anomaly "terminate_lemma: not a constant" + in + let (evmap, env) = Command.get_current_context() in + let f_constr = (constr_of_global f_ref) in + let equation_lemma_type = subst1 f_constr equation_lemma_type in + (start_proof eq_name (Global, Proof Lemma) + (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); + by + (start_equation f_ref terminate_ref + (fun x -> + prove_eq + (constr_of_global terminate_ref) + f_constr + functional_ref + [] + (instantiate_lambda + (def_of_const (constr_of_global functional_ref)) + (f_constr::List.map mkVar x) + ) + ) + ); +(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) +(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) + Flags.silently (fun () ->Command.save_named opacity) () ; +(* Pp.msgnl (str "eqn finished"); *) + + );; + +let nf_zeta env = + Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + env + Evd.empty + +let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq + generate_induction_principle using_lemmas : unit = + let function_type = interp_constr Evd.empty (Global.env()) type_of_f in + let env = push_named (function_name,None,function_type) (Global.env()) in +(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) + let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in +(* Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *) + let res_vars,eq' = decompose_prod equation_lemma_type in + let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in + let eq' = nf_zeta env_eq' eq' in + let res = +(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) +(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) +(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) + match kind_of_term eq' with + | App(e,[|_;_;eq_fix|]) -> + mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) + | _ -> failwith "Recursive Definition (res not eq)" + in + let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in + let (_, rec_arg_type, _) = destProd function_type_before_rec_arg in + let arg_types = List.rev_map snd (fst (decompose_prod_n (List.length res_vars) function_type)) in + let equation_id = add_suffix function_name "_equation" in + let functional_id = add_suffix function_name "_F" in + let term_id = add_suffix function_name "_terminate" in + let functional_ref = declare_fun functional_id (IsDefinition Definition) res in + let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in + let relation = + interp_constr + Evd.empty + env_with_pre_rec_args + r + in + let tcc_lemma_name = add_suffix function_name "_tcc" in + let tcc_lemma_constr = ref None in +(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) + let hook _ _ = + let term_ref = Nametab.locate (make_short_qualid term_id) in + let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in +(* message "start second proof"; *) + let stop = ref false in + begin + try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) + with e -> + begin + if Tacinterp.get_debug () <> Tactic_debug.DebugOff + then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e) + else anomaly "Cannot create equation Lemma" + ; +(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) + stop := true; + end + end; + if not !stop + then + let eq_ref = Nametab.locate (make_short_qualid equation_id ) in + let f_ref = destConst (constr_of_global f_ref) + and functional_ref = destConst (constr_of_global functional_ref) + and eq_ref = destConst (constr_of_global eq_ref) in + generate_induction_principle f_ref tcc_lemma_constr + functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; + if Flags.is_verbose () + then msgnl (h 1 (Ppconstr.pr_id function_name ++ + spc () ++ str"is defined" )++ fnl () ++ + h 1 (Ppconstr.pr_id equation_id ++ + spc () ++ str"is defined" ) + ) + in + try + com_terminate + tcc_lemma_name + tcc_lemma_constr + is_mes functional_ref + rec_arg_type + relation rec_arg_num + term_id + using_lemmas + (List.length res_vars) + hook + with e -> + begin + ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); +(* anomaly "Cannot create termination Lemma" *) + raise e + end + + + diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 deleted file mode 100644 index 4dc4f1fd3f..0000000000 --- a/contrib/funind/tacinv.ml4 +++ /dev/null @@ -1,869 +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 *) - -(*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 global_reference 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: *** -*) - - diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml deleted file mode 100644 index ce775e0bee..0000000000 --- a/contrib/funind/tacinvutils.ml +++ /dev/null @@ -1,284 +0,0 @@ -(* tacinvutils.ml *) -(*s utilities *) - -(*i*) -open Names -open Util -open Term -open Termops -open Coqlib -open Pp -open Printer -open Inductiveops -open Environ -open Declarations -open Nameops -open Evd -open Sign -open Reductionops -(*i*) - -(*s printing of constr -- debugging *) - -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" - (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ pr_lconstr c ++ str"\n") -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) - -let prchr () = msg (str" (ret) \n") -let prNamedConstr s c = - begin - msg(str ""); - msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n"); - msg(str ""); - end - -let prNamedLConstr_aux lc = - List.iter (prNamedConstr "#>") lc - -let prNamedLConstr s lc = - begin - prstr s; - prNamedLConstr_aux lc - end - - -(* FIXME: ref 1, pas bon, si? *) -let evarcpt = ref 0 -let metacpt = ref 0 -let mknewexist ()= - begin - evarcpt := !evarcpt+1; - !evarcpt,[||] - end - -let resetexist ()= evarcpt := 0 - -let mknewmeta ()= - begin - metacpt := !metacpt+1; - mkMeta (!metacpt) - end - -let resetmeta () = metacpt := 0 - -let rec mkevarmap_from_listex lex = - match lex with - | [] -> Evd.empty - | ((ex,_),typ)::lex' -> -(* let _ = prstr "mkevarmap" in - let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in - let _ = prstr "OF TYPE: " in - let _ = prconstr typ in*) - let info = { - evar_concl = typ; - evar_hyps = empty_named_context_val; - evar_body = Evar_empty; - evar_extra = None} in - Evd.add (mkevarmap_from_listex lex') ex info - -let mkEq typ c1 c2 = - mkApp (build_coq_eq(),[| typ; c1; c2|]) - -let mkRefl typ c1 = - mkApp ((build_coq_eq_data()).refl, [| typ; c1|]) - -let rec popn i c = if i<=0 then c else pop (popn (i-1) c) - - -(* Operations on names *) -let id_of_name = function - Anonymous -> id_of_string "H" - | Name id -> id;; -let string_of_name nme = string_of_id (id_of_name nme) -let name_of_string str = Name (id_of_string str) -let newname_append nme str = - Name(id_of_string ((string_of_id (id_of_name nme))^str)) - -(* Substitutions in constr *) - -let compare_constr_nosub t1 t2 = - if compare_constr (fun _ _ -> false) t1 t2 - then true - else false - -let rec compare_constr' t1 t2 = - if compare_constr_nosub t1 t2 - then true - else (compare_constr (compare_constr') t1 t2) - -let rec substitterm prof t by_t in_u = - if (compare_constr' (lift prof t) in_u) - then (lift prof by_t) - else map_constr_with_binders succ - (fun i -> substitterm i t by_t) prof in_u - - -let apply_eqtrpl eq t = - let r,(tb,b,by_t) = eq in - substitterm 0 b by_t t - -let apply_eqtrpl_lt lt eq = List.map (apply_eqtrpl eq) lt - -let apply_leqtrpl_t t leq = - List.fold_left (fun x y -> apply_eqtrpl y x) t leq - - -let apply_refl_term eq t = - let _,arr = destApp eq in - let reli= (Array.get arr 1) in - let by_t= (Array.get arr 2) in - substitterm 0 reli by_t t - -let apply_eq_leqtrpl leq eq = - List.map - (function (r,(tb,b,t)) -> - r,(tb, - (if isRel b then b else (apply_refl_term eq b)), apply_refl_term eq t)) - leq - - - -(* [(a b c) a] -> true *) -let constr_head_match u t= - if isApp u - then - let uhd,args= destApp u in - uhd=t - else false - -(* My operations on constr *) -let lift1L l = (List.map (lift 1) l) -let mkArrow_lift t1 t2 = mkArrow t1 (lift 1 t2) -let mkProd_liftc nme c1 c2 = mkProd (nme,c1,(lift 1 c2)) -(* prod_it_lift x [a1 a2 ...] *) -let prod_it_lift ini lcpl = - List.fold_right (function a,b -> (fun c -> mkProd_liftc a b c)) ini lcpl;; - -let prod_it_anonym_lift trm lst = List.fold_right mkArrow_lift lst trm - -let lam_it_anonymous trm lst = - List.fold_right - (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm - -let lambda_id id typeofid cstr = - let cstr' = mkNamedLambda (id_of_string "FUNX") typeofid cstr in - substitterm 0 id (mkRel 0) cstr' - -let prod_id id typeofid cstr = - let cstr' = mkNamedProd (id_of_string "FUNX") typeofid cstr in - substitterm 0 id (mkRel 0) cstr' - - - - - -let nth_dep_constructor indtype n = - let sigma = Evd.empty and env = Global.env() in - let indtypedef = find_rectype env sigma indtype in - let indfam,_ = dest_ind_type indtypedef in - let arr_cstr_summary = get_constructors env indfam in - let cstr_sum = Array.get arr_cstr_summary n in - build_dependent_constructor cstr_sum, cstr_sum.cs_nargs - - -let rec buildrefl_from_eqs eqs = - match eqs with - | [] -> [] - | cstr::eqs' -> - let eq,args = destApp cstr in - (mkRefl (Array.get args 0) (Array.get args 2)) - :: (buildrefl_from_eqs eqs') - - - - -(* list of occurrences of a term inside another *) -(* Cofix will be wrong, not sure Fix is correct too *) -let rec hdMatchSub u t= - let subres = - match kind_of_term u with - | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t - | Fix (_,(lna,tl,bl)) -> - Array.fold_left - (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) - [] bl - | LetIn _ -> assert false - (* Correct? *) - | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u - in - if constr_head_match u t then u :: subres else subres - - -(* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *) -let hdMatchSub_cpl u (d,f) = - let res = ref [] in - begin - for i = d to f do res := hdMatchSub u (mkRel i) @ !res done; - !res - end - - -(* destApplication raises an exception if [t] is not an application *) -let exchange_hd_prod subst_hd t = - let hd,args= destApplication t in mkApp (subst_hd,args) - -(* 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 - let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in - x - else - map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u - -(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each - reli by tarr.(f-i). *) -let exchange_reli_arrayi tarr (d,f) t = - let hd,args= destApp t in - let i = destRel hd in - let res = whd_beta (mkApp (tarr.(f-i) ,args)) in - res - -let exchange_reli_arrayi_L tarr (d,f) = - List.map (exchange_reli_arrayi tarr (d,f)) - - -(* expand all letins in a term, before building the principle. *) -let rec expand_letins mimick = - match kind_of_term mimick with - | LetIn(nme,cstr1, typ, cstr) -> - let cstr' = substitterm 0 (mkRel 1) (lift 1 cstr1) cstr in - expand_letins (pop cstr') - | x -> map_constr expand_letins mimick - - -(* Valeur d'une constante, or identity *) -let def_of_const t = - match kind_of_term t with - | Const sp -> - (try - match Global.lookup_constant sp with - {const_body=Some c} -> force c - |_ -> assert false - with _ -> assert false) - | _ -> t - -(* nom d'une constante. Must be a constante. x*) -let name_of_const t = - match (kind_of_term t) with - Const cst -> Names.string_of_label (Names.con_label cst) - |_ -> assert false - ;; - - -(*i -*** 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 deleted file mode 100644 index 64b212130a..0000000000 --- a/contrib/funind/tacinvutils.mli +++ /dev/null @@ -1,80 +0,0 @@ -(* tacinvutils.ml *) -(*s utilities *) - -(*i*) -open Termops -open Equality -open Names -open Pp -open Tacmach -open Proof_type -open Tacinterp -open Tactics -open Tacticals -open Term -open Util -open Printer -open Reductionops -open Inductiveops -open Coqlib -open Refine -open Evd -(*i*) - -(* printing 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 - - -val mknewmeta: unit -> constr -val mknewexist: unit -> existential -val resetmeta: unit -> unit (* safe *) -val resetexist: unit -> unit (* be careful with this one *) -val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map -val mkEq: types -> constr -> constr -> constr -(* let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *) -val mkRefl: types -> constr -> constr -val buildrefl_from_eqs: constr list -> constr list -(* typ c1 = mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *) - -val nth_dep_constructor: constr -> int -> (constr*int) - -val prod_it_lift: (name*constr) list -> constr -> constr -val prod_it_anonym_lift: constr -> constr list -> constr -val lam_it_anonymous: constr -> constr list -> constr -val lift1L: (constr list) -> constr list -val popn: int -> constr -> constr -val lambda_id: constr -> constr -> constr -> constr -val prod_id: constr -> constr -> constr -> constr - - -val name_of_string : string -> name -val newname_append: name -> string -> name - -val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr -val substitterm: int -> constr -> constr -> constr -> constr -val apply_leqtrpl_t: - constr -> (constr*(constr*constr*constr)) list -> constr -val apply_eq_leqtrpl: - (constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list -(* val apply_leq_lt: constr list -> constr list -> constr list *) - -val hdMatchSub: constr -> constr -> constr list -val hdMatchSub_cpl: constr -> int*int -> constr list -val exchange_hd_prod: constr -> constr -> constr -val exchange_reli_arrayi_L: constr array -> int*int -> constr list -> constr list -val substit_red: int -> constr -> constr -> constr -> constr -val expand_letins: constr -> constr - -val def_of_const: constr -> constr -val name_of_const: constr -> string - -(*i - *** Local Variables: *** - *** compile-command: "make -C ../.. contrib/funind/tacinvutils.cmi" *** - *** End: *** -i*) - diff --git a/contrib/recdef/Recdef.v b/contrib/recdef/Recdef.v deleted file mode 100644 index 2d206220e4..0000000000 --- a/contrib/recdef/Recdef.v +++ /dev/null @@ -1,48 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A) -> A -> A := - fun (fl : A -> A) (def : A) => - match n with - | O => def - | S m => fl (iter m fl def) - end. -End Iter. - -Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')). - intro p; intro p'; change (S p <= S (S (p + p'))); - apply le_S; apply Gt.gt_le_S; change (p < S (p + p')); - apply Lt.le_lt_n_Sm; apply Plus.le_plus_l. -Qed. - - -Theorem Splus_lt : forall p p' : nat, p' < S (p + p'). - intro p; intro p'; change (S p' <= S (p + p')); - apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm; - apply Plus.le_plus_r. -Qed. - -Theorem le_lt_SS : forall x y, x <= y -> x < S (S y). -intro x; intro y; intro H; change (S x <= S (S y)); - apply le_S; apply Gt.gt_le_S; change (x < S y); - apply Lt.le_lt_n_Sm; exact H. -Qed. - -Inductive max_type (m n:nat) : Set := - cmt : forall v, m <= v -> n <= v -> max_type m n. - -Definition max : forall m n:nat, max_type m n. -intros m n; case (Compare_dec.le_gt_dec m n). -intros h; exists n; [exact h | apply le_n]. -intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h]. -Defined. diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 deleted file mode 100644 index 7d4eb72a97..0000000000 --- a/contrib/recdef/recdef.ml4 +++ /dev/null @@ -1,1448 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* next_global_ident_away false id (acc@ids)::acc) - idl - [] - -let pf_get_new_id id g = - List.hd (pf_get_new_ids [id] g) - -let h_intros l = - tclMAP h_intro l - -let do_observe_tac s tac g = - let goal = begin (Printer.pr_goal (sig_it g)) end in - try let v = tac g in msgnl (goal ++ fnl () ++ (str "recdef ") ++ - (str s)++(str " ")++(str "finished")); v - with e -> - msgnl (str "observation "++str s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); - raise e;; - - -let observe_tac s tac g = - if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then do_observe_tac s tac g - else tac g - -let hyp_ids = List.map id_of_string - ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res"; - "hspec";"heq"; "hrec"; "hex"; "teq"; "pmax";"hle"];; - -let rec nthtl = function - l, 0 -> l | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];; - -let hyp_id n l = List.nth l n;; - -let (x_id:identifier) = hyp_id 0 hyp_ids;; -let (v_id:identifier) = hyp_id 1 hyp_ids;; -let (k_id:identifier) = hyp_id 2 hyp_ids;; -let (def_id:identifier) = hyp_id 3 hyp_ids;; -let (p_id:identifier) = hyp_id 4 hyp_ids;; -let (h_id:identifier) = hyp_id 5 hyp_ids;; -let (n_id:identifier) = hyp_id 6 hyp_ids;; -let (h'_id:identifier) = hyp_id 7 hyp_ids;; -let (ano_id:identifier) = hyp_id 8 hyp_ids;; -let (rec_res_id:identifier) = hyp_id 10 hyp_ids;; -let (hspec_id:identifier) = hyp_id 11 hyp_ids;; -let (heq_id:identifier) = hyp_id 12 hyp_ids;; -let (hrec_id:identifier) = hyp_id 13 hyp_ids;; -let (hex_id:identifier) = hyp_id 14 hyp_ids;; -let (teq_id:identifier) = hyp_id 15 hyp_ids;; -let (pmax_id:identifier) = hyp_id 16 hyp_ids;; -let (hle_id:identifier) = hyp_id 17 hyp_ids;; - -let message s = if Flags.is_verbose () then msgnl(str s);; - -let def_of_const t = - match (kind_of_term t) with - Const sp -> - (try (match (Global.lookup_constant sp) with - {const_body=Some c} -> Declarations.force c - |_ -> assert false) - with _ -> - anomaly ("Cannot find definition of constant "^ - (string_of_id (id_of_label (con_label sp)))) - ) - |_ -> assert false - -let type_of_const t = - match (kind_of_term t) with - Const sp -> Typeops.type_of_constant (Global.env()) sp - |_ -> assert false - -let arg_type t = - match kind_of_term (def_of_const t) with - Lambda(a,b,c) -> b - | _ -> assert false;; - -let evaluable_of_global_reference r = - match r with - ConstRef sp -> EvalConstRef sp - | VarRef id -> EvalVarRef id - | _ -> assert false;; - - -let rank_for_arg_list h = - let predicate a b = - try List.for_all2 eq_constr a b with - Invalid_argument _ -> false in - let rec rank_aux i = function - | [] -> None - | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in - rank_aux 0;; - -let rec (find_call_occs : int -> constr -> constr -> - (constr list -> constr) * constr list list) = - fun nb_lam f expr -> - match (kind_of_term expr) with - App (g, args) when g = f -> - (fun l -> List.hd l), [Array.to_list args] - | App (g, args) -> - let (largs: constr list) = Array.to_list args in - let rec find_aux = function - [] -> (fun x -> []), [] - | a::upper_tl -> - (match find_aux upper_tl with - (cf, ((arg1::args) as args_for_upper_tl)) -> - (match find_call_occs nb_lam f a with - cf2, (_ :: _ as other_args) -> - let rec avoid_duplicates args = - match args with - | [] -> (fun _ -> []), [] - | h::tl -> - let recomb_tl, args_for_tl = - avoid_duplicates tl in - match rank_for_arg_list h args_for_upper_tl with - | None -> - (fun l -> List.hd l::recomb_tl(List.tl l)), - h::args_for_tl - | Some i -> - (fun l -> List.nth l (i+List.length args_for_tl):: - recomb_tl l), - args_for_tl - in - let recombine, other_args' = - avoid_duplicates other_args in - let len1 = List.length other_args' in - (fun l -> cf2 (recombine l)::cf(nthtl(l,len1))), - other_args'@args_for_upper_tl - | _, [] -> (fun x -> a::cf x), args_for_upper_tl) - | _, [] -> - (match find_call_occs nb_lam f a with - cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args) - | _, [] -> (fun x -> a::upper_tl), [])) in - begin - match (find_aux largs) with - cf, [] -> (fun l -> mkApp(g, args)), [] - | cf, args -> - (fun l -> mkApp (g, Array.of_list (cf l))), args - end - | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[]) - | Var(id) -> (fun l -> expr), [] - | Meta(_) -> error "find_call_occs : Meta" - | Evar(_) -> error "find_call_occs : Evar" - | Sort(_) -> (fun l -> expr), [] - | Cast(b,_,_) -> find_call_occs nb_lam f b - | Prod(_,_,_) -> error "find_call_occs : Prod" - | Lambda(na,t,b) -> - begin - match find_call_occs (succ nb_lam) f b with - | _, [] -> (* Lambda are authorized as long as they do not contain - recursives calls *) - (fun l -> expr),[] - | _ -> error "find_call_occs : Lambda" - end - | LetIn(na,v,t,b) -> - begin - match find_call_occs nb_lam f v, find_call_occs (succ nb_lam) f b with - | (_,[]),(_,[]) -> - ((fun l -> expr), []) - | (_,[]),(cf,(_::_ as l)) -> - ((fun l -> mkLetIn(na,v,t,cf l)),l) - | (cf,(_::_ as l)),(_,[]) -> - ((fun l -> mkLetIn(na,cf l,t,b)), l) - | _ -> error "find_call_occs : LetIn" - end - | Const(_) -> (fun l -> expr), [] - | Ind(_) -> (fun l -> expr), [] - | Construct (_, _) -> (fun l -> expr), [] - | Case(i,t,a,r) -> - (match find_call_occs nb_lam f a with - cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args) - | _ -> (fun l -> expr),[]) - | Fix(_) -> error "find_call_occs : Fix" - | CoFix(_) -> error "find_call_occs : CoFix";; - -let coq_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" - (Coqlib.init_modules @ Coqlib.arith_modules) s;; - -let constant sl s = - constr_of_global - (locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; - -let find_reference sl s = - (locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; - -let delayed_force f = f () - -let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") -let le_lt_n_Sm = function () -> (coq_constant "le_lt_n_Sm") - -let le_trans = function () -> (coq_constant "le_trans") -let le_lt_trans = function () -> (coq_constant "le_lt_trans") -let lt_S_n = function () -> (coq_constant "lt_S_n") -let le_n = function () -> (coq_constant "le_n") -let refl_equal = function () -> (coq_constant "refl_equal") -let eq = function () -> (coq_constant "eq") -let ex = function () -> (coq_constant "ex") -let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") -let coq_sig = function () -> (coq_constant "sig") -let coq_O = function () -> (coq_constant "O") -let coq_S = function () -> (coq_constant "S") - -let gt_antirefl = function () -> (coq_constant "gt_irrefl") -let lt_n_O = function () -> (coq_constant "lt_n_O") -let lt_n_Sn = function () -> (coq_constant "lt_n_Sn") - -let f_equal = function () -> (coq_constant "f_equal") -let well_founded_induction = function () -> (coq_constant "well_founded_induction") -let well_founded = function () -> (coq_constant "well_founded") -let acc_rel = function () -> (coq_constant "Acc") -let acc_inv_id = function () -> (coq_constant "Acc_inv") -let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof") -let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded") -let max_ref = function () -> (find_reference ["Recdef"] "max") -let iter = function () -> (constr_of_global (delayed_force iter_ref)) -let max_constr = function () -> (constr_of_global (delayed_force max_ref)) - -let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") -let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" - -(* These are specific to experiments in nat with lt as well_founded_relation, *) -(* but this should be made more general. *) -let nat = function () -> (coq_constant "nat") -let lt = function () -> (coq_constant "lt") - -(* This is simply an implementation of the case_eq tactic. this code - should be replaced with the tactic defined in Ltac in Init/Tactics.v *) -let mkCaseEq a : tactic = - (fun g -> - let type_of_a = pf_type_of g a in - tclTHENLIST - [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; - (fun g2 -> - change_in_concl None - (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2)) - g2); - simplest_case a] g);; - -(* This is like the previous one except that it also rewrite on all - hypotheses except the ones given in the first argument. All the - modified hypotheses are generalized in the process and should be - introduced back later; the result is the pair of the tactic and the - list of hypotheses that have been generalized and cleared. *) -let mkDestructEq : - identifier list -> constr -> goal sigma -> tactic * identifier list = - fun not_on_hyp expr g -> - let hyps = pf_hyps g in - let to_revert = - Util.map_succeed - (fun (id,_,t) -> - if List.mem id not_on_hyp || not (Termops.occur_term expr t) - then failwith "is_expr_context"; - id) hyps in - let to_revert_constr = List.rev_map mkVar to_revert in - let type_of_expr = pf_type_of g expr in - let new_hyps = mkApp(delayed_force refl_equal, [|type_of_expr; expr|]):: - to_revert_constr in - tclTHENLIST - [h_generalize new_hyps; - (fun g2 -> - change_in_concl None - (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); - simplest_case expr], to_revert - -let rec mk_intros_and_continue thin_intros (extra_eqn:bool) - cont_function (eqs:constr list) nb_lam (expr:constr) g = - let finalize () = if extra_eqn then - let teq = pf_get_new_id teq_id g in - tclTHENLIST - [ h_intro teq; - thin thin_intros; - h_intros thin_intros; - - tclMAP - (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false)) - (List.rev eqs); - (fun g1 -> - let ty_teq = pf_type_of g1 (mkVar teq) in - let teq_lhs,teq_rhs = - let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in - args.(1),args.(2) - in - cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1 - ) - ] - g - else - tclTHENSEQ[ - thin thin_intros; - h_intros thin_intros; - cont_function eqs expr - ] g - in - if nb_lam = 0 - then finalize () - else - match kind_of_term expr with - | Lambda (n, _, b) -> - let n1 = - match n with - Name x -> x - | Anonymous -> ano_id - in - let new_n = pf_get_new_id n1 g in - tclTHEN (h_intro new_n) - (mk_intros_and_continue thin_intros extra_eqn cont_function eqs - (pred nb_lam) (subst1 (mkVar new_n) b)) g - | _ -> - assert false -(* finalize () *) -let const_of_ref = function - ConstRef kn -> kn - | _ -> anomaly "ConstRef expected" - -let simpl_iter clause = - reduce - (Lazy - {rBeta=true;rIota=true;rZeta= true; rDelta=false; - rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]}) -(* (Simpl (Some ([],mkConst (const_of_ref (delayed_force iter_ref))))) *) - clause - -(* The boolean value is_mes expresses that the termination is expressed - using a measure function instead of a well-founded relation. *) -let tclUSER tac is_mes l g = - let clear_tac = - match l with - | None -> h_clear true [] - | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l) - in - tclTHENSEQ - [ - clear_tac; - if is_mes - then tclTHEN - (unfold_in_concl [([], evaluable_of_global_reference - (delayed_force ltof_ref))]) - tac - else tac - ] - g - - -let list_rewrite (rev:bool) (eqs: constr list) = - tclREPEAT - (List.fold_right - (fun eq i -> tclORELSE (rewriteLR eq) i) - (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; - -let base_leaf_terminate (func:global_reference) eqs expr = -(* let _ = msgnl (str "entering base_leaf") in *) - (fun g -> - let k',h = - match pf_get_new_ids [k_id;h_id] g with - [k';h] -> k',h - | _ -> assert false - in - tclTHENLIST - [observe_tac "first split" (split (ImplicitBindings [expr])); - observe_tac "second split" - (split (ImplicitBindings [delayed_force coq_O])); - observe_tac "intro k" (h_intro k'); - observe_tac "case on k" - (tclTHENS (simplest_case (mkVar k')) - [(tclTHEN (h_intro h) - (tclTHEN (simplest_elim (mkApp (delayed_force gt_antirefl, - [| delayed_force coq_O |]))) - default_auto)); tclIDTAC ]); - intros; - simpl_iter onConcl; - unfold_constr func; - list_rewrite true eqs; - default_auto] g);; - -(* La fonction est donnee en premier argument a la - fonctionnelle suivie d'autres Lambdas et de Case ... - Pour recuperer la fonction f a partir de la - fonctionnelle *) - -let get_f foncl = - match (kind_of_term (def_of_const foncl)) with - Lambda (Name f, _, _) -> f - |_ -> error "la fonctionnelle est mal definie";; - - -let rec compute_le_proofs = function - [] -> assumption - | a::tl -> - tclORELSE assumption - (tclTHENS - (fun g -> - let le_trans = delayed_force le_trans in - let t_le_trans = compute_renamed_type g le_trans in - let m_id = - let _,_,t = destProd t_le_trans in - let na,_,_ = destProd t in - Nameops.out_name na - in - apply_with_bindings - (le_trans, - ExplicitBindings[dummy_loc,NamedHyp m_id,a]) - g) - [compute_le_proofs tl; - tclORELSE (apply (delayed_force le_n)) assumption]) - -let make_lt_proof pmax le_proof = - tclTHENS - (fun g -> - let le_lt_trans = delayed_force le_lt_trans in - let t_le_lt_trans = compute_renamed_type g le_lt_trans in - let m_id = - let _,_,t = destProd t_le_lt_trans in - let na,_,_ = destProd t in - Nameops.out_name na - in - apply_with_bindings - (le_lt_trans, - ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g) - [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); - tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];; - -let rec list_cond_rewrite k def pmax cond_eqs le_proofs = - match cond_eqs with - [] -> tclIDTAC - | eq::eqs -> - (fun g -> - let t_eq = compute_renamed_type g (mkVar eq) in - let k_id,def_id = - let k_na,_,t = destProd t_eq in - let _,_,t = destProd t in - let def_na,_,_ = destProd t in - Nameops.out_name k_na,Nameops.out_name def_na - in - tclTHENS - (general_rewrite_bindings false [] - (mkVar eq, - ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; - dummy_loc, NamedHyp def_id, mkVar def]) false) - [list_cond_rewrite k def pmax eqs le_proofs; - observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g - ) - -let rec introduce_all_equalities func eqs values specs bound le_proofs - cond_eqs = - match specs with - [] -> - fun g -> - let ids = pf_ids_of_hyps g in - let s_max = mkApp(delayed_force coq_S, [|bound|]) in - let k = next_global_ident_away true k_id ids in - let ids = k::ids in - let h' = next_global_ident_away true (h'_id) ids in - let ids = h'::ids in - let def = next_global_ident_away true def_id ids in - tclTHENLIST - [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max])); - observe_tac "introduce_all_equalities_final intro k" (h_intro k); - tclTHENS - (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k))) - [ - tclTHENLIST[h_intro h'; - simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])); - default_full_auto]; - tclIDTAC - ]; - observe_tac "clearing k " (clear [k]); - observe_tac "intros k h' def" (h_intros [k;h';def]); - observe_tac "simple_iter" (simpl_iter onConcl); - observe_tac "unfold functional" - (unfold_in_concl[([1],evaluable_of_global_reference func)]); - observe_tac "rewriting equations" - (list_rewrite true eqs); - observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs); - observe_tac "refl equal" (apply (delayed_force refl_equal))] g - | spec1::specs -> - fun g -> - let ids = ids_of_named_context (pf_hyps g) in - let p = next_global_ident_away true p_id ids in - let ids = p::ids in - let pmax = next_global_ident_away true pmax_id ids in - let ids = pmax::ids in - let hle1 = next_global_ident_away true hle_id ids in - let ids = hle1::ids in - let hle2 = next_global_ident_away true hle_id ids in - let ids = hle2::ids in - let heq = next_global_ident_away true heq_id ids in - tclTHENLIST - [simplest_elim (mkVar spec1); - list_rewrite true eqs; - h_intros [p; heq]; - simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|])); - h_intros [pmax; hle1; hle2]; - introduce_all_equalities func eqs values specs - (mkVar pmax) ((mkVar pmax)::le_proofs) - (heq::cond_eqs)] g;; - -let string_match s = - if String.length s < 3 then failwith "string_match"; - try - for i = 0 to 3 do - if String.get s i <> String.get "Acc_" i then failwith "string_match" - done; - with Invalid_argument _ -> failwith "string_match" - -let retrieve_acc_var g = - (* Julien: I don't like this version .... *) - let hyps = pf_ids_of_hyps g in - map_succeed - (fun id -> string_match (string_of_id id);id) - hyps - -let rec introduce_all_values concl_tac is_mes acc_inv func context_fn - eqs hrec args values specs = - (match args with - [] -> - tclTHENLIST - [observe_tac "split" (split(ImplicitBindings - [context_fn (List.map mkVar (List.rev values))])); - observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs - (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])] - | arg::args -> - (fun g -> - let ids = ids_of_named_context (pf_hyps g) in - let rec_res = next_global_ident_away true rec_res_id ids in - let ids = rec_res::ids in - let hspec = next_global_ident_away true hspec_id ids in - let tac = - observe_tac "introduce_all_values" ( - introduce_all_values concl_tac is_mes acc_inv func context_fn eqs - hrec args - (rec_res::values)(hspec::specs)) in - (tclTHENS - (observe_tac "elim h_rec" - (simplest_elim (mkApp(mkVar hrec, Array.of_list arg))) - ) - [tclTHENLIST [h_intros [rec_res; hspec]; - tac]; - (tclTHENS - (observe_tac "acc_inv" (apply (Lazy.force acc_inv))) - [(* tclTHEN (tclTRY(list_rewrite true eqs)) *) - (observe_tac "h_assumption" h_assumption) - ; - tclTHENLIST - [ - tclTRY(list_rewrite true eqs); - observe_tac "user proof" - (fun g -> - tclUSER - concl_tac - is_mes - (Some (hrec::hspec::(retrieve_acc_var g)@specs)) - g - ) - ] - ] - ) - ]) g) - - ) - - -let rec_leaf_terminate concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = - match find_call_occs 0 (mkVar (get_f (constr_of_global func))) expr with - | context_fn, args -> - observe_tac "introduce_all_values" - (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] []) - -let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier) - (f_constr:constr) (func:global_reference) base_leaf rec_leaf = - let rec proveterminate (eqs:constr list) (expr:constr) = - try - (* let _ = msgnl (str "entering proveterminate") in *) - let v = - match (kind_of_term expr) with - Case (ci, t, a, l) -> - (match find_call_occs 0 f_constr a with - _,[] -> - (fun g -> - let destruct_tac, rev_to_thin_intro = - mkDestructEq rec_arg_id a g in - tclTHENS destruct_tac - (list_map_i - (fun i -> mk_intros_and_continue - (List.rev rev_to_thin_intro) - true - proveterminate - eqs - ci.ci_cstr_nargs.(i)) - 0 (Array.to_list l)) g) - | _, _::_ -> - (match find_call_occs 0 f_constr expr with - _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr) - | _, _:: _ -> - observe_tac "rec_leaf" - (rec_leaf is_mes acc_inv hrec func eqs expr))) - | _ -> - (match find_call_occs 0 f_constr expr with - _,[] -> - (try observe_tac "base_leaf" (base_leaf func eqs expr) - with e -> (msgerrnl (str "failure in base case");raise e )) - | _, _::_ -> - observe_tac "rec_leaf" - (rec_leaf is_mes acc_inv hrec func eqs expr)) in - v - with e -> begin msgerrnl(str "failure in proveterminate"); raise e end - in - proveterminate - -let hyp_terminates nb_args func = - let a_arrow_b = arg_type (constr_of_global func) in - let rev_args,b = decompose_prod_n nb_args a_arrow_b in - let left = - mkApp(delayed_force iter, - Array.of_list - (lift 5 a_arrow_b:: mkRel 3:: - constr_of_global func::mkRel 1:: - List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args) - ) - ) - in - let right = mkRel 5 in - let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in - let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in - let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in - let nb_iter = - mkApp(delayed_force ex, - [|delayed_force nat; - (mkLambda - (Name - p_id, - delayed_force nat, - (mkProd (Name k_id, delayed_force nat, - mkArrow cond result))))|])in - let value = mkApp(delayed_force coq_sig, - [|b; - (mkLambda (Name v_id, b, nb_iter))|]) in - compose_prod rev_args value - - - -let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = - if is_mes - then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof)) - else tclUSER concl_tac is_mes names_to_suppress - -let termination_proof_header is_mes input_type ids args_id relation - rec_arg_num rec_arg_id tac wf_tac : tactic = - begin - fun g -> - let nargs = List.length args_id in - let pre_rec_args = - List.rev_map - mkVar (fst (list_chop (rec_arg_num - 1) args_id)) - in - let relation = substl pre_rec_args relation in - let input_type = substl pre_rec_args input_type in - let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in - let wf_rec_arg = - next_global_ident_away true - (id_of_string ("Acc_"^(string_of_id rec_arg_id))) - (wf_thm::ids) - in - let hrec = next_global_ident_away true hrec_id - (wf_rec_arg::wf_thm::ids) in - let acc_inv = - lazy ( - mkApp ( - delayed_force acc_inv_id, - [|input_type;relation;mkVar rec_arg_id|] - ) - ) - in - tclTHEN - (h_intros args_id) - (tclTHENS - (observe_tac - "first assert" - (assert_tac - true (* the assert thm is in first subgoal *) - (Name wf_rec_arg) - (mkApp (delayed_force acc_rel, - [|input_type;relation;mkVar rec_arg_id|]) - ) - ) - ) - [ - (* accesibility proof *) - tclTHENS - (observe_tac - "second assert" - (assert_tac - true - (Name wf_thm) - (mkApp (delayed_force well_founded,[|input_type;relation|])) - ) - ) - [ - (* interactive proof that the relation is well_founded *) - observe_tac "wf_tac" (wf_tac is_mes (Some args_id)); - (* this gives the accessibility argument *) - observe_tac - "apply wf_thm" - (h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])) - ) - ] - ; - (* rest of the proof *) - tclTHENSEQ - [observe_tac "generalize" - (onNLastHyps (nargs+1) - (fun (id,_,_) -> - tclTHEN (h_generalize [mkVar id]) (h_clear false [id]) - )) - ; - observe_tac "h_fix" (h_fix (Some hrec) (nargs+1)); - h_intros args_id; - h_intro wf_rec_arg; - observe_tac "tac" (tac wf_rec_arg hrec acc_inv) - ] - ] - ) g - end - - - -let rec instantiate_lambda t l = - match l with - | [] -> t - | a::l -> - let (bound_name, _, body) = destLambda t in - instantiate_lambda (subst1 a body) l -;; - - -let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic = - begin - fun g -> - let ids = ids_of_named_context (pf_hyps g) in - let func_body = (def_of_const (constr_of_global func)) in - let (f_name, _, body1) = destLambda func_body in - let f_id = - match f_name with - | Name f_id -> next_global_ident_away true f_id ids - | Anonymous -> anomaly "Anonymous function" - in - let n_names_types,_ = decompose_lam_n nb_args body1 in - let n_ids,ids = - List.fold_left - (fun (n_ids,ids) (n_name,_) -> - match n_name with - | Name id -> - let n_id = next_global_ident_away true id ids in - n_id::n_ids,n_id::ids - | _ -> anomaly "anonymous argument" - ) - ([],(f_id::ids)) - n_names_types - in - let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in - let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in - termination_proof_header - is_mes - input_type - ids - n_ids - relation - rec_arg_num - rec_arg_id - (fun rec_arg_id hrec acc_inv g -> - (proveterminate - [rec_arg_id] - is_mes - acc_inv - hrec - (mkVar f_id) - func - base_leaf_terminate - (rec_leaf_terminate concl_tac) - [] - expr - ) - g - ) - (tclUSER_if_not_mes concl_tac) - g - end - -let get_current_subgoals_types () = - let pts = get_pftreestate () in - let _,subs = extract_open_pftreestate pts in - List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs ) - -let build_and_l l = - let and_constr = Coqlib.build_coq_and () in - let conj_constr = coq_conj () in - let mk_and p1 p2 = - Term.mkApp(and_constr,[|p1;p2|]) in - let rec f = function - | [] -> failwith "empty list of subgoals!" - | [p] -> p,tclIDTAC,1 - | p1::pl -> - let c,tac,nb = f pl in - mk_and p1 c, - tclTHENS - (apply (constr_of_global conj_constr)) - [tclIDTAC; - tac - ],nb+1 - in f l - - -let is_rec_res id = - let rec_res_name = string_of_id rec_res_id in - let id_name = string_of_id id in - try - String.sub id_name 0 (String.length rec_res_name) = rec_res_name - with _ -> false - -let clear_goals = - let rec clear_goal t = - match kind_of_term t with - | Prod(Name id as na,t,b) -> - let b' = clear_goal b in - if noccurn 1 b' && (is_rec_res id) - then pop b' - else if b' == b then t - else mkProd(na,t,b') - | _ -> map_constr clear_goal t - in - List.map clear_goal - - -let build_new_goal_type () = - let sub_gls_types = get_current_subgoals_types () in - let sub_gls_types = clear_goals sub_gls_types in - let res = build_and_l sub_gls_types in - res - - - (* -let prove_with_tcc lemma _ : tactic = - fun gls -> - let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in - tclTHENSEQ - [ - h_generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); - gen_eauto(* default_eauto *) false (false,5) [] (Some []) - (* default_auto *) - ] - gls - *) - - - -let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = - let current_proof_name = get_current_proof_name () in - let name = match goal_name with - | Some s -> s - | None -> - try (add_suffix current_proof_name "_subproof") - with _ -> anomaly "open_new_goal with an unamed theorem" - in - let sign = Global.named_context () in - let sign = clear_proofs sign in - let na = next_global_ident_away false name [] in - if occur_existential gls_type then - Util.error "\"abstract\" cannot handle existentials"; - let hook _ _ = - let opacity = - let na_ref = Libnames.Ident (dummy_loc,na) in - let na_global = Nametab.global na_ref in - match na_global with - ConstRef c -> - let cb = Global.lookup_constant c in - if cb.Declarations.const_opaque then true - else begin match cb.const_body with None -> true | _ -> false end - | _ -> anomaly "equation_lemma: not a constant" - in - let lemma = mkConst (Lib.make_con na) in - ref_ := Some lemma ; - let lid = ref [] in - let h_num = ref (-1) in - Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None); - build_proof - ( fun gls -> - let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in - tclTHENSEQ - [ - h_generalize [lemma]; - h_intro hid; - (fun g -> - let ids = pf_ids_of_hyps g in - tclTHEN - (Elim.h_decompose_and (mkVar hid)) - (fun g -> - let ids' = pf_ids_of_hyps g in - lid := List.rev (list_subtract ids' ids); - if !lid = [] then lid := [hid]; -(* list_iter_i *) -(* (fun i v -> *) -(* msgnl (str "hyp" ++ int i ++ str " " ++ *) -(* Nameops.pr_id v ++ fnl () ++ fnl())) *) -(* !lid; *) - tclIDTAC g - ) - g - ); - ] gls) - (fun g -> - match kind_of_term (pf_concl g) with - | App(f,_) when eq_constr f (well_founded ()) -> - Auto.h_auto None [] (Some []) g - | _ -> - incr h_num; - tclTHEN - (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) - e_assumption - g) -; - Command.save_named opacity; - in - start_proof - na - (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) - sign - gls_type - hook ; - by ( - fun g -> - tclTHEN - (decompose_and_tac) - (tclORELSE - (tclFIRST - (List.map - (fun c -> - tclTHENSEQ - [intros; - h_simplest_apply (interp_constr Evd.empty (Global.env()) c); - tclCOMPLETE Auto.default_auto - ] - ) - using_lemmas) - ) tclIDTAC) - g); - try - by tclIDTAC; (* raises UserError _ if the proof is complete *) - if Flags.is_verbose () then (pp (Printer.pr_open_subgoals())) - with UserError _ -> - defined () - -;; - - -let com_terminate - tcc_lemma_name - tcc_lemma_ref - is_mes - fonctional_ref - input_type - relation - rec_arg_num - thm_name using_lemmas - nb_args - hook = - let start_proof (tac_start:tactic) (tac_end:tactic) = - let (evmap, env) = Command.get_current_context() in - start_proof thm_name - (Global, Proof Lemma) (Environ.named_context_val env) - (hyp_terminates nb_args fonctional_ref) hook; - by (observe_tac "starting_tac" tac_start); - by (observe_tac "whole_start" (whole_start tac_end nb_args is_mes fonctional_ref - input_type relation rec_arg_num )) - - in - start_proof tclIDTAC tclIDTAC; - try - let new_goal_type = build_new_goal_type () in - open_new_goal start_proof using_lemmas tcc_lemma_ref - (Some tcc_lemma_name) - (new_goal_type) - with Failure "empty list of subgoals!" -> - (* a non recursive function declared with measure ! *) - defined () - - - - -let ind_of_ref = function - | IndRef (ind,i) -> (ind,i) - | _ -> anomaly "IndRef expected" - -let (value_f:constr list -> global_reference -> constr) = - fun al fterm -> - let d0 = dummy_loc in - let rev_x_id_l = - ( - List.fold_left - (fun x_id_l _ -> - let x_id = next_global_ident_away true x_id x_id_l in - x_id::x_id_l - ) - [] - al - ) - in - let fun_body = - RCases - (d0,RegularStyle,None, - [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l), - (Anonymous,None)], - [d0, [v_id], [PatCstr(d0,(ind_of_ref - (delayed_force coq_sig_ref),1), - [PatVar(d0, Name v_id); - PatVar(d0, Anonymous)], - Anonymous)], - RVar(d0,v_id)]) - in - let value = - List.fold_left2 - (fun acc x_id a -> - RLambda - (d0, Name x_id, Explicit, RDynamic(d0, constr_in a), - acc - ) - ) - fun_body - rev_x_id_l - (List.rev al) - in - understand Evd.empty (Global.env()) value;; - -let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = - fun f_id kind value -> - let ce = {const_entry_body = value; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true} in - ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; - -let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) = - fun f_id kind input_type fterm_ref -> - declare_fun f_id kind (value_f input_type fterm_ref);; - -let rec n_x_id ids n = - if n = 0 then [] - else let x = next_global_ident_away true x_id ids in - x::n_x_id (x::ids) (n-1);; - -let start_equation (f:global_reference) (term_f:global_reference) - (cont_tactic:identifier list -> tactic) g = - let ids = pf_ids_of_hyps g in - let terminate_constr = constr_of_global term_f in - let nargs = nb_prod (type_of_const terminate_constr) in - let x = n_x_id ids nargs in - tclTHENLIST [ - h_intros x; - unfold_in_concl [([], evaluable_of_global_reference f)]; - observe_tac "simplest_case" - (simplest_case (mkApp (terminate_constr, - Array.of_list (List.map mkVar x)))); - observe_tac "prove_eq" (cont_tactic x)] g;; - -let base_leaf_eq func eqs f_id g = - let ids = pf_ids_of_hyps g in - let k = next_global_ident_away true k_id ids in - let p = next_global_ident_away true p_id (k::ids) in - let v = next_global_ident_away true v_id (p::k::ids) in - let heq = next_global_ident_away true heq_id (v::p::k::ids) in - let heq1 = next_global_ident_away true heq_id (heq::v::p::k::ids) in - let hex = next_global_ident_away true hex_id (heq1::heq::v::p::k::ids) in - tclTHENLIST [ - h_intros [v; hex]; - simplest_elim (mkVar hex); - h_intros [p;heq1]; - tclTRY - (rewriteRL - (mkApp(mkVar heq1, - [|mkApp (delayed_force coq_S, [|mkVar p|]); - mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|]))); - simpl_iter onConcl; - tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]); - list_rewrite true eqs; - apply (delayed_force refl_equal)] g;; - -let f_S t = mkApp(delayed_force coq_S, [|t|]);; - - -let rec introduce_all_values_eq cont_tac functional termine - f p heq1 pmax bounds le_proofs eqs ids = - function - [] -> - let heq2 = next_global_ident_away true heq_id ids in - tclTHENLIST - [forward None (IntroIdentifier heq2) - (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); - simpl_iter (onHyp heq2); - unfold_in_hyp [([1], evaluable_of_global_reference - (global_of_constr functional))] - (([], heq2), Tacexpr.InHyp); - tclTHENS - (fun gls -> - let t_eq = compute_renamed_type gls (mkVar heq2) in - let def_id = - let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in - Nameops.out_name def_na - in - observe_tac "rewrite heq" (general_rewrite_bindings false [] - (mkVar heq2, - ExplicitBindings[dummy_loc,NamedHyp def_id, - f]) false) gls) - [tclTHENLIST - [observe_tac "list_rewrite" (list_rewrite true eqs); - cont_tac pmax le_proofs]; - tclTHENLIST[apply (delayed_force le_lt_SS); - compute_le_proofs le_proofs]]] - | arg::args -> - let v' = next_global_ident_away true v_id ids in - let ids = v'::ids in - let hex' = next_global_ident_away true hex_id ids in - let ids = hex'::ids in - let p' = next_global_ident_away true p_id ids in - let ids = p'::ids in - let new_pmax = next_global_ident_away true pmax_id ids in - let ids = pmax::ids in - let hle1 = next_global_ident_away true hle_id ids in - let ids = hle1::ids in - let hle2 = next_global_ident_away true hle_id ids in - let ids = hle2::ids in - let heq = next_global_ident_away true heq_id ids in - let ids = heq::ids in - let heq2 = next_global_ident_away true heq_id ids in - let ids = heq2::ids in - tclTHENLIST - [mkCaseEq(mkApp(termine, Array.of_list arg)); - h_intros [v'; hex']; - simplest_elim(mkVar hex'); - h_intros [p']; - simplest_elim(mkApp(delayed_force max_constr, [|mkVar pmax; - mkVar p'|])); - h_intros [new_pmax;hle1;hle2]; - introduce_all_values_eq - (fun pmax' le_proofs'-> - tclTHENLIST - [cont_tac pmax' le_proofs'; - h_intros [heq;heq2]; - observe_tac ("rewriteRL " ^ (string_of_id heq2)) - (tclTRY (rewriteLR (mkVar heq2))); - tclTRY (tclTHENS - ( fun g -> - let t_eq = compute_renamed_type g (mkVar heq) in - let k_id,def_id = - let k_na,_,t = destProd t_eq in - let _,_,t = destProd t in - let def_na,_,_ = destProd t in - Nameops.out_name k_na,Nameops.out_name def_na - in - let c_b = (mkVar heq, - ExplicitBindings - [dummy_loc, NamedHyp k_id, - f_S(mkVar pmax'); - dummy_loc, NamedHyp def_id, f]) - in - observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false [] - c_b false)) - g - ) - [tclIDTAC; - tclTHENLIST - [apply (delayed_force le_lt_n_Sm); - compute_le_proofs le_proofs']])]) - functional termine f p heq1 new_pmax - (p'::bounds)((mkVar pmax)::le_proofs) eqs - (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args] - - -let rec_leaf_eq termine f ids functional eqs expr fn args = - let p = next_global_ident_away true p_id ids in - let ids = p::ids in - let v = next_global_ident_away true v_id ids in - let ids = v::ids in - let hex = next_global_ident_away true hex_id ids in - let ids = hex::ids in - let heq1 = next_global_ident_away true heq_id ids in - let ids = heq1::ids in - let hle1 = next_global_ident_away true hle_id ids in - let ids = hle1::ids in - tclTHENLIST - [observe_tac "intros v hex" (h_intros [v;hex]); - simplest_elim (mkVar hex); - h_intros [p;heq1]; - h_generalize [mkApp(delayed_force le_n,[|mkVar p|])]; - h_intros [hle1]; - observe_tac "introduce_all_values_eq" (introduce_all_values_eq - (fun _ _ -> tclIDTAC) - functional termine f p heq1 p [] [] eqs ids args); - observe_tac "failing here" (apply (delayed_force refl_equal))] - -let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) - (eqs:constr list) (expr:constr) = -(* tclTRY *) - (match kind_of_term expr with - Case(ci,t,a,l) -> - (match find_call_occs 0 f a with - _,[] -> - (fun g -> - let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in - tclTHENS - destruct_tac - (list_map_i - (fun i -> mk_intros_and_continue - (List.rev rev_to_thin_intro) true - (prove_eq termine f functional) - eqs ci.ci_cstr_nargs.(i)) - 0 (Array.to_list l)) g) - | _,_::_ -> - (match find_call_occs 0 f expr with - _,[] -> base_leaf_eq functional eqs f - | fn,args -> - fun g -> - let ids = ids_of_named_context (pf_hyps g) in - rec_leaf_eq termine f ids - (constr_of_global functional) - eqs expr fn args g)) - | _ -> - (match find_call_occs 0 f expr with - _,[] -> base_leaf_eq functional eqs f - | fn,args -> - fun g -> - let ids = ids_of_named_context (pf_hyps g) in - observe_tac "rec_leaf_eq" (rec_leaf_eq - termine f ids (constr_of_global functional) - eqs expr fn args) g));; - -let (com_eqn : identifier -> - global_reference -> global_reference -> global_reference - -> constr -> unit) = - fun eq_name functional_ref f_ref terminate_ref equation_lemma_type -> - let opacity = - match terminate_ref with - | ConstRef c -> - let cb = Global.lookup_constant c in - if cb.Declarations.const_opaque then true - else begin match cb.const_body with None -> true | _ -> false end - | _ -> anomaly "terminate_lemma: not a constant" - in - let (evmap, env) = Command.get_current_context() in - let f_constr = (constr_of_global f_ref) in - let equation_lemma_type = subst1 f_constr equation_lemma_type in - (start_proof eq_name (Global, Proof Lemma) - (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); - by - (start_equation f_ref terminate_ref - (fun x -> - prove_eq - (constr_of_global terminate_ref) - f_constr - functional_ref - [] - (instantiate_lambda - (def_of_const (constr_of_global functional_ref)) - (f_constr::List.map mkVar x) - ) - ) - ); -(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) -(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) - Flags.silently (fun () ->Command.save_named opacity) () ; -(* Pp.msgnl (str "eqn finished"); *) - - );; - -let nf_zeta env = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) - env - Evd.empty - -let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq - generate_induction_principle using_lemmas : unit = - let function_type = interp_constr Evd.empty (Global.env()) type_of_f in - let env = push_named (function_name,None,function_type) (Global.env()) in -(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in -(* Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *) - let res_vars,eq' = decompose_prod equation_lemma_type in - let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in - let eq' = nf_zeta env_eq' eq' in - let res = -(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) -(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) -(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) - match kind_of_term eq' with - | App(e,[|_;_;eq_fix|]) -> - mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) - | _ -> failwith "Recursive Definition (res not eq)" - in - let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in - let (_, rec_arg_type, _) = destProd function_type_before_rec_arg in - let arg_types = List.rev_map snd (fst (decompose_prod_n (List.length res_vars) function_type)) in - let equation_id = add_suffix function_name "_equation" in - let functional_id = add_suffix function_name "_F" in - let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Definition) res in - let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in - let relation = - interp_constr - Evd.empty - env_with_pre_rec_args - r - in - let tcc_lemma_name = add_suffix function_name "_tcc" in - let tcc_lemma_constr = ref None in -(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook _ _ = - let term_ref = Nametab.locate (make_short_qualid term_id) in - let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in -(* message "start second proof"; *) - let stop = ref false in - begin - try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) - with e -> - begin - if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e) - else anomaly "Cannot create equation Lemma" - ; -(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) - stop := true; - end - end; - if not !stop - then - let eq_ref = Nametab.locate (make_short_qualid equation_id ) in - let f_ref = destConst (constr_of_global f_ref) - and functional_ref = destConst (constr_of_global functional_ref) - and eq_ref = destConst (constr_of_global eq_ref) in - generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; - if Flags.is_verbose () - then msgnl (h 1 (Ppconstr.pr_id function_name ++ - spc () ++ str"is defined" )++ fnl () ++ - h 1 (Ppconstr.pr_id equation_id ++ - spc () ++ str"is defined" ) - ) - in - try - com_terminate - tcc_lemma_name - tcc_lemma_constr - is_mes functional_ref - rec_arg_type - relation rec_arg_num - term_id - using_lemmas - (List.length res_vars) - hook - with e -> - begin - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); -(* anomaly "Cannot create termination Lemma" *) - raise e - end - - -VERNAC COMMAND EXTEND RecursiveDefinition - [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf) - constr(proof) integer_opt(rec_arg_num) constr(eq) ] -> - [ - warning "Recursive Definition is obsolete. Use Function instead"; - ignore(proof);ignore(wf); - let rec_arg_num = - match rec_arg_num with - | None -> 1 - | Some n -> n - in - recursive_definition false f [] type_of_f r rec_arg_num eq (fun _ _ _ _ _ _ _ _ -> ()) []] -| [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf) - "[" ne_constr_list(proof) "]" constr(eq) ] -> - [ ignore(proof);ignore(wf);recursive_definition false f [] type_of_f r 1 eq (fun _ _ _ _ _ _ _ _ -> ()) []] -END - - - -- cgit v1.2.3