From 433e66b381d1b89e48c05d517494fc300fd0abb5 Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Sun, 31 Mar 2019 14:58:51 +0200 Subject: [PATCH] Add drafts for some tactics Add drafts for assume, suppose, we_need_to_prove. Add a just type to handle justfications in tactics. Add drafts for the by_done and by_just_we_proved tactics. Everything needs testing --- matita/components/grafite/grafiteAst.ml | 18 +- matita/components/grafite/grafiteAstPp.ml | 30 ++- .../grafite_engine/grafiteEngine.ml | 28 ++- .../grafite_parser/grafiteParser.ml | 38 +++- matita/components/ng_tactics/Makefile | 2 +- matita/components/ng_tactics/declarative.ml | 185 +++++++++++++++++- matita/components/ng_tactics/declarative.mli | 10 +- matita/matita/matita.lang | 8 + 8 files changed, 298 insertions(+), 21 deletions(-) diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 29dfe324b..ed757f601 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -36,6 +36,11 @@ type npattern = type auto_params = nterm list option * (string*string) list +(* The additional a is for abstract *) +type 'term aauto_params = 'term list option * (string*string) list + +type 'term just = [`Term of 'term | `Auto of 'term aauto_params] + type ntactic = | NApply of loc * nterm | NSmartApply of loc * nterm @@ -77,8 +82,17 @@ 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 (* loc, identifier, term *) - | Suppose of loc * nterm *string * nterm option + | 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 * nterm 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 *) + | Bydone of loc * nterm just + (* + | ExistsElim of loc * nterm just * string * nterm * nterm * string + | AndElim of loc * nterm just * nterm * string * nterm * string + *) type nmacro = | NCheck of loc * nterm diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 00789961c..4e685c26d 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -51,6 +51,19 @@ let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) = in Printf.sprintf "%sin %s%s" what_text hyp_text goal_text +let pp_auto_params params status = + match params with + | (None,flags) -> String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags) + | (Some l,flags) -> (String.concat "," (List.map (NotationPp.pp_term status) l)) ^ + String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags) +;; + +let pp_just status just = + match just with + `Term term -> "exact " ^ NotationPp.pp_term status term + | `Auto params -> pp_auto_params params status +;; + let rec pp_ntactic status ~map_unicode_to_tex = let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in function @@ -107,9 +120,22 @@ 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) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term + | 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) + 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,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) + | Bydone (_, just) -> pp_just status just ^ "done" + (* + | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" + ^ NotationPp.pp_term term ^ "such that " ^ NotationPp.pp_term term1 ^ "(" ^ ident1 ^ ")" + | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just ~NotationPp.pp_term just ^ "we have " ^ NotationPp.pp_term term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term term2 ^ " (" ^ ident2 ^ ")" + *) ;; let pp_nmacro status = function diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index be7154179..9dd266ed9 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -404,6 +404,16 @@ let eval_add_constraint status acyclic u1 u2 = ;; let eval_ng_tac tac = + let just_to_tacstatus_just just text prefix_len = + match just with + | `Term t -> `Term (text,prefix_len,t) + | `Auto (l,params) -> + ( + match l with + | None -> `Auto (None,params) + | Some l -> `Auto (Some (List.map (fun t -> (text,prefix_len,t)) l),params) + ) + in let rec aux f (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) @@ -481,8 +491,22 @@ 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) -> Declarative.assume id t - |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose t id t1 + |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, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id + (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2)) + | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len) + (* + | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) -> + Declarative.existselim just id1 t1 t2 id2 + | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> + Declarative.andelim just t1 id1 t2 id2 + *) 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 90abc0a89..803051e69 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -82,7 +82,7 @@ let nnon_punct_of_punct = function type by_continuation = BYC_done | BYC_weproved of N.term * string option * N.term option - | BYC_letsuchthat of string * N.term * string * N.term + | BYC_letsuchthat of string * N.term * N.term * string | BYC_wehaveand of string * N.term * string * N.term let mk_parser statement lstatus = @@ -239,9 +239,35 @@ 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 -> G.NTactic (loc,[G.Assume (loc,id,t)]) + | 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)]) + | just = + [ IDENT "using"; t=tactic_term -> `Term t + | params = auto_params -> + let just,params = params in + `Auto + (match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; + 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_letsuchthat (id1,t1,t2,id2) -> + G.ExistsElim (loc, just, id1, t1, t2, id2) + | BYC_wehaveand (id1,t1,id2,t2) -> + G.AndElim (loc, just, id1, t1, id2, t2)*)) + ]) + | 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)]) ] ]; auto_fixed_param: [ @@ -266,7 +292,6 @@ EXTEND ] ]; -(* MATITA 1.0 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] ; @@ -274,19 +299,18 @@ EXTEND | "done" -> BYC_done | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; - id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2) + id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,t2,id2) | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> BYC_wehaveand (id1,t1,id2,t2) ] ]; -*) -(* MATITA 1.0 + rewriting_step_continuation : [ [ "done" -> true | -> false ] ]; -*) + (* MATITA 1.0 atomic_tactical: [ "sequence" LEFTA diff --git a/matita/components/ng_tactics/Makefile b/matita/components/ng_tactics/Makefile index c9b82e044..b7a98406f 100644 --- a/matita/components/ng_tactics/Makefile +++ b/matita/components/ng_tactics/Makefile @@ -6,8 +6,8 @@ INTERFACE_FILES = \ nTacStatus.mli \ nCicElim.mli \ nTactics.mli \ - declarative.mli \ nnAuto.mli \ + declarative.mli \ nDestructTac.mli \ nInversion.mli diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml index ae07c18ee..eb0966570 100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@ -25,10 +25,185 @@ module Ast = NotationPt open NTactics +open NTacStatus -let assume name ty = - exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit `JustOne))) +type just = [ `Term of NTacStatus.tactic_term | `Auto of NTacStatus.tactic_term GrafiteAst.aauto_params ] -let suppose t id t1 = - let t1 = match t1 with None -> t | Some t1 -> t1 in - exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit `JustOne))) +let mk_just = + function + `Auto (l,params) -> NnAuto.auto_tac ~params:(l,params) ?trace_ref:None + | `Term t -> apply_tac t + +let extract_conclusion_type status goal = + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let status,gty = term_of_cic_term status gty ctx in + gty +;; + +let same_type_as_conclusion 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 + let (_,_,metasenv,subst,_) = status#obj in + let status,ty = term_of_cic_term status cicterm ctx in + if NCicReduction.alpha_eq status metasenv subst ctx t ty then + true + else + false +;; + +let same_type t1 t2 status goal = + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let status1,cicterm1 = disambiguate status ctx t1 `XTNone in + let status1,term1 = term_of_cic_term status cicterm1 (ctx_of cicterm1) in + let status2,cicterm2 = disambiguate status ctx t2 `XTNone in + let status2,term2 = term_of_cic_term status cicterm2 (ctx_of cicterm2) in + let (_,_,metasenv,subst,_) = status#obj in + if NCicReduction.alpha_eq status1 metasenv subst ctx term1 term2 then + true + else + false +;; + +let assume name ty eqty = + distribute_tac (fun status goal -> + match extract_conclusion_type status goal with + | NCic.Prod (_,t,_) -> + if same_type_as_conclusion ty t status goal then + match eqty with + | None -> + let (_,_,ty) = ty in + exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit + `JustOne)))) status goal + + | Some eqty -> + if same_type ty eqty status goal then + let (_,_,eqty) = eqty in + exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some eqty),Ast.Implicit + `JustOne)))) status goal + else + fail (lazy "The two given types are not equivalent") + else + fail (lazy "The assumed type is wrong") + | _ -> fail (lazy "You can't assume without an universal quantification") + ) +;; + +let suppose t1 id t2 = + distribute_tac (fun status goal -> + match extract_conclusion_type status goal with + | NCic.Prod (_,t,_) -> + if same_type_as_conclusion t1 t status goal then + match t2 with + | None -> + let (_,_,t1) = t1 in + exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit + `JustOne)))) status goal + + | Some t2 -> + if same_type t1 t2 status goal then + let (_,_,t2) = t2 in + exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit + `JustOne)))) status goal + else + fail (lazy "The two given proposition are not equivalent") + else + fail (lazy "The supposed proposition is different from the premise") + | _ -> fail (lazy "You can't suppose without a logical implication") + ) + +let we_need_to_prove t id t1 = + distribute_tac (fun status goal -> + match id with + | None -> + ( + match t1 with + (* Change the conclusion of the sequent with t *) + (* Is the pattern correct? Probably not *) + | None -> (* We need to prove t *) + exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t) status goal + | Some t1 -> (* We need to prove t or equivalently t1 *) + if same_type t1 t status goal then + exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1) status goal + else + fail (lazy "The two conclusions are not equivalent") + ) + | Some id -> + ( + let (_,_,npt_t) = t in + match t1 with + | None -> (* We need to prove t (id) *) + exec (block_tac [cut_tac t; exact_tac ("",0,(Ast.LetIn ((Ast.Ident + (id,None),None),npt_t,Ast.Implicit + `JustOne)))]) status goal + | Some t1 -> (* We need to prove t (id) or equivalently t1 *) + exec (block_tac [cut_tac t; change_tac ~where:("",0,(None,[],Some Ast.UserInput)) + ~with_what:t1; exact_tac ("",0,(Ast.LetIn ((Ast.Ident (id,None),None),npt_t,Ast.Implicit + `JustOne)))]) status goal + ) + ) +;; + +let by_just_we_proved just ty id ty' = + let just = mk_just just in + match id with + | None -> + (match ty' with + | None -> (* just we proved P done *) + just + | Some ty' -> (* just we proved P that is equivalent to P' done *) + (* I should probably check that ty' is the same thing as the conclusion of the + sequent of the open goal and that ty and ty' are equivalent *) + block_tac [ change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just] + ) + | Some id -> + let ty',continuation = + match ty' with + | None -> ty,just + | Some ty' -> ty', block_tac [change_tac ~where:("",0,(None,[id,Ast.Implicit `JustOne],None)) + ~with_what:ty; just] + in block_tac [cut_tac ty'; continuation ] +;; + +let bydone just = + mk_just just +;; + +(* +let existselim just id1 t1 t2 id2 = + let aux (proof, goal) = + let (n,metasenv,_subst,bo,ty,attrs) = proof in + let metano,context,_ = CicUtil.lookup_meta goal metasenv in + let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in + let proof' = (n,metasenv,_subst,bo,ty,attrs) in + ProofEngineTypes.apply_tactic ( + Tacticals.thens + ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)])) + ~continuations: + [ Tactics.elim_intros (Cic.Rel 1) + ~mk_fresh_name_callback: + (let i = ref 0 in + fun _ _ _ ~typ -> + incr i; + if !i = 1 then Cic.Name id1 else Cic.Name id2) ; + (mk_just ~dbd ~automation_cache just) + ]) (proof', goal) + in + ProofEngineTypes.mk_tactic aux +;; + +let andelim just t1 id1 t2 id2 = + Tacticals.thens + ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2])) + ~continuations: + [ Tactics.elim_intros (Cic.Rel 1) + ~mk_fresh_name_callback: + (let i = ref 0 in + fun _ _ _ ~typ -> + incr i; + if !i = 1 then Cic.Name id1 else Cic.Name id2) ; + (mk_just ~dbd ~automation_cache just) ] +;; + *) diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli index a7ec0e44d..d345275b4 100644 --- a/matita/components/ng_tactics/declarative.mli +++ b/matita/components/ng_tactics/declarative.mli @@ -23,5 +23,11 @@ * http://cs.unibo.it/helm/. *) -val assume : string -> NotationPt.term -> 's NTacStatus.tactic -val suppose : NotationPt.term -> string -> NotationPt.term option -> 's NTacStatus.tactic +type just = [ `Term of NTacStatus.tactic_term | `Auto of NTacStatus.tactic_term GrafiteAst.aauto_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 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/matita/matita.lang b/matita/matita/matita.lang index 6fa587de3..c6d55ae38 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -112,6 +112,14 @@ is equivalent to + we + need + prove + or + equivalently + by + done + proved alias -- 2.39.2