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
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"
--- /dev/null
+(* aritmetic operators *)
+
+interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
+interpretation "Coq's real plus" 'plus x y = (cic:/Coq/Reals/Rdefinitions/Rplus.con x y).
+interpretation "Coq's binary integer plus" 'plus x y = (cic:/Coq/ZArith/BinInt/Zplus.con x y).
+interpretation "Coq's binary positive plus" 'plus x y = (cic:/Coq/NArith/BinPos/Pplus.con x y).
+interpretation "Coq's natural minus" 'minus x y = (cic:/Coq/Init/Peano/minus.con x y).
+interpretation "Coq's real minus" 'minus x y = (cic:/Coq/Reals/Rdefinitions/Rminus.con x y).
+interpretation "Coq's binary integer minus" 'minus x y = (cic:/Coq/ZArith/BinInt/Zminus.con x y).
+interpretation "Coq's binary positive minus" 'minus x y = (cic:/Coq/NArith/BinPos/Pminus.con x y).
+interpretation "Coq's natural times" 'times x y = (cic:/Coq/Init/Peano/mult.con x y).
+interpretation "Coq's real times" 'times x y = (cic:/Coq/Reals/Rdefinitions/Rmult.con x y).
+interpretation "Coq's binary positive times" 'times x y = (cic:/Coq/NArith/BinPos/Pmult.con x y).
+interpretation "Coq's binary integer times" 'times x y = (cic:/Coq/ZArith/BinInt/Zmult.con x y).
+interpretation "Coq's real power" 'power x y = (cic:/Coq/Reals/Rfunctions/pow.con x y).
+interpretation "Coq's integer power" 'power x y = (cic:/Coq/ZArith/Zpower/Zpower.con x y).
+interpretation "Coq's real divide" 'divide x y = (cic:/Coq/Reals/Rdefinitions/Rdiv.con x y).
+interpretation "Coq's real unary minus" 'uminus x = (cic:/Coq/Reals/Rdefinitions/Ropp.con x).
+interpretation "Coq's binary integer negative sign" 'uminus x = (cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/3) x).
+interpretation "Coq's binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/Zopp.con x).
+
+(* logical operators *)
+
+interpretation "Coq's logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y).
+interpretation "Coq's logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y).
+interpretation "Coq's logical not" 'not x = (cic:/Coq/Init/Logic/not.con x).
+interpretation "Coq's exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y).
+
+(* relational operators *)
+
+interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
+interpretation "Coq's real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
+interpretation "Coq's natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
+interpretation "Coq's real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).
+interpretation "Coq's natural 'less than'" 'lt x y = (cic:/Coq/Init/Peano/lt.con x y).
+interpretation "Coq's real 'less than'" 'lt x y = (cic:/Coq/Reals/Rdefinitions/Rlt.con x y).
+interpretation "Coq's natural 'greater than'" 'gt x y = (cic:/Coq/Init/Peano/gt.con x y).
+interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinitions/Rgt.con x y).
+
+interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
+interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
+
+++ /dev/null
-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).
-interpretation "Coq's real plus" 'plus x y = (cic:/Coq/Reals/Rdefinitions/Rplus.con x y).
-interpretation "Coq's binary integer plus" 'plus x y = (cic:/Coq/ZArith/BinInt/Zplus.con x y).
-interpretation "Coq's binary positive plus" 'plus x y = (cic:/Coq/NArith/BinPos/Pplus.con x y).
-interpretation "Coq's natural minus" 'minus x y = (cic:/Coq/Init/Peano/minus.con x y).
-interpretation "Coq's real minus" 'minus x y = (cic:/Coq/Reals/Rdefinitions/Rminus.con x y).
-interpretation "Coq's binary integer minus" 'minus x y = (cic:/Coq/ZArith/BinInt/Zminus.con x y).
-interpretation "Coq's binary positive minus" 'minus x y = (cic:/Coq/NArith/BinPos/Pminus.con x y).
-interpretation "Coq's natural times" 'times x y = (cic:/Coq/Init/Peano/mult.con x y).
-interpretation "Coq's real times" 'times x y = (cic:/Coq/Reals/Rdefinitions/Rmult.con x y).
-interpretation "Coq's binary positive times" 'times x y = (cic:/Coq/NArith/BinPos/Pmult.con x y).
-interpretation "Coq's binary integer times" 'times x y = (cic:/Coq/ZArith/BinInt/Zmult.con x y).
-interpretation "Coq's real power" 'power x y = (cic:/Coq/Reals/Rfunctions/pow.con x y).
-interpretation "Coq's integer power" 'power x y = (cic:/Coq/ZArith/Zpower/Zpower.con x y).
-interpretation "Coq's real divide" 'divide x y = (cic:/Coq/Reals/Rdefinitions/Rdiv.con x y).
-interpretation "Coq's real unary minus" 'uminus x = (cic:/Coq/Reals/Rdefinitions/Ropp.con x).
-interpretation "Coq's binary integer negative sign" 'uminus x = (cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/3) x).
-interpretation "Coq's binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/Zopp.con x).
-
-(* logical operators *)
-
-interpretation "Coq's logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y).
-interpretation "Coq's logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y).
-interpretation "Coq's logical not" 'not x = (cic:/Coq/Init/Logic/not.con x).
-interpretation "Coq's exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y).
-
-(* relational operators *)
-
-interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
-interpretation "Coq's real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
-interpretation "Coq's natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
-interpretation "Coq's real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).
-interpretation "Coq's natural 'less than'" 'lt x y = (cic:/Coq/Init/Peano/lt.con x y).
-interpretation "Coq's real 'less than'" 'lt x y = (cic:/Coq/Reals/Rdefinitions/Rlt.con x y).
-interpretation "Coq's natural 'greater than'" 'gt x y = (cic:/Coq/Init/Peano/gt.con x y).
-interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinitions/Rgt.con x y).
-
-interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
-interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
-
--- /dev/null
+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 }.
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))));
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 =
| `String of string
]
-let reloadable = function
- | `About `Current_proof
- | `Dir _ ->
- true
- | _ -> false
-
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));
(* 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 ()
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
(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;
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
| [] -> []
(_, 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 ->
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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.
+(**************************************************************************)
+(* ___ *)
+(* ||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)".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
+(**************************************************************************)
+(* ___ *)
+(* ||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)".
+(**************************************************************************)
+(* ___ *)
+(* ||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/".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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.
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
+(**************************************************************************)
+(* ___ *)
+(* ||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
-(****************************************************************************)
-(* ___ *)
-(* ||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
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
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".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
set "baseuri" "cic:/matita/tests/elim".
+include "coq.ma".
inductive stupidtype: Set \def
| Base : stupidtype
+(**************************************************************************)
+(* ___ *)
+(* ||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)".
].
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
| 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).
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.
*)
+(**************************************************************************)
+(* ___ *)
+(* ||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
+(**************************************************************************)
+(* ___ *)
+(* ||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)".
+(**************************************************************************)
+(* ___ *)
+(* ||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".
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
(**************************************************************************)
set "baseuri" "cic:/matita/generalize".
+include "coq.ma".
alias num (instance 0) = "natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+(**************************************************************************)
+(* ___ *)
+(* ||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
+(**************************************************************************)
+(* ___ *)
+(* ||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/".
+(**************************************************************************)
+(* ___ *)
+(* ||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
+(**************************************************************************)
+(* ___ *)
+(* ||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.
-
-
(**************************************************************************)
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".
+(**************************************************************************)
+(* ___ *)
+(* ||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 {}.
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+(**************************************************************************)
+(* ___ *)
+(* ||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)".
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+(**************************************************************************)
+(* ___ *)
+(* ||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
+(**************************************************************************)
+(* ___ *)
+(* ||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)".
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.
unfold myplus.
rewrite > lem.
reflexivity.
-qed.
\ No newline at end of file
+qed.
projects / helm.git / commitdiff