From 223f17d088cd8bf01f9314580fc34e66256841ac Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 10 Jun 2006 16:25:50 +0000 Subject: [PATCH] keeping the generated manual on svn is overkilling --- helm/www/matita/docs/manual/WrtCoq.html | 13 -- helm/www/matita/docs/manual/authoring.html | 62 -------- .../manual/axiom_definition_declaration.html | 39 ----- helm/www/matita/docs/manual/cicbrowser.html | 22 --- helm/www/matita/docs/manual/docbook.css | 51 ------- helm/www/matita/docs/manual/index.html | 9 -- helm/www/matita/docs/manual/proofs.html | 11 -- helm/www/matita/docs/manual/sec_commands.html | 5 - .../docs/manual/sec_gettingstarted.html | 16 -- helm/www/matita/docs/manual/sec_install.html | 137 ------------------ helm/www/matita/docs/manual/sec_intro.html | 7 - helm/www/matita/docs/manual/sec_license.html | 14 -- .../www/matita/docs/manual/sec_tacticals.html | 5 - helm/www/matita/docs/manual/sec_tactics.html | 7 - helm/www/matita/docs/manual/sec_terms.html | 56 ------- .../matita/docs/manual/sec_usernotation.html | 5 - helm/www/matita/docs/manual/tac_apply.html | 13 -- .../matita/docs/manual/tac_assumption.html | 6 - helm/www/matita/docs/manual/tac_auto.html | 12 -- helm/www/matita/docs/manual/tac_change.html | 10 -- helm/www/matita/docs/manual/tac_clear.html | 7 - .../www/matita/docs/manual/tac_clearbody.html | 7 - .../matita/docs/manual/tac_constructor.html | 10 -- .../matita/docs/manual/tac_contradiction.html | 7 - helm/www/matita/docs/manual/tac_cut.html | 9 -- .../www/matita/docs/manual/tac_decompose.html | 5 - .../matita/docs/manual/tac_discriminate.html | 7 - helm/www/matita/docs/manual/tac_elim.html | 15 -- helm/www/matita/docs/manual/tac_elimType.html | 5 - helm/www/matita/docs/manual/tac_exact.html | 6 - helm/www/matita/docs/manual/tac_exists.html | 9 -- helm/www/matita/docs/manual/tac_fail.html | 5 - helm/www/matita/docs/manual/tac_fold.html | 10 -- helm/www/matita/docs/manual/tac_fourier.html | 8 - helm/www/matita/docs/manual/tac_fwd.html | 5 - .../matita/docs/manual/tac_generalize.html | 14 -- helm/www/matita/docs/manual/tac_id.html | 5 - .../www/matita/docs/manual/tac_injection.html | 9 -- helm/www/matita/docs/manual/tac_intro.html | 11 -- helm/www/matita/docs/manual/tac_intros.html | 15 -- .../www/matita/docs/manual/tac_inversion.html | 13 -- helm/www/matita/docs/manual/tac_lapply.html | 5 - helm/www/matita/docs/manual/tac_left.html | 9 -- helm/www/matita/docs/manual/tac_letin.html | 6 - .../www/matita/docs/manual/tac_normalize.html | 6 - .../docs/manual/tac_paramodulation.html | 5 - helm/www/matita/docs/manual/tac_reduce.html | 6 - .../matita/docs/manual/tac_reflexivity.html | 7 - helm/www/matita/docs/manual/tac_replace.html | 10 -- helm/www/matita/docs/manual/tac_rewrite.html | 13 -- helm/www/matita/docs/manual/tac_right.html | 9 -- helm/www/matita/docs/manual/tac_ring.html | 9 -- helm/www/matita/docs/manual/tac_simplify.html | 6 - helm/www/matita/docs/manual/tac_split.html | 9 -- helm/www/matita/docs/manual/tac_symmetry.html | 6 - .../matita/docs/manual/tac_transitivity.html | 7 - helm/www/matita/docs/manual/tac_unfold.html | 10 -- helm/www/matita/docs/manual/tac_whd.html | 6 - 58 files changed, 811 deletions(-) delete mode 100644 helm/www/matita/docs/manual/WrtCoq.html delete mode 100644 helm/www/matita/docs/manual/authoring.html delete mode 100644 helm/www/matita/docs/manual/axiom_definition_declaration.html delete mode 100644 helm/www/matita/docs/manual/cicbrowser.html delete mode 100644 helm/www/matita/docs/manual/docbook.css delete mode 100644 helm/www/matita/docs/manual/index.html delete mode 100644 helm/www/matita/docs/manual/proofs.html delete mode 100644 helm/www/matita/docs/manual/sec_commands.html delete mode 100644 helm/www/matita/docs/manual/sec_gettingstarted.html delete mode 100644 helm/www/matita/docs/manual/sec_install.html delete mode 100644 helm/www/matita/docs/manual/sec_intro.html delete mode 100644 helm/www/matita/docs/manual/sec_license.html delete mode 100644 helm/www/matita/docs/manual/sec_tacticals.html delete mode 100644 helm/www/matita/docs/manual/sec_tactics.html delete mode 100644 helm/www/matita/docs/manual/sec_terms.html delete mode 100644 helm/www/matita/docs/manual/sec_usernotation.html delete mode 100644 helm/www/matita/docs/manual/tac_apply.html delete mode 100644 helm/www/matita/docs/manual/tac_assumption.html delete mode 100644 helm/www/matita/docs/manual/tac_auto.html delete mode 100644 helm/www/matita/docs/manual/tac_change.html delete mode 100644 helm/www/matita/docs/manual/tac_clear.html delete mode 100644 helm/www/matita/docs/manual/tac_clearbody.html delete mode 100644 helm/www/matita/docs/manual/tac_constructor.html delete mode 100644 helm/www/matita/docs/manual/tac_contradiction.html delete mode 100644 helm/www/matita/docs/manual/tac_cut.html delete mode 100644 helm/www/matita/docs/manual/tac_decompose.html delete mode 100644 helm/www/matita/docs/manual/tac_discriminate.html delete mode 100644 helm/www/matita/docs/manual/tac_elim.html delete mode 100644 helm/www/matita/docs/manual/tac_elimType.html delete mode 100644 helm/www/matita/docs/manual/tac_exact.html delete mode 100644 helm/www/matita/docs/manual/tac_exists.html delete mode 100644 helm/www/matita/docs/manual/tac_fail.html delete mode 100644 helm/www/matita/docs/manual/tac_fold.html delete mode 100644 helm/www/matita/docs/manual/tac_fourier.html delete mode 100644 helm/www/matita/docs/manual/tac_fwd.html delete mode 100644 helm/www/matita/docs/manual/tac_generalize.html delete mode 100644 helm/www/matita/docs/manual/tac_id.html delete mode 100644 helm/www/matita/docs/manual/tac_injection.html delete mode 100644 helm/www/matita/docs/manual/tac_intro.html delete mode 100644 helm/www/matita/docs/manual/tac_intros.html delete mode 100644 helm/www/matita/docs/manual/tac_inversion.html delete mode 100644 helm/www/matita/docs/manual/tac_lapply.html delete mode 100644 helm/www/matita/docs/manual/tac_left.html delete mode 100644 helm/www/matita/docs/manual/tac_letin.html delete mode 100644 helm/www/matita/docs/manual/tac_normalize.html delete mode 100644 helm/www/matita/docs/manual/tac_paramodulation.html delete mode 100644 helm/www/matita/docs/manual/tac_reduce.html delete mode 100644 helm/www/matita/docs/manual/tac_reflexivity.html delete mode 100644 helm/www/matita/docs/manual/tac_replace.html delete mode 100644 helm/www/matita/docs/manual/tac_rewrite.html delete mode 100644 helm/www/matita/docs/manual/tac_right.html delete mode 100644 helm/www/matita/docs/manual/tac_ring.html delete mode 100644 helm/www/matita/docs/manual/tac_simplify.html delete mode 100644 helm/www/matita/docs/manual/tac_split.html delete mode 100644 helm/www/matita/docs/manual/tac_symmetry.html delete mode 100644 helm/www/matita/docs/manual/tac_transitivity.html delete mode 100644 helm/www/matita/docs/manual/tac_unfold.html delete mode 100644 helm/www/matita/docs/manual/tac_whd.html diff --git a/helm/www/matita/docs/manual/WrtCoq.html b/helm/www/matita/docs/manual/WrtCoq.html deleted file mode 100644 index c72e87572..000000000 --- a/helm/www/matita/docs/manual/WrtCoq.html +++ /dev/null @@ -1,13 +0,0 @@ - - -Matita vs Coq

Matita vs Coq

- The system shares a common look&feel with the Coq proof assistant - and its graphical user interface. The two systems have the same logic, - very close proof languages and similar sets of tactics. Moreover, - Matita is compatible with the library of Coq. - From the user point of view the main lacking features - with respect to Coq are: -

  • proof extraction;

  • an extensible language of tactics;

  • automatic implicit arguments;

  • several ad-hoc decision procedures;

  • several rarely used variants for most of the tactics;

  • sections and local variables. To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions.

- Still from the user point of view, the main differences with respect - to Coq are: -

  • the language of tacticals that allows execution of partial tactical application;

  • the unification of the concept of metavariable and existential variable;

  • terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;

  • ambiguous terms are disambiguated by direct interaction with the user;

  • theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.

diff --git a/helm/www/matita/docs/manual/authoring.html b/helm/www/matita/docs/manual/authoring.html deleted file mode 100644 index bb4cab4b4..000000000 --- a/helm/www/matita/docs/manual/authoring.html +++ /dev/null @@ -1,62 +0,0 @@ - - -Authoring

Authoring

How to use developments

- A development is a set of scripts files that are strictly related (i.e. - they depend on each other). Matita is able to automatically manage - dependencies among the scripts in a development, compiling them in the - correct order. -

- The include statement can be performed by Matita only if the mentioned - script is compiled. If both scripts (the one that includes and the included) - are part of the same development, the included script (and recursively all - its dependencies) can be compiled automatically. Dependencies among scripts - belonging to different developments is not implemented yet. -

- The "Developments..." item the File menu (or pressing - Ctrl+D) opens the Developments window. -

Figure 3.1. The Developments window

Screenshot of the Developments window.

-

Developments window buttons

New

- To create a new Development the user needs to specify a name[1] - and the root directory in which all scripts will be placed, - eventually organized in subdirectories. The Development should be - named as the directory in which it lives. A "makefile" - file is placed in the specified root directory. That makefile - supports the following targets: -

all

- Build the whole development. -

clean

- Cleans the whole development. -

cleanall

- Resets the user environment (i.e. deleting all the results - of compilation of every development, including the contents - of the database). This target should be used only in case - something goes wrong and Matita behaves incorrectly. -

scriptname.mo

- Compiles "scriptname.ma" -

-

Delete

- Decompiles the whole development and removes it. -

Build

- Compiles all the scripts in the development. -

Clean

- Decompiles the whole development. -

Publish

- All the user developments live in the "user" space. That is, the - result of the compilation of scripts is placed in his home directory - and the tuples are placed in personal tables inside the database. - Publishing a development means putting it in the "library" space. This - means putting the result of compilation in the same place where the - standard library lives. This feature will be improved in the future - to support publishing the development in the "distributed - library" space (making your development public). -

Close

- Closes the Developments window -

-



[1] - The name of the Development should be the name of the directory in - which it lives. This is not a requirement, but the makefile - automatically generated by matita in the root directory of the - development will eventually generate a new Development with a name - that follows this convention. Having more than one development for - the same set of files is not an issue. -

diff --git a/helm/www/matita/docs/manual/axiom_definition_declaration.html b/helm/www/matita/docs/manual/axiom_definition_declaration.html deleted file mode 100644 index dd632607c..000000000 --- a/helm/www/matita/docs/manual/axiom_definition_declaration.html +++ /dev/null @@ -1,39 +0,0 @@ - - -Definitions and declarations

Definitions and declarations

axiom id: term

axiom H: P

H is declared as an axiom that states P

definition id[: term] [≝ term]

definition f: T ≝ t

f is defined as t; - T is its type. An error is raised if the type of - t is not convertible to T.

T is inferred from t if - omitted.

t can be omitted only if T is - given. In this case Matita enters in interactive mode and - f must be defined by means of tactics.

Notice that the command is equivalent to theorem f: T ≝ t.

[inductive|coinductive] id [args2]… : term ≝ [|] [id:term] [| id:term]… -[with id : term ≝ [|] [id:term] [| id:term]…]… -

inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'

Declares a family of two mutually inductive types - i and i' whose types are - S and S', which must be convertible - to sorts.

The constructors ki of type Ti - and ki' of type Ti' are also - simultaneously declared. The declared types i and - i' may occur in the types of the constructors, but - only in strongly positive positions according to the rules of the - calculus.

The whole family is parameterized over the arguments x,y,z.

If the keyword coinductive is used, the declared - types are considered mutually coinductive.

Elimination principles for the record are automatically generated - by Matita, if allowed by the typing rules of the calculus according to - the sort S. If generated, - they are named i_ind, i_rec and - i_rect according to the sort of their induction - predicate.

record id [args2]… : term ≝{[id [:|:>] term] [;id [:|:>] term]…}

record id x y z: S ≝ { f1: T1; …; fn:Tn }

Declares a new record family id parameterized over - x,y,z.

S is the type of the record - and it must be convertible to a sort.

Each field fi is declared by giving its type - Ti. A record without any field is admitted.

Elimination principles for the record are automatically generated - by Matita, if allowed by the typing rules of the calculus according to - the sort S. If generated, - they are named i_ind, i_rec and - i_rect according to the sort of their induction - predicate.

For each field fi a record projection - fi is also automatically generated if projection - is allowed by the typing rules of the calculus according to the - sort S, the type T1 and - the definability of depending record projections.

If the type of a field is declared with :>, - the corresponding record projection becomes an implicit coercion. - This is just syntactic sugar and it has the same effect of declaring the - record projection as a coercion later on.

diff --git a/helm/www/matita/docs/manual/cicbrowser.html b/helm/www/matita/docs/manual/cicbrowser.html deleted file mode 100644 index 68ea22383..000000000 --- a/helm/www/matita/docs/manual/cicbrowser.html +++ /dev/null @@ -1,22 +0,0 @@ - - -Browsing and searching

Browsing and searching

The CIC browser is used to browse and search the library. - You can open a new CIC browser selecting "New Cic Browser" - from the "View" menu of Matita, or by pressing "F3". - The CIC browser is similar to a traditional Web browser.

Browsing the library

To browse the library, type in the location bar the absolute URI of - the theorem, definition or library fragment you are interested in. - "cic:/" is the root of the library. Contributions developed - in Matita are under "cic:/matita"; all the others are - part of the library of Coq.

Following the hyperlinks it is possible to navigate in the Web - of mathematical notions. Proof are rendered in pseudo-natural language - and mathematical notation is used for formulae. For now, mathematical - notation must be included in the current script to be activated, but we - plan to remove this limitation.

Looking at a proof under development

A proof under development is not yet part of the library. - The special URI "about:proof" can be used to browse the - proof currently under development, if there is one. - The "home" button of the CIC browser sets the location bar to - "about:proof". -

Searching the library

The query bar of the CIC browser can be used to search the library - of Matita for theorems or definitions that match certain criteria. - The criteria is given by typing a term in the query bar and selecting - an action in the drop down menu right of it.

Searching by name

TODO

List of lemmas that can be applied

TODO

Searching by exact match

TODO

List of elimination principles for a given type

TODO

Searching by instantiation

TODO

