From b8a04566e67338e7e5375ff4175277704cd16432 Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Mon, 17 Jun 2019 10:10:31 +0200 Subject: [PATCH] Make 'that is equivalent to' a standalone tactic Simplify AST types, parsing rules and pp of tactics that had 'that is equivalent to' or 'or equivalently' Modify grafiteEngine accordingly Simplify the signature and the code of the implementations of tactics that had 'that is equivalent to' or 'or equivalently' A new "volatile_hypo" key is added to the parameter list of the currest stack level to indicate that the beta rewriting should happen on that hypothesis, instead of the thesis Modify beta_rewrite accordingly Add some "obvious" terms to the given candidates for the automation (such as refl, sym_eq, trans_eq, etc.) The weakening of the automation is now only partial: the second flag for weakening is off. Setting it on makes theorem proving pretty impossible with the declarative fragment. --- matita/components/grafite/grafiteAst.ml | 19 +-- matita/components/grafite/grafiteAstPp.ml | 26 ++-- .../grafite_engine/grafiteEngine.ml | 17 +-- .../grafite_parser/grafiteParser.ml | 28 ++--- matita/components/ng_tactics/declarative.ml | 113 +++++++----------- matita/components/ng_tactics/declarative.mli | 11 +- matita/components/ng_tactics/nnAuto.ml | 8 +- matita/components/syntax_extensions/.depend | 4 +- matita/matita/.depend.opt | 73 ++++------- 9 files changed, 105 insertions(+), 194 deletions(-) diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index c29babd55..7750dab27 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -79,30 +79,21 @@ type ntactic = | NBlock of loc * ntactic list (* Declarative langauge *) (* Not the best idea to use a string directly, an abstract type for identifiers would be better *) - | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *) - | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *) - | By_just_we_proved of loc * just * nterm * string option * nterm option (* loc, - justification, conclusion, identifier, eqconcl *) - | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion, - identifier, equivnewcon *) + | Assume of loc * string * nterm (* loc, identifier, type *) + | Suppose of loc * nterm * string (* loc, assumption, identifier *) + | By_just_we_proved of loc * just * nterm * string option (* loc, justification, conclusion, identifier *) + | We_need_to_prove of loc * nterm * string option (* loc, newconclusion, identifier *) | BetaRewritingStep of loc * nterm | Bydone of loc * just | ExistsElim of loc * just * string * nterm * nterm * string | AndElim of loc * just * nterm * string * nterm * string - (* - | RewritingStep of - loc * (string option * nterm) option * nterm * - [ `Term of nterm | `Auto of auto_params - | `Proof | `SolveWith of nterm ] * - bool (* last step*) - *) | RewritingStep of loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*) | Obtain of loc * string * nterm | Conclude of loc * nterm - | Thesisbecomes of loc * nterm * nterm option + | Thesisbecomes of loc * nterm | We_proceed_by_induction_on of loc * nterm * nterm | We_proceed_by_cases_on of loc * nterm * nterm | Byinduction of loc * nterm * string diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index e8864255d..0d394540a 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -120,27 +120,21 @@ let rec pp_ntactic status ~map_unicode_to_tex = | NBlock (_,l) -> "(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")" | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t - | Assume (_, ident, term, term1) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term ^ - (match term1 with None -> " " | Some t1 -> " that is eqivalent to " ^ NotationPp.pp_term status t1) - | Suppose (_,term,ident,term1) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" ^ (match - term1 with None -> " " | Some t -> " that is equivalent to " ^ NotationPp.pp_term status t) - | 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,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) + | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term + | Suppose (_,term,ident) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" + | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ "we proved" ^ + NotationPp.pp_term status term1 ^ (match ident with + None -> "" | Some ident -> "(" ^ident^ ")") + | We_need_to_prove (_,term,ident) -> "we need to prove" ^ NotationPp.pp_term status term ^ + (match ident with None -> "" | Some id -> "(" ^ id ^ ")") + | BetaRewritingStep (_,t) -> "that is equivalent to" ^ (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 ^ ")" + ^ 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 (_, t, t1) -> "the thesis becomes " ^ NotationPp.pp_term status t ^ - (match t1 with None -> "" | Some t1 -> " or equivalently " ^ - NotationPp.pp_term status - t1) + | Thesisbecomes (_, t) -> "the thesis becomes" ^ NotationPp.pp_term status t | RewritingStep (_, rhs, just, cont) -> "=" ^ NotationPp.pp_term status rhs ^ diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index ee0573ae7..93396d2bd 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -492,15 +492,11 @@ let eval_ng_tac tac = NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l) |GrafiteAst.NRepeat (_,tac) -> NTactics.repeat_tac (f f (text, prefix_len, tac)) - |GrafiteAst.Assume (_,id,t,t1) -> Declarative.assume id (text,prefix_len,t) (match t1 with None -> - None | Some t1 -> (Some (text,prefix_len,t1))) - |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose (text,prefix_len,t) id (match t1 with None - -> None | Some t1 -> (Some (text,prefix_len,t1))) - |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, t1) -> Declarative.we_need_to_prove (text,prefix_len,t) id - (match t1 with None -> None | Some t1 -> Some (text,prefix_len,t1)) + |GrafiteAst.Assume (_,id,t) -> Declarative.assume id (text,prefix_len,t) + |GrafiteAst.Suppose (_,t,id) -> Declarative.suppose (text,prefix_len,t) id + |GrafiteAst.By_just_we_proved (_,j,t1,s) -> Declarative.by_just_we_proved + (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s + |GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove (text,prefix_len,t) id |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) -> @@ -508,8 +504,7 @@ let eval_ng_tac tac = (text,prefix_len,t2) id2 | 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)) + | GrafiteAst.Thesisbecomes (_, t1) -> Declarative.thesisbecomes (text,prefix_len,t1) | 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 5acdf2bd0..b1e3cc733 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -81,7 +81,7 @@ let nnon_punct_of_punct = function type by_continuation = BYC_done - | BYC_weproved of N.term * string option * N.term option + | BYC_weproved of N.term * string option | BYC_letsuchthat of string * N.term * N.term * string | BYC_wehaveand of string * N.term * string * N.term @@ -239,10 +239,8 @@ EXTEND | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")]) | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")]) | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) - | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term ; t1 = OPT [IDENT "that"; IDENT "is"; - IDENT "equivalent"; "to"; t' = tactic_term -> t']-> G.NTactic (loc,[G.Assume (loc,id,t,t1)]) - | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that"; IDENT - "is"; IDENT "equivalent"; "to"; t' = tactic_term -> t'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)]) + | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)]) + | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> G.NTactic (loc,[G.Suppose (loc,t,id)]) | "let"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> G.NTactic(loc,[G.NLetIn (loc,(None,[],Some N.UserInput),t,name)]) | just = @@ -260,21 +258,17 @@ EXTEND cont=by_continuation -> G.NTactic (loc,[ (match cont with BYC_done -> G.Bydone (loc, just) - | BYC_weproved (ty,id,t1) -> - G.By_just_we_proved(loc, just, ty, id, t1) + | BYC_weproved (ty,id) -> + G.By_just_we_proved(loc, just, ty, id) | BYC_letsuchthat (id1,t1,t2,id2) -> G.ExistsElim (loc, just, id1, t1, t2, id2) | 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']-> - 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] -> - G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)]) + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] -> + G.NTactic (loc,[G.We_need_to_prove (loc, t, id)]) + | IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)]) + | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term -> G.NTactic (loc,[G.Thesisbecomes(loc,t1)]) | 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)]) | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> @@ -376,9 +370,7 @@ t']-> ]; by_continuation: [ - [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1) - | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; - "done" -> BYC_weproved (ty,None,t1) + [ WEPROVED; ty = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id] -> BYC_weproved (ty,id) | "done" -> BYC_done | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml index 41584d1d3..f29dcf289 100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@ -94,14 +94,26 @@ let clear_volatile_params_tac status = status#set_stack ((g,t,k,tag,newp)::tl) ;; +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) +;; + + (* 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. ? *) -let lambda_abstract_tac id t1 t2 status goal = +let lambda_abstract_tac id t1 status goal = match extract_conclusion_type status goal with | NCic.Prod (_,t,_) -> if alpha_eq_tacterm_kerterm t1 t status goal then + let (_,_,t1) = t1 in + block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit + `JustOne))); clear_volatile_params_tac; + add_parameter_tac "volatile_newhypo" id] status +(* match t2 with | None -> let (_,_,t1) = t1 in @@ -115,22 +127,23 @@ let lambda_abstract_tac id t1 t2 status goal = `JustOne))); clear_volatile_params_tac] status else raise NotEquivalentTypes +*) else raise FirstTypeWrong | _ -> raise NotAProduct -let assume name ty eqty status = +let assume name ty status = let goal = extract_first_goal_from_status status in - try lambda_abstract_tac name ty eqty status goal + try lambda_abstract_tac name ty 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 status = +let suppose t1 id status = let goal = extract_first_goal_from_status status in - try lambda_abstract_tac id t1 t2 status goal + try lambda_abstract_tac id t1 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") @@ -168,7 +181,14 @@ let status_parameter key status = 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'") + if ctx <> "beta_rewrite" then + ( + let newhypo = status_parameter "volatile_newhypo" status in + if newhypo = "" then + fail (lazy "Invalid use of 'or equivalently'") + else + change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status + ) else change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t status @@ -214,88 +234,35 @@ let push_goals_tac status = 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 we_need_to_prove t id status = let goal = extract_first_goal_from_status status in match id with | None -> ( - match t1 with - | None -> (* We need to prove t *) - ( - 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 (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") - ) + 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 id -> ( - match t1 with - (* We need to prove t (id) *) - | None -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac; - push_goals_tac + block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac; + push_goals_tac; add_parameter_tac "volatile_context" "beta_rewrite" ] status - (* We need to prove t (id) or equivalently t1 *) - | 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; - branch_tac; push_goals_tac - ] - status ) ;; -let by_just_we_proved just ty id ty' status = +let by_just_we_proved just ty id status = let goal = extract_first_goal_from_status status in let wrappedjust = just in let just = mk_just status goal just in match id with | None -> - (match ty' with - | None -> (* just we proved P done *) - ( - try - assert_tac ty None status goal (bydone wrappedjust status) - with - | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") - | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") - ) - | Some ty' -> (* just we proved P that is equivalent to P' done *) - ( - try - assert_tac ty' None status goal (block_tac [change_tac ~where:("",0,(None,[],Some - Ast.UserInput)) - ~with_what:ty; bydone wrappedjust] - status ) - with - | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion") - | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") - ) - ) + assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac + "volatile_context" "beta_rewrite"] status) | Some id -> ( - match ty' with - | 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; clear_volatile_params_tac] status + block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac; + clear_volatile_params_tac; add_parameter_tac "volatile_newhypo" id] status ) ;; @@ -351,7 +318,7 @@ let swap_first_two_goals_tac status = in status#set_stack gstatus -let thesisbecomes t1 l = we_need_to_prove t1 None l +let thesisbecomes t1 = we_need_to_prove t1 None ;; let obtain id t1 status = @@ -586,7 +553,7 @@ let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status = | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion") ;; -let byinduction t1 id = suppose t1 id None ;; +let byinduction t1 id = suppose t1 id ;; let name_of_conj conj = let mattrs,_,_ = conj in @@ -667,7 +634,7 @@ else match l with [] -> [id_tac] | (id,ty)::tl -> - (try_tac (assume id ("",0,ty) None)) :: (aux tl) + (try_tac (assume id ("",0,ty))) :: (aux tl) in aux l in diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli index cfbbac7dc..f6863be27 100644 --- a/matita/components/ng_tactics/declarative.mli +++ b/matita/components/ng_tactics/declarative.mli @@ -25,18 +25,17 @@ 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 assume : string -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val suppose : NTacStatus.tactic_term -> string -> 's NTacStatus.tactic +val we_need_to_prove : NTacStatus.tactic_term -> string 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 +val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> 's NTacStatus.tactic val andelim : just -> NTacStatus.tactic_term -> string -> NTacStatus.tactic_term -> string -> 's NTacStatus.tactic val existselim : just -> string -> NTacStatus.tactic_term -> NTacStatus.tactic_term -> string -> 's NTacStatus.tactic -val thesisbecomes : NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic +val thesisbecomes : NTacStatus.tactic_term -> 's NTacStatus.tactic val rewritingstep : NTacStatus.tactic_term -> [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params | `Proof | `SolveWith of NTacStatus.tactic_term ] -> bool (* last step *) -> 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index c2a739dea..3e3685063 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -1926,13 +1926,17 @@ let candidates_from_ctx univ ctx status = let status, res = disambiguate status ctx t `XTNone in let _,res = term_of_cic_term status res (ctx_of res) in Ast.NCic res - in Some (List.map to_Ast l) + in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None); + Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None); + Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None); + Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None) + ]) 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:false ~use_given_only:true flags ~trace_ref:(ref []) + auto_tac' candidates ~local_candidates:false ~use_given_only:false 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/components/syntax_extensions/.depend b/matita/components/syntax_extensions/.depend index 4b9bcffd4..8b3261bc8 100644 --- a/matita/components/syntax_extensions/.depend +++ b/matita/components/syntax_extensions/.depend @@ -1,5 +1,5 @@ +utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi +utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi utf8Macro.cmi : utf8MacroTable.cmo : utf8MacroTable.cmx : -utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index 2df448773..5c7d0715a 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -1,78 +1,47 @@ -applyTransformation.cmo : applyTransformation.cmi applyTransformation.cmx : applyTransformation.cmi -buildTimeConf.cmo : +applyTransformation.cmi : buildTimeConf.cmx : -cicMathView.cmo : matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \ - buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi cicMathView.cmx : matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi -lablGraphviz.cmo : lablGraphviz.cmi +cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi lablGraphviz.cmx : lablGraphviz.cmi -matitaclean.cmo : matitaMisc.cmi matitaInit.cmi matitaclean.cmi -matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi -matitac.cmo : matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \ - matitaEngine.cmi -matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \ - matitaEngine.cmx -matitaEngine.cmo : applyTransformation.cmi matitaEngine.cmi +lablGraphviz.cmi : +matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \ + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaEngine.cmx : applyTransformation.cmx matitaEngine.cmi -matitaExcPp.cmo : matitaEngine.cmi matitaExcPp.cmi +matitaEngine.cmi : applyTransformation.cmi matitaExcPp.cmx : matitaEngine.cmx matitaExcPp.cmi -matitaGeneratedGui.cmo : +matitaExcPp.cmi : matitaGeneratedGui.cmx : -matitaGtkMisc.cmo : matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \ - matitaGtkMisc.cmi matitaGtkMisc.cmx : matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi -matitaGui.cmo : matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \ - matitaGeneratedGui.cmx matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi +matitaGtkMisc.cmi : matitaGeneratedGui.cmx matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi -matitaInit.cmo : matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi +matitaGui.cmi : matitaGuiTypes.cmi +matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi -matitaMathView.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \ - matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmx \ - applyTransformation.cmi matitaMathView.cmi +matitaInit.cmi : matitaMathView.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \ matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \ applyTransformation.cmx matitaMathView.cmi -matitaMisc.cmo : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi +matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi matitaMisc.cmx : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi -matita.cmo : predefined_virtuals.cmi matitaScript.cmi matitaMisc.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx \ - applyTransformation.cmi -matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \ - applyTransformation.cmx -matitaScript.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \ - buildTimeConf.cmx matitaScript.cmi +matitaMisc.cmi : matitaGuiTypes.cmi matitaScript.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \ buildTimeConf.cmx matitaScript.cmi -matitaTypes.cmo : matitaTypes.cmi -matitaTypes.cmx : matitaTypes.cmi -predefined_virtuals.cmo : virtuals.cmi predefined_virtuals.cmi -predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi -virtuals.cmo : virtuals.cmi -virtuals.cmx : virtuals.cmi -applyTransformation.cmi : -cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi -lablGraphviz.cmi : -matitaclean.cmi : -matitaEngine.cmi : applyTransformation.cmi -matitaExcPp.cmi : -matitaGtkMisc.cmi : matitaGeneratedGui.cmx -matitaGui.cmi : matitaGuiTypes.cmi -matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi -matitaInit.cmi : -matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi -matitaMisc.cmi : matitaGuiTypes.cmi matitaScript.cmi : +matitaTypes.cmx : matitaTypes.cmi matitaTypes.cmi : +matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \ + matitaEngine.cmx +matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi +matitaclean.cmi : +predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi predefined_virtuals.cmi : +virtuals.cmx : virtuals.cmi virtuals.cmi : -- 2.39.2