X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2Fdeclarative.ml;fp=matita%2Fcomponents%2Fng_tactics%2Fdeclarative.ml;h=eb0966570b5d3af71b4c8e44ac81801953d63aa1;hb=433e66b381d1b89e48c05d517494fc300fd0abb5;hp=ae07c18ee7361ffad9188ba0171a89fe61804146;hpb=185541ccf10a6c4bf69b3db36fdc4ebc09e4cc42;p=helm.git 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) ] +;; + *)