From: Enrico Tassi Date: Mon, 26 May 2008 14:01:04 +0000 (+0000) Subject: new, more rigid syntax, for auto_params affecting the declarative language. X-Git-Tag: make_still_working~5126 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd93fa0155994b70482e0f07d8e45c238cce835d;p=helm.git new, more rigid syntax, for auto_params affecting the declarative language. many multi-word constructs (like 'we proved') are now a single token. all declarative tactics now use auto_params. syntax of declarative tactics changed. many camlp5 refactoring to avoid many rule conflics. --- diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 9d7f2f99d..bbf7de133 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -50,6 +50,10 @@ let is_ligature_char = true with Not_found -> false)) +let regexp we_proved = "we" ' '+ "proved" +let regexp we_have = "we" ' '+ "have" +let regexp let_rec = "let" ' '+ "rec" +let regexp let_corec = "let" ' '+ "corec" let regexp ident_decoration = '\'' | '?' | '`' let regexp ident_cont = ident_letter | xml_digit | '_' let regexp ident = ident_letter ident_cont* ident_decoration* @@ -109,8 +113,8 @@ let level2_meta_keywords = 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"; "by"; "and"; "to"; "as"; "on"; "return"; "done" ] + [ "CProp"; "Prop"; "Type"; "Set"; "let"; "match"; + "with"; "in"; "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 @@ -274,6 +278,10 @@ let rec ligatures_token k = and level2_ast_token = lexer + | let_rec -> return lexbuf ("LETREC","") + | let_corec -> return lexbuf ("LETCOREC","") + | we_proved -> return lexbuf ("WEPROVED","") + | we_have -> return lexbuf ("WEHAVE","") | utf8_blank+ -> ligatures_token level2_ast_token lexbuf | meta -> let s = Ulexing.utf8_lexeme lexbuf in diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 461e2fc9f..5aac1ef7d 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -496,11 +496,6 @@ EXTEND | _ -> failwith "Invalid index name." ] ]; - induction_kind: [ - [ "rec" -> `Inductive - | "corec" -> `CoInductive - ] - ]; let_defs: [ [ defs = LIST1 [ name = single_arg; @@ -558,9 +553,12 @@ EXTEND [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) - | "let"; k = induction_kind; defs = let_defs; "in"; + | LETCOREC; defs = let_defs; "in"; + body = term -> + return_term loc (Ast.LetRec (`CoInductive, defs, body)) + | LETREC; defs = let_defs; "in"; body = term -> - return_term loc (Ast.LetRec (k, defs, body)) + return_term loc (Ast.LetRec (`Inductive, defs, body)) ] ]; term: LEVEL "20R" (* binder *) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 5668b3cba..fc9ea8c5d 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -42,6 +42,10 @@ type 'ident intros_spec = int option * 'ident option list type 'term auto_params = 'term list * (string*string) list +type 'term just = + [ `Term of 'term + | `Auto of 'term auto_params ] + type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Higher order tactics (i.e. tacticals) *) | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic @@ -102,16 +106,17 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* 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 + | By_just_we_proved of loc * 'term just * + 'term * 'ident option * 'term option | We_need_to_prove of loc * 'term * 'ident option * 'term option - | Bydone of loc * 'term option + | Bydone of loc * 'term just | We_proceed_by_induction_on of loc * 'term * 'term | We_proceed_by_cases_on of loc * 'term * 'term | Byinduction of loc * 'term * 'ident | Thesisbecomes of loc * 'term | Case of loc * string * (string * 'term) list - | ExistsElim of loc * 'term option * 'ident * 'term * 'ident * 'lazy_term - | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term + | ExistsElim of loc * 'term just * 'ident * 'term * 'ident * 'lazy_term + | AndElim of loc * 'term just * 'ident * 'term * 'ident * 'term | RewritingStep of loc * (string option * 'term) option * 'term * [ `Term of 'term | `Auto of 'term auto_params diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index a98fb8e9d..9fa1d05b6 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -83,6 +83,12 @@ let pp_auto_params ~term_pp (univ, params) = else "" ;; +let pp_just ~term_pp = + function + `Term term -> "exact " ^ term_pp term + | `Auto params -> pp_auto_params ~term_pp params +;; + let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = let pp_terms = pp_terms ~term_pp in let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in @@ -190,16 +196,16 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = (* Tattiche Aggiunte *) | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1) - | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done" - | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ + | Bydone (_, just) -> pp_just ~term_pp just ^ "done" + | By_just_we_proved (_, just, term1, ident, term2) -> pp_just ~term_pp just ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match term2 with None -> " " | Some term2 -> term_pp term2) | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1) | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ 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 - | 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 ^ ")" + | ExistsElim (_, just, ident, term, ident1, term1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")" + | AndElim (_, just, ident1, term1, ident2, term2) -> pp_just ~term_pp just ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" | RewritingStep (_, term, term1, term2, cont) -> (match term with | None -> " " diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index a73e53a1f..3746403d9 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -179,9 +179,9 @@ let rec tactic_of_ast status ast = (* Implementazioni Aggiunte *) | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1 - | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) -> - Declarative.by_term_we_proved ~dbd:(LibraryDb.instance()) - ~universe:status.GrafiteTypes.universe t ty id t1 + | GrafiteAst.By_just_we_proved (_, just, ty, id, t1) -> + Declarative.by_just_we_proved ~dbd:(LibraryDb.instance()) + ~universe:status.GrafiteTypes.universe just ty id t1 | GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove t id t2 | GrafiteAst.Bydone (_, t) -> @@ -193,11 +193,13 @@ let rec tactic_of_ast status ast = Declarative.we_proceed_by_induction_on t t1 | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t - | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) -> + | GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) -> Declarative.existselim ~dbd:(LibraryDb.instance()) - ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2 + ~universe:status.GrafiteTypes.universe just 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.AndElim(_,just,id1,t1,id2,t2) -> + Declarative.andelim ~dbd:(LibraryDb.instance ()) + ~universe:status.GrafiteTypes.universe just id1 t1 id2 t2 | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe termine t1 t2 cont diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 516c4af20..73e71c815 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -120,6 +120,18 @@ let disambiguate_auto_params metasenv, (terms, params) ;; +let disambiguate_just disambiguate_term context metasenv = + function + `Term t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv, `Term t + | `Auto params -> + let metasenv,params = disambiguate_auto_params disambiguate_term metasenv + context params + in + metasenv, `Auto params +;; + let rec disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tactic) = @@ -339,14 +351,11 @@ let rec disambiguate_tactic let metasenv,t = disambiguate_term context metasenv t in metasenv,Some t in metasenv,GrafiteAst.Suppose (loc, cic, id, cic') - | GrafiteAst.Bydone (loc,term) -> - let metasenv,cic = - match term with - None -> metasenv,None - |Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in - metasenv,GrafiteAst.Bydone (loc, cic) + | GrafiteAst.Bydone (loc,just) -> + let metasenv,just = + disambiguate_just disambiguate_term context metasenv just + in + metasenv,GrafiteAst.Bydone (loc, just) | GrafiteAst.We_need_to_prove (loc,term,id,term') -> let metasenv,cic = disambiguate_term context metasenv term in let metasenv,cic' = @@ -356,13 +365,9 @@ let rec disambiguate_tactic let metasenv,t = disambiguate_term context metasenv t in metasenv,Some t in metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic') - | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') -> - let metasenv,cic = - match term with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in + | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') -> + let metasenv,just = + disambiguate_just disambiguate_term context metasenv just in let metasenv,cic' = disambiguate_term context metasenv term' in let metasenv,cic'' = match term'' with @@ -370,7 +375,7 @@ let rec disambiguate_tactic | Some t -> let metasenv,t = disambiguate_term context metasenv t in metasenv,Some t in - metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'') + metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'') | GrafiteAst.We_proceed_by_cases_on (loc, term, term') -> let metasenv,cic = disambiguate_term context metasenv term in let metasenv,cic' = disambiguate_term context metasenv term' in @@ -385,21 +390,18 @@ let rec disambiguate_tactic | GrafiteAst.Thesisbecomes (loc, term) -> 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 = - match term with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in + | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) -> + let metasenv,just = + disambiguate_just disambiguate_term context metasenv just in let metasenv,cic' = disambiguate_term context metasenv term1 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 + metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'') + | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) -> + let metasenv,just = + disambiguate_just disambiguate_term context metasenv just in let metasenv,cic'= disambiguate_term context metasenv term1 in let metasenv,cic''= disambiguate_term context metasenv term2 in - metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'') + metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'') | GrafiteAst.Case (loc, id, params) -> let metasenv,params' = List.fold_right diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 0b1398016..101e55a54 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -57,6 +57,35 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) let default_precedence = 50 let default_associativity = Gramext.NonA + +let mk_rec_corec ind_kind defs loc = + (* In case of mutual definitions here we produce just + the syntax tree for the first one. The others will be + generated from the completely specified term just before + insertion in the environment. We use the flavour + `MutualDefinition to rememer this. *) + let name,ty = + match defs with + | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ -> + let ty = + List.fold_right + (fun var ty -> Ast.Binder (`Pi,var,ty) + ) params ty + in + name,ty + | (_,(Ast.Ident (name, None), None),_,_) :: _ -> + name, Ast.Implicit + | _ -> assert false + in + let body = Ast.Ident (name,None) in + let flavour = + if List.length defs = 1 then + `Definition + else + `MutualDefinition + in + GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty, + Some (Ast.LetRec (ind_kind, defs, body)))) type by_continuation = BYC_done @@ -167,22 +196,22 @@ EXTEND | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> GrafiteAst.Cut (loc, ident, t) | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] -> - let idents = match idents with None -> [] | Some idents -> idents in - GrafiteAst.Decompose (loc, idents) + let idents = match idents with None -> [] | Some idents -> idents in + GrafiteAst.Decompose (loc, idents) | 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; pattern = OPT pattern_spec; (num, idents) = intros_spec -> - let pattern = match pattern with - | None -> None, [], Some Ast.UserInput - | Some pattern -> pattern - in - GrafiteAst.Elim (loc, what, using, pattern, (num, idents)) + let pattern = match pattern with + | None -> None, [], Some Ast.UserInput + | Some pattern -> pattern + in + GrafiteAst.Elim (loc, what, using, pattern, (num, idents)) | IDENT "elimType"; what = tactic_term; using = using; (num, idents) = intros_spec -> - GrafiteAst.ElimType (loc, what, using, (num, idents)) + GrafiteAst.ElimType (loc, what, using, (num, idents)) | IDENT "exact"; t = tactic_term -> GrafiteAst.Exact (loc, t) | IDENT "exists" -> @@ -218,7 +247,7 @@ EXTEND to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; ident = OPT [ "as" ; ident = IDENT -> ident ] -> let linear = match linear with None -> false | Some _ -> true in - let to_what = match to_what with None -> [] | Some to_what -> to_what in + let to_what = match to_what with None -> [] | Some to_what -> to_what in GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) | IDENT "left" -> GrafiteAst.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> @@ -238,7 +267,7 @@ EXTEND (CicNotationParser.Parse_error "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) else - let n = match xnames with None -> [] | Some names -> names in + let n = match xnames with None -> [] | Some names -> names in GrafiteAst.Rewrite (loc, d, t, p, n) | IDENT "right" -> GrafiteAst.Right loc @@ -253,76 +282,104 @@ EXTEND (* Produzioni Aggiunte *) | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> 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']-> + | 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) - | "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc]; + | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; + IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; + id2 = IDENT ; RPAREN -> + GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2) + | just = + [ IDENT "using"; t=tactic_term -> `Term t + | params = auto_params -> `Auto params] ; cont=by_continuation -> - let t' = match t with LNone _ -> None | LSome t -> Some t in (match cont with - 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))) + BYC_done -> GrafiteAst.Bydone (loc, just) + | BYC_weproved (ty,id,t1) -> + GrafiteAst.By_just_we_proved(loc, just, ty, id, t1) + | BYC_letsuchthat (id1,t1,id2,t2) -> + GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2) + | BYC_wehaveand (id1,t1,id2,t2) -> + GrafiteAst.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']-> GrafiteAst.We_need_to_prove (loc, t, id, t1) - | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + | IDENT "we" ; IDENT "proceed" ; IDENT "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" ; "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> GrafiteAst.We_proceed_by_induction_on (loc, t, t1) - | "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + | IDENT "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 = OPT [ - start = - [ IDENT "conclude" -> None - | IDENT "obtain" ; name = IDENT -> Some name ] ; - termine = tactic_term -> start, termine]; + GrafiteAst.Case(loc,id,params) + (* DO NOT FACTORIZE with the two following, camlp5 sucks*) + | IDENT "conclude"; + termine = tactic_term; + SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> `Auto params]; + cont = rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont) + | IDENT "obtain" ; name = IDENT; + termine = tactic_term; SYMBOL "=" ; t1=tactic_term ; t2 = - [ IDENT "exact"; t=tactic_term -> `Term t - | IDENT "using"; term=tactic_term -> `SolveWith term + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term | IDENT "proof" -> `Proof | params = auto_params -> `Auto params]; cont = rewriting_step_continuation -> - GrafiteAst.RewritingStep(loc, start, t1, t2, cont) + GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont) + | SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> `Auto params]; + cont = rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, None, t1, t2, cont) ] +]; + auto_fixed_param: [ + [ IDENT "paramodulation" + | IDENT "depth" + | IDENT "width" + | IDENT "size" + | IDENT "timeout" + | IDENT "library" + | IDENT "type" + ] ]; auto_params: [ [ params = - LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> + LIST0 [ + i = auto_fixed_param -> i,"" + | i = auto_fixed_param ; SYMBOL "="; v = [ v = int -> string_of_int v | v = IDENT -> v ] -> i,v ]; - tl = OPT [ "by"; tl = LIST1 tactic_term -> tl] -> + tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> (match tl with Some l -> l | None -> []), 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] ; + [ 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] ; "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 -> - BYC_wehaveand (id1,t1,id2,t2) + IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; + id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2) + | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> + BYC_wehaveand (id1,t1,id2,t2) ] ]; rewriting_step_continuation : [ @@ -439,13 +496,13 @@ EXTEND GrafiteAst.Check (loc, t) | [ IDENT "inline"]; style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; - suri = QSTRING; prefix = OPT QSTRING -> + suri = QSTRING; prefix = OPT QSTRING -> let style = match style with - | None -> GrafiteAst.Declarative - | Some depth -> GrafiteAst.Procedural depth - in - let prefix = match prefix with None -> "" | Some prefix -> prefix in - GrafiteAst.Inline (loc,style,suri,prefix) + | None -> GrafiteAst.Declarative + | Some depth -> GrafiteAst.Procedural depth + in + let prefix = match prefix with None -> "" | Some prefix -> prefix in + GrafiteAst.Inline (loc,style,suri,prefix) | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true) | IDENT "auto"; params = auto_params -> @@ -587,35 +644,10 @@ EXTEND Ast.Theorem (flavour, name, Ast.Implicit, Some body)) | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) - | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = CicNotationParser.let_defs -> - (* In case of mutual definitions here we produce just - the syntax tree for the first one. The others will be - generated from the completely specified term just before - insertion in the environment. We use the flavour - `MutualDefinition to rememer this. *) - let name,ty = - match defs with - | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ -> - let ty = - List.fold_right - (fun var ty -> Ast.Binder (`Pi,var,ty) - ) params ty - in - name,ty - | (_,(Ast.Ident (name, None), None),_,_) :: _ -> - name, Ast.Implicit - | _ -> assert false - in - let body = Ast.Ident (name,None) in - let flavour = - if List.length defs = 1 then - `Definition - else - `MutualDefinition - in - GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty, - Some (Ast.LetRec (ind_kind, defs, body)))) + | LETCOREC ; defs = CicNotationParser.let_defs -> + mk_rec_corec `CoInductive defs loc + | LETREC ; defs = CicNotationParser.let_defs -> + mk_rec_corec `Inductive defs loc | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) @@ -639,11 +671,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" ; "by" ; + refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ; refl = tactic_term -> refl ] ; - sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; "by" ; + sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ; sym = tactic_term -> sym ] ; - trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; "by" ; + trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ; trans = tactic_term -> trans ] ; "as" ; id = IDENT -> GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) @@ -681,7 +713,7 @@ EXTEND fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> - let _root, buri, fullpath, _rrelpath = + let _root, buri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in let status = @@ -689,7 +721,7 @@ EXTEND else LexiconEngine.eval_command status (LexiconAst.Include (iloc,buri,mode,fullpath)) in - !out fname; + !out fname; status, LSome (GrafiteAst.Executable @@ -697,7 +729,7 @@ EXTEND (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> - let status = LexiconEngine.eval_command status scom in + let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file ] diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index b9c0779c7..15fdbf725 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -23,6 +23,14 @@ * http://cs.unibo.it/helm/. *) +type just = [ `Term of Cic.term | `Auto of Auto.auto_params ] + +let mk_just ~dbd ~universe = + function + `Auto params -> Tactics.auto ~dbd ~params ~universe + | `Term t -> Tactics.apply t +;; + let assume id t = Tacticals.then_ ~start: @@ -45,12 +53,8 @@ let suppose t id ty = (fun _ metasenv ugraph -> ty,metasenv,ugraph)) ;; -let by_term_we_proved ~dbd ~universe t ty id ty' = - let just = - match t with - | None -> Tactics.auto ~dbd ~params:([],[]) ~universe - | Some t -> Tactics.apply t - in +let by_just_we_proved ~dbd ~universe just ty id ty' = + let just = mk_just ~dbd ~universe just in match id with None -> (match ty' with @@ -83,13 +87,8 @@ let by_term_we_proved ~dbd ~universe t ty id ty' = ~continuations:[ Tacticals.id_tac ; continuation ] ;; -let bydone ~dbd ~universe t = - let just = - match t with - | None -> Tactics.auto ~dbd ~params:([],[]) ~universe - | Some t -> Tactics.apply t - in - just +let bydone ~dbd ~universe just = + mk_just ~dbd ~universe just ;; let we_need_to_prove t id ty = @@ -127,7 +126,7 @@ let we_need_to_prove t id ty = ProofEngineTypes.mk_tactic aux ;; -let existselim ~dbd ~universe t id1 t1 id2 t2 = +let existselim ~dbd ~universe just id1 t1 id2 t2 = let aux (proof, goal) = let (n,metasenv,_subst,bo,ty,attrs) = proof in let metano,context,_ = CicUtil.lookup_meta goal metasenv in @@ -143,21 +142,24 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 = 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) + (mk_just ~dbd ~universe just) ]) (proof', goal) in ProofEngineTypes.mk_tactic aux ;; -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 andelim ~dbd ~universe just id1 t1 id2 t2 = + 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 ~universe just) ] +;; let rewritingstep ~dbd ~universe lhs rhs just last_step = let aux ((proof,goal) as status) = diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli index 08852c79c..987663e15 100644 --- a/helm/software/components/tactics/declarative.mli +++ b/helm/software/components/tactics/declarative.mli @@ -23,16 +23,19 @@ * http://cs.unibo.it/helm/. *) +type just = [ `Term of Cic.term | `Auto of Auto.auto_params ] + val assume : string -> Cic.term -> ProofEngineTypes.tactic val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic -val by_term_we_proved : - dbd:HSql.dbd -> universe:Universe.universe -> Cic.term option -> Cic.term -> - string option -> Cic.term option -> ProofEngineTypes.tactic +val by_just_we_proved : + dbd:HSql.dbd -> universe:Universe.universe -> + just -> Cic.term -> string option -> Cic.term option -> + ProofEngineTypes.tactic -val bydone : dbd:HSql.dbd -> universe:Universe.universe -> Cic.term option -> - ProofEngineTypes.tactic +val bydone : dbd:HSql.dbd -> universe:Universe.universe -> + just -> ProofEngineTypes.tactic val we_need_to_prove : Cic.term -> string option -> Cic.term option -> ProofEngineTypes.tactic @@ -48,11 +51,12 @@ val thesisbecomes : Cic.term -> ProofEngineTypes.tactic val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic val existselim : - dbd:HSql.dbd -> universe:Universe.universe -> - Cic.term option -> string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic + dbd:HSql.dbd -> universe:Universe.universe -> just -> + string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic val andelim : - Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic + dbd:HSql.dbd -> universe:Universe.universe -> just -> + string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic val rewritingstep : dbd:HSql.dbd -> universe:Universe.universe -> diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma index 917cbe2bc..893c4f1fd 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSeries". - include "CoRN.ma". (* $Id: FunctSeries.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *) diff --git a/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma b/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma index fcefda244..53c8bf9cf 100644 --- a/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma +++ b/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma @@ -34,7 +34,7 @@ lemma l1: monotone_not_increasing alpha. assume n:nat. we need to prove (alpha (S n) ≤ alpha n) or equivalently (Rdiv (alpha n) (S (S O)) ≤ alpha n). - by _ done. + done. qed. lemma l2: inf_bounded alpha. @@ -54,12 +54,12 @@ lemma l2: inf_bounded alpha. (* approssimiamo con questo *) we need to prove (R0 ≤ alpha O) or equivalently (R0 ≤ R1). - by _ done. + done. case S (m:nat). by induction hypothesis we know (R0 ≤ alpha m) (H). we need to prove (R0 ≤ alpha (S m)) or equivalently (R0 ≤ Rdiv (alpha m) (S (S O))). - by _ done. + done. qed. axiom xxx': @@ -68,15 +68,16 @@ axiom xxx': punto_fisso F l. theorem dimostrazione: tends_to alpha O. - by _ let l:R such that (tends_to alpha l) (H). + let l:R such that (tends_to alpha l) (H). (* unfold alpha in H. change in match alpha in H with (successione F O). check(xxx' F cont l H).*) - by (lim_punto_fisso F R1 cont l H) we proved (punto_fisso F l) (H2) +(* end auto($Revision: 8612 $) proof: TIME=0.01 SIZE=100 DEPTH=100 *) + using (lim_punto_fisso F R1 cont l H) we proved (punto_fisso F l) (H2) that is equivalent to (l = (Rdiv l (S (S O)))). - by _ we proved (tends_to alpha l = tends_to alpha O) (H4). + we proved (tends_to alpha l = tends_to alpha O) (H4). rewrite < H4. - by _ done. + done. qed. (******************************************************************************) @@ -95,15 +96,15 @@ lemma uno: ∀n. alpha2 n ≥ R1. alias num (instance 0) = "natural number". we need to prove (alpha2 0 ≥ R1) or equivalently ((S (S O)) ≥ R1). - by _ done. + done. case S (m:nat). by induction hypothesis we know (alpha2 m ≥ R1) (H). we need to prove (alpha2 (S m) ≥ R1) or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n); - by _ we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1). - by _ we proved (R1 · R1 = R1) (H2). + we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1). + we proved (R1 · R1 = R1) (H2). rewrite < H2. - by _ done. + done. qed. lemma mono1: monotone_not_decreasing alpha2. @@ -112,7 +113,7 @@ lemma mono1: monotone_not_decreasing alpha2. assume n:nat. we need to prove (alpha2 n ≤ alpha2 (S n)) or equivalently (alpha2 n ≤ Rmult (alpha2 n) (alpha2 n)). - by _ done. + done. qed. (* diff --git a/helm/software/matita/contribs/dama/dama_didactic/reals.ma b/helm/software/matita/contribs/dama/dama_didactic/reals.ma index 7d8a068c8..3328c0e96 100644 --- a/helm/software/matita/contribs/dama/dama_didactic/reals.ma +++ b/helm/software/matita/contribs/dama/dama_didactic/reals.ma @@ -90,8 +90,8 @@ axiom Relev_le: ∀x,y:R. lemma stupido: ∀x:R.R0+x=x. assume x:R. - conclude (R0+x) = (x+R0) by _. - = x by _ + conclude (R0+x) = (x+R0). + = x done. qed. diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 592e583e4..6f247d04a 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -737,7 +737,7 @@ ::= [&simpleautoparam;]… [by - &term;, [&term;]…] + &term; [,&term;]…] @@ -780,6 +780,13 @@ Try to close the goal performing unit-equality paramodulation + + + | + timeout=&nat; + Timeout in seconds + + diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index fd58c9564..590c5c07e 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -256,7 +256,6 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n). elim n 0. case O. the thesis becomes (D[x \sup 0] = 0·x \sup (pred 0)). - by _ done. case S (m:nat). by induction hypothesis we know @@ -265,24 +264,24 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n). (D[x \sup (1+m)] = (1+m) · x \sup m). we need to prove (m · (x \sup (1+ pred m)) = m · x \sup m) (Ppred). - by _ we proved (0 < m ∨ 0=m) (cases). + we proved (0 < m ∨ 0=m) (cases). we proceed by induction on cases to prove (m · (x \sup (1+ pred m)) = m · x \sup m). case left. suppose (0 < m) (m_pos). - by (S_pred m m_pos) we proved (m = 1 + pred m) (H1). - by _ + using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1). done. case right. - suppose (0=m) (m_zero). by _ done. + suppose (0=m) (m_zero). + done. conclude (D[x \sup (1+m)]) = (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 + x · (m · x \sup (pred m))) timeout=30. = (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 + = ((1+m) · x \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum done. qed. @@ -310,7 +309,6 @@ theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n. (D[x \sup (1+n)] = (1+n) · x \sup n).*) elim n 0. case O. the thesis becomes (D[x \sup 1] = 1 · x \sup 0). - by _ done. case S (m:nat). by induction hypothesis we know @@ -323,7 +321,7 @@ theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n. = (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)). - = ((2+m) · x \sup (1+m)) by Fmult_one_f Fmult_commutative - Fmult_Fplus_distr assoc_plus plus_n_SO costante_sum + = ((2+m) · x \sup (1+m)) timeout=30 by Fmult_one_f, Fmult_commutative, + Fmult_Fplus_distr, assoc_plus, plus_n_SO, costante_sum done. -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 3ba6499a9..98612ab2b 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -428,9 +428,10 @@ class gui () = ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png")) ~name:"Matita" ~version:BuildTimeConf.version - ~website:"http://helm.cs.unibo.it" + ~website:"http://matita.cs.unibo.it" () in + ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ())); connect_menu_item main#contentsMenuItem (fun () -> let cmd = sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma index 569a2f8ff..3e1bdd374 100644 --- a/helm/software/matita/tests/decl.ma +++ b/helm/software/matita/tests/decl.ma @@ -22,8 +22,8 @@ theorem easy: ∀n,m. n * m = O → n = O ∨ m = O. assume m: nat. (* base case *) by (refl_eq ? O) we proved (O = O) (trivial). - by (or_introl ? ? trivial) we proved (O = O ∨ m = O) (trivial2). - by (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case). + by or_introl we proved (O = O ∨ m = O) (trivial2). + using (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case). (* inductive case *) we need to prove (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O) @@ -31,8 +31,8 @@ theorem easy: ∀n,m. n * m = O → n = O ∨ m = O. assume n1: nat. suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp). (* base case *) - by (or_intror ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2). - by (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2). + by or_intror we proved (S n1 = O ∨ O = O) (pre_base_case2). + using (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2). (* inductive case *) we need to prove (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) → @@ -41,15 +41,15 @@ theorem easy: ∀n,m. n * m = O → n = O ∨ m = O. suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless). suppose (S n1 * S m1 = O) (absurd_hyp). simplify in absurd_hyp. - by (sym_eq ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp'). - by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd). + by sym_eq we proved (O = S (m1+n1*S m1)) (absurd_hyp'). + by not_eq_O_S we proved False (the_absurd). by (False_ind ? the_absurd) done. (* the induction *) - by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m) + using (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m) done. (* the induction *) - by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n) + using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n) done. qed. @@ -76,9 +76,9 @@ theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O. assume n: nat. assume m: nat. (* base case *) - by _ we proved (O = O) (trivial). - by _ we proved (O = O ∨ m = O) (trivial2). - by _ we proved (O*m=O → O=O ∨ m=O) (base_case). + we proved (O = O) (trivial). + we proved (O = O ∨ m = O) (trivial2). + we proved (O*m=O → O=O ∨ m=O) (base_case). (* inductive case *) we need to prove (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O) @@ -86,8 +86,8 @@ theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O. assume n1: nat. suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp). (* base case *) - by _ we proved (S n1 = O ∨ O = O) (pre_base_case2). - by _ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2). + we proved (S n1 = O ∨ O = O) (pre_base_case2). + we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2). (* inductive case *) we need to prove (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) → @@ -96,17 +96,14 @@ theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O. suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless). suppose (S n1 * S m1 = O) (absurd_hyp). simplify in absurd_hyp. - by _ we proved (O = S (m1+n1*S m1)) (absurd_hyp'). - (* BUG: automation failure *) - by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd). - (* BUG: automation failure *) - by (False_ind ? the_absurd) - done. + we proved (O = S (m1+n1*S m1)) (absurd_hyp'). + we proved False (the_absurd). + we proceed by cases on the_absurd to prove (S n1=O ∨ S m1=O). (* the induction *) - by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m) + using (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m) done. (* the induction *) - by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n) + using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n) done. qed. @@ -150,7 +147,7 @@ assume n: nat. we proceed by induction on n to prove False. case O. the thesis becomes (O*O=O). - by (refl_eq ? O) done. + done. case S (m:nat). by induction hypothesis we know (m*O=O) (I). the thesis becomes (S m * O = O).