+let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
+ let add_name_to_goal name goal metasenv =
+ let (mattrs,ctx,t) = try List.assoc goal metasenv with _ -> assert false in
+ let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
+ let newconj = (mattrs,ctx,t) in
+ list_change_assoc goal newconj metasenv
+ in
+ let new_goals =
+ (* It's important that this tactic is called before branching and right after the creation of
+ * the new goals, when they are still under focus *)
+ match status#stack with
+ [] -> fail (lazy "Can not add names to an empty stack")
+ | (g,_,_,_,_) :: _tl ->
+ let rec sublist n = function
+ [] -> []
+ | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
+ in
+ List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+ in
+ let rec add_names_to_goals g cl metasenv =
+ match g,cl with
+ [],[] -> metasenv
+ | hd::tl, (_,consname,_)::tl' ->
+ add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
+ | _,_ -> fail (lazy "There are less goals than constructors")
+ in
+ let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+ let newmetasenv = add_names_to_goals new_goals !cl metasenv
+ in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
+;;
+(*
+ let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+ let remove_name_from_metaattrs =
+ List.filter (function `Name _ -> false | _ -> true) in
+ let rec add_names_to_metasenv cl metasenv =
+ match cl,metasenv with
+ [],_ -> metasenv
+ | hd :: tl, mhd :: mtl ->
+ let _,consname,_ = hd in
+ let gnum,conj = mhd in
+ let mattrs,ctx,t = conj in
+ let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
+ in
+ let newconj = mattrs,ctx,t in
+ let newmeta = gnum,newconj in
+ newmeta :: (add_names_to_metasenv tl mtl)
+ | _,[] -> assert false
+ in
+ let newmetasenv = add_names_to_metasenv !cl metasenv in
+ status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
+*)
+
+let unfocus_branch_tac status =
+ match status#stack with
+ [] -> status
+ | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
+;;
+
+let we_proceed_by_induction_on t1 t2 status =
+ let goal = extract_first_goal_from_status status in
+ let txt,len,t1 = t1 in
+ let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
+ let indtyinfo = ref None in
+ let sort = ref (NCic.Rel 1) in
+ let cl = ref [] in (* this is a ref on purpose, as the block of code after sort_of_goal_tac in
+ block_tac acts as a block of asynchronous code, in which cl gets modified with the info retrieved
+ with analize_indty_tac, and later used to label each new goal with a costructor name. Using a
+ plain list this doesn't seem to work, as add_names_to_goals_tac would immediately act on an empty
+ list, instead of acting on the list of constructors *)
+ try
+ assert_tac t2 None status goal (block_tac [
+ analyze_indty_tac ~what:t1 indtyinfo;
+ sort_of_goal_tac sort;
+ (fun status ->
+ let ity = HExtlib.unopt !indtyinfo in
+ let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
+ let name =
+ NUri.name_of_uri uri ^ "_" ^
+ snd (NCicElim.ast_of_sort
+ (match !sort with NCic.Sort x -> x | _ -> assert false))
+ in
+ let eliminator =
+ let l = [Ast.Ident (name,None)] in
+ (* Generating an implicit for each argument of the inductive type, plus one the
+ * predicate, plus an implicit for each constructor of the inductive type *)
+ let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
+ let _,_,t1 = t1 in
+ let l = l @ [t1] in
+ Ast.Appl l
+ in
+ cl := ity.cl;
+ exact_tac ("",0,eliminator) status);
+ add_names_to_goals_tac cl;
+ branch_tac;
+ push_goals_tac;
+ unfocus_branch_tac;
+ add_parameter_tac "context" "induction"
+ ] status)
+ with
+ | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status =
+ let goal = extract_first_goal_from_status status in
+ let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
+ let indtyinfo = ref None in
+ let cl = ref [] in
+ try
+ assert_tac t2 None status goal (block_tac [
+ analyze_indty_tac ~what:npt1 indtyinfo;
+ cases_tac ~what:t1 ~where:("",0,(None,[],Some
+ Ast.UserInput));
+ (
+ fun status ->
+ let ity = HExtlib.unopt !indtyinfo in
+ cl := ity.cl; add_names_to_goals_tac cl status
+ );
+ branch_tac; push_goals_tac;
+ unfocus_branch_tac;
+ add_parameter_tac "context" "cases"
+ ] status)
+ with
+ | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let byinduction t1 id status =
+ let ctx = status_parameter "context" status in
+ if ctx <> "induction" then fail (lazy "You can't use this tactic outside of an induction context")
+ else suppose t1 id status