diff options
| -rw-r--r-- | tactics/tacticals.ml | 4 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1694 | ||||
| -rw-r--r-- | tactics/tactics.mli | 244 |
4 files changed, 1942 insertions, 3 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 1794755ff..56cd5a42f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -413,7 +413,7 @@ let make_elim_branch_assumptions ba gl = | (_, _) -> error "make_elim_branch_assumptions" in makerec ([],[],[],[],[]) ba.branchsign - (try firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl)) + (try list_firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl)) with Failure _ -> anomaly "make_elim_branch_assumptions") let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl @@ -441,7 +441,7 @@ let make_case_branch_assumptions ba gl = | (_, _) -> error "make_case_branch_assumptions" in makerec ([],[],[],[]) ba.branchsign - (try firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl)) + (try list_firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl)) with Failure _ -> anomaly "make_case_branch_assumptions") let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 1ebd64f43..216a24b31 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -101,7 +101,8 @@ type branch_assumptions = { val sort_of_goal : goal sigma -> sorts val suff : goal sigma -> constr -> string -val lookup_eliminator : context -> section_path -> string -> constr +val lookup_eliminator : + typed_type signature -> section_path -> string -> constr val general_elim_then_using : constr -> (constr -> int -> bool list) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml new file mode 100644 index 000000000..8bf647a69 --- /dev/null +++ b/tactics/tactics.ml @@ -0,0 +1,1694 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Sign +open Generic +open Term +open Inductive +open Reduction +open Environ +open Evd +open Pfedit +open Tacred +open Tacmach +open Proof_trees +open Logic +open Clenv +open Tacticals +open Pattern + +exception Bound + +(*********************************************) +(* Tactics *) +(*********************************************) + +(****************************************) +(* General functions *) +(****************************************) + +let get_pairs_from_bindings = + let pair_from_binding = function + | [(Bindings binds)] -> binds + | _ -> error "not a binding list!" + in + List.map pair_from_binding + +let get_commands = + let command_from_tacarg = function + | (Command x) -> x + | _ -> error "get_commands: not a command!" + in + List.map command_from_tacarg + +let rec string_head_bound = function + | DOPN(Const _,_) as x -> + string_of_id (basename (path_of_const x)) + | DOPN(MutInd _,_) as x -> + let mispec = Global.lookup_mind_specif x in + string_of_id (mis_typename mispec) + | DOPN(MutConstruct ((sp,tyi),i),_) -> + let mib = Global.lookup_mind sp in + string_of_id (mib.mind_packets.(tyi).mind_consnames.(i-1)) + | VAR id -> string_of_id id + | _ -> raise Bound + +let string_head c = + try string_head_bound c with Bound -> error "Bound head variable" + +let rec head_constr_bound t l = + let t = strip_outer_cast(collapse_appl t) in + match t with + | DOP2(Prod,_,DLAM(_,c2)) -> head_constr_bound c2 l + | DOPN(AppL,cl) -> + head_constr_bound (array_hd cl) ((List.tl (Array.to_list cl))@l) + | DOPN(Const _,_) as x -> x::l + | DOPN(MutInd _,_) as x -> x::l + | DOPN(MutConstruct _,_) as x -> x::l + | VAR _ as x -> x::l + | _ -> raise Bound + +let head_constr c = + try head_constr_bound c [] with Bound -> error "Bound head variable" + +let bad_tactic_args s l = + raise (RefinerError (BadTacticArgs (s,l))) + +(******************************************) +(* Primitive tactics *) +(******************************************) + +let introduction = Tacmach.introduction +let intro_replacing = Tacmach.intro_replacing +let refine = Tacmach.refine +let convert_concl = Tacmach.convert_concl +let convert_hyp = Tacmach.convert_hyp +let thin = Tacmach.thin +let move_hyp = Tacmach.move_hyp + +let mutual_fix = Tacmach.mutual_fix +let fix f n = mutual_fix [f] [n] [] + +let fix_noname n = + let l = Pfedit.list_proofs() in + let id = id_of_string (List.hd l) in + fix id n + +(***TODO: les versions dyn_ +let dyn_mutual_fix argsl gl = + match argsl with + | [Integer n] -> fix_noname n gl + | [Identifier id;Integer n] -> fix id n gl + | ((Identifier id)::(Integer n)::lfix) -> + let rec decomp lid ln lar = function + | (Fixexp (id,n,ar)::rest) -> + decomp (id::lid) (n::ln) (ar::lar) rest + | [] -> (List.rev lid,List.rev ln,List.rev lar) + | _ -> bad_tactic_args "mutual_fix" argsl + in + let (lid,ln,lar) = decomp [] [] [] lfix in + mutual_fix (id::lid) (n::ln) (List.map (pf_constr_of_com gl) lar) gl + | l -> bad_tactic_args "mutual_fix" l +***) + +let mutual_cofix = Tacmach.mutual_cofix +let cofix f = mutual_cofix [f] [] + +let cofix_noname n = + let l = Pfedit.list_proofs() in + let id = id_of_string (List.hd l) in + cofix id n + +(***TODO +let dyn_mutual_cofix argsl gl = + match argsl with + | [] -> cofix_noname gl + | [(Identifier id)] -> cofix id gl + | ((Identifier id)::lcofix) -> + let rec decomp lid lar = function + | (Cofixexp (id,ar)::rest) -> + decomp (id::lid) (ar::lar) rest + | [] -> (List.rev lid,List.rev lar) + | _ -> bad_tactic_args "mutual_cofix" argsl + in + let (lid,lar) = decomp [] [] lcofix in + mutual_cofix (id::lid) (List.map (pf_constr_of_com gl) lar) gl + | l -> bad_tactic_args "mutual_cofix" l +***) + +(**************************************************************) +(* Reduction and conversion tactics *) +(**************************************************************) + +(* The following two tactics apply an arbitrary + reduction function either to the conclusion or to a + certain hypothesis *) + +let reduct_in_concl redfun gl = + convert_concl (pf_reduce redfun gl (pf_concl gl)) gl + +let reduct_in_hyp redfun id gl = + let ty = pf_get_hyp gl id in + let redfun' = under_casts (fun _ _ -> pf_reduce redfun gl) in + convert_hyp id (redfun' (pf_env gl) (project gl) ty) gl + +let reduct_option redfun = function + | Some id -> reduct_in_hyp redfun id + | None -> reduct_in_concl redfun + +(* The following tactic determines whether the reduction + function has to be applied to the conclusion or + to the hypotheses. *) + +let in_combinator tac1 tac2 = function + | [] -> tac1 + | x -> (tclMAP tac2 x) + +let redin_combinator redfun = function + | [] -> reduct_in_concl redfun + | x -> (tclMAP (reduct_in_hyp redfun) x) + + +(* Now we introduce different instances of the previous tacticals *) +let change_hyp_and_check t env sigma c = + if is_conv (Global.unsafe_env()) sigma t c then + t + else + errorlabstrm "convert-check-hyp" [< 'sTR "Not convertible" >] + +let change_concl_and_check t env sigma c = + if is_conv_leq (Global.unsafe_env()) sigma t c then + t + else + errorlabstrm "convert-check-concl" [< 'sTR "Not convertible" >] + +let change_in_concl t = reduct_in_concl (change_concl_and_check t) +let change_in_hyp t = reduct_in_hyp (change_hyp_and_check t) + +let change_option t = function + | Some id -> reduct_in_hyp (change_hyp_and_check t) id + | None -> reduct_in_concl (change_concl_and_check t) + +(* Pour usage interne (le niveau User est pris en compte par dyn_reduce) *) +let red_in_concl = reduct_in_concl red_product +let red_in_hyp = reduct_in_hyp red_product +let red_option = reduct_option red_product +let hnf_in_concl = reduct_in_concl hnf_constr +let hnf_in_hyp = reduct_in_hyp hnf_constr +let hnf_option = reduct_option hnf_constr +let simpl_in_concl = reduct_in_concl nf +let simpl_in_hyp = reduct_in_hyp nf +let simpl_option = reduct_option nf +let normalise_in_concl = reduct_in_concl compute +let normalise_in_hyp = reduct_in_hyp compute +let normalise_option = reduct_option compute +let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname) +let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) +let unfold_option loccname = reduct_option (unfoldn loccname) +let pattern_option l = reduct_option (pattern_occs l) + +(*** +let dyn_change = function + | [Command (com); Clause cl] -> + (fun goal -> + let c = constr_of_com_sort (project goal) (pf_hyps goal) com in + in_combinator (change_in_concl c) (change_in_hyp c) cl goal) + | l -> bad_tactic_args "change" l +***) + +(* A function which reduces accordingly to a reduction expression, + as the command Eval does. *) + +let reduce redexp cl goal = + redin_combinator (reduction_of_redexp redexp) cl goal + +(*** +let dyn_reduce = function + | [Redexp (redn,args); Clause cl] -> + (fun goal -> + let redexp = + redexp_of_ast (project goal) (pf_hyps goal) (redn,args) in + reduce redexp cl goal) + | l -> bad_tactic_args "reduce" l +***) + +(* Unfolding occurrences of a constant *) + +let unfold_constr c = + match strip_outer_cast c with + | DOPN(Const(sp),_) -> + unfold_in_concl [[],sp] + | t -> + errorlabstrm "unfold_constr" + [< 'sTR "Cannot unfold a non-constant." >] + +(*******************************************) +(* Introduction tactics *) +(*******************************************) + +let next_global_ident_from id avoid = + let rec next_rec id = + let id = next_ident_away_from id avoid in + if not (Declare.is_global id) then + id + else + next_rec (lift_ident id) + in + next_rec id + +let next_global_ident_away id avoid = + let id = next_ident_away id avoid in + if not (Declare.is_global id) then + id + else + next_global_ident_from (lift_ident id) avoid + +let fresh_id avoid id gl = + next_global_ident_away id (avoid@(ids_of_sign (pf_untyped_hyps gl))) + +let id_of_name_with_default s = function + | Anonymous -> id_of_string s + | Name id -> id + +let default_id gl = + match strip_outer_cast (pf_concl gl) with + | DOP2(Prod,c1,DLAM(name,c2)) -> + (match pf_whd_betadeltaiota gl (pf_type_of gl c1) with + | DOP0(Sort(Prop _)) -> (id_of_name_with_default "H" name) + | DOP0(Sort(Type(_))) -> (id_of_name_with_default "X" name) + | _ -> anomaly "Wrong sort") + | _ -> error "Introduction needs a product" + +(* Non primitive introduction tactics are treated by central_intro + There is possibly renaming, with possibly names to avoid and + possibly a move to do after the introduction *) + +type intro_name_flag = + | IAvoid of identifier list + | IBasedOn of identifier * identifier list + | IMustBe of identifier + +let rec central_intro name_flag move_flag force_flag gl = + try + let id = + match name_flag with + | IAvoid idl -> fresh_id idl (default_id gl) gl + | IBasedOn (id,idl) -> fresh_id idl id gl + | IMustBe id -> + let id' = fresh_id [] id gl in + if id' <> id then warning + ((string_of_id id)^ + " is already used; changed to "^(string_of_id id')); + id' + in + begin match move_flag with + | None -> introduction id gl + | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) gl + end + with (UserError ("Introduction needs a product",_)) as e -> + if force_flag then + try + ((tclTHEN (reduce Red []) (central_intro name_flag move_flag + force_flag)) gl) + with UserError ("Term not reducible",_) -> + errorlabstrm "Intro" + [<'sTR "No product even after head-reduction">] + else + raise e + +let intro_using_warning id = central_intro (IMustBe id) None false +let intro_using id = central_intro (IBasedOn (id,[])) None false +let intro_force force_flag = central_intro (IAvoid []) None force_flag +let intro = intro_force false +let introf = intro_force true + +(**** Multiple introduction tactics ****) + +let rec intros_using = function + [] -> tclIDTAC + | str::l -> tclTHEN (intro_using str) (intros_using l) + +let intros = tclREPEAT (intro_force false) + +let intro_erasing id = tclTHEN (thin [id]) (intro_using id) + +(* User-level introduction tactics *) + +let dyn_intro = function + | [] -> central_intro (IAvoid []) None true + | [Identifier id] -> central_intro (IMustBe id) None true + | l -> bad_tactic_args "intro" l + +let dyn_intro_move = function + | [Identifier id2] -> central_intro (IAvoid []) (Some id2) true + | [Identifier id; Identifier id2] -> + central_intro (IMustBe id) (Some id2) true + | l -> bad_tactic_args "intro_move" l + +let rec intros_until s g = + match pf_lookup_name_as_renamed (pf_hyps g) (pf_concl g) s with + | Some depth -> tclDO depth intro g + | None -> + try + ((tclTHEN (reduce Red []) (intros_until s)) g) + with UserError ("Term not reducible",_) -> + errorlabstrm "Intros" + [<'sTR "No such hypothesis in current goal"; + 'sTR "even after head-reduction" >] + +let rec intros_until_n n g = + match pf_lookup_index_as_renamed (pf_concl g) n with + | Some depth -> tclDO depth intro g + | None -> + try + ((tclTHEN (reduce Red []) (intros_until_n n)) g) + with UserError ("Term not reducible",_) -> + errorlabstrm "Intros" + [<'sTR "No such hypothesis in current goal"; + 'sTR "even after head-reduction" >] + +let dyn_intros_until = function + | [Identifier id] -> intros_until id + | [Integer n] -> intros_until_n n + | l -> bad_tactic_args "Intros until" l + +let intros_do n g = + let depth = + let rec lookup all nodep = function + | DOP2(Prod,_,DLAM(name,c')) -> + (match name with + | Name(s') -> + if dependent (Rel 1) c' then + lookup (all+1) nodep c' + else if nodep = n then + all + else + lookup (all+1) (nodep+1) c' + | Anonymous -> + if nodep=n then all else lookup (all+1) (nodep+1) c') + | DOP2(Cast,c,_) -> lookup all nodep c + | _ -> error "No such hypothesis in current goal" + in + lookup 1 1 (pf_concl g) + in + tclDO depth intro g + +let rec intros_move = function + | [] -> tclIDTAC + | (hyp,destopt) :: rest -> + tclTHEN (central_intro (IMustBe hyp) destopt false) + (intros_move rest) + +let move_to_rhyp rhyp gl = + let rec get_lhyp lastfixed deptyp = function + | [] -> + (match rhyp with + | None -> lastfixed + | Some h -> anomaly ("Hypothesis should occur: "^ (string_of_id h))) + | (hyp,typ) as ht :: rest -> + if Some hyp = rhyp then + lastfixed + else if List.exists (occur_var hyp) deptyp then + get_lhyp lastfixed (typ::deptyp) rest + else + get_lhyp (Some hyp) deptyp rest + in + let sign = pf_untyped_hyps gl in + let (hyp,typ) = hd_sign sign in + match get_lhyp None [typ] (list_of_sign sign) with + | None -> tclIDTAC gl + | Some hypto -> move_hyp true hyp hypto gl + +let rec intros_rmove = function + | [] -> tclIDTAC + | (hyp,destopt) :: rest -> + tclTHENLIST [ introduction hyp; + move_to_rhyp destopt; + intros_rmove rest ] + +(****************************************************) +(* Resolution tactics *) +(****************************************************) + +(* Refinement tactic: unification with the head of the head normal form + * of the type of a term. *) + +let apply_type hdcty argl gl = + refine (DOPN(AppL,Array.of_list + ((DOP2(Cast,DOP0(Meta(newMETA())),hdcty))::argl))) gl + +let apply_term hdc argl gl = + refine (DOPN(AppL,Array.of_list(hdc::argl))) gl + +let bring_hyps clsl gl = + let ids = + List.map + (function + | (Some id) -> id + | None -> error "BringHyps") clsl in + let newcl = + List.fold_right + (fun id cl' -> mkNamedProd id (pf_type_of gl (VAR id)) cl') + ids (pf_concl gl) + in + apply_type newcl (List.map (fun id -> VAR id) ids) gl + +(* Resolution with missing arguments *) + +let collect_com lbind = + map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind + +let make_clenv_binding_apply wc (c,t) lbind = + let largs = collect_com lbind in + let lcomargs = List.length largs in + if lcomargs = List.length lbind then + let clause = mk_clenv_from wc (c,t) in + clenv_constrain_missing_args largs clause + else if lcomargs = 0 then + let clause = mk_clenv_rename_from wc (c,t) in + clenv_match_args lbind clause + else + errorlabstrm "make_clenv_bindings" + [<'sTR "Cannot mix bindings and free associations">] + +let apply_with_bindings (c,lbind) gl = + let (wc,kONT) = startWalk gl in + let t = w_hnf_constr wc (w_type_of wc c) in + let clause = make_clenv_binding_apply wc (c,t) lbind in + let apply = + match c with + | DOP2(Lambda,_,_) -> res_pf_cast + | _ -> res_pf + in + apply kONT clause gl + +let apply c = apply_with_bindings (c,[]) +let apply_com = tactic_com (fun c -> apply_with_bindings (c,[])) + +let apply_list = function + | c::l -> apply_with_bindings (c,List.map (fun com ->(Com,com)) l) + | _ -> assert false + +(* Resolution with no reduction on the type *) + +let apply_without_reduce c gl = + let (wc,kONT) = startWalk gl in + let clause = mk_clenv_type_of wc c in + res_pf kONT clause gl + +let apply_without_reduce_com = tactic_com apply_without_reduce + +let refinew_scheme kONT clause gl = res_pf kONT clause gl + +let dyn_apply l = + match l with + | [Command com; BINDINGS binds] -> + tactic_com_bind_list apply_with_bindings (com,binds) + | [CONSTR c; CBINDINGS binds] -> + apply_with_bindings (c,binds) + | l -> + bad_tactic_args "apply" l + +(* A useful resolution tactic, equivalent to Cut type_of_c;[Idtac|Apply c] *) + +let cut_and_apply c gl = + let goal_constr = pf_concl gl in + match (pf_hnf_constr gl (pf_type_of gl c)) with + | DOP2(Prod,c1,DLAM(_,c2)) when not (dependent (Rel 1) c2) -> + tclTHENS + (apply_type (DOP2(Prod,c2,DLAM(Anonymous,goal_constr))) + [DOP0(Meta(newMETA()))]) + [tclIDTAC;apply_term c [DOP0(Meta(newMETA()))]] gl + | _ -> error "Imp_elim needs a non-dependent product" + +let dyn_cut_and_apply = function + | [Command com] -> tactic_com cut_and_apply com + | [Constr c] -> cut_and_apply c + | l -> bad_tactic_args "cut_and_apply" l + +(**************************) +(* Cut tactics *) +(**************************) + +let cut c gl = + match hnf_type_of gl c with + | (DOP0(Sort _)) -> + apply_type (DOP2(Prod,c,DLAM(Anonymous,(pf_concl gl)))) + [DOP0(Meta (newMETA()))] gl + | _ -> error "Not a proposition or a type" + +let dyn_cut = function + | [Command com] -> tactic_com_sort cut com + | [Constr c] -> cut c + | l -> bad_tactic_args "cut" l + +let cut_intro t = (tclTHENS (cut t) [intro;tclIDTAC]) + +let cut_replacing id t = + (tclTHENS (cut t) + [(tclORELSE (intro_replacing id) + (tclORELSE (intro_erasing id) + (intro_using id))); + tclIDTAC]) + +let cut_in_parallel l = + let rec prec = function + | [] -> tclIDTAC + | h::t -> (tclTHENS (cut h) ([prec t;tclIDTAC])) + in + prec (List.rev l) + +(**************************) +(* Generalize tactics *) +(**************************) + +let generalize_goal gl c cl = + let t = pf_type_of gl c in + match c with + | (VAR id) -> mkNamedProd id t cl + | _ -> + let cl' = subst_term c cl in + if noccurn 1 cl' then + DOP2(Prod,t,DLAM(Anonymous,cl)) + (* On ne se casse pas la tete : on prend pour nom de variable + la premiere lettre du type, meme si "ci" est une + constante et qu'on pourrait prendre directement son nom *) + else + prod_name (Anonymous, t, cl') + +let generalize_dep c gl = + let sign = pf_untyped_hyps gl in + let init_ids = ids_of_sign (initial_sign ()) in + let rec seek ((hl,tl) as toquant) h t = + if List.exists (fun id -> occur_var id t) hl or dependent c t then + (h::hl,t::tl) + else + toquant + in + let (hl,tl) = it_sign seek ([],[]) sign in + let tothin = filter (fun id -> not (List.mem id init_ids)) hl in + let tothin' = + match c with + | VAR id when mem_sign sign id & not (List.mem id init_ids) -> id::tothin + | _ -> tothin + in + let cl' = List.fold_right2 mkNamedProd hl tl (pf_concl gl) in + let cl'' = generalize_goal gl c cl' in + tclTHEN + (apply_type cl'' (c::(List.map (fun id -> VAR id) hl))) + (thin (List.rev tothin')) + gl + +let generalize lconstr gl = + let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in + apply_type newcl lconstr gl + +let dyn_generalize = + fun argsl -> tactic_com_list generalize (get_commands argsl) + +let dyn_generalize_dep = function + | [Command com] -> tactic_com generalize_dep com + | l -> bad_tactic_args "dyn_generalize_dep" l + +(* Faudra-t-il une version avec plusieurs args de generalize_dep ? +Cela peut-être troublant de faire "Generalize Dependent H n" dans +"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la +généralisation dépendante par n. + +let quantify lconstr = + List.fold_right + (fun com tac -> tclTHEN tac (tactic_com generalize_dep c)) + lconstr + tclIDTAC +*) + +(* A dependent cut rule à la sequent calculus *) + +(* Sera simplifiable le jour où il y aura un let in primitif dans constr *) + +(* if [occhypl] is empty, [c] is substituted in every hyp where it occurs *) +(* if name = Anonymous, the name is build from the first letter of the type *) + +let letin_abstract id c occ_ccl occhypl gl = + let allhyp = occhypl=[] in + let hyps = pf_untyped_hyps gl in + let abstract ((dephyps,deptyps,marks,occl as accu),lhyp) hyp typ = + try + let occ = if allhyp then [] else List.assoc hyp occl in + let newtyp = subst1 (VAR id) (subst_term_occ occ c typ) in + let newoccl = except_assoc hyp occl in + if typ=newtyp then + (accu,Some hyp) + else + ((hyp::dephyps,newtyp::deptyps,(hyp,lhyp)::marks,newoccl),lhyp) + with Not_found -> + (accu,Some hyp) + in + let (dephyps,deptyps,marks,rest),_ = + it_sign abstract (([],[],[],occhypl),None) hyps in + if rest <> [] then begin + let id = fst (List.hd rest) in + if mem_sign hyps id + then error ("Hypothesis "^(string_of_id id)^" occurs twice") + else error ("No such hypothesis : " ^ (string_of_id id)) + end; + let ccl = match occ_ccl with + | None -> (pf_concl gl) + | Some occ -> subst1 (VAR id) (subst_term_occ occ c (pf_concl gl)) + in + (dephyps,deptyps,marks,ccl) + +let letin_tac with_eq name c occ_ccl occhypl gl = + let x = id_of_name_using_hdchar (pf_type_of gl c) name in + let hyps = pf_untyped_hyps gl in + let id = next_global_ident_away x (ids_of_sign hyps) in + if mem_sign hyps id then error "New variable is already declared"; + let (dephyps,deptyps,marks,ccl)= letin_abstract id c occ_ccl occhypl gl in + let t = pf_type_of gl c in + let (eqc,reflc) = + let sort = pf_type_of gl t in + if is_Set sort then + (pf_parse_const gl "eq", pf_parse_const gl "refl_equal") + else if is_Type sort then + (pf_parse_const gl "eqT", pf_parse_const gl "refl_eqT") + else error "Not possible with proofs yet" + in + let heq = next_global_ident_away (id_of_string "Heq") (ids_of_sign hyps) in + let tmpcl = List.fold_right2 mkNamedProd dephyps deptyps ccl in + let tmpargs = List.map (fun id -> VAR id) dephyps in + let newcl,args = + if with_eq then + let eq = applist (eqc,[t;VAR id;c]) in + let refl = applist (reflc,[t;c]) in + (mkNamedProd id t (mkNamedProd heq eq tmpcl), c::refl::tmpargs) + else + (mkNamedProd id t tmpcl, c::tmpargs) + in + let lastlhyp = if marks=[] then None else snd (List.hd marks) in + tclTHENLIST + [ apply_type newcl args; + thin dephyps; + central_intro (IMustBe id) lastlhyp false; + if with_eq then central_intro (IMustBe heq) lastlhyp false else tclIDTAC; + intros_move marks ] gl + +let dyn_lettac args gl = match args with + | [Identifier id; Command com; Letpatterns (o,l)] -> + letin_tac true (Name id) (pf_constr_of_com gl com) o l gl + | [Identifier id; Constr c; Letpatterns (o,l)] -> + letin_tac true (Name id) c o l gl + | l -> bad_tactic_args "letin" l + + +(********************************************************************) +(* Exact tactics *) +(********************************************************************) + +let exact c gl = + let concl = (pf_concl gl) in + let ct = pf_type_of gl c in + if pf_conv_x_leq gl ct concl then + refine c gl + else + error "Not an exact proof" + +(* +let dyn_exact = + function [(COMMAND com)] -> tactic_com exact com + | l -> bad_tactic_args "exact" l + +*) + +let dyn_exact cc gl = match cc with + | [Constr c] -> exact c gl + | [Command com] -> + let evc = (project gl) in + let concl = (pf_concl gl) in + let c = constr_of_com_casted evc (pf_hyps gl) com concl in + refine c gl + | l -> bad_tactic_args "exact" l + +let (assumption:tactic) = fun gl -> + let concl = pf_concl gl in + let rec arec = function + | ([],[]) -> error "No such assumption" + | (s::sl,a::al) -> if pf_conv_x_leq gl a concl then + refine (VAR(s)) gl else arec (sl,al) + | _ -> assert false + in + arec (pf_untyped_hyps gl) + +let dyn_assumption = function + | [] -> assumption + | l -> bad_tactic_args "assumption" l + + +(*****************************************************************) +(* Modification of a local context *) +(*****************************************************************) + +(* This tactic enables the user to remove hypotheses from the signature. + * Some care is taken to prevent him from removing variables that are + * subsequently used in other hypotheses or in the conclusion of the + * goal. *) + +let clear ids gl = thin ids gl +let clear_one id gl = clear [id] gl +let dyn_clear = function + | [Clause ids] -> clear ids + | _ -> assert false + +(* Clears a list of identifiers clauses form the context *) + +let clear_clauses clsl = + clear (List.map + (function + | Some id -> id + | None -> error "ThinClauses") clsl) + +(* Clears one identifier clause from the context *) + +let clear_clause cls = clear_clauses [cls] + + +(* Takes a list of booleans, and introduces all the variables + * quantified in the goal which are associated with a value + * true in the boolean list. *) + +let rec intros_clearing = function + | [] -> tclIDTAC + | (false::tl) -> tclTHEN intro (intros_clearing tl) + | (true::tl) -> + tclTHENLIST [ intro; onLastHyp clear_clause; intros_clearing tl] + +(* Adding new hypotheses *) + +let new_hyp mopt c blist g = + let (wc,kONT) = startWalk g in + let clause = mk_clenv_printable_type_of wc c in + let clause' = clenv_match_args blist clause in + let (thd,tstack) = whd_castapp_stack (clenv_instance_template clause')[] in + let nargs = List.length tstack in + let cut_pf = + applist(thd, + match mopt with + | Some m -> if m < nargs then firstn m tstack else tstack + | None -> tstack) + in + (tclTHENL (tclTHEN (kONT clause.hook) + (cut (pf_type_of g cut_pf))) + ((tclORELSE (apply cut_pf) (exact cut_pf)))) g + +let dyn_new_hyp argsl gl = + match argsl with + | [Integer n; Command com; Bindings binds] -> + tactic_bind_list + (new_hyp (Some n) + (pf_constr_of_com gl com)) + binds gl + | [Command com; Bindings binds] -> + tactic_bind_list + (new_hyp None + (pf_constr_of_com gl com)) + binds gl + | [Integer n; Constr c; Cbindings binds] -> + new_hyp (Some n) c binds gl + | [Constr c; Cbindings binds] -> + new_hyp None c binds gl + | l -> bad_tactic_args "new_hyp" l + +(* Moving hypotheses *) + +let dyn_move = function + | [Identifier idfrom; Identifier idto] -> move_hyp false idfrom idto + | _ -> assert false + +let dyn_move_dep = function + | [Identifier idfrom; Identifier idto] -> move_hyp true idfrom idto + | _ -> assert false + +(************************) +(* Introduction tactics *) +(************************) + +let constructor_checking_bound boundopt i lbind gl = + let cl = pf_concl gl in + let (mind,_,redcl) = reduce_to_mind (project gl) cl in + let (x_0,x_1,args) = destMutInd mind in + let nconstr = mis_nconstr (mind_specif_of_mind mind) + and sigma = project gl in + if i=0 then error "The constructors are numbered starting from 1"; + if i > nconstr then error "Not enough constructors"; + begin match boundopt with + | Some expctdnum -> + if expctdnum <> nconstr then + error "Not the expected number of constructors" + | None -> () + end; + let cons = DOPN(MutConstruct((x_0,x_1),i),args) in + let apply_tac = apply_with_bindings (cons,lbind) in + (tclTHENLIST [convert_concl redcl; intros; apply_tac]) gl + +let one_constructor i = (constructor_checking_bound None i) + +let any_constructor gl = + let cl = pf_concl gl in + let (mind,_,redcl) = reduce_to_mind (project gl) cl in + let (x_0,x_1,args) = destMutInd mind in + let nconstr = mis_nconstr (mind_specif_of_mind mind) + and sigma = project gl in + if nconstr = 0 then error "The type has no constructors"; + tclFIRST (List.map (fun i -> one_constructor i []) + (interval 1 nconstr)) gl + +let dyn_constructor = function + | [Integer i; Bindings binds] -> tactic_bind_list (one_constructor i) binds + | [Integer i; Cbindings binds] -> (one_constructor i) binds + | [] -> any_constructor + | l -> bad_tactic_args "constructor" l + +let left = (constructor_checking_bound (Some 2) 1) +let simplest_left = left [] + +let dyn_left = function + | [Cbindings binds] -> left binds + | [Bindings binds] -> tactic_bind_list left binds + | l -> bad_tactic_args "left" l + +let right = (constructor_checking_bound (Some 2) 2) +let simplest_right = right [] + +let dyn_right = function + | [Cbindings binds] -> right binds + | [Bindings binds] -> tactic_bind_list right binds + | l -> bad_tactic_args "right" l + + +let split = (constructor_checking_bound (Some 1) 1) +let simplest_split = split [] + +let dyn_split = function + | [Cbindings binds] -> split binds + | [Bindings binds] -> tactic_bind_list split binds + | l -> bad_tactic_args "split" l + +(********************************************) +(* Elimination tactics *) +(********************************************) + + +(* kONT : ?? + * wc : ?? + * elimclause : ?? + * inclause : ?? + * gl : the current goal +*) + +let last_arg = function + | DOPN(AppL,cl) -> cl.(Array.length cl - 1) + | _ -> anomaly "last_arg" + +let elimination_clause_scheme kONT wc elimclause indclause gl = + let indmv = + (match last_arg (clenv_template elimclause).rebus with + | DOP0(Meta mv) -> mv + | _ -> errorlabstrm "elimination_clause" + [< 'sTR "The type of elimination clause is not well-formed" >]) + in + let elimclause' = clenv_fchain indmv elimclause indclause in + elim_res_pf kONT elimclause' gl + +(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and + * refine fails *) + +let make_clenv_binding wc (c,t) lbind = + let largs = collect_com lbind in + let lcomargs = List.length largs in + if lcomargs = List.length lbind then + let clause = mk_clenv_from wc (c,t) in + clenv_constrain_dep_args largs clause + else if lcomargs = 0 then + let clause = mk_clenv_rename_from wc (c,t) in + clenv_match_args lbind clause + else + errorlabstrm "make_clenv_bindings" + [<'sTR "Cannot mix bindings and free associations">] + +let type_clenv_binding wc (c,t) lbind = + clenv_instance_template_type (make_clenv_binding wc (c,t) lbind) + +(* + * Elimination tactic with bindings and using an arbitrary + * elimination constant called elimc. This constant should end + * with a clause (x:I)(P .. ), where P is a bound variable. + * The term c is of type t, which is a product ending with a type + * matching I, lbindc are the expected terms for c arguments + *) + +let general_elim (c,lbindc) (elimc,lbindelimc) gl = + let (wc,kONT) = startWalk gl in + let (_,_,t) = reduce_to_ind (project gl) (pf_type_of gl c) in + let indclause = make_clenv_binding wc (c,t) lbindc in + let elimt = w_type_of wc elimc in + let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in + elimination_clause_scheme kONT wc elimclause indclause gl + +(* Elimination tactic with bindings but using the default elimination + * constant associated with the type. *) + +let default_elim (c,lbindc) gl = + let (path_name,_,t) = reduce_to_ind (project gl) (pf_type_of gl c) in + let elimc = + lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl)) + in + general_elim (c,lbindc) (elimc,[]) gl + + +(* The simplest elimination tactic, with no substitutions at all. *) + +let simplest_elim c = default_elim (c,[]) + +(* + * A "natural" induction tactic + * + - [H0:T0, ..., Hi:Ti, hyp0:P->I(args), Hi+1:Ti+1, ..., Hn:Tn |-G] is the goal + - [hyp0] is the induction hypothesis + - we extract from [args] the variables which are not rigid parameters + of the inductive type, this is [indvars] (other terms are forgotten); + [indhyps] are the ones which actually are declared in context + (done in [find_atomic_param_of_ind]) + - we look for all hyps depending of [hyp0] or one of [indvars]: + this is [dephyps] of types [deptyps] respectively + - [statuslist] tells for each hyps in [dephyps] after which other hyp + fixed in the context they must be moved (when induction is done) + - [hyp0succ] is the name of the hyp fixed in the context after which to + move the subterms of [hyp0succ] in the i-th branch where it is supposed + to be the i-th constructor of the inductive type. + + Strategy: (cf in [induction_from_context]) + - requantify and clear all [dephyps] + - apply induction on [hyp0] + - clear [indhyps] and [hyp0] + - in the i-th subgoal, intro the arguments of the i-th constructor + of the inductive type after [hyp0succ] (done in + [induct_discharge]) let the induction hypotheses on top of the + hyps because they may depend on variables between [hyp0] and the + top. A counterpart is that the dep hyps programmed to be intro-ed + on top must now be intro-ed after the induction hypotheses + - move each of [dephyps] at the right place following the + [statuslist] + + *) + + +let rec is_rec_arg indpath t = + try + mind_path (fst (find_mrectype empty_evd t)) = indpath + with Induc -> + false + +let induct_discharge indpath statuslists cname destopt avoid (_,t) = + let (lstatus,rstatus) = statuslists in + let tophyp = ref None in + let (l,_) = decompose_prod t in + let n = List.length (filter (fun (_,t') -> is_rec_arg indpath t') l) in + let recvarname = + if n=1 then + cname + else if id_without_number cname then + id_of_string ((string_of_id cname)^"1") + else + id_of_string ((string_of_id cname)^"_1") + in + let hyprecname = id_of_string ("Hrec"^(string_of_id recvarname)) in + let rec peel_tac = function + | DOP2 (Prod,t,DLAM(na,DOP2(Prod,tr,DLAM(nar,c)))) + when is_rec_arg indpath t + -> if !tophyp=None then tophyp:=Some hyprecname;(* for lstatus *) + tclTHENLIST + [ central_intro (IBasedOn (recvarname,avoid)) destopt false; + central_intro (IBasedOn (hyprecname,avoid)) None false; + peel_tac c] + | DOP2 (Cast,c,t) -> peel_tac c + | DOP2 (Prod,t,DLAM(na,c)) + -> tclTHEN (central_intro (IAvoid avoid) destopt false) + (peel_tac c) + | _ -> tclIDTAC + in + let evaluated_peel_tac = peel_tac t in (* because side effect on tophyp *) + let newlstatus = (* if some Hrec has taken place at the top of hyps *) + List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus + in + tclTHENLIST [ evaluated_peel_tac; + intros_rmove rstatus; + intros_move newlstatus ] + +(* - le recalcul de indtyp à chaque itération de atomize_one est pour ne pas + s'embêter à regarder si un letin_tac ne fait pas des + substitutions aussi sur l'argument voisin *) + +(* Marche pas... faut prendre en compte l'occurence précise... *) + +let atomize_param_of_ind hyp0 gl = + let tmptyp0 = + try + (snd(lookup_sign hyp0 (pf_untyped_hyps gl))) + with Not_found -> + error ("No such hypothesis : " ^ (string_of_id hyp0)) + in + let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in + let mis = mind_specif_of_mind mind in + let nparams = mis_nparams mis in + let argl = snd (decomp_app indtyp) in + let params = firstn nparams argl in + (* le gl est important pour ne pas préévaluer *) + let rec atomize_one i avoid gl = + if i<>nparams then + let tmptyp0 = pf_get_hyp gl hyp0 in + let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in + match (destAppL (whd_castapp indtyp)).(i) with + | VAR id when not (List.exists (occur_var id) avoid) -> + atomize_one (i-1) ((VAR id)::avoid) gl + | VAR id -> + let x = fresh_id [] id gl in + tclTHEN + (letin_tac true (Name x) (VAR id) (Some []) []) + (atomize_one (i-1) ((VAR x)::avoid)) gl + | c -> + let id = id_of_name_using_hdchar (pf_type_of gl c) Anonymous in + let x = fresh_id [] id gl in + tclTHEN + (letin_tac true (Name x) c (Some []) []) + (atomize_one (i-1) ((VAR x)::avoid)) gl + else + tclIDTAC gl + in + atomize_one (List.length argl) params gl + +let find_atomic_param_of_ind mind indtyp = + let mis = mind_specif_of_mind mind in + let nparams = mis_nparams mis in + let argl = snd (decomp_app indtyp) in + let argv = Array.of_list argl in + let params = firstn nparams argl in + let indvars = ref [] in + for i = nparams to (Array.length argv)-1 do + match argv.(i) with + | VAR id when not (List.exists (occur_var id) params) -> + indvars := add_set id !indvars + | _ -> () + done; + !indvars + + (* [cook_sign] builds the lists [indhyps] of hyps that must be + erased, the lists of hyps to be generalize [(hdeps,tdeps)] on the + goal together with the places [(lstatus,rstatus)] where to re-intro + them after induction. To know where to re-intro the dep hyp, we + remember the name of the hypothesis [lhyp] after which (if the dep + hyp is more recent than [hyp0]) or [rhyp] before which (if older + than [hyp0]) its equivalent must be moved when the induction has + been applied. Since computation of dependencies and [rhyp] is from + more ancient (on the right) to more recent hyp (on the left) but + the computation of [lhyp] progresses from the other way, [cook_hyp] + is in two passes (an alternative would have been to write an + higher-order algorithm). We strongly use references to reduce + the accumulation of arguments. + + To summarize, the situation looks like this + + Goal(n,x) -| H6:(Q n); x:A; H5:True; H4:(le O n); H3:(P n); H2:True; n:nat + Left Right + + Induction hypothesis is H4 ([hyp0]) + Variable parameters of (le O n) is the singleton list with "n" ([indvars]) + Part of [indvars] really in context is the same ([indhyps] + The dependent hyps are H3 and H6 ([dephyps]) + For H3 the memorized places are H5 ([lhyp]) and H2 ([rhyp]) + because these names are among the hyp which are fixed through the induction + For H6 the neighbours are None ([lhyp]) and H5 ([rhyp]) + For H3, because on the right of H4, we remember rhyp (here H2) + For H6, because on the left of H4, we remember lhyp (here None) + For H4, we remember lhyp (here H5) + + The right neighbour is then translated into the left neighbour + because move_hyp tactic needs the name of the hyp _after_ which we + move the hyp to move. + + But, say in the 2nd subgoal of the hypotheses, the goal will be + + (m:nat)((P m)->(Q m)->(Goal m)) -> (P Sm)-> (Q Sm)-> (Goal Sm) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ + both go where H4 was goes where goes where + H3 was H6 was + + We have to intro and move m and the recursive hyp first, but then + where to move H3 ??? Only the hyp on its right is relevant, but we + have to translate it into the name of the hyp on the left + + Note: this case where some hyp(s) in [dephyps] has(have) the same + left neighbour as [hyp0] is the only problematic case with right + neighbours. For the other cases (e.g. an hyp H1:(R n) between n and H2 + would have posed no problem. But for uniformity, we decided to use + the right hyp for all hyps on the right of H4. + + Others solutions are welcome *) + +exception Shunt of identifier option + +let cook_sign hyp0 indvars sign = + (* First pass from L to R: get [indhyps], [dephyps] and [statuslist] + for the hypotheses before (= more ancient than) hyp0 (see above) *) + let allindhyps = hyp0::indvars in + let indhyps = ref [] in + let hdeps = ref [] in + let tdeps = ref [] in + let ldeps = ref [] in + let rstatus = ref [] in + let lstatus = ref [] in + let before = ref true in + let seek_deps hyp typ rhyp = + if hyp = hyp0 then begin + before:=false; + None (* fake value *) + end else if List.mem hyp indvars then begin + indhyps := hyp::!indhyps; + rhyp + end else if (List.exists (fun id -> occur_var id typ) allindhyps + or List.exists (fun id -> occur_var id typ) !hdeps) then begin + hdeps := hyp::!hdeps; + tdeps := typ::!tdeps; + if !before then + rstatus := (hyp,rhyp)::!rstatus + else + ldeps := hyp::!ldeps; (* status calculé lors de la 2ème passe *) + Some hyp + end else + Some hyp + in + let _ = sign_it seek_deps sign None in + (* 2nd pass from R to L: get left hyp of [hyp0] and [lhyps] *) + let compute_lstatus lhyp hyp typ = + if hyp = hyp0 then raise (Shunt lhyp); + if List.mem hyp !ldeps then begin + lstatus := (hyp,lhyp)::!lstatus; + lhyp + end else + (Some hyp) + in + try + let _ = it_sign compute_lstatus None sign in anomaly "hyp0 not found" + with Shunt lhyp0 -> + let statuslists = (!lstatus,List.rev !rstatus) in + let deps = (List.rev !hdeps, List.rev !tdeps) in + (statuslists, lhyp0, !indhyps, deps) + + +(* Vieille version en une seule passe grace à l'ordre supérieur mais + trop difficile à comprendre + +let cook_sign hyp0 indvars sign = + let finaldeps = ref ([],[]) in + let indhyps = ref [] in + let hyp0succ = ref None in + let cook_init (hdeps,tdeps) rhyp before = + finaldeps := (List.rev hdeps, List.rev tdeps); + (None, []) in + let cook_hyp compute_rhyp hyp typ ((hdeps,tdeps) as deps) = + fun rhyp before -> + match () with + _ when (List.mem hyp indvars) + -> let result = compute_rhyp deps rhyp before in + indhyps := hyp::!indhyps; result + | _ when hyp = hyp0 + -> let (lhyp,statl) = compute_rhyp deps rhyp true in + hyp0succ := lhyp; (None (* fake value *),statl) + | _ when (List.exists (fun id -> occur_var id typ) (hyp0::indvars) + or List.exists (fun id -> occur_var id typ) hdeps) + -> let deps' = (hyp::hdeps, typ::tdeps) in + let (lhyp,statl) = compute_rhyp deps' rhyp before in + let hyp = if before then lhyp else rhyp in + (lhyp,(DEPENDENT (before,hyp,hyp))::statl) + | _ -> + let (_,statl) = compute_rhyp deps (Some hyp) before + in (Some hyp, statl) + in let (_,statuslist) = it_sign cook_hyp cook_init sign ([],[]) None false in + (statuslist, !hyp0succ, !indhyps, !finaldeps) +*) + +let induction_tac varname typ (elimc,elimt) gl = + let c = VAR varname in + let (wc,kONT) = startWalk gl in + let indclause = make_clenv_binding wc (c,typ) [] in + let elimclause = make_clenv_binding wc (DOP2(Cast,elimc,elimt),elimt) [] in + elimination_clause_scheme kONT wc elimclause indclause gl + +let get_constructors varname (elimc,elimt) mind mindpath = + (* Je suppose que w_type_of=type_of pour les constantes comme elimc *) + (* J'espere que je ne me trompe pas *) + let (hyps_of_elimt,_) = decompose_prod elimt in + let mis = mind_specif_of_mind mind in + let nconstr = mis_nconstr mis in + let nparam = mis_nparams mis in + try + List.rev (firstn nconstr (lastn (nconstr + nparam + 1) hyps_of_elimt)) + with Failure _ -> + anomaly "induct_elim: bad elimination predicate" + +let induction_from_context hyp0 gl = + (*test suivant sans doute inutile car protégé par le letin_tac avant appel*) + if List.mem hyp0 (ids_of_sign (initial_sign ())) then + errorlabstrm "induction" [< 'sTR "Cannot generalize a global variable" >]; + let sign = pf_untyped_hyps gl in + let tsign = pf_hyps gl in + let tmptyp0 = pf_get_hyp gl hyp0 in + let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in + let indvars = find_atomic_param_of_ind mind indtyp in + let mindpath = mind_path mind in + let elimc = lookup_eliminator tsign mindpath (suff gl (pf_concl gl)) in + let elimt = pf_type_of gl elimc in + let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars sign in + let (dephyps,deptyps) = deps in + let tmpcl = List.fold_right2 mkNamedProd dephyps deptyps (pf_concl gl) in + let lc = get_constructors hyp0 (elimc,elimt) mind mindpath in + tclTHENLIST + [ apply_type tmpcl (List.map (fun id -> VAR id) dephyps); + thin dephyps; + tclTHENS + (tclTHEN + (induction_tac hyp0 typ0 (elimc,elimt)) + (thin (hyp0::(List.rev indhyps)))) + (List.map (induct_discharge mindpath statlists hyp0 lhyp0 dephyps) lc)] + gl + +let induction_with_atomization_of_ind_arg hyp0 = + tclTHEN + (atomize_param_of_ind hyp0) + (induction_from_context hyp0) + +let new_induct c gl = + match c with + | (VAR id) when not (List.mem id (ids_of_sign (initial_sign ()))) -> + tclORELSE + (tclTHEN (intros_until id) (tclLAST_HYP simplest_elim)) + (induction_with_atomization_of_ind_arg id) gl + | _ -> + let x = id_of_name_using_hdchar (pf_type_of gl c) Anonymous in + let id = fresh_id [] x gl in + tclTHEN + (letin_tac true (Name id) c (Some []) []) + (induction_with_atomization_of_ind_arg id) gl + +(***) + +(* The registered tactic, which calls the default elimination + * if no elimination constant is provided. *) + +let dyn_elim = function + | [Constr mp; Cbindings mpbinds] -> + default_elim (mp,mpbinds) + | [Command mp; Bindings mpbinds] -> + tactic_com_bind_list default_elim (mp,mpbinds) + | [Command mp; Bindings mpbinds; Command elimc; Bindings elimcbinds] -> + let funpair2funlist f = (function [x;y] -> f x y | _ -> assert false) in + tactic_com_bind_list_list + (funpair2funlist general_elim) + [(mp,mpbinds);(elimc,elimcbinds)] + | [Constr mp; Cbindings mpbinds; Constr elimc; Cbindings elimcbinds] -> + general_elim (mp,mpbinds) (elimc,elimcbinds) + | l -> bad_tactic_args "elim" l + +(* Induction tactics *) + +let induct s = + tclORELSE (tclTHEN (intros_until s) (tclLAST_HYP simplest_elim)) + (induction_from_context s) + +let induct_nodep n = tclTHEN (intros_do n) (tclLAST_HYP simplest_elim) + +(* Pour le futur +let dyn_induct = function + | [(COMMAND c)] -> tactic_com new_induct x + | [(CONSTR x)] -> new_induct x + | [(INTEGER n)] -> induct_nodep n + | l -> bad_tactic_args "induct" l +*) + +let dyn_induct = function + | [Identifier x] -> induct x + | [Integer n] -> induct_nodep n + | l -> bad_tactic_args "induct" l + +(* Case analysis tactics *) + +let general_case_analysis (c,lbindc) gl = + let (mind,_,_) = reduce_to_mind (project gl) (pf_type_of gl c) in + let sigma = project gl in + let sort = sort_of_goal gl in + let elim = Indrec.make_case_gen sigma mind sort in + general_elim (c,lbindc) (elim,[]) gl + +let simplest_case c = general_case_analysis (c,[]) + +let dyn_case =function + | [(CONSTR mp);(CBINDINGS mpbinds)] -> + general_case_analysis (mp,mpbinds) + | [(COMMAND mp);(BINDINGS mpbinds)] -> + tactic_com_bind_list general_case_analysis (mp,mpbinds) + | l -> bad_tactic_args "case" l + + +(* Destruction tactics *) + +let destruct s = (tclTHEN (intros_until s) (tclLAST_HYP simplest_case)) +let destruct_nodep n = (tclTHEN (intros_do n) (tclLAST_HYP simplest_case)) + +let dyn_destruct = function + | [(IDENTIFIER x)] -> destruct x + | [(INTEGER n)] -> destruct_nodep n + | l -> bad_tactic_args "destruct" l + +(* + * Eliminations giving the type instead of the proof. + * These tactics use the default elimination constant and + * no substitutions at all. + * May be they should be integrated into Elim ... + *) + +let elim_scheme_type elim t gl = + let (wc,kONT) = startWalk gl in + let clause = mk_clenv_type_of wc elim in + match last_arg (clenv_template clause).rebus with + | DOP0(Meta mv) -> + let clause' = clenv_unify (clenv_instance_type clause mv) t clause in + elim_res_pf kONT clause' gl + | _ -> anomaly "elim_scheme_type" + +let elim_type t gl = + let (path_name,tind,t) = reduce_to_ind (project gl) t in + let elimc = + lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl)) + in + match t with + | DOP2(Prod,_,_) -> error "Not an inductive definition" + | _ -> elim_scheme_type elimc tind gl + +let dyn_elim_type = function + | [(CONSTR c)] -> elim_type c + | [(COMMAND com)] -> tactic_com_sort elim_type com + | l -> bad_tactic_args "elim_type" l + +let case_type t gl = + let (mind,_,t) = reduce_to_mind (project gl) t in + match t with + | DOP2(Prod,_,_) -> error "Not an inductive definition" + | _ -> + let sigma = project gl in + let sort = sort_of_goal gl in + let elimc = Indrec.make_case_gen sigma mind sort in + elim_scheme_type elimc t gl + +let dyn_case_type = function + | [CONSTR c] -> case_type c + | [COMMAND com] -> tactic_com case_type com + |l -> bad_tactic_args "case_type" l + + +(* Some eliminations frequently used *) + +(* These elimination tactics are particularly adapted for sequent + calculus. They take a clause as argument, and yield the + elimination rule if the clause is of the form (Some id) and a + suitable introduction rule otherwise. They do not depend on + the name of the eliminated constant, so they can be also + used on ad-hoc disjunctions and conjunctions introduced by + the user. + -- Eduardo Gimenez (11/8/97) + + HH (29/5/99) replaces failures by specific error messages + *) + +let andE id gl = + let t = pf_get_hyp gl id in + if is_conjunction (pf_hnf_constr gl t) then + (tclTHEN (simplest_elim (VAR id)) (tclDO 2 intro)) gl + else + errorlabstrm "andE" + [< 'sTR("Tactic andE expects "^(string_of_id id)^" is a conjunction.")>] + +let dAnd cls gl = + match cls with + | None -> simplest_split gl + | Some id -> andE id gl + +let orE id gl = + let t = pf_get_hyp gl id in + if is_disjunction (pf_hnf_constr gl t) then + (tclTHEN (simplest_elim (VAR id)) intro) gl + else + errorlabstrm "orE" + [< 'sTR("Tactic orE expects "^(string_of_id id)^" is a disjunction.")>] + +let dorE b cls gl = + match cls with + | (Some id) -> orE id gl + | None -> (if b then right else left) [] gl + +let impE id gl = + let t = pf_get_hyp gl id in + if is_imp_term (pf_hnf_constr gl t) then + let (dom, _, rng) = destProd (pf_hnf_constr gl t) in + (tclTHENS (cut_intro rng) + [tclIDTAC;apply_term (VAR id) [DOP0(Meta(newMETA()))]]) gl + else + errorlabstrm "impE" + [< 'sTR("Tactic impE expects "^(string_of_id id)^ + " is a an implication.")>] + +let dImp cls gl = + match cls with + | None -> intro gl + | Some id -> impE id gl + +(******************************************) +(* Instantiation of existential variables *) +(******************************************) + +let instantiate_pf n c pfts = + let gls = top_goal_of_pftreestate pfts in + let (wc,_) = startWalk gls in + let sigma = (w_Underlying wc) in + let (sp,_) = + try + List.nth (Evd.non_instantiated sigma) (n-1) + with Failure _ -> + error "not so many uninstantiated existential variables" + in + let wc' = w_Define sp c wc in + let newgc = ts_mk (w_Underlying wc') in + change_constraints_pftreestate newgc pfts + +let instantiate_pf_com n com pfts = + let gls = top_goal_of_pftreestate pfts in + let (wc,_) = startWalk gls in + let sigma = (w_Underlying wc) in + let (sp,evd) = + try + List.nth (Evd.non_instantiated sigma) (n-1) + with Failure _ -> + error "not so many uninstantiated existential variables" + in + let c = constr_of_com sigma evd.hyps com in + let wc' = w_Define sp c wc in + let newgc = ts_mk (w_Underlying wc') in + change_constraints_pftreestate newgc pfts + +(************************************************) +(* Tactics related with logic connectives *) +(************************************************) + +(* Contradiction *) + +let contradiction_on_hyp id gl = + let hyp = pf_get_hyp gl id in + if is_empty_type hyp then + simplest_elim (VAR id) gl + else + error "Not a contradiction" + +(* Absurd *) +let absurd c gls = + let falseterm = pf_constr_of_com_sort gls (nvar "False") in + (tclTHENS + (tclTHEN (elim_type falseterm) (cut c)) + ([(tclTHENS + (cut (applist(pf_global gls (id_of_string "not"),[c]))) + ([(tclTHEN (intros) + ((fun gl -> + let (ida,_) = pf_nth_hyp gl 1 + and (idna,_) = pf_nth_hyp gl 2 in + exact (applist(VAR idna,[VAR ida])) gl))); + tclIDTAC])); + tclIDTAC])) gls + +let dyn_absurd = function + | [(CONSTR c)] -> absurd c + | [(COMMAND com)] -> tactic_com_sort absurd com + | l -> bad_tactic_args "absurd" l + +let contradiction gls = + let falseterm = pf_constr_of_com_sort gls (nvar "False") in + tclTHENLIST [ intros; elim_type falseterm; assumption ] gls + +let dyn_contradiction = function + | [] -> contradiction + | l -> bad_tactic_args "contradiction" l + +(* Relfexivity tactics *) + +let reflexivity gl = + match match_with_equation (pf_concl gl) with + | None -> error "The conclusion is not a substitutive equation" + | Some (hdcncl,args) -> one_constructor 1 [] gl + +let intros_reflexivity = (tclTHEN intros reflexivity) + +let dyn_reflexivity = function + | [] -> intros_reflexivity + | _ -> errorlabstrm "Tactics.reflexivity" + [<'sTR "Tactic applied to bad arguments!">] + +(* Symmetry tactics *) + +(* This tactic first tries to apply a constant named sym_eq, where eq + is the name of the equality predicate. If this constant is not + defined and the conclusion is a=b, it solves the goal doing (Cut + b=a;Intro H;Case H;Constructor 1) *) + +let symmetry gl = + match match_with_equation (pf_concl gl) with + | None -> error "The conclusion is not a substitutive equation" + | Some (hdcncl,args) -> + let hdcncls = string_head hdcncl in + begin + try + (apply (pf_parse_const gl ("sym_"^hdcncls)) gl) + with _ -> + let symc = match args with + | [typ;c1;c2] -> mkAppL [| hdcncl; typ; c2; c1 |] + | [c1;c2] -> mkAppL [| hdcncl; c2; c1 |] + | _ -> assert false + in + (tclTHENS (cut symc) + [ tclTHENLIST [ intro; + tclLAST_HYP simplest_case; + one_constructor 1 [] ]; + tclIDTAC ]) gl + end + +let intros_symmetry = (tclTHEN intros symmetry) + +let dyn_symmetry = function + | [] -> intros_symmetry + | l -> bad_tactic_args "symmetry" l + +(* Transitivity tactics *) + +(* This tactic first tries to apply a constant named trans_eq, where eq + is the name of the equality predicate. If this constant is not + defined and the conclusion is a=b, it solves the goal doing + Cut x1=x2; + [Cut x2=x3; [Intros e1 e2; Case e2;Assumption + | Idtac] + | Idtac] + --Eduardo (19/8/97) +*) + +let transitivity t gl = + match match_with_equation (pf_concl gl) with + | None -> error "The conlcusion is not a substitutive equation" + | Some (hdcncl,args) -> + let hdcncls = string_head hdcncl in + begin + try + apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl + with _ -> + let eq1 = match args with + | [typ;c1;c2] -> mkAppL [| hdcncl; typ; c1; t |] + | [c1;c2] -> mkAppL [| hdcncl; c1; t|] + | _ -> assert false + in + let eq2 = match args with + | [typ;c1;c2] -> mkAppL [| hdcncl; typ; t; c2 |] + | [c1;c2] -> mkAppL [| hdcncl; t; c2 |] + | _ -> assert false + in + (tclTHENS (cut eq2) + [tclTHENS (cut eq1) + [ tclTHENLIST [ tclDO 2 intro; + tclLAST_HYP simplest_case; + assumption ]; + tclIDTAC]; + tclIDTAC])gl + end + +let intros_transitivity n = tclTHEN intros (transitivity n) + +let dyn_transitivity = function + | [(CONSTR n)] -> intros_transitivity n + | [(COMMAND n)] -> tactic_com intros_transitivity n + | l -> bad_tactic_args "transitivity" l + +(* tactical to save as name a subproof such that the generalisation of + the current goal, abstracted with respect to the local signature, + is solved by tac *) + +let abstract_subproof name tac gls = + let current_sign = initial_sign() + and global_sign = pf_untyped_hyps gls in + let sign = Names.sign_it + (fun id typ s -> + if mem_sign current_sign id then s else add_sign (id,typ) s) + global_sign nil_sign + in + let na = next_global_ident_away name + (ids_of_sign global_sign) in + let nas = string_of_id na in + let concl = Names.it_sign (fun t id typ -> mkNamedProd id typ t) + (pf_concl gls) sign in + let top_goal = mkGOAL (mt_ctxt Spset.empty) current_sign concl in + let ts = {top_hyps = initial_assumptions(); + top_goal = top_goal; + top_strength = Constrtypes.NeverDischarge} + in + start(nas,ts);set_proof (Some nas); + begin + try + by (tclCOMPLETE (tclTHEN (tclDO (sign_length sign) intro) + tac)); + save_named true + with UserError _ as e -> + (abort_cur_goal(); raise e) + end; + exact (applist ((Machops.global (gLOB current_sign) na), + (List.map (fun id -> VAR(id)) + (List.rev (ids_of_sign sign))))) + gls + +let tclABSTRACT name_op tac gls = + let s = match name_op with + | Some s -> s + | None -> id_of_string ((get_proof ())^"_subproof") + in + abstract_subproof s tac gls + +let dyn_tclABSTRACT = + hide_tactic "ABSTRACT" + (function + | [TACEXP tac] -> + tclABSTRACT None (Tacinterp.interp tac) + | [IDENTIFIER s; TACEXP tac] -> + tclABSTRACT (Some s) (Tacinterp.interp tac) + | _ -> invalid_arg "tclABSTRACT") diff --git a/tactics/tactics.mli b/tactics/tactics.mli new file mode 100644 index 000000000..db60df966 --- /dev/null +++ b/tactics/tactics.mli @@ -0,0 +1,244 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Tacmach +open Proof_trees +open Reduction +open Evd +open Clenv +open Tacred +open Tacticals +(*i*) + +(* Main tactics. *) + +(*s General functions. *) + +val make_clenv_binding_apply : + walking_constraints -> constr * constr -> constr substitution -> + walking_constraints clausenv + +val type_clenv_binding : walking_constraints -> + constr * constr -> constr substitution -> constr + +val string_head : constr -> string +val head_constr : constr -> constr list +val head_constr_bound : constr -> constr list -> constr list +val bad_tactic_args : string -> tactic_arg list -> 'a + +exception Bound + +(*s Primitive tactics. *) + +val introduction : identifier -> tactic +val refine : constr -> tactic +val convert_concl : constr -> tactic +val convert_hyp : identifier -> constr -> tactic +val thin : identifier list -> tactic +val mutual_fix : identifier list -> int list -> constr list -> tactic +val fix : identifier -> int -> tactic +val mutual_cofix : identifier list -> constr list -> tactic +val cofix : identifier -> tactic + +val dyn_mutual_fix : tactic_arg list -> tactic +val dyn_mutual_cofix : tactic_arg list -> tactic + +(*s Introduction tactics. *) + +val next_global_ident_away : identifier -> identifier list -> identifier + +val intro : tactic +val introf : tactic +val intro_force : bool -> tactic +val dyn_intro : tactic_arg list -> tactic + +val dyn_intro_move : tactic_arg list -> tactic + +val intro_replacing : identifier -> tactic +val intro_using : identifier -> tactic +val intro_using_warning : identifier -> tactic +val intros_using : identifier list -> tactic +val intro_erasing : identifier -> tactic + +val intros : tactic + +(*i Obsolete, subsumed by Elim.dyn_intro_pattern +val dyn_intros_using : tactic_arg list -> tactic +i*) + +val intros_until : identifier -> tactic +val dyn_intros_until : tactic_arg list -> tactic + +val intros_clearing : bool list -> tactic + +(*s Exact tactics. *) + +val assumption : tactic +val dyn_assumption : tactic_arg list -> tactic + +val exact : constr -> tactic +val dyn_exact : tactic_arg list -> tactic + +(*s Reduction tactics. *) + +val reduct_in_hyp : 'a reduction_function -> identifier -> tactic +val reduct_option : 'a reduction_function -> identifier option -> tactic +val reduct_in_concl : 'a reduction_function -> tactic +val change_in_concl : constr -> tactic + +val change_in_hyp : constr -> identifier -> tactic +val change_option : constr -> identifier option -> tactic +val red_in_concl : tactic +val red_in_hyp : identifier -> tactic +val red_option : identifier option -> tactic +val hnf_in_concl : tactic +val hnf_in_hyp : identifier -> tactic +val hnf_option : identifier option -> tactic +val simpl_in_concl : tactic +val simpl_in_hyp : identifier -> tactic +val simpl_option : identifier option -> tactic +val normalise_in_concl: tactic +val normalise_in_hyp : identifier -> tactic +val normalise_option : identifier option -> tactic +val unfold_in_concl : (int list * section_path) list -> tactic +val unfold_in_hyp : + (int list * section_path) list -> identifier -> tactic +val unfold_option : + (int list * section_path) list -> identifier option -> tactic +val reduce : red_expr -> identifier list -> tactic +val dyn_reduce : tactic_arg list -> tactic +val dyn_change : tactic_arg list -> tactic + +val unfold_constr : constr -> tactic +val pattern_option : + (int list * constr * constr) list -> identifier option -> tactic + +(*s Modification of the local context. *) + +val clear : identifier list -> tactic +val clear_one : identifier -> tactic +val dyn_clear : tactic_arg list -> tactic + +val clear_clauses : clause list -> tactic +val clear_clause : clause -> tactic + +val new_hyp : int option ->constr -> constr substitution -> tactic +val dyn_new_hyp : tactic_arg list -> tactic + +val dyn_move : tactic_arg list -> tactic +val dyn_move_dep : tactic_arg list -> tactic + +(*s Resolution tactics. *) + +val apply_type : constr -> constr list -> tactic +val apply_term : constr -> constr list -> tactic +val bring_hyps : clause list -> tactic + +val apply : constr -> tactic +val apply_without_reduce : constr -> tactic +val apply_list : constr list -> tactic +val apply_with_bindings : (constr * constr substitution) -> tactic +val dyn_apply : tactic_arg list -> tactic + +val cut_and_apply : constr -> tactic +val dyn_cut_and_apply : tactic_arg list -> tactic + +(*s Instantiation tactics. *) + +val instantiate_pf : int -> constr -> pftreestate -> pftreestate + +(*s Elimination tactics. *) + +val general_elim : constr * constr substitution -> + constr * constr substitution -> tactic +val default_elim : constr * constr substitution -> tactic +val simplest_elim : constr -> tactic +val dyn_elim : tactic_arg list -> tactic + +val induct : identifier -> tactic +val induct_nodep : int -> tactic +val dyn_induct : tactic_arg list -> tactic + +(*s Case analysis tactics. *) + +val general_case_analysis : constr * constr substitution -> tactic +val simplest_case : constr -> tactic +val dyn_case : tactic_arg list -> tactic + +val destruct : identifier -> tactic +val destruct_nodep : int -> tactic +val dyn_destruct : tactic_arg list -> tactic + +(*s Eliminations giving the type instead of the proof. *) + +val case_type : constr -> tactic +val dyn_case_type : tactic_arg list -> tactic + +val elim_type : constr -> tactic +val dyn_elim_type : tactic_arg list -> tactic + + +(*s Some eliminations which are frequently used. *) + +val impE : identifier -> tactic +val andE : identifier -> tactic +val orE : identifier -> tactic +val dImp : clause -> tactic +val dAnd : clause -> tactic +val dorE : bool -> clause ->tactic + + +(*s Introduction tactics. *) + +val constructor_checking_bound : int option -> int -> + constr substitution -> tactic +val one_constructor : int -> constr substitution -> tactic +val any_constructor : tactic +val left : constr substitution -> tactic +val simplest_left : tactic +val right : constr substitution -> tactic +val simplest_right : tactic +val split : constr substitution -> tactic +val simplest_split : tactic + +val dyn_constructor : tactic_arg list -> tactic +val dyn_left : tactic_arg list -> tactic +val dyn_right : tactic_arg list -> tactic +val dyn_split : tactic_arg list -> tactic + +(*s Logical connective tactics. *) + +val absurd : constr -> tactic +val dyn_absurd : tactic_arg list -> tactic + +val contradiction_on_hyp : identifier -> tactic +val contradiction : tactic +val dyn_contradiction : tactic_arg list -> tactic + +val reflexivity : tactic +val intros_reflexivity : tactic +val dyn_reflexivity : tactic_arg list -> tactic + +val symmetry : tactic +val intros_symmetry : tactic +val dyn_symmetry : tactic_arg list -> tactic + +val transitivity : constr -> tactic +val intros_transitivity : constr -> tactic +val dyn_transitivity : tactic_arg list -> tactic + +val cut : constr -> tactic +val cut_intro : constr -> tactic +val cut_replacing : identifier -> constr -> tactic +val cut_in_parallel : constr list -> tactic +val dyn_cut : tactic_arg list -> tactic +val dyn_lettac : tactic_arg list -> tactic + +val generalize : constr list -> tactic +val dyn_generalize : tactic_arg list -> tactic +val dyn_generalize_dep : tactic_arg list -> tactic + +val tclABSTRACT : identifier option -> tactic -> tactic |