+let swap_first_two_goals_tac status =
+ let gstatus =
+ match status#stack with
+ | [] -> assert false
+ | (g,t,k,tag) :: s ->
+ match g with
+ | (loc1) :: (loc2) :: tl ->
+ ([loc2;loc1] @+ tl,t,k,tag) :: s
+ | _ -> assert false
+ in
+ status#set_stack gstatus
+
+let thesisbecomes t1 t2 = we_need_to_prove t1 None t2
+;;
+
+let obtain id t1 status =
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let cicty = type_of_tactic_term status ctx t1 in
+ let _,ty = term_of_cic_term status cicty ctx in
+ let (_,_,t1) = t1 in
+ block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
+ `JustOne]));
+ swap_first_two_goals_tac;
+ branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; dot_tac;
+ ]
+ status
+;;
+
+let conclude t1 =
+ distribute_tac (fun status goal ->
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let _,gty = term_of_cic_term status cicgty ctx in
+ match gty with
+ NCic.Appl [_;_;plhs;_] ->
+ if alpha_eq_tacterm_kerterm t1 plhs status goal then
+ exec id_tac status goal
+ else
+ fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
+ | _ -> fail (lazy "Your conclusion needs to be an equality")
+ )
+;;
+
+let rewritingstep rhs just last_step status =
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let _,gty = term_of_cic_term status cicgty ctx in
+ let cicty = type_of_tactic_term status ctx rhs in
+ let _,ty = term_of_cic_term status cicty ctx in
+ let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
+ match just with
+ `Auto (univ, params) ->
+ let params =
+ if not (List.mem_assoc "timeout" params) then
+ ("timeout","3")::params
+ else params
+ in
+ let params' =
+ if not (List.mem_assoc "paramodulation" params) then
+ ("paramodulation","1")::params
+ else params
+ in
+ if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
+ else
+ first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
+ ~params:(univ, params') status goal]
+ | `Term just -> apply_tac just
+ | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
+ | `Proof -> id_tac
+ in
+ let plhs,prhs,prepare =
+ match gty with (* Extracting the lhs and rhs of the previous equality *)
+ NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
+ | _ -> fail (lazy "You are not building an equaility chain")
+ in
+ let continuation =
+ if last_step then
+ (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
+ let todo = [just'] in
+ let todo = if mustdot status then List.append todo [dot_tac] else todo
+ in
+ block_tac todo
+ else
+ let (_,_,rhs) = rhs in
+ block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
+ rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
+ in
+ prepare continuation
+;;
+
+(*