From 5649890273cf8e660bba744e84ce5fee1e5efe69 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Mar 2008 17:42:42 +0000 Subject: [PATCH] changed auto_tac params type and all derivate tactics like applyS and demodulate honors the same syntax. new syntax for auto parameters: auto string-params by only_terms_to_use new syntax for declarative eq chains: [(conclude|obtain H) t1] = t2 (auto-params|exact t|using t|proof) exact t : apply t using t : 1 demodulation step using t auto-params : first [ auto ; auto paramodulation ] proof : id_tac manual still to be updated --- .../content_pres/cicNotationLexer.ml | 2 +- .../components/content_pres/content2pres.ml | 20 +- .../software/components/grafite/grafiteAst.ml | 15 +- .../components/grafite/grafiteAstPp.ml | 39 +- .../grafite_engine/grafiteEngine.ml | 5 +- .../grafite_parser/grafiteDisambiguate.ml | 34 +- .../grafite_parser/grafiteParser.ml | 63 ++- helm/software/components/tactics/auto.ml | 375 ++++++------------ helm/software/components/tactics/auto.mli | 13 +- .../components/tactics/declarative.ml | 31 +- .../components/tactics/declarative.mli | 3 +- helm/software/components/tactics/tactics.mli | 13 +- helm/software/components/tactics/universe.mli | 1 + .../components/tptp_grafite/tptp2grafite.ml | 6 +- .../matita/library/demo/power_derivative.ma | 95 ++++- helm/software/matita/matitaScript.ml | 2 +- helm/software/matita/tests/decl.ma | 6 +- .../matita/tests/demodulation_matita.ma | 3 +- 18 files changed, 362 insertions(+), 364 deletions(-) diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 911ddc57e..9d7f2f99d 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -110,7 +110,7 @@ let level2_ast_keywords = Hashtbl.create 23 let _ = List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; - "with"; "in"; "and"; "to"; "as"; "on"; "return" ] + "with"; "in"; "by"; "and"; "to"; "as"; "on"; "return"; "done" ] let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k () let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index b9e897694..228b6fdeb 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -121,7 +121,7 @@ let add_xref id = function | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) | _ -> assert false (* TODO, add_xref is meaningful for all boxes *) -let rec justification ~ignore_atoms term2pres p = +let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = if p.Con.proof_conclude.Con.conclude_method = "Exact" && ignore_atoms then @@ -136,10 +136,16 @@ let rec justification ~ignore_atoms term2pres p = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in [B.H([], - (B.b_kw "by")::B.b_space:: + (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by")):: + B.b_space:: B.Text([],"(")::pres_args@[B.Text([],")")])], None else - [B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"])], + [B.H([], + if for_rewriting_step then + [B.b_kw "proof"] + else + [B.b_kw "by"; B.b_space; B.b_kw "proof"] + )], Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)]) and proof2pres ?skip_initial_lambdas is_top_down term2pres p = @@ -441,7 +447,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( || conclude.Con.conclude_method = "RewriteRL" then let justif1,justif2 = (match (List.nth conclude.Con.conclude_args 6) with - Con.ArgProof p -> justification ~ignore_atoms:true term2pres p + Con.ArgProof p -> + justification ~for_rewriting_step:true ~ignore_atoms:true + term2pres p | _ -> assert false) in let justif = match justif2 with @@ -483,7 +491,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.V([], justif @ [B.b_kw "by _"]) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = - let j1,j2 = justification ~ignore_atoms:false term2pres p in + let j1,j2 = + justification ~for_rewriting_step:true ~ignore_atoms:false term2pres p + in j1, match j2 with Some j -> [j] | None -> [] in let rec aux args = diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 6b20ab9c8..5668b3cba 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -40,6 +40,8 @@ type 'lazy_term reduction = type 'ident intros_spec = int option * 'ident option list +type 'term auto_params = 'term list * (string*string) list + type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Higher order tactics (i.e. tacticals) *) | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic @@ -57,9 +59,9 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Real tactics *) | Absurd of loc * 'term | Apply of loc * 'term - | ApplyS of loc * 'term * (string * string) list + | ApplyS of loc * 'term * 'term auto_params | Assumption of loc - | AutoBatch of loc * (string * string) list + | AutoBatch of loc * 'term auto_params | Cases of loc * 'term * 'ident intros_spec | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident list @@ -69,7 +71,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Contradiction of loc | Cut of loc * 'ident option * 'term | Decompose of loc * 'ident option list - | Demodulate of loc + | Demodulate of loc * 'term auto_params | Destruct of loc * 'term list option | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern * 'ident intros_spec @@ -97,7 +99,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Split of loc | Symmetry of loc | Transitivity of loc * 'term - (* Costruttori Aggiunti *) + (* Declarative language *) | Assume of loc * 'ident * 'term | Suppose of loc * 'term *'ident * 'term option | By_term_we_proved of loc *'term option * 'term * 'ident option * 'term option @@ -112,7 +114,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term | RewritingStep of loc * (string option * 'term) option * 'term * - [ `Term of 'term | `Auto of (string * string) list | `Proof ] * + [ `Term of 'term | `Auto of 'term auto_params + | `Proof | `SolveWith of 'term ] * bool (* last step*) type search_kind = [ `Locate | `Hint | `Match | `Elim ] @@ -132,7 +135,7 @@ type 'term macro = (* real macros *) | Check of loc * 'term | Hint of loc * bool - | AutoInteractive of loc * (string * string) list + | AutoInteractive of loc * 'term auto_params | Inline of loc * presentation_style * string * string (* URI or base-uri, name prefix *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index fd3c444b9..a98fb8e9d 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -73,6 +73,15 @@ let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms) let opt_string_pp = function | None -> "" | Some what -> what ^ " " + +let pp_auto_params ~term_pp (univ, params) = + String.concat " " + (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^ + if univ <> [] then + (if params <> [] then " " else "") ^ "by " ^ + String.concat " " (List.map term_pp univ) + else "" +;; let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = let pp_terms = pp_terms ~term_pp in @@ -100,12 +109,9 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term | ApplyS (_, term, params) -> - "applyS " ^ term_pp term ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) - | AutoBatch (_,params) -> "auto batch " ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) + "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params + | AutoBatch (_,params) -> "autobatch " ^ + pp_auto_params ~term_pp params | Assumption _ -> "assumption" | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^ pp_intros_specs "names " specs @@ -126,7 +132,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | Decompose (_, names) -> Printf.sprintf "decompose%s" (pp_intros_specs "names " (None, names)) - | Demodulate _ -> "demodulate" + | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params | Destruct (_, None) -> "destruct" | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms | Elim (_, what, using, pattern, specs) -> @@ -194,7 +200,20 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term | 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 ^ " by " ^ (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 | `Proof -> "proof") ^ (if cont then " done" else "") + | 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 -> pp_auto_params ~term_pp params + | `Term term2 -> " exact " ^ term_pp term2 + | `Proof -> " proof" + | `SolveWith term -> " using " ^ term_pp term) + ^ (if cont then " done" else "") | Case (_, id, args) -> "case" ^ id ^ String.concat " " @@ -242,9 +261,7 @@ let pp_macro ~term_pp = | Check (_, term) -> Printf.sprintf "check %s" (term_pp term) | Hint (_, true) -> "hint rewrite" | Hint (_, false) -> "hint" - | AutoInteractive (_,params) -> "auto " ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) + | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params | Inline (_, style, suri, prefix) -> Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index aa056f3e2..bc56ce35d 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -107,9 +107,10 @@ let rec tactic_of_ast status ast = | GrafiteAst.Decompose (_, names) -> let mk_fresh_name_callback = namer_of names in Tactics.decompose ~mk_fresh_name_callback () - | GrafiteAst.Demodulate _ -> + | GrafiteAst.Demodulate (_, params) -> Tactics.demodulate - ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe + ~dbd:(LibraryDb.instance ()) ~params + ~universe:status.GrafiteTypes.universe | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index dfaf5b424..516c4af20 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -108,6 +108,18 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function | `Whd as kind -> kind ;; +let disambiguate_auto_params + disambiguate_term metasenv context (terms, params) += + let metasenv, terms = + List.fold_right + (fun t (metasenv, terms) -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,t::terms) terms (metasenv, []) + in + metasenv, (terms, params) +;; + let rec disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tactic) = @@ -121,6 +133,9 @@ let rec disambiguate_tactic disambiguate_lazy_term text prefix_len lexicon_status_ref in let disambiguate_tactic metasenv tac = disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tac) + in + let disambiguate_auto_params m p = + disambiguate_auto_params disambiguate_term m context p in match tactic with (* Higher order tactics *) @@ -181,11 +196,13 @@ let rec disambiguate_tactic let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Apply (loc, cic) | GrafiteAst.ApplyS (loc, term, params) -> + let metasenv, params = disambiguate_auto_params metasenv params in let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.ApplyS (loc, cic, params) | GrafiteAst.Assumption loc -> metasenv,GrafiteAst.Assumption loc | GrafiteAst.AutoBatch (loc,params) -> + let metasenv, params = disambiguate_auto_params metasenv params in metasenv,GrafiteAst.AutoBatch (loc,params) | GrafiteAst.Cases (loc, what, idents) -> let metasenv,what = disambiguate_term context metasenv what in @@ -217,8 +234,9 @@ let rec disambiguate_tactic metasenv,GrafiteAst.Cut (loc, ident, cic) | GrafiteAst.Decompose (loc, names) -> metasenv,GrafiteAst.Decompose (loc, names) - | GrafiteAst.Demodulate loc -> - metasenv,GrafiteAst.Demodulate loc + | GrafiteAst.Demodulate (loc, params) -> + let metasenv, params = disambiguate_auto_params metasenv params in + metasenv,GrafiteAst.Demodulate (loc, params) | GrafiteAst.Destruct (loc, Some terms) -> let map term (metasenv, terms) = let metasenv, term = disambiguate_term context metasenv term in @@ -401,7 +419,12 @@ let rec disambiguate_tactic let metasenv,cic'= disambiguate_term context metasenv term2 in let metasenv,cic'' = match term3 with - `Auto _ as t -> metasenv,t + | `SolveWith term -> + let metasenv,term = disambiguate_term context metasenv term in + metasenv, `SolveWith term + | `Auto params -> + let metasenv, params = disambiguate_auto_params metasenv params in + metasenv,`Auto params | `Term t -> let metasenv,t = disambiguate_term context metasenv t in metasenv,`Term t @@ -495,7 +518,10 @@ let disambiguate_macro | GrafiteAst.Check (loc,term) -> let metasenv,term = disambiguate_term context metasenv term in metasenv,GrafiteAst.Check (loc,term) - | GrafiteAst.AutoInteractive _ + | GrafiteAst.AutoInteractive (loc, params) -> + let metasenv, params = + disambiguate_auto_params disambiguate_term metasenv context params in + metasenv, GrafiteAst.AutoInteractive (loc, params) | GrafiteAst.Hint _ | GrafiteAst.WLocate _ | GrafiteAst.Inline _ as macro -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 378931c14..0b1398016 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -141,9 +141,7 @@ EXTEND GrafiteAst.Absurd (loc, t) | IDENT "apply"; t = tactic_term -> GrafiteAst.Apply (loc, t) - | IDENT "applyS"; t = tactic_term ; params = - LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> - string_of_int v | v = IDENT -> v ] -> i,v ] -> + | IDENT "applyS"; t = tactic_term ; params = auto_params -> GrafiteAst.ApplyS (loc, t, params) | IDENT "assumption" -> GrafiteAst.Assumption loc @@ -171,7 +169,7 @@ EXTEND | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] -> let idents = match idents with None -> [] | Some idents -> idents in GrafiteAst.Decompose (loc, idents) - | IDENT "demodulate" -> GrafiteAst.Demodulate loc + | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p) | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] -> GrafiteAst.Destruct (loc, xts) | IDENT "elim"; what = tactic_term; using = using; @@ -257,7 +255,7 @@ 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 -> LSome t' | SYMBOL "_" -> LNone loc]; + | "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 @@ -280,58 +278,47 @@ EXTEND | LSome t -> GrafiteAst.AndElim (loc, t, 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']-> GrafiteAst.We_need_to_prove (loc, t, id, t1) - | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> GrafiteAst.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 -> + | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> GrafiteAst.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 -> + | "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> GrafiteAst.Byinduction(loc, t, id) | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term -> GrafiteAst.Thesisbecomes(loc, t) | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> GrafiteAst.Case(loc,id,params) - | start = - [ IDENT "conclude" -> None - | IDENT "obtain" ; name = IDENT -> Some name ] ; - termine = tactic_term ; + | start = OPT [ + start = + [ IDENT "conclude" -> None + | IDENT "obtain" ; name = IDENT -> Some name ] ; + termine = tactic_term -> start, termine]; SYMBOL "=" ; t1=tactic_term ; - IDENT "by" ; t2 = - [ t=tactic_term -> `Term t - | SYMBOL "_" ; params = auto_params' -> `Auto params - | IDENT "proof" -> `Proof] ; + [ IDENT "exact"; t=tactic_term -> `Term t + | IDENT "using"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> `Auto params]; cont = rewriting_step_continuation -> - GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont) - | SYMBOL "=" ; - t1=tactic_term ; - IDENT "by" ; - t2= - [ t=tactic_term -> `Term t - | SYMBOL "_" ; params = auto_params' -> `Auto params - | IDENT "proof" -> `Proof] ; - cont=rewriting_step_continuation -> - GrafiteAst.RewritingStep(loc, None, t1, t2, cont) + GrafiteAst.RewritingStep(loc, start, t1, t2, cont) ] ]; auto_params: [ [ params = LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> - string_of_int v | v = IDENT -> v ] -> i,v ] -> + string_of_int v | v = IDENT -> v ] -> i,v ]; + tl = OPT [ "by"; tl = LIST1 tactic_term -> tl] -> + (match tl with Some l -> l | None -> []), params ] -]; - auto_params': [ - [ LPAREN; params = auto_params; RPAREN -> params - | -> [] - ] ]; 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] -> BYC_weproved (ty,Some id,t1) | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; - IDENT "done" -> BYC_weproved (ty,None,t1) - | IDENT "done" -> BYC_done + "done" -> BYC_weproved (ty,None,t1) + | "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 -> @@ -339,7 +326,7 @@ EXTEND ] ]; rewriting_step_continuation : [ - [ IDENT "done" -> true + [ "done" -> true | -> false ] ]; @@ -652,11 +639,11 @@ EXTEND let uris = List.map UriManager.uri_of_string uris in GrafiteAst.Default (loc,what,uris) | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ; - refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ; + refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; "by" ; refl = tactic_term -> refl ] ; - sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ; + sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; "by" ; sym = tactic_term -> sym ] ; - trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ; + trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; "by" ; trans = tactic_term -> trans ] ; "as" ; id = IDENT -> GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 9be698dcf..41ea1e5e4 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -30,6 +30,8 @@ let debug = false;; let debug_print s = if debug then prerr_endline (Lazy.force s);; +type auto_params = Cic.term list * (string * string) list + let elems = ref [] ;; (* closing a term w.r.t. its metavariables @@ -480,6 +482,80 @@ let find_context_equalities indexes, equalities, maxm, cache ;; +(********** PARAMETERS PASSING ***************) + +let bool params name default = + try + let s = List.assoc name params in + if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true + else if s = "0" || s = "false" || s = "no" || s= "off" then false + else + let msg = "Unrecognized value for parameter "^name^"\n" in + let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in + raise (ProofEngineTypes.Fail (lazy msg)) + with Not_found -> default +;; + +let string params name default = + try List.assoc name params with + | Not_found -> default +;; + +let int params name default = + try int_of_string (List.assoc name params) with + | Not_found -> default + | Failure _ -> + raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) +;; + +let flags_of_params params ?(for_applyS=false) () = + let int = int params in + let bool = bool params in + let close_more = bool "close_more" false in + let use_paramod = bool "use_paramod" true in + let use_only_paramod = + if for_applyS then true else bool "paramodulation" false in + let use_library = bool "library" + ((AutoTypes.default_flags()).AutoTypes.use_library) in + let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in + let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in + let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in + let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in + let do_type = bool "type" false in + let timeout = int "timeout" 0 in + { AutoTypes.maxdepth = + if use_only_paramod then 2 else depth; + AutoTypes.maxwidth = width; + AutoTypes.maxsize = size; + AutoTypes.timeout = + if timeout = 0 then + if for_applyS then Unix.gettimeofday () +. 30.0 + else + infinity + else + Unix.gettimeofday() +. (float_of_int timeout); + AutoTypes.use_library = use_library; + AutoTypes.use_paramod = use_paramod; + AutoTypes.use_only_paramod = use_only_paramod; + AutoTypes.close_more = close_more; + AutoTypes.dont_cache_failures = false; + AutoTypes.maxgoalsizefactor = gsize; + AutoTypes.do_types = do_type; + } + +let universe_of_params metasenv context universe tl = + if tl = [] then universe else + let tys = + List.map + (fun term -> + fst (CicTypeChecker.type_of_aux' metasenv context term + CicUniv.oblivion_ugraph)) + tl + in + Universe.index_list Universe.empty context (List.combine tl tys) +;; + + (***************** applyS *******************) let new_metasenv_and_unify_and_t @@ -542,12 +618,16 @@ let rec count_prods context ty = Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) = +let apply_smart + ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal) += let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let flags = flags_of_params params ~for_applyS:true () in + let universe = universe_of_params metasenv context universe univ in let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -1475,72 +1555,12 @@ let auto flags metasenv tables universe cache context metasenv gl = None,cache ;; -let bool params name default = - try - let s = List.assoc name params in - if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true - else if s = "0" || s = "false" || s = "no" || s= "off" then false - else - let msg = "Unrecognized value for parameter "^name^"\n" in - let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in - raise (ProofEngineTypes.Fail (lazy msg)) - with Not_found -> default -;; - -let string params name default = - try List.assoc name params with - | Not_found -> default -;; - -let int params name default = - try int_of_string (List.assoc name params) with - | Not_found -> default - | Failure _ -> - raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) -;; - -let flags_of_params params ?(for_applyS=false) () = - let int = int params in - let bool = bool params in - let close_more = bool "close_more" false in - let use_paramod = bool "use_paramod" true in - let use_only_paramod = - if for_applyS then true else bool "paramodulation" false in - let use_library = bool "library" - ((AutoTypes.default_flags()).AutoTypes.use_library) in - let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in - let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in - let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in - let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in - let do_type = bool "type" false in - let timeout = int "timeout" 0 in - { AutoTypes.maxdepth = - if use_only_paramod then 2 else depth; - AutoTypes.maxwidth = width; - AutoTypes.maxsize = size; - AutoTypes.timeout = - if timeout = 0 then - if for_applyS then Unix.gettimeofday () +. 30.0 - else - infinity - else - Unix.gettimeofday() +. (float_of_int timeout); - AutoTypes.use_library = use_library; - AutoTypes.use_paramod = use_paramod; - AutoTypes.use_only_paramod = use_only_paramod; - AutoTypes.close_more = close_more; - AutoTypes.dont_cache_failures = false; - AutoTypes.maxgoalsizefactor = gsize; - AutoTypes.do_types = do_type; - } - let applyS_tac ~dbd ~term ~params ~universe = ProofEngineTypes.mk_tactic (fun status -> try let proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] ~universe - (flags_of_params params ~for_applyS:true ()) status + apply_smart ~dbd ~term ~subst:[] ~params ~universe status in proof, gl with @@ -1548,185 +1568,45 @@ let applyS_tac ~dbd ~term ~params ~universe = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) -(* SUPERPOSITION *) - -(* Syntax: - * auto superposition target = NAME - * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only] - * - * - if table is omitted no superposition will be performed - * - if demod_table is omitted no demodulation will be prformed - * - subterms_only is passed to Indexing.superposition_right - * - * lists are coded using _ (example: H_H1_H2) - *) - -let eq_and_ty_of_goal = function - | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> - uri,t - | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) -;; - -let rec find_in_ctx i name = function - | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) - | Some (Cic.Name name', _)::tl when name = name' -> i - | _::tl -> find_in_ctx (i+1) name tl -;; - -let rec position_of i x = function - | [] -> assert false - | j::tl when j <> x -> position_of (i+1) x tl - | _ -> i -;; - - -let superposition_tac ~target ~table ~subterms_only ~demod_table status = - Saturation.reset_refs(); - let proof,goalno = status in - let curi,metasenv,_subst,pbo,pty, attrs = proof in - let metano,context,ty = CicUtil.lookup_meta goalno metasenv in - let eq_uri,tty = eq_and_ty_of_goal ty in - let env = (metasenv, context, CicUniv.empty_ugraph) in - let names = Utils.names_of_context context in - let bag = Equality.mk_equality_bag () in - let eq_index, equalities, maxm,cache = - find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty - in - let eq_what = - let what = find_in_ctx 1 target context in - List.nth equalities (position_of 0 what eq_index) - in - let eq_other = - if table <> "" then - let other = - let others = Str.split (Str.regexp "_") table in - List.map (fun other -> find_in_ctx 1 other context) others - in - List.map - (fun other -> List.nth equalities (position_of 0 other eq_index)) - other - else - [] - in - let index = List.fold_left Indexing.index Indexing.empty eq_other in - let maxm, eql = - if table = "" then maxm,[eq_what] else - Indexing.superposition_right bag - ~subterms_only eq_uri maxm env index eq_what +let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) = + let _,metasenv,_subst,_,_, _ = proof in + let _,context,goalty = CicUtil.lookup_meta goal metasenv in + let universe = universe_of_params metasenv context universe univ in + let flags = flags_of_params params () in + let use_library = flags.use_library in + let tables,cache,newmeta = + init_cache_and_tables ~dbd use_library flags.use_only_paramod true + false universe (proof, goal) in + let tables,cache,newmeta = + if flags.close_more then + close_more + tables newmeta context (proof, goal) + auto_all_solutions universe cache + else tables,cache,newmeta in + let initial_time = Unix.gettimeofday() in + let (_,oldmetasenv,_subst,_,_, _) = proof in + hint := None; + let elem = + metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] in - debug_print (lazy ("Superposition right:")); - debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env)); - debug_print (lazy ("\n table: ")); - List.iter - (fun e -> - debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other; - debug_print (lazy ("\n result: ")); - List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql; - debug_print (lazy ("\n result (cut&paste): ")); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - debug_print (lazy (CicPp.pp t names))) - eql; - debug_print (lazy ("\n result proofs: ")); - List.iter (fun e -> - debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in - let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in - Subst.ppsubst s ^ "\n" ^ - CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql; - if demod_table <> "" then - begin - let eql = - if eql = [] then [eq_what] else eql - in - let demod = - let demod = Str.split (Str.regexp "_") demod_table in - List.map (fun other -> find_in_ctx 1 other context) demod - in - let eq_demod = - List.map - (fun demod -> List.nth equalities (position_of 0 demod eq_index)) - demod - in - let table = List.fold_left Indexing.index Indexing.empty eq_demod in - let maxm,eql = - List.fold_left - (fun (maxm,acc) e -> - let maxm,eq = - Indexing.demodulation_equality bag eq_uri maxm env table e - in - maxm,eq::acc) - (maxm,[]) eql - in - let eql = List.rev eql in - debug_print (lazy ("\n result [demod]: ")); - List.iter - (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql; - debug_print (lazy ("\n result [demod] (cut&paste): ")); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - debug_print (lazy (CicPp.pp t names))) - eql; - end; - proof,[goalno] -;; - -let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) = - (* argument parsing *) - let string = string params in - let bool = bool params in - (* hacks to debug paramod *) - let superposition = bool "superposition" false in - let target = string "target" "" in - let table = string "table" "" in - let subterms_only = bool "subterms_only" false in - let demod_table = string "demod_table" "" in - match superposition with - | true -> - (* this is the ugly hack to debug paramod *) - superposition_tac - ~target ~table ~subterms_only ~demod_table (proof,goal) - | false -> - (* this is the real auto *) - let _,metasenv,_subst,_,_, _ = proof in - let _,context,goalty = CicUtil.lookup_meta goal metasenv in - let flags = flags_of_params params () in - (* just for testing *) - let use_library = flags.use_library in - let tables,cache,newmeta = - init_cache_and_tables ~dbd use_library flags.use_only_paramod true - false universe (proof, goal) in - let tables,cache,newmeta = - if flags.close_more then - close_more - tables newmeta context (proof, goal) - auto_all_solutions universe cache - else tables,cache,newmeta in - let initial_time = Unix.gettimeofday() in - let (_,oldmetasenv,_subst,_,_, _) = proof in - hint := None; - let elem = - metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] - in - match auto_main tables newmeta context flags universe cache [elem] with - | Proved (metasenv,subst,_, tables,cache,_) -> - (*prerr_endline - ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*) - let proof,metasenv = - ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goal subst metasenv - in - let opened = - ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:metasenv - in - proof,opened - | Gaveup (tables,cache,maxm) -> - debug_print - (lazy ("TIME:"^ - string_of_float(Unix.gettimeofday()-.initial_time))); - raise (ProofEngineTypes.Fail (lazy "Auto gave up")) + match auto_main tables newmeta context flags universe cache [elem] with + | Proved (metasenv,subst,_, tables,cache,_) -> + (*prerr_endline + ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*) + let proof,metasenv = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goal subst metasenv + in + let opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv + ~newmetasenv:metasenv + in + proof,opened + | Gaveup (tables,cache,maxm) -> + debug_print + (lazy ("TIME:"^ + string_of_float(Unix.gettimeofday()-.initial_time))); + raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; let auto_tac ~dbd ~params ~universe = @@ -1740,9 +1620,11 @@ let eq_of_goal = function (* performs steps of rewrite with the universe, obtaining if possible * a trivial goal *) -let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)= +let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= let _,metasenv,_subst,_,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in + let steps = int_of_string (string params "steps" "1") in + let universe = universe_of_params metasenv context universe univ in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = (* we take the whole universe (no signature filtering) *) @@ -1774,14 +1656,15 @@ let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)= (ProofEngineTypes.Fail (lazy ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) ;; -let solve_rewrite_tac ~universe ?steps () = - ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps) +let solve_rewrite_tac ~params ~universe () = + ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params) ;; (* DEMODULATE *) -let demodulate_tac ~dbd ~universe (proof,goal)= +let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let universe = universe_of_params metasenv context universe univ in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let initgoal = [], metasenv, ty in let eq_uri = eq_of_goal ty in @@ -1823,8 +1706,8 @@ let demodulate_tac ~dbd ~universe (proof,goal)= ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) ;; -let demodulate_tac ~dbd ~universe = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);; +let demodulate_tac ~dbd ~params ~universe = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);; let pp_proofterm = Equality.pp_proofterm;; diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index a40d00fc5..a300a3132 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -23,30 +23,31 @@ * http://cs.unibo.it/helm/. *) -(* stops at the first solution *) +type auto_params = Cic.term list * (string * string) list + val auto_tac: dbd:HSql.dbd -> - params:(string * string) list -> + params:auto_params -> universe:Universe.universe -> ProofEngineTypes.tactic val applyS_tac: dbd:HSql.dbd -> term: Cic.term -> - params:(string * string) list -> + params:auto_params -> universe:Universe.universe -> ProofEngineTypes.tactic val demodulate_tac : dbd:HSql.dbd -> + params:auto_params -> universe:Universe.universe -> ProofEngineTypes.tactic val solve_rewrite_tac: + params:auto_params -> universe:Universe.universe -> - ?steps:int -> - unit -> - ProofEngineTypes.tactic + unit -> ProofEngineTypes.tactic type auto_status = Cic.context * diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index c248d0cad..db1345344 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -48,7 +48,7 @@ let suppose t id ty = let by_term_we_proved ~dbd ~universe t ty id ty' = let just = match t with - None -> Tactics.auto ~dbd ~params:[] ~universe + | None -> Tactics.auto ~dbd ~params:([],[]) ~universe | Some t -> Tactics.apply t in match id with @@ -86,7 +86,7 @@ let by_term_we_proved ~dbd ~universe t ty id ty' = let bydone ~dbd ~universe t = let just = match t with - None -> Tactics.auto ~dbd ~params:[] ~universe + | None -> Tactics.auto ~dbd ~params:([],[]) ~universe | Some t -> Tactics.apply t in just @@ -144,7 +144,7 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 = incr i; if !i = 1 then Cic.Name id1 else Cic.Name id2) ; (match t with - None -> Tactics.auto ~dbd ~params:[] ~universe + | None -> Tactics.auto ~dbd ~params:([],[]) ~universe | Some t -> Tactics.apply t) ]) (proof', goal) in @@ -173,7 +173,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in let just' = match just with - `Auto params -> + `Auto (univ, params) -> let params = if not (List.exists (fun (k,_) -> k = "timeout") params) then ("timeout","3")::params @@ -185,20 +185,14 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = else params in if params = params' then - Tactics.auto ~dbd ~params ~universe + Tactics.auto ~dbd ~params:(univ, params) ~universe else Tacticals.first - [Tactics.auto ~dbd ~params ~universe ; - Tactics.auto ~dbd ~params:params' ~universe] - | `Term just -> - let ty,_ = - CicTypeChecker.type_of_aux' metasenv context just - CicUniv.empty_ugraph - in - Tactics.solve_rewrite - ~universe:(Universe.index Universe.empty - (Universe.key ty) just) ~steps:1 () - (* Tactics.apply just *) + [Tactics.auto ~dbd ~params:(univ, params) ~universe ; + Tactics.auto ~dbd ~params:(univ, params') ~universe] + | `Term just -> Tactics.apply just + | `SolveWith term -> + Tactics.solve_rewrite ~universe ~params:([term],["steps","1"]) () | `Proof -> Tacticals.id_tac in @@ -249,7 +243,10 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = match just,goals with `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1] | _, [g1;g2] -> [g2;newmeta;g1] - | _ -> assert false + | _, l -> + prerr_endline (String.concat "," (List.map string_of_int l)); + prerr_endline (CicMetaSubst.ppmetasenv [] metasenv); + assert false in proof,goals) in diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli index 8fd91b0e8..08852c79c 100644 --- a/helm/software/components/tactics/declarative.mli +++ b/helm/software/components/tactics/declarative.mli @@ -57,5 +57,6 @@ val andelim : val rewritingstep : dbd:HSql.dbd -> universe:Universe.universe -> (string option * Cic.term) option -> Cic.term -> - [ `Term of Cic.term | `Auto of (string * string) list | `Proof ] -> + [ `Term of Cic.term | `Auto of Auto.auto_params + | `Proof | `SolveWith of Cic.term] -> bool (* last step *) -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index d016bc55d..3c27f52f4 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,15 +1,15 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 10 16:49:47 CET 2008 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar 20 16:36:00 CET 2008 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HSql.dbd -> term:Cic.term -> - params:(string * string) list -> + params:Auto.auto_params -> universe:Universe.universe -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : dbd:HSql.dbd -> - params:(string * string) list -> + params:Auto.auto_params -> universe:Universe.universe -> ProofEngineTypes.tactic val cases_intros : ?howmany:int -> @@ -31,7 +31,9 @@ val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> ProofEngineTypes.tactic val demodulate : - dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic + dbd:HSql.dbd -> + params:Auto.auto_params -> + universe:Universe.universe -> ProofEngineTypes.tactic val destruct : Cic.term list option -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> @@ -95,7 +97,8 @@ val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val solve_rewrite : - universe:Universe.universe -> ?steps:int -> unit -> ProofEngineTypes.tactic + params:Auto.auto_params -> + universe:Universe.universe -> unit -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli index ee5dc489a..9201d92b8 100644 --- a/helm/software/components/tactics/universe.mli +++ b/helm/software/components/tactics/universe.mli @@ -37,6 +37,7 @@ val index_term_and_unfolded_term: universe -> Cic.context -> Cic.term -> Cic.term -> universe val index_local_term: universe -> Cic.context -> Cic.term -> Cic.term -> universe +(* pairs are (term,ty) *) val index_list: universe -> Cic.context -> (Cic.term*Cic.term) list -> universe val remove: diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 667b7e3d6..63dfe0285 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -260,10 +260,10 @@ let convert_ast statements context = function else [])@ [GA.Executable(floc,GA.Tactic(floc, Some ( if ueq_case then - GA.AutoBatch (floc,["paramodulation",""; - "timeout",string_of_int !paramod_timeout]) + GA.AutoBatch (floc,([],["paramodulation",""; + "timeout",string_of_int !paramod_timeout])) else - GA.AutoBatch (floc,["depth",string_of_int !depth]) + GA.AutoBatch (floc,([],["depth",string_of_int !depth])) ), GA.Semicolon(floc))); GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc, diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index e910c8b6a..4f1b44000 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -277,13 +277,12 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n). suppose (0=m) (m_zero). by _ done. conclude (D[x \sup (1+m)]) - = (D[x · x \sup m]) by _. - = (D[x] · x \sup m + x · D[x \sup m]) by _. - = (x \sup m + x · (m · x \sup (pred m))) by _. -clear H. - = (x \sup m + m · (x \sup (1 + pred m))) by _. - = (x \sup m + m · x \sup m) by _. - = ((1+m) · x \sup m) by _ (timeout=120) + = (D[x · x \sup m]). + = (D[x] · x \sup m + x · D[x \sup m]). + = (x \sup m + x · (m · x \sup (pred m))). + = (x \sup m + m · (x \sup (1 + pred m))). + = (x \sup m + m · x \sup m). + = ((1+m) · x \sup m) by Fmult_one_f Fmult_commutative Fmult_Fplus_distr costante_sum done. qed. @@ -320,11 +319,79 @@ theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n. (D[x \sup (2+m)] = (2+m) · x \sup (1+m)). conclude (D[x \sup (2+m)]) - = (D[x · x \sup (1+m)]) by _. - = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]) by _. - = (x \sup (1+m) + x · (costante (1+m) · x \sup m)) by _. -clear H. - = (x \sup (1+m) + costante (1+m) · x \sup (1+m)) by _. - = (x \sup (1+m) · (costante (2 + m))) by _ - done. + = (D[x · x \sup (1+m)]). + = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]). + = (x \sup (1+m) + x · (costante (1+m) · x \sup m)). + = (x \sup (1+m) + costante (1+m) · x \sup (1+m)). + + + + conclude (x \sup (1+m) + costante (1+m) · x \sup (1+m)) + = (costante 1 · x \sup (1+m) + costante (1+m) ·(x) \sup (1+m)) proof. + by (Fmult_one_f ((x)\sup(1+m))) + we proved (costante 1·(x)\sup(1+m)=(x)\sup(1+m)) (previous). + by (eq_OF_eq ? ? (λfoo:(R→R).foo+costante (1+m)·(x)\sup(1+m)) (costante 1 + ·(x)\sup(1 + +m)) ((x)\sup(1 + +m)) previous) + done. + = ((x)\sup(1+m)·costante 1+costante (1+m)·(x)\sup(1+m)) proof. + by (Fmult_commutative (costante 1) ((x)\sup(1+m))) + we proved (costante 1·(x)\sup(1+m)=(x)\sup(1+m)·costante 1) (previous). + by (eq_f ? ? (λfoo:(R→R).foo+costante (1+m)·(x)\sup(1+m)) (costante 1 + ·(x)\sup(1+m)) ((x)\sup(1 + +m) + ·costante + 1) previous) + done. + = ((x)\sup(1+m)·costante 1+(x)\sup(1+m)·costante (1+m)) proof. + by (Fmult_commutative ((x)\sup(1+m)) (costante (1+m))) + we proved ((x)\sup(1+m)·costante (1+m)=costante (1+m)·(x)\sup(1+m)) + + (previous) + . + by (eq_OF_eq ? ? (λfoo:(R→R).(x)\sup(1+m)·costante 1+foo) ((x)\sup(1+m) + ·costante + (1+m)) (costante + (1 + +m) + ·(x)\sup(1 + +m)) previous) + done. + = ((x)\sup(1+m)·(costante 1+costante (1+m))) proof. + by (Fmult_Fplus_distr ((x)\sup(1+m)) (costante 1) (costante (1+m))) + we proved + ((x)\sup(1+m)·(costante 1+costante (1+m)) + =(x)\sup(1+m)·costante 1+(x)\sup(1+m)·costante (1+m)) + + (previous) + . + by (sym_eq ? ((x)\sup(1+m)·(costante 1+costante (1+m))) ((x)\sup(1+m) + ·costante 1 + +(x)\sup(1+m) + ·costante (1+m)) previous) + done. + = ((costante 1+costante (1+m))·(x)\sup(1+m)) + exact (Fmult_commutative ((x)\sup(1+m)) (costante 1+costante (1+m))). + = (costante (1+(1+m))·(x)\sup(1+m)) proof. + by (costante_sum 1 (1+m)) + we proved (costante 1+costante (1+m)=costante (1+(1+m))) (previous). + by (eq_f ? ? (λfoo:(R→R).foo·(x)\sup(1+m)) (costante 1+costante (1+m)) (costante + (1 + +(1 + +m))) previous) + done. + = (costante (1+1+m)·(x)\sup(1+m)) proof. + by (assoc_plus 1 1 m) + we proved (1+1+m=1+(1+m)) (previous). + by (eq_OF_eq ? ? (λfoo:nat.costante foo·(x)\sup(1+m)) ? ? previous) + done. + = (costante (2+m)·(x)\sup(1+m)) proof done. + by (plus_n_SO 1) + we proved (2=1+1) (previous). + by (eq_OF_eq ? ? (λfoo:nat.costante (foo+m)·(x)\sup(1+m)) ? ? previous) + done. + + +(* end auto($Revision: 8206 $) proof: TIME=0.06 SIZE=100 DEPTH=100 *) done. qed. diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index ae33d1f83..a27b01831 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -534,7 +534,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status Auto.revision time size depth in let proof_script = - if List.exists (fun (s,_) -> s = "paramodulation") params then + if List.exists (fun (s,_) -> s = "paramodulation") (snd params) then let proof_term, how_many_lambdas = Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma index 84a597fda..569a2f8ff 100644 --- a/helm/software/matita/tests/decl.ma +++ b/helm/software/matita/tests/decl.ma @@ -138,9 +138,9 @@ assume p:nat. suppose (n=m) (H). suppose (S m = S p) (K). suppose (n = S p) (L). -conclude (S n) = (S m) by _. - = (S p) by _. - = n by _ +conclude (S n) = (S m). + = (S p). + = n done. qed. diff --git a/helm/software/matita/tests/demodulation_matita.ma b/helm/software/matita/tests/demodulation_matita.ma index d1201a6c4..1556359ae 100644 --- a/helm/software/matita/tests/demodulation_matita.ma +++ b/helm/software/matita/tests/demodulation_matita.ma @@ -17,7 +17,8 @@ include "nat/minus.ma". theorem p2: \forall x,y:nat. x+x = (S(S O))*x. -intros.demodulate.reflexivity. +intros. +demodulate by times_n_Sm times_n_O sym_times plus_n_O. qed. theorem p4: \forall x:nat. (x+(S O))*(x-(S O))=x*x - (S O). -- 2.39.2