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.
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*
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
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
| _ -> failwith "Invalid index name."
]
];
- induction_kind: [
- [ "rec" -> `Inductive
- | "corec" -> `CoInductive
- ]
- ];
let_defs: [
[ defs = LIST1 [
name = single_arg;
[ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
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 *)
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
(* 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
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
(* 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 -> " "
(* 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) ->
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
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)
=
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' =
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
| 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
| 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
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
| 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" ->
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<def>> ; t = tactic_term ->
(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
(* 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 : [
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 ->
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))
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)
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 =
else LexiconEngine.eval_command status
(LexiconAst.Include (iloc,buri,mode,fullpath))
in
- !out fname;
+ !out fname;
status,
LSome
(GrafiteAst.Executable
(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
]
* 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:
(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
~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 =
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
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) =
* 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
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 ->
(* 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 $ *)
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.
(* 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':
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.
(******************************************************************************)
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.
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.
(*
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.
<entry>::=</entry>
<entry>[&simpleautoparam;]…
[<emphasis role="bold">by</emphasis>
- &term;, [&term;]…]
+ &term; [,&term;]…]
</entry>
</row>
</tbody>
<entry>Try to close the goal performing unit-equality paramodulation
</entry>
</row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">timeout=&nat;</emphasis></entry>
+ <entry>Timeout in seconds
+ </entry>
+ </row>
</tbody>
</tgroup>
</table>
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
(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.
(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
= (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.
~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
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)
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) →
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.
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)
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) →
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.
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).
projects / helm.git / commitdiff