From: Enrico Zoli Date: Thu, 1 Mar 2007 12:15:24 +0000 (+0000) Subject: "by j let x : T such that P(x)" generalized to allow arbitrary justifications. X-Git-Tag: 0.4.95@7852~581 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd5b3afb330c2efc69b97cc8762b71bd86685acd;p=helm.git "by j let x : T such that P(x)" generalized to allow arbitrary justifications. The code and behaviour should be cleaned up a little bit. --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 24fb99d79..1ec71be92 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -93,7 +93,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Byinduction of loc * 'term * 'ident | Thesisbecomes of loc * 'term | Case of loc * string * (string * 'term) list - | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term + | ExistsElim of loc * 'term option * 'ident * 'term * 'ident * 'lazy_term | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term | RewritingStep of loc * (string option * 'term) option * 'term * diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 423e68d4f..e433c9b7b 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -166,7 +166,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | 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 - | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ term_pp term0 ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ term_pp term1 ^ "(" ^ ident1 ^ ")" + | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_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 (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2) ^ (if cont then " done" else "") | Case (_, id, args) -> diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 1714bf470..db08a6038 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -173,7 +173,8 @@ let tactic_of_ast status ast = | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) -> - Declarative.existselim t id1 t1 id2 t2 + Declarative.existselim ~dbd:(LibraryDb.instance()) + ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2 | GrafiteAst.Case (_,id,params) -> Declarative.case id params | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2 | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 0c64bbb07..cc8360c28 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -297,9 +297,14 @@ let disambiguate_tactic let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Thesisbecomes (loc, cic) | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) -> - let metasenv,cic = disambiguate_term context metasenv term in + 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 + let cic''= disambiguate_lazy_term 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 diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index fd757d141..3653c4606 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -253,12 +253,12 @@ EXTEND | BYC_weproved (ty,id,t1) -> GrafiteAst.By_term_we_proved(loc, t', ty, id, t1) | BYC_letsuchthat (id1,t1,id2,t2) -> - (match t with + (* (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)) + | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*) | BYC_wehaveand (id1,t1,id2,t2) -> (match t with LNone floc -> diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index c669a4161..110f72fb1 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -121,18 +121,37 @@ let we_need_to_prove t id ty = ProofEngineTypes.mk_tactic aux ;; -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 existselim ~dbd ~universe t id1 t1 id2 t2 = + let aux (proof, goal) = + let (n,metasenv,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,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) ; + (match t with + None -> Tactics.auto ~dbd ~params:[] ~universe + | Some t -> Tactics.apply t) + ]) (proof', goal) + in + ProofEngineTypes.mk_tactic aux +;; -let andelim = existselim;; +let andelim t id1 t1 id2 t2 = + 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 rewritingstep ~dbd ~universe lhs rhs just last_step = let aux ((proof,goal) as status) = diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli index 4693085d2..a42faac4b 100644 --- a/components/tactics/declarative.mli +++ b/components/tactics/declarative.mli @@ -48,7 +48,8 @@ val thesisbecomes : Cic.term -> ProofEngineTypes.tactic val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic val existselim : - Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> universe:Universe.universe -> + Cic.term option -> string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic val andelim : Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 47119060b..deaf84aa6 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Feb 25 17:03:54 CET 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar 1 10:25:04 CET 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS :