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
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
| 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
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 =
|| 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
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 =
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
(* 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
| 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
| 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
| 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 ]
(* 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 *)
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
| 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
| 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) ->
| 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 " "
| 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)
| 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)
| `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)
=
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 *)
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
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
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
| 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 ->
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
| 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;
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
| 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 ->
]
];
rewriting_step_continuation : [
- [ IDENT "done" -> true
+ [ "done" -> true
| -> false
]
];
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)
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
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
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
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
| 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 =
(* 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) *)
(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
~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;;
* 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 *
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
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
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
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
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
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
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
-(* 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 ->
?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 ->
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
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:
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,
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.
(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.
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
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.
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).
projects / helm.git / commitdiff