1 (* Copyright (C) 2019, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 open Continuationals.Stack
27 module Ast = NotationPt
31 type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ]
33 let mk_just status goal =
35 `Auto (l,params) -> NnAuto.auto_lowtac ~params:(l,params) status goal
36 | `Term t -> apply_tac t
39 exception FirstTypeWrong
40 exception NotEquivalentTypes
42 let extract_first_goal_from_status status =
43 let s = status#stack in
45 | [] -> fail (lazy "There's nothing to prove")
46 | (g1, _, k, tag1) :: tl ->
47 let goals = filter_open g1 in
48 let (loc::tl) = goals in
49 let goal = goal_of_loc (loc) in
52 let extract_conclusion_type status goal =
53 let gty = get_goalty status goal in
54 let ctx = ctx_of gty in
55 let status,gty = term_of_cic_term status gty ctx in
59 let alpha_eq_tacterm_kerterm ty t status goal =
60 let gty = get_goalty status goal in
61 let ctx = ctx_of gty in
62 let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
63 let (_,_,metasenv,subst,_) = status#obj in
64 let status,ty = term_of_cic_term status cicterm ctx in
65 if NCicReduction.alpha_eq status metasenv subst ctx t ty then
71 let are_convertible ty1 ty2 status goal =
72 let gty = get_goalty status goal in
73 let ctx = ctx_of gty in
74 let status,cicterm1 = disambiguate status ctx ty1 `XTNone in
75 let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
76 NTacStatus.are_convertible status ctx cicterm1 cicterm2
78 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
79 the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
80 \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
82 let lambda_abstract_tac id t1 t2 status goal =
83 match extract_conclusion_type status goal with
84 | NCic.Prod (_,t,_) ->
85 if alpha_eq_tacterm_kerterm t1 t status goal then
89 exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
90 `JustOne))) (*status*)
92 let status,res = are_convertible t1 t2 status goal in
95 exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
96 `JustOne))) (*status*)
98 raise NotEquivalentTypes
101 | _ -> raise NotAProduct
103 let assume name ty eqty =
104 distribute_tac (fun status goal ->
105 try exec (lambda_abstract_tac name ty eqty status goal) status goal
107 | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
108 | FirstTypeWrong -> fail (lazy "The assumed type is wrong")
109 | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
113 let suppose t1 id t2 =
114 distribute_tac (fun status goal ->
115 try exec (lambda_abstract_tac id t1 t2 status goal) status goal
117 | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
118 | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise")
119 | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
123 let assert_tac t1 t2 status goal continuation =
124 let t = extract_conclusion_type status goal in
125 if alpha_eq_tacterm_kerterm t1 t status goal then
127 | None -> continuation
129 let status,res = are_convertible t1 t2 status goal in
130 if res then continuation
132 raise NotEquivalentTypes
137 let s = status#stack in
139 | [] -> fail (lazy "No goals to dot")
140 | (_, _, k, _) :: tl ->
141 if List.length k > 0 then
146 let bydone just status =
147 let goal = extract_first_goal_from_status status in
148 let mustdot = mustdot status in
149 let l = [mk_just status goal just] in
151 if mustdot then List.append l [dot_tac] else l
156 let we_need_to_prove t id t1 status =
157 let goal = extract_first_goal_from_status status in
162 | None -> (* We need to prove t *)
164 try assert_tac t None status goal (id_tac status)
166 | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
168 | Some t1 -> (* We need to prove t or equivalently t1 *)
170 try assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some
171 Ast.UserInput)) ~with_what:t1 status)
173 | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
174 | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
180 (* We need to prove t (id) *)
181 | None -> block_tac [cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac;
184 (* We need to prove t (id) or equivalently t1 *)
185 | Some t1 -> block_tac [cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some
187 ~with_what:t1; shift_tac; intro_tac id; merge_tac;
194 let by_just_we_proved just ty id ty' status =
195 let goal = extract_first_goal_from_status status in
196 let wrappedjust = just in
197 let just = mk_just status goal just in
201 | None -> (* just we proved P done *)
204 assert_tac ty None status goal (bydone wrappedjust status)
206 | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
207 | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
209 | Some ty' -> (* just we proved P that is equivalent to P' done *)
212 assert_tac ty' None status goal (block_tac [change_tac ~where:("",0,(None,[],Some
214 ~with_what:ty; bydone wrappedjust]
217 | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
218 | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
224 | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac ] status
225 | Some ty' -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; change_tac
226 ~where:("",0,(None,[id,Ast.UserInput],None)) ~with_what:ty';
231 let existselim just id1 t1 t2 id2 =
232 distribute_tac (fun status goal ->
235 let just = mk_just status goal just in
237 cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
238 (id1,None), Some t1),t2)]));
239 branch_tac ~force:false;
243 intros_tac ~names_ref:(ref []) [id1;id2];
249 let andelim just t1 id1 t2 id2 =
250 distribute_tac (fun status goal ->
253 let just = mk_just status goal just in
255 cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
256 branch_tac ~force:false;
260 intros_tac ~names_ref:(ref []) [id1;id2];
266 let type_of_tactic_term status ctx t =
267 let status,cicterm = disambiguate status ctx t `XTNone in
268 let (_,cicty) = typeof status ctx cicterm in
271 let swap_first_two_goals_tac status =
273 match status#stack with
275 | (g,t,k,tag) :: s ->
277 | (loc1) :: (loc2) :: tl ->
278 ([loc2;loc1] @+ tl,t,k,tag) :: s
281 status#set_stack gstatus
283 let thesisbecomes t1 t2 = we_need_to_prove t1 None t2
286 let obtain id t1 status =
287 let goal = extract_first_goal_from_status status in
288 let cicgty = get_goalty status goal in
289 let ctx = ctx_of cicgty in
290 let cicty = type_of_tactic_term status ctx t1 in
291 let _,ty = term_of_cic_term status cicty ctx in
293 block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
295 swap_first_two_goals_tac;
296 branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; dot_tac;
302 distribute_tac (fun status goal ->
303 let cicgty = get_goalty status goal in
304 let ctx = ctx_of cicgty in
305 let _,gty = term_of_cic_term status cicgty ctx in
307 NCic.Appl [_;_;plhs;_] ->
308 if alpha_eq_tacterm_kerterm t1 plhs status goal then
309 exec id_tac status goal
311 fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
312 | _ -> fail (lazy "Your conclusion needs to be an equality")
316 let rewritingstep rhs just last_step status =
317 let goal = extract_first_goal_from_status status in
318 let cicgty = get_goalty status goal in
319 let ctx = ctx_of cicgty in
320 let _,gty = term_of_cic_term status cicgty ctx in
321 let cicty = type_of_tactic_term status ctx rhs in
322 let _,ty = term_of_cic_term status cicty ctx in
323 let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
325 `Auto (univ, params) ->
327 if not (List.mem_assoc "timeout" params) then
328 ("timeout","3")::params
332 if not (List.mem_assoc "paramodulation" params) then
333 ("paramodulation","1")::params
336 if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
338 first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
339 ~params:(univ, params') status goal]
340 | `Term just -> apply_tac just
341 | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
344 let plhs,prhs,prepare =
345 match gty with (* Extracting the lhs and rhs of the previous equality *)
346 NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
347 | _ -> fail (lazy "You are not building an equaility chain")
351 (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
352 let todo = [just'] in
353 let todo = if mustdot status then List.append todo [dot_tac] else todo
357 let (_,_,rhs) = rhs in
358 block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
359 rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
364 let rec pp_metasenv_names (metasenv:NCic.metasenv) =
369 let meta_attrs,_,_ = conj in
370 let rec find_name_aux meta_attrs = match meta_attrs with
372 | hd :: tl -> match hd with
374 | _ -> find_name_aux tl
376 let name = find_name_aux meta_attrs
378 "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
381 let print_goals_names_tac s (status:#NTacStatus.tac_status) =
382 let (_,_,metasenv,_,_) = status#obj in
383 prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
385 let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
386 let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
387 let rec remove_name_from_metaattrs mattrs =
392 `Name n -> remove_name_from_metaattrs tl
393 | _ as it -> it :: (remove_name_from_metaattrs tl)
395 let rec add_names_to_metasenv cl metasenv =
399 let _,consname,_ = hd
400 in match metasenv with
403 let gnum,conj = mhd in
404 let mattrs,ctx,t = conj in
405 let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
407 let newconj = mattrs,ctx,t in
408 let newmeta = gnum,newconj in
409 newmeta :: (add_names_to_metasenv tl mtl)
411 let newmetasenv = add_names_to_metasenv !cl metasenv in
412 status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
414 let we_proceed_by_induction_on t1 t2 status =
415 let goal = extract_first_goal_from_status status in
416 let txt,len,t1 = t1 in
417 let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
418 let indtyinfo = ref None in
419 let sort = ref (NCic.Rel 1) in
422 assert_tac t2 None status goal (block_tac [
423 analyze_indty_tac ~what:t1 indtyinfo;
424 sort_of_goal_tac sort;
426 let ity = HExtlib.unopt !indtyinfo in
427 let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
429 NUri.name_of_uri uri ^ "_" ^
430 snd (NCicElim.ast_of_sort
431 (match !sort with NCic.Sort x -> x | _ -> assert false))
434 let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in
435 (* Generating as many implicits as open goals *)
436 let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in
442 exact_tac ("",0,eliminator) status);
443 add_names_to_goals_tac cl; dot_tac] status)
445 | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
448 let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status =
449 let goal = extract_first_goal_from_status status in
450 let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
451 let indtyinfo = ref None in
454 assert_tac t2 None status goal (block_tac [
455 analyze_indty_tac ~what:npt1 indtyinfo;
456 cases_tac ~what:t1 ~where:("",0,(None,[],Some
458 print_goals_names_tac "Pre Adding";
461 let ity = HExtlib.unopt !indtyinfo in
462 cl := ity.cl; add_names_to_goals_tac cl status
464 print_goals_names_tac "Post Adding";
467 | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
470 let byinduction t1 id = suppose t1 id None ;;
472 let name_of_conj conj =
473 let mattrs,_,_ = conj in
474 let rec search_name mattrs =
480 | _ -> search_name tl
484 let rec loc_of_goal goal l =
486 [] -> fail (lazy "Reached the end")
489 let g = goal_of_switch sw in
491 else loc_of_goal goal tl
494 let focus_on_case_tac case status =
495 let goal = extract_first_goal_from_status status in
496 let (_,_,metasenv,_,_) = status#obj in
497 let rec goal_of_case case metasenv =
499 [] -> fail (lazy "The given case does not exist")
500 | (goal,conj) :: tl ->
501 if name_of_conj conj = case then goal
502 else goal_of_case case tl
504 let goal_to_focus = goal_of_case case metasenv in
506 match status#stack with
507 [] -> fail (lazy "There is nothing to prove")
508 | (g,t,k,tag) :: s ->
509 let loc = loc_of_goal goal_to_focus k in
510 let curloc = loc_of_goal goal g in
511 (((g @- [curloc]) @+ [loc]),t,([curloc] @+ (k @- [loc])),tag) :: s
512 in status#set_stack gstatus
514 let case id l status =
515 let goal = extract_first_goal_from_status status in
516 let (_,_,metasenv,_,_) = status#obj in
517 let conj = NCicUtils.lookup_meta goal metasenv in
518 let name = name_of_conj conj in
524 (try_tac (assume id ("",0,ty) None)) :: (aux tl)
528 if name = id then block_tac continuation status
529 else block_tac ([focus_on_case_tac id] @ continuation) status
532 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
534 (* vim: ts=2: sw=0: et: