From 5b99087bf1b8b8fb1086a72feb6f3fb258a402d8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 10 Jun 2006 13:20:50 +0000 Subject: [PATCH] first generation of manual from docbook better Makefile --- helm/www/matita/Makefile | 6 + 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/index.html | 32 ++++ 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, 789 insertions(+) create mode 100644 helm/www/matita/docs/manual/WrtCoq.html create mode 100644 helm/www/matita/docs/manual/authoring.html create mode 100644 helm/www/matita/docs/manual/axiom_definition_declaration.html create mode 100644 helm/www/matita/docs/manual/cicbrowser.html create mode 100644 helm/www/matita/docs/manual/index.html create mode 100644 helm/www/matita/docs/manual/proofs.html create mode 100644 helm/www/matita/docs/manual/sec_commands.html create mode 100644 helm/www/matita/docs/manual/sec_gettingstarted.html create mode 100644 helm/www/matita/docs/manual/sec_install.html create mode 100644 helm/www/matita/docs/manual/sec_intro.html create mode 100644 helm/www/matita/docs/manual/sec_license.html create mode 100644 helm/www/matita/docs/manual/sec_tacticals.html create mode 100644 helm/www/matita/docs/manual/sec_tactics.html create mode 100644 helm/www/matita/docs/manual/sec_terms.html create mode 100644 helm/www/matita/docs/manual/sec_usernotation.html create mode 100644 helm/www/matita/docs/manual/tac_apply.html create mode 100644 helm/www/matita/docs/manual/tac_assumption.html create mode 100644 helm/www/matita/docs/manual/tac_auto.html create mode 100644 helm/www/matita/docs/manual/tac_change.html create mode 100644 helm/www/matita/docs/manual/tac_clear.html create mode 100644 helm/www/matita/docs/manual/tac_clearbody.html create mode 100644 helm/www/matita/docs/manual/tac_constructor.html create mode 100644 helm/www/matita/docs/manual/tac_contradiction.html create mode 100644 helm/www/matita/docs/manual/tac_cut.html create mode 100644 helm/www/matita/docs/manual/tac_decompose.html create mode 100644 helm/www/matita/docs/manual/tac_discriminate.html create mode 100644 helm/www/matita/docs/manual/tac_elim.html create mode 100644 helm/www/matita/docs/manual/tac_elimType.html create mode 100644 helm/www/matita/docs/manual/tac_exact.html create mode 100644 helm/www/matita/docs/manual/tac_exists.html create mode 100644 helm/www/matita/docs/manual/tac_fail.html create mode 100644 helm/www/matita/docs/manual/tac_fold.html create mode 100644 helm/www/matita/docs/manual/tac_fourier.html create mode 100644 helm/www/matita/docs/manual/tac_fwd.html create mode 100644 helm/www/matita/docs/manual/tac_generalize.html create mode 100644 helm/www/matita/docs/manual/tac_id.html create mode 100644 helm/www/matita/docs/manual/tac_injection.html create mode 100644 helm/www/matita/docs/manual/tac_intro.html create mode 100644 helm/www/matita/docs/manual/tac_intros.html create mode 100644 helm/www/matita/docs/manual/tac_inversion.html create mode 100644 helm/www/matita/docs/manual/tac_lapply.html create mode 100644 helm/www/matita/docs/manual/tac_left.html create mode 100644 helm/www/matita/docs/manual/tac_letin.html create mode 100644 helm/www/matita/docs/manual/tac_normalize.html create mode 100644 helm/www/matita/docs/manual/tac_paramodulation.html create mode 100644 helm/www/matita/docs/manual/tac_reduce.html create mode 100644 helm/www/matita/docs/manual/tac_reflexivity.html create mode 100644 helm/www/matita/docs/manual/tac_replace.html create mode 100644 helm/www/matita/docs/manual/tac_rewrite.html create mode 100644 helm/www/matita/docs/manual/tac_right.html create mode 100644 helm/www/matita/docs/manual/tac_ring.html create mode 100644 helm/www/matita/docs/manual/tac_simplify.html create mode 100644 helm/www/matita/docs/manual/tac_split.html create mode 100644 helm/www/matita/docs/manual/tac_symmetry.html create mode 100644 helm/www/matita/docs/manual/tac_transitivity.html create mode 100644 helm/www/matita/docs/manual/tac_unfold.html create mode 100644 helm/www/matita/docs/manual/tac_whd.html diff --git a/helm/www/matita/Makefile b/helm/www/matita/Makefile index 72b216cb4..2cb06a5ab 100644 --- a/helm/www/matita/Makefile +++ b/helm/www/matita/Makefile @@ -17,12 +17,16 @@ all: @echo " images # build images for the splash screen" @echo +clean: + manual: manual-stamp manual-stamp: $(DOCS_SRC_DIR)/*.xml $(MAKE) -C $(DOCS_SRC_DIR)/ html + test -d $(DOCS_DEST_DIR)/ || mkdir -p $(DOCS_SRC_DIR)/ cp $(DOCS_SRC_DIR)/*.html $(DOCS_DEST_DIR)/ touch $@ +.PHONY: images images: images/matita.xcf for Y in `seq 0 $(SEQ)`; do \ convert images/matita.png -crop \ @@ -32,6 +36,8 @@ images: images/matita.xcf rm tmp.png clean: + rm -f manual-stamp +dist-clean: clean for X in `seq 0 $(SEQ)`; do\ rm images/bg$$X.png;\ done diff --git a/helm/www/matita/docs/manual/WrtCoq.html b/helm/www/matita/docs/manual/WrtCoq.html new file mode 100644 index 000000000..e365ebb4a --- /dev/null +++ b/helm/www/matita/docs/manual/WrtCoq.html @@ -0,0 +1,13 @@ + + +Matita vs Coq
Matita vs Coq
Prev Chapter 1. Introduction Next

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.

Prev Up Next
Chapter 1. Introduction Home Chapter 2. Installation
diff --git a/helm/www/matita/docs/manual/authoring.html b/helm/www/matita/docs/manual/authoring.html new file mode 100644 index 000000000..6219d1fa4 --- /dev/null +++ b/helm/www/matita/docs/manual/authoring.html @@ -0,0 +1,62 @@ + + +Authoring
Authoring
Prev Chapter 3. Getting started Next

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

Prev Up Next
Browsing and searching Home Chapter 4. Syntax
diff --git a/helm/www/matita/docs/manual/axiom_definition_declaration.html b/helm/www/matita/docs/manual/axiom_definition_declaration.html new file mode 100644 index 000000000..ab327f1bf --- /dev/null +++ b/helm/www/matita/docs/manual/axiom_definition_declaration.html @@ -0,0 +1,39 @@ + + +Definitions and declarations
Definitions and declarations
Prev Chapter 4. Syntax Next

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.

Prev Up Next
Chapter 4. Syntax Home Proofs
diff --git a/helm/www/matita/docs/manual/cicbrowser.html b/helm/www/matita/docs/manual/cicbrowser.html new file mode 100644 index 000000000..881b720b2 --- /dev/null +++ b/helm/www/matita/docs/manual/cicbrowser.html @@ -0,0 +1,22 @@ + + +Browsing and searching
Browsing and searching
Prev Chapter 3. Getting started Next

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

Prev Up Next
Chapter 3. Getting started Home Authoring
diff --git a/helm/www/matita/docs/manual/index.html b/helm/www/matita/docs/manual/index.html new file mode 100644 index 000000000..46e5f05cd --- /dev/null +++ b/helm/www/matita/docs/manual/index.html @@ -0,0 +1,32 @@ + + +Matita V0.1.0 + Manual (rev. 0)
Matita V0.1.0 + Manual (rev. 0)
   Next

Matita V0.1.0 + Manual (rev. 0)

Andrea Asperti

  

Claudio Sacerdoti Coen

  

Enrico Tassi

  

Stefano Zacchiroli

  

This manual describes version 0.1.0 + of Matita. +

Copyright © 2006 The HELM team.

This file is 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., 59 + Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU + General Public License is available at this link.

Feedback

To report a bug or make a suggestion regarding the Matita + application or this manual, follow the directions in the + HELM Bug + Tracking System Page. +

Revision History
Revision Matita V0.1.0 + Manual (rev. 0)February 2006 
+

The HELM team + +

+ +
Revision 04 February 2006HELM
+ First draft completed. +

Table of Contents

1. Introduction
Features
Matita vs Coq
2. Installation
Installing from sources
Getting the source code
Requirements
Database setup
Compiling and installing
3. Getting started
How to type Unicode symbols
Browsing and searching
Browsing the library
Looking at a proof under development
Searching the library
Authoring
How to use developments
4. Syntax
Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
(co)inductive types declaration
record
Proofs
theorem
variant
lemma
fact
remark
5. Extending the syntax
Introduction
6. Tactics
absurd
apply
assumption
auto
clear
clearbody
change
constructor
contradiction
cut
decompose
discriminate
elim
elimType
exact
exists
failt
fold
fourier
fwd
generalize
id
injection
intro
intros
inversion
lapply
left
letin
normalize
paramodulation
reduce
reflexivity
change
rewrite
right
ring
simplify
split
symmetry
transitivity
unfold
whd
7. Tacticals
Introduction
8. Other commands
Introduction
9. License

List of Figures

3.1. The Developments window

List of Tables

2.1. configure command line + arguments
4.1. id
4.2. nat
4.3. uri
4.4. Terms
4.5. Simple terms
4.6. Arguments
4.7. Miscellaneous arguments
4.8. Pattern matching
   Next
   Chapter 1. Introduction
diff --git a/helm/www/matita/docs/manual/proofs.html b/helm/www/matita/docs/manual/proofs.html new file mode 100644 index 000000000..45f9c1f9b --- /dev/null +++ b/helm/www/matita/docs/manual/proofs.html @@ -0,0 +1,11 @@ + + +Proofs
Proofs
Prev Chapter 4. Syntax Next

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

Prev Up Next
Definitions and declarations Home Chapter 5. Extending the syntax
diff --git a/helm/www/matita/docs/manual/sec_commands.html b/helm/www/matita/docs/manual/sec_commands.html new file mode 100644 index 000000000..86c388c58 --- /dev/null +++ b/helm/www/matita/docs/manual/sec_commands.html @@ -0,0 +1,5 @@ + + +Chapter 8. Other commands
Chapter 8. Other commands
Prev   Next

Chapter 8. Other commands

Table of Contents

Introduction

Introduction

+ TODO +

Prev   Next
Chapter 7. Tacticals Home Chapter 9. License
diff --git a/helm/www/matita/docs/manual/sec_gettingstarted.html b/helm/www/matita/docs/manual/sec_gettingstarted.html new file mode 100644 index 000000000..26df16cec --- /dev/null +++ b/helm/www/matita/docs/manual/sec_gettingstarted.html @@ -0,0 +1,16 @@ + + +Chapter 3. Getting started
Chapter 3. Getting started
Prev   Next

Chapter 3. Getting started

Table of Contents

How to type Unicode symbols
Browsing and searching
Browsing the library
Looking at a proof under development
Searching the library
Authoring
How to use developments

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 "⇒").

Prev   Next
Chapter 2. Installation Home Browsing and searching
diff --git a/helm/www/matita/docs/manual/sec_install.html b/helm/www/matita/docs/manual/sec_install.html new file mode 100644 index 000000000..6eb21eb3a --- /dev/null +++ b/helm/www/matita/docs/manual/sec_install.html @@ -0,0 +1,137 @@ + + +Chapter 2. Installation
Chapter 2. Installation
Prev   Next

Chapter 2. Installation

Table of Contents

Installing from sources
Getting the source code
Requirements
Database setup
Compiling and installing

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

+ +

Prev   Next
Matita vs Coq Home Chapter 3. Getting started
diff --git a/helm/www/matita/docs/manual/sec_intro.html b/helm/www/matita/docs/manual/sec_intro.html new file mode 100644 index 000000000..a7f5cb375 --- /dev/null +++ b/helm/www/matita/docs/manual/sec_intro.html @@ -0,0 +1,7 @@ + + +Chapter 1. Introduction
Chapter 1. Introduction
Prev   Next

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

Prev   Next
Matita V0.1.0 + Manual (rev. 0) Home Matita vs Coq
diff --git a/helm/www/matita/docs/manual/sec_license.html b/helm/www/matita/docs/manual/sec_license.html new file mode 100644 index 000000000..7bcc0d633 --- /dev/null +++ b/helm/www/matita/docs/manual/sec_license.html @@ -0,0 +1,14 @@ + + +Chapter 9. License
Chapter 9. License
Prev   

Chapter 9. License

This file is 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., 59 + Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU + General Public License is available at this link.

Prev   
Chapter 8. Other commands Home 
diff --git a/helm/www/matita/docs/manual/sec_tacticals.html b/helm/www/matita/docs/manual/sec_tacticals.html new file mode 100644 index 000000000..12468ccea --- /dev/null +++ b/helm/www/matita/docs/manual/sec_tacticals.html @@ -0,0 +1,5 @@ + + +Chapter 7. Tacticals
Chapter 7. Tacticals
Prev   Next

Chapter 7. Tacticals

Table of Contents

Introduction

Introduction

+ TODO +

Prev   Next
whd <pattern> Home Chapter 8. Other commands
diff --git a/helm/www/matita/docs/manual/sec_tactics.html b/helm/www/matita/docs/manual/sec_tactics.html new file mode 100644 index 000000000..81b8e6ee7 --- /dev/null +++ b/helm/www/matita/docs/manual/sec_tactics.html @@ -0,0 +1,7 @@ + + +Chapter 6. Tactics
Chapter 6. Tactics
Prev   Next

Chapter 6. Tactics

Table of Contents

absurd
apply
assumption
auto
clear
clearbody
change
constructor
contradiction
cut
decompose
discriminate
elim
elimType
exact
exists
failt
fold
fourier
fwd
generalize
id
injection
intro
intros
inversion
lapply
left
letin
normalize
paramodulation
reduce
reflexivity
change
rewrite
right
ring
simplify
split
symmetry
transitivity
unfold
whd

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.

+

Prev   Next
Chapter 5. Extending the syntax Home apply sterm
diff --git a/helm/www/matita/docs/manual/sec_terms.html b/helm/www/matita/docs/manual/sec_terms.html new file mode 100644 index 000000000..2d7469668 --- /dev/null +++ b/helm/www/matita/docs/manual/sec_terms.html @@ -0,0 +1,56 @@ + + +Chapter 4. Syntax
Chapter 4. Syntax
Prev   Next

Chapter 4. Syntax

Table of Contents

Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
(co)inductive types declaration
record
Proofs
theorem
variant
lemma
fact
remark

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)

+

Prev   Next
Authoring Home Definitions and declarations
diff --git a/helm/www/matita/docs/manual/sec_usernotation.html b/helm/www/matita/docs/manual/sec_usernotation.html new file mode 100644 index 000000000..215602b19 --- /dev/null +++ b/helm/www/matita/docs/manual/sec_usernotation.html @@ -0,0 +1,5 @@ + + +Chapter 5. Extending the syntax
Chapter 5. Extending the syntax
Prev   Next

Chapter 5. Extending the syntax

Table of Contents

Introduction

Introduction

+ TODO +

Prev   Next
Proofs Home Chapter 6. Tactics
diff --git a/helm/www/matita/docs/manual/tac_apply.html b/helm/www/matita/docs/manual/tac_apply.html new file mode 100644 index 000000000..9518c40d7 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_apply.html @@ -0,0 +1,13 @@ + + +apply sterm
apply sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
Chapter 6. Tactics Home assumption
diff --git a/helm/www/matita/docs/manual/tac_assumption.html b/helm/www/matita/docs/manual/tac_assumption.html new file mode 100644 index 000000000..63a4a0798 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_assumption.html @@ -0,0 +1,6 @@ + + +assumption
assumption
Prev Chapter 6. Tactics Next

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

+

Prev Up Next
apply sterm Home auto [depth=nat] [width=nat] [paramodulation] [full]
diff --git a/helm/www/matita/docs/manual/tac_auto.html b/helm/www/matita/docs/manual/tac_auto.html new file mode 100644 index 000000000..eb67e6dca --- /dev/null +++ b/helm/www/matita/docs/manual/tac_auto.html @@ -0,0 +1,12 @@ + + +auto [depth=nat] [width=nat] [paramodulation] [full]
auto [depth=nat] [width=nat] [paramodulation] [full]
Prev Chapter 6. Tactics Next

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

+

Prev Up Next
assumption Home clear id
diff --git a/helm/www/matita/docs/manual/tac_change.html b/helm/www/matita/docs/manual/tac_change.html new file mode 100644 index 000000000..82c07ced8 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_change.html @@ -0,0 +1,10 @@ + + +change <pattern> with sterm
change <pattern> with sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
clearbody id Home constructor nat
diff --git a/helm/www/matita/docs/manual/tac_clear.html b/helm/www/matita/docs/manual/tac_clear.html new file mode 100644 index 000000000..31d632ca8 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_clear.html @@ -0,0 +1,7 @@ + + +clear id
clear id
Prev Chapter 6. Tactics Next

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

+

Prev Up Next
auto [depth=nat] [width=nat] [paramodulation] [full] Home clearbody id
diff --git a/helm/www/matita/docs/manual/tac_clearbody.html b/helm/www/matita/docs/manual/tac_clearbody.html new file mode 100644 index 000000000..678b62f12 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_clearbody.html @@ -0,0 +1,7 @@ + + +clearbody id
clearbody id
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
clear id Home change <pattern> with sterm
diff --git a/helm/www/matita/docs/manual/tac_constructor.html b/helm/www/matita/docs/manual/tac_constructor.html new file mode 100644 index 000000000..4679c535d --- /dev/null +++ b/helm/www/matita/docs/manual/tac_constructor.html @@ -0,0 +1,10 @@ + + +constructor nat
constructor nat
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
change <pattern> with sterm Home contradiction
diff --git a/helm/www/matita/docs/manual/tac_contradiction.html b/helm/www/matita/docs/manual/tac_contradiction.html new file mode 100644 index 000000000..2fe4c21d0 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_contradiction.html @@ -0,0 +1,7 @@ + + +contradiction
contradiction
Prev Chapter 6. Tactics Next

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

+

Prev Up Next
constructor nat Home cut sterm [as id]
diff --git a/helm/www/matita/docs/manual/tac_cut.html b/helm/www/matita/docs/manual/tac_cut.html new file mode 100644 index 000000000..fa956c441 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_cut.html @@ -0,0 +1,9 @@ + + +cut sterm [as id]
cut sterm [as id]
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
contradiction Home decompose id [id]… [<intros_spec>]
diff --git a/helm/www/matita/docs/manual/tac_decompose.html b/helm/www/matita/docs/manual/tac_decompose.html new file mode 100644 index 000000000..2fabae2e8 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_decompose.html @@ -0,0 +1,5 @@ + + +decompose id [id]… [<intros_spec>]
decompose id [id]… [<intros_spec>]
Prev Chapter 6. Tactics Next

decompose id [id]… [<intros_spec>]

decompose ???

+

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

+

Prev Up Next
cut sterm [as id] Home discriminate sterm
diff --git a/helm/www/matita/docs/manual/tac_discriminate.html b/helm/www/matita/docs/manual/tac_discriminate.html new file mode 100644 index 000000000..34f6c6aaa --- /dev/null +++ b/helm/www/matita/docs/manual/tac_discriminate.html @@ -0,0 +1,7 @@ + + +discriminate sterm
discriminate sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
decompose id [id]… [<intros_spec>] Home elim sterm [using sterm] [<intros_spec>]
diff --git a/helm/www/matita/docs/manual/tac_elim.html b/helm/www/matita/docs/manual/tac_elim.html new file mode 100644 index 000000000..22ad67bf9 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_elim.html @@ -0,0 +1,15 @@ + + +elim sterm [using sterm] [<intros_spec>]
elim sterm [using sterm] [<intros_spec>]
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
discriminate sterm Home elimType sterm [using sterm] [<intros_spec>]
diff --git a/helm/www/matita/docs/manual/tac_elimType.html b/helm/www/matita/docs/manual/tac_elimType.html new file mode 100644 index 000000000..0381aeea4 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_elimType.html @@ -0,0 +1,5 @@ + + +elimType sterm [using sterm] [<intros_spec>]
elimType sterm [using sterm] [<intros_spec>]
Prev Chapter 6. Tactics Next

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

+

Prev Up Next
elim sterm [using sterm] [<intros_spec>] Home exact sterm
diff --git a/helm/www/matita/docs/manual/tac_exact.html b/helm/www/matita/docs/manual/tac_exact.html new file mode 100644 index 000000000..b7e7d7e8c --- /dev/null +++ b/helm/www/matita/docs/manual/tac_exact.html @@ -0,0 +1,6 @@ + + +exact sterm
exact sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
elimType sterm [using sterm] [<intros_spec>] Home exists
diff --git a/helm/www/matita/docs/manual/tac_exists.html b/helm/www/matita/docs/manual/tac_exists.html new file mode 100644 index 000000000..7b977fbf6 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_exists.html @@ -0,0 +1,9 @@ + + +exists
exists
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
exact sterm Home fail
diff --git a/helm/www/matita/docs/manual/tac_fail.html b/helm/www/matita/docs/manual/tac_fail.html new file mode 100644 index 000000000..62f634fa5 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_fail.html @@ -0,0 +1,5 @@ + + +fail
fail
Prev Chapter 6. Tactics Next

fail

fail

+

Pre-conditions:

None.

Action:

This tactic always fail.

New sequents to prove:

N.A.

+

Prev Up Next
exists Home fold <reduction_kind> sterm <pattern>
diff --git a/helm/www/matita/docs/manual/tac_fold.html b/helm/www/matita/docs/manual/tac_fold.html new file mode 100644 index 000000000..e408787e0 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_fold.html @@ -0,0 +1,10 @@ + + +fold <reduction_kind> sterm <pattern>
fold <reduction_kind> sterm <pattern>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
fail  Home fourier
diff --git a/helm/www/matita/docs/manual/tac_fourier.html b/helm/www/matita/docs/manual/tac_fourier.html new file mode 100644 index 000000000..10f29a1e2 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_fourier.html @@ -0,0 +1,8 @@ + + +fourier
fourier
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
fold <reduction_kind> sterm <pattern> Home fwd id [<ident list>]
diff --git a/helm/www/matita/docs/manual/tac_fwd.html b/helm/www/matita/docs/manual/tac_fwd.html new file mode 100644 index 000000000..6f99a1e19 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_fwd.html @@ -0,0 +1,5 @@ + + +fwd id [<ident list>]
fwd id [<ident list>]
Prev Chapter 6. Tactics Next

fwd id [<ident list>]

fwd ...TODO

+

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

+

Prev Up Next
fourier Home generalize <pattern> [as id]
diff --git a/helm/www/matita/docs/manual/tac_generalize.html b/helm/www/matita/docs/manual/tac_generalize.html new file mode 100644 index 000000000..8e03a551f --- /dev/null +++ b/helm/www/matita/docs/manual/tac_generalize.html @@ -0,0 +1,14 @@ + + +generalize <pattern> [as id]
generalize <pattern> [as id]
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
fwd id [<ident list>] Home id
diff --git a/helm/www/matita/docs/manual/tac_id.html b/helm/www/matita/docs/manual/tac_id.html new file mode 100644 index 000000000..bef48017b --- /dev/null +++ b/helm/www/matita/docs/manual/tac_id.html @@ -0,0 +1,5 @@ + + +id
id
Prev Chapter 6. Tactics Next

id

id

+

Pre-conditions:

None.

Action:

This identity tactic does nothing without failing.

New sequents to prove:

None.

+

Prev Up Next
generalize <pattern> [as id] Home injection sterm
diff --git a/helm/www/matita/docs/manual/tac_injection.html b/helm/www/matita/docs/manual/tac_injection.html new file mode 100644 index 000000000..f6a4b2676 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_injection.html @@ -0,0 +1,9 @@ + + +injection sterm
injection sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
id Home intro [id]
diff --git a/helm/www/matita/docs/manual/tac_intro.html b/helm/www/matita/docs/manual/tac_intro.html new file mode 100644 index 000000000..6361dd079 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_intro.html @@ -0,0 +1,11 @@ + + +intro [id]
intro [id]
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
injection sterm Home intros <intros_spec>
diff --git a/helm/www/matita/docs/manual/tac_intros.html b/helm/www/matita/docs/manual/tac_intros.html new file mode 100644 index 000000000..2732fc853 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_intros.html @@ -0,0 +1,15 @@ + + +intros <intros_spec>
intros <intros_spec>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
intro [id] Home inversion sterm
diff --git a/helm/www/matita/docs/manual/tac_inversion.html b/helm/www/matita/docs/manual/tac_inversion.html new file mode 100644 index 000000000..ea424be3e --- /dev/null +++ b/helm/www/matita/docs/manual/tac_inversion.html @@ -0,0 +1,13 @@ + + +inversion sterm
inversion sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
intros <intros_spec> Home lapply [depth=nat] sterm [to <term list>] [using id]
diff --git a/helm/www/matita/docs/manual/tac_lapply.html b/helm/www/matita/docs/manual/tac_lapply.html new file mode 100644 index 000000000..6784e7679 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_lapply.html @@ -0,0 +1,5 @@ + + +lapply [depth=nat] sterm [to <term list>] [using id]
lapply [depth=nat] sterm [to <term list>] [using id]
Prev Chapter 6. Tactics Next

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

lapply ???

+

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

+

Prev Up Next
inversion sterm Home left
diff --git a/helm/www/matita/docs/manual/tac_left.html b/helm/www/matita/docs/manual/tac_left.html new file mode 100644 index 000000000..65298b52f --- /dev/null +++ b/helm/www/matita/docs/manual/tac_left.html @@ -0,0 +1,9 @@ + + +left
left
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
lapply [depth=nat] sterm [to <term list>] [using id] Home letin id ≝ sterm
diff --git a/helm/www/matita/docs/manual/tac_letin.html b/helm/www/matita/docs/manual/tac_letin.html new file mode 100644 index 000000000..97b285b3b --- /dev/null +++ b/helm/www/matita/docs/manual/tac_letin.html @@ -0,0 +1,6 @@ + + +letin id ≝ sterm
letin id ≝ sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
left Home normalize <pattern>
diff --git a/helm/www/matita/docs/manual/tac_normalize.html b/helm/www/matita/docs/manual/tac_normalize.html new file mode 100644 index 000000000..f4a60120b --- /dev/null +++ b/helm/www/matita/docs/manual/tac_normalize.html @@ -0,0 +1,6 @@ + + +normalize <pattern>
normalize <pattern>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
letin id ≝ sterm Home paramodulation <pattern>
diff --git a/helm/www/matita/docs/manual/tac_paramodulation.html b/helm/www/matita/docs/manual/tac_paramodulation.html new file mode 100644 index 000000000..7a0973326 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_paramodulation.html @@ -0,0 +1,5 @@ + + +paramodulation <pattern>
paramodulation <pattern>
Prev Chapter 6. Tactics Next

paramodulation <pattern>

paramodulation patt

+

Pre-conditions:

TODO.

Action:

TODO.

New sequents to prove:

TODO.

+

Prev Up Next
normalize <pattern> Home reduce <pattern>
diff --git a/helm/www/matita/docs/manual/tac_reduce.html b/helm/www/matita/docs/manual/tac_reduce.html new file mode 100644 index 000000000..309681c9e --- /dev/null +++ b/helm/www/matita/docs/manual/tac_reduce.html @@ -0,0 +1,6 @@ + + +reduce <pattern>
reduce <pattern>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
paramodulation <pattern> Home reflexivity
diff --git a/helm/www/matita/docs/manual/tac_reflexivity.html b/helm/www/matita/docs/manual/tac_reflexivity.html new file mode 100644 index 000000000..1afd09b38 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_reflexivity.html @@ -0,0 +1,7 @@ + + +reflexivity
reflexivity
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
reduce <pattern> Home replace <pattern> with sterm
diff --git a/helm/www/matita/docs/manual/tac_replace.html b/helm/www/matita/docs/manual/tac_replace.html new file mode 100644 index 000000000..d7134f590 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_replace.html @@ -0,0 +1,10 @@ + + +replace <pattern> with sterm
replace <pattern> with sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
reflexivity Home rewrite [<|>] sterm <pattern>
diff --git a/helm/www/matita/docs/manual/tac_rewrite.html b/helm/www/matita/docs/manual/tac_rewrite.html new file mode 100644 index 000000000..21155e6d9 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_rewrite.html @@ -0,0 +1,13 @@ + + +rewrite [<|>] sterm <pattern>
rewrite [<|>] sterm <pattern>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
replace <pattern> with sterm Home right
diff --git a/helm/www/matita/docs/manual/tac_right.html b/helm/www/matita/docs/manual/tac_right.html new file mode 100644 index 000000000..2874f0b37 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_right.html @@ -0,0 +1,9 @@ + + +right
right
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
rewrite [<|>] sterm <pattern> Home ring
diff --git a/helm/www/matita/docs/manual/tac_ring.html b/helm/www/matita/docs/manual/tac_ring.html new file mode 100644 index 000000000..798602f85 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_ring.html @@ -0,0 +1,9 @@ + + +ring
ring
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
right Home simplify <pattern>
diff --git a/helm/www/matita/docs/manual/tac_simplify.html b/helm/www/matita/docs/manual/tac_simplify.html new file mode 100644 index 000000000..3ed94a32c --- /dev/null +++ b/helm/www/matita/docs/manual/tac_simplify.html @@ -0,0 +1,6 @@ + + +simplify <pattern>
simplify <pattern>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
ring Home split
diff --git a/helm/www/matita/docs/manual/tac_split.html b/helm/www/matita/docs/manual/tac_split.html new file mode 100644 index 000000000..52872dc7e --- /dev/null +++ b/helm/www/matita/docs/manual/tac_split.html @@ -0,0 +1,9 @@ + + +split
split
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
simplify <pattern> Home symmetry
diff --git a/helm/www/matita/docs/manual/tac_symmetry.html b/helm/www/matita/docs/manual/tac_symmetry.html new file mode 100644 index 000000000..0f544da10 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_symmetry.html @@ -0,0 +1,6 @@ + + +symmetry
symmetry
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
split Home transitivity sterm
diff --git a/helm/www/matita/docs/manual/tac_transitivity.html b/helm/www/matita/docs/manual/tac_transitivity.html new file mode 100644 index 000000000..0db99505c --- /dev/null +++ b/helm/www/matita/docs/manual/tac_transitivity.html @@ -0,0 +1,7 @@ + + +transitivity sterm
transitivity sterm
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
symmetry Home unfold [sterm] <pattern>
diff --git a/helm/www/matita/docs/manual/tac_unfold.html b/helm/www/matita/docs/manual/tac_unfold.html new file mode 100644 index 000000000..120ce67d3 --- /dev/null +++ b/helm/www/matita/docs/manual/tac_unfold.html @@ -0,0 +1,10 @@ + + +unfold [sterm] <pattern>
unfold [sterm] <pattern>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
transitivity sterm Home whd <pattern>
diff --git a/helm/www/matita/docs/manual/tac_whd.html b/helm/www/matita/docs/manual/tac_whd.html new file mode 100644 index 000000000..636ff383a --- /dev/null +++ b/helm/www/matita/docs/manual/tac_whd.html @@ -0,0 +1,6 @@ + + +whd <pattern>
whd <pattern>
Prev Chapter 6. Tactics Next

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.

+

Prev Up Next
unfold [sterm] <pattern> Home Chapter 7. Tacticals
-- 2.39.2