From 54e651eaa3cbcc16cfdf3fcc8b53482bffc78b76 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 1 Dec 2008 18:09:10 +0000 Subject: [PATCH] 0.5.6 almost ok --- helm/software/Makefile | 2 - helm/software/matita/dist/ChangeLog | 8 + helm/software/matita/dist/INSTALL | 196 ------------------ helm/software/matita/dist/Makefile | 7 +- helm/software/matita/dist/README | 53 ----- .../didactic/exercises/natural_deduction.ma | 18 +- .../exercises/natural_deduction_fst_order.ma | 104 +++++++++- 7 files changed, 122 insertions(+), 266 deletions(-) delete mode 100644 helm/software/matita/dist/INSTALL delete mode 100644 helm/software/matita/dist/README diff --git a/helm/software/Makefile b/helm/software/Makefile index ce51f175b..aa73b1647 100644 --- a/helm/software/Makefile +++ b/helm/software/Makefile @@ -63,8 +63,6 @@ EXTRA_DIST = \ matita/dist/BUGS \ matita/dist/ChangeLog \ matita/dist/COPYING \ - matita/dist/INSTALL \ - matita/dist/README \ Makefile \ Makefile.defs.in \ $(NULL) diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index f03ee5e9e..110e101a7 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,3 +1,11 @@ +0.5.6 - 1/12/2008 - bugfix release + * more abstract disambiguation algorithm, simpler instantiation + to a different CIC/refiner + * natural deduction support improved in the first order case + * natural deduction lem rule does now support lemmas + with (up to) 3 premises (multicut rule, displayed as + a collapsed tree) + 0.5.5 - 17/11/2008 - bugfix release with students in mind * by ... we proved fixed to use only the specified lemmas but using full unification inside auto. diff --git a/helm/software/matita/dist/INSTALL b/helm/software/matita/dist/INSTALL deleted file mode 100644 index 2a1533815..000000000 --- a/helm/software/matita/dist/INSTALL +++ /dev/null @@ -1,196 +0,0 @@ - -Tiny Matita logoMatita Home - - Chapter 2. Installation -Prev     Next - -━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ - -Chapter 2. Installation - -Table of Contents - -Installing from sources - - Getting the source code - Requirements - (optional) MySQL setup - Compiling and installing - -Configuring Matita - -Installing from sources - -Currently, the only intended way to install Matita is starting from its source -code. - -Getting the source code - -You can get the Matita source code in two ways: - - 1. go to the download page and get the latest released source tarball; - - 2. get the development sources from our SVN repository. You will need the - components/ and matita/ directories from the trunk/helm/software/ - directory, plus the configure and Makefile* stuff from the same directory. - - In this case you will need to run autoconf before proceding with the - building instructions below. - -Requirements - -In order to build Matita from sources you will need some tools and libraries. -They are listed below. - -Note for Debian (and derivatives) users - -If you are running a Debian GNU/Linux distribution, or any of its derivative -like Ubuntu, you can use APT to install all the required tools and libraries -since they are all part of the Debian archive. - -apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev liblablgtk2-ocaml-dev -liblablgtkmathview-ocaml-dev liblablgtksourceview-ocaml-dev -libsqlite3-ocaml-dev libocamlnet-ocaml-dev libzip-ocaml-dev libhttp-ocaml-dev -ocaml-ulex08 libexpat-ocaml-dev libmysql-ocaml-dev camlp5 - -An official debian package is going to be added to the archive too. - -Required tools and libraries - -OCaml - - the Objective Caml compiler, version 3.09 or above - -Findlib - - OCaml package manager, version 1.1.1 or above - -OCaml Expat - - OCaml bindings for the expat library - -GMetaDOM - - OCaml bindings for the Gdome 2 library - -OCaml HTTP - - OCaml library to write HTTP daemons (and clients) - -LablGTK - - OCaml bindings for the GTK+ library , version 2.6.0 or above - -GtkMathView , LablGtkMathView - - GTK+ widget to render MathML documents and its OCaml bindings - -GtkSourceView , LablGtkSourceView - - extension for the GTK+ text widget (adding the typical features of source - code editors) and its OCaml bindings - -MySQL , OCaml MySQL - - SQL database and OCaml bindings for its client-side library - - The SQL database itself is not strictly needed to run Matita, but the - client libraries are. - -Sqlite , OCaml Sqlite3 - - Sqlite database and OCaml bindings - -Ocamlnet - - collection of OCaml libraries to deal with application-level Internet - protocols and conventions - -ulex - - Unicode lexer generator for OCaml - -CamlZip - - OCaml library to access .gz files - -(optional) MySQL setup - -To fully exploit Matita indexing and search capabilities on a huge metadata set -you may need a working MySQL database. Detalied instructions on how to do it -can be found in the MySQL documentation. Here you can find a quick howto. - -In order to create a database you need administrator permissions on your MySQL -installation, usually the root account has them. Once you have the permissions, -a new database can be created executing mysqladmin create matita (matita is the -default database name, you can change it using the db.user key of the -configuration file). - -Then you need to grant the necessary access permissions to the database user of -Matita, typing echo "grant all privileges on matita.* to helm;" | mysql matita -should do the trick (helm is the default user name used by Matita to access the -database, you can change it using the db.user key of the configuration file). - -Note - -This way you create a database named matita on which anyone claiming to be the -helm user can do everything (like adding dummy data or destroying the contained -one). It is strongly suggested to apply more fine grained permissions, how to -do it is out of the scope of this manual. - -Compiling and installing - -Once you get the source code the installations steps should be quite familiar. - -First of all you need to configure the build process executing ./configure. -This will check that all needed tools and library are installed and prepare the -sources for compilation and installation. - -Quite a few (optional) arguments may be passed to the configure command line to -change build time parameters. They are listed below, together with their -default values: - -configure command line arguments - ---with-runtime-dir=dir - - (Default: /usr/local/matita) Runtime base directory where all Matita stuff - (executables, configuration files, standard library, ...) will be installed - ---with-dbhost=host - - (Default: localhost) Default SQL server hostname. Will be used while - building the standard library during the installation and to create the - default Matita configuration. May be changed later in configuration file. - ---enable-debug - - (Default: disabled) Enable debugging code. Not for the casual user. - -Then you will manage the build and install process using make as usual. Below -are reported the targets you have to invoke in sequence to build and install: - -make targets - -world - - builds components needed by Matita and Matita itself (in bytecode or native - code depending on the availability of the OCaml native code compiler) - -install - - installs Matita related tools, standard library and the needed runtime - stuff in the proper places on the filesystem. - - As a part of the installation process the Matita standard library will be - compiled, thus testing that the just built matitac compiler works properly. - - For this step you will need a working SQL database (for indexing the - standard library while you are compiling it). See Database setup for - instructions on how to set it up. - -━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ - -Prev     Next -Matita vs Coq  Home  Configuring Matita - diff --git a/helm/software/matita/dist/Makefile b/helm/software/matita/dist/Makefile index 33aeac735..c7b9de92b 100644 --- a/helm/software/matita/dist/Makefile +++ b/helm/software/matita/dist/Makefile @@ -19,9 +19,4 @@ matita_stdlib.sql: %.gz: % gzip -c $< > $@ -dist_pre: INSTALL README -INSTALL: $(MANUAL_DIR)/txt-stamp - cp $(MANUAL_DIR)/sec_install.txt $@ -$(MANUAL_DIR)/txt-stamp: - $(MAKE) -C $(MANUAL_DIR) txt-stamp - +dist_pre: diff --git a/helm/software/matita/dist/README b/helm/software/matita/dist/README deleted file mode 100644 index a27350d32..000000000 --- a/helm/software/matita/dist/README +++ /dev/null @@ -1,53 +0,0 @@ - -MATITA ------- - -Matita is a new document-centric interactive theorem prover that integrates -several Mathematical Knowledge Management tools and techniques. - -Matita is traditional. Its logical foundation is the Calculus of (Co)Inductive -Constructions (CIC). It can re-use mathematical concepts produced by other -proof assistants like Coq and encoded in an XML encoding of CIC. The -interaction paradigm of Matita is familiar, being inspired by CtCoq and Proof -General. Its proof language is procedural in the same spirit of LCF. - -Matita is innovative: - -- the user interface sports high quality bidimensional rendering of proofs and - formulae transformed on-the-fly to MathML markup, on which direct - manipulation of the underlying CIC terms is still possible; - -- the knowledge base is distributed: every authored concepts can be published - becoming part of the Matita library which can be browsed as an hypertext - (locally or on the World Wide Web) and searched by means of content-based - queries; - -- the tactical language, part of the proof language, has step-by-step - semantics, enabling inspection and replaying of deeply structured proof - scripts. - -More information are available on the Matita web site: - - http://matita.cs.unibo.it/ - - -INSTALLATION ------------- - -See the file INSTALL for building and installation instructions. - - -BUGS ----- - -Bugs reporting is handled using the Bugzilla bug tracker available at: - - http://bugs.mowgli.cs.unibo.it/ - - -LICENSE -------- - -Matita and its documentation are free software. -See the file COPYING for copying conditions. - diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index 3a5bca154..078c7fb00 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma @@ -124,14 +124,16 @@ far seguire le parentesi quadre come spiegato in precedenza. Si noti che "regola" `lem` non è una vera regola, ma una forma compatta per rappresentare l'albero di prova del lemma che si sta riutilizzando. -Per motivi che saranno più chiari una volta studiate logiche del primo ordine -o di ordine superiore, i lemmi che si intende riutilizzare è bene -che siano dimostrati astratti sugli atomi, ovvero per ogni -atomo `A`...`Z` che compare nella formula, è bene aggiungere -una quantificazione all'inizio della formula stessa (es. `∀A:CProp.`) -e iniziare la dimostrazione con il comando `assume`. In tale -modo il lemma EM può essere utilizzato sia per dimostrare -`A ∨ ¬A` sia `B ∨ ¬B` sia `(A∨C) ∨ ¬(A∨C)` ... +Per motivi che saranno più chiari una volta studiate logiche del +primo ordine o di ordine superiore, i lemmi che si intende +riutilizzare è bene che siano dimostrati astratti sugli atomi. +Ovvero per ogni atomo `A`...`Z` che compare nella formula, +è bene aggiungere una quantificazione all'inizio della formula stessa. +Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`. +La dimostrazione deve poi iniziare con il comando `assume`. + +In tale modo il lemma EM può essere utilizzato sia per dimostrare +`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ... DOCEND*) diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma index 9022b8d03..9a865597b 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma @@ -46,6 +46,86 @@ I termini, le formule e i nomi delle ipotesi * I nomi delle ipotesi, quando argomenti di una regola, vengono scritti tra `[` e `]`. +Le regole di deduzione naturale +=============================== + +Per digitare le regole di deduzione naturale +è possibile utilizzare la palette che compare +sulla sinistra dopo aver premuto `F2`. + +L'albero si descrive partendo dalla radice. Le regole +con premesse multiple sono seguite da `[`, `|` e `]`. +Ad esempio: + + apply rule (∧_i (A∨B) ⊥); + [ …continua qui il sottoalbero per (A∨B) + | …continua qui il sottoalbero per ⊥ + ] + +Le regole vengono applicate alle loro premesse, ovvero +gli argomenti delle regole sono le formule che normalmente +scrivete sopra la linea che rappresenta l'applicazione della +regola stessa. Ad esempio: + + aply rule (∨_e (A∨B) [h1] C [h2] C); + [ …prova di (A∨B) + | …prova di C sotto l'ipotesi A (di nome h1) + | …prova di C sotto l'ipotesi B (di nome h2) + ] + +Le regole che hanno una sola premessa non vengono seguite +da parentesi quadre. + +L'albero di deduzione +===================== + +Per visualizzare l'albero man mano che viene costruito +dai comandi impartiti al sistema, premere `F3` e poi +premere sul bottome home (in genere contraddistinto da +una icona rappresentate una casa). + +Si suggerisce di marcare tale finestra come `always on top` +utilizzando il menu a tendina che nella maggior parte degli +ambienti grafici si apre cliccando nel suo angolo in +alto a sinistra. + +Applicazioni di regole errate vengono contrassegnate con +il colore rosso. + +Usare i lemmi dimostrati in precedenza +====================================== + +Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile +riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`. + +La "regola" `lem` prende come argomenti: + +- Il numero delle ipotesi del lemma che si vuole utilizzare, nel + caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`. + +- Dopo il numero di ipotesi, è necessario digitare il nome del lemma. + +- Infine, le formule che devono essere scritte come premesse per la + "regola". + +Ad esempio, per usare il lemma EM (terzo escluso) basta digitare +`lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare +`lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario +far seguire le parentesi quadre come spiegato in precedenza. + +Si noti che "regola" `lem` non è una vera regola, ma una forma compatta +per rappresentare l'albero di prova del lemma che si sta riutilizzando. + +Per motivi che saranno più chiari una volta studiate logiche del +primo ordine o di ordine superiore, i lemmi che si intende +riutilizzare è bene che siano dimostrati astratti sugli atomi. +Ovvero per ogni atomo `A`...`Z` che compare nella formula, +è bene aggiungere una quantificazione all'inizio della formula stessa. +Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`. +La dimostrazione deve poi iniziare con il comando `assume`. + +In tale modo il lemma EM può essere utilizzato sia per dimostrare +`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ... DOCEND*) @@ -67,7 +147,29 @@ axiom R : sort →sort → CProp. axiom S : sort →sort → CProp. (* assumiamo il terzo escluso *) -axiom EM : ∀A:CProp.A ∨ ¬A. +theorem EM: ∀A:CProp. A ∨ ¬ A. +assume A: CProp. +apply rule (prove (A ∨ ¬A)); +apply rule (RAA [H] (⊥)). +apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A)); + [ apply rule (discharge [H]). + | apply rule (⊥_e (⊥)); + apply rule (¬_e (¬¬A) (¬A)); + [ apply rule (¬_i [K] (⊥)). + apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A)); + [ apply rule (discharge [H]). + | apply rule (∨_i_r (¬A)). + apply rule (discharge [K]). + ] + | apply rule (¬_i [K] (⊥)). + apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A)); + [ apply rule (discharge [H]). + | apply rule (∨_i_l (A)). + apply rule (discharge [K]). + ] + ] + ] +qed. (* intuizionista *) lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x. -- 2.39.2