diff --git a/helm/www/matita/docs/manual/docbook.css b/helm/www/matita/docs/manual/docbook.css deleted file mode 100644 index 0c92e77c9..000000000 --- a/helm/www/matita/docs/manual/docbook.css +++ /dev/null @@ -1,51 +0,0 @@ - -body { - background: url(../../images/sheetbg.png); -} - -ul.authorgroup { - list-style-type: none; - padding-left: 1em; -} - -div.titlepage { - background: #eaeaea; -} - -div.titlepage hr { - display: none; -} - -div.navheader hr { - display: none; -} - -div.navfooter hr { - display: none; -} - -div.navheader { - padding-left: 150px; - background: #eaeaea; -} - -div.navfooter { - background: #eaeaea; -} - -div.matita_logo { - position: absolute; - top: 3px; - left: 5px; -} - -div.matita_logo img { - border-style: none; -} - -div.matita_logo span { - position: absolute; - top: 13px; - left: 65px; - text-decoration: underline; -} diff --git a/helm/www/matita/docs/manual/index.html b/helm/www/matita/docs/manual/index.html deleted file mode 100644 index 0cf3d98f6..000000000 --- a/helm/www/matita/docs/manual/index.html +++ /dev/null @@ -1,9 +0,0 @@ - - -Matita V0.1.0 - User Manual (rev. 1α)

Matita V0.1.0 - User Manual (rev. 1α)

Both Matita and this document are free software, you can - redistribute them and/or modify them under the terms of the GNU General - Public License as published by the Free Software Foundation. See Chapter 9, License for more information.

Revision: 1α, 10/06/2006

List of Figures

3.1. The Developments window
diff --git a/helm/www/matita/docs/manual/proofs.html b/helm/www/matita/docs/manual/proofs.html deleted file mode 100644 index 19cecf7b8..000000000 --- a/helm/www/matita/docs/manual/proofs.html +++ /dev/null @@ -1,11 +0,0 @@ - - -Proofs

Proofs

theorem id[: term] [≝ term]

theorem f: P ≝ p

Proves a new theorem f whose thesis is - P.

If p is provided, it must be a proof term for - P. Otherwise an interactive proof is started.

P can be omitted only if the proof is not - interactive.

Proving a theorem already proved in the library is an error. - To provide an alternative name and proof for the same theorem, use - variant f: P ≝ p.

A warning is raised if the name of the theorem cannot be obtained - by mangling the name of the constants in its thesis.

Notice that the command is equivalent to definition f: T ≝ t.

variant id[: term] [≝ term]

variant f: T ≝ t

Same as theorem f: T ≝ t, but it does not - complain if the theorem has already been proved. To be used to give - an alternative name or proof to a theorem.

lemma id[: term] [≝ term]

lemma f: T ≝ t

Same as theorem f: T ≝ t

fact id[: term] [≝ term]

fact f: T ≝ t

Same as theorem f: T ≝ t

remark id[: term] [≝ term]

remark f: T ≝ t

Same as theorem f: T ≝ t

diff --git a/helm/www/matita/docs/manual/sec_commands.html b/helm/www/matita/docs/manual/sec_commands.html deleted file mode 100644 index 786d496b3..000000000 --- a/helm/www/matita/docs/manual/sec_commands.html +++ /dev/null @@ -1,5 +0,0 @@ - - -Chapter 8. Other commands

Chapter 8. Other commands

Table of Contents

Introduction

Introduction

- TODO -

diff --git a/helm/www/matita/docs/manual/sec_gettingstarted.html b/helm/www/matita/docs/manual/sec_gettingstarted.html deleted file mode 100644 index 66eaac015..000000000 --- a/helm/www/matita/docs/manual/sec_gettingstarted.html +++ /dev/null @@ -1,16 +0,0 @@ - - -Chapter 3. Getting started

Chapter 3. Getting started

If you are already familiar with the Calculus of (Co)Inductive - Constructions (CIC) and with interactive theorem provers with procedural - proof languages (expecially Coq), getting started with Matita is relatively - easy. You just need to learn how to type Unicode symbols, how to browse - and search the library and how to author a proof script.

How to type Unicode symbols

Unicode characters can be typed in several ways:

  • Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".

  • Typing the ligature "\name" where "name" - is a standard Unicode or LaTeX name for the character. Pressing - "Alt+L" just after the last character of the name converts - the ligature to the Unicode symbol. This operation is - not required since Matita understands also the "\name" - sequences. E.g. "\Omega" followed by Alt+L generates - "Ω".

  • Typing one of the following ligatures (and optionally - converting the ligature to the Unicode character has described before): - ":=" (which stands for ≝); "->" (which stands for - "→"); "=>" (which stands for "⇒").

diff --git a/helm/www/matita/docs/manual/sec_install.html b/helm/www/matita/docs/manual/sec_install.html deleted file mode 100644 index ee9361051..000000000 --- a/helm/www/matita/docs/manual/sec_install.html +++ /dev/null @@ -1,137 +0,0 @@ - - -Chapter 2. Installation

Chapter 2. Installation

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 users

If you are running a Debian GNU/Linux distribution - you can have APT install all the required tools and libraries by - adding the following repository to your - /etc/apt/sources.list:

-	      deb http://people.debian.org/~zack unstable helm
-	  

and installing the - helm-matita-deps package.

- -

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 we stronly encourage its use since a lot of - features are disabled without it. Still, the OCaml bindings of - the library are needed at compile time.

- 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 -

Database setup

To fully exploit Matita indexing and search capabilities you - will 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 in the table below, together with their - default values. - -

Table 2.1.  configure command line - arguments

ArgumentDefaultDescription
- --with-runtime-dir=dir - /usr/local/matita/

Runtime base directory where all Matita stuff - (executables, configuration files, standard - library, ...) will be installed

- --with-dbhost=host - 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 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. -

- -

diff --git a/helm/www/matita/docs/manual/sec_intro.html b/helm/www/matita/docs/manual/sec_intro.html deleted file mode 100644 index 47bfd2de1..000000000 --- a/helm/www/matita/docs/manual/sec_intro.html +++ /dev/null @@ -1,7 +0,0 @@ - - -Chapter 1. Introduction

Chapter 1. Introduction

Table of Contents

Features
Matita vs Coq

Features

Matita is an interactive theorem prover - (or proof assistant) with the following characteristics:

  • It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.

  • It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.

  • It has a stand-alone graphical user interface (GUI) inspired by -CtCoq/Proof General. The GUI is implemented according to the state -of the art. In particular:

    • It is based and fully integrated with Gtk/Gnome.

    • An on-line help can be browsed via the Gnome documentation browser.

    • Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.

  • It integrates advanced browsing and searching procedures.

  • It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.

  • It is compatible with the library of Coq (definitions and proof objects).

diff --git a/helm/www/matita/docs/manual/sec_license.html b/helm/www/matita/docs/manual/sec_license.html deleted file mode 100644 index c930a136a..000000000 --- a/helm/www/matita/docs/manual/sec_license.html +++ /dev/null @@ -1,14 +0,0 @@ - - -Chapter 9. License

Chapter 9. License

Both Matita and this document are part of HELM, an Hypertextual, - Electronic Library of Mathematics, developed at the Computer Science - Department, University of Bologna, Italy.

HELM is free software; you can redistribute it and/or modify it under - the terms of the GNU General Public License as published by the Free Software - Foundation; either version 2 of the License, or (at your option) any later - version.

HELM is distributed in the hope that it will be useful, but WITHOUT ANY - WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR - A PARTICULAR PURPOSE. See the GNU General Public License for more details. -

You should have received a copy of the GNU General Public License along - with HELM; if not, write to the Free Software Foundation, Inc., 51 Franklin - St, Fifth Floor, Boston, MA 02110-1301 USA. A copy of the GNU General - Public License is available at this link.

diff --git a/helm/www/matita/docs/manual/sec_tacticals.html b/helm/www/matita/docs/manual/sec_tacticals.html deleted file mode 100644 index 269c1119f..000000000 --- a/helm/www/matita/docs/manual/sec_tacticals.html +++ /dev/null @@ -1,5 +0,0 @@ - - -Chapter 7. Tacticals

Chapter 7. Tacticals

Table of Contents

Introduction

Introduction

- TODO -

diff --git a/helm/www/matita/docs/manual/sec_tactics.html b/helm/www/matita/docs/manual/sec_tactics.html deleted file mode 100644 index ae7e166ba..000000000 --- a/helm/www/matita/docs/manual/sec_tactics.html +++ /dev/null @@ -1,7 +0,0 @@ - - -Chapter 6. Tactics

Chapter 6. Tactics

absurd sterm

absurd P

-

Pre-conditions:

P must have type Prop.

Action:

It closes the current sequent by eliminating an - absurd term.

New sequents to prove:

It opens two new sequents of conclusion P - and ¬P.

-

diff --git a/helm/www/matita/docs/manual/sec_terms.html b/helm/www/matita/docs/manual/sec_terms.html deleted file mode 100644 index 9bd09915a..000000000 --- a/helm/www/matita/docs/manual/sec_terms.html +++ /dev/null @@ -1,56 +0,0 @@ - - -Chapter 4. Syntax

Chapter 4. Syntax

To describe syntax in this manual we use the following conventions:

  1. Non terminal symbols are emphasized and have a link to their - definition. E.g.: term

  2. Terminal symbols are in bold. E.g.: - theorem

  3. Optional sequences of elements are put in square brackets. - E.g.: [in term]

  4. Alternatives are put in square brakets and they are - separated by vertical bars. E.g.: [<|>]

  5. Repetition of sequences of elements are given by putting the - first sequence in square brackets, that are followed by three dots. - E.g.: [and term]…

Terms & co.

Lexical conventions

-

Table 4.1. id

id::=〈〈TODO〉〉 

-

Table 4.2. nat

nat::=〈〈TODO〉〉 

-

Table 4.3. uri

uri::=〈〈TODO〉〉 

-

Terms

-

Table 4.4. Terms

term::=stermsimple or delimited term
 |term termapplication
 |λargs.termλ-abstraction
 |Πargs.termdependent product meant to define a datatype
 |∀args.termdependent product meant to define a proposition
 |term → termnon-dependent product (logical implication or function space)
 |let [id|(id: term)] ≝ term in termlocal definition
 |let - [co]rec - id [id|(id[,term]… :term)]… [on nat] - [: term] - ≝ term - (co)recursive definitions
   - [and - [id|(id[,term]… :term)]… [on nat] - [: term] - ≝ term]… -  
   - in term -  
 |…user provided notation

- -

Table 4.5. Simple terms

sterm::=(term) 
 |id[\subst[ - id≔term - [;id≔term]… - ]] - identifier with optional explicit named substitution
 |uria qualified reference
 |Propthe impredicative sort of propositions
 |Setthe impredicate sort of datatypes
 |Typeone predicative sort of datatypes
 |?implicit argument
 |?n - [[ - [_|term]… - ]]metavariable
 |match term - [ in term ] - [ return term ] - with - case analysis
   - [ - match_pattern ⇒ term - [ - | - match_pattern ⇒ term - ]…]  
 |(term:term)cast
 |…user provided notation at precedence 90

- -

Table 4.6. Arguments

args::= - _[: term] - ignored argument
 | - (_[: term]) - ignored argument
 |id[,id]…[: term] 
 |(id[,id]…[: term]) 

- -

Table 4.7. Miscellaneous arguments

args2::=id 
 |(id[,id]…: term) 

- -

Table 4.8. Pattern matching

match_pattern::=id0-ary constructor
 |(id id [id]…)n-ary constructor (binds the n arguments)

-

diff --git a/helm/www/matita/docs/manual/sec_usernotation.html b/helm/www/matita/docs/manual/sec_usernotation.html deleted file mode 100644 index db6c34afd..000000000 --- a/helm/www/matita/docs/manual/sec_usernotation.html +++ /dev/null @@ -1,5 +0,0 @@ - - -Chapter 5. Extending the syntax

Chapter 5. Extending the syntax

Table of Contents

Introduction

Introduction

- TODO -

diff --git a/helm/www/matita/docs/manual/tac_apply.html b/helm/www/matita/docs/manual/tac_apply.html deleted file mode 100644 index ab85e3471..000000000 --- a/helm/www/matita/docs/manual/tac_apply.html +++ /dev/null @@ -1,13 +0,0 @@ - - -apply sterm

apply sterm

apply t

-

Pre-conditions:

t must have type - T1 → ... → - Tn → G - where G can be unified with the conclusion - of the current sequent.

Action:

It closes the current sequent by applying t to n implicit arguments (that become new sequents).

New sequents to prove:

It opens a new sequent for each premise - Ti that is not - instantiated by unification. Ti is - the conclusion of the i-th new sequent to - prove.

-

diff --git a/helm/www/matita/docs/manual/tac_assumption.html b/helm/www/matita/docs/manual/tac_assumption.html deleted file mode 100644 index 6dd35ee36..000000000 --- a/helm/www/matita/docs/manual/tac_assumption.html +++ /dev/null @@ -1,6 +0,0 @@ - - -assumption

assumption

assumption

-

Pre-conditions:

There must exist an hypothesis whose type can be unified with - the conclusion of the current sequent.

Action:

It closes the current sequent exploiting an hypothesis.

New sequents to prove:

None

-

diff --git a/helm/www/matita/docs/manual/tac_auto.html b/helm/www/matita/docs/manual/tac_auto.html deleted file mode 100644 index 31b733a64..000000000 --- a/helm/www/matita/docs/manual/tac_auto.html +++ /dev/null @@ -1,12 +0,0 @@ - - -auto [depth=nat] [width=nat] [paramodulation] [full]

auto [depth=nat] [width=nat] [paramodulation] [full]

auto depth=d width=w paramodulation full

-

Pre-conditions:

None, but the tactic may fail finding a proof if every - proof is in the search space that is pruned away. Pruning is - controlled by d and w. - Moreover, only lemmas whose type signature is a subset of the - signature of the current sequent are considered. The signature of - a sequent is ...TODO

Action:

It closes the current sequent by repeated application of - rewriting steps (unless paramodulation is - omitted), hypothesis and lemmas in the library.

New sequents to prove:

None

-

diff --git a/helm/www/matita/docs/manual/tac_change.html b/helm/www/matita/docs/manual/tac_change.html deleted file mode 100644 index 074ffa5b6..000000000 --- a/helm/www/matita/docs/manual/tac_change.html +++ /dev/null @@ -1,10 +0,0 @@ - - -change <pattern> with sterm

change <pattern> with sterm

change patt with t

-

Pre-conditions:

Each subterm matched by the pattern must be convertible - with the term t disambiguated in the context - of the matched subterm.

Action:

It replaces the subterms of the current sequent matched by - patt with the new term t. - For each subterm matched by the pattern, t is - disambiguated in the context of the subterm.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_clear.html b/helm/www/matita/docs/manual/tac_clear.html deleted file mode 100644 index 8bdfc8f57..000000000 --- a/helm/www/matita/docs/manual/tac_clear.html +++ /dev/null @@ -1,7 +0,0 @@ - - -clear id

clear id

clear H

-

Pre-conditions:

H must be an hypothesis of the - current sequent to prove.

Action:

It hides the hypothesis H from the - current sequent.

New sequents to prove:

None

-

diff --git a/helm/www/matita/docs/manual/tac_clearbody.html b/helm/www/matita/docs/manual/tac_clearbody.html deleted file mode 100644 index 8bc46403b..000000000 --- a/helm/www/matita/docs/manual/tac_clearbody.html +++ /dev/null @@ -1,7 +0,0 @@ - - -clearbody id

clearbody id

clearbody H

-

Pre-conditions:

H must be an hypothesis of the - current sequent to prove.

Action:

It hides the definiens of a definition in the current - sequent context. Thus the definition becomes an hypothesis.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_constructor.html b/helm/www/matita/docs/manual/tac_constructor.html deleted file mode 100644 index 9fc2a8b25..000000000 --- a/helm/www/matita/docs/manual/tac_constructor.html +++ /dev/null @@ -1,10 +0,0 @@ - - -constructor nat

constructor nat

constructor n

-

Pre-conditions:

The conclusion of the current sequent must be - an inductive type or the application of an inductive type with - at least n constructors.

Action:

It applies the n-th constructor of the - inductive type of the conclusion of the current sequent.

New sequents to prove:

It opens a new sequent for each premise of the constructor - that can not be inferred by unification. For more details, - see the apply tactic.

-

diff --git a/helm/www/matita/docs/manual/tac_contradiction.html b/helm/www/matita/docs/manual/tac_contradiction.html deleted file mode 100644 index 66a4e4c4d..000000000 --- a/helm/www/matita/docs/manual/tac_contradiction.html +++ /dev/null @@ -1,7 +0,0 @@ - - -contradiction

contradiction

contradiction

-

Pre-conditions:

There must be in the current context an hypothesis of type - False.

Action:

It closes the current sequent by applying an hypothesis of - type False.

New sequents to prove:

None

-

diff --git a/helm/www/matita/docs/manual/tac_cut.html b/helm/www/matita/docs/manual/tac_cut.html deleted file mode 100644 index dd9550209..000000000 --- a/helm/www/matita/docs/manual/tac_cut.html +++ /dev/null @@ -1,9 +0,0 @@ - - -cut sterm [as id]

cut sterm [as id]

cut P as H

-

Pre-conditions:

P must have type Prop.

Action:

It closes the current sequent.

New sequents to prove:

It opens two new sequents. The first one has an extra - hypothesis H:P. If H is - omitted, the name of the hypothesis is automatically generated. - The second sequent has conclusion P and - hypotheses the hypotheses of the current sequent to prove.

-

diff --git a/helm/www/matita/docs/manual/tac_decompose.html b/helm/www/matita/docs/manual/tac_decompose.html deleted file mode 100644 index d299feb29..000000000 --- a/helm/www/matita/docs/manual/tac_decompose.html +++ /dev/null @@ -1,5 +0,0 @@ - - -decompose id [id]… [<intros_spec>]

decompose id [id]… [<intros_spec>]

decompose ???

-

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

-

diff --git a/helm/www/matita/docs/manual/tac_discriminate.html b/helm/www/matita/docs/manual/tac_discriminate.html deleted file mode 100644 index 06c9c8333..000000000 --- a/helm/www/matita/docs/manual/tac_discriminate.html +++ /dev/null @@ -1,7 +0,0 @@ - - -discriminate sterm

discriminate sterm

discriminate p

-

Pre-conditions:

p must have type K t1 ... tn = K' t'1 ... t'm where K and K' must be different constructors of the same inductive type and each argument list can be empty if -its constructor takes no arguments.

Action:

It closes the current sequent by proving the absurdity of - p.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_elim.html b/helm/www/matita/docs/manual/tac_elim.html deleted file mode 100644 index 8638f4442..000000000 --- a/helm/www/matita/docs/manual/tac_elim.html +++ /dev/null @@ -1,15 +0,0 @@ - - -elim sterm [using sterm] [<intros_spec>]

elim sterm [using sterm] [<intros_spec>]

elim t using th hyps

-

Pre-conditions:

t must inhabit an inductive type and - th must be an elimination principle for that - inductive type. If th is omitted the appropriate - standard elimination principle is chosen.

Action:

It proceeds by cases on the values of t, - according to the elimination principle th. -

New sequents to prove:

It opens one new sequent for each case. The names of - the new hypotheses are picked by hyps, if - provided. If hyps specifies also a number of hypotheses that - is less than the number of new hypotheses for a new sequent, - then the exceeding hypothesis will be kept as implications in - the conclusion of the sequent.

-

diff --git a/helm/www/matita/docs/manual/tac_elimType.html b/helm/www/matita/docs/manual/tac_elimType.html deleted file mode 100644 index 95be78578..000000000 --- a/helm/www/matita/docs/manual/tac_elimType.html +++ /dev/null @@ -1,5 +0,0 @@ - - -elimType sterm [using sterm] [<intros_spec>]

elimType sterm [using sterm] [<intros_spec>]

elimType T using th hyps

-

Pre-conditions:

T must be an inductive type.

Action:

TODO (severely bugged now).

New sequents to prove:

TODO

-

diff --git a/helm/www/matita/docs/manual/tac_exact.html b/helm/www/matita/docs/manual/tac_exact.html deleted file mode 100644 index 37a49619d..000000000 --- a/helm/www/matita/docs/manual/tac_exact.html +++ /dev/null @@ -1,6 +0,0 @@ - - -exact sterm

exact sterm

exact p

-

Pre-conditions:

The type of p must be convertible - with the conclusion of the current sequent.

Action:

It closes the current sequent using p.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_exists.html b/helm/www/matita/docs/manual/tac_exists.html deleted file mode 100644 index 99d1bad19..000000000 --- a/helm/www/matita/docs/manual/tac_exists.html +++ /dev/null @@ -1,9 +0,0 @@ - - -exists

exists

exists

-

Pre-conditions:

The conclusion of the current sequent must be - an inductive type or the application of an inductive type - with at least one constructor.

Action:

Equivalent to constructor 1.

New sequents to prove:

It opens a new sequent for each premise of the first - constructor of the inductive type that is the conclusion of the - current sequent. For more details, see the constructor tactic.

-

diff --git a/helm/www/matita/docs/manual/tac_fail.html b/helm/www/matita/docs/manual/tac_fail.html deleted file mode 100644 index fefd9fbf3..000000000 --- a/helm/www/matita/docs/manual/tac_fail.html +++ /dev/null @@ -1,5 +0,0 @@ - - -fail

fail

fail

-

Pre-conditions:

None.

Action:

This tactic always fail.

New sequents to prove:

N.A.

-

diff --git a/helm/www/matita/docs/manual/tac_fold.html b/helm/www/matita/docs/manual/tac_fold.html deleted file mode 100644 index 35e8b50dc..000000000 --- a/helm/www/matita/docs/manual/tac_fold.html +++ /dev/null @@ -1,10 +0,0 @@ - - -fold <reduction_kind> sterm <pattern>

fold <reduction_kind> sterm <pattern>

fold red t patt

-

Pre-conditions:

The pattern must not specify the wanted term.

Action:

First of all it locates all the subterms matched by - patt. In the context of each matched subterm - it disambiguates the term t and reduces it - to its red normal form; then it replaces with - t every occurrence of the normal form in the - matched subterm.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_fourier.html b/helm/www/matita/docs/manual/tac_fourier.html deleted file mode 100644 index 506295b46..000000000 --- a/helm/www/matita/docs/manual/tac_fourier.html +++ /dev/null @@ -1,8 +0,0 @@ - - -fourier

fourier

fourier

-

Pre-conditions:

The conclusion of the current sequent must be a linear - inequation over real numbers taken from standard library of - Coq. Moreover the inequations in the hypotheses must imply the - inequation in the conclusion of the current sequent.

Action:

It closes the current sequent by applying the Fourier method.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_fwd.html b/helm/www/matita/docs/manual/tac_fwd.html deleted file mode 100644 index ccd4dc55f..000000000 --- a/helm/www/matita/docs/manual/tac_fwd.html +++ /dev/null @@ -1,5 +0,0 @@ - - -fwd id [<ident list>]

fwd id [<ident list>]

fwd ...TODO

-

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

-

diff --git a/helm/www/matita/docs/manual/tac_generalize.html b/helm/www/matita/docs/manual/tac_generalize.html deleted file mode 100644 index bcba8c3f9..000000000 --- a/helm/www/matita/docs/manual/tac_generalize.html +++ /dev/null @@ -1,14 +0,0 @@ - - -generalize <pattern> [as id]

generalize <pattern> [as id]

generalize patt as H

-

Pre-conditions:

All the terms matched by patt must be - convertible and close in the context of the current sequent.

Action:

It closes the current sequent by applying a stronger - lemma that is proved using the new generated sequent.

New sequents to prove:

It opens a new sequent where the current sequent conclusion - G is generalized to - ∀x.G{x/t} where {x/t} - is a notation for the replacement with x of all - the occurrences of the term t matched by - patt. If patt matches no - subterm then t is defined as the - wanted part of the pattern.

-

diff --git a/helm/www/matita/docs/manual/tac_id.html b/helm/www/matita/docs/manual/tac_id.html deleted file mode 100644 index f01158f6e..000000000 --- a/helm/www/matita/docs/manual/tac_id.html +++ /dev/null @@ -1,5 +0,0 @@ - - -id

id

id

-

Pre-conditions:

None.

Action:

This identity tactic does nothing without failing.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_injection.html b/helm/www/matita/docs/manual/tac_injection.html deleted file mode 100644 index 143c3a293..000000000 --- a/helm/www/matita/docs/manual/tac_injection.html +++ /dev/null @@ -1,9 +0,0 @@ - - -injection sterm

injection sterm

injection p

-

Pre-conditions:

p must have type K t1 ... tn = K t'1 ... t'n where both argument lists are empty if -K takes no arguments.

Action:

It derives new hypotheses by injectivity of - K.

New sequents to prove:

The new sequent to prove is equal to the current sequent - with the additional hypotheses - t1=t'1 ... tn=t'n.

-

diff --git a/helm/www/matita/docs/manual/tac_intro.html b/helm/www/matita/docs/manual/tac_intro.html deleted file mode 100644 index f99fdb346..000000000 --- a/helm/www/matita/docs/manual/tac_intro.html +++ /dev/null @@ -1,11 +0,0 @@ - - -intro [id]

intro [id]

intro H

-

Pre-conditions:

The conclusion of the sequent to prove must be an implication - or a universal quantification.

Action:

It applies the right introduction rule for implication, - closing the current sequent.

New sequents to prove:

It opens a new sequent to prove adding to the hypothesis - the antecedent of the implication and setting the conclusion - to the consequent of the implicaiton. The name of the new - hypothesis is H if provided; otherwise it - is automatically generated.

-

diff --git a/helm/www/matita/docs/manual/tac_intros.html b/helm/www/matita/docs/manual/tac_intros.html deleted file mode 100644 index 98683d76e..000000000 --- a/helm/www/matita/docs/manual/tac_intros.html +++ /dev/null @@ -1,15 +0,0 @@ - - -intros <intros_spec>

intros <intros_spec>

intros hyps

-

Pre-conditions:

If hyps specifies a number of hypotheses - to introduce, then the conclusion of the current sequent must - be formed by at least that number of imbricated implications - or universal quantifications.

Action:

It applies several times the right introduction rule for - implication, closing the current sequent.

New sequents to prove:

It opens a new sequent to prove adding a number of new - hypotheses equal to the number of new hypotheses requested. - If the user does not request a precise number of new hypotheses, - it adds as many hypotheses as possible. - The name of each new hypothesis is either popped from the - user provided list of names, or it is automatically generated when - the list is (or becomes) empty.

-

diff --git a/helm/www/matita/docs/manual/tac_inversion.html b/helm/www/matita/docs/manual/tac_inversion.html deleted file mode 100644 index ab2e5c36c..000000000 --- a/helm/www/matita/docs/manual/tac_inversion.html +++ /dev/null @@ -1,13 +0,0 @@ - - -inversion sterm

inversion sterm

inversion t

-

Pre-conditions:

The type of the term t must be an inductive - type or the application of an inductive type.

Action:

It proceeds by cases on t paying attention - to the constraints imposed by the actual "right arguments" - of the inductive type.

New sequents to prove:

It opens one new sequent to prove for each case in the - definition of the type of t. With respect to - a simple elimination, each new sequent has additional hypotheses - that states the equalities of the "right parameters" - of the inductive type with terms originally present in the - sequent to prove.

-

diff --git a/helm/www/matita/docs/manual/tac_lapply.html b/helm/www/matita/docs/manual/tac_lapply.html deleted file mode 100644 index 8684738db..000000000 --- a/helm/www/matita/docs/manual/tac_lapply.html +++ /dev/null @@ -1,5 +0,0 @@ - - -lapply [depth=nat] sterm [to <term list>] [using id]

lapply [depth=nat] sterm [to <term list>] [using id]

lapply ???

-

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

-

diff --git a/helm/www/matita/docs/manual/tac_left.html b/helm/www/matita/docs/manual/tac_left.html deleted file mode 100644 index 623ced5f2..000000000 --- a/helm/www/matita/docs/manual/tac_left.html +++ /dev/null @@ -1,9 +0,0 @@ - - -left

left

left

-

Pre-conditions:

The conclusion of the current sequent must be - an inductive type or the application of an inductive type - with at least one constructor.

Action:

Equivalent to constructor 1.

New sequents to prove:

It opens a new sequent for each premise of the first - constructor of the inductive type that is the conclusion of the - current sequent. For more details, see the constructor tactic.

-

diff --git a/helm/www/matita/docs/manual/tac_letin.html b/helm/www/matita/docs/manual/tac_letin.html deleted file mode 100644 index 83318bdb5..000000000 --- a/helm/www/matita/docs/manual/tac_letin.html +++ /dev/null @@ -1,6 +0,0 @@ - - -letin id ≝ sterm

letin id ≝ sterm

letin x ≝ t

-

Pre-conditions:

None.

Action:

It adds to the context of the current sequent to prove a new - definition x ≝ t.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_normalize.html b/helm/www/matita/docs/manual/tac_normalize.html deleted file mode 100644 index 4d1364cef..000000000 --- a/helm/www/matita/docs/manual/tac_normalize.html +++ /dev/null @@ -1,6 +0,0 @@ - - -normalize <pattern>

normalize <pattern>

normalize patt

-

Pre-conditions:

None.

Action:

It replaces all the terms matched by patt - with their βδιζ-normal form.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_paramodulation.html b/helm/www/matita/docs/manual/tac_paramodulation.html deleted file mode 100644 index b93cad741..000000000 --- a/helm/www/matita/docs/manual/tac_paramodulation.html +++ /dev/null @@ -1,5 +0,0 @@ - - -paramodulation <pattern>

paramodulation <pattern>

paramodulation patt

-

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

-

diff --git a/helm/www/matita/docs/manual/tac_reduce.html b/helm/www/matita/docs/manual/tac_reduce.html deleted file mode 100644 index 94120657d..000000000 --- a/helm/www/matita/docs/manual/tac_reduce.html +++ /dev/null @@ -1,6 +0,0 @@ - - -reduce <pattern>

reduce <pattern>

reduce patt

-

Pre-conditions:

None.

Action:

It replaces all the terms matched by patt - with their βδιζ-normal form.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_reflexivity.html b/helm/www/matita/docs/manual/tac_reflexivity.html deleted file mode 100644 index bbd9e3e32..000000000 --- a/helm/www/matita/docs/manual/tac_reflexivity.html +++ /dev/null @@ -1,7 +0,0 @@ - - -reflexivity

reflexivity

reflexivity

-

Pre-conditions:

The conclusion of the current sequent must be - t=t for some term t

Action:

It closes the current sequent by reflexivity - of equality.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_replace.html b/helm/www/matita/docs/manual/tac_replace.html deleted file mode 100644 index 48bdcfc4c..000000000 --- a/helm/www/matita/docs/manual/tac_replace.html +++ /dev/null @@ -1,10 +0,0 @@ - - -replace <pattern> with sterm

replace <pattern> with sterm

change patt with t

-

Pre-conditions:

None.

Action:

It replaces the subterms of the current sequent matched by - patt with the new term t. - For each subterm matched by the pattern, t is - disambiguated in the context of the subterm.

New sequents to prove:

For each matched term t' it opens - a new sequent to prove whose conclusion is - t'=t.

-

diff --git a/helm/www/matita/docs/manual/tac_rewrite.html b/helm/www/matita/docs/manual/tac_rewrite.html deleted file mode 100644 index 99185ab02..000000000 --- a/helm/www/matita/docs/manual/tac_rewrite.html +++ /dev/null @@ -1,13 +0,0 @@ - - -rewrite [<|>] sterm <pattern>

rewrite [<|>] sterm <pattern>

rewrite dir p patt

-

Pre-conditions:

p must be the proof of an equality, - possibly under some hypotheses.

Action:

It looks in every term matched by patt - for all the occurrences of the - left hand side of the equality that p proves - (resp. the right hand side if dir is - <). Every occurence found is replaced with - the opposite side of the equality.

New sequents to prove:

It opens one new sequent for each hypothesis of the - equality proved by p that is not closed - by unification.

-

diff --git a/helm/www/matita/docs/manual/tac_right.html b/helm/www/matita/docs/manual/tac_right.html deleted file mode 100644 index 25fea3b6a..000000000 --- a/helm/www/matita/docs/manual/tac_right.html +++ /dev/null @@ -1,9 +0,0 @@ - - -right

right

right

-

Pre-conditions:

The conclusion of the current sequent must be - an inductive type or the application of an inductive type with - at least two constructors.

Action:

Equivalent to constructor 2.

New sequents to prove:

It opens a new sequent for each premise of the second - constructor of the inductive type that is the conclusion of the - current sequent. For more details, see the constructor tactic.

-

diff --git a/helm/www/matita/docs/manual/tac_ring.html b/helm/www/matita/docs/manual/tac_ring.html deleted file mode 100644 index 64c63ed22..000000000 --- a/helm/www/matita/docs/manual/tac_ring.html +++ /dev/null @@ -1,9 +0,0 @@ - - -ring

ring

ring

-

Pre-conditions:

The conclusion of the current sequent must be an - equality over Coq's real numbers that can be proved using - the ring properties of the real numbers only.

Action:

It closes the current sequent veryfying the equality by - means of computation (i.e. this is a reflexive tactic, implemented - exploiting the "two level reasoning" technique).

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_simplify.html b/helm/www/matita/docs/manual/tac_simplify.html deleted file mode 100644 index a04a93994..000000000 --- a/helm/www/matita/docs/manual/tac_simplify.html +++ /dev/null @@ -1,6 +0,0 @@ - - -simplify <pattern>

simplify <pattern>

simplify patt

-

Pre-conditions:

None.

Action:

It replaces all the terms matched by patt - with other convertible terms that are supposed to be simpler.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_split.html b/helm/www/matita/docs/manual/tac_split.html deleted file mode 100644 index 00ffcd154..000000000 --- a/helm/www/matita/docs/manual/tac_split.html +++ /dev/null @@ -1,9 +0,0 @@ - - -split

split

split

-

Pre-conditions:

The conclusion of the current sequent must be - an inductive type or the application of an inductive type with - at least one constructor.

Action:

Equivalent to constructor 1.

New sequents to prove:

It opens a new sequent for each premise of the first - constructor of the inductive type that is the conclusion of the - current sequent. For more details, see the constructor tactic.

-

diff --git a/helm/www/matita/docs/manual/tac_symmetry.html b/helm/www/matita/docs/manual/tac_symmetry.html deleted file mode 100644 index 9bb5e00bd..000000000 --- a/helm/www/matita/docs/manual/tac_symmetry.html +++ /dev/null @@ -1,6 +0,0 @@ - - -symmetry

symmetry

The tactic symmetry

symmetry

-

Pre-conditions:

The conclusion of the current proof must be an equality.

Action:

It swaps the two sides of the equalityusing the symmetric - property.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_transitivity.html b/helm/www/matita/docs/manual/tac_transitivity.html deleted file mode 100644 index c7f26a277..000000000 --- a/helm/www/matita/docs/manual/tac_transitivity.html +++ /dev/null @@ -1,7 +0,0 @@ - - -transitivity sterm

transitivity sterm

transitivity t

-

Pre-conditions:

The conclusion of the current proof must be an equality.

Action:

It closes the current sequent by transitivity of the equality.

New sequents to prove:

It opens two new sequents l=t and - t=r where l and r are the left and right hand side of the equality in the conclusion of -the current sequent to prove.

-

diff --git a/helm/www/matita/docs/manual/tac_unfold.html b/helm/www/matita/docs/manual/tac_unfold.html deleted file mode 100644 index 0f23f268e..000000000 --- a/helm/www/matita/docs/manual/tac_unfold.html +++ /dev/null @@ -1,10 +0,0 @@ - - -unfold [sterm] <pattern>

unfold [sterm] <pattern>

unfold t patt

-

Pre-conditions:

None.

Action:

It finds all the occurrences of t - (possibly applied to arguments) in the subterms matched by - patt. Then it δ-expands each occurrence, - also performing β-reduction of the obtained term. If - t is omitted it defaults to each - subterm matched by patt.

New sequents to prove:

None.

-

diff --git a/helm/www/matita/docs/manual/tac_whd.html b/helm/www/matita/docs/manual/tac_whd.html deleted file mode 100644 index 25190ce3e..000000000 --- a/helm/www/matita/docs/manual/tac_whd.html +++ /dev/null @@ -1,6 +0,0 @@ - - -whd <pattern>

whd <pattern>

whd patt

-

Pre-conditions:

None.

Action:

It replaces all the terms matched by patt - with their βδιζ-weak-head normal form.

New sequents to prove:

None.

-

-- 2.39.2