From 650e3b3c9ff0b9cafb76a0edf8139a53446937ba Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 29 Jul 2005 08:10:41 +0000 Subject: [PATCH] 0. core_notation.ma splitted into coq.moo and core_notation.moo 1. 'include "coq.ma"' is now explicitly required to activate the notation of Coq 2. 'include "coq.ma"' added here and there in the tests 3. .ma headers updated --- helm/matita/buildTimeConf.ml.in | 3 +- helm/matita/{core_notation.ma => coq.moo} | 76 ----------------------- helm/matita/core_notation.moo | 75 ++++++++++++++++++++++ helm/matita/matita.ml | 1 + helm/matita/matitaEngine.ml | 24 +++---- helm/matita/matitaMathView.ml | 19 +++--- helm/matita/matitaMisc.ml | 5 +- helm/matita/matitadep.ml | 15 ++--- helm/matita/tests/absurd.ma | 5 +- helm/matita/tests/apply.ma | 15 +++++ helm/matita/tests/assumption.ma | 3 +- helm/matita/tests/auto.ma | 15 +++++ helm/matita/tests/baseuri.ma | 14 +++++ helm/matita/tests/change.ma | 3 +- helm/matita/tests/clear.ma | 5 +- helm/matita/tests/clearbody.ma | 3 +- helm/matita/tests/coercions.ma | 15 +++++ helm/matita/tests/comments.ma | 27 ++++---- helm/matita/tests/constructor.ma | 3 +- helm/matita/tests/contradiction.ma | 3 +- helm/matita/tests/cut.ma | 3 +- helm/matita/tests/decompose.ma | 3 +- helm/matita/tests/discriminate.ma | 3 +- helm/matita/tests/elim.ma | 3 +- helm/matita/tests/fguidi.ma | 43 ++++++++----- helm/matita/tests/first.ma | 14 +++++ helm/matita/tests/fix_betareduction.ma | 14 +++++ helm/matita/tests/fold.ma | 15 +++++ helm/matita/tests/generalize.ma | 3 +- helm/matita/tests/inversion.ma | 15 +++++ helm/matita/tests/letrec.ma | 14 +++++ helm/matita/tests/match_inference.ma | 14 +++++ helm/matita/tests/mysql_escaping.ma | 16 ++++- helm/matita/tests/paramodulation.ma | 1 + helm/matita/tests/record.ma | 14 +++++ helm/matita/tests/replace.ma | 15 +++++ helm/matita/tests/rewrite.ma | 15 +++++ helm/matita/tests/second.ma | 14 +++++ helm/matita/tests/simpl.ma | 15 +++++ helm/matita/tests/test2.ma | 15 +++++ helm/matita/tests/test3.ma | 15 +++++ helm/matita/tests/test4.ma | 15 +++++ helm/matita/tests/third.ma | 14 +++++ helm/matita/tests/unfold.ma | 4 +- 44 files changed, 471 insertions(+), 155 deletions(-) rename helm/matita/{core_notation.ma => coq.moo} (64%) create mode 100644 helm/matita/core_notation.moo diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 5ceabc66f..d8daa1fd7 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -40,7 +40,8 @@ let images_dir = runtime_base_dir ^ "/icons" let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc" let lang_file = runtime_base_dir ^ "/matita.lang" let script_template = runtime_base_dir ^ "/matita.ma.templ" -let core_notation_script = runtime_base_dir ^ "/core_notation.ma" +let core_notation_script = runtime_base_dir ^ "/core_notation.moo" +let coq_notation_script = runtime_base_dir ^ "/coq.moo" let matita_conf = runtime_base_dir ^ "/matita.conf.xml" let gtkmathview_conf = runtime_base_dir ^ "/gtkmathview.matita.conf.xml" diff --git a/helm/matita/core_notation.ma b/helm/matita/coq.moo similarity index 64% rename from helm/matita/core_notation.ma rename to helm/matita/coq.moo index 91e205fe1..4c3d8f772 100644 --- a/helm/matita/core_notation.ma +++ b/helm/matita/coq.moo @@ -1,79 +1,3 @@ -notation "hvbox(a break \to b)" - right associative with precedence 20 -for @{ \forall $_:$a.$b }. - -notation < "hvbox(a break \to b)" - right associative with precedence 20 -for @{ \Pi $_:$a.$b }. - -notation "hvbox(a break = b)" - non associative with precedence 45 -for @{ 'eq $a $b }. - -notation "hvbox(a break \leq b)" - non associative with precedence 45 -for @{ 'leq $a $b }. - -notation "hvbox(a break \geq b)" - non associative with precedence 45 -for @{ 'geq $a $b }. - -notation "hvbox(a break \lt b)" - non associative with precedence 45 -for @{ 'lt $a $b }. - -notation "hvbox(a break \gt b)" - non associative with precedence 45 -for @{ 'gt $a $b }. - -notation "hvbox(a break \neq b)" - non associative with precedence 45 -for @{ 'neq $a $b }. - -notation "hvbox(a break + b)" - left associative with precedence 50 -for @{ 'plus $a $b }. - -notation "hvbox(a break - b)" - left associative with precedence 50 -for @{ 'minus $a $b }. - -notation "hvbox(a break * b)" - left associative with precedence 55 -for @{ 'times $a $b }. - -notation "hvbox(a break / b)" - left associative with precedence 55 -for @{ 'divide $a $b }. - -notation "\frac a b" - non associative with precedence 90 -for @{ 'divide $a $b }. - -notation "a \over b" - left associative with precedence 55 -for @{ 'divide $a $b }. - -notation "- a" - non associative with precedence 60 -for @{ 'uminus $a }. - -notation "\sqrt a" - non associative with precedence 60 -for @{ 'sqrt $a }. - -notation "hvbox(a break \lor b)" - left associative with precedence 30 -for @{ 'or $a $b }. - -notation "hvbox(a break \land b)" - left associative with precedence 35 -for @{ 'and $a $b }. - -notation "hvbox(\lnot a)" - left associative with precedence 40 -for @{ 'not $a }. - (* aritmetic operators *) interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y). diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo new file mode 100644 index 000000000..5b3759cb0 --- /dev/null +++ b/helm/matita/core_notation.moo @@ -0,0 +1,75 @@ +notation "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \forall $_:$a.$b }. + +notation < "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \Pi $_:$a.$b }. + +notation "hvbox(a break = b)" + non associative with precedence 45 +for @{ 'eq $a $b }. + +notation "hvbox(a break \leq b)" + non associative with precedence 45 +for @{ 'leq $a $b }. + +notation "hvbox(a break \geq b)" + non associative with precedence 45 +for @{ 'geq $a $b }. + +notation "hvbox(a break \lt b)" + non associative with precedence 45 +for @{ 'lt $a $b }. + +notation "hvbox(a break \gt b)" + non associative with precedence 45 +for @{ 'gt $a $b }. + +notation "hvbox(a break \neq b)" + non associative with precedence 45 +for @{ 'neq $a $b }. + +notation "hvbox(a break + b)" + left associative with precedence 50 +for @{ 'plus $a $b }. + +notation "hvbox(a break - b)" + left associative with precedence 50 +for @{ 'minus $a $b }. + +notation "hvbox(a break * b)" + left associative with precedence 55 +for @{ 'times $a $b }. + +notation "hvbox(a break / b)" + left associative with precedence 55 +for @{ 'divide $a $b }. + +notation "\frac a b" + non associative with precedence 90 +for @{ 'divide $a $b }. + +notation "a \over b" + left associative with precedence 55 +for @{ 'divide $a $b }. + +notation "- a" + non associative with precedence 60 +for @{ 'uminus $a }. + +notation "\sqrt a" + non associative with precedence 60 +for @{ 'sqrt $a }. + +notation "hvbox(a break \lor b)" + left associative with precedence 30 +for @{ 'or $a $b }. + +notation "hvbox(a break \land b)" + left associative with precedence 35 +for @{ 'and $a $b }. + +notation "hvbox(\lnot a)" + left associative with precedence 40 +for @{ 'not $a }. diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 72dff8058..0066d1c18 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -82,6 +82,7 @@ let script = let _ = let cic_math_view = MatitaMathView.cicMathView_instance () in let sequents_viewer = MatitaMathView.sequentsViewer_instance () in + sequents_viewer#load_logo; cic_math_view#set_href_callback (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri)))); diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index f32978063..24872ffd0 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -518,17 +518,19 @@ let disambiguate_command status = function status, GrafiteAst.Obj (loc,obj) let make_absolute paths path = - let rec aux = function - | [] -> ignore (Unix.stat path); path - | p :: tl -> - let path = p ^ "/" ^ path in - try - ignore (Unix.stat path); path - with Unix.Unix_error _ -> aux tl - in - try - aux paths - with Unix.Unix_error _ as exc -> raise (UnableToInclude path) + if path = "coq.ma" then path + else + let rec aux = function + | [] -> ignore (Unix.stat path); path + | p :: tl -> + let path = p ^ "/" ^ path in + try + ignore (Unix.stat path); path + with Unix.Unix_error _ -> aux tl + in + try + aux paths + with Unix.Unix_error _ as exc -> raise (UnableToInclude path) ;; let eval_command opts status cmd = diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 13035b02b..481b8fd6c 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -519,12 +519,6 @@ type term_source = | `String of string ] -let reloadable = function - | `About `Current_proof - | `Dir _ -> - true - | _ -> false - class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = @@ -605,7 +599,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> self#load (`About `Current_proof)))); ignore (win#browserRefreshButton#connect#clicked - (handle_error' self#refresh)); + (handle_error' (self#refresh ~force:true))); ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); ignore (win#browserForwardButton#connect#clicked (handle_error' self#forward)); @@ -685,9 +679,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (* loads a uri which can be a cic uri or an about:* uri * @param uri string *) - method private _load entry = + method private _load ?(force=false) entry = try - if entry <> current_entry || reloadable entry then begin + if entry <> current_entry || entry = `About `Current_proof || force then + begin (match entry with | `About `Current_proof -> self#home () | `About `Blank -> self#blank () @@ -808,8 +803,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method win = win method history = history method currentEntry = current_entry - method refresh () = - if reloadable current_entry then self#_load current_entry + method refresh ~force () = self#_load ~force current_entry end @@ -864,7 +858,8 @@ let mathViewer () = (self#get_browser reuse)#load entry end -let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers +let refresh_all_browsers () = + List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers let update_font_sizes () = List.iter (fun b -> b#updateFontSize) !cicBrowsers; diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index ca8dc2446..e3aadd5b5 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -291,8 +291,9 @@ let obj_file_of_baseuri baseuri = path ^ ".moo" let obj_file_of_script f = - let baseuri = baseuri_of_file f in - obj_file_of_baseuri baseuri + if f = "coq.ma" then BuildTimeConf.coq_notation_script else + let baseuri = baseuri_of_file f in + obj_file_of_baseuri baseuri let rec list_uniq = function | [] -> [] diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index e355ab59c..0676aa93e 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -95,13 +95,14 @@ let main () = (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> Hashtbl.add aliases file uri | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> - (try - Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path)) - with - Sys_error _ -> - MatitaLog.error - ("In file " ^ file ^ " unable to include " ^ path) - ) + if path <> "coq.ma" then + (try + Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path)) + with + Sys_error _ -> + MatitaLog.error + ("In file " ^ file ^ " unable to include " ^ path) + ) | _ -> () with CicNotationParser.Parse_error _ as exn -> diff --git a/helm/matita/tests/absurd.ma b/helm/matita/tests/absurd.ma index 24d2d885f..19c738d05 100644 --- a/helm/matita/tests/absurd.ma +++ b/helm/matita/tests/absurd.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,12 +13,11 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/absurd/". +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "not" = "cic:/Coq/Init/Logic/not.con". - - theorem stupid : \forall a:Prop. a \to not a \to 0 = 1. intros. absurd a. diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma index 41bdd3afc..35a788ac6 100644 --- a/helm/matita/tests/apply.ma +++ b/helm/matita/tests/apply.ma @@ -1,5 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + (* test _with_ the WHD on the apply argument *) set "baseuri" "cic:/matita/tests/apply/". +include "coq.ma". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". diff --git a/helm/matita/tests/assumption.ma b/helm/matita/tests/assumption.ma index 4679ea1c3..fde8f8c98 100644 --- a/helm/matita/tests/assumption.ma +++ b/helm/matita/tests/assumption.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/assumption". +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma index e7e59554c..5c6c04358 100755 --- a/helm/matita/tests/auto.ma +++ b/helm/matita/tests/auto.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/auto/". +include "coq.ma". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". diff --git a/helm/matita/tests/baseuri.ma b/helm/matita/tests/baseuri.ma index eb4ae6a68..0e06223fa 100644 --- a/helm/matita/tests/baseuri.ma +++ b/helm/matita/tests/baseuri.ma @@ -1,2 +1,16 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/baseuri/". set "baseuri" "cic:/matita/tests/baseuri/". diff --git a/helm/matita/tests/change.ma b/helm/matita/tests/change.ma index 199ce3bd8..2c5daf0d2 100644 --- a/helm/matita/tests/change.ma +++ b/helm/matita/tests/change.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/change/". +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/helm/matita/tests/clear.ma b/helm/matita/tests/clear.ma index 24bb3377c..71457ae2c 100644 --- a/helm/matita/tests/clear.ma +++ b/helm/matita/tests/clear.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,12 +13,11 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/clear". +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". - - theorem stupid: \forall a: True. \forall b: 0 = 0. diff --git a/helm/matita/tests/clearbody.ma b/helm/matita/tests/clearbody.ma index 9a125e687..0956cbc1e 100644 --- a/helm/matita/tests/clearbody.ma +++ b/helm/matita/tests/clearbody.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/clearbody". +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index 5c157368d..663656e05 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/coercions/". +include "coq.ma". inductive pos: Set \def | one : pos diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma index e9caa7edc..f9412f45a 100644 --- a/helm/matita/tests/comments.ma +++ b/helm/matita/tests/comments.ma @@ -1,18 +1,19 @@ -(****************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| A.Asperti, C.Sacerdoti Coen, *) -(* ||A|| E.Tassi, S.Zacchiroli *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(****************************************************************************) +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) set "baseuri" "cic:/matita/tests/comments/". +include "coq.ma". (* commento che va nell'ast, ma non viene contato come step perche' non e' un executable diff --git a/helm/matita/tests/constructor.ma b/helm/matita/tests/constructor.ma index 0cd22d35b..3ee7f4b98 100644 --- a/helm/matita/tests/constructor.ma +++ b/helm/matita/tests/constructor.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/constructor". +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/contradiction.ma b/helm/matita/tests/contradiction.ma index e4519ec3e..886bc8c80 100644 --- a/helm/matita/tests/contradiction.ma +++ b/helm/matita/tests/contradiction.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/contradiction". +include "coq.ma". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma index f5850e576..e20db6f5d 100644 --- a/helm/matita/tests/cut.ma +++ b/helm/matita/tests/cut.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/cut". +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/decompose.ma b/helm/matita/tests/decompose.ma index 0b5ef7a80..caf2d5289 100644 --- a/helm/matita/tests/decompose.ma +++ b/helm/matita/tests/decompose.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/decompose". +include "coq.ma". alias symbol "and" (instance 0) = "Coq's logical and". alias symbol "or" (instance 0) = "Coq's logical or". diff --git a/helm/matita/tests/discriminate.ma b/helm/matita/tests/discriminate.ma index f94624567..6cfcea0bb 100644 --- a/helm/matita/tests/discriminate.ma +++ b/helm/matita/tests/discriminate.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/discriminate". +include "coq.ma". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma index ab7afafa6..fcc130e9e 100644 --- a/helm/matita/tests/elim.ma +++ b/helm/matita/tests/elim.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/elim". +include "coq.ma". inductive stupidtype: Set \def | Base : stupidtype diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 07e7989ce..e72e28e5c 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/fguidi/". +include "coq.ma". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". @@ -27,20 +42,20 @@ definition pred: nat \to nat \def ]. theorem eq_gen_S_O: \forall x. (S x = O) \to \forall P:Prop. P. -intros. apply False_ind. cut (is_S O). auto. elim H. exact I. +intros. apply False_ind. cut (is_S O). auto paramodulation. elim H. exact I. qed. theorem eq_gen_S_O_cc: (\forall P:Prop. P) \to \forall x. (S x = O). -intros. auto. +intros. auto. (* paramodulation non trova la prova *) qed. theorem eq_gen_S_S: \forall m,n. (S m) = (S n) \to m = n. intros. cut (pred (S m)) = (pred (S n)). -assumption. elim H. auto. +assumption. elim H. auto. (* bug paramodulation *) qed. theorem eq_gen_S_S_cc: \forall m,n. m = n \to (S m) = (S n). -intros. elim H. auto. +intros. elim H. auto. (* bug paramodulation *) qed. inductive le: nat \to nat \to Prop \def @@ -48,37 +63,37 @@ inductive le: nat \to nat \to Prop \def | le_succ: \forall m, n. (le m n) \to (le (S m) (S n)). theorem le_refl: \forall x. (le x x). -intros. elim x. auto. auto. +intros. elim x. auto paramodulation. auto paramodulation. qed. theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to (x = O). -intros 3. elim H. auto. apply eq_gen_S_O. exact n1. auto. +intros 3. elim H. auto paramodulation. apply eq_gen_S_O. exact n1. auto paramodulation. qed. theorem le_gen_x_O: \forall x. (le x O) \to (x = O). -intros. apply le_gen_x_O_aux. exact O. auto. auto. +intros. apply le_gen_x_O_aux. exact O. auto paramodulation. auto. (* bug paramodulation *) qed. theorem le_gen_x_O_cc: \forall x. (x = O) \to (le x O). -intros. elim H. auto. +intros. elim H. auto paramodulation. qed. theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to (\exists n. x = (S n) \land (le m n)). intros 4. elim H. -apply eq_gen_S_O. exact m. elim H1. auto. -cut n = m. elim Hcut. apply ex_intro. exact n1. auto. auto. +apply eq_gen_S_O. exact m. elim H1. auto. (* bug paramodulation *) +cut n = m. elim Hcut. apply ex_intro. exact n1. auto paramodulation. auto. (* paramodulation non trova la prova *) qed. theorem le_gen_S_x: \forall m,x. (le (S m) x) \to (\exists n. x = (S n) \land (le m n)). -intros. apply le_gen_S_x_aux. exact (S m). auto. auto. +intros. apply le_gen_S_x_aux. exact (S m). auto paramodulation. auto. (* bug paramodulation *) qed. theorem le_gen_S_x_cc: \forall m,x. (\exists n. x = (S n) \land (le m n)) \to (le (S m) x). -intros. elim H. elim H1. cut (S x1) = x. elim Hcut. auto. elim H2. auto. +intros. elim H. elim H1. cut (S x1) = x. elim Hcut. auto paramodulation. elim H2. auto. (* bug paramodulation *) qed. theorem le_gen_S_S: \forall m,n. (le (S m) (S n)) \to (le m n). @@ -88,12 +103,12 @@ lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption. qed. theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)). -intros. auto. +intros. auto paramodulation. qed. (* theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z). intros 1. elim x; clear H. clear x. -auto. +auto paramodulation. fwd H1 [H]. decompose H. *) diff --git a/helm/matita/tests/first.ma b/helm/matita/tests/first.ma index 69b4adf26..6120d93c4 100644 --- a/helm/matita/tests/first.ma +++ b/helm/matita/tests/first.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/first/". inductive nat : Set \def diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma index b4ea8d8b5..82f0b1cf6 100644 --- a/helm/matita/tests/fix_betareduction.ma +++ b/helm/matita/tests/fix_betareduction.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/fix_betareduction/". alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". diff --git a/helm/matita/tests/fold.ma b/helm/matita/tests/fold.ma index 7b91c5b24..003d45f47 100644 --- a/helm/matita/tests/fold.ma +++ b/helm/matita/tests/fold.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/fold". +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/generalize.ma b/helm/matita/tests/generalize.ma index 4fe9af340..ee0732225 100644 --- a/helm/matita/tests/generalize.ma +++ b/helm/matita/tests/generalize.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/generalize". +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma index 99e18012d..4f8c4c6d4 100644 --- a/helm/matita/tests/inversion.ma +++ b/helm/matita/tests/inversion.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/inversion/". +include "coq.ma". inductive nat : Set \def O : nat diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma index e8e81fa01..55933cd31 100644 --- a/helm/matita/tests/letrec.ma +++ b/helm/matita/tests/letrec.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/letrec/". diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma index afb2513ee..0e27ce409 100644 --- a/helm/matita/tests/match_inference.ma +++ b/helm/matita/tests/match_inference.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/match_inference/". inductive pos: Set \def diff --git a/helm/matita/tests/mysql_escaping.ma b/helm/matita/tests/mysql_escaping.ma index e1698abd2..bd0eb8d5a 100644 --- a/helm/matita/tests/mysql_escaping.ma +++ b/helm/matita/tests/mysql_escaping.ma @@ -1,5 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/mysql_escaping/". theorem a' : Prop \to Prop.intros.assumption.qed. - - diff --git a/helm/matita/tests/paramodulation.ma b/helm/matita/tests/paramodulation.ma index 80a39fa3f..d918fb451 100644 --- a/helm/matita/tests/paramodulation.ma +++ b/helm/matita/tests/paramodulation.ma @@ -13,6 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/paramodulation". +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma index 02ef85a05..ed9ecfed8 100644 --- a/helm/matita/tests/record.ma +++ b/helm/matita/tests/record.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/record/". record empty : Type \def {}. diff --git a/helm/matita/tests/replace.ma b/helm/matita/tests/replace.ma index d70a7af60..6d62e41d1 100644 --- a/helm/matita/tests/replace.ma +++ b/helm/matita/tests/replace.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/replace/". +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index 71a7514fa..ebb54f126 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/rewrite/". +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/second.ma b/helm/matita/tests/second.ma index ef13fc18c..450c67671 100644 --- a/helm/matita/tests/second.ma +++ b/helm/matita/tests/second.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/second/". alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)". alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)". diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma index 61d5b1163..dbc4e9c06 100644 --- a/helm/matita/tests/simpl.ma +++ b/helm/matita/tests/simpl.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/simpl/". +include "coq.ma". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma index 1adf17326..0ffdb8268 100644 --- a/helm/matita/tests/test2.ma +++ b/helm/matita/tests/test2.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/test2/". +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias symbol "and" (instance 0) = "Coq's logical and". diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma index 561bd6564..6b05351e6 100644 --- a/helm/matita/tests/test3.ma +++ b/helm/matita/tests/test3.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/test3/". +include "coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:\forall x.x=x. diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma index 8d8cac4e3..d680378eb 100644 --- a/helm/matita/tests/test4.ma +++ b/helm/matita/tests/test4.ma @@ -1,4 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/test4/". +include "coq.ma". (* commento che va nell'ast, ma non viene contato diff --git a/helm/matita/tests/third.ma b/helm/matita/tests/third.ma index e0ae453b4..124cdc121 100644 --- a/helm/matita/tests/third.ma +++ b/helm/matita/tests/third.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/tests/third/". alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)". alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)". diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma index c91ff1863..28ffcf3f2 100644 --- a/helm/matita/tests/unfold.ma +++ b/helm/matita/tests/unfold.ma @@ -14,6 +14,8 @@ set "baseuri" "cic:/matita/unfold". +include "coq.ma". + alias symbol "plus" (instance 0) = "Coq's natural plus". definition myplus \def \lambda x,y. x+y. @@ -27,4 +29,4 @@ theorem trivial: \forall n. S (myplus n n) = myplus (S n) n. unfold myplus. rewrite > lem. reflexivity. -qed. \ No newline at end of file +qed. -- 2.39.2