0.5.9 released

[helm.git] / helm / www / matita / docs / manual-0.5.9 / matita.txt

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

Andrea Asperti

    <asperti@cs.unibo.it>

Claudio Sacerdoti Coen

    <sacerdot@cs.unibo.it>

Ferruccio Guidi

    <fguidi@cs.unibo.it>

Enrico Tassi

    <tassi@cs.unibo.it>

Stefano Zacchiroli

    <zacchiro@cs.unibo.it>

   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 for more information.
     _________________________________________________________

   Table of Contents
   1. Introduction

        1.1. Features
        1.2. Matita vs Coq

   2. Installation

        2.1. Installing from sources

              2.1.1. Getting the source code
              2.1.2. Requirements
              2.1.3. Database setup
              2.1.4. Compiling and installing

        2.2. Configuring Matita

   3. Getting started

        3.1. How to type Unicode symbols
        3.2. Browsing and searching

              3.2.1. Browsing the library
              3.2.2. Looking at a proof under development
              3.2.3. Searching the library

        3.3. Authoring

              3.3.1. How to use developments
              3.3.2. The authoring interface

   4. Syntax

        4.1. Terms & co.

              4.1.1. Lexical conventions
              4.1.2. Terms

        4.2. Definitions and declarations

              4.2.1. axiom id: term
              4.2.2. definition id[: term] [â term]
              4.2.3. [inductive|coinductive] id [args2]⦠: term
                      â [|] [id:term] [| id:term]⦠[with id :
                      term â [|] [id:term] [| id:term]â¦]â¦

              4.2.4. record id [args2]⦠: term â{[id [:|:>]
                      term] [;id [:|:>] term]â¦}

        4.3. Proofs

              4.3.1. theorem id[: term] [â term]
              4.3.2. variant id: term â term
              4.3.3. lemma id[: term] [â term]
              4.3.4. fact id[: term] [â term]
              4.3.5. remark id[: term] [â term]

        4.4. Tactic arguments

              4.4.1. intros-spec
              4.4.2. pattern
              4.4.3. reduction-kind
              4.4.4. auto-params

   5. Extending the syntax

        5.1. Introduction

   6. Tacticals

        6.1. Interactive proofs and definitions
        6.2. The proof status
        6.3. Tacticals

   7. Tactics

        7.1. Quick reference card
        7.2. absurd
        7.3. apply
        7.4. applyS
        7.5. assumption
        7.6. auto
        7.7. clear
        7.8. clearbody
        7.9. change
        7.10. constructor
        7.11. contradiction
        7.12. cut
        7.13. decompose
        7.14. demodulate
        7.15. destruct
        7.16. elim
        7.17. elimType
        7.18. exact
        7.19. exists
        7.20. fail
        7.21. fold
        7.22. fourier
        7.23. fwd
        7.24. generalize
        7.25. id
        7.26. intro
        7.27. intros
        7.28. inversion
        7.29. lapply
        7.30. left
        7.31. letin
        7.32. normalize
        7.33. reduce
        7.34. reflexivity
        7.35. replace
        7.36. rewrite
        7.37. right
        7.38. ring
        7.39. simplify
        7.40. split
        7.41. subst
        7.42. symmetry
        7.43. transitivity
        7.44. unfold
        7.45. whd

   8. Other commands

        8.1. alias
        8.2. check
        8.3. coercion
        8.4. default
        8.5. hint
        8.6. include
        8.7. include' "s"
        8.8. set
        8.9. whelp
        8.10. qed

   9. License

   List of Tables
   4-1. qstring
   4-2. id
   4-3. nat
   4-4. char
   4-5. uri-step
   4-6. uri
   4-7. Terms
   4-8. Simple terms
   4-9. Arguments
   4-10. Pattern matching
   4-11. intros-spec
   4-12. pattern
   4-13. path
   4-14. reduction-kind
   4-15. reduction-kind
   6-1. proof script
   6-2. proof steps
   6-3. tactics and LCF tacticals
   7-1. tactics
   8-1. clusters

   List of Figures
   3-1. The Developments window
     _________________________________________________________

Chapter 1. Introduction

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

1.2. 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.
     _________________________________________________________

Chapter 2. Installation

2.1. Installing from sources

   Currently, the only intended way to install Matita is starting
   from its source code.
     _________________________________________________________

2.1.1. 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.
     _________________________________________________________

2.1.2. Requirements

   In order to build Matita from sources you will need some tools
   and libraries. They are listed below.

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

