From 8ae1653eb75d2b57c50e077c49cb9d078313ea9d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 5 Jun 2009 22:18:01 +0000 Subject: [PATCH] - Procedural convertible rewrites in the conclusion are now detected and replaced by change - grafiteAst: semantics of the Include flag changed: now true means normal include, New Inline flags Coercions, Comments (activated) Debug (not yet) - library: eq_plus_Zplus moved from Z/times to Z/plus now Z/plus.ma Z/times.ma are fully reconstructed :) --- .../acic_procedural/acic2Procedural.ml | 8 +++-- .../components/acic_procedural/procedural2.ml | 29 +++++++++++----- .../acic_procedural/proceduralConversion.ml | 4 +++ .../acic_procedural/proceduralConversion.mli | 2 ++ .../acic_procedural/proceduralHelpers.ml | 4 +-- .../acic_procedural/proceduralHelpers.mli | 2 +- .../acic_procedural/proceduralOptimizer.ml | 2 +- .../binaries/transcript/.depend.opt | 5 --- .../components/binaries/transcript/engine.ml | 33 +++++++++++-------- .../binaries/transcript/gallina8Parser.mly | 6 ++-- .../components/binaries/transcript/grafite.ml | 6 ++-- .../software/components/grafite/grafiteAst.ml | 17 ++++++---- .../components/grafite/grafiteAstPp.ml | 13 +++++--- .../grafite_parser/dependenciesParser.ml | 2 +- .../grafite_parser/grafiteParser.ml | 19 ++++++----- .../components/ng_paramodulation/.depend | 6 ++-- .../components/ng_paramodulation/.depend.opt | 20 ++++++++--- .../components/tptp_grafite/tptp2grafite.ml | 2 +- helm/software/matita/applyTransformation.ml | 12 ++++++- .../procedural/library/library.conf.xml | 1 + helm/software/matita/library/Z/plus.ma | 12 ++++++- helm/software/matita/library/Z/times.ma | 10 ------ helm/software/matita/matita.lang | 5 +++ helm/software/matita/matitacLib.ml | 2 +- 24 files changed, 141 insertions(+), 81 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 4ce01707c..68c88496b 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -63,8 +63,12 @@ let proc_obj ?(info="") proc_proof sorts params context = function | flavour when List.mem flavour th_flavours -> let ast = proc_proof v in let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in - let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s" - "COMMENTS" info "Tactics" steps "Final nodes" nodes "END" + let text = + if List.mem G.IPComments params then + Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s" + "COMMENTS" info "Tactics" steps "Final nodes" nodes "END" + else + "" in T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text] | flavour when List.mem flavour def_flavours -> diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 06fc9b358..826cfb986 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -26,6 +26,7 @@ module C = Cic module I = CicInspect module S = CicSubstitution +module R = CicReduction module TC = CicTypeChecker module Un = CicUniv module UM = UriManager @@ -57,7 +58,7 @@ type status = { case : int list } -let debug = ref true +let debug = ref false (* helpers ******************************************************************) @@ -186,6 +187,11 @@ let is_reflexivity st step = | None -> false | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 +let are_convertible st pred sx dx = + let pred, sx, dx = H.cic pred, H.cic sx, H.cic dx in + let sx, dx = C.Appl [pred; sx], C.Appl [pred; dx] in + fst (R.are_convertible st.context sx dx Un.default_ugraph) + (* proof construction *******************************************************) let anonymous_premise = C.Name "UNNAMED" @@ -227,7 +233,7 @@ let mk_convert st ?name sty ety note = note sname (ppterm csty) (ppterm cety) else "" in - if H.alpha_equivalence ~flatten:true st.context csty cety then [T.Note note] else + if H.alpha ~flatten:true st.context csty cety then [T.Note note] else let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in match name with | None -> [T.Change (sty, ety, None, e, note)] @@ -294,11 +300,18 @@ let mk_rewrite st dtext where qs tl direction t ity = let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a in assert (List.length tl = 5); - let predicate = List.nth tl 2 in - let dtext = if !debug then dtext ^ ppterm (H.cic predicate) else dtext in - let e = Cn.mk_pattern 1 ity predicate in + let pred, sx, dx = List.nth tl 2, List.nth tl 1, List.nth tl 4 in + let dtext = if !debug then dtext ^ ppterm (H.cic pred) else dtext in + let e = Cn.mk_pattern 1 ity pred in let script = [T.Branch (qs, "")] in - if (Cn.does_not_occur e) then script else + if Cn.does_not_occur e then script else + if are_convertible st pred sx dx then + let dtext = "convertible rewrite" ^ dtext in + let ity, ety, e = Cn.beta sx pred, Cn.beta dx pred, Cn.hole "" in + let city, cety = H.cic ity, H.cic ety in + if H.alpha ~flatten:true st.context city cety then script else + T.Change (ity, ety, None, e, dtext) :: script + else T.Rewrite (direction, where, None, e, dtext) :: script let rec proc_lambda st what name v t = @@ -319,8 +332,8 @@ and proc_letin st what name v w t = let script = if proceed then let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with | Some (C.ALetIn (_, _, iv, iw, _), _), _ when - H.alpha_equivalence ~flatten:true st.context (H.cic v) (H.cic iv) && - H.alpha_equivalence ~flatten:true st.context (H.cic w) (H.cic iw) + H.alpha ~flatten:true st.context (H.cic v) (H.cic iv) && + H.alpha ~flatten:true st.context (H.cic w) (H.cic iw) -> st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)] | _, Some (ity, ety) -> diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 65d5f1edf..e73ccfe59 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -219,6 +219,10 @@ let convert g ity k predicate = let mk_pattern psno ity predicate = clear_absts (convert (generalize psno) ity) psno 0 predicate +let beta v = function + | C.ALambda (_, _, _, t) -> subst 1 v t + | _ -> assert false + let get_clears c p xtypes = let meta = C.Implicit None in let rec aux c names p it et = function diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli index 2e556511b..418d911a9 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.mli +++ b/helm/software/components/acic_procedural/proceduralConversion.mli @@ -33,6 +33,8 @@ val fake_annotate: Cic.id -> Cic.context -> Cic.term -> Cic.annterm val mk_pattern: int -> Cic.annterm -> Cic.annterm -> Cic.annterm +val beta: Cic.annterm -> Cic.annterm -> Cic.annterm + val get_clears: Cic.context -> Cic.term -> (Cic.term * Cic.term) option -> Cic.context * string list diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index c42fe7532..4305f9153 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -239,7 +239,7 @@ let flatten_appls = let sober ?(flatten=false) c t = if flatten then flatten_appls t else (assert (Ut.is_sober c t); t) -let alpha_equivalence ?flatten c t1 t2 = +let alpha ?flatten c t1 t2 = let t1 = sober ?flatten c t1 in let t2 = sober ?flatten c t2 in Ut.alpha_equivalence t1 t2 @@ -247,7 +247,7 @@ let alpha_equivalence ?flatten c t1 t2 = let occurs c ~what ~where = let result = ref false in let equality c t1 t2 = - let r = alpha_equivalence ~flatten:true c t1 t2 in + let r = alpha ~flatten:true c t1 t2 in result := !result || r; r in let context, what, with_what = c, [what], [C.Rel 0] in diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 03faf269b..c021c7c69 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -99,5 +99,5 @@ val is_acic_proof: (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm -> bool -val alpha_equivalence: +val alpha: ?flatten:bool -> Cic.context -> Cic.term -> Cic.term -> bool diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 2faade402..c5a27efc4 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -42,7 +42,7 @@ module Cl = ProceduralClassify (* debugging ****************************************************************) -let debug = ref true +let debug = ref false (* term optimization ********************************************************) diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 6776bb1f3..a51d3f0c2 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -179,8 +179,8 @@ let set_heading st name = let heading = st.heading_path, st.heading_lines in set_items st name [T.Heading heading] -let require st name src inc = - set_items st name [T.Include (src, inc)] +let require st name moo inc = + set_items st name [T.Include (moo, inc)] let get_coercion st str = try List.assoc str st.coercions with Not_found -> "" @@ -198,6 +198,8 @@ let make_script_name st script name = let get_iparams st name = let map = function | "nodefaults" -> GA.IPNoDefaults + | "coercions" -> GA.IPCoercions + | "comments" -> GA.IPComments | s -> failwith ("unknown inline parameter: " ^ s) in List.map map (X.list_assoc_all name st.iparams) @@ -233,14 +235,19 @@ let produce st = let obj, p = if b then Filename.concat (make_path path) obj, make_prefix path else obj, p - in - let s = obj ^ G.string_of_inline_kind k in - let full_s = Filename.concat in_base_uri s in - let params = params @ get_iparams st (Filename.concat name obj) in - path, Some (T.Inline (b, k, full_s, p, f, params)) - | T.Include (src, s) -> + in + let ext = G.string_of_inline_kind k in + let s = Filename.concat in_base_uri (obj ^ ext) in + let params = + params @ + get_iparams st "*" @ + get_iparams st ("*" ^ ext) @ + get_iparams st (Filename.concat name obj) + in + path, Some (T.Inline (b, k, s, p, f, params)) + | T.Include (moo, s) -> begin - try path, Some (T.Include (src, List.assoc s st.requires)) + try path, Some (T.Include (moo, List.assoc s st.requires)) with Not_found -> path, None end | T.Coercion (b, obj) -> @@ -258,7 +265,7 @@ let produce st = | item -> path, Some item in let set_includes st name = - try require st name false (List.assoc name st.includes) + try require st name true (List.assoc name st.includes) with Not_found -> () in let rec remove_lines ich n = @@ -279,8 +286,8 @@ let produce st = set_items st st.input_package (comment :: global_items); init name; begin match st.input_type with - | T.Grafite "" -> require st name true file - | _ -> require st name true st.input_package + | T.Grafite "" -> require st name false file + | _ -> require st name false st.input_package end; set_includes st name; set_items st name local_items; commit st name with e -> @@ -293,7 +300,7 @@ let produce st = List.iter (produce st) st.files | T.Grafite s -> let theory = Filename.concat st.input_path s in - require st st.input_package true theory; + require st st.input_package false theory; List.iter (produce st) st.files; commit st st.input_package | _ -> diff --git a/helm/software/components/binaries/transcript/gallina8Parser.mly b/helm/software/components/binaries/transcript/gallina8Parser.mly index b51a3d76e..e72dbbf30 100644 --- a/helm/software/components/binaries/transcript/gallina8Parser.mly +++ b/helm/software/components/binaries/transcript/gallina8Parser.mly @@ -332,11 +332,11 @@ | unx xskips FS { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } | req xp ident FS - { out "REQ" $3; [T.Include (false, trim $3)] } + { out "REQ" $3; [T.Include (true, trim $3)] } | req ident FS - { out "REQ" $2; [T.Include (false, trim $2)] } + { out "REQ" $2; [T.Include (true, trim $2)] } | load str FS - { out "REQ" $2; [T.Include (false, strip2 (trim $2))] } + { out "REQ" $2; [T.Include (true, strip2 (trim $2))] } | coerc qid spcs skips FS { out "COERCE" (hd $2); coercion (hd $2) } | id coerc qid spcs skips FS diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index 0037e6145..cae0bdfb5 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -75,8 +75,8 @@ let command_of_obj obj = let command_of_macro macro = G.Executable (floc, G.Macro (floc, macro)) -let require src value = - command_of_obj (G.Include (floc, src, value ^ ".ma")) +let require moo value = + command_of_obj (G.Include (floc, moo, value ^ ".ma")) let coercion value = command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0)) @@ -111,7 +111,7 @@ let commit kind och items = | T.Heading heading -> out_preamble och heading | T.Line line -> if !O.comments then out_line_comment och line - | T.Include (src, script) -> out_command och (require src script) + | T.Include (moo, script) -> out_command och (require moo script) | T.Coercion specs -> if !O.comments then out_unexported och "COERCION" (snd specs) | T.Notation specs -> diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 169873bf0..6b9a3eba1 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -148,12 +148,15 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] -type inline_param = IPPrefix of string - | IPAs of Cic.object_flavour - | IPProcedural - | IPNoDefaults - | IPLevel of int - | IPDepth of int +type inline_param = IPPrefix of string (* undocumented *) + | IPAs of Cic.object_flavour (* preferred flavour *) + | IPProcedural (* procedural rendering *) + | IPNoDefaults (* no default-based tactics *) + | IPLevel of int (* granularity level *) + | IPDepth of int (* undocumented *) + | IPComments (* show statistics *) + | IPCoercions (* show coercions *) + | IPDebug of int (* set debug level *) type ('term,'lazy_term) macro = (* Whelp's stuff *) @@ -185,7 +188,7 @@ type ('term,'obj) command = | UnificationHint of loc * 'term * int (* term, precedence *) | Default of loc * string * UriManager.uri list | Drop of loc - | Include of loc * bool (* source? *) * string + | Include of loc * bool (* normal? *) * string | Obj of loc * 'obj | Relation of loc * string * 'term * 'term * 'term option * 'term option * 'term option diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index a9a15568f..cdf90c5b9 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -281,11 +281,14 @@ let pp_macro ~term_pp ~lazy_term_pp = let pp_inline_params l = let pp_param = function | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\"" - | IPAs flavour -> flavour_pp flavour - | IPProcedural -> "procedural" - | IPNoDefaults -> "nodefaults" + | IPAs flavour -> flavour_pp flavour + | IPProcedural -> "procedural" + | IPNoDefaults -> "nodefaults" | IPDepth depth -> "depth = " ^ string_of_int depth | IPLevel level -> "level = " ^ string_of_int level + | IPComments -> "comments" + | IPCoercions -> "coercions" + | IPDebug debug -> "debug = " ^ string_of_int debug in let s = String.concat " " (List.map pp_param l) in if s = "" then s else " " ^ s @@ -342,8 +345,8 @@ let pp_command ~term_pp ~obj_pp = function "unification hint " ^ string_of_int n ^ " " ^ term_pp t | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" - | Include (_,false,path) -> "include \"" ^ path ^ "\"" - | Include (_,true,path) -> "include source \"" ^ path ^ "\"" + | Include (_,true,path) -> "include \"" ^ path ^ "\"" + | Include (_,false,path) -> "include source \"" ^ path ^ "\"" | Obj (_,obj) -> obj_pp obj | Qed _ -> "qed" | Relation (_,id,a,aeq,refl,sym,trans) -> diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml index 53fb7ab6d..923739924 100644 --- a/helm/software/components/grafite_parser/dependenciesParser.ml +++ b/helm/software/components/grafite_parser/dependenciesParser.ml @@ -56,7 +56,7 @@ let parse_dependencies lexbuf = true, (UriDep (UriManager.uri_of_string u) :: acc) | [< '("IDENT", "include"); '("QSTRING", fname) >] -> true, (IncludeDep fname :: acc) - | [< '("IDENT", "include"); '("IDENT", "source"); '("QSTRING", fname) >] -> + | [< '("IDENT", "include"); '("IDENT", "lexicon"); '("QSTRING", fname) >] -> true, (IncludeDep fname :: acc) | [< '("IDENT", "include'"); '("QSTRING", fname) >] -> true, (IncludeDep fname :: acc) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 222e85f09..06a753f88 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -466,6 +466,9 @@ EXTEND | IDENT "nodefaults" -> G.IPNoDefaults | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level + | IDENT "comments" -> G.IPComments + | IDENT "coercions" -> G.IPCoercions + | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug ] -> params ] ]; @@ -728,11 +731,11 @@ EXTEND include_command: [ [ IDENT "include" ; path = QSTRING -> - loc,path,false,L.WithPreferences + loc,path,true,L.WithPreferences | IDENT "include" ; IDENT "source" ; path = QSTRING -> - loc,path,true,L.WithPreferences + loc,path,false,L.WithPreferences | IDENT "include'" ; path = QSTRING -> - loc,path,false,L.WithoutPreferences + loc,path,true,L.WithoutPreferences ]]; grafite_command: [ [ @@ -892,22 +895,22 @@ EXTEND let stm = G.Comment (loc, com) in !grafite_callback status stm; status, LSome stm - | (iloc,fname,source,mode) = include_command ; SYMBOL "." -> + | (iloc,fname,normal,mode) = include_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> let stm = - G.Executable (loc, G.Command (loc, G.Include (iloc, source, fname))) + G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname))) in !grafite_callback status stm; let _root, buri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in - let stm = - G.Executable (loc, G.Command (loc, G.Include (iloc, source, buri))) - in let status = if never_include then raise (NoInclusionPerformed fullpath) else LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in + let stm = + G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri))) + in status, LSome stm | scom = lexicon_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 9cb1b46ee..0033d44db 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,22 +1,22 @@ pp.cmi: terms.cmi +fosubst.cmi: terms.cmi founif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi -fosubst.cmi: terms.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi +fosubst.cmo: terms.cmi fosubst.cmi +fosubst.cmx: terms.cmx fosubst.cmi founif.cmo: terms.cmi fosubst.cmi founif.cmi founif.cmx: terms.cmx fosubst.cmx founif.cmi index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi -fosubst.cmo: terms.cmi fosubst.cmi -fosubst.cmx: terms.cmx fosubst.cmi nCicBlob.cmo: terms.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 75490d3ba..0033d44db 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -1,15 +1,25 @@ -terms.cmi: pp.cmi: terms.cmi +fosubst.cmi: terms.cmi founif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi +nCicBlob.cmi: terms.cmi +cicBlob.cmi: terms.cmi terms.cmo: terms.cmi terms.cmx: terms.cmi -pp.cmo: pp.cmi -pp.cmx: pp.cmi -founif.cmo: founif.cmi -founif.cmx: founif.cmi +pp.cmo: terms.cmi pp.cmi +pp.cmx: terms.cmx pp.cmi +fosubst.cmo: terms.cmi fosubst.cmi +fosubst.cmx: terms.cmx fosubst.cmi +founif.cmo: terms.cmi fosubst.cmi founif.cmi +founif.cmx: terms.cmx fosubst.cmx founif.cmi index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi +nCicBlob.cmo: terms.cmi nCicBlob.cmi +nCicBlob.cmx: terms.cmx nCicBlob.cmi +cicBlob.cmo: terms.cmi cicBlob.cmi +cicBlob.cmx: terms.cmx cicBlob.cmi +paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi founif.cmi paramod.cmi +paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index e2a05e1c7..10ed2bc72 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -370,7 +370,7 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam match raw_preamble with | None -> pp (GA.Executable(floc, - GA.Command(floc,GA.Include(floc,false,"logic/equality.ma")))) + GA.Command(floc,GA.Include(floc,true,"logic/equality.ma")))) | Some s -> s buri in let extra_statements_end = [] in diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 91fe7bcd0..4015293a4 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -234,9 +234,13 @@ let txt_of_cic_object let aux = function | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm -> + let hc = !Acic2content.hide_coercions in + if List.mem G.IPCoercions params then + Acic2content.hide_coercions := false; enable_notations false; let str = stm_pp stm in enable_notations true; + Acic2content.hide_coercions := hc; str (* FG: we disable notation for Inductive to avoid recursive notation *) | G.Executable (_, G.Tactic _) as stm -> @@ -246,7 +250,13 @@ let txt_of_cic_object Acic2content.hide_coercions := hc; str (* FG: we show coercion because the reconstruction is not aware of them *) - | stm -> stm_pp stm + | stm -> + let hc = !Acic2content.hide_coercions in + if List.mem G.IPCoercions params then + Acic2content.hide_coercions := false; + let str = stm_pp stm in + Acic2content.hide_coercions := hc; + str in let script = Acic2Procedural.procedural_of_acic_object diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml index 2f7264fc7..51e8b568b 100644 --- a/helm/software/matita/contribs/procedural/library/library.conf.xml +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -16,5 +16,6 @@ logic/equality/eq_elim_r nodefaults logic/equality/eq_f nodefaults logic/equality/eq_f' nodefaults + Z/plus/eq_plus_Zplus nocoercions diff --git a/helm/software/matita/library/Z/plus.ma b/helm/software/matita/library/Z/plus.ma index 00da44a00..242be1b53 100644 --- a/helm/software/matita/library/Z/plus.ma +++ b/helm/software/matita/library/Z/plus.ma @@ -39,7 +39,17 @@ definition Zplus :Z \to Z \to Z \def | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ]. interpretation "integer plus" 'plus x y = (Zplus x y). - + +theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) = +Z_of_nat n + Z_of_nat m. +intro.cases n;intro + [reflexivity + |cases m + [simplify.rewrite < plus_n_O.reflexivity + |simplify.reflexivity. + ]] +qed. + theorem Zplus_z_OZ: \forall z:Z. z+OZ = z. intro.elim z. simplify.reflexivity. diff --git a/helm/software/matita/library/Z/times.ma b/helm/software/matita/library/Z/times.ma index 742ef5462..eefe4af7e 100644 --- a/helm/software/matita/library/Z/times.ma +++ b/helm/software/matita/library/Z/times.ma @@ -248,13 +248,3 @@ qed. variant distr_Ztimes_Zplus: \forall x,y,z. x * (y + z) = x*y + x*z \def distributive_Ztimes_Zplus. - -theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) = -Z_of_nat n + Z_of_nat m. -intro.cases n;intro - [reflexivity - |cases m - [simplify.rewrite < plus_n_O.reflexivity - |simplify.reflexivity. - ]] -qed. diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index 24e7eee28..ed1d5650b 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -49,6 +49,7 @@ rec record return + source to using with @@ -184,6 +185,10 @@ hint set auto + nodefaults + coercions + comments + debug () + | G.Executable (loc, G.Command (_, G.Include (_, false, _))) -> () | stm -> output_string och (pp_statement stm); nl (); nl () in -- 2.39.2