From f64e7e9e24f63a926191f08c6e36ef6763718127 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 10 Jun 2006 16:20:16 +0000 Subject: [PATCH] manual regenerated --- helm/www/matita/docs/manual/WrtCoq.html | 2 +- helm/www/matita/docs/manual/authoring.html | 8 +-- .../manual/axiom_definition_declaration.html | 2 +- helm/www/matita/docs/manual/cicbrowser.html | 2 +- helm/www/matita/docs/manual/docbook.css | 51 +++++++++++++++++++ helm/www/matita/docs/manual/index.html | 35 +++---------- helm/www/matita/docs/manual/proofs.html | 2 +- helm/www/matita/docs/manual/sec_commands.html | 2 +- .../docs/manual/sec_gettingstarted.html | 2 +- helm/www/matita/docs/manual/sec_install.html | 4 +- helm/www/matita/docs/manual/sec_intro.html | 6 +-- helm/www/matita/docs/manual/sec_license.html | 24 ++++----- .../www/matita/docs/manual/sec_tacticals.html | 2 +- helm/www/matita/docs/manual/sec_tactics.html | 2 +- helm/www/matita/docs/manual/sec_terms.html | 18 +++---- .../matita/docs/manual/sec_usernotation.html | 2 +- helm/www/matita/docs/manual/tac_apply.html | 2 +- .../matita/docs/manual/tac_assumption.html | 2 +- helm/www/matita/docs/manual/tac_auto.html | 2 +- helm/www/matita/docs/manual/tac_change.html | 2 +- helm/www/matita/docs/manual/tac_clear.html | 2 +- .../www/matita/docs/manual/tac_clearbody.html | 2 +- .../matita/docs/manual/tac_constructor.html | 2 +- .../matita/docs/manual/tac_contradiction.html | 2 +- helm/www/matita/docs/manual/tac_cut.html | 2 +- .../www/matita/docs/manual/tac_decompose.html | 2 +- .../matita/docs/manual/tac_discriminate.html | 2 +- helm/www/matita/docs/manual/tac_elim.html | 2 +- helm/www/matita/docs/manual/tac_elimType.html | 2 +- helm/www/matita/docs/manual/tac_exact.html | 2 +- helm/www/matita/docs/manual/tac_exists.html | 2 +- helm/www/matita/docs/manual/tac_fail.html | 2 +- helm/www/matita/docs/manual/tac_fold.html | 2 +- helm/www/matita/docs/manual/tac_fourier.html | 2 +- helm/www/matita/docs/manual/tac_fwd.html | 2 +- .../matita/docs/manual/tac_generalize.html | 2 +- helm/www/matita/docs/manual/tac_id.html | 2 +- .../www/matita/docs/manual/tac_injection.html | 2 +- helm/www/matita/docs/manual/tac_intro.html | 2 +- helm/www/matita/docs/manual/tac_intros.html | 2 +- .../www/matita/docs/manual/tac_inversion.html | 2 +- helm/www/matita/docs/manual/tac_lapply.html | 2 +- helm/www/matita/docs/manual/tac_left.html | 2 +- helm/www/matita/docs/manual/tac_letin.html | 2 +- .../www/matita/docs/manual/tac_normalize.html | 2 +- .../docs/manual/tac_paramodulation.html | 2 +- helm/www/matita/docs/manual/tac_reduce.html | 2 +- .../matita/docs/manual/tac_reflexivity.html | 2 +- helm/www/matita/docs/manual/tac_replace.html | 2 +- helm/www/matita/docs/manual/tac_rewrite.html | 2 +- helm/www/matita/docs/manual/tac_right.html | 2 +- helm/www/matita/docs/manual/tac_ring.html | 2 +- helm/www/matita/docs/manual/tac_simplify.html | 2 +- helm/www/matita/docs/manual/tac_split.html | 2 +- helm/www/matita/docs/manual/tac_symmetry.html | 2 +- .../matita/docs/manual/tac_transitivity.html | 2 +- helm/www/matita/docs/manual/tac_unfold.html | 2 +- helm/www/matita/docs/manual/tac_whd.html | 2 +- 58 files changed, 138 insertions(+), 110 deletions(-) create mode 100644 helm/www/matita/docs/manual/docbook.css diff --git a/helm/www/matita/docs/manual/WrtCoq.html b/helm/www/matita/docs/manual/WrtCoq.html index e365ebb4a..c72e87572 100644 --- a/helm/www/matita/docs/manual/WrtCoq.html +++ b/helm/www/matita/docs/manual/WrtCoq.html @@ -1,6 +1,6 @@ -Matita vs Coq
Matita vs Coq
Prev Chapter 1. Introduction Next