2.1.3. 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.
     _________________________________________________________

2.1.4. Compiling and installing

   Once you get the source code the installations steps should be
   quite familiar.

   First of all you need to configure the build process executing
   ./configure. This will check that all needed tools and library
   are installed and prepare the sources for compilation and
   installation.

   Quite a few (optional) arguments may be passed to the
   configure command line to change build time parameters. They
   are listed below, together with their default values:

   configure command line arguments

   --with-runtime-dir=dir
          (Default: /usr/local/matita) Runtime base directory
          where all Matita stuff (executables, configuration
          files, standard library, ...) will be installed

   --with-dbhost=host
          (Default: localhost) Default SQL server hostname. Will
          be used while building the standard library during the
          installation and to create the default Matita
          configuration. May be changed later in configuration
          file.

   --enable-debug
          (Default: disabled) Enable debugging code. Not for the
          casual user.

   Then you will manage the build and install process using make
   as usual. Below are reported the targets you have to invoke in
   sequence to build and install:

   make targets

   world
          builds components needed by Matita and Matita itself
          (in bytecode or native code depending on the
          availability of the OCaml native code compiler)

   install
          installs Matita related tools, standard library and the
          needed runtime stuff in the proper places on the
          filesystem.

          As a part of the installation process the Matita
          standard library will be compiled, thus testing that
          the just built matitac compiler works properly.

          For this step you will need a working SQL database (for
          indexing the standard library while you are compiling
          it). See Database setup for instructions on how to set
          it up.
     _________________________________________________________

2.2. Configuring Matita

   The file matita.conf.xml... TODO
     _________________________________________________________

Chapter 3. Getting started

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

3.1. 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 "â").
     _________________________________________________________

3.2. 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.
     _________________________________________________________

3.2.1. 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.
     _________________________________________________________

3.2.2. 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".
     _________________________________________________________

3.2.3. 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.
     _________________________________________________________

3.2.3.1. Searching by name

   TODO
     _________________________________________________________

3.2.3.2. List of lemmas that can be applied

   TODO
     _________________________________________________________

3.2.3.3. Searching by exact match

   TODO
     _________________________________________________________

3.2.3.4. List of elimination principles for a given type

   TODO
     _________________________________________________________

3.2.3.5. Searching by instantiation

   TODO
     _________________________________________________________

3.3. Authoring

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

   [developments.png]

   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
     _________________________________________________________

3.3.2. The authoring interface

   TODO
     _________________________________________________________

Chapter 4. Syntax

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

    1. Non terminal symbols are emphasized and have a link to
       their definition. E.g.: term
    2. Terminal symbols are in bold. E.g.: theorem
    3. Optional sequences of elements are put in square brackets.
       E.g.: [in term]
    4. Alternatives are put in square brakets and they are
       separated by vertical bars. E.g.: [<|>]
    5. Repetitions of a sequence of elements are given by putting
       the sequence in square brackets, that are followed by
       three dots. The empty sequence is a valid repetition.
       E.g.: [and term]â¦
    6. Characters belonging to a set of characters are given by
       listing the set elements in square brackets. Hyphens are
       used to specify ranges of characters in the set. E.g.:
       [a-zA-Z0-9_-]
     _________________________________________________________

4.1. Terms & co.

4.1.1. Lexical conventions

   Table 4-1. qstring
   qstring ::= "â©â©any sequence of characters excluded "âªâª"

   Table 4-2. id
   id ::= â©â©any sequence of letters, underscores or valid XML
   digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by
   a possible empty sequence of decorators ([?'`])âªâª

   Table 4-3. nat
   nat ::= â©â©any sequence of valid XML digitsâªâª

   Table 4-4. char
   char ::= [a-zA-Z0-9_-]

   Table 4-5. uri-step
   uri-step ::= char[char]â¦

   Table 4-6. uri
                 uri ::=
   [cic:/|theory:/]uri-step[/uri-step]â¦.id[.id]â¦[#xpointer(nat/
   nat[/nat]â¦)]
     _________________________________________________________

4.1.2. Terms

   Table 4-7. Terms
   term ::= sterm simple or delimited term
     | term term application
     | λargs.term λ-abstraction
     | Î args.term dependent product meant to define a datatype
     | âargs.term dependent product meant to define a proposition
     | term â term non-dependent product (logical implication or
   function space)
     | let [id|(id: term)] â term in term local definition
     | let [co]rec rec_def (co)recursive definitions
       [and rec_def]â¦
       in term
     | ⦠user provided notation
   rec_def ::= id [id|(id[,term]⦠:term)]â¦
       [on id] [: term] â term]

   Table 4-8. Simple terms
   sterm ::= (term)
     | id[\subst[ idâterm [;idâterm]⦠]] identifier with
   optional explicit named substitution
     | uri a qualified reference
     | Prop the impredicative sort of propositions
     | Set the impredicate sort of datatypes
     | CProp one fixed predicative sort of constructive
   propositions
     | Type one predicative sort of datatypes
     | ? implicit argument
     | ?n [[ [_|term]⦠]] metavariable
     | match term [ in term ] [ return term ] with case analysis
       [ match_branch[|match_branch]⦠]
     | (term:term) cast
     | ⦠user provided notation at precedence 90

   Table 4-9. Arguments
   args  ::= _[: term]           ignored argument
         |   (_[: term])         ignored argument
         |   id[,id]â¦[: term]  
         |   (id[,id]â¦[: term])
   args2 ::= id                 
         |   (id[,id]â¦: term)  

   Table 4-10. Pattern matching
   match_branch ::= match_pattern â term
   match_pattern ::= id 0-ary constructor
     | (id id [id]â¦) n-ary constructor (binds the n arguments)
     _________________________________________________________

4.2. Definitions and declarations

4.2.1. axiom id: term

   axiom H: P

   H is declared as an axiom that states P
     _________________________________________________________

4.2.2. 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.
     _________________________________________________________

4.2.3. [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.
     _________________________________________________________

4.2.4. 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.
     _________________________________________________________

4.3. Proofs

4.3.1. 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.
     _________________________________________________________

4.3.2. 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.
     _________________________________________________________

4.3.3. lemma id[: term] [â term]

   lemma f: T â t

   Same as theorem f: T â t
     _________________________________________________________

4.3.4. fact id[: term] [â term]

   fact f: T â t

   Same as theorem f: T â t
     _________________________________________________________

4.3.5. remark id[: term] [â term]

   remark f: T â t

   Same as theorem f: T â t
     _________________________________________________________

4.4. Tactic arguments

   This section documents the syntax of some recurring arguments
   for tactics.
     _________________________________________________________

4.4.1. intros-spec

   Table 4-11. intros-spec
   intros-spec ::= [nat] [([id]â¦)]

   The natural number is the number of new hypotheses to be
   introduced. The list of identifiers gives the name for the
   first hypotheses.
     _________________________________________________________

4.4.2. pattern

   Table 4-12. pattern
 pattern ::= in [id[: path]]⦠[⢠path]]                simple pattern
         |   in match term [in [id[: path]]⦠[⢠path]] full pattern

   Table 4-13. path
   path ::= â©â©any sterm whithout occurrences of Set, Prop,
   CProp, Type, id, uri and user provided notation; however, % is
   now an additional production for stermâªâª

   A path locates zero or more subterms of a given term by
   mimicking the term structure up to:

    1. Occurrences of the subterms to locate that are represented
       by %.
    2. Subterms without any occurrence of subterms to locate that
       can be represented by ?.

   For instance, the path â_,_:?.(? ? % ?)â(? ? ? %) locates at
   once the subterms x+y and x*y in the term âx,y:nat.x+y=1â0=x*y
   (where the notation A=B hides the term (eq T A B) for some
   type T).

   A simple pattern extends paths to locate subterms in a whole
   sequent. In particular, the pattern in H: p K: q ⢠r locates
   at once all the subterms located by the pattern r in the
   conclusion of the sequent and by the patterns p and q in the
   hypotheses H and K of the sequent.

   If no list of hypotheses is provided in a simple pattern, no
   subterm is selected in the hypothesis. If the ⢠p part of the
   pattern is not provided, no subterm will be matched in the
   conclusion if at least one hypothesis is provided; otherwise
   the whole conclusion is selected.

   Finally, a full pattern is interpreted in three steps. In the
   first step the match T in part is ignored and a set S of
   subterms is located as for the case of simple patterns. In the
   second step the term T is parsed and interpreted in the
   context of each subterm s â S. In the last term for each s â S
   the interpreted term T computed in the previous step is looked
   for. The final set of subterms located by the full pattern is
   the set of occurrences of the interpreted T in the subterms s.

   A full pattern can always be replaced by a simple pattern,
   often at the cost of increased verbosity or decreased
   readability.

   Example: the pattern ⢠in match x+y in â_,_:?.(? ? % ?)
   locates only the first occurrence of x+y in the sequent x,y:
   nat ⢠âz,w:nat. (x+y) * (z+w) = z * (x+y) + w * (x+y). The
   corresponding simple pattern is ⢠â_,_:?.(? ? (? % ?) ?).

   Every tactic that acts on subterms of the selected sequents
   have a pattern argument for uniformity. To automatically
   generate a simple pattern:

    1. Select in the current goal the subterms to pass to the
       tactic by using the mouse. In order to perform a multiple
       selection of subterms, hold the Ctrl key while selecting
       every subterm after the first one.
    2. From the contextual menu select "Copy".
    3. From the "Edit" or the contextual menu select "Paste as
       pattern"
     _________________________________________________________

4.4.3. reduction-kind

   Reduction kinds are normalization functions that transform a
   term to a convertible but simpler one. Each reduction kind can
   be used both as a tactic argument and as a stand-alone tactic.

   Table 4-14. reduction-kind
   reduction-kind ::= normalize Computes the βδιζ-normal form
     | reduce Computes the βδιζ-normal form
     | simplify Computes a form supposed to be simpler
     | unfold [sterm] δ-reduces the constant or variable if
   specified, or that in head position
     | whd Computes the βδιζ-weak-head normal form
     _________________________________________________________

4.4.4. auto-params

   TODO

   Table 4-15. reduction-kind
   auto_params ::= depth=â« TODO
               |   width=â« TODO
               |   TODO     TODO
     _________________________________________________________

Chapter 5. Extending the syntax

5.1. Introduction

   TODO

   notation: TODO

   interpretation: TODO
     _________________________________________________________

Chapter 6. Tacticals

6.1. Interactive proofs and definitions

   An interactive definition is started by giving a definition
   command omitting the definiens. An interactive proof is
   started by using one of the proof commands omitting an
   explicit proof term.

   An interactive proof or definition can and must be terminated
   by a qed command when no more sequents are left to prove.
   Between the command that starts the interactive session and
   the qed command the user must provide a procedural proof
   script made of tactics structured by means of tacticals.

   In the tradition of the LCF system, tacticals can be
   considered higher order tactics. Their syntax is structured
   and they are executed atomically. On the contrary, in Matita
   the syntax of several tacticals is destructured into a
   sequence of tokens and tactics in such a way that is is
   possible to stop execution after every single token or tactic.
   The original semantics is preserved: the execution of the
   whole sequence yields the result expected by the original
   LCF-like tactical.
     _________________________________________________________

6.2. The proof status

   During an interactive proof, the proof status is made of the
   set of sequents to prove and the partial proof built so far.

   The partial proof can be inspected on demand in the CIC
   browser. It will be shown in pseudo-natural language produced
   on the fly from the proof term.

   The set of sequents to prove is shown in the notebook of the
   authoring interface, in the top-right corner of the main
   window of Matita. Each tab shows a different sequent, named
   with a question mark followed by a number. The current role of
   the sequent, according to the following description, is also
   shown in the tab tag.

    1. Selected sequents (name in boldface, e.g. ?3). The next
       tactic will be applied to every selected sequent,
       producing new selected sequents. Tacticals such as
       branching ("[") or "focus" can be used to change the set
       of selected sequents.
    2. Sibling sequents (name prefixed by a vertical bar and
       their position, e.g. |[3]?2). When the set of selected
       sequents has more than one element, the user can decide to
       focus in turn on each of them. The branching tactical
       ("[") selects the first sequent only, marking every
       previously selected sequent as a sibling sequent. Each
       sibling sequent is given a different position. The
       tactical "2,3:" can be used to select one or more sibling
       sequents, different from the one proposed, according to
       their position. Once the user starts to work on the
       selected sibling sequents it becomes impossible to select
       a new set of siblings until the ("|") tactical is used to
       end work on the current one.
    3. Automatically solved sibling sequents (name strokethrough,
       e.g. |[3]?2). Sometimes a tactic can close by side effects
       a sibling sequent the user has not selected yet. The
       sequent is left in the automatically solved status in
       order for the user to explicitly accept (using the "skip"
       tactical) the automatic instantiation in the proof script.
       This way the correspondence between the number of branches
       in the proof script and the number of sequents generated
       in the proof is preserved.
     _________________________________________________________

6.3. Tacticals

   Table 6-1. proof script
   proof-script ::= proof-step [proof-step]â¦

   Every proof step can be immediately executed.

   Table 6-2. proof steps
   proof-step ::= LCF-tactical The tactical is applied to each
   selected sequent. Each new sequent becomes a selected sequent.
     | . The first selected sequent becomes the only one
   selected. All the remaining previously selected sequents are
   proposed to the user one at a time when the next "." is used.
     | ; Nothing changes. Use this proof step as a separator in
   concrete syntax.
     | [ Every selected sequent becomes a sibling sequent that
   constitute a branch in the proof. Moreover, the first sequent
   is also selected.
     | | Stop working on the current branch of the innermost
   branching proof. The sibling branches become the sibling
   sequents and the first one is also selected.
     | nat[,nat]â¦: The sibling sequents specified by the user
   become the next selected sequents.
     | *: Every sibling branch not considered yet in the
   innermost branching proof becomes a selected sequent.
     | skip Accept the automatically provided instantiation (not
   shown to the user) for the currently selected automatically
   closed sibling sequent.
     | ] Stop analyzing branches for the innermost branching
   proof. Every sequent opened during the branching proof and not
   closed yet becomes a selected sequent.
     | focus nat [nat]⦠Selects the sequents specified by the
   user. The selected sequents must be completely closed (no new
   sequents left open) before doing an "unfocus that restores the
   current set of sibling branches.
     | unfocus Used to match the innermost "focus" tactical when
   all the sequents selected by it have been closed. Until
   "unfocus" is performed, it is not possible to progress in the
   rest of the proof.

   Table 6-3. tactics and LCF tacticals
   LCF-tactical ::= tactic Applies the specified tactic.
     | LCF-tactical ; LCF-tactical Applies the first tactical
   first and the second tactical to each sequent opened by the
   first one.
     | LCF-tactical [ [LCF-tactical] [| LCF-tactical]⦠] Applies
   the first tactical first and each tactical in the list of
   tacticals to the corresponding sequent opened by the first
   one. The number of tacticals provided in the list must be
   equal to the number of sequents opened by the first tactical.
     | do nat LCF-tactical end TODO
     | repeat LCF-tactical end TODO
     | first [ [LCF-tactical] [| LCF-tactical]⦠] TODO
     | try LCF-tactical TODO
     | solve [ [LCF-tactical] [| LCF-tactical]⦠] TODO
     | (LCF-tactical) Used for grouping during parsing.
     _________________________________________________________

Chapter 7. Tactics

7.1. Quick reference card

   Table 7-1. tactics
   tactic ::= absurd sterm
     | apply sterm
     | applyS sterm
     | assumption 
     | auto [depth=nat] [width=nat] [paramodulation] [full]
     | change pattern with sterm
     | clear id [idâ¦]
     | clearbody id
     | constructor nat
     | contradiction 
     | cut sterm [as id]
     | decompose [( id⦠)] [id] [as idâ¦]
     | demodulate 
     | destruct sterm
     | elim sterm [using sterm] intros-spec
     | elimType sterm [using sterm] intros-spec
     | exact sterm
     | exists 
     | fail 
     | fold reduction-kind sterm pattern
     | fourier 
     | fwd id [as id [id]â¦]
     | generalize pattern [as id]
     | id 
     | intro [id]
     | intros intros-spec
     | inversion sterm
     | lapply [linear] [depth=nat] sterm [to sterm [,stermâ¦] ]
   [as id]
     | left 
     | letin id â sterm
     | normalize pattern
     | reduce pattern
     | reflexivity 
     | replace pattern with sterm
     | rewrite [<|>] sterm pattern
     | right 
     | ring 
     | simplify pattern
     | split 
     | subst 
     | symmetry 
     | transitivity sterm
     | unfold [sterm] pattern
     | whd pattern
     _________________________________________________________

7.2. absurd

   absurd P

   Synopsis:
          absurd sterm

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

7.3. apply

   apply t

   Synopsis:
          apply sterm

   Pre-conditions:
          t must have type T[1] â ... â T[n] â 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 T[i] that is
          not instantiated by unification. T[i] is the conclusion
          of the i-th new sequent to prove.
     _________________________________________________________

7.4. applyS

   applyS t auto_params

   Synopsis:
          applyS sterm auto_params

   Pre-conditions:
          t must have type T[1] â ... â T[n] â G.

   Action:
          applyS is useful when apply fails because the current
          goal and the conclusion of the applied theorems are
          extensionally equivalent up to instantiation of
          metavariables, but cannot be unified. E.g. the goal is
          P(n*O+m) and the theorem to be applied proves
          âm.P(m+O).

          It tries to automatically rewrite the current goal
          using auto paramodulation to make it unifiable with G.
          Then it closes the current sequent by applying t to n
          implicit arguments (that become new sequents). The
          auto_params parameters are passed directly to auto
          paramodulation.

   New sequents to prove:
          It opens a new sequent for each premise T[i] that is
          not instantiated by unification. T[i] is the conclusion
          of the i-th new sequent to prove.
     _________________________________________________________

7.5. assumption

   assumption

   Synopsis:
          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
     _________________________________________________________

7.6. auto

   auto depth=d width=w paramodulation full

   Synopsis:
          auto [depth=nat] [width=nat] [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
     _________________________________________________________

7.7. clear

   clear H[1] ... H[m]

   Synopsis:
          clear id [idâ¦]

   Pre-conditions:
          H[1] ... H[m] must be hypotheses of the current sequent
          to prove.

   Action:
          It hides the hypotheses H[1] ... H[m] from the current
          sequent.

   New sequents to prove:
          None
     _________________________________________________________

7.8. clearbody

   clearbody H

   Synopsis:
          clearbody id

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

7.9. change

   change patt with t

   Synopsis:
          change pattern with sterm

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

7.10. constructor

   constructor n

   Synopsis:
          constructor nat

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

7.11. contradiction

   contradiction

   Synopsis:
          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
     _________________________________________________________

7.12. cut

   cut P as H

   Synopsis:
          cut sterm [as id]

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

7.13. decompose

   decompose (T[1] ... T[n]) H as H[1] ... H[m]

   Synopsis:
          decompose [( id⦠)] [id] [as idâ¦]

   Pre-conditions:
          H must inhabit one inductive type among T[1] ... T[n]
          and the types of a predefined list.

   Action:
          Runs elim H H[1] ... H[m] , clears H and tries to run
          itself recursively on each new identifier introduced by
          elim in the opened sequents. If H is not provided tries
          this operation on each premise in the current context.

   New sequents to prove:
          The ones generated by all the elim tactics run.
     _________________________________________________________

7.14. demodulate

   demodulate

   Synopsis:
          demodulate

   Pre-conditions:
          None.

   Action:
          TODO

   New sequents to prove:
          None.
     _________________________________________________________

7.15. destruct

   destruct p

   Synopsis:
          destruct sterm

   Pre-conditions:
          p must have type E[1] = E[2] where the two sides of the
          equality are possibly applied constructors of an
          inductive type.

   Action:
          The tactic recursively compare the two sides of the
          equality looking for different constructors in
          corresponding position. If two of them are found, the
          tactic closes the current sequent by proving the
          absurdity of p. Otherwise it adds a new hypothesis for
          each leaf of the formula that states the equality of
          the subformulae in the corresponding positions on the
          two sides of the equality.

   New sequents to prove:
          None.
     _________________________________________________________

7.16. elim

   elim t using th hyps

   Synopsis:
          elim sterm [using sterm] intros-spec

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

7.17. elimType

   elimType T using th hyps

   Synopsis:
          elimType sterm [using sterm] intros-spec

   Pre-conditions:
          T must be an inductive type.

   Action:
          TODO (severely bugged now).

   New sequents to prove:
          TODO
     _________________________________________________________

7.18. exact

   exact p

   Synopsis:
          exact sterm

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

7.19. exists

   exists

   Synopsis:
          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.
     _________________________________________________________

7.20. fail

   fail

   Synopsis:
          fail

   Pre-conditions:
          None.

   Action:
          This tactic always fail.

   New sequents to prove:
          N.A.
     _________________________________________________________

7.21. fold

   fold red t patt

   Synopsis:
          fold reduction-kind sterm pattern

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

7.22. fourier

   fourier

   Synopsis:
          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.
     _________________________________________________________

7.23. fwd

   fwd H as H[0] ... H[n]

   Synopsis:
          fwd id [as id [id]â¦]

   Pre-conditions:
          The type of H must be the premise of a forward
          simplification theorem.

   Action:
          This tactic is under development. It simplifies the
          current context by removing H using the following
          methods: forward application (by lapply) of a suitable
          simplification theorem, chosen automatically, of which
          the type of H is a premise, decomposition (by
          decompose), rewriting (by rewrite). H[0] ... H[n] are
          passed to the tactics fwd invokes, as names for the
          premise they introduce.

   New sequents to prove:
          The ones opened by the tactics fwd invokes.
     _________________________________________________________

7.24. generalize

   generalize patt as H

   Synopsis:
          generalize pattern [as id]

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

7.25. id

   id

   Synopsis:
          id

   Pre-conditions:
          None.

   Action:
          This identity tactic does nothing without failing.

   New sequents to prove:
          None.
     _________________________________________________________

7.26. intro

   intro H

   Synopsis:
          intro [id]

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

7.27. intros

   intros hyps

   Synopsis:
          intros intros-spec

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

7.28. inversion

   inversion t

   Synopsis:
          inversion sterm

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

7.29. lapply

   lapply linear depth=d t to t[1], ..., t[n] as H

   Synopsis:
          lapply [linear] [depth=nat] sterm [to sterm [,stermâ¦]
          ] [as id]

   Pre-conditions:
          t must have at least d independent premises and n must
          not be greater than d.

   Action:
          Invokes letin H â (t ? ... ?) with enough ?'s to reach
          the d-th independent premise of t (d is maximum if
          unspecified). Then istantiates (by apply) with t[1],
          ..., t[n] the ?'s corresponding to the first n
          independent premises of t. Usually the other ?'s
          preceding the n-th independent premise of t are
          istantiated as a consequence. If the linear flag is
          specified and if t, t[1], ..., t[n] are (applications
          of) premises in the current context, they are cleared.

   New sequents to prove:
          The ones opened by the tactics lapply invokes.
     _________________________________________________________

7.30. left

   left

   Synopsis:
          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.
     _________________________________________________________

7.31. letin

   letin x â t

   Synopsis:
          letin id â sterm

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

7.32. normalize

   normalize patt

   Synopsis:
          normalize pattern

   Pre-conditions:
          None.

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

   New sequents to prove:
          None.
     _________________________________________________________

7.33. reduce

   reduce patt

   Synopsis:
          reduce pattern

   Pre-conditions:
          None.

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

   New sequents to prove:
          None.
     _________________________________________________________

7.34. reflexivity

   reflexivity

   Synopsis:
          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.
     _________________________________________________________

7.35. replace

   change patt with t

   Synopsis:
          replace pattern with sterm

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

7.36. rewrite

   rewrite dir p patt

   Synopsis:
          rewrite [<|>] sterm pattern

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

7.37. right

   right

   Synopsis:
          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.
     _________________________________________________________

7.38. ring

   ring

   Synopsis:
          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.
     _________________________________________________________

7.39. simplify

   simplify patt

   Synopsis:
          simplify pattern

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

7.40. split

   split

   Synopsis:
          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.
     _________________________________________________________

7.41. subst

   subst

   Synopsis:
          subst

   Pre-conditions:
          None.

   Action:
          For each premise of the form H: x = t or H: t = x where
          x is a local variable and t does not depend on x, the
          tactic rewrites H wherever x appears clearing H and x
          afterwards.

   New sequents to prove:
          The one opened by the applied tactics.
     _________________________________________________________

7.42. symmetry

   The tactic symmetry

   symmetry

   Synopsis:
          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.
     _________________________________________________________

7.43. transitivity

   transitivity t

   Synopsis:
          transitivity sterm

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

7.44. unfold

   unfold t patt

   Synopsis:
          unfold [sterm] pattern

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

7.45. whd

   whd patt

   Synopsis:
          whd pattern

   Pre-conditions:
          None.

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

   New sequents to prove:
          None.
     _________________________________________________________

Chapter 8. Other commands

8.1. alias

   alias id "s" = "def"

   alias symbol "s" (instance n) = "def"

   alias num (instance n) = "def"

   Synopsis:
          alias [id qstring = qstring | symbol qstring [(instance
          nat)] = qstring | num [(instance nat)] = qstring ]

   Action:
          Used to give an hint to the disambiguating parser. When
          the parser is faced to the identifier (or symbol) s or
          to any number, it will prefer interpretations that "map
          s (or the number) to def". For identifiers, "def" is
          the URI of the interpretation. E.g.:
          cic:/matita/nat/nat.ind#xpointer(1/1/1) for the first
          constructor of the first inductive type defined in the
          block of inductive type(s) cic:/matita/nat/nat.ind. For
          symbols and numbers, "def" is the label used to mark
          the wanted interpretation.

          When a symbol or a number occurs several times in the
          term to be parsed, it is possible to give an hint only
          for the instance n. When the instance is omitted, the
          hint is valid for every occurrence.

          Hints are automatically inserted in the script by
          Matita every time the user is interactively asked a
          question to disambiguate a term. This way the user
          won't be posed the same question twice when the script
          will be executed again.
     _________________________________________________________

8.2. check

   check t

   Synopsis:
          check term

   Action:
          Opens a CIC browser window that shows t together with
          its type. The command is immediately removed from the
          script.
     _________________________________________________________

8.3. coercion

   coercion u

   Synopsis:
          coercion uri

   Action:
          Declares u as an implicit coercion from the type of its
          last argument (source) to its codomain (target). Every
          time a term x of type source is used with expected type
          target, Matita automatically replaces x with (u ? ⦠?
          x) to avoid a typing error.

          Implicit coercions are not displayed to the user: (u ?
          ⦠? x) is rendered simply as x.

          When a coercion u is declared from source s to target t
          and there is already a coercion u' of target s or
          source t, a composite implicit coercion is
          automatically computed by Matita.
     _________________________________________________________

8.4. default

   default "s" u[1] ⦠u[n]

   Synopsis:
          default qstring uri [uri]â¦

   Action:
          It registers a cluster of related definitions and
          theorems to be used by tactics and the rendering
          engine. Some functionalities of Matita are not
          available when some clusters have not been registered.
          Overloading a cluster registration is possible: the
          last registration will be the default one, but the
          previous ones are still in effect.

          s is an identifier of the cluster and u[1] ⦠u[n] are
          the URIs of the definitions and theorems of the
          cluster. The number n of required URIs depends on the
          cluster. The following clusters are supported.

          Table 8-1. clusters

   name expected object for 1st URI expected object for 2nd URI
   expected object for 3rd URI expected object for 4th URI
   expected object for 5th URI
   equality an inductive type (say, of type eq) of type âA:Type.A
   â Prop with one family parameter and one constructor of type
   âx:A.eq A x a theorem of type âA.âx,y:A.eq A x y â eq A y x a
   theorem of type âA.âx,y,z:A.eq A x y â eq A y z â eq A x z
   âA.âa.â P:A â Prop.P x â ây.eq A x y â P y âA.âa.â P:A â
   Prop.P x â ây.eq A y x â P y
   true an inductive type of type Prop with only one constructor
   that has no arguments
   false an inductive type of type Prop without constructors

   absurd a theorem of type âA:Prop.âB:Prop.A â Not A â B
     _________________________________________________________

8.5. hint

   hint

   Synopsis:
          hint

   Action:
          Displays a list of theorems that can be successfully
          applied to the current selected sequent. The command is
          removed from the script, but the window that displays
          the theorems allow to add to the script the application
          of the selected theorem.
     _________________________________________________________

8.6. include

   include "s"

   Synopsis:
          include qstring

   Action:
          Every coercion, notation and interpretation that was
          active when the file s was compiled last time is made
          active. The same happens for declarations of default
          definitions and theorems and disambiguation hints
          (aliases). On the contrary, theorem and definitions
          declared in a file can be immediately used without
          including it.

          The file s is automatically compiled if it is not
          compiled yet and if it is handled by a development.
     _________________________________________________________

8.7. include' "s"

   Synopsis:
          include' qstring

   Action:
          Not documented (TODO), do not use it.
     _________________________________________________________

8.8. set

   set "baseuri" "s"

   Synopsis:
          set qstring qstring

   Action:
          Sets to s the baseuri of all the theorems and
          definitions stated in the current file. The baseuri
          should be a/b/c/foo if the file is named foo and it is
          in the subtree a/b/c of the current development. This
          requirement is not enforced, but it could be in the
          future.

          Currently, baseuri is the only property that can be set
          even if the parser accepts arbitrary property names.
     _________________________________________________________

8.9. whelp

   whelp locate "s"

   whelp hint t

   whelp elim t

   whelp match t

   whelp instance t

   Synopsis:
          whelp [locate qstring | hint term | elim term | match
          term | instance term ]

   Action:
          Performs the corresponding query, showing the result in
          the CIC browser. The command is removed from the
          script.
     _________________________________________________________

8.10. qed

   Synopsis:
          qed

   Action:
          Saves and indexes the current interactive theorem or
          definition. In order to do this, the set of sequents
          still to be proved must be empty.
     _________________________________________________________

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.

  Notes

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