Matita V0.1.0 User Manual (rev. 1α) Andrea Asperti Claudio Sacerdoti Coen Ferruccio Guidi Enrico Tassi Stefano Zacchiroli 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.