From: maiorino Date: Thu, 27 Jul 2006 14:47:57 +0000 (+0000) Subject: Declarative tactics for rewriting steps, elimination of the existential X-Git-Tag: 0.4.95@7852~1140 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=36243ef64310a9ea2e51a0295744ab5de7abe055;p=helm.git Declarative tactics for rewriting steps, elimination of the existential quantifier and elimination of conjunciton implemented. --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 65e35634f..dc7db34bc 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -95,9 +95,10 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Byinduction of loc * 'term * 'ident | Thesisbecomes of loc * 'term | Case of loc * string * (string * 'term) list - | Let1 of loc * 'ident * 'term * 'term - | Bywehave of loc * 'term option * 'term * 'ident * 'term * 'ident - | RewritingStep of loc * 'term option * 'term * 'term option + | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term + | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term + | RewritingStep of + loc * 'term option * 'term * 'term option * Cic.name option type search_kind = [ `Locate | `Hint | `Match | `Elim ] @@ -116,7 +117,7 @@ type 'term macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 7 +let magic = 8 type 'obj command = | Default of loc * string * UriManager.uri list diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 8f037f032..7d12c2129 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -163,10 +163,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1) | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1 | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")" - | Thesisbecomes (_, term) -> "the thesis becomes" ^ term_pp term - | Let1 (_, ident, term, term1) -> "let" ^ ident ^ ":" ^ term_pp term ^ "such that" ^ term_pp term1 - | Bywehave (_, term, term1, ident, term2, ident1) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we have" ^ term_pp term1 ^ "(" ^ ident ^ ")" ^ "and" ^ term_pp term2 ^ "(" ^ ident1 ^ ")" - | RewritingStep (_, term, term1, term2 ) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2 ) + | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term + | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ term_pp term0 ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ term_pp term1 ^ "(" ^ ident1 ^ ")" + | AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" + | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2) ^ (match cont with None -> " done" | Some Cic.Anonymous -> "" | Some (Cic.Name id) -> " we proved " ^ id) | Case (_, id, args) -> "case" ^ id ^ String.concat " " diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index c96de1896..6c31f906a 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -166,10 +166,12 @@ let tactic_of_ast ast = Declarative.we_proceed_by_induction_on t t1 | GrafiteAst.Byinduction (_, t, id) -> Declarative.assume id t | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t - | GrafiteAst.Let1 (_, id, t, t1) -> Declarative.let1 id t t1 + | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) -> + Declarative.existselim t id1 t1 id2 t2 | GrafiteAst.Case (_,id,params) -> Declarative.case id params - | GrafiteAst.Bywehave(_,t,t1,id,t2,id1) -> Declarative.bywehave t t1 id t2 id1 - | GrafiteAst.RewritingStep (_,termine,t1,t2) -> Declarative.prova termine t1 t2 + | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2 + | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> + Declarative.rewritingstep termine t1 t2 cont let classify_tactic tactic = match tactic with diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 2e7f1224f..e4df929d7 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -306,20 +306,16 @@ let disambiguate_tactic | GrafiteAst.Thesisbecomes (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Thesisbecomes (loc, cic) - | GrafiteAst.Let1 (loc, id, term, term1) -> + | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) -> let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic'= disambiguate_term context metasenv term1 in - metasenv,GrafiteAst.Let1(loc, id, cic, cic') - | GrafiteAst.Bywehave (loc, term, term1, id, term2, id1) -> - let metasenv,cic = - match term with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in + let metasenv,cic' = disambiguate_term context metasenv term1 in + let metasenv,cic''= disambiguate_term context metasenv term2 in + metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'') + | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) -> + let metasenv,cic = disambiguate_term context metasenv term in let metasenv,cic'= disambiguate_term context metasenv term1 in let metasenv,cic''= disambiguate_term context metasenv term2 in - metasenv,GrafiteAst.Bywehave(loc, cic, cic', id, cic'', id1) + metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'') | GrafiteAst.Case (loc, id, params) -> let metasenv,params' = List.fold_right @@ -329,7 +325,7 @@ let disambiguate_tactic ) params (metasenv,[]) in metasenv,GrafiteAst.Case(loc, id, params') - | GrafiteAst.RewritingStep (loc, term1, term2, term3) -> + | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) -> let metasenv,cic = match term1 with None -> metasenv,None @@ -343,7 +339,7 @@ let disambiguate_tactic | Some t -> let metasenv,t = disambiguate_term context metasenv t in metasenv,Some t in - metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'') + metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) = diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 5d6dac771..1eb2a495d 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -53,6 +53,12 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) let default_precedence = 50 let default_associativity = Gramext.NonA +type by_continuation = + BYC_done + | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option + | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term + | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term + EXTEND GLOBAL: term statement; arg: [ @@ -236,12 +242,27 @@ EXTEND GrafiteAst.Assume (loc, id, t) | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']-> GrafiteAst.Suppose (loc, t, id, t1) - | IDENT "by" ; t = [t' = tactic_term -> Some t' | SYMBOL "_" -> None]; + | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc]; cont=by_continuation -> + let t' = match t with LNone _ -> None | LSome t -> Some t in (match cont with - None -> GrafiteAst.Bydone (loc, t) - | Some (ty,id,t1) -> - GrafiteAst.By_term_we_proved(loc, t, ty, id, t1)) + BYC_done -> GrafiteAst.Bydone (loc, t') + | BYC_weproved (ty,id,t1) -> + GrafiteAst.By_term_we_proved(loc, t', ty, id, t1) + | BYC_letsuchthat (id1,t1,id2,t2) -> + (match t with + LNone floc -> + raise (HExtlib.Localized + (floc,CicNotationParser.Parse_error + "tactic_term expected here")) + | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2)) + | BYC_wehaveand (id1,t1,id2,t2) -> + (match t with + LNone floc -> + raise (HExtlib.Localized + (floc,CicNotationParser.Parse_error + "tactic_term expected here")) + | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2))) | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> GrafiteAst.We_need_to_prove (loc, t, id, t1) | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> @@ -253,19 +274,27 @@ EXTEND | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> GrafiteAst.Case(loc,id,params) - | IDENT "let" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ; IDENT "such" ; IDENT "that" ; t1=tactic_term -> - GrafiteAst.Let1 (loc, id, t, t1) - | IDENT "by" ; t=[t'=tactic_term->Some t'|SYMBOL "_"-> None] ; IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id=IDENT ; RPAREN ; IDENT "and" ; t2=tactic_term ; LPAREN ; id1=IDENT ; RPAREN -> - GrafiteAst.Bywehave (loc, t, t1, id, t2, id1) - | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] -> - GrafiteAst.RewritingStep(loc, Some termine, t1, t2) - | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] -> - GrafiteAst.RewritingStep(loc, None, t1, t2) + | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont) + | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, None, t1, t2, cont) ] ]; by_continuation: [ - [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> Some (ty,id,t1) - | IDENT "done" -> None + [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,id,t1) + | IDENT "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) + | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ; + "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> + BYC_wehaveand (id1,t1,id2,t2) + ] +]; + rewriting_step_continuation : [ + [ IDENT "done" -> None + | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id) + | -> Some Cic.Anonymous ] ]; atomic_tactical: diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 1604d92d8..3a24b0d5f 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -34,16 +34,18 @@ let assume id t = ;; let suppose t id ty = +(*BUG: ty not used *) Tacticals.then_ ~start: (Tactics.intros ~howmany:1 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ()) ~continuation: - (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) - (fun _ metasenv ugraph -> t,metasenv,ugraph)) + (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> t,metasenv,ugraph)) ;; let by_term_we_proved t ty id ty' = +(*BUG: ty' not used *) match t with None -> assert false | Some t -> @@ -63,6 +65,7 @@ let bydone t = ;; let we_need_to_prove t id ty = +(*BUG: ty not used *) let aux status = let proof,goals = ProofEngineTypes.apply_tactic @@ -80,10 +83,98 @@ let we_need_to_prove t id ty = ProofEngineTypes.mk_tactic aux ;; -let prova _ = assert false -;; -let bywehave _ = assert false +let existselim t id1 t1 id2 t2 = +(*BUG: t1 and t2 not used *) +(*PARSING BUG: t2 is parsed in the current context, but it may + have occurrences of id1 in it *) + Tactics.elim_intros t + ~mk_fresh_name_callback: + (let i = ref 0 in + fun _ _ _ ~typ -> + incr i; + if !i = 1 then Cic.Name id1 else Cic.Name id2) + +let andelim = existselim;; + +let rewritingstep lhs rhs just conclude = + let aux ((proof,goal) as status) = + let (curi,metasenv,proofbo,proofty) = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let eq,trans = + match LibraryObjects.eq_URI () with + None -> assert false (*TODO*) + | Some uri -> + Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[]) + in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in + let just = + match just with + None -> assert false (*TOOD*) + | Some just -> just + in + match lhs with + None -> + let plhs,prhs = + match + fst + (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1) + CicUniv.empty_ugraph) + with + Cic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> assert false in + let last_hyp_name = + match context with + (Some (Cic.Name id,_))::_ -> id + | _ -> assert false + in + (match conclude with + None -> + ProofEngineTypes.apply_tactic + (Tacticals.thens + ~start:(Tactics.apply ~term:trans) + ~continuations: + [ Tactics.apply prhs ; + Tactics.apply (Cic.Rel 1) ; + Tactics.apply just]) status + | Some name -> + let mk_fresh_name_callback = + fun metasenv context _ ~typ -> + FreshNamesGenerator.mk_fresh_name ~subst:[] + metasenv context name ~typ + in + ProofEngineTypes.apply_tactic + (Tacticals.thens + ~start:(Tactics.cut ~mk_fresh_name_callback + (Cic.Appl [eq ; ty ; plhs ; rhs])) + ~continuations: + [ Tactics.clear ~hyps:[last_hyp_name] ; + Tacticals.thens + ~start:(Tactics.apply ~term:trans) + ~continuations: + [ Tactics.apply prhs ; + Tactics.apply (Cic.Rel 1) ; + Tactics.apply just] + ]) status) + | Some lhs -> + match conclude with + None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status + | Some name -> + let mk_fresh_name_callback = + fun metasenv context _ ~typ -> + FreshNamesGenerator.mk_fresh_name ~subst:[] + metasenv context name ~typ + in + ProofEngineTypes.apply_tactic + (Tacticals.thens + ~start: + (Tactics.cut ~mk_fresh_name_callback + (Cic.Appl [eq ; ty ; lhs ; rhs])) + ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status + in + ProofEngineTypes.mk_tactic aux ;; + let case _ = assert false ;; let thesisbecomes _ = assert false @@ -92,4 +183,3 @@ let byinduction _ = assert false ;; let we_proceed_by_induction_on _ = assert false ;; -let let1 _ = assert false diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli index ba2eaaea4..6e3a7b696 100644 --- a/components/tactics/declarative.mli +++ b/components/tactics/declarative.mli @@ -42,11 +42,12 @@ val thesisbecomes : Cic.term -> ProofEngineTypes.tactic val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic -val let1 : string -> Cic.term -> Cic.term -> ProofEngineTypes.tactic +val existselim : + Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic -val bywehave : - Cic.term option -> Cic.term -> string -> Cic.term -> string -> - ProofEngineTypes.tactic +val andelim : + Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic -val prova : - Cic.term option -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic +val rewritingstep : + Cic.term option -> Cic.term -> Cic.term option -> Cic.name option -> + ProofEngineTypes.tactic diff --git a/matita/matita.lang b/matita/matita.lang index 0dbfa4c78..3aa42083e 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -153,6 +153,7 @@ know case obtain + done diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma index 285d07c23..e2035d182 100644 --- a/matita/tests/decl.ma +++ b/matita/tests/decl.ma @@ -71,4 +71,29 @@ theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O. ] ] qed. - \ No newline at end of file + + +theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True. + assume P: Prop. + suppose (P ∧ ∃m:nat.m ≠ m) (H). + by H we have P (H1) and (∃x:nat.x≠x) (H2). + (*BUG: + by H2 let q:nat such that (q ≠ q) (Ineq). + *) + (* the next line is wrong, but for the moment it does the job *) + by H2 let q:nat such that False (Ineq). + by I done. +qed. + +theorem easy4: ∀n,m,p. n = m → S m = S p → n = S p → S n = n. +assume n: nat. +assume m:nat. +assume p:nat. +suppose (n=m) (H). +suppose (S m = S p) (K). +suppose (n = S p) (L). +obtain (S n) = (S m) by (eq_f ? ? ? ? ? H). + = (S p) by K. + = n by (sym_eq ? ? ? L) +done. +qed.