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