Matita vs Coq

+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, diff --git a/helm/www/matita/docs/manual/authoring.html b/helm/www/matita/docs/manual/authoring.html index 6219d1fa4..bb4cab4b4 100644 --- a/helm/www/matita/docs/manual/authoring.html +++ b/helm/www/matita/docs/manual/authoring.html @@ -1,6 +1,6 @@ -Authoring

Authoring
Prev Chapter 3. Getting started Next

Authoring

How to use developments

+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 @@ -14,9 +14,9 @@

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.

+

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] + 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" @@ -52,7 +52,7 @@

Close

Closes the Developments window

-


[1] +


[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 diff --git a/helm/www/matita/docs/manual/axiom_definition_declaration.html b/helm/www/matita/docs/manual/axiom_definition_declaration.html index ab327f1bf..dd632607c 100644 --- a/helm/www/matita/docs/manual/axiom_definition_declaration.html +++ b/helm/www/matita/docs/manual/axiom_definition_declaration.html @@ -1,6 +1,6 @@ -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; +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 diff --git a/helm/www/matita/docs/manual/cicbrowser.html b/helm/www/matita/docs/manual/cicbrowser.html index 881b720b2..68ea22383 100644 --- a/helm/www/matita/docs/manual/cicbrowser.html +++ b/helm/www/matita/docs/manual/cicbrowser.html @@ -1,6 +1,6 @@ -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. +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 diff --git a/helm/www/matita/docs/manual/docbook.css b/helm/www/matita/docs/manual/docbook.css new file mode 100644 index 000000000..0c92e77c9 --- /dev/null +++ b/helm/www/matita/docs/manual/docbook.css @@ -0,0 +1,51 @@ + +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 index 46e5f05cd..0cf3d98f6 100644 --- a/helm/www/matita/docs/manual/index.html +++ b/helm/www/matita/docs/manual/index.html @@ -1,32 +1,9 @@ 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
+ User Manual (rev. 1α)
Matita V0.1.0 + User Manual (rev. 1α)
   Next

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

Copyright © 2006 The HELM team.

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

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 index 45f9c1f9b..19cecf7b8 100644 --- a/helm/www/matita/docs/manual/proofs.html +++ b/helm/www/matita/docs/manual/proofs.html @@ -1,6 +1,6 @@ -Proofs
Proofs
Prev Chapter 4. Syntax Next

Proofs

theorem id[: term] [≝ term]

theorem f: P ≝ p

Proves a new theorem f whose thesis is +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. diff --git a/helm/www/matita/docs/manual/sec_commands.html b/helm/www/matita/docs/manual/sec_commands.html index 86c388c58..786d496b3 100644 --- a/helm/www/matita/docs/manual/sec_commands.html +++ b/helm/www/matita/docs/manual/sec_commands.html @@ -1,5 +1,5 @@ -Chapter 8. Other commands

Chapter 8. Other commands
Prev   Next

Chapter 8. Other commands

Table of Contents

Introduction

Introduction

+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 index 26df16cec..66eaac015 100644 --- a/helm/www/matita/docs/manual/sec_gettingstarted.html +++ b/helm/www/matita/docs/manual/sec_gettingstarted.html @@ -1,6 +1,6 @@ -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 +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 diff --git a/helm/www/matita/docs/manual/sec_install.html b/helm/www/matita/docs/manual/sec_install.html index 6eb21eb3a..ee9361051 100644 --- a/helm/www/matita/docs/manual/sec_install.html +++ b/helm/www/matita/docs/manual/sec_install.html @@ -1,6 +1,6 @@ -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 +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 @@ -103,7 +103,7 @@ parameters. They are listed in the table below, together with their default values. -

    Table 2.1.  configure command line +

    Table 2.1.  configure command line arguments

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

    Runtime base directory where all Matita stuff diff --git a/helm/www/matita/docs/manual/sec_intro.html b/helm/www/matita/docs/manual/sec_intro.html index a7f5cb375..47bfd2de1 100644 --- a/helm/www/matita/docs/manual/sec_intro.html +++ b/helm/www/matita/docs/manual/sec_intro.html @@ -1,7 +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 +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
      + User Manual (rev. 1α) 
    		Home Matita vs Coq
    diff --git a/helm/www/matita/docs/manual/sec_license.html b/helm/www/matita/docs/manual/sec_license.html index 7bcc0d633..c930a136a 100644 --- a/helm/www/matita/docs/manual/sec_license.html +++ b/helm/www/matita/docs/manual/sec_license.html @@ -1,14 +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 
    +Chapter 9. License
    Chapter 9. License
    Prev   

    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.

    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 index 12468ccea..269c1119f 100644 --- a/helm/www/matita/docs/manual/sec_tacticals.html +++ b/helm/www/matita/docs/manual/sec_tacticals.html @@ -1,5 +1,5 @@ -Chapter 7. Tacticals
    Chapter 7. Tacticals
    Prev   Next

    Chapter 7. Tacticals

    Table of Contents

    Introduction

    Introduction

    +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 index 81b8e6ee7..ae7e166ba 100644 --- a/helm/www/matita/docs/manual/sec_tactics.html +++ b/helm/www/matita/docs/manual/sec_tactics.html @@ -1,6 +1,6 @@ -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

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

    diff --git a/helm/www/matita/docs/manual/sec_terms.html b/helm/www/matita/docs/manual/sec_terms.html index 2d7469668..9bd09915a 100644 --- a/helm/www/matita/docs/manual/sec_terms.html +++ b/helm/www/matita/docs/manual/sec_terms.html @@ -1,17 +1,17 @@ -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 +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〉〉 

      +

      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 +

      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] @@ -25,7 +25,7 @@ in term  
       |…user provided notation

      -

      Table 4.5. Simple terms

      sterm::=(term) 
       |id[\subst[ +

      Table 4.5. Simple terms

      sterm::=(term) 
       |id[\subst[ id≔term [;id≔term]… ]] @@ -44,13 +44,13 @@ match_pattern ⇒ term ]…]  
       |(term:term)cast
       |…user provided notation at precedence 90

      -

      Table 4.6. Arguments

      args::= +

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

      +

      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 index 215602b19..db6c34afd 100644 --- a/helm/www/matita/docs/manual/sec_usernotation.html +++ b/helm/www/matita/docs/manual/sec_usernotation.html @@ -1,5 +1,5 @@ -Chapter 5. Extending the syntax
      Chapter 5. Extending the syntax
      Prev   Next

      Chapter 5. Extending the syntax

      Table of Contents

      Introduction

      Introduction

      +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 index 9518c40d7..ab85e3471 100644 --- a/helm/www/matita/docs/manual/tac_apply.html +++ b/helm/www/matita/docs/manual/tac_apply.html @@ -1,6 +1,6 @@ -apply sterm
      apply sterm
      Prev Chapter 6. Tactics Next

      apply sterm

      apply t

      +apply sterm

      apply sterm
      Prev Chapter 6. Tactics Next

      apply sterm

      apply t

      Pre-conditions:

      t must have type T1 → ... → Tn → G diff --git a/helm/www/matita/docs/manual/tac_assumption.html b/helm/www/matita/docs/manual/tac_assumption.html index 63a4a0798..6dd35ee36 100644 --- a/helm/www/matita/docs/manual/tac_assumption.html +++ b/helm/www/matita/docs/manual/tac_assumption.html @@ -1,6 +1,6 @@ -assumption

      assumption
      Prev Chapter 6. Tactics Next

      assumption

      assumption

      +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 index eb67e6dca..31b733a64 100644 --- a/helm/www/matita/docs/manual/tac_auto.html +++ b/helm/www/matita/docs/manual/tac_auto.html @@ -1,6 +1,6 @@ -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

      +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. diff --git a/helm/www/matita/docs/manual/tac_change.html b/helm/www/matita/docs/manual/tac_change.html index 82c07ced8..074ffa5b6 100644 --- a/helm/www/matita/docs/manual/tac_change.html +++ b/helm/www/matita/docs/manual/tac_change.html @@ -1,6 +1,6 @@ -change <pattern> with sterm

      change <pattern> with sterm
      Prev Chapter 6. Tactics Next

      change <pattern> with sterm

      change patt with t

      +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 diff --git a/helm/www/matita/docs/manual/tac_clear.html b/helm/www/matita/docs/manual/tac_clear.html index 31d632ca8..8bdfc8f57 100644 --- a/helm/www/matita/docs/manual/tac_clear.html +++ b/helm/www/matita/docs/manual/tac_clear.html @@ -1,6 +1,6 @@ -clear id

      clear id
      Prev Chapter 6. Tactics Next

      clear id

      clear H

      +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

      diff --git a/helm/www/matita/docs/manual/tac_clearbody.html b/helm/www/matita/docs/manual/tac_clearbody.html index 678b62f12..8bc46403b 100644 --- a/helm/www/matita/docs/manual/tac_clearbody.html +++ b/helm/www/matita/docs/manual/tac_clearbody.html @@ -1,6 +1,6 @@ -clearbody id

      clearbody id
      Prev Chapter 6. Tactics Next

      clearbody id

      clearbody H

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

      diff --git a/helm/www/matita/docs/manual/tac_constructor.html b/helm/www/matita/docs/manual/tac_constructor.html index 4679c535d..9fc2a8b25 100644 --- a/helm/www/matita/docs/manual/tac_constructor.html +++ b/helm/www/matita/docs/manual/tac_constructor.html @@ -1,6 +1,6 @@ -constructor nat

      constructor nat
      Prev Chapter 6. Tactics Next

      constructor nat

      constructor n

      +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 diff --git a/helm/www/matita/docs/manual/tac_contradiction.html b/helm/www/matita/docs/manual/tac_contradiction.html index 2fe4c21d0..66a4e4c4d 100644 --- a/helm/www/matita/docs/manual/tac_contradiction.html +++ b/helm/www/matita/docs/manual/tac_contradiction.html @@ -1,6 +1,6 @@ -contradiction

      contradiction
      Prev Chapter 6. Tactics Next

      contradiction

      contradiction

      +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

      diff --git a/helm/www/matita/docs/manual/tac_cut.html b/helm/www/matita/docs/manual/tac_cut.html index fa956c441..dd9550209 100644 --- a/helm/www/matita/docs/manual/tac_cut.html +++ b/helm/www/matita/docs/manual/tac_cut.html @@ -1,6 +1,6 @@ -cut sterm [as id]

      cut sterm [as id]
      Prev Chapter 6. Tactics Next

      cut sterm [as id]

      cut P as H

      +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. diff --git a/helm/www/matita/docs/manual/tac_decompose.html b/helm/www/matita/docs/manual/tac_decompose.html index 2fabae2e8..d299feb29 100644 --- a/helm/www/matita/docs/manual/tac_decompose.html +++ b/helm/www/matita/docs/manual/tac_decompose.html @@ -1,5 +1,5 @@ -decompose id [id]… [<intros_spec>]

      decompose id [id]… [<intros_spec>]
      Prev Chapter 6. Tactics Next

      decompose id [id]… [<intros_spec>]

      decompose ???

      +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 index 34f6c6aaa..06c9c8333 100644 --- a/helm/www/matita/docs/manual/tac_discriminate.html +++ b/helm/www/matita/docs/manual/tac_discriminate.html @@ -1,6 +1,6 @@ -discriminate sterm
      discriminate sterm
      Prev Chapter 6. Tactics Next

      discriminate sterm

      discriminate p

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

      diff --git a/helm/www/matita/docs/manual/tac_elim.html b/helm/www/matita/docs/manual/tac_elim.html index 22ad67bf9..8638f4442 100644 --- a/helm/www/matita/docs/manual/tac_elim.html +++ b/helm/www/matita/docs/manual/tac_elim.html @@ -1,6 +1,6 @@ -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

      +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 diff --git a/helm/www/matita/docs/manual/tac_elimType.html b/helm/www/matita/docs/manual/tac_elimType.html index 0381aeea4..95be78578 100644 --- a/helm/www/matita/docs/manual/tac_elimType.html +++ b/helm/www/matita/docs/manual/tac_elimType.html @@ -1,5 +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

      +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 index b7e7d7e8c..37a49619d 100644 --- a/helm/www/matita/docs/manual/tac_exact.html +++ b/helm/www/matita/docs/manual/tac_exact.html @@ -1,6 +1,6 @@ -exact sterm
      exact sterm
      Prev Chapter 6. Tactics Next

      exact sterm

      exact p

      +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 index 7b977fbf6..99d1bad19 100644 --- a/helm/www/matita/docs/manual/tac_exists.html +++ b/helm/www/matita/docs/manual/tac_exists.html @@ -1,6 +1,6 @@ -exists
      exists
      Prev Chapter 6. Tactics Next

      exists

      exists

      +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 diff --git a/helm/www/matita/docs/manual/tac_fail.html b/helm/www/matita/docs/manual/tac_fail.html index 62f634fa5..fefd9fbf3 100644 --- a/helm/www/matita/docs/manual/tac_fail.html +++ b/helm/www/matita/docs/manual/tac_fail.html @@ -1,5 +1,5 @@ -fail

      fail
      Prev Chapter 6. Tactics Next

      fail

      fail

      +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 index e408787e0..35e8b50dc 100644 --- a/helm/www/matita/docs/manual/tac_fold.html +++ b/helm/www/matita/docs/manual/tac_fold.html @@ -1,6 +1,6 @@ -fold <reduction_kind> sterm <pattern>
      fold <reduction_kind> sterm <pattern>
      Prev Chapter 6. Tactics Next

      fold <reduction_kind> sterm <pattern>

      fold red t patt

      +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 diff --git a/helm/www/matita/docs/manual/tac_fourier.html b/helm/www/matita/docs/manual/tac_fourier.html index 10f29a1e2..506295b46 100644 --- a/helm/www/matita/docs/manual/tac_fourier.html +++ b/helm/www/matita/docs/manual/tac_fourier.html @@ -1,6 +1,6 @@ -fourier

      fourier
      Prev Chapter 6. Tactics Next

      fourier

      fourier

      +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 diff --git a/helm/www/matita/docs/manual/tac_fwd.html b/helm/www/matita/docs/manual/tac_fwd.html index 6f99a1e19..ccd4dc55f 100644 --- a/helm/www/matita/docs/manual/tac_fwd.html +++ b/helm/www/matita/docs/manual/tac_fwd.html @@ -1,5 +1,5 @@ -fwd id [<ident list>]

      fwd id [<ident list>]
      Prev Chapter 6. Tactics Next

      fwd id [<ident list>]

      fwd ...TODO

      +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 index 8e03a551f..bcba8c3f9 100644 --- a/helm/www/matita/docs/manual/tac_generalize.html +++ b/helm/www/matita/docs/manual/tac_generalize.html @@ -1,6 +1,6 @@ -generalize <pattern> [as id]
      generalize <pattern> [as id]
      Prev Chapter 6. Tactics Next

      generalize <pattern> [as id]

      generalize patt as H

      +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 diff --git a/helm/www/matita/docs/manual/tac_id.html b/helm/www/matita/docs/manual/tac_id.html index bef48017b..f01158f6e 100644 --- a/helm/www/matita/docs/manual/tac_id.html +++ b/helm/www/matita/docs/manual/tac_id.html @@ -1,5 +1,5 @@ -id

      id
      Prev Chapter 6. Tactics Next

      id

      id

      +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 index f6a4b2676..143c3a293 100644 --- a/helm/www/matita/docs/manual/tac_injection.html +++ b/helm/www/matita/docs/manual/tac_injection.html @@ -1,6 +1,6 @@ -injection sterm
      injection sterm
      Prev Chapter 6. Tactics Next

      injection sterm

      injection p

      +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 diff --git a/helm/www/matita/docs/manual/tac_intro.html b/helm/www/matita/docs/manual/tac_intro.html index 6361dd079..f99fdb346 100644 --- a/helm/www/matita/docs/manual/tac_intro.html +++ b/helm/www/matita/docs/manual/tac_intro.html @@ -1,6 +1,6 @@ -intro [id]

      intro [id]
      Prev Chapter 6. Tactics Next

      intro [id]

      intro H

      +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 diff --git a/helm/www/matita/docs/manual/tac_intros.html b/helm/www/matita/docs/manual/tac_intros.html index 2732fc853..98683d76e 100644 --- a/helm/www/matita/docs/manual/tac_intros.html +++ b/helm/www/matita/docs/manual/tac_intros.html @@ -1,6 +1,6 @@ -intros <intros_spec>

      intros <intros_spec>
      Prev Chapter 6. Tactics Next

      intros <intros_spec>

      intros hyps

      +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 diff --git a/helm/www/matita/docs/manual/tac_inversion.html b/helm/www/matita/docs/manual/tac_inversion.html index ea424be3e..ab2e5c36c 100644 --- a/helm/www/matita/docs/manual/tac_inversion.html +++ b/helm/www/matita/docs/manual/tac_inversion.html @@ -1,6 +1,6 @@ -inversion sterm

      inversion sterm
      Prev Chapter 6. Tactics Next

      inversion sterm

      inversion t

      +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" diff --git a/helm/www/matita/docs/manual/tac_lapply.html b/helm/www/matita/docs/manual/tac_lapply.html index 6784e7679..8684738db 100644 --- a/helm/www/matita/docs/manual/tac_lapply.html +++ b/helm/www/matita/docs/manual/tac_lapply.html @@ -1,5 +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 ???

      +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 index 65298b52f..623ced5f2 100644 --- a/helm/www/matita/docs/manual/tac_left.html +++ b/helm/www/matita/docs/manual/tac_left.html @@ -1,6 +1,6 @@ -left
      left
      Prev Chapter 6. Tactics Next

      left

      left

      +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 diff --git a/helm/www/matita/docs/manual/tac_letin.html b/helm/www/matita/docs/manual/tac_letin.html index 97b285b3b..83318bdb5 100644 --- a/helm/www/matita/docs/manual/tac_letin.html +++ b/helm/www/matita/docs/manual/tac_letin.html @@ -1,6 +1,6 @@ -letin id ≝ sterm

      letin id ≝ sterm
      Prev Chapter 6. Tactics Next

      letin id ≝ sterm

      letin x ≝ t

      +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 index f4a60120b..4d1364cef 100644 --- a/helm/www/matita/docs/manual/tac_normalize.html +++ b/helm/www/matita/docs/manual/tac_normalize.html @@ -1,6 +1,6 @@ -normalize <pattern>
      normalize <pattern>
      Prev Chapter 6. Tactics Next

      normalize <pattern>

      normalize patt

      +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 index 7a0973326..b93cad741 100644 --- a/helm/www/matita/docs/manual/tac_paramodulation.html +++ b/helm/www/matita/docs/manual/tac_paramodulation.html @@ -1,5 +1,5 @@ -paramodulation <pattern>
      paramodulation <pattern>
      Prev Chapter 6. Tactics Next

      paramodulation <pattern>

      paramodulation patt

      +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 index 309681c9e..94120657d 100644 --- a/helm/www/matita/docs/manual/tac_reduce.html +++ b/helm/www/matita/docs/manual/tac_reduce.html @@ -1,6 +1,6 @@ -reduce <pattern>
      reduce <pattern>
      Prev Chapter 6. Tactics Next

      reduce <pattern>

      reduce patt

      +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 index 1afd09b38..bbd9e3e32 100644 --- a/helm/www/matita/docs/manual/tac_reflexivity.html +++ b/helm/www/matita/docs/manual/tac_reflexivity.html @@ -1,6 +1,6 @@ -reflexivity
      reflexivity
      Prev Chapter 6. Tactics Next

      reflexivity

      reflexivity

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

      diff --git a/helm/www/matita/docs/manual/tac_replace.html b/helm/www/matita/docs/manual/tac_replace.html index d7134f590..48bdcfc4c 100644 --- a/helm/www/matita/docs/manual/tac_replace.html +++ b/helm/www/matita/docs/manual/tac_replace.html @@ -1,6 +1,6 @@ -replace <pattern> with sterm

      replace <pattern> with sterm
      Prev Chapter 6. Tactics Next

      replace <pattern> with sterm

      change patt with t

      +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 diff --git a/helm/www/matita/docs/manual/tac_rewrite.html b/helm/www/matita/docs/manual/tac_rewrite.html index 21155e6d9..99185ab02 100644 --- a/helm/www/matita/docs/manual/tac_rewrite.html +++ b/helm/www/matita/docs/manual/tac_rewrite.html @@ -1,6 +1,6 @@ -rewrite [<|>] sterm <pattern>

      rewrite [<|>] sterm <pattern>
      Prev Chapter 6. Tactics Next

      rewrite [<|>] sterm <pattern>

      rewrite dir p patt

      +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 diff --git a/helm/www/matita/docs/manual/tac_right.html b/helm/www/matita/docs/manual/tac_right.html index 2874f0b37..25fea3b6a 100644 --- a/helm/www/matita/docs/manual/tac_right.html +++ b/helm/www/matita/docs/manual/tac_right.html @@ -1,6 +1,6 @@ -right

      right
      Prev Chapter 6. Tactics Next

      right

      right

      +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 diff --git a/helm/www/matita/docs/manual/tac_ring.html b/helm/www/matita/docs/manual/tac_ring.html index 798602f85..64c63ed22 100644 --- a/helm/www/matita/docs/manual/tac_ring.html +++ b/helm/www/matita/docs/manual/tac_ring.html @@ -1,6 +1,6 @@ -ring

      ring
      Prev Chapter 6. Tactics Next

      ring

      ring

      +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 diff --git a/helm/www/matita/docs/manual/tac_simplify.html b/helm/www/matita/docs/manual/tac_simplify.html index 3ed94a32c..a04a93994 100644 --- a/helm/www/matita/docs/manual/tac_simplify.html +++ b/helm/www/matita/docs/manual/tac_simplify.html @@ -1,6 +1,6 @@ -simplify <pattern>

      simplify <pattern>
      Prev Chapter 6. Tactics Next

      simplify <pattern>

      simplify patt

      +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 index 52872dc7e..00ffcd154 100644 --- a/helm/www/matita/docs/manual/tac_split.html +++ b/helm/www/matita/docs/manual/tac_split.html @@ -1,6 +1,6 @@ -split
      split
      Prev Chapter 6. Tactics Next

      split

      split

      +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 diff --git a/helm/www/matita/docs/manual/tac_symmetry.html b/helm/www/matita/docs/manual/tac_symmetry.html index 0f544da10..9bb5e00bd 100644 --- a/helm/www/matita/docs/manual/tac_symmetry.html +++ b/helm/www/matita/docs/manual/tac_symmetry.html @@ -1,6 +1,6 @@ -symmetry

      symmetry
      Prev Chapter 6. Tactics Next

      symmetry

      The tactic symmetry

      symmetry

      +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 index 0db99505c..c7f26a277 100644 --- a/helm/www/matita/docs/manual/tac_transitivity.html +++ b/helm/www/matita/docs/manual/tac_transitivity.html @@ -1,6 +1,6 @@ -transitivity sterm
      transitivity sterm
      Prev Chapter 6. Tactics Next

      transitivity sterm

      transitivity t

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

      diff --git a/helm/www/matita/docs/manual/tac_unfold.html b/helm/www/matita/docs/manual/tac_unfold.html index 120ce67d3..0f23f268e 100644 --- a/helm/www/matita/docs/manual/tac_unfold.html +++ b/helm/www/matita/docs/manual/tac_unfold.html @@ -1,6 +1,6 @@ -unfold [sterm] <pattern>

      unfold [sterm] <pattern>
      Prev Chapter 6. Tactics Next

      unfold [sterm] <pattern>

      unfold t patt

      +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, diff --git a/helm/www/matita/docs/manual/tac_whd.html b/helm/www/matita/docs/manual/tac_whd.html index 636ff383a..25190ce3e 100644 --- a/helm/www/matita/docs/manual/tac_whd.html +++ b/helm/www/matita/docs/manual/tac_whd.html @@ -1,6 +1,6 @@ -whd <pattern>

      whd <pattern>
      Prev Chapter 6. Tactics Next

      whd <pattern>

      whd patt

      +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