From 5cfd68a5d9e73edb40e1cfe021a1426354767aa8 Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Sun, 19 May 2019 19:00:13 +0200 Subject: [PATCH] Many changes Add a BetaRewritingStep tactic, for multiple 'or equivalently' statements in theorems proofs Remove old code Add a key-value list to the tiny-cals stack (parameters list) for context related infos. Can be used as a general purpose store for key-value pairs Adapt code that works on the stack to work with the new parameter list Add function to add and retrieve key-value pairs to the parameters list Add the concept of volatile-context: they are contexts that are cleared after the application of some tactics. E.g., the context for a beta_rewriting (sequence of 'or equivalently') is a volatile context, as any tactic breaks the chain Add a function to clear volatile parameters from the paramters list Add a case in extract_first_goal_from_status for the case where the stack is empty Make the tactics that make use of distribute High tactics Reimplement the dot tac on top of the stack to handle branching. This makes use of the second iterator list of the stack Add a "done_continuation" function that checks whether it needs to dot or recursively merge branches after a done statement Add a function to push goals from the focus iterator list of the previous level on the stack to the second iteretaor list of the current level Change conclude and obtain to use a volatile context to obligate the user to only use = inside it Change the add_names_to_goals function to use the stack instead of the metasenv directly Add a unfocus_branch_tac to unfocus from goals in a stack level (useful for cases and induction) Change induction and cases to use a context to obligate the user to use case only inside it. Furthermore, the new stack based branching for declarative tactics obligates the user to only switch between cases of the last level Change induction and cases to start without focusing on any goal and without automatically focusing on the next goal after a done. The user is compelled to use case to switch between each case Change the case to only change case when the current case has been dealt with Attempt to fix automation Add first draft for matita's helper --- matita/components/grafite/grafiteAst.ml | 1 + matita/components/grafite/grafiteAstPp.ml | 29 +- .../grafite_engine/grafiteEngine.ml | 7 +- .../grafite_parser/grafiteParser.ml | 7 +- .../components/ng_tactics/continuationals.ml | 79 +-- .../components/ng_tactics/continuationals.mli | 5 +- matita/components/ng_tactics/declarative.ml | 505 ++++++++++------ matita/components/ng_tactics/declarative.mli | 1 + matita/components/ng_tactics/nTactics.ml | 54 +- matita/components/ng_tactics/nnAuto.ml | 81 ++- .../matita/help/C/sec_declarative_tactics.xml | 561 ++++++++++-------- 11 files changed, 772 insertions(+), 558 deletions(-) diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index c4ec503c7..c29babd55 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -85,6 +85,7 @@ type ntactic = justification, conclusion, identifier, eqconcl *) | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion, identifier, equivnewcon *) + | BetaRewritingStep of loc * nterm | Bydone of loc * just | ExistsElim of loc * just * string * nterm * nterm * string | AndElim of loc * just * nterm * string * nterm * string diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index a4a5788d9..e8864255d 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -127,17 +127,20 @@ let rec pp_ntactic status ~map_unicode_to_tex = | By_just_we_proved (_, just, term1, ident, term2) -> pp_just status just ^ "we proved" ^ NotationPp.pp_term status term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match term2 with None -> " " | Some term2 -> " that is equivalent to " ^ NotationPp.pp_term status term2) - | We_need_to_prove (_,term,ident,term1) -> "we need to prove" ^ NotationPp.pp_term status term ^ - (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match term1 with None -> " " | Some t1 - -> "or equivalently" ^ NotationPp.pp_term status t1) + | We_need_to_prove (_,term,ident,t) -> "we need to prove" ^ NotationPp.pp_term status term ^ + (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match t with None -> "" | Some t -> + " or equivalently " ^ (NotationPp.pp_term status t)) + | BetaRewritingStep (_,t) -> "or equivalently " ^ (NotationPp.pp_term status t) | Bydone (_, just) -> pp_just status just ^ "done" | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":" ^ NotationPp.pp_term status term ^ "such that " ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")" | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^ NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2 ^ " (" ^ ident2 ^ ")" - | Thesisbecomes (_, term1, term2) -> "the thesis becomes " ^ NotationPp.pp_term status term1 ^ (match - term2 with None -> " " | Some term2 -> NotationPp.pp_term status term2) + | Thesisbecomes (_, t, t1) -> "the thesis becomes " ^ NotationPp.pp_term status t ^ + (match t1 with None -> "" | Some t1 -> " or equivalently " ^ + NotationPp.pp_term status + t1) | RewritingStep (_, rhs, just, cont) -> "=" ^ NotationPp.pp_term status rhs ^ @@ -147,22 +150,6 @@ let rec pp_ntactic status ~map_unicode_to_tex = | `Proof -> " proof" | `SolveWith t -> " using " ^ NotationPp.pp_term status t) ^ (if cont then " done" else "") -(* - | RewritingStep (_, term, term1, term2, cont) -> - (match term with - | None -> " " - | Some (None,term) -> "conclude " ^ NotationPp.pp_term status term - | Some (Some name,term) -> - "obtain (" ^ name ^ ") " ^ NotationPp.pp_term status term) - ^ "=" ^ - NotationPp.pp_term status term1 ^ - (match term2 with - | `Auto params -> pp_auto_params params status - | `Term term2 -> " exact " ^ NotationPp.pp_term status term2 - | `Proof -> " proof" - | `SolveWith term -> " using " ^ NotationPp.pp_term status term) - ^ (if cont then " done" else "") -*) | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ NotationPp.pp_term status t1 | Conclude (_,t1) -> "conclude " ^ NotationPp.pp_term status t1 | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ NotationPp.pp_term status term ^ "to prove" ^ NotationPp.pp_term status term1 diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index f2876d2a9..ee0573ae7 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -499,8 +499,9 @@ let eval_ng_tac tac = |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2))) - |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id - (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2)) + |GrafiteAst.We_need_to_prove (_, t, id, t1) -> Declarative.we_need_to_prove (text,prefix_len,t) id + (match t1 with None -> None | Some t1 -> Some (text,prefix_len,t1)) + |GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t) | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len) | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) -> Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1) @@ -508,7 +509,7 @@ let eval_ng_tac tac = | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2 | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1) - (match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2))) + (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2)) | GrafiteAst.RewritingStep (_,rhs,just,cont) -> Declarative.rewritingstep (text,prefix_len,rhs) (match just with diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index eaf0c4c01..5acdf2bd0 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -267,10 +267,13 @@ EXTEND | BYC_wehaveand (id1,t1,id2,t2) -> G.AndElim (loc, just, t1, id1, t2, id2)) ]) - | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = +IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> +t']-> G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)]) + | IDENT "or"; IDENT "equivalently"; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)]) | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT - "equivalently"; t2 = tactic_term -> t2] -> +"equivalently"; t2 = tactic_term -> t2] -> G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)]) | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)]) diff --git a/matita/components/ng_tactics/continuationals.ml b/matita/components/ng_tactics/continuationals.ml index b10877130..5538a3c2d 100644 --- a/matita/components/ng_tactics/continuationals.ml +++ b/matita/components/ng_tactics/continuationals.ml @@ -35,21 +35,23 @@ let fail msg = raise (Error msg) type goal = int +type parameters = (string * string) list + module Stack = struct type switch = Open of goal | Closed of goal type locator = int * switch type tag = [ `BranchTag | `FocusTag | `NoTag ] - type entry = locator list * locator list * locator list * tag + type entry = locator list * locator list * locator list * tag * parameters type t = entry list - let empty = [ [], [], [], `NoTag ] + let empty = [ [], [], [], `NoTag , []] let fold ~env ~cont ~todo init stack = let rec aux acc depth = function | [] -> acc - | (locs, todos, conts, tag) :: tl -> + | (locs, todos, conts, tag, p) :: tl -> let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in @@ -64,10 +66,10 @@ struct let map ~env ~cont ~todo = let depth = ref ~-1 in List.map - (fun (s, t, c, tag) -> + (fun (s, t, c, tag, p) -> incr depth; let d = !depth in - env d tag s, todo d tag t, cont d tag c, tag) + env d tag s, todo d tag t, cont d tag c, tag, p) let is_open = function _, Open _ -> true | _ -> false let close = function n, Open g -> n, Closed g | l -> l @@ -103,39 +105,39 @@ struct let rec find_goal = function | [] -> raise (Failure "Continuationals.find_goal") - | (l :: _, _ , _ , _) :: _ -> goal_of_loc l - | ( _ , _ , l :: _, _) :: _ -> goal_of_loc l - | ( _ , l :: _, _ , _) :: _ -> goal_of_loc l + | (l :: _, _ , _ , _, _) :: _ -> goal_of_loc l + | ( _ , _ , l :: _, _, _) :: _ -> goal_of_loc l + | ( _ , l :: _, _ , _, _) :: _ -> goal_of_loc l | _ :: tl -> find_goal tl let is_empty = function | [] -> assert false - | [ [], [], [], `NoTag ] -> true + | [ [], [], [], `NoTag , _] -> true | _ -> false let of_nmetasenv metasenv = let goals = List.map (fun (g, _) -> g) metasenv in - [ zero_pos goals, [], [], `NoTag ] + [ zero_pos goals, [], [], `NoTag , []] let head_switches = function - | (locs, _, _, _) :: _ -> List.map switch_of_loc locs + | (locs, _, _, _, _) :: _ -> List.map switch_of_loc locs | [] -> assert false let head_goals = function - | (locs, _, _, _) :: _ -> List.map goal_of_loc locs + | (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs | [] -> assert false let head_tag = function - | (_, _, _, tag) :: _ -> tag + | (_, _, _, tag, _) :: _ -> tag | [] -> assert false let shift_goals = function - | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs + | _ :: (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs | [] -> assert false | _ -> [] @@ -163,9 +165,10 @@ struct let pp_loc (i, s) = string_of_int i ^ pp_switch s in let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in - let pp_stack_entry (env, todo, cont, tag) = - sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont) - (pp_tag tag) + let pp_par = function [] -> "" | _ as l -> List.fold_left (fun acc (k,v) -> acc ^ "K: " ^ k ^ " V: " ^ v ^ "; ") "" l in + let pp_stack_entry (env, todo, cont, tag, parameters) = + sprintf "(%s, %s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont) + (pp_tag tag) (pp_par parameters) in String.concat " :: " (List.map pp_stack_entry stack) end @@ -270,7 +273,7 @@ struct let ostatus, stack = match cmd, stack with | _, [] -> assert false - | Tactical tac, (g, t, k, tag) :: s -> + | Tactical tac, (g, t, k, tag, p) :: s -> (* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A * auto paramodulation.try assumption. * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO. @@ -300,49 +303,49 @@ struct debug_print (lazy ("closed: " ^ String.concat " " (List.map string_of_int gcn))); let stack = - (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s + (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s in sn, stack - | Dot, ([], _, [], _) :: _ -> + | Dot, ([], _, [], _, _) :: _ -> (* backward compatibility: do-nothing-dot *) new_stack stack - | Dot, (g, t, k, tag) :: s -> + | Dot, (g, t, k, tag, p) :: s -> (match filter_open g, k with - | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s) + | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag, p) :: s) | [], loc :: k -> assert (is_open loc); - new_stack (([ loc ], t, k, tag) :: s) + new_stack (([ loc ], t, k, tag, p) :: s) | _ -> fail (lazy "can't use \".\" here")) | Semicolon, _ -> new_stack stack - | Branch, (g, t, k, tag) :: s -> + | Branch, (g, t, k, tag, p) :: s -> (match init_pos g with | [] | [ _ ] -> fail (lazy "too few goals to branch"); | loc :: loc_tl -> new_stack - (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s)) - | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> + (([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag,p) :: s)) + | Shift, (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s -> (match g' with | [] -> fail (lazy "no more goals to shift") | loc :: loc_tl -> new_stack - (([ loc ], t @+ filter_open g @+ k, [],`BranchTag) - :: (loc_tl, t', k', tag) :: s)) + (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p) + :: (loc_tl, t', k', tag, p') :: s)) | Shift, _ -> fail (lazy "can't shift goals here") - | Pos i_s, ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | Pos i_s, ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in new_stack - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | Pos _, _ -> fail (lazy "can't use relative positioning here") - | Wildcard, ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s + | Wildcard, ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> new_stack - (([loc] @+ g', t, [], `BranchTag) - :: ([], t', k', tag) :: s) + (([loc] @+ g', t, [], `BranchTag, p) + :: ([], t', k', tag, p') :: s) | Wildcard, _ -> fail (lazy "can't use wildcard here") - | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> - new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) + | Merge, (g, t, k,`BranchTag,_) :: (g', t', k', tag,p') :: s -> + new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag, p') :: s) | Merge, _ -> fail (lazy "can't merge goals here") | Focus [], _ -> assert false | Focus gs, s -> @@ -355,8 +358,8 @@ struct if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then fail (lazy (sprintf "goal %d not found (or closed)" g))) gs; - new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s) - | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s + new_stack ((zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s) + | Unfocus, ([], [], [], `FocusTag, _) :: s -> new_stack s | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open") in debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack))); diff --git a/matita/components/ng_tactics/continuationals.mli b/matita/components/ng_tactics/continuationals.mli index 1dcf4aa7d..d3fdf716c 100644 --- a/matita/components/ng_tactics/continuationals.mli +++ b/matita/components/ng_tactics/continuationals.mli @@ -29,12 +29,15 @@ type goal = int (** {2 Goal stack} *) +(* Key value pairs *) +type parameters = (string * string) list + module Stack: sig type switch = Open of goal | Closed of goal type locator = int * switch type tag = [ `BranchTag | `FocusTag | `NoTag ] - type entry = locator list * locator list * locator list * tag + type entry = locator list * locator list * locator list * tag * parameters type t = entry list val empty: t diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml index b01f4259d..41584d1d3 100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@ -43,11 +43,13 @@ let extract_first_goal_from_status status = let s = status#stack in match s with | [] -> fail (lazy "There's nothing to prove") - | (g1, _, k, tag1) :: tl -> + | (g1, _, k, tag1, _) :: tl -> let goals = filter_open g1 in - let (loc::tl) = goals in - let goal = goal_of_loc (loc) in - goal ;; + match goals with + [] -> fail (lazy "No goals under focus") + | loc::tl -> + let goal = goal_of_loc (loc) in + goal ;; let extract_conclusion_type status goal = let gty = get_goalty status goal in @@ -75,6 +77,23 @@ let are_convertible ty1 ty2 status goal = let status,cicterm2 = disambiguate status ctx ty2 `XTNone in NTacStatus.are_convertible status ctx cicterm1 cicterm2 +let clear_volatile_params_tac status = + match status#stack with + [] -> fail (lazy "Empty stack") + | (g,t,k,tag,p)::tl -> + let rec remove_volatile = function + [] -> [] + | (k,v as hd')::tl' -> + let re = Str.regexp "volatile_.*" in + if Str.string_match re k 0 then + remove_volatile tl' + else + hd'::(remove_volatile tl') + in + let newp = remove_volatile p in + status#set_stack ((g,t,k,tag,newp)::tl) +;; + (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ? @@ -86,38 +105,36 @@ let lambda_abstract_tac id t1 t2 status goal = match t2 with | None -> let (_,_,t1) = t1 in - exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit - `JustOne))) (*status*) + block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit + `JustOne))); clear_volatile_params_tac] status | Some t2 -> let status,res = are_convertible t1 t2 status goal in if res then let (_,_,t2) = t2 in - exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit - `JustOne))) (*status*) + block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit + `JustOne))); clear_volatile_params_tac] status else raise NotEquivalentTypes else raise FirstTypeWrong | _ -> raise NotAProduct -let assume name ty eqty = - distribute_tac (fun status goal -> - try exec (lambda_abstract_tac name ty eqty status goal) status goal - with - | NotAProduct -> fail (lazy "You can't assume without an universal quantification") - | FirstTypeWrong -> fail (lazy "The assumed type is wrong") - | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent") - ) +let assume name ty eqty status = + let goal = extract_first_goal_from_status status in + try lambda_abstract_tac name ty eqty status goal + with + | NotAProduct -> fail (lazy "You can't assume without an universal quantification") + | FirstTypeWrong -> fail (lazy "The assumed type is wrong") + | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent") ;; -let suppose t1 id t2 = - distribute_tac (fun status goal -> - try exec (lambda_abstract_tac id t1 t2 status goal) status goal - with - | NotAProduct -> fail (lazy "You can't suppose without a logical implication") - | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise") - | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent") - ) +let suppose t1 id t2 status = + let goal = extract_first_goal_from_status status in + try lambda_abstract_tac id t1 t2 status goal + with + | NotAProduct -> fail (lazy "You can't suppose without a logical implication") + | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise") + | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent") ;; let assert_tac t1 t2 status goal continuation = @@ -133,26 +150,76 @@ let assert_tac t1 t2 status goal continuation = else raise FirstTypeWrong -let mustdot status = - let s = status#stack in - match s with - | [] -> fail (lazy "No goals to dot") - | (_, _, k, _) :: tl -> - if List.length k > 0 then - true +let branch_dot_tac status = + match status#stack with + ([],t,k,tag,p) :: tl -> + if List.length t > 0 then + status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl) else - false + status + | _ -> status +;; + +let status_parameter key status = + match status#stack with + [] -> "" + | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> "" +;; + +let beta_rewriting_step t status = + let ctx = status_parameter "volatile_context" status in + if ctx <> "beta_rewrite" then fail (lazy "Invalid use of 'or equivalently'") + else + change_tac ~where:("",0,(None,[],Some + Ast.UserInput)) ~with_what:t status +;; + +let done_continuation status = + let rec continuation l = + match l with + [] -> [] + | (_,t,_,tag,p)::tl -> + if tag = `BranchTag then + if List.length t > 0 then + let continue = + let ctx = + try List.assoc "context" p + with Not_found -> "" + in + ctx <> "induction" && ctx <> "cases" + in + if continue then [clear_volatile_params_tac;branch_dot_tac] else + [clear_volatile_params_tac] + else + [merge_tac] @ (continuation tl) + else + [] + in + continuation status#stack +;; let bydone just status = let goal = extract_first_goal_from_status status in - let mustdot = mustdot status in - let l = [mk_just status goal just] in - let l = - if mustdot then List.append l [dot_tac] else l - in + let continuation = done_continuation status in + let l = [mk_just status goal just] @ continuation in block_tac l status ;; +let push_goals_tac status = + match status#stack with + [] -> fail (lazy "Error pushing goals") + | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl -> + if List.length g2 > 0 then + status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl) + else status (* Nothing to push *) + | _ -> status + +let add_parameter_tac key value status = + match status#stack with + [] -> status + | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl) +;; + let we_need_to_prove t id t1 status = let goal = extract_first_goal_from_status status in match id with @@ -161,14 +228,17 @@ let we_need_to_prove t id t1 status = match t1 with | None -> (* We need to prove t *) ( - try assert_tac t None status goal (id_tac status) + try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status) with | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") ) | Some t1 -> (* We need to prove t or equivalently t1 *) ( - try assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some - Ast.UserInput)) ~with_what:t1 status) + try assert_tac t (Some t1) status goal (block_tac [change_tac ~where:("",0,(None,[],Some + Ast.UserInput)) + ~with_what:t1; + add_parameter_tac "volatile_context" + "beta_rewrite"] status) with | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") @@ -178,14 +248,14 @@ let we_need_to_prove t id t1 status = ( match t1 with (* We need to prove t (id) *) - | None -> block_tac [cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; - dot_tac + | None -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac; + push_goals_tac ] status (* We need to prove t (id) or equivalently t1 *) - | Some t1 -> block_tac [cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some + | Some t1 -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1; shift_tac; intro_tac id; merge_tac; - dot_tac + branch_tac; push_goals_tac ] status ) @@ -221,46 +291,47 @@ let by_just_we_proved just ty id ty' status = | Some id -> ( match ty' with - | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac ] status + | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac; + clear_volatile_params_tac ] status | Some ty' -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None)) ~with_what:ty'; - merge_tac] status + merge_tac; clear_volatile_params_tac] status ) ;; -let existselim just id1 t1 t2 id2 = - distribute_tac (fun status goal -> - let (_,_,t1) = t1 in - let (_,_,t2) = t2 in - let just = mk_just status goal just in - exec (block_tac [ - cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident - (id1,None), Some t1),t2)])); - branch_tac ~force:false; - just; - shift_tac; - case1_tac "_"; - intros_tac ~names_ref:(ref []) [id1;id2]; - merge_tac - ]) status goal - ) +let existselim just id1 t1 t2 id2 status = + let goal = extract_first_goal_from_status status in + let (_,_,t1) = t1 in + let (_,_,t2) = t2 in + let just = mk_just status goal just in + (block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident + (id1,None), Some t1),t2)])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac; + clear_volatile_params_tac + ]) status ;; -let andelim just t1 id1 t2 id2 = - distribute_tac (fun status goal -> - let (_,_,t1) = t1 in - let (_,_,t2) = t2 in - let just = mk_just status goal just in - exec (block_tac [ - cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2])); - branch_tac ~force:false; - just; - shift_tac; - case1_tac "_"; - intros_tac ~names_ref:(ref []) [id1;id2]; - merge_tac - ]) status goal - ) +let andelim just t1 id1 t2 id2 status = + let goal = extract_first_goal_from_status status in + let (_,_,t1) = t1 in + let (_,_,t2) = t2 in + let just = mk_just status goal just in + (block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac; + clear_volatile_params_tac + ]) status ;; let type_of_tactic_term status ctx t = @@ -272,15 +343,15 @@ let swap_first_two_goals_tac status = let gstatus = match status#stack with | [] -> assert false - | (g,t,k,tag) :: s -> + | (g,t,k,tag,p) :: s -> match g with | (loc1) :: (loc2) :: tl -> - ([loc2;loc1] @+ tl,t,k,tag) :: s + ([loc2;loc1] @+ tl,t,k,tag,p) :: s | _ -> assert false in status#set_stack gstatus -let thesisbecomes t1 t2 = we_need_to_prove t1 None t2 +let thesisbecomes t1 l = we_need_to_prove t1 None l ;; let obtain id t1 status = @@ -293,72 +364,78 @@ let obtain id t1 status = 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; + branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac; + add_parameter_tac "volatile_context" "rewrite" ] 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 conclude 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 _,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 + match gty with + NCic.Appl [_;_;plhs;_] -> + if alpha_eq_tacterm_kerterm t1 plhs status goal then + add_parameter_tac "volatile_context" "rewrite" status + 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 ctx = status_parameter "volatile_context" status in + if ctx = "rewrite" then + ( + 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 params' = - if not (List.mem_assoc "paramodulation" params) then - ("paramodulation","1")::params - else params + 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 - 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 + let continuation = + if last_step then + (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*) + let todo = [just'] @ (done_continuation status) 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 - 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 + prepare continuation + ) + else + fail (lazy "You are not building an equality chain") ;; let rec pp_metasenv_names (metasenv:NCic.metasenv) = @@ -382,24 +459,51 @@ let print_goals_names_tac s (status:#NTacStatus.tac_status) = let (_,_,metasenv,_,_) = status#obj in prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status +(* Useful as it does not change the order in the list *) +let rec list_change_assoc k v = function + [] -> [] + | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl) +;; + let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) = - let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in - let rec remove_name_from_metaattrs mattrs = - match mattrs with - [] -> [] - | hd :: tl -> - match hd with - `Name n -> remove_name_from_metaattrs tl - | _ as it -> it :: (remove_name_from_metaattrs tl) + let add_name_to_goal name goal metasenv = + let (mattrs,ctx,t as conj) = 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 with - [] -> metasenv - | hd :: tl -> - let _,consname,_ = hd - in match metasenv with - [] -> [] - | mhd :: mtl -> + 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) @@ -407,9 +511,17 @@ let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.ta 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 @@ -431,16 +543,22 @@ let we_proceed_by_induction_on t1 t2 status = (match !sort with NCic.Sort x -> x | _ -> assert false)) in let eliminator = - let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in - (* Generating as many implicits as open goals *) - let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in + 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; dot_tac] 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") ;; @@ -455,14 +573,15 @@ let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status = analyze_indty_tac ~what:npt1 indtyinfo; cases_tac ~what:t1 ~where:("",0,(None,[],Some Ast.UserInput)); - print_goals_names_tac "Pre Adding"; ( fun status -> let ity = HExtlib.unopt !indtyinfo in cl := ity.cl; add_names_to_goals_tac cl status ); - print_goals_names_tac "Post Adding"; - dot_tac] 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") ;; @@ -491,8 +610,14 @@ let rec loc_of_goal goal l = else loc_of_goal goal tl ;; +let has_focused_goal status = + match status#stack with + [] -> false + | ([],_,_,_,_) :: tl -> false + | _ -> true +;; + let focus_on_case_tac case status = - let goal = extract_first_goal_from_status status in let (_,_,metasenv,_,_) = status#obj in let rec goal_of_case case metasenv = match metasenv with @@ -505,28 +630,52 @@ let focus_on_case_tac case status = let gstatus = match status#stack with [] -> fail (lazy "There is nothing to prove") - | (g,t,k,tag) :: s -> - let loc = loc_of_goal goal_to_focus k in - let curloc = loc_of_goal goal g in - (((g @- [curloc]) @+ [loc]),t,([curloc] @+ (k @- [loc])),tag) :: s - in status#set_stack gstatus + | (g,t,k,tag,p) :: s -> + let loc = + try + loc_of_goal goal_to_focus t + with _ -> fail (lazy "The given case is not part of the current induction/cases analysis + context") + in + let curloc = if has_focused_goal status then + let goal = extract_first_goal_from_status status in + [loc_of_goal goal g] + else [] + in + (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s + in + status#set_stack gstatus +;; let case id l status = - let goal = extract_first_goal_from_status status in - let (_,_,metasenv,_,_) = status#obj in - let conj = NCicUtils.lookup_meta goal metasenv in - let name = name_of_conj conj in - let continuation = - let rec aux l = - match l with - [] -> [id_tac] - | (id,ty)::tl -> - (try_tac (assume id ("",0,ty) None)) :: (aux tl) - in - aux l - in - if name = id then block_tac continuation status - else block_tac ([focus_on_case_tac id] @ continuation) status + let ctx = status_parameter "context" status in + if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an + induction/cases analysis context") +else + ( + if has_focused_goal status then fail (lazy "Finish the current case before switching") + else + ( +(* + let goal = extract_first_goal_from_status status in + let (_,_,metasenv,_,_) = status#obj in + let conj = NCicUtils.lookup_meta goal metasenv in + let name = name_of_conj conj in +*) + let continuation = + let rec aux l = + match l with + [] -> [id_tac] + | (id,ty)::tl -> + (try_tac (assume id ("",0,ty) None)) :: (aux tl) + in + aux l + in +(* if name = id then block_tac continuation status *) +(* else *) + block_tac ([focus_on_case_tac id] @ continuation) status + ) + ) ;; let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;; diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli index 24b85a608..cfbbac7dc 100644 --- a/matita/components/ng_tactics/declarative.mli +++ b/matita/components/ng_tactics/declarative.mli @@ -28,6 +28,7 @@ type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ] val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic +val beta_rewriting_step : NTacStatus.tactic_term -> 's NTacStatus.tactic val bydone : just -> 's NTacStatus.tactic val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 8e73f5305..a8a78999a 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -31,16 +31,16 @@ let dot_tac status = let gstatus = match status#stack with | [] -> assert false - | ([], _, [], _) :: _ as stack -> + | ([], _, [], _, _) :: _ as stack -> (* backward compatibility: do-nothing-dot *) stack - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> match filter_open g, k with | loc :: loc_tl, _ -> - (([ loc ], t, loc_tl @+ k, tag) :: s) + (([ loc ], t, loc_tl @+ k, tag, p) :: s) | [], loc :: k -> assert (is_open loc); - (([ loc ], t, k, tag) :: s) + (([ loc ], t, k, tag, p) :: s) | _ -> fail (lazy "can't use \".\" here") in status#set_stack gstatus @@ -50,12 +50,12 @@ let branch_tac ?(force=false) status = let gstatus = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> match init_pos g with (* TODO *) | [] -> fail (lazy "empty goals") | [_] when (not force) -> fail (lazy "too few goals to branch") | loc :: loc_tl -> - ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s + ([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag, p) :: s in status#set_stack gstatus ;; @@ -63,12 +63,12 @@ let branch_tac ?(force=false) status = let shift_tac status = let gstatus = match status#stack with - | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> + | (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s -> (match g' with | [] -> fail (lazy "no more goals to shift") | loc :: loc_tl -> - (([ loc ], t @+ filter_open g @+ k, [],`BranchTag) - :: (loc_tl, t', k', tag) :: s)) + (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p) + :: (loc_tl, t', k', tag, p') :: s)) | _ -> fail (lazy "can't shift goals here") in status#set_stack gstatus @@ -78,11 +78,11 @@ let pos_tac i_s status = let gstatus = match status#stack with | [] -> assert false - | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | _ -> fail (lazy "can't use relative positioning here") in status#set_stack gstatus @@ -92,7 +92,7 @@ let case_tac lab status = let gstatus = match status#stack with | [] -> assert false - | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter @@ -101,8 +101,8 @@ let case_tac lab status = match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with attrs,_,_ when List.mem (`Name lab) attrs -> true | _ -> false) ([loc] @+ g') in - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | _ -> fail (lazy "can't use relative positioning here") in status#set_stack gstatus @@ -112,9 +112,9 @@ let wildcard_tac status = let gstatus = match status#stack with | [] -> assert false - | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s + | ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> - (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s) + (([loc] @+ g', t, [], `BranchTag, p) :: ([], t', k', tag, p') :: s) | _ -> fail (lazy "can't use wildcard here") in status#set_stack gstatus @@ -124,8 +124,8 @@ let merge_tac status = let gstatus = match status#stack with | [] -> assert false - | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> - ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) + | (g, t, k,`BranchTag, _) :: (g', t', k', tag, p) :: s -> + ((t @+ filter_open g @+ g' @+ k, t', k', tag, p) :: s) | _ -> fail (lazy "can't merge goals here") in status#set_stack gstatus @@ -145,7 +145,7 @@ let focus_tac gs status = if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then fail (lazy (sprintf "goal %d not found (or closed)" g))) gs; - (zero_pos gs, [], [], `FocusTag) :: deep_close gs s + (zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s in status#set_stack gstatus ;; @@ -154,7 +154,7 @@ let unfocus_tac status = let gstatus = match status#stack with | [] -> assert false - | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s + | (g, [], [], `FocusTag, _) :: s when filter_open g = [] -> s | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^ Continuationals.Stack.pp s)) in @@ -165,12 +165,12 @@ let skip_tac status = let gstatus = match status#stack with | [] -> assert false - | (gl, t, k, tag) :: s -> + | (gl, t, k, tag, p) :: s -> let gl = List.map switch_of_loc gl in if List.exists (function Open _ -> true | Closed _ -> false) gl then fail (lazy "cannot skip an open goal") else - ([],t,k,tag) :: s + ([],t,k,tag,p) :: s in status#set_stack gstatus ;; @@ -219,7 +219,7 @@ let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStat ;; let exec tac (low_status : #lowtac_status) g = - let stack = [ [0,Open g], [], [], `NoTag ] in + let stack = [ [0,Open g], [], [], `NoTag, [] ] in let status = change_stack_type low_status stack in let status = tac status in (low_status#set_pstatus status)#set_obj status#obj @@ -228,7 +228,7 @@ let exec tac (low_status : #lowtac_status) g = let distribute_tac tac (status : #tac_status) = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> debug_print (lazy ("context length " ^string_of_int (List.length g))); let rec aux s go gc = function @@ -258,7 +258,7 @@ let distribute_tac tac (status : #tac_status) = debug_print (lazy ("closed: " ^ String.concat " " (List.map string_of_int gcn))); let stack = - (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s + (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s in ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn ;; @@ -704,7 +704,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let assert_tac seqs status = match status#stack with | [] -> assert false - | (g,_,_,_) :: s -> + | (g,_,_,_,_) :: s -> assert (List.length g = List.length seqs); (match seqs with [] -> id_tac diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 4873481ed..c2a739dea 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -1005,7 +1005,7 @@ let rec stack_goals level gs = if level = 0 then [] else match gs with | [] -> assert false - | (g,_,_,_)::s -> + | (g,_,_,_,_)::s -> let is_open = function | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None @@ -1092,6 +1092,15 @@ let get_cands retrieve_for diff empty gty weak_gty = cands, diff more_cands cands ;; +let is_a_needed_uri s d = + prerr_endline ("DEBUG: " ^ d ^ ": "^ s); + s = "cic:/matita/basics/logic/eq.ind" || + s = "cic:/matita/basics/logic/sym_eq.con" || + s = "cic:/matita/basics/logic/trans_eq.con" || + s = "cic:/matita/basics/logic/eq_f3.con" || + s = "cic:/matita/basics/logic/eq_f2.con" || + s = "cic:/matita/basics/logic/eq_f.con" + let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty = let universe = status#auto_cache in let _,_,metasenv,subst,_ = status#obj in @@ -1124,26 +1133,31 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty in (* we now compute global candidates *) let global_cands, smart_global_cands = - if flags.local_candidates then - let mapf s = - let to_ast = function - | NCic.Const r when true - (*is_relevant statistics r*) -> Some (Ast.NRef r) - (* | NCic.Const _ -> None *) - | _ -> assert false in - HExtlib.filter_map - to_ast (NDiscriminationTree.TermSet.elements s) in - let g,l = - get_cands - (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe) - NDiscriminationTree.TermSet.diff - NDiscriminationTree.TermSet.empty - raw_gty raw_weak_gty in - mapf g, mapf l - else [],[] in + let mapf s = + let to_ast = function + | NCic.Const r when true + (*is_relevant statistics r*) -> Some (Ast.NRef r) + (* | NCic.Const _ -> None *) + | _ -> assert false in + HExtlib.filter_map + to_ast (NDiscriminationTree.TermSet.elements s) in + let g,l = + get_cands + (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe) + NDiscriminationTree.TermSet.diff + NDiscriminationTree.TermSet.empty + raw_gty raw_weak_gty in + mapf g, mapf l + in + let global_cands,smart_global_cands = + if flags.local_candidates then global_cands,smart_global_cands + else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri + (NUri.string_of_uri + uri) "GLOBAL" | _ -> false) + in filter global_cands,filter smart_global_cands + in (* we now compute local candidates *) let local_cands,smart_local_cands = - if flags.local_candidates then let mapf s = let to_ast t = let _status, t = term_of_cic_term status t context @@ -1154,7 +1168,14 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty (fun ty -> search_in_th ty cache) Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in mapf g, mapf l - else [],[] in + in + let local_cands,smart_local_cands = + if flags.local_candidates then local_cands,smart_local_cands + else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri + (NUri.string_of_uri + uri) "LOCAL" | _ -> false) + in filter local_cands,filter smart_local_cands + in (* we now splits candidates in facts or not facts *) let test = is_a_fact_ast status subst metasenv context in let by,given_candidates = @@ -1303,7 +1324,7 @@ let is_subsumed depth filter_depth status gty cache = NCicMetaSubst.mk_meta metasenv ctx ~with_type:implication `IsType in let status = status#set_obj (n,h,metasenv,subst,obj) in - let status = status#set_stack [([1,Open j],[],[],`NoTag)] in + let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in try let status = NTactics.intro_tac "foo" status in let status = @@ -1481,7 +1502,7 @@ let sort_tac status = let gstatus = match status#stack with | [] -> assert false - | (goals, t, k, tag) :: s -> + | (goals, t, k, tag, p) :: s -> let g = head_goals status#stack in let sortedg = (List.rev (MS.topological_sort g (deps status))) in @@ -1496,7 +1517,7 @@ let sort_tac status = let sorted_goals = List.map (fun i -> List.find (is_it i) goals) sortedg in - (sorted_goals, t, k, tag) :: s + (sorted_goals, t, k, tag, p) :: s in status#set_stack gstatus ;; @@ -1505,13 +1526,13 @@ let clean_up_tac status = let gstatus = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> let is_open = function | (_,Continuationals.Stack.Open _) -> true | (_,Continuationals.Stack.Closed _) -> false in let g' = List.filter is_open g in - (g', t, k, tag) :: s + (g', t, k, tag, p) :: s in status#set_stack gstatus ;; @@ -1542,11 +1563,11 @@ let deep_focus_tac level focus status = if level = 0 then [],[],gs else match gs with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag,p) :: s -> let f,o,gs = slice (level-1) s in let f1,o1 = List.partition in_focus g in - (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs + (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs in let gstatus = let f,o,s = slice level status#stack in f@o@s @@ -1557,7 +1578,7 @@ let deep_focus_tac level focus status = let move_to_side level status = match status#stack with | [] -> assert false - | (g,_,_,_)::tl -> + | (g,_,_,_,_)::tl -> let is_open = function | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None @@ -1880,7 +1901,7 @@ let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace let _ = debug_print (pptrace status trace) in let stack = match s#stack with - | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest + | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest | _ -> assert false in let s = s#set_stack stack in @@ -1911,7 +1932,7 @@ let auto_lowtac ~params:(univ,flags as params) status goal = let gty = get_goalty status goal in let ctx = ctx_of gty in let candidates = candidates_from_ctx univ ctx status in - auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref []) + auto_tac' candidates ~local_candidates:false ~use_given_only:true flags ~trace_ref:(ref []) let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let candidates = candidates_from_ctx univ [] status in diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml index bc0b424e0..9c1ed995c 100644 --- a/matita/matita/help/C/sec_declarative_tactics.xml +++ b/matita/matita/help/C/sec_declarative_tactics.xml @@ -14,13 +14,14 @@ assume assume - assume x : t + assume x : T that is equivalent to T' Synopsis: - assume &id; : &sterm; + assume &id; : + &sterm; [ that is equivalent to &term; ] @@ -36,9 +37,10 @@ Action: - It adds to the context of the current sequent to prove a new - declaration x : T . The new conclusion becomes - P. + It adds to the context of the current sequent to prove a new declaration x : T + . The new conclusion becomes P. Alternatively, if a type + T' is supplied and T and T' are beta equivalent the new declaration that is added to the context is + x:T'. @@ -51,75 +53,126 @@ - - by induction hypothesis we know - by induction hypothesis we know - by induction hypothesis we know t (id) - - - - Synopsis: - by induction hypothesis we know &term; ( &id; ) - - - - Pre-condition: - - To be used in a proof by induction to state the inductive - hypothesis. - - - - Action: - - Introduces the inductive hypothesis. - - - - New sequents to prove: - - None. - - - - - + + suppose + suppose + suppose T (x) that is equivalent to T' + + + + Synopsis: + + suppose &term; ( &id; + ) [ that is equivalent to &term; ] + + + + Pre-condition: + + The conclusion of the current proof must be + ∀x:T.P or + T→P where T is + a proposition (i.e. T has type + Prop or CProp). + + + + Action: + + It adds to the context of the current sequent to prove a new declaration x : T + . The new conclusion becomes P. Alternatively, if a type + T' is supplied and T and T' are beta equivalent the new declaration that is added to the context is + x:T'. + + + + + New sequents to prove: + + None. + + + + + - - case - case - case id (id1:t1) … (idn:tn) + + letin + letin + let x := T + + + + Synopsis: + + let &id; = &term; + + + + Pre-condition: + + None + + + + Action: + + It adds a new local definition x := T to the context of the sequent to prove. + + + + New sequents to prove: + + None. + + + + + + + + we proved + we proved + justification we proved T (id) that is equivalent to T' Synopsis: - case &id; [( &id; : &term; )] … - - - - Pre-condition: - - To be used in a proof by induction or by cases to start - a new case - - - - Action: - - Starts the new case id declaring - the local parameters (id1:t1) … (idn:tn) - - - - New sequents to prove: - - None + &justification; we proved &term; + ( &id; + ) [ that is equivalent to &term;] [ done] - - - - + + + Pre-condition: + + T must have type Prop. + + + + + Action: + + It derives T + using the justification and labels the conclusion with + id. Alternatively, if a proposition + T' is supplied and T and T' are beta equivalent the new hypothesis that is added to the context is + id:T'. + + If the user does not supply a label and ends the command with done then if T is alpha equivalent to the conclusion of the current sequent then it closes it (if T' is supplied this must be alpha equivalent to the conclusion, but in this case T does not need to). + + + + + New sequent to prove: + + None. + + + + + done @@ -155,8 +208,7 @@ - - + let such that let such that justification let x:t such that p (id) @@ -199,123 +251,47 @@ - - obtain - obtain - obtain H t1 = t2 justification + + we have + we have + justification we have t1 (id1) and t2 (id2) + - - Synopsis: - - [obtain &id; | conclude &term;] = &term; [&autoparams; | using &term; | using once &term; | proof] [done] - - - - Pre-condition: - - conclude can be used only if the current - sequent is stating an equality. The left hand side must be omitted - in an equality chain. - - - - Action: - - Starts or continues an equality chain. If the chain starts - with obtain H a new subproof named - H is started. - - - - New sequent to prove: - - If the chain starts - with obtain H a nre sequent for - t2 = ? is opened. - - - - - - - - - suppose - suppose - suppose t1 (x) that is equivalent to t2 - - - - Synopsis: - - suppose &term; ( &id; - ) [ that is equivalent to &term; ] - - - - Pre-condition: - - The conclusion of the current proof must be - ∀x:T.P or - T→P where T is - a proposition (i.e. T has type - Prop or CProp). - - - - Action: + + Synopsis: - It adds to the context of the current sequent to prove a new - declaration x : T . The new conclusion becomes - P. + &justification; we have &term; + ( &id; ) and &term; + ( &id; ) + + + + Pre-condition: + + - - - New sequents to prove: - - None. - - - - + + + Action: + + It derives t1∧t2 using the + justification then it introduces in the context + t1 labelled with id1 and + t2 labelled with id2. + + + + + New sequent to prove: + + None. + + + + - - the thesis becomes - the thesis becomes - the thesis becomes t - - - - Synopsis: - - the thesis becomes &term; - - - - Pre-condition: - - The provided term t must be convertible with - current sequent. - - - - Action: - - It changes the current goal to the one provided. - - - - New sequent to prove: - - None. - - - - - - we need to prove we need to prove @@ -358,44 +334,39 @@ - - - we have - we have - justification we have t1 (id1) and t2 (id2) - + + we proceed by induction on + we proceed by induction on + we proceed by induction on t to prove th - + Synopsis: - &justification; we have &term; - ( &id; ) and &term; - ( &id; ) - + we proceed by induction on &term; to prove &term; + - + Pre-condition: - + t must inhabitant of an inductive type and + th must be the conclusion to be proved by induction. + Action: - - It derives t1∧t2 using the - justification then it introduces in the context - t1 labelled with id1 and - t2 labelled with id2. - - - - - New sequent to prove: - - None. - + + It proceed by induction on t. + + + New sequents to prove: + + It opens one new sequent for each constructor of the + type of t. + + @@ -436,73 +407,100 @@ - - - we proceed by induction on - we proceed by induction on - we proceed by induction on t to prove th - - - - Synopsis: - - we proceed by induction on &term; to prove &term; - - - - Pre-condition: - - t must inhabitant of an inductive type and - th must be the conclusion to be proved by induction. - - - - - Action: - - It proceed by induction on t. - - - - New sequents to prove: - - It opens one new sequent for each constructor of the - type of t. - - - - - - - - we proved - we proved - justification we proved t (id) + + case + case + case id (id1:t1) … (idn:tn) Synopsis: - &justification; we proved &term; - ( &id; - ) + case &id; [( &id; : &term; )] … + + + + Pre-condition: + + To be used in a proof by induction or by cases to start + a new case + + + + Action: + + Starts the new case id declaring + the local parameters (id1:t1) … (idn:tn) + + + + New sequents to prove: + + None + + + + + + + by induction hypothesis we know + by induction hypothesis we know + by induction hypothesis we know t (id) + + + + Synopsis: + by induction hypothesis we know &term; ( &id; ) + + + + Pre-condition: + + To be used in a proof by induction to state the inductive + hypothesis. + + + + Action: + + Introduces the inductive hypothesis. + + + + New sequents to prove: + + None. + + + + + + + + the thesis becomes + the thesis becomes + the thesis becomes t + + + + Synopsis: + + the thesis becomes &term; + Pre-condition: - tmust have type Prop. - + The provided term t must be convertible with + current sequent. Action: - It derives t - using the justification and labels the conclusion with - id. - + It changes the current goal to the one provided. @@ -513,6 +511,53 @@ - + + + conclude/obtain + conclude/obtain + conclude/obtain (H) t1 = t2 justification + + + + Synopsis: + + [obtain &id; | conclude &term;] = &term; [&autoparams; | using &term; | using once &term; | proof] [done] + + + + Pre-condition: + + conclude can be used only if the current + sequent is stating an equality. The left hand side must be omitted + in an equality chain. + + + + Action: + + Starts or continues an equality chain. If the chain starts + with obtain H a new subproof named + H is started. + + + + New sequent to prove: + + If the chain starts + with obtain H a nre sequent for + t2 = ? is opened. + + + + + + + + + + + + + -- 2.39.2