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
49 [] -> fail (lazy "No goals under focus")
51 let goal = goal_of_loc (loc) in
54 let extract_conclusion_type status goal =
55 let gty = get_goalty status goal in
56 let ctx = ctx_of gty in
57 let status,gty = term_of_cic_term status gty ctx in
61 let alpha_eq_tacterm_kerterm ty t status goal =
62 let gty = get_goalty status goal in
63 let ctx = ctx_of gty in
64 let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
65 let (_,_,metasenv,subst,_) = status#obj in
66 let status,ty = term_of_cic_term status cicterm ctx in
67 if NCicReduction.alpha_eq status metasenv subst ctx t ty then
73 let are_convertible ty1 ty2 status goal =
74 let gty = get_goalty status goal in
75 let ctx = ctx_of gty in
76 let status,cicterm1 = disambiguate status ctx ty1 `XTNone in
77 let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
78 NTacStatus.are_convertible status ctx cicterm1 cicterm2
80 let clear_volatile_params_tac status =
81 match status#stack with
82 [] -> fail (lazy "Empty stack")
83 | (g,t,k,tag,p)::tl ->
84 let rec remove_volatile = function
86 | (k,v as hd')::tl' ->
87 let re = Str.regexp "volatile_.*" in
88 if Str.string_match re k 0 then
91 hd'::(remove_volatile tl')
93 let newp = remove_volatile p in
94 status#set_stack ((g,t,k,tag,newp)::tl)
97 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
98 the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
99 \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
101 let lambda_abstract_tac id t1 t2 status goal =
102 match extract_conclusion_type status goal with
103 | NCic.Prod (_,t,_) ->
104 if alpha_eq_tacterm_kerterm t1 t status goal then
108 block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
109 `JustOne))); clear_volatile_params_tac] status
111 let status,res = are_convertible t1 t2 status goal in
114 block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
115 `JustOne))); clear_volatile_params_tac] status
117 raise NotEquivalentTypes
120 | _ -> raise NotAProduct
122 let assume name ty eqty status =
123 let goal = extract_first_goal_from_status status in
124 try lambda_abstract_tac name ty eqty status goal
126 | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
127 | FirstTypeWrong -> fail (lazy "The assumed type is wrong")
128 | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
131 let suppose t1 id t2 status =
132 let goal = extract_first_goal_from_status status in
133 try lambda_abstract_tac id t1 t2 status goal
135 | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
136 | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise")
137 | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
140 let assert_tac t1 t2 status goal continuation =
141 let t = extract_conclusion_type status goal in
142 if alpha_eq_tacterm_kerterm t1 t status goal then
144 | None -> continuation
146 let status,res = are_convertible t1 t2 status goal in
147 if res then continuation
149 raise NotEquivalentTypes
153 let branch_dot_tac status =
154 match status#stack with
155 ([],t,k,tag,p) :: tl ->
156 if List.length t > 0 then
157 status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl)
163 let status_parameter key status =
164 match status#stack with
166 | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> ""
169 let beta_rewriting_step t status =
170 let ctx = status_parameter "volatile_context" status in
171 if ctx <> "beta_rewrite" then fail (lazy "Invalid use of 'or equivalently'")
173 change_tac ~where:("",0,(None,[],Some
174 Ast.UserInput)) ~with_what:t status
177 let done_continuation status =
178 let rec continuation l =
181 | (_,t,_,tag,p)::tl ->
182 if tag = `BranchTag then
183 if List.length t > 0 then
186 try List.assoc "context" p
189 ctx <> "induction" && ctx <> "cases"
191 if continue then [clear_volatile_params_tac;branch_dot_tac] else
192 [clear_volatile_params_tac]
194 [merge_tac] @ (continuation tl)
198 continuation status#stack
201 let bydone just status =
202 let goal = extract_first_goal_from_status status in
203 let continuation = done_continuation status in
204 let l = [mk_just status goal just] @ continuation in
208 let push_goals_tac status =
209 match status#stack with
210 [] -> fail (lazy "Error pushing goals")
211 | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl ->
212 if List.length g2 > 0 then
213 status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl)
214 else status (* Nothing to push *)
217 let add_parameter_tac key value status =
218 match status#stack with
220 | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
223 let we_need_to_prove t id t1 status =
224 let goal = extract_first_goal_from_status status in
229 | None -> (* We need to prove t *)
231 try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
233 | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
235 | Some t1 -> (* We need to prove t or equivalently t1 *)
237 try assert_tac t (Some t1) status goal (block_tac [change_tac ~where:("",0,(None,[],Some
240 add_parameter_tac "volatile_context"
241 "beta_rewrite"] status)
243 | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
244 | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
250 (* We need to prove t (id) *)
251 | None -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
254 (* We need to prove t (id) or equivalently t1 *)
255 | Some t1 -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some
257 ~with_what:t1; shift_tac; intro_tac id; merge_tac;
258 branch_tac; push_goals_tac
264 let by_just_we_proved just ty id ty' status =
265 let goal = extract_first_goal_from_status status in
266 let wrappedjust = just in
267 let just = mk_just status goal just in
271 | None -> (* just we proved P done *)
274 assert_tac ty None status goal (bydone wrappedjust status)
276 | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
277 | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
279 | Some ty' -> (* just we proved P that is equivalent to P' done *)
282 assert_tac ty' None status goal (block_tac [change_tac ~where:("",0,(None,[],Some
284 ~with_what:ty; bydone wrappedjust]
287 | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
288 | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
294 | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
295 clear_volatile_params_tac ] status
296 | Some ty' -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; change_tac
297 ~where:("",0,(None,[id,Ast.UserInput],None)) ~with_what:ty';
298 merge_tac; clear_volatile_params_tac] status
302 let existselim just id1 t1 t2 id2 status =
303 let goal = extract_first_goal_from_status status in
306 let just = mk_just status goal just in
308 cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
309 (id1,None), Some t1),t2)]));
310 branch_tac ~force:false;
314 intros_tac ~names_ref:(ref []) [id1;id2];
316 clear_volatile_params_tac
320 let andelim just t1 id1 t2 id2 status =
321 let goal = extract_first_goal_from_status status in
324 let just = mk_just status goal just in
326 cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
327 branch_tac ~force:false;
331 intros_tac ~names_ref:(ref []) [id1;id2];
333 clear_volatile_params_tac
337 let type_of_tactic_term status ctx t =
338 let status,cicterm = disambiguate status ctx t `XTNone in
339 let (_,cicty) = typeof status ctx cicterm in
342 let swap_first_two_goals_tac status =
344 match status#stack with
346 | (g,t,k,tag,p) :: s ->
348 | (loc1) :: (loc2) :: tl ->
349 ([loc2;loc1] @+ tl,t,k,tag,p) :: s
352 status#set_stack gstatus
354 let thesisbecomes t1 l = we_need_to_prove t1 None l
357 let obtain id t1 status =
358 let goal = extract_first_goal_from_status status in
359 let cicgty = get_goalty status goal in
360 let ctx = ctx_of cicgty in
361 let cicty = type_of_tactic_term status ctx t1 in
362 let _,ty = term_of_cic_term status cicty ctx in
364 block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
366 swap_first_two_goals_tac;
367 branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
368 add_parameter_tac "volatile_context" "rewrite"
373 let conclude t1 status =
374 let goal = extract_first_goal_from_status status in
375 let cicgty = get_goalty status goal in
376 let ctx = ctx_of cicgty in
377 let _,gty = term_of_cic_term status cicgty ctx in
379 NCic.Appl [_;_;plhs;_] ->
380 if alpha_eq_tacterm_kerterm t1 plhs status goal then
381 add_parameter_tac "volatile_context" "rewrite" status
383 fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
384 | _ -> fail (lazy "Your conclusion needs to be an equality")
387 let rewritingstep rhs just last_step status =
388 let ctx = status_parameter "volatile_context" status in
389 if ctx = "rewrite" then
391 let goal = extract_first_goal_from_status status in
392 let cicgty = get_goalty status goal in
393 let ctx = ctx_of cicgty in
394 let _,gty = term_of_cic_term status cicgty ctx in
395 let cicty = type_of_tactic_term status ctx rhs in
396 let _,ty = term_of_cic_term status cicty ctx in
397 let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
399 `Auto (univ, params) ->
401 if not (List.mem_assoc "timeout" params) then
402 ("timeout","3")::params
406 if not (List.mem_assoc "paramodulation" params) then
407 ("paramodulation","1")::params
410 if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
412 first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
413 ~params:(univ, params') status goal]
414 | `Term just -> apply_tac just
415 | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
418 let plhs,prhs,prepare =
419 match gty with (* Extracting the lhs and rhs of the previous equality *)
420 NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
421 | _ -> fail (lazy "You are not building an equaility chain")
425 (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
426 let todo = [just'] @ (done_continuation status) in
427 (* let todo = if mustdot status then List.append todo [dot_tac] else todo *)
431 let (_,_,rhs) = rhs in
432 block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
433 rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
438 fail (lazy "You are not building an equality chain")
441 let rec pp_metasenv_names (metasenv:NCic.metasenv) =
446 let meta_attrs,_,_ = conj in
447 let rec find_name_aux meta_attrs = match meta_attrs with
449 | hd :: tl -> match hd with
451 | _ -> find_name_aux tl
453 let name = find_name_aux meta_attrs
455 "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
458 let print_goals_names_tac s (status:#NTacStatus.tac_status) =
459 let (_,_,metasenv,_,_) = status#obj in
460 prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
462 (* Useful as it does not change the order in the list *)
463 let rec list_change_assoc k v = function
465 | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
468 let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
469 let add_name_to_goal name goal metasenv =
470 let (mattrs,ctx,t as conj) = try List.assoc goal metasenv with _ -> assert false in
471 let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
472 let newconj = (mattrs,ctx,t) in
473 list_change_assoc goal newconj metasenv
476 (* It's important that this tactic is called before branching and right after the creation of
477 * the new goals, when they are still under focus *)
478 match status#stack with
479 [] -> fail (lazy "Can not add names to an empty stack")
480 | (g,_,_,_,_) :: tl ->
481 let rec sublist n = function
483 | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
485 List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
487 let rec add_names_to_goals g cl metasenv =
490 | hd::tl, (_,consname,_)::tl' ->
491 add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
492 | _,_ -> fail (lazy "There are less goals than constructors")
494 let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
495 let newmetasenv = add_names_to_goals new_goals !cl metasenv
496 in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
499 let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
500 let remove_name_from_metaattrs =
501 List.filter (function `Name _ -> false | _ -> true) in
502 let rec add_names_to_metasenv cl metasenv =
503 match cl,metasenv with
505 | hd :: tl, mhd :: mtl ->
506 let _,consname,_ = hd in
507 let gnum,conj = mhd in
508 let mattrs,ctx,t = conj in
509 let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
511 let newconj = mattrs,ctx,t in
512 let newmeta = gnum,newconj in
513 newmeta :: (add_names_to_metasenv tl mtl)
514 | _,[] -> assert false
516 let newmetasenv = add_names_to_metasenv !cl metasenv in
517 status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
520 let unfocus_branch_tac status =
521 match status#stack with
523 | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
526 let we_proceed_by_induction_on t1 t2 status =
527 let goal = extract_first_goal_from_status status in
528 let txt,len,t1 = t1 in
529 let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
530 let indtyinfo = ref None in
531 let sort = ref (NCic.Rel 1) in
534 assert_tac t2 None status goal (block_tac [
535 analyze_indty_tac ~what:t1 indtyinfo;
536 sort_of_goal_tac sort;
538 let ity = HExtlib.unopt !indtyinfo in
539 let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
541 NUri.name_of_uri uri ^ "_" ^
542 snd (NCicElim.ast_of_sort
543 (match !sort with NCic.Sort x -> x | _ -> assert false))
546 let l = [Ast.Ident (name,None)] in
547 (* Generating an implicit for each argument of the inductive type, plus one the
548 * predicate, plus an implicit for each constructor of the inductive type *)
549 let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
555 exact_tac ("",0,eliminator) status);
556 add_names_to_goals_tac cl;
560 add_parameter_tac "context" "induction"
563 | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
566 let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status =
567 let goal = extract_first_goal_from_status status in
568 let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
569 let indtyinfo = ref None in
572 assert_tac t2 None status goal (block_tac [
573 analyze_indty_tac ~what:npt1 indtyinfo;
574 cases_tac ~what:t1 ~where:("",0,(None,[],Some
578 let ity = HExtlib.unopt !indtyinfo in
579 cl := ity.cl; add_names_to_goals_tac cl status
581 branch_tac; push_goals_tac;
583 add_parameter_tac "context" "cases"
586 | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
589 let byinduction t1 id = suppose t1 id None ;;
591 let name_of_conj conj =
592 let mattrs,_,_ = conj in
593 let rec search_name mattrs =
599 | _ -> search_name tl
603 let rec loc_of_goal goal l =
605 [] -> fail (lazy "Reached the end")
608 let g = goal_of_switch sw in
610 else loc_of_goal goal tl
613 let has_focused_goal status =
614 match status#stack with
616 | ([],_,_,_,_) :: tl -> false
620 let focus_on_case_tac case status =
621 let (_,_,metasenv,_,_) = status#obj in
622 let rec goal_of_case case metasenv =
624 [] -> fail (lazy "The given case does not exist")
625 | (goal,conj) :: tl ->
626 if name_of_conj conj = case then goal
627 else goal_of_case case tl
629 let goal_to_focus = goal_of_case case metasenv in
631 match status#stack with
632 [] -> fail (lazy "There is nothing to prove")
633 | (g,t,k,tag,p) :: s ->
636 loc_of_goal goal_to_focus t
637 with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
640 let curloc = if has_focused_goal status then
641 let goal = extract_first_goal_from_status status in
645 (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
647 status#set_stack gstatus
650 let case id l status =
651 let ctx = status_parameter "context" status in
652 if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
653 induction/cases analysis context")
656 if has_focused_goal status then fail (lazy "Finish the current case before switching")
660 let goal = extract_first_goal_from_status status in
661 let (_,_,metasenv,_,_) = status#obj in
662 let conj = NCicUtils.lookup_meta goal metasenv in
663 let name = name_of_conj conj in
670 (try_tac (assume id ("",0,ty) None)) :: (aux tl)
674 (* if name = id then block_tac continuation status *)
676 block_tac ([focus_on_case_tac id] @ continuation) status
681 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
683 (* vim: ts=2: sw=0: et: