(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* assert false end in try let v = tac g in msgnl (goal ++ fnl () ++ (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 = 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 Options.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 -> (Global.lookup_constant sp).const_type |_ -> 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 rec (find_call_occs: constr -> constr -> (constr list ->constr)*(constr list list)) = fun f expr -> match (kind_of_term expr) with App (g, args) when g = f -> (* For now we suppose that the function takes only one argument. *) (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::tl -> (match find_aux tl with (cf, ((arg1::args) as opt_args)) -> (match find_call_occs f a with cf2, (_ :: _ as other_args) -> let len1 = List.length other_args in (fun l -> cf2 l::(cf (nthtl(l,len1)))), other_args@opt_args | _, [] -> (fun x -> a::cf x), opt_args) | _, [] -> (match find_call_occs f a with cf, (arg1::args) -> (fun l -> cf l::tl), (arg1::args) | _, [] -> (fun x -> a::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(_) -> error "find_call_occs : Rel" | Var(id) -> (fun l -> expr), [] | Meta(_) -> error "find_call_occs : Meta" | Evar(_) -> error "find_call_occs : Evar" | Sort(_) -> error "find_call_occs : Sort" | Cast(_,_,_) -> error "find_call_occs : cast" | Prod(_,_,_) -> error "find_call_occs : Prod" | Lambda(_,_,_) -> error "find_call_occs : Lambda" | LetIn(_,_,_,_) -> error "find_call_occs : let in" | Const(_) -> (fun l -> expr), [] | Ind(_) -> (fun l -> expr), [] | Construct (_, _) -> (fun l -> expr), [] | Case(i,t,a,r) -> (match find_call_occs f a with cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args) | _ -> (fun l -> mkCase(i, t, a, r)),[]) | 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_reference (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_reference (delayed_force iter_ref)) let max_constr = function () -> (constr_of_reference (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") let mkCaseEq a : tactic = (fun g -> (* commentaire de Yves: on pourra avoir des problemes si a n'est pas bien type dans l'environnement du but *) let type_of_a = pf_type_of g a in (tclTHEN (generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]) (tclTHEN (fun g2 -> change_in_concl None (pattern_occs [([2], a)] (pf_env g2) Evd.empty (pf_concl g2)) g2) (simplest_case a))) g);; let rec mk_intros_and_continue (extra_eqn:bool) cont_function (eqs:constr list) (expr:constr) g = let ids = pf_ids_of_hyps g in match kind_of_term expr with | Lambda (n, _, b) -> let n1 = match n with Name x -> x | Anonymous -> ano_id in let new_n = next_global_ident_away true n1 ids in tclTHEN (h_intro new_n) (mk_intros_and_continue extra_eqn cont_function eqs (subst1 (mkVar new_n) b)) g | _ -> if extra_eqn then let teq = next_global_ident_away true teq_id ids in tclTHEN (h_intro teq) (cont_function (mkVar teq::eqs) expr) g else cont_function eqs expr g let const_of_ref = function ConstRef kn -> kn | _ -> anomaly "ConstRef expected" let simpl_iter () = reduce (Lazy {rBeta=true;rIota=true;rZeta= true; rDelta=false; rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]}) onConcl let tclUSER is_mes l g = let b,l = match l with None -> true,[] | Some l -> false,l in tclTHENSEQ [ (h_clear b l); if is_mes then unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] else tclIDTAC ] 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 ids = pf_ids_of_hyps g in let k' = next_global_ident_away true k_id ids in let h = next_global_ident_away true h_id (k'::ids) 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(); 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 (apply_with_bindings (delayed_force le_trans, ExplicitBindings[dummy_loc,NamedHyp(id_of_string "m"),a])) [compute_le_proofs tl; tclORELSE (apply (delayed_force le_n)) assumption]) let make_lt_proof pmax le_proof = tclTHENS (apply_with_bindings (delayed_force le_lt_trans, ExplicitBindings[dummy_loc,NamedHyp(id_of_string "m"), pmax])) [compute_le_proofs le_proof; tclTHENLIST[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 -> tclTHENS (general_rewrite_bindings false (mkVar eq, ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; dummy_loc, NamedHyp def_id, mkVar def])) [list_cond_rewrite k def pmax eqs le_proofs; make_lt_proof pmax le_proofs];; 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]); h_intros [k;h';def]; simpl_iter(); unfold_in_concl[([1],evaluable_of_global_reference func)]; list_rewrite true eqs; list_cond_rewrite k def bound cond_eqs le_proofs; 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 = try for i = 0 to 3 do if String.get s i <> String.get "Acc_" i then failwith "" done; with Invalid_argument _ -> failwith "" let retrieve_acc_var g = (* Julien: I don't like this version .... *) let hyps = pf_ids_of_hyps g in map_succeed (fun id -> try string_match (string_of_id id); id with _ -> failwith "") hyps let rec introduce_all_values is_mes acc_inv func context_fn eqs hrec args values specs = (match args with [] -> tclTHENLIST [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 = introduce_all_values is_mes acc_inv func context_fn eqs hrec args (rec_res::values)(hspec::specs) in (tclTHENS (simplest_elim (mkApp(mkVar hrec, Array.of_list arg))) [tclTHENLIST [h_intros [rec_res; hspec]; tac]; (tclTHENS (apply (Lazy.force acc_inv)) [ h_assumption ; (fun g -> tclUSER is_mes (Some (hrec::hspec::(retrieve_acc_var g)@specs)) g ) ] ) ]) g) ) let rec_leaf_terminate is_mes acc_inv hrec (func:global_reference) eqs expr = match find_call_occs (mkVar (get_f (constr_of_reference func))) expr with | context_fn, args -> observe_tac "introduce_all_values" (introduce_all_values is_mes acc_inv func context_fn eqs hrec args [] []) (* let rec proveterminate is_mes acc_inv (hrec:identifier) (f_constr:constr) (func:global_reference) (eqs:constr list) (expr:constr) = try (* let _ = msgnl (str "entering proveterminate") in *) let v = match (kind_of_term expr) with Case (_, t, a, l) -> (match find_call_occs f_constr a with _,[] -> tclTHENS (fun g -> (* let _ = msgnl(str "entering mkCaseEq") in *) let v = (mkCaseEq a) g in (* let _ = msgnl (str "exiting mkCaseEq") in *) v ) (List.map (mk_intros_and_continue true (proveterminate is_mes acc_inv hrec f_constr func) eqs) (Array.to_list l)) | _, _::_ -> ( match find_call_occs 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 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 (* let _ = msgnl(str "exiting proveterminate") in *) v with e -> msgerrnl(str "failure in proveterminate"); raise e *) let proveterminate 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 (_, t, a, l) -> (match find_call_occs f_constr a with _,[] -> tclTHENS (fun g -> (* let _ = msgnl(str "entering mkCaseEq") in *) let v = (mkCaseEq a) g in (* let _ = msgnl (str "exiting mkCaseEq") in *) v ) (List.map (mk_intros_and_continue true proveterminate eqs) (Array.to_list l) ) | _, _::_ -> ( match find_call_occs 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 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 (* let _ = msgnl(str "exiting proveterminate") in *) v with e -> msgerrnl(str "failure in proveterminate"); raise e in proveterminate let hyp_terminates func = let a_arrow_b = arg_type (constr_of_reference func) in let rev_args,b = decompose_prod a_arrow_b in let left = mkApp(delayed_force iter, Array.of_list (lift 5 a_arrow_b:: mkRel 3:: constr_of_reference 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 is_mes = if is_mes then tclCOMPLETE (h_apply (delayed_force well_founded_ltof,Rawterm.NoBindings)) else tclUSER is_mes None let start 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 of the well_foundness of the relation *) wf_tac is_mes; (* well_foundness -> Acc for any element *) observe_tac "apply wf_thm" (h_apply ((mkApp(mkVar wf_thm, [|mkVar rec_arg_id |])),Rawterm.NoBindings) ) ] ; (* rest of the proof *) tclTHENSEQ [observe_tac "generalize" (onNLastHyps (nargs+1) (fun (id,_,_) -> tclTHEN (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 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 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_reference 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 -> assert false in let n_names_types,_ = decompose_lam 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 | _ -> assert false ) ([],(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 start is_mes input_type ids n_ids relation rec_arg_num rec_arg_id (fun hrec acc_inv g -> (proveterminate is_mes acc_inv hrec (mkVar f_id) func base_leaf_terminate rec_leaf_terminate [] expr ) g ) tclUSER_if_not_mes g end let get_current_subgoals_types () = let pts = get_pftreestate () in let _,subs = extract_open_pftreestate pts in List.map snd 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 | [] -> assert false | [p] -> p,tclIDTAC,1 | p1::pl -> let c,tac,nb = f pl in mk_and p1 c, tclTHENS (apply (constr_of_reference conj_constr)) [tclIDTAC; tac ],nb+1 in f l let build_new_goal_type () = let sub_gls_types = get_current_subgoals_types () in let res = build_and_l sub_gls_types in res let interpretable_as_section_decl d1 d2 = match d1,d2 with | (_,Some _,_), (_,None,_) -> false | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2 | (_,None,t1), (_,_,t2) -> eq_constr t1 t2 (* let final_decompose lemma n : tactic = *) (* fun gls -> *) (* let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in *) (* tclTHENSEQ *) (* [ *) (* generalize [lemma]; *) (* tclDO *) (* n *) (* (tclTHENSEQ *) (* [h_intro hid; *) (* h_case (mkVar hid,Rawterm.NoBindings); *) (* clear [hid]; *) (* intro_patterns [Genarg.IntroWildcard] *) (* ] *) (* ); *) (* h_intro hid; *) (* tclTRY *) (* (tclTHENSEQ [h_case (mkVar hid,Rawterm.NoBindings); *) (* clear [hid]; *) (* h_intro hid; *) (* intro_patterns [Genarg.IntroWildcard] *) (* ]); *) (* e_resolve_constr (mkVar hid); *) (* e_assumption *) (* ] *) (* gls *) let prove_with_tcc lemma _ : tactic = fun gls -> let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in tclTHENSEQ [ 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 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 _ -> assert false 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 v = let lemme = mkConst (Lib.make_con na) in *) (* Tactics.exact_no_check *) (* (applist (lemme, *) (* List.rev (Array.to_list (Sign.instance_from_named_context sign)))) *) (* gls in *) let hook _ _ = let lemma = mkConst (Lib.make_con na) in Array.iteri (fun i _ -> by (observe_tac "tac" (prove_with_tcc lemma i))) (Array.make nb_goal ()); ref := Some lemma ; Command.save_named true; in start_proof na (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) sign gls_type hook ; by (decompose_and_tac); () let com_terminate ref is_mes fonctional_ref input_type relation rec_arg_num thm_name hook = let (evmap, env) = Command.get_current_context() in start_proof thm_name (Global, Proof Lemma) (Environ.named_context_val env) (hyp_terminates fonctional_ref) hook; by (observe_tac "whole_start" (whole_start is_mes fonctional_ref input_type relation rec_arg_num )); open_new_goal ref None (build_new_goal_type ()) 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,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, 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 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_reference term_f in let nargs = nb_prod (type_of_const terminate_constr) in let x = let rec f ids n = if n = 0 then [] else let x = next_global_ident_away true x_id ids in x::f (x::ids) (n-1) in f ids nargs in tclTHENLIST [ h_intros x; unfold_constr f; simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))); 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(); 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 [] -> tclTHENLIST [tclTHENS (general_rewrite_bindings false (mkVar heq1, ExplicitBindings[dummy_loc,NamedHyp k_id, f_S(f_S(mkVar pmax)); dummy_loc,NamedHyp def_id, f])) [tclTHENLIST [simpl_iter(); unfold_constr (reference_of_constr functional); 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]; rewriteLR (mkVar heq2); tclTHENS (general_rewrite_bindings false (mkVar heq, ExplicitBindings [dummy_loc, NamedHyp k_id, f_S(mkVar pmax'); dummy_loc, NamedHyp def_id, f])) [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 [h_intros [v;hex]; simplest_elim (mkVar hex); h_intros [p;heq1]; generalize [mkApp(delayed_force le_n,[|mkVar p|])]; h_intros [hle1]; introduce_all_values_eq (fun _ _ -> tclIDTAC) functional termine f p heq1 p [] [] eqs ids args; 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(_,t,a,l) -> (match find_call_occs f a with _,[] -> tclTHENS(mkCaseEq a)(* (simplest_case a) *) (List.map (mk_intros_and_continue true (prove_eq termine f functional) eqs) (Array.to_list l)) | _,_::_ -> (match find_call_occs 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_reference functional) eqs expr fn args g)) | _ -> (match find_call_occs 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_reference functional) eqs expr fn args g));; let (com_eqn : identifier -> global_reference -> global_reference -> global_reference -> constr_expr -> unit) = fun eq_name functional_ref f_ref terminate_ref eq -> let (evmap, env) = Command.get_current_context() in let eq_constr = interp_constr evmap env eq in let f_constr = (constr_of_reference f_ref) in (start_proof eq_name (Global, Proof Lemma) (Environ.named_context_val env) eq_constr (fun _ _ -> ()); by (start_equation f_ref terminate_ref (fun x -> prove_eq (constr_of_reference terminate_ref) f_constr functional_ref [] (instantiate_lambda (def_of_const (constr_of_reference functional_ref)) (f_constr::List.map mkVar x) ) ) ); Command.save_named true);; let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_principle : unit = let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_rel (Name f,None,function_type) (Global.env()) in let res_vars,eq' = decompose_prod (interp_constr Evd.empty env 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 f,function_type,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 f "_equation" in let functional_id = add_suffix f "_F" in let term_id = add_suffix f "_terminate" in let functional_ref = declare_fun functional_id (IsDefinition Definition) res in (* let _ = Pp.msgnl (str "res := " ++ Printer.pr_lconstr 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_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 f (IsProof Lemma) arg_types term_ref in (* let _ = message "start second proof" in *) com_eqn equation_id functional_ref f_ref term_ref eq; let eq_ref = Nametab.locate (make_short_qualid equation_id ) in generate_induction_principle tcc_lemma_constr functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; () in com_terminate tcc_lemma_constr is_mes functional_ref rec_arg_type relation rec_arg_num term_id hook ;; (* let observe_tac = do_observe_tac *) let base_leaf_princ eq_cst functional_ref eqs expr = tclTHENSEQ [rewriteLR (mkConst eq_cst); tclTRY (list_rewrite true eqs); gen_eauto(* default_eauto *) false (false,5) [] (Some []) ] let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with | None -> tclIDTAC_MESSAGE (str "No tcc proof !!") | Some lemma -> fun gls -> let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in tclTHENSEQ [ generalize [lemma]; h_intro hid; Elim.h_decompose_and (mkVar hid); tclTRY(list_rewrite true eqs); gen_eauto(* default_eauto *) false (false,5) [] (Some []) (* default_auto *) ] gls let finalize_rec_leaf_princ_with tcc_lemma_constr is_mes hrec acc_inv eqs br = fun g -> tclTHENSEQ [ Eauto.e_resolve_constr (mkVar br); tclFIRST [ e_assumption; reflexivity; tclTHEN (apply (mkVar hrec)) (tclTHENS (* (try *) (observe_tac "applying inversion" (apply (Lazy.force acc_inv))) (* with e -> Pp.msgnl (Printer.pr_lconstr (Lazy.force acc_inv));raise e *) (* ) *) [ h_assumption ; tclTHEN (fun g -> tclUSER is_mes (Some (hrec::(retrieve_acc_var g))) g ) (fun g -> prove_with_tcc tcc_lemma_constr eqs g) ] ); gen_eauto(* default_eauto *) false (false,5) [] (Some []); (fun g -> tclIDTAC_MESSAGE (str "here" ++ Printer.pr_goal (sig_it g)) g) ] ] g let rec_leaf_princ tcc_lemma_constr eq_cst branches_names is_mes acc_inv hrec (functional_ref:global_reference) eqs expr = fun g -> tclTHENSEQ [ rewriteLR (mkConst eq_cst); list_rewrite true eqs; tclFIRST (List.map (finalize_rec_leaf_princ_with tcc_lemma_constr is_mes hrec acc_inv eqs) branches_names) ] g let fresh_id avoid na = let id = match na with | Name id -> id | Anonymous -> h_id in next_global_ident_away true id avoid let prove_principle tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation = (* f_ref eq_ref rec_arg_num rec_arg_type nb_args relation *) let eq_cst = match eq_ref with ConstRef sp -> sp | _ -> assert false in fun g -> let type_of_goal = pf_concl g in let goal_ids = pf_ids_of_hyps g in let goal_elim_infos = compute_elim_sig type_of_goal in let params_names,ids = List.fold_left (fun (params_names,avoid) (na,_,_) -> let new_id = fresh_id avoid na in (new_id::params_names,new_id::avoid) ) ([],goal_ids) goal_elim_infos.params in let predicates_names,ids = List.fold_left (fun (predicates_names,avoid) (na,_,_) -> let new_id = fresh_id avoid na in (new_id::predicates_names,new_id::avoid) ) ([],ids) goal_elim_infos.predicates in let branches_names,ids = List.fold_left (fun (branches_names,avoid) (na,_,_) -> let new_id = fresh_id avoid na in (new_id::branches_names,new_id::avoid) ) ([],ids) goal_elim_infos.branches in let to_intro = params_names@predicates_names@branches_names in let nparams = List.length params_names in let rec_arg_num = rec_arg_num - nparams in begin tclTHEN (h_intros to_intro) (observe_tac (string_of_int (rec_arg_num)) (fun g -> let ids = ids_of_named_context (pf_hyps g) in let func_body = (def_of_const (constr_of_reference functional_ref)) in (* let _ = Pp.msgnl (Printer.pr_lconstr func_body) 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 -> assert false in let n_names_types,_ = decompose_lam 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 | _ -> assert false ) ([],(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 start is_mes rec_arg_type ids (snd (list_chop nparams n_ids)) (substl (List.map mkVar params_names) relation) (rec_arg_num) rec_arg_id (fun hrec acc_inv g -> (proveterminate is_mes acc_inv hrec (mkVar f_id) functional_ref (base_leaf_princ eq_cst) (rec_leaf_princ tcc_lemma_ref eq_cst branches_names) [] expr ) g ) (if is_mes then tclUSER_if_not_mes else fun _ -> prove_with_tcc tcc_lemma_ref []) g ) ) end g 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) ] -> [ 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