From 489639a3c319d0349a9c864fd0eeaf659daa3d3f Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Thu, 25 Apr 2019 15:07:24 +0200 Subject: [PATCH] Add last declarative tactics, modify rewriting tactics Add types for induction and case analysis to grafiteAst. Add new types for obtain and conclude Add pp code for induction, case, obtain, conclude Add calls in grafiteEngine for induction, case, obtain, conclude Add parsing rules for induction, case, obtain, conclude Rename a function for code clarity Add function to swap two goals on the stack (useful for obtain) Add a conclude function that checks that the given term is the lhs of the current goal Add a obtain function that starts an equality chain beginning with the given term in a new goal Modify rewriting step to only handle single equality chains steps Add implementation for induction and case. Add signatures for induction, case, conclude, obtain Add keywords to matita.lang for induction, case, conclude, obtain --- matita/components/grafite/grafiteAst.ml | 12 + matita/components/grafite/grafiteAstPp.ml | 21 ++ .../grafite_engine/grafiteEngine.ml | 22 +- .../grafite_parser/grafiteParser.ml | 18 +- matita/components/ng_tactics/declarative.ml | 256 +++++++++++++----- matita/components/ng_tactics/declarative.mli | 9 +- matita/matita/matita.lang | 7 + 7 files changed, 262 insertions(+), 83 deletions(-) diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 27f3830b6..c4ec503c7 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -88,12 +88,24 @@ type ntactic = | 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 + | We_proceed_by_induction_on of loc * nterm * nterm + | We_proceed_by_cases_on of loc * nterm * nterm + | Byinduction of loc * nterm * string + | Case of loc * string * (string * nterm) list (* This is a debug tactic to print the stack to stdout, can be safely removed *) | PrintStack of loc diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index a333dccfc..a4a5788d9 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -138,6 +138,16 @@ let rec pp_ntactic status ~map_unicode_to_tex = ^ " (" ^ ident2 ^ ")" | Thesisbecomes (_, term1, term2) -> "the thesis becomes " ^ NotationPp.pp_term status term1 ^ (match term2 with None -> " " | Some term2 -> NotationPp.pp_term status term2) + | RewritingStep (_, rhs, just, cont) -> + "=" ^ + NotationPp.pp_term status rhs ^ + (match just with + | `Auto params -> pp_auto_params params status + | `Term t -> " exact " ^ NotationPp.pp_term status t + | `Proof -> " proof" + | `SolveWith t -> " using " ^ NotationPp.pp_term status t) + ^ (if cont then " done" else "") +(* | RewritingStep (_, term, term1, term2, cont) -> (match term with | None -> " " @@ -152,6 +162,17 @@ let rec pp_ntactic status ~map_unicode_to_tex = | `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 + | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ NotationPp.pp_term status term ^ "to prove" ^ NotationPp.pp_term status term1 + | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" + | Case (_, id, args) -> + "case" ^ id ^ + String.concat " " + (List.map (function (id,term) -> "(" ^ id ^ ": " ^ NotationPp.pp_term status term ^ ")") + args) ;; let pp_nmacro status = function diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index c0faf6102..f2876d2a9 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -509,17 +509,25 @@ let eval_ng_tac tac = 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.RewritingStep (_,termine,t1,t2,cont) -> - Declarative.rewritingstep (match termine with None -> None - | Some (s,t) -> Some (s, (text,prefix_len,t))) - (text,prefix_len,t1) - (match t2 with - `Term t -> just_to_tacstatus_just t2 text prefix_len - | `Auto params -> just_to_tacstatus_just t2 text prefix_len + | GrafiteAst.RewritingStep (_,rhs,just,cont) -> + Declarative.rewritingstep (text,prefix_len,rhs) + (match just with + `Term t -> just_to_tacstatus_just just text prefix_len + | `Auto params -> just_to_tacstatus_just just text prefix_len |`Proof -> `Proof |`SolveWith t -> `SolveWith (text,prefix_len,t) ) cont + | GrafiteAst.Obtain (_,id,t1) -> + Declarative.obtain id (text,prefix_len,t1) + | GrafiteAst.Conclude (_,t1) -> + Declarative.conclude (text,prefix_len,t1) + | GrafiteAst.We_proceed_by_cases_on (_, t, t1) -> + Declarative.we_proceed_by_cases_on (text,prefix_len,t) (text,prefix_len,t1) + | GrafiteAst.We_proceed_by_induction_on (_, t, t1) -> + Declarative.we_proceed_by_induction_on (text,prefix_len,t) (text,prefix_len,t1) + | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction (text,prefix_len,t) id + | GrafiteAst.Case (_,id,params) -> Declarative.case id params | GrafiteAst.PrintStack (_) -> Declarative.print_stack in aux aux tac (* trick for non uniform recursion call *) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 1b60e9902..eaf0c4c01 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -272,8 +272,18 @@ EXTEND | 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 "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 -> + G.NTactic (loc,[G.We_proceed_by_induction_on (loc, t, t1)]) + | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + G.NTactic (loc,[G.Byinduction(loc, t, id)]) + | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; + SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> + G.NTactic (loc,[G.Case(loc,id,params)]) | IDENT "print_stack" -> G.NTactic (loc,[G.PrintStack loc]) (* DO NOT FACTORIZE with the two following, camlp5 sucks*) +(* | IDENT "conclude"; termine = tactic_term; SYMBOL "=" ; @@ -314,6 +324,12 @@ EXTEND ]; cont = rewriting_step_continuation -> G.NTactic(loc,[G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)]) +*) + | IDENT "obtain" ; name = IDENT; + termine = tactic_term -> + G.NTactic(loc,[G.Obtain(loc, name, termine)]) + | IDENT "conclude" ; termine = tactic_term -> + G.NTactic(loc,[G.Conclude(loc, termine)]) | SYMBOL "=" ; t1=tactic_term ; t2 = @@ -331,7 +347,7 @@ EXTEND ) ]; cont = rewriting_step_continuation -> - G.NTactic(loc,[G.RewritingStep(loc, None, t1, t2, cont)]) + G.NTactic(loc,[G.RewritingStep(loc, t1, t2, cont)]) ] ]; auto_fixed_param: [ diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml index 3a700ba96..0802edd1d 100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@ -62,7 +62,7 @@ let extract_conclusion_type status goal = gty ;; -let same_type_as_conclusion ty t status goal = +let alpha_eq_tacterm_kerterm ty t status goal = let gty = get_goalty status goal in let ctx = ctx_of gty in let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in @@ -88,7 +88,7 @@ let are_convertible ty1 ty2 status goal = let lambda_abstract_tac id t1 t2 status goal = match extract_conclusion_type status goal with | NCic.Prod (_,t,_) -> - if same_type_as_conclusion t1 t status goal then + if alpha_eq_tacterm_kerterm t1 t status goal then match t2 with | None -> let (_,_,t1) = t1 in @@ -130,7 +130,7 @@ let suppose t1 id t2 (*status*) = let assert_tac t1 t2 status goal continuation = let t = extract_conclusion_type status goal in - if same_type_as_conclusion t1 t status goal then + if alpha_eq_tacterm_kerterm t1 t status goal then match t2 with | None -> continuation | Some t2 -> @@ -278,45 +278,41 @@ let we_need_to_prove t id t1 status = ) ;; -let by_just_we_proved just ty id ty' (*status*) = - distribute_tac (fun status goal -> - 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 (exec (bydone wrappedjust) status goal) - 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' (Some ty) status goal (exec (block_tac [change_tac - ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; bydone - wrappedjust]) status goal) - with - | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion") - | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") - ) - ) - | Some id -> - ( - match ty' with - | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac - id; merge_tac ]) status goal - | Some ty' -> exec (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 goal - ) - ) -;; - -let thesisbecomes t1 t2 status = we_need_to_prove t1 None t2 status +let by_just_we_proved just ty id ty' 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") + ) + ) + | Some id -> + ( + match ty' with + | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_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 + ) ;; let existselim just id1 t1 t2 id2 (*status*) = @@ -360,7 +356,100 @@ let type_of_tactic_term status ctx t = let (_,cicty) = typeof status ctx cicterm in cicty -let rewritingstep lhs rhs just last_step status = +let swap_first_two_goals_tac status = + let gstatus = + match status#stack with + | [] -> assert false + | (g,t,k,tag) :: s -> + match g with + | (loc1) :: (loc2) :: tl -> + ([loc2;loc1] @+ tl,t,k,tag) :: s + | _ -> assert false + in + status#set_stack gstatus + +let thesisbecomes t1 t2 = we_need_to_prove t1 None t2 +;; + +let obtain id 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 cicty = type_of_tactic_term status ctx t1 in + let _,ty = term_of_cic_term status cicty ctx in + let (_,_,t1) = t1 in + 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; + ] + 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 goal = extract_first_goal_from_status status in + let cicgty = get_goalty status goal in + let ctx = ctx_of cicgty in + let _,gty = term_of_cic_term status cicgty ctx in + let cicty = type_of_tactic_term status ctx rhs in + let _,ty = term_of_cic_term status cicty ctx in + let just' = (* Extraction of the ""justification"" from the ad hoc justification *) + match just with + `Auto (univ, params) -> + let params = + if not (List.mem_assoc "timeout" params) then + ("timeout","3")::params + else params + in + let params' = + if not (List.mem_assoc "paramodulation" params) then + ("paramodulation","1")::params + else params + in + if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal + else + first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac + ~params:(univ, params') status goal] + | `Term just -> apply_tac just + | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"]) + | `Proof -> id_tac + in + let plhs,prhs,prepare = + match 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 + in + block_tac todo + else + let (_,_,rhs) = rhs in + block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs; + rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac] + in + prepare continuation +;; + +(* let goal = extract_first_goal_from_status status in let cicgty = get_goalty status goal in let ctx = ctx_of cicgty in @@ -409,37 +498,22 @@ let rewritingstep lhs rhs just last_step status = plhs,prhs, (fun continuation -> continuation status) | Some (Some name,lhs) -> (* obtain *) - fail (lazy "Not implemented") - (* - let plhs = lhs in - let prhs = Cic.Meta(newmeta,irl) in - plhs,prhs, + NCic.Rel 1, NCic.Rel 1, (* continuation for this case is gonna be ignored, so it doesn't + matter what the values of these two are *) (fun continuation -> - let metasenv = (newmeta, ctx, ty)::metasenv in - let mk_fresh_name_callback = - fun metasenv ctx _ ~typ -> - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv ctx - (Cic.Name name) ~typ - in - let proof = curi,metasenv,_subst,proofbo,proofty, attrs in - let proof,goals = - ProofEngineTypes.apply_tactic - (Tacticals.thens - ~start:(Tactics.cut ~mk_fresh_name_callback - (Cic.Appl [eq ; ty ; lhs ; prhs])) - ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal) - in - let goals = - match just,goals with - `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1] - | _, [g1;g2] -> [g2;newmeta;g1] - | _, l -> - prerr_endline (String.concat "," (List.map string_of_int l)); - prerr_endline (CicMetaSubst.ppmetasenv [] metasenv); - assert false - in - proof,goals) - *) + let (_,_,lhs) = lhs in + block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; lhs; Ast.Implicit + `JustOne])); + swap_first_two_goals_tac; + branch_tac; shift_tac; shift_tac; intro_tac name; merge_tac; dot_tac; +(* + change_tac ~where:("",0,(None,[],Some Ast.Appl[Ast.Implicit `JustOne;Ast.Implicit + `JustOne; Ast.UserInput; Ast.Implicit `JustOne])) + ~with_what:rhs +*) + ] + status + ) in let continuation = if last_step then @@ -455,6 +529,42 @@ let rewritingstep lhs rhs just last_step status = in prepare continuation ;; + *) + +let we_proceed_by_cases_on t1 t2 status = + let goal = extract_first_goal_from_status status in + try + assert_tac t2 None status goal (block_tac [cases_tac ~what:t1 ~where:("",0,(None,[],Some + Ast.UserInput)); + dot_tac] status) + with + | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion") + +let we_proceed_by_induction_on t1 t2 status = + let goal = extract_first_goal_from_status status in + try + assert_tac t2 None status goal (block_tac [elim_tac ~what:t1 ~where:("",0,(None,[],Some + Ast.UserInput)); + dot_tac] status) + with + | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion") +;; + +let byinduction t1 id = suppose t1 id None ;; + +let case id l = + distribute_tac (fun status goal -> + let rec aux l = + match l with + [] -> [id_tac] + | (id,ty)::tl -> + (try_tac (assume id ("",0,ty) None)) :: (aux tl) + in +(* if l == [] then exec (try_tac (intro_tac "H")) status goal *) +(* else *) + exec (block_tac (aux l)) status goal + ) +;; let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;; diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli index 5b154382f..24b85a608 100644 --- a/matita/components/ng_tactics/declarative.mli +++ b/matita/components/ng_tactics/declarative.mli @@ -36,8 +36,13 @@ 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 rewritingstep : (string option * NTacStatus.tactic_term) option -> NTacStatus.tactic_term -> - [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params +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 +val we_proceed_by_cases_on: NTacStatus.tactic_term -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val we_proceed_by_induction_on: NTacStatus.tactic_term -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val byinduction: NTacStatus.tactic_term -> string -> 's NTacStatus.tactic +val case: string -> (string*NotationPt.term) list -> 's NTacStatus.tactic +val obtain: string -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val conclude: NTacStatus.tactic_term -> 's NTacStatus.tactic val print_stack : 's NTacStatus.tactic diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index 8437cd081..56cb0c411 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -125,6 +125,13 @@ the thesis becomes + conclude + obtain + proceed + induction + case + hypothesis + know alias -- 2.39.2