-let existselim just id1 t1 t2 id2 =
- let aux (proof, goal) =
- let (n,metasenv,_subst,bo,ty,attrs) = proof in
- let metano,context,_ = CicUtil.lookup_meta goal metasenv in
- let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
- let proof' = (n,metasenv,_subst,bo,ty,attrs) in
- ProofEngineTypes.apply_tactic (
- Tacticals.thens
- ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
- ~continuations:
- [ Tactics.elim_intros (Cic.Rel 1)
- ~mk_fresh_name_callback:
- (let i = ref 0 in
- fun _ _ _ ~typ ->
- incr i;
- if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
- (mk_just ~dbd ~automation_cache just)
- ]) (proof', goal)
- in
- ProofEngineTypes.mk_tactic aux
-;;
-
-let andelim just t1 id1 t2 id2 =
- Tacticals.thens
- ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2]))
- ~continuations:
- [ Tactics.elim_intros (Cic.Rel 1)
- ~mk_fresh_name_callback:
- (let i = ref 0 in
- fun _ _ _ ~typ ->
- incr i;
- if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
- (mk_just ~dbd ~automation_cache just) ]
-;;
- *)
+ 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 lhs with
+ None -> (* = E2 *)
+ let plhs,prhs =
+ match gty with (* Extracting the lhs and rhs of the previous equality *)
+ NCic.Appl [_;_;plhs;prhs] -> plhs,prhs
+ | _ -> fail (lazy "You are not building an equaility chain")
+ in
+ plhs,prhs,
+ (fun continuation -> continuation status)
+ | Some (None,lhs) -> (* conclude *)
+ let plhs,prhs =
+ match gty with
+ NCic.Appl [_;_;plhs;prhs] -> plhs,prhs
+ | _ -> fail (lazy "You are not building an equaility chain")
+ in
+ (*TODO*)
+ (*CSC: manca check plhs convertibile con lhs *)
+ plhs,prhs,
+ (fun continuation -> continuation status)
+ | Some (Some name,lhs) -> (* obtain *)
+ NCic.Rel 1, NCic.Rel 1, (* continuation for this case is gonna be ignored, so it doesn't
+ matter what the values of these two are *)
+ (fun continuation ->
+ let (_,_,lhs) = lhs in
+ block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; lhs; Ast.Implicit
+ `JustOne]));
+ swap_first_two_goals_tac;
+ branch_tac; shift_tac; shift_tac; intro_tac name; merge_tac; dot_tac;
+(*
+ change_tac ~where:("",0,(None,[],Some Ast.Appl[Ast.Implicit `JustOne;Ast.Implicit
+ `JustOne; Ast.UserInput; Ast.Implicit `JustOne]))
+ ~with_what:rhs
+*)
+ ]
+ status
+ )
+ 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
+;;
+ *)
+
+let we_proceed_by_cases_on t1 t2 status =
+ let goal = extract_first_goal_from_status status in
+ try
+ assert_tac t2 None status goal (block_tac [cases_tac ~what:t1 ~where:("",0,(None,[],Some
+ Ast.UserInput));
+ dot_tac] status)
+ with
+ | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+
+let we_proceed_by_induction_on t1 t2 status =
+ let goal = extract_first_goal_from_status status in
+ try
+ assert_tac t2 None status goal (block_tac [elim_tac ~what:t1 ~where:("",0,(None,[],Some
+ Ast.UserInput));
+ dot_tac] status)
+ with
+ | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let byinduction t1 id = suppose t1 id None ;;
+
+let case id l =
+ distribute_tac (fun status goal ->
+ let rec aux l =
+ match l with
+ [] -> [id_tac]
+ | (id,ty)::tl ->
+ (try_tac (assume id ("",0,ty) None)) :: (aux tl)
+ in
+(* if l == [] then exec (try_tac (intro_tac "H")) status goal *)
+(* else *)
+ exec (block_tac (aux l)) status goal
+ )
+;;
+
+let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
+
+(* vim: ts=2: sw=0: et:
+ * *)