diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
-rw-r--r-- | tactics/decl_proof_instr.ml | 1476 |
1 files changed, 1476 insertions, 0 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml new file mode 100644 index 00000000..e7acd6d6 --- /dev/null +++ b/tactics/decl_proof_instr.ml @@ -0,0 +1,1476 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Util +open Pp +open Evd + +open Refiner +open Proof_type +open Proof_trees +open Tacmach +open Tacinterp +open Decl_expr +open Decl_mode +open Decl_interp +open Rawterm +open Names +open Declarations +open Tactics +open Tacticals +open Term +open Termops +open Reductionops +open Goptions + +(* Strictness option *) + +let get_its_info gls = get_info gls.it + +let get_strictness,set_strictness = + let strictness = ref false in + (fun () -> (!strictness)),(fun b -> strictness:=b) + +let _ = + declare_bool_option + { optsync = true; + optname = "strict mode"; + optkey = (SecondaryTable ("Strict","Proofs")); + optread = get_strictness; + optwrite = set_strictness } + +let tcl_change_info_gen info_gen = + (fun gls -> + let gl =sig_it gls in + {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, + function + [pftree] -> + {pftree with + goal=gl; + ref=Some (Change_evars,[pftree])} + | _ -> anomaly "change_info : Wrong number of subtrees") + +let tcl_change_info info gls = tcl_change_info_gen (Some (pm_in info)) gls + +let tcl_erase_info gls = tcl_change_info_gen None gls + +let special_whd gl= + let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let special_nf gl= + let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in + (fun t -> Closure.norm_val infos (Closure.inject t)) + +let is_good_inductive env ind = + let mib,oib = Inductive.lookup_mind_specif env ind in + oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) + +let check_not_per pts = + if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then + match get_stack pts with + Per (_,_,_,_)::_ -> + error "You are inside a proof per cases/induction.\n\ +Please \"suppose\" something or \"end\" it now." + | _ -> () + +let get_thesis gls0 = + let info = get_its_info gls0 in + match info.pm_subgoals with + [m,thesis] -> thesis + | _ -> error "Thesis is split" + +let mk_evd metalist gls = + let evd0= create_evar_defs (sig_sig gls) in + let add_one (meta,typ) evd = + meta_declare meta typ evd in + List.fold_right add_one metalist evd0 + +(* start a proof *) + +let start_proof_tac gls= + let gl=sig_it gls in + let info={pm_last=Anonymous; + pm_partial_goal=mkMeta 1; + pm_hyps= + begin + let hyps = pf_ids_of_hyps gls in + List.fold_right Idset.add hyps Idset.empty + end; + pm_subgoals= [1,gl.evar_concl]; + pm_stack=[]} in + {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, + function + [pftree] -> + {pftree with + goal=gl; + ref=Some (Decl_proof true,[pftree])} + | _ -> anomaly "Dem : Wrong number of subtrees" + +let go_to_proof_mode () = + Pfedit.mutate + (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts)) + +(* closing gaps *) + +let daimon_tac gls = + set_daimon_flag (); + ({it=[];sigma=sig_sig gls}, + function + [] -> + {open_subgoals=0; + goal=sig_it gls; + ref=Some (Daimon,[])} + | _ -> anomaly "Daimon: Wrong number of subtrees") + +let daimon _ pftree = + set_daimon_flag (); + {pftree with + open_subgoals=0; + ref=Some (Daimon,[])} + +let daimon_subtree = map_pftreestate (fun _ -> frontier_mapi daimon ) + +(* marking closed blocks *) + +let rec is_focussing_instr = function + Pthus i | Pthen i | Phence i -> is_focussing_instr i + | Pescape | Pper _ | Pclaim _ | Pfocus _ + | Psuppose _ | Pcase (_,_,_) -> true + | _ -> false + +let mark_rule_as_done = function + Decl_proof true -> Decl_proof false + | Decl_proof false -> + anomaly "already marked as done" + | Nested(Proof_instr (lock_focus,instr),spfl) -> + if lock_focus then + Nested(Proof_instr (false,instr),spfl) + else + anomaly "already marked as done" + | _ -> anomaly "mark_rule_as_done" + +let mark_proof_tree_as_done pt = + match pt.ref with + None -> anomaly "mark_proof_tree_as_done" + | Some (r,spfl) -> + {pt with ref= Some (mark_rule_as_done r,spfl)} + +let mark_as_done pts = + map_pftreestate + (fun _ -> mark_proof_tree_as_done) + (traverse 0 pts) + +(* post-instruction focus management *) + +let goto_current_focus pts = up_until_matching_rule is_focussing_command pts + +let goto_current_focus_or_top pts = + try + up_until_matching_rule is_focussing_command pts + with Not_found -> top_of_tree pts + +(* return *) + +let close_tactic_mode pts = + let pts1= + try goto_current_focus pts + with Not_found -> + error "\"return\" cannot be used outside of Declarative Proof Mode" in + let pts2 = daimon_subtree pts1 in + let pts3 = mark_as_done pts2 in + goto_current_focus pts3 + +let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode + +(* end proof/claim *) + +let close_block bt pts = + let stack = + if Proof_trees.is_complete_proof (proof_of_pftreestate pts) then + get_top_stack pts + else + get_stack pts in + match bt,stack with + B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> + daimon_subtree (goto_current_focus pts) + | _, Claim::_ -> + error "\"end claim\" expected" + | _, Focus_claim::_ -> + error "\"end focus\" expected" + | _, [] -> + error "\"end proof\" expected" + | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) -> + begin + match et with + ET_Case_analysis -> error "\"end cases\" expected" + | ET_Induction -> error "\"end induction\" expected" + end + | _,_ -> anomaly "lonely suppose on stack" + +(* utility for suppose / suppose it is *) + +let close_previous_case pts = + if + Proof_trees.is_complete_proof (proof_of_pftreestate pts) + then + match get_top_stack pts with + Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus (mark_as_done pts) + | _ -> error "Not inside a proof per cases or induction." + else + match get_stack pts with + Per (et,_,_,_) :: _ -> pts + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus (mark_as_done (daimon_subtree pts)) + | _ -> error "Not inside a proof per cases or induction." + +(* Proof instructions *) + +(* automation *) + +let filter_hyps f gls = + let filter_aux (id,_,_) = + if f id then + tclIDTAC + else + tclTRY (clear [id]) in + tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls + +let local_hyp_prefix = id_of_string "___" + +let add_justification_hyps keep items gls = + let add_aux c gls= + match kind_of_term c with + Var id -> + keep:=Idset.add id !keep; + tclIDTAC gls + | _ -> + let id=pf_get_new_id local_hyp_prefix gls in + keep:=Idset.add id !keep; + letin_tac false (Names.Name id) c Tacexpr.nowhere gls in + tclMAP add_aux items gls + +let apply_to_prepared_goal items kont gls = + let tokeep = ref Idset.empty in + let auxres = add_justification_hyps tokeep items gls in + tclTHENLIST + [ (fun _ -> auxres); + filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep); + kont ] gls + +let my_automation_tac = ref + (fun gls -> anomaly "No automation registered") + +let register_automation_tac tac = my_automation_tac:= tac + +let automation_tac gls = !my_automation_tac gls + +let justification tac gls= + tclORELSE + (tclSOLVE [tac]) + (fun gls -> + if get_strictness () then + error "insufficient justification" + else + begin + msgnl (str "Warning: insufficient justification"); + daimon_tac gls + end) gls + +let default_justification items gls= + justification (apply_to_prepared_goal items automation_tac) gls + +(* code for have/then/thus/hence *) + +type stackd_elt = +{se_meta:metavariable; + se_type:types; + se_last_meta:metavariable; + se_meta_list:(metavariable*types) list; + se_evd: evar_defs} + +let rec replace_in_list m l = function + [] -> raise Not_found + | c::q -> if m=fst c then l@q else c::replace_in_list m l q + +let enstack_subsubgoals env se stack gls= + let hd,params = decompose_app (special_whd gls se.se_type) in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let process i gentyp = + let constructor = mkConstruct(ind,succ i) + (* constructors numbering*) in + let appterm = applist (constructor,params) in + let apptype = Term.prod_applist gentyp params in + let rc,_ = Reduction.dest_prod env apptype in + let rec meta_aux last lenv = function + [] -> (last,lenv,[]) + | (nam,_,typ)::q -> + let nlast=succ last in + let (llast,holes,metas) = + meta_aux nlast (mkMeta nlast :: lenv) q in + (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in + let (nlast,holes,nmetas) = + meta_aux se.se_last_meta [] (List.rev rc) in + let refiner = applist (appterm,List.rev holes) in + let evd = meta_assign se.se_meta refiner se.se_evd in + let ncreated = replace_in_list + se.se_meta nmetas se.se_meta_list in + let evd0 = List.fold_left + (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in + List.iter (fun (m,typ) -> + Stack.push + {se_meta=m; + se_type=typ; + se_evd=evd0; + se_meta_list=ncreated; + se_last_meta=nlast} stack) (List.rev nmetas) + in + Array.iteri process gentypes + | _ -> () + +let find_subsubgoal env c ctyp skip evd metas gls = + let stack = Stack.create () in + let max_meta = + List.fold_left (fun a (m,_) -> max a m) 0 metas in + let _ = + List.iter (fun (m,typ) -> + Stack.push + {se_meta=m; + se_type=typ; + se_last_meta=max_meta; + se_meta_list=metas; + se_evd=evd} stack) (List.rev metas) in + let rec dfs n = + let se = Stack.pop stack in + try + let unifier = + Unification.w_unify true env Reduction.CUMUL + ctyp se.se_type se.se_evd in + if n <= 0 then + {se with se_evd=meta_assign se.se_meta c unifier} + else + dfs (pred n) + with _ -> + begin + enstack_subsubgoals env se stack gls; + dfs n + end in + let nse= try dfs skip with Stack.Empty -> raise Not_found in + nse.se_meta_list,nse.se_evd + +let rec nf_list evd = + function + [] -> [] + | (m,typ)::others -> + if meta_defined evd m then + nf_list evd others + else + (m,nf_meta evd typ)::nf_list evd others + + +let rec max_linear_context meta_one c = + if !meta_one = None then + if isMeta c then + begin + meta_one:= Some c; + mkMeta 1 + end + else + try + map_constr (max_linear_context meta_one) c + with Not_found -> + begin + meta_one:= Some c; + mkMeta 1 + end + else + if isMeta c then + raise Not_found + else + map_constr (max_linear_context meta_one) c + +let thus_tac c ctyp gls = + let info = get_its_info gls in + let evd0 = mk_evd info.pm_subgoals gls in + let list,evd = + try + find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals gls + with Not_found -> + error "I could not relate this statement to the thesis" in + let nflist = nf_list evd list in + let nfgoal = nf_meta evd info.pm_partial_goal in +(* let _ = msgnl (str "Partial goal : " ++ + print_constr_env (pf_env gls) nfgoal) in *) + let rgl = ref None in + let refiner = max_linear_context rgl nfgoal in + match !rgl with + None -> exact_check refiner gls + | Some pgl when not (isMeta refiner) -> + let ninfo={info with + pm_partial_goal = pgl; + pm_subgoals = nflist} in + tclTHEN + (Tactics.refine refiner) + (tcl_change_info ninfo) + gls + | _ -> + let ninfo={info with + pm_partial_goal = nfgoal; + pm_subgoals = nflist} in + tcl_change_info ninfo gls + +let anon_id_base = id_of_string "__" + + +let mk_stat_or_thesis info = function + This c -> c + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here" + | Thesis (Sub n) -> + begin + try List.assoc n info.pm_subgoals + with Not_found -> error "No such part in thesis." + end + | Thesis Plain -> + match info.pm_subgoals with + [_,c] -> c + | _ -> error + "\"thesis\" is split, please specify which part you refer to." + +let instr_cut mkstat _thus _then cut gls0 = + let info = get_its_info gls0 in + let just_tac gls = + match cut.cut_by with + Automated l -> + let elems = + if _then then + match info.pm_last with + Anonymous -> l + | Name id -> (mkVar id) ::l + else l in + default_justification elems gls + | By_tactic t -> + justification (Tacinterp.eval_tactic t) gls in + let c_id = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_fact") gls0 + | Name id -> id in + let c_stat = mkstat info cut.cut_stat.st_it in + let thus_tac gls= + if _thus then + thus_tac (mkVar c_id) c_stat gls + else tclIDTAC gls in + let ninfo = {info with pm_last=Name c_id} in + tclTHENS (internal_cut c_id c_stat) + [tclTHEN tcl_erase_info just_tac; + tclTHEN (tcl_change_info ninfo) thus_tac] gls0 + +(* iterated equality *) +let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) + +let decompose_eq id gls = + let typ = pf_get_hyp_typ gls id in + let whd = (special_whd gls typ) in + match kind_of_term whd with + App (f,args)-> + if eq_constr f _eq && (Array.length args)=3 + then (args.(0), + args.(1), + args.(2)) + else error "previous step is not an equality" + | _ -> error "previous step is not an equality" + +let instr_rew _thus rew_side cut gls0 = + let info = get_its_info gls0 in + let last_id = + match info.pm_last with + Anonymous -> error "no previous equality" + | Name id -> id in + let typ,lhs,rhs = decompose_eq last_id gls0 in + let just_tac gls = + match cut.cut_by with + Automated l -> + let elems = (mkVar last_id) :: l in + default_justification elems gls + | By_tactic t -> + justification (Tacinterp.eval_tactic t) gls in + let c_id = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_eq") gls0 + | Name id -> id in + let ninfo = {info with pm_last=Name c_id} in + let thus_tac new_eq gls= + if _thus then + thus_tac (mkVar c_id) new_eq gls + else tclIDTAC gls in + match rew_side with + Lhs -> + let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in + tclTHENS (internal_cut c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity lhs) + [just_tac;exact_check (mkVar last_id)]); + tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + | Rhs -> + let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in + tclTHENS (internal_cut c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity rhs) + [exact_check (mkVar last_id);just_tac]); + tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + + + +(* tactics for claim/focus *) + +let instr_claim _thus st gls0 = + let info = get_its_info gls0 in + let id = match st.st_label with + Anonymous -> pf_get_new_id (id_of_string "_claim") gls0 + | Name id -> id in + let thus_tac gls= + if _thus then + thus_tac (mkVar id) st.st_it gls + else tclIDTAC gls in + let ninfo1 = {info with + pm_stack= + (if _thus then Focus_claim else Claim)::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,st.st_it]} in + let ninfo2 = {info with pm_last=Name id} in + tclTHENS (internal_cut id st.st_it) + [tcl_change_info ninfo1; + tclTHEN (tcl_change_info ninfo2) thus_tac] gls0 + +(* tactics for assume *) + +let reset_concl gls = + let info = get_its_info gls in + tcl_change_info + {info with + pm_partial_goal=mkMeta 1; + pm_subgoals= [1,gls.it.evar_concl]} gls + +let set_last id gls = + let info = get_its_info gls in + tcl_change_info + {info with + pm_last=Name id} gls + +let intro_pm id gls= + let info = get_its_info gls in + match info.pm_subgoals with + [(_,typ)] -> + tclTHEN (intro_mustbe_force id) reset_concl gls + | _ -> error "Goal is split" + +let push_intro_tac coerce nam gls = + let hid = + match nam with + Anonymous -> pf_get_new_id (id_of_string "_hyp") gls + | Name id -> id in + let mark_id gls0 = + let info = get_its_info gls0 in + let ninfo = {info with + pm_last = Name hid; + pm_hyps = Idset.add hid info.pm_hyps } in + tcl_change_info ninfo gls0 in + tclTHENLIST + [intro_pm hid; + coerce hid; + mark_id] + gls + +let assume_tac hyps gls = + List.fold_right + (fun (Hvar st | Hprop st) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_hyps_or_theses hyps gls = + List.fold_right + (function + (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,c)) nam) + | Hprop {st_label=nam;st_it=Thesis (tk)} -> + tclTHEN + (push_intro_tac + (fun id -> tclIDTAC) nam)) + hyps tclIDTAC gls + +let assume_st hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_st_letin hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) + hyps tclIDTAC gls + +(* tactics for consider/given *) + +let update_goal_info gls = + let info = get_its_info gls in + match info.pm_subgoals with + [m,_] -> tcl_change_info {info with pm_subgoals =[m,pf_concl gls]} gls + | _ -> error "thesis is split" + +let conjunction_arity id gls = + let typ = pf_get_hyp_typ gls id in + let hd,params = decompose_app (special_whd gls typ) in + let env =pf_env gls in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let _ = if Array.length gentypes <> 1 then raise Not_found in + let apptype = Term.prod_applist gentypes.(0) params in + let rc,_ = Reduction.dest_prod env apptype in + List.length rc + | _ -> raise Not_found + +let rec intron_then n ids ltac gls = + if n<=0 then + tclTHEN + (fun gls -> + if List.exists (fun id -> occur_id [] id (pf_concl gls)) ids then + update_goal_info gls + else + tclIDTAC gls) + (ltac ids) + gls + else + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (intro_mustbe_force id) + (intron_then (pred n) (id::ids) ltac) gls + +let pm_rename_hyp id hid gls = + if occur_id [] id (pf_concl gls) then + tclTHEN (rename_hyp id hid) update_goal_info gls + else + rename_hyp id hid gls + +let rec consider_match may_intro introduced available expected gls = + match available,expected with + [],[] -> + if not may_intro then + set_last (List.hd introduced) gls + else + let info = get_its_info gls in + let nameset=List.fold_right Idset.add introduced info.pm_hyps in + tcl_change_info {info with + pm_last = Name (List.hd introduced); + pm_hyps = nameset} gls + | _,[] -> error "last statements do not match a complete hypothesis" + (* should tell which ones *) + | [],hyps -> + if may_intro then + begin + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclIFTHENELSE + (intro_pm id) + (consider_match true [] [id] hyps) + (fun _ -> + error "not enough sub-hypotheses to match statements") + gls + end + else + error "not enough sub-hypotheses to match statements" + (* should tell which ones *) + | id::rest_ids,(Hvar st | Hprop st)::rest -> + tclIFTHENELSE (convert_hyp (id,None,st.st_it)) + begin + match st.st_label with + Anonymous -> + consider_match may_intro (id::introduced) rest_ids rest + | Name hid -> + tclTHENLIST + [pm_rename_hyp id hid; + consider_match may_intro (hid::introduced) rest_ids rest] + end + begin + (fun gls -> + let nhyps = + try conjunction_arity id gls with + Not_found -> error "matching hypothesis not found" in + tclTHENLIST + [general_case_analysis (mkVar id,NoBindings); + intron_then nhyps [] + (fun l -> consider_match may_intro introduced + (List.rev_append l rest_ids) expected)] gls) + end + gls + +let consider_tac c hyps gls = + match kind_of_term (strip_outer_cast c) with + Var id -> + consider_match false [] [id] hyps gls + | _ -> + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (forward None (Genarg.IntroIdentifier id) c) + (consider_match false [] [id] hyps) gls + + +let given_tac hyps gls = + consider_match true [] [] hyps gls + +(* tactics for take *) + +let rec take_tac wits gls = + match wits with + [] -> tclIDTAC gls + | wit::rest -> + let typ = pf_type_of gls wit in + tclTHEN (thus_tac wit typ) (take_tac rest) gls + + +(* tactics for define *) + +let rec build_function args body = + match args with + st::rest -> + let pfun= lift 1 (build_function rest body) in + let id = match st.st_label with + Anonymous -> assert false + | Name id -> id in + mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) + | [] -> body + +let define_tac id args body gls = + let t = build_function args body in + letin_tac true (Name id) t Tacexpr.nowhere gls + +(* tactics for reconsider *) + +let cast_tac id_or_thesis typ gls = + let info = get_its_info gls in + match id_or_thesis with + This id -> + let (_,body,_) = pf_get_hyp gls id in + convert_hyp (id,body,typ) gls + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here" + | Thesis (Sub n) -> + begin + let old_typ = + try List.assoc n info.pm_subgoals + with Not_found -> error "No such part in thesis." in + if is_conv_leq (pf_env gls) (sig_sig gls) typ old_typ then + let new_sg = List.merge + (fun (n,_) (p,_) -> Pervasives.compare n p) + [n,typ] (List.remove_assoc n info.pm_subgoals) in + tcl_change_info {info with pm_subgoals=new_sg} gls + else + error "not convertible" + end + | Thesis Plain -> + match info.pm_subgoals with + [m,c] -> + tclTHEN + (convert_concl typ DEFAULTcast) + (tcl_change_info {info with pm_subgoals= [m,typ]}) gls + | _ -> error + "\"thesis\" is split, please specify which part you refer to." + + +(* per cases *) + +let start_tree env ind = + let constrs = (snd (Inductive.lookup_mind_specif env ind)).mind_consnames in + Split (Idset.empty,ind,Array.map (fun _ -> None) constrs) + +let build_per_info etype casee gls = + let concl=get_thesis gls in + let env=pf_env gls in + let ctyp=pf_type_of gls casee in + let is_dep = dependent casee concl in + let hd,args = decompose_app (special_whd gls ctyp) in + let ind = + try + destInd hd + with _ -> + error "Case analysis must be done on an inductive object" in + let nparams = + let mind = fst (Global.lookup_inductive ind) in + match etype with + ET_Induction -> mind.mind_nparams_rec + | _ -> mind.mind_nparams in + let params,real_args = list_chop nparams args in + let abstract_obj body c = + let typ=pf_type_of gls c in + lambda_create env (typ,subst_term c body) in + let pred= List.fold_left abstract_obj + (lambda_create env (ctyp,subst_term casee concl)) real_args in + is_dep, + {per_casee=casee; + per_ctype=ctyp; + per_ind=ind; + per_pred=pred; + per_args=real_args; + per_params=params; + per_nparams=nparams} + +let per_tac etype casee gls= + let env=pf_env gls in + let info = get_its_info gls in + match casee with + Real c -> + let is_dep,per_info = build_per_info etype c gls in + let ek = + if is_dep then + EK_dep (start_tree env per_info.per_ind) + else EK_unknown in + tcl_change_info + {info with + pm_stack= + Per(etype,per_info,ek,[])::info.pm_stack} gls + | Virtual cut -> + assert (cut.cut_stat.st_label=Anonymous); + let id = pf_get_new_id (id_of_string "_matched") gls in + let c = mkVar id in + let modified_cut = + {cut with cut_stat={cut.cut_stat with st_label=Name id}} in + tclTHEN + (instr_cut (fun _ c -> c) false false modified_cut) + (fun gls0 -> + let is_dep,per_info = build_per_info etype c gls0 in + assert (not is_dep); + tcl_change_info + {info with pm_stack= + Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) + gls + +(* suppose *) + +let rec build_product args body = + match args with + (Hprop st| Hvar st )::rest -> + let pprod= lift 1 (build_product rest body) in + let lbody = + match st.st_label with + Anonymous -> body + | Name id -> subst_term (mkVar id) pprod in + mkProd (st.st_label, st.st_it, lbody) + | [] -> body + +let register_nodep_subcase id= function + Per(et,pi,ek,clauses)::s -> + begin + match ek with + EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." + end + | _ -> anomaly "wrong stack state" + +let suppose_tac hyps gls0 = + let info = get_its_info gls0 in + let thesis = get_thesis gls0 in + let id = pf_get_new_id (id_of_string "_subcase") gls0 in + let clause = build_product hyps thesis in + let ninfo1 = {info with + pm_stack=Suppose_case::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,clause]} in + let old_clauses,stack = register_nodep_subcase id info.pm_stack in + let ninfo2 = {info with + pm_stack=stack} in + tclTHENS (internal_cut id clause) + [tclTHENLIST [tcl_change_info ninfo1; + assume_tac hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* suppose it is ... *) + +(* pattern matching compiling *) + +let rec nb_prod_after n c= + match kind_of_term c with + | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else + 1+(nb_prod_after 0 b) + | _ -> 0 + +let constructor_arities env ind = + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let constr_types = Inductiveops.arities_of_constructors env ind in + let hyp = nb_prod_after nparams in + Array.map hyp constr_types + +let rec n_push rest ids n = + if n<=0 then Pop rest else Push (ids,n_push rest ids (pred n)) + +let explode_branches ids env ind rest= + Array.map (fun n -> Some (Idset.empty,n_push rest ids n)) (constructor_arities env ind) + +let rec tree_of_pats env ((id,_) as cpl) pats = + match pats with + [] -> End_of_branch cpl + | args::stack -> + match args with + [] -> Pop (tree_of_pats env cpl stack) + | patt :: rest_args -> + match patt with + PatVar (_,v) -> + Push (Idset.singleton id, + tree_of_pats env cpl (rest_args::stack)) + | PatCstr (_,(ind,cnum),args,nam) -> + let _,mind = Inductive.lookup_mind_specif env ind in + let br= Array.map (fun _ -> None) mind.mind_consnames in + br.(pred cnum) <- + Some (Idset.singleton id, + tree_of_pats env cpl (args::rest_args::stack)); + Split(Idset.empty,ind,br) + +let rec add_branch env ((id,_) as cpl) pats tree= + match pats with + [] -> + begin + match tree with + End_of_branch cpl0 -> End_of_branch cpl0 + (* this ensures precedence *) + | _ -> anomaly "tree is expected to end here" + end + | args::stack -> + match args with + [] -> + begin + match tree with + Pop t -> Pop (add_branch env cpl stack t) + | _ -> anomaly "we should pop here" + end + | patt :: rest_args -> + match patt with + PatVar (_,v) -> + begin + match tree with + Push (ids,t) -> + Push (Idset.add id ids, + add_branch env cpl (rest_args::stack) t) + | Split (ids,ind,br) -> + Split (Idset.add id ids, + ind,array_map2 + (append_branch env cpl 1 + (rest_args::stack)) + (constructor_arities env ind) br) + | _ -> anomaly "No pop/stop expected here" + end + | PatCstr (_,(ind,cnum),args,nam) -> + match tree with + Push (ids,t) -> + let br = explode_branches ids env ind t in + let _ = + br.(pred cnum)<- + option_map + (fun (ids,tree) -> + Idset.add id ids, + add_branch env cpl + (args::rest_args::stack) tree) + br.(pred cnum) in + Split (ids,ind,br) + | Split (ids,ind0,br0) -> + if (ind <> ind0) then error + (* this can happen with coercions *) + "Case pattern belongs to wrong inductive type"; + let br=Array.copy br0 in + let ca = constructor_arities env ind in + let _= br.(pred cnum)<- + append_branch env cpl 0 (args::rest_args::stack) + ca.(pred cnum) br.(pred cnum) in + Split (ids,ind,br) + | _ -> anomaly "No pop/stop expected here" +and append_branch env ((id,_) as cpl) depth pats nargs = function + Some (ids,tree) -> + Some (Idset.add id ids,append_tree env cpl depth pats tree) + | None -> + Some (* (n_push (tree_of_pats env cpl pats) + (Idset.singleton id) nargs) *) + (Idset.singleton id,tree_of_pats env cpl pats) +and append_tree env ((id,_) as cpl) depth pats tree = + if depth<=0 then add_branch env cpl pats tree + else match tree with + Pop t -> Pop (append_tree env cpl (pred depth) pats t) + | Push (ids,t) -> Push (Idset.add id ids, + append_tree env cpl depth pats t) + | End_of_branch _ -> anomaly "Premature end of branch" + | Split (ids,ind,branches) -> + Split (Idset.add id ids,ind, + array_map2 + (append_branch env cpl (succ depth) pats) + (constructor_arities env ind) + branches) + +(* suppose it is *) + +let rec st_assoc id = function + [] -> raise Not_found + | st::_ when st.st_label = id -> st.st_it + | _ :: rest -> st_assoc id rest + +let thesis_for obj typ per_info env= + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + let ind = destInd cind in + let _ = if ind <> per_info.per_ind then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str "cannot give an induction hypothesis (wrong inductive type)") in + let params,args = list_chop per_info.per_nparams all_args in + let _ = if not (List.for_all2 eq_constr params per_info.per_params) then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str "cannot give an induction hypothesis (wrong parameters)") in + let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in + compose_prod rc (whd_beta hd2) + +let rec build_product_dep pat_info per_info args body gls = + match args with + (Hprop {st_label=nam;st_it=This c} + | Hvar {st_label=nam;st_it=c})::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match nam with + Anonymous -> body + | Name id -> subst_var id pprod in + mkProd (nam,c,lbody) + | Hprop ({st_it=Thesis tk} as st)::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match st.st_label with + Anonymous -> body + | Name id -> subst_var id pprod in + let ptyp = + match tk with + For id -> + let obj = mkVar id in + let typ = + try st_assoc (Name id) pat_info.pat_vars + with Not_found -> + snd (st_assoc (Name id) pat_info.pat_aliases) in + thesis_for obj typ per_info (pf_env gls) + | Plain -> get_thesis gls + | Sub n -> anomaly "Subthesis in cases" in + mkProd (st.st_label,ptyp,lbody) + | [] -> body + +let build_dep_clause params pat_info per_info hyps gls = + let concl= + thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in + let open_clause = + build_product_dep pat_info per_info hyps concl gls in + let prod_one st body = + match st.st_label with + Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body) + | Name id -> mkNamedProd id st.st_it (lift 1 body) in + let let_one_in st body = + match st.st_label with + Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body) + | Name id -> + mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in + let aliased_clause = + List.fold_right let_one_in pat_info.pat_aliases open_clause in + List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause + +let rec register_dep_subcase id env per_info pat = function + EK_nodep -> error "Only \"suppose it is\" can be used here." + | EK_unknown -> + register_dep_subcase id env per_info pat + (EK_dep (start_tree env per_info.per_ind)) + | EK_dep tree -> EK_dep (add_branch env id [[pat]] tree) + +let case_tac params pat_info hyps gls0 = + let info = get_its_info gls0 in + let id = pf_get_new_id (id_of_string "_subcase") gls0 in + let et,per_info,ek,old_clauses,rest = + match info.pm_stack with + Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) + | _ -> anomaly "wrong place for cases" in + let clause = build_dep_clause params pat_info per_info hyps gls0 in + let ninfo1 = {info with + pm_stack=Suppose_case::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,clause]} in + let nek = + register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info + pat_info.pat_pat ek in + let ninfo2 = {info with + pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in + tclTHENS (internal_cut id clause) + [tclTHENLIST + [tcl_change_info ninfo1; + assume_st (params@pat_info.pat_vars); + assume_st_letin pat_info.pat_aliases; + assume_hyps_or_theses hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* end cases *) + +type instance_stack = + (constr option*bool*(constr list) list) list + +let initial_instance_stack ids = + List.map (fun id -> id,[None,false,[]]) ids + +let push_one_arg arg = function + [] -> anomaly "impossible" + | (head,is_rec,args) :: ctx -> + ((head,is_rec,(arg::args)) :: ctx) + +let push_arg arg stacks = + List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks + + +let push_one_head c is_rec ids (id,stack) = + let head = if Idset.mem id ids then Some c else None in + id,(head,is_rec,[]) :: stack + +let push_head c is_rec ids stacks = + List.map (push_one_head c is_rec ids) stacks + +let pop_one rec_flag (id,stack) = + let nstack= + match stack with + [] -> anomaly "impossible" + | [c] as l -> l + | (Some head,is_rec,args)::(head0,is_rec0,args0)::ctx -> + let arg = applist (head,(List.rev args)) in + rec_flag:= !rec_flag || is_rec; + (head0,is_rec0,(arg::args0))::ctx + | (None,is_rec,args)::(head0,is_rec0,args0)::ctx -> + rec_flag:= !rec_flag || is_rec; + (head0,is_rec0,(args@args0))::ctx + in id,nstack + +let pop_stacks stacks = + let rec_flag= ref false in + let nstacks = List.map (pop_one rec_flag) stacks in + !rec_flag , nstacks + +let patvar_base = id_of_string "__" + +let test_fun (str:string) = () + +let hrec_for obj_id fix_id per_info gls= + let obj=mkVar obj_id in + let typ=pf_get_hyp_typ gls obj_id in + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + match kind_of_term cind with + Ind ind when ind=per_info.per_ind -> + let params,args= list_chop per_info.per_nparams all_args in + if try + (List.for_all2 eq_constr params per_info.per_params) + with Invalid_argument _ -> false then + let hd2 = applist (mkVar fix_id,args@[obj]) in + Some (compose_lam rc (whd_beta hd2)) + else None + | _ -> None + +let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = + match tree with + Pop t -> + let is_rec,nstacks = pop_stacks stacks in + if is_rec then + let _ = test_fun "is_rec=true" in + let c_id = pf_get_new_id (id_of_string "_hrec") gls in + tclTHEN + (intro_mustbe_force c_id) + (execute_cases false fix_name per_info kont0 nstacks t) gls + else + execute_cases false fix_name per_info kont0 nstacks t gls + | Push (_,t) -> + let id = pf_get_new_id patvar_base gls in + let nstacks = push_arg (mkVar id) stacks in + let kont = execute_cases false fix_name per_info kont0 nstacks t in + tclTHEN + (intro_mustbe_force id) + begin + match fix_name with + Anonymous -> kont + | Name fix_id -> + (fun gls -> + if at_top then + kont gls + else + match hrec_for id fix_id per_info gls with + None -> kont gls + | Some c_obj -> + let c_id = + pf_get_new_id (id_of_string "_hrec") gls in + tclTHENLIST + [generalize [c_obj]; + intro_mustbe_force c_id; + kont] gls) + end gls + | Split(ids,ind,br) -> + let (_,typ,_)=destProd (pf_concl gls) in + let hd,args=decompose_app (special_whd gls typ) in + let _ = assert (ind = destInd hd) in + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let params = list_firstn nparams args in + let constr i =applist (mkConstruct(ind,succ i),params) in + let next_tac is_rec i = function + Some (sub_ids,tree) -> + let br_stacks = + List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in + let p_stacks = + push_head (constr i) is_rec ids br_stacks in + execute_cases false fix_name per_info kont0 p_stacks tree + | None -> + msgnl (str "Warning : missing case"); + kont0 (mkMeta 1) + in + let id = pf_get_new_id patvar_base gls in + let kont is_rec = + tclTHENSV + (general_case_analysis (mkVar id,NoBindings)) + (Array.mapi (next_tac is_rec) br) in + tclTHEN + (intro_mustbe_force id) + begin + match fix_name with + Anonymous -> kont false + | Name fix_id -> + (fun gls -> + if at_top then + kont false gls + else + match hrec_for id fix_id per_info gls with + None -> kont false gls + | Some c_obj -> + tclTHENLIST + [generalize [c_obj]; + kont true] gls) + end gls + | End_of_branch (id,nhyps) -> + match List.assoc id stacks with + [None,_,args] -> + let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in + kont0 (applist (mkVar id,List.rev_append args metas)) gls + | _ -> anomaly "wrong stack size" + +let end_tac et2 gls = + let info = get_its_info gls in + let et1,pi,ek,clauses = + match info.pm_stack with + Suppose_case::_ -> + anomaly "This case should already be trapped" + | Claim::_ -> + error "\"end claim\" expected." + | Focus_claim::_ -> + error "\"end focus\" expected." + | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) + | [] -> + anomaly "This case should already be trapped" in + let et = + if et1 <> et2 then + match et1 with + ET_Case_analysis -> + error "\"end cases\" expected." + | ET_Induction -> + error "\"end induction\" expected." + else et1 in + tclTHEN + tcl_erase_info + begin + match et,ek with + _,EK_unknown -> + tclSOLVE [simplest_elim pi.per_casee] + | ET_Case_analysis,EK_nodep -> + tclTHEN + (general_case_analysis (pi.per_casee,NoBindings)) + (default_justification (List.map mkVar clauses)) + | ET_Induction,EK_nodep -> + tclTHENLIST + [generalize (pi.per_args@[pi.per_casee]); + simple_induct (AnonHyp (succ (List.length pi.per_args))); + default_justification (List.map mkVar clauses)] + | ET_Case_analysis,EK_dep tree -> + tclTHENLIST + [generalize (pi.per_args@[pi.per_casee]); + execute_cases true Anonymous pi + (fun c -> tclTHENLIST + [refine c; + clear clauses; + justification assumption]) + (initial_instance_stack clauses) tree] + | ET_Induction,EK_dep tree -> + tclTHEN (generalize (pi.per_args@[pi.per_casee])) + begin + fun gls0 -> + let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in + tclTHEN + (fix (Some fix_id) (succ (List.length pi.per_args))) + (execute_cases true (Name fix_id) pi + (fun c -> + tclTHENLIST + [clear [fix_id]; + refine c; + clear clauses; + justification assumption + (* justification automation_tac *)]) + (initial_instance_stack clauses) tree) gls0 + end + end gls + +(* escape *) + +let rec abstract_metas n avoid head = function + [] -> 1,head,[] + | (meta,typ)::rest -> + let id = Nameops.next_ident_away (id_of_string "_sbgl") avoid in + let p,term,args = abstract_metas (succ n) (id::avoid) head rest in + succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term), + (mkMeta n)::args + +let build_refining_context gls = + let info = get_its_info gls in + let avoid=pf_ids_of_hyps gls in + let _,fn,args=abstract_metas 1 avoid info.pm_partial_goal info.pm_subgoals in + applist (fn,args) + +let escape_command pts = + let pts1 = nth_unproven 1 pts in + let gls = top_goal_of_pftreestate pts1 in + let term = build_refining_context gls in + let tac = tclTHEN + (abstract_operation (Proof_instr (true,{emph=0;instr=Pescape})) tcl_erase_info) + (Tactics.refine term) in + traverse 1 (solve_pftreestate tac pts1) + +(* General instruction engine *) + +let rec do_proof_instr_gen _thus _then instr = + match instr with + Pthus i -> + assert (not _thus); + do_proof_instr_gen true _then i + | Pthen i -> + assert (not _then); + do_proof_instr_gen _thus true i + | Phence i -> + assert (not (_then || _thus)); + do_proof_instr_gen true true i + | Pcut c -> + instr_cut mk_stat_or_thesis _thus _then c + | Prew (s,c) -> + assert (not _then); + instr_rew _thus s c + | Pconsider (c,hyps) -> consider_tac c hyps + | Pgiven hyps -> given_tac hyps + | Passume hyps -> assume_tac hyps + | Plet hyps -> assume_tac hyps + | Pclaim st -> instr_claim false st + | Pfocus st -> instr_claim true st + | Ptake witl -> take_tac witl + | Pdefine (id,args,body) -> define_tac id args body + | Pcast (id,typ) -> cast_tac id typ + | Pper (et,cs) -> per_tac et cs + | Psuppose hyps -> suppose_tac hyps + | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps + | Pend (B_elim et) -> end_tac et + | Pend _ | Pescape -> anomaly "Not applicable" + +let eval_instr {instr=instr} = + do_proof_instr_gen false false instr + +let rec preprocess pts instr = + match instr with + Phence i |Pthus i | Pthen i -> preprocess pts i + | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ + | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ + | Pdefine (_,_,_) | Pper _ | Prew _ -> + check_not_per pts; + true,pts + | Pescape -> + check_not_per pts; + false,pts + | Pcase _ | Psuppose _ | Pend (B_elim _) -> + true,close_previous_case pts + | Pend bt -> + false,close_block bt pts + +let rec postprocess pts instr = + match instr with + Phence i | Pthus i | Pthen i -> postprocess pts i + | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) + | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts + | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts + | Pescape -> + escape_command pts + | Pend _ -> + goto_current_focus_or_top (mark_as_done pts) + +let do_instr raw_instr pts = + let has_tactic,pts1 = preprocess pts raw_instr.instr in + let pts2 = + if has_tactic then + let gl = nth_goal_of_pftreestate 1 pts1 in + let env= pf_env gl in + let sigma= project gl in + let ist = {ltacvars = ([],[]); ltacrecvars = []; + gsigma = sigma; genv = env} in + let glob_instr = intern_proof_instr ist raw_instr in + let instr = + interp_proof_instr (get_its_info gl) sigma env glob_instr in + let lock_focus = is_focussing_instr instr.instr in + let marker= Proof_instr (lock_focus,instr) in + solve_nth_pftreestate 1 + (abstract_operation marker (eval_instr instr)) pts1 + else pts1 in + postprocess pts2 raw_instr.instr + +let proof_instr raw_instr = + Pfedit.mutate (do_instr raw_instr) + +(* + +(* STUFF FOR ITERATED RELATIONS *) +let decompose_bin_app t= + let hd,args = destApp + +let identify_transitivity_lemma c = + let varx,tx,c1 = destProd c in + let vary,ty,c2 = destProd (pop c1) in + let varz,tz,c3 = destProd (pop c2) in + let _,p1,c4 = destProd (pop c3) in + let _,lp2,lp3 = destProd (pop c4) in + let p2=pop lp2 in + let p3=pop lp3 in +*) + |