2 Matita V0.1.0 User Manual (rev. 1α)
10 <sacerdot@cs.unibo.it>
22 <zacchiro@cs.unibo.it>
24 Copyright © 2006 The HELM team.
26 Both Matita and this document are free software, you can
27 redistribute them and/or modify them under the terms of the
28 GNU General Public License as published by the Free Software
29 Foundation. See Chapter 9 for more information.
30 _________________________________________________________
40 2.1. Installing from sources
42 2.1.1. Getting the source code
45 2.1.4. Compiling and installing
47 2.2. Configuring Matita
51 3.1. How to type Unicode symbols
52 3.2. Browsing and searching
54 3.2.1. Browsing the library
55 3.2.2. Looking at a proof under development
56 3.2.3. Searching the library
60 3.3.1. How to use developments
61 3.3.2. The authoring interface
67 4.1.1. Lexical conventions
70 4.2. Definitions and declarations
73 4.2.2. definition id[: term] [â term]
74 4.2.3. [inductive|coinductive] id [args2]⦠: term
75 â [|] [id:term] [| id:term]⦠[with id :
76 term â [|] [id:term] [| id:term]â¦]â¦
78 4.2.4. record id [args2]⦠: term â{[id [:|:>]
79 term] [;id [:|:>] term]â¦}
83 4.3.1. theorem id[: term] [â term]
84 4.3.2. variant id: term â term
85 4.3.3. lemma id[: term] [â term]
86 4.3.4. fact id[: term] [â term]
87 4.3.5. remark id[: term] [â term]
96 5. Extending the syntax
102 6.1. Interactive proofs and definitions
103 6.2. The proof status
108 7.1. Quick reference card
179 4-10. Pattern matching
187 6-3. tactics and LCF tacticals
192 3-1. The Developments window
193 _________________________________________________________
195 Chapter 1. Introduction
199 Matita is an interactive theorem prover (or proof assistant)
200 with the following characteristics:
202 * It is based on a variant of the Calculus of (Co)Inductive
203 Constructions (CIC). CIC is also the logic of the Coq
205 * It adopts a procedural proof language, but it has a new
206 set of small step tacticals that improve proof structuring
208 * It has a stand-alone graphical user interface (GUI)
209 inspired by CtCoq/Proof General. The GUI is implemented
210 according to the state of the art. In particular:
211 + It is based and fully integrated with Gtk/Gnome.
212 + An on-line help can be browsed via the Gnome
213 documentation browser.
214 + Mathematical formulae are rendered in two dimensional
215 notation via MathML and Unicode.
216 * It integrates advanced browsing and searching procedures.
217 * It allows the use of the typical ambiguous mathematical
218 notation by means of a disambiguating parser.
219 * It is compatible with the library of Coq (definitions and
221 _________________________________________________________
225 The system shares a common look&feel with the Coq proof
226 assistant and its graphical user interface. The two systems
227 have the same logic, very close proof languages and similar
228 sets of tactics. Moreover, Matita is compatible with the
229 library of Coq. From the user point of view the main lacking
230 features with respect to Coq are:
233 * an extensible language of tactics;
234 * automatic implicit arguments;
235 * several ad-hoc decision procedures;
236 * several rarely used variants for most of the tactics;
237 * sections and local variables. To maintain compatibility
238 with the library of Coq, theorems defined inside sections
239 are abstracted by name over the section variables; their
240 instances are explicitly applied to actual arguments by
241 means of explicit named substitutions.
243 Still from the user point of view, the main differences with
246 * the language of tacticals that allows execution of partial
247 tactical application;
248 * the unification of the concept of metavariable and
249 existential variable;
250 * terms with subterms that cannot be inferred are always
251 allowed as arguments of tactics or other commands;
252 * ambiguous terms are disambiguated by direct interaction
254 * theorems and definitions in the library are always
255 accessible without needing to require/include them; right
256 now, only notation needs to be included to become active,
257 but we plan to remove this limitation.
258 _________________________________________________________
260 Chapter 2. Installation
262 2.1. Installing from sources
264 Currently, the only intended way to install Matita is starting
265 from its source code.
266 _________________________________________________________
268 2.1.1. Getting the source code
270 You can get the Matita source code in two ways:
272 1. go to the download page and get the latest released source
274 2. get the development sources from our SVN repository. You
275 will need the components/ and matita/ directories from the
276 trunk/helm/software/ directory, plus the configure and
277 Makefile* stuff from the same directory.
278 In this case you will need to run autoconf before
279 proceding with the building instructions below.
280 _________________________________________________________
284 In order to build Matita from sources you will need some tools
285 and libraries. They are listed below.
287 Note Note for Debian users
290 If you are running a Debian GNU/Linux distribution you can
291 have APT install all the required tools and libraries by
292 adding the following repository to your /etc/apt/sources.list:
293 deb http://people.debian.org/~zack unstable helm
296 and installing the helm-matita-deps package.
298 Required tools and libraries
301 the Objective Caml compiler, version 3.09 or above
304 OCaml package manager, version 1.1.1 or above
307 OCaml bindings for the expat library
310 OCaml bindings for the Gdome 2 library
313 OCaml library to write HTTP daemons (and clients)
316 OCaml bindings for the GTK+ library , version 2.6.0 or
319 GtkMathView , LablGtkMathView
320 GTK+ widget to render MathML documents and its OCaml
323 GtkSourceView , LablGtkSourceView
324 extension for the GTK+ text widget (adding the typical
325 features of source code editors) and its OCaml bindings
328 SQL database and OCaml bindings for its client-side
331 The SQL database itself is not strictly needed to run
332 Matita, but we stronly encourage its use since a lot of
333 features are disabled without it. Still, the OCaml
334 bindings of the library are needed at compile time.
337 collection of OCaml libraries to deal with
338 application-level Internet protocols and conventions
341 Unicode lexer generator for OCaml
344 OCaml library to access .gz files
345 _________________________________________________________
347 2.1.3. Database setup
349 To fully exploit Matita indexing and search capabilities you
350 will need a working MySQL database. Detalied instructions on
351 how to do it can be found in the MySQL documentation. Here you
352 can find a quick howto.
354 In order to create a database you need administrator
355 permissions on your MySQL installation, usually the root
356 account has them. Once you have the permissions, a new
357 database can be created executing mysqladmin create matita
358 (matita is the default database name, you can change it using
359 the db.user key of the configuration file).
361 Then you need to grant the necessary access permissions to the
362 database user of Matita, typing echo "grant all privileges on
363 matita.* to helm;" | mysql matita should do the trick (helm is
364 the default user name used by Matita to access the database,
365 you can change it using the db.user key of the configuration
370 This way you create a database named matita on which anyone
371 claiming to be the helm user can do everything (like adding
372 dummy data or destroying the contained one). It is strongly
373 suggested to apply more fine grained permissions, how to do it
374 is out of the scope of this manual.
375 _________________________________________________________
377 2.1.4. Compiling and installing
379 Once you get the source code the installations steps should be
382 First of all you need to configure the build process executing
383 ./configure. This will check that all needed tools and library
384 are installed and prepare the sources for compilation and
387 Quite a few (optional) arguments may be passed to the
388 configure command line to change build time parameters. They
389 are listed below, together with their default values:
391 configure command line arguments
393 --with-runtime-dir=dir
394 (Default: /usr/local/matita) Runtime base directory
395 where all Matita stuff (executables, configuration
396 files, standard library, ...) will be installed
399 (Default: localhost) Default SQL server hostname. Will
400 be used while building the standard library during the
401 installation and to create the default Matita
402 configuration. May be changed later in configuration
406 (Default: disabled) Enable debugging code. Not for the
409 Then you will manage the build and install process using make
410 as usual. Below are reported the targets you have to invoke in
411 sequence to build and install:
416 builds components needed by Matita and Matita itself
417 (in bytecode or native code depending on the
418 availability of the OCaml native code compiler)
421 installs Matita related tools, standard library and the
422 needed runtime stuff in the proper places on the
425 As a part of the installation process the Matita
426 standard library will be compiled, thus testing that
427 the just built matitac compiler works properly.
429 For this step you will need a working SQL database (for
430 indexing the standard library while you are compiling
431 it). See Database setup for instructions on how to set
433 _________________________________________________________
435 2.2. Configuring Matita
437 The file matita.conf.xml... TODO
438 _________________________________________________________
440 Chapter 3. Getting started
442 If you are already familiar with the Calculus of (Co)Inductive
443 Constructions (CIC) and with interactive theorem provers with
444 procedural proof languages (expecially Coq), getting started
445 with Matita is relatively easy. You just need to learn how to
446 type Unicode symbols, how to browse and search the library and
447 how to author a proof script.
448 _________________________________________________________
450 3.1. How to type Unicode symbols
452 Unicode characters can be typed in several ways:
454 * Using the "Ctrl+Shift+Unicode code" standard Gnome
455 shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".
456 * Typing the ligature "\name" where "name" is a standard
457 Unicode or LaTeX name for the character. Pressing "Alt+L"
458 just after the last character of the name converts the
459 ligature to the Unicode symbol. This operation is not
460 required since Matita understands also the "\name"
461 sequences. E.g. "\Omega" followed by Alt+L generates "Ω".
462 * Typing one of the following ligatures (and optionally
463 converting the ligature to the Unicode character has
464 described before): ":=" (which stands for â); "->" (which
465 stands for "â"); "=>" (which stands for "â").
466 _________________________________________________________
468 3.2. Browsing and searching
470 The CIC browser is used to browse and search the library. You
471 can open a new CIC browser selecting "New Cic Browser" from
472 the "View" menu of Matita, or by pressing "F3". The CIC
473 browser is similar to a traditional Web browser.
474 _________________________________________________________
476 3.2.1. Browsing the library
478 To browse the library, type in the location bar the absolute
479 URI of the theorem, definition or library fragment you are
480 interested in. "cic:/" is the root of the library.
481 Contributions developed in Matita are under "cic:/matita"; all
482 the others are part of the library of Coq.
484 Following the hyperlinks it is possible to navigate in the Web
485 of mathematical notions. Proof are rendered in pseudo-natural
486 language and mathematical notation is used for formulae. For
487 now, mathematical notation must be included in the current
488 script to be activated, but we plan to remove this limitation.
489 _________________________________________________________
491 3.2.2. Looking at a proof under development
493 A proof under development is not yet part of the library. The
494 special URI "about:proof" can be used to browse the proof
495 currently under development, if there is one. The "home"
496 button of the CIC browser sets the location bar to
498 _________________________________________________________
500 3.2.3. Searching the library
502 The query bar of the CIC browser can be used to search the
503 library of Matita for theorems or definitions that match
504 certain criteria. The criteria is given by typing a term in
505 the query bar and selecting an action in the drop down menu
507 _________________________________________________________
509 3.2.3.1. Searching by name
512 _________________________________________________________
514 3.2.3.2. List of lemmas that can be applied
517 _________________________________________________________
519 3.2.3.3. Searching by exact match
522 _________________________________________________________
524 3.2.3.4. List of elimination principles for a given type
527 _________________________________________________________
529 3.2.3.5. Searching by instantiation
532 _________________________________________________________
536 3.3.1. How to use developments
538 A development is a set of scripts files that are strictly
539 related (i.e. they depend on each other). Matita is able to
540 automatically manage dependencies among the scripts in a
541 development, compiling them in the correct order.
543 The include statement can be performed by Matita only if the
544 mentioned script is compiled. If both scripts (the one that
545 includes and the included) are part of the same development,
546 the included script (and recursively all its dependencies) can
547 be compiled automatically. Dependencies among scripts
548 belonging to different developments is not implemented yet.
550 The "Developments..." item the File menu (or pressing Ctrl+D)
551 opens the Developments window.
553 Figure 3-1. The Developments window
557 Developments window buttons
560 To create a new Development the user needs to specify a
561 name[1] and the root directory in which all scripts
562 will be placed, eventually organized in subdirectories.
563 The Development should be named as the directory in
564 which it lives. A "makefile" file is placed in the
565 specified root directory. That makefile supports the
569 Build the whole development.
572 Cleans the whole development.
575 Resets the user environment (i.e. deleting all
576 the results of compilation of every development,
577 including the contents of the database). This
578 target should be used only in case something goes
579 wrong and Matita behaves incorrectly.
582 Compiles "scriptname.ma"
585 Decompiles the whole development and removes it.
588 Compiles all the scripts in the development.
591 Decompiles the whole development.
594 All the user developments live in the "user" space.
595 That is, the result of the compilation of scripts is
596 placed in his home directory and the tuples are placed
597 in personal tables inside the database. Publishing a
598 development means putting it in the "library" space.
599 This means putting the result of compilation in the
600 same place where the standard library lives. This
601 feature will be improved in the future to support
602 publishing the development in the "distributed library"
603 space (making your development public).
606 Closes the Developments window
607 _________________________________________________________
609 3.3.2. The authoring interface
612 _________________________________________________________
616 To describe syntax in this manual we use the following
619 1. Non terminal symbols are emphasized and have a link to
620 their definition. E.g.: term
621 2. Terminal symbols are in bold. E.g.: theorem
622 3. Optional sequences of elements are put in square brackets.
624 4. Alternatives are put in square brakets and they are
625 separated by vertical bars. E.g.: [<|>]
626 5. Repetitions of a sequence of elements are given by putting
627 the sequence in square brackets, that are followed by
628 three dots. The empty sequence is a valid repetition.
630 6. Characters belonging to a set of characters are given by
631 listing the set elements in square brackets. Hyphens are
632 used to specify ranges of characters in the set. E.g.:
634 _________________________________________________________
638 4.1.1. Lexical conventions
641 qstring ::= "â©â©any sequence of characters excluded "âªâª"
644 id ::= â©â©any sequence of letters, underscores or valid XML
645 digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by
646 a possible empty sequence of decorators ([?'`])âªâª
649 nat ::= â©â©any sequence of valid XML digitsâªâª
652 char ::= [a-zA-Z0-9_-]
655 uri-step ::= char[char]â¦
659 [cic:/|theory:/]uri-step[/uri-step]â¦.id[.id]â¦[#xpointer(nat/
661 _________________________________________________________
666 term ::= sterm simple or delimited term
667 | term term application
668 | λargs.term λ-abstraction
669 | Î args.term dependent product meant to define a datatype
670 | âargs.term dependent product meant to define a proposition
671 | term â term non-dependent product (logical implication or
673 | let [id|(id: term)] â term in term local definition
674 | let [co]rec rec_def (co)recursive definitions
677 | ⦠user provided notation
678 rec_def ::= id [id|(id[,term]⦠:term)]â¦
679 [on id] [: term] â term]
681 Table 4-8. Simple terms
683 | id[\subst[ idâterm [;idâterm]⦠]] identifier with
684 optional explicit named substitution
685 | uri a qualified reference
686 | Prop the impredicative sort of propositions
687 | Set the impredicate sort of datatypes
688 | CProp one fixed predicative sort of constructive
690 | Type one predicative sort of datatypes
691 | ? implicit argument
692 | ?n [[ [_|term]⦠]] metavariable
693 | match term [ in term ] [ return term ] with case analysis
694 [ match_branch[|match_branch]⦠]
696 | ⦠user provided notation at precedence 90
699 args ::= _[: term] ignored argument
700 | (_[: term]) ignored argument
702 | (id[,id]â¦[: term])
706 Table 4-10. Pattern matching
707 match_branch ::= match_pattern â term
708 match_pattern ::= id 0-ary constructor
709 | (id id [id]â¦) n-ary constructor (binds the n arguments)
710 _________________________________________________________
712 4.2. Definitions and declarations
714 4.2.1. axiom id: term
718 H is declared as an axiom that states P
719 _________________________________________________________
721 4.2.2. definition id[: term] [â term]
725 f is defined as t; T is its type. An error is raised if the
726 type of t is not convertible to T.
728 T is inferred from t if omitted.
730 t can be omitted only if T is given. In this case Matita
731 enters in interactive mode and f must be defined by means of
734 Notice that the command is equivalent to theorem f: T â t.
735 _________________________________________________________
737 4.2.3. [inductive|coinductive] id [args2]⦠: term â [|] [id:term]
738 [| id:term]⦠[with id : term â [|] [id:term] [| id:term]â¦]â¦
740 inductive i x y z: S â k1:T1 | ⦠| kn:Tn with i' : S' â
741 k1':T1' | ⦠| km':Tm'
743 Declares a family of two mutually inductive types i and i'
744 whose types are S and S', which must be convertible to sorts.
746 The constructors ki of type Ti and ki' of type Ti' are also
747 simultaneously declared. The declared types i and i' may occur
748 in the types of the constructors, but only in strongly
749 positive positions according to the rules of the calculus.
751 The whole family is parameterized over the arguments x,y,z.
753 If the keyword coinductive is used, the declared types are
754 considered mutually coinductive.
756 Elimination principles for the record are automatically
757 generated by Matita, if allowed by the typing rules of the
758 calculus according to the sort S. If generated, they are named
759 i_ind, i_rec and i_rect according to the sort of their
761 _________________________________________________________
763 4.2.4. record id [args2]⦠: term â{[id [:|:>] term] [;id [:|:>]
766 record id x y z: S â { f1: T1; â¦; fn:Tn }
768 Declares a new record family id parameterized over x,y,z.
770 S is the type of the record and it must be convertible to a
773 Each field fi is declared by giving its type Ti. A record
774 without any field is admitted.
776 Elimination principles for the record are automatically
777 generated by Matita, if allowed by the typing rules of the
778 calculus according to the sort S. If generated, they are named
779 i_ind, i_rec and i_rect according to the sort of their
782 For each field fi a record projection fi is also automatically
783 generated if projection is allowed by the typing rules of the
784 calculus according to the sort S, the type T1 and the
785 definability of depending record projections.
787 If the type of a field is declared with :>, the corresponding
788 record projection becomes an implicit coercion. This is just
789 syntactic sugar and it has the same effect of declaring the
790 record projection as a coercion later on.
791 _________________________________________________________
795 4.3.1. theorem id[: term] [â term]
799 Proves a new theorem f whose thesis is P.
801 If p is provided, it must be a proof term for P. Otherwise an
802 interactive proof is started.
804 P can be omitted only if the proof is not interactive.
806 Proving a theorem already proved in the library is an error.
807 To provide an alternative name and proof for the same theorem,
808 use variant f: P â p.
810 A warning is raised if the name of the theorem cannot be
811 obtained by mangling the name of the constants in its thesis.
813 Notice that the command is equivalent to definition f: T â t.
814 _________________________________________________________
816 4.3.2. variant id: term â term
820 Same as theorem f: T â t, but it does not complain if the
821 theorem has already been proved. To be used to give an
822 alternative name or proof to a theorem.
823 _________________________________________________________
825 4.3.3. lemma id[: term] [â term]
829 Same as theorem f: T â t
830 _________________________________________________________
832 4.3.4. fact id[: term] [â term]
836 Same as theorem f: T â t
837 _________________________________________________________
839 4.3.5. remark id[: term] [â term]
843 Same as theorem f: T â t
844 _________________________________________________________
846 4.4. Tactic arguments
848 This section documents the syntax of some recurring arguments
850 _________________________________________________________
854 Table 4-11. intros-spec
855 intros-spec ::= [nat] [([id]â¦)]
857 The natural number is the number of new hypotheses to be
858 introduced. The list of identifiers gives the name for the
860 _________________________________________________________
865 pattern ::= in [id[: path]]⦠[⢠path]] simple pattern
866 | in match term [in [id[: path]]⦠[⢠path]] full pattern
869 path ::= â©â©any sterm whithout occurrences of Set, Prop,
870 CProp, Type, id, uri and user provided notation; however, % is
871 now an additional production for stermâªâª
873 A path locates zero or more subterms of a given term by
874 mimicking the term structure up to:
876 1. Occurrences of the subterms to locate that are represented
878 2. Subterms without any occurrence of subterms to locate that
879 can be represented by ?.
881 For instance, the path â_,_:?.(? ? % ?)â(? ? ? %) locates at
882 once the subterms x+y and x*y in the term âx,y:nat.x+y=1â0=x*y
883 (where the notation A=B hides the term (eq T A B) for some
886 A simple pattern extends paths to locate subterms in a whole
887 sequent. In particular, the pattern in H: p K: q ⢠r locates
888 at once all the subterms located by the pattern r in the
889 conclusion of the sequent and by the patterns p and q in the
890 hypotheses H and K of the sequent.
892 If no list of hypotheses is provided in a simple pattern, no
893 subterm is selected in the hypothesis. If the ⢠p part of the
894 pattern is not provided, no subterm will be matched in the
895 conclusion if at least one hypothesis is provided; otherwise
896 the whole conclusion is selected.
898 Finally, a full pattern is interpreted in three steps. In the
899 first step the match T in part is ignored and a set S of
900 subterms is located as for the case of simple patterns. In the
901 second step the term T is parsed and interpreted in the
902 context of each subterm s â S. In the last term for each s â S
903 the interpreted term T computed in the previous step is looked
904 for. The final set of subterms located by the full pattern is
905 the set of occurrences of the interpreted T in the subterms s.
907 A full pattern can always be replaced by a simple pattern,
908 often at the cost of increased verbosity or decreased
911 Example: the pattern ⢠in match x+y in â_,_:?.(? ? % ?)
912 locates only the first occurrence of x+y in the sequent x,y:
913 nat ⢠âz,w:nat. (x+y) * (z+w) = z * (x+y) + w * (x+y). The
914 corresponding simple pattern is ⢠â_,_:?.(? ? (? % ?) ?).
916 Every tactic that acts on subterms of the selected sequents
917 have a pattern argument for uniformity. To automatically
918 generate a simple pattern:
920 1. Select in the current goal the subterms to pass to the
921 tactic by using the mouse. In order to perform a multiple
922 selection of subterms, hold the Ctrl key while selecting
923 every subterm after the first one.
924 2. From the contextual menu select "Copy".
925 3. From the "Edit" or the contextual menu select "Paste as
927 _________________________________________________________
929 4.4.3. reduction-kind
931 Reduction kinds are normalization functions that transform a
932 term to a convertible but simpler one. Each reduction kind can
933 be used both as a tactic argument and as a stand-alone tactic.
935 Table 4-14. reduction-kind
936 reduction-kind ::= normalize Computes the βδιζ-normal form
937 | reduce Computes the βδιζ-normal form
938 | simplify Computes a form supposed to be simpler
939 | unfold [sterm] δ-reduces the constant or variable if
940 specified, or that in head position
941 | whd Computes the βδιζ-weak-head normal form
942 _________________________________________________________
948 Table 4-15. reduction-kind
949 auto_params ::= depth=â« TODO
952 _________________________________________________________
954 Chapter 5. Extending the syntax
963 _________________________________________________________
967 6.1. Interactive proofs and definitions
969 An interactive definition is started by giving a definition
970 command omitting the definiens. An interactive proof is
971 started by using one of the proof commands omitting an
974 An interactive proof or definition can and must be terminated
975 by a qed command when no more sequents are left to prove.
976 Between the command that starts the interactive session and
977 the qed command the user must provide a procedural proof
978 script made of tactics structured by means of tacticals.
980 In the tradition of the LCF system, tacticals can be
981 considered higher order tactics. Their syntax is structured
982 and they are executed atomically. On the contrary, in Matita
983 the syntax of several tacticals is destructured into a
984 sequence of tokens and tactics in such a way that is is
985 possible to stop execution after every single token or tactic.
986 The original semantics is preserved: the execution of the
987 whole sequence yields the result expected by the original
989 _________________________________________________________
991 6.2. The proof status
993 During an interactive proof, the proof status is made of the
994 set of sequents to prove and the partial proof built so far.
996 The partial proof can be inspected on demand in the CIC
997 browser. It will be shown in pseudo-natural language produced
998 on the fly from the proof term.
1000 The set of sequents to prove is shown in the notebook of the
1001 authoring interface, in the top-right corner of the main
1002 window of Matita. Each tab shows a different sequent, named
1003 with a question mark followed by a number. The current role of
1004 the sequent, according to the following description, is also
1005 shown in the tab tag.
1007 1. Selected sequents (name in boldface, e.g. ?3). The next
1008 tactic will be applied to every selected sequent,
1009 producing new selected sequents. Tacticals such as
1010 branching ("[") or "focus" can be used to change the set
1011 of selected sequents.
1012 2. Sibling sequents (name prefixed by a vertical bar and
1013 their position, e.g. |[3]?2). When the set of selected
1014 sequents has more than one element, the user can decide to
1015 focus in turn on each of them. The branching tactical
1016 ("[") selects the first sequent only, marking every
1017 previously selected sequent as a sibling sequent. Each
1018 sibling sequent is given a different position. The
1019 tactical "2,3:" can be used to select one or more sibling
1020 sequents, different from the one proposed, according to
1021 their position. Once the user starts to work on the
1022 selected sibling sequents it becomes impossible to select
1023 a new set of siblings until the ("|") tactical is used to
1024 end work on the current one.
1025 3. Automatically solved sibling sequents (name strokethrough,
1026 e.g. |[3]?2). Sometimes a tactic can close by side effects
1027 a sibling sequent the user has not selected yet. The
1028 sequent is left in the automatically solved status in
1029 order for the user to explicitly accept (using the "skip"
1030 tactical) the automatic instantiation in the proof script.
1031 This way the correspondence between the number of branches
1032 in the proof script and the number of sequents generated
1033 in the proof is preserved.
1034 _________________________________________________________
1038 Table 6-1. proof script
1039 proof-script ::= proof-step [proof-step]â¦
1041 Every proof step can be immediately executed.
1043 Table 6-2. proof steps
1044 proof-step ::= LCF-tactical The tactical is applied to each
1045 selected sequent. Each new sequent becomes a selected sequent.
1046 | . The first selected sequent becomes the only one
1047 selected. All the remaining previously selected sequents are
1048 proposed to the user one at a time when the next "." is used.
1049 | ; Nothing changes. Use this proof step as a separator in
1051 | [ Every selected sequent becomes a sibling sequent that
1052 constitute a branch in the proof. Moreover, the first sequent
1054 | | Stop working on the current branch of the innermost
1055 branching proof. The sibling branches become the sibling
1056 sequents and the first one is also selected.
1057 | nat[,nat]â¦: The sibling sequents specified by the user
1058 become the next selected sequents.
1059 | *: Every sibling branch not considered yet in the
1060 innermost branching proof becomes a selected sequent.
1061 | skip Accept the automatically provided instantiation (not
1062 shown to the user) for the currently selected automatically
1063 closed sibling sequent.
1064 | ] Stop analyzing branches for the innermost branching
1065 proof. Every sequent opened during the branching proof and not
1066 closed yet becomes a selected sequent.
1067 | focus nat [nat]⦠Selects the sequents specified by the
1068 user. The selected sequents must be completely closed (no new
1069 sequents left open) before doing an "unfocus that restores the
1070 current set of sibling branches.
1071 | unfocus Used to match the innermost "focus" tactical when
1072 all the sequents selected by it have been closed. Until
1073 "unfocus" is performed, it is not possible to progress in the
1076 Table 6-3. tactics and LCF tacticals
1077 LCF-tactical ::= tactic Applies the specified tactic.
1078 | LCF-tactical ; LCF-tactical Applies the first tactical
1079 first and the second tactical to each sequent opened by the
1081 | LCF-tactical [ [LCF-tactical] [| LCF-tactical]⦠] Applies
1082 the first tactical first and each tactical in the list of
1083 tacticals to the corresponding sequent opened by the first
1084 one. The number of tacticals provided in the list must be
1085 equal to the number of sequents opened by the first tactical.
1086 | do nat LCF-tactical end TODO
1087 | repeat LCF-tactical end TODO
1088 | first [ [LCF-tactical] [| LCF-tactical]⦠] TODO
1089 | try LCF-tactical TODO
1090 | solve [ [LCF-tactical] [| LCF-tactical]⦠] TODO
1091 | (LCF-tactical) Used for grouping during parsing.
1092 _________________________________________________________
1096 7.1. Quick reference card
1099 tactic ::= absurd sterm
1103 | auto [depth=nat] [width=nat] [paramodulation] [full]
1104 | change pattern with sterm
1110 | decompose [( id⦠)] [id] [as idâ¦]
1113 | elim sterm [using sterm] intros-spec
1114 | elimType sterm [using sterm] intros-spec
1118 | fold reduction-kind sterm pattern
1120 | fwd id [as id [id]â¦]
1121 | generalize pattern [as id]
1124 | intros intros-spec
1126 | lapply [linear] [depth=nat] sterm [to sterm [,stermâ¦] ]
1133 | replace pattern with sterm
1134 | rewrite [<|>] sterm pattern
1141 | transitivity sterm
1142 | unfold [sterm] pattern
1144 _________________________________________________________
1154 P must have type Prop.
1157 It closes the current sequent by eliminating an absurd
1160 New sequents to prove:
1161 It opens two new sequents of conclusion P and ¬P.
1162 _________________________________________________________
1172 t must have type T[1] â ... â T[n] â G where G can be
1173 unified with the conclusion of the current sequent.
1176 It closes the current sequent by applying t to n
1177 implicit arguments (that become new sequents).
1179 New sequents to prove:
1180 It opens a new sequent for each premise T[i] that is
1181 not instantiated by unification. T[i] is the conclusion
1182 of the i-th new sequent to prove.
1183 _________________________________________________________
1187 applyS t auto_params
1190 applyS sterm auto_params
1193 t must have type T[1] â ... â T[n] â G.
1196 applyS is useful when apply fails because the current
1197 goal and the conclusion of the applied theorems are
1198 extensionally equivalent up to instantiation of
1199 metavariables, but cannot be unified. E.g. the goal is
1200 P(n*O+m) and the theorem to be applied proves
1203 It tries to automatically rewrite the current goal
1204 using auto paramodulation to make it unifiable with G.
1205 Then it closes the current sequent by applying t to n
1206 implicit arguments (that become new sequents). The
1207 auto_params parameters are passed directly to auto
1210 New sequents to prove:
1211 It opens a new sequent for each premise T[i] that is
1212 not instantiated by unification. T[i] is the conclusion
1213 of the i-th new sequent to prove.
1214 _________________________________________________________
1224 There must exist an hypothesis whose type can be
1225 unified with the conclusion of the current sequent.
1228 It closes the current sequent exploiting an hypothesis.
1230 New sequents to prove:
1232 _________________________________________________________
1236 auto depth=d width=w paramodulation full
1239 auto [depth=nat] [width=nat] [paramodulation] [full]
1242 None, but the tactic may fail finding a proof if every
1243 proof is in the search space that is pruned away.
1244 Pruning is controlled by d and w. Moreover, only lemmas
1245 whose type signature is a subset of the signature of
1246 the current sequent are considered. The signature of a
1250 It closes the current sequent by repeated application
1251 of rewriting steps (unless paramodulation is omitted),
1252 hypothesis and lemmas in the library.
1254 New sequents to prove:
1256 _________________________________________________________
1266 H[1] ... H[m] must be hypotheses of the current sequent
1270 It hides the hypotheses H[1] ... H[m] from the current
1273 New sequents to prove:
1275 _________________________________________________________
1285 H must be an hypothesis of the current sequent to
1289 It hides the definiens of a definition in the current
1290 sequent context. Thus the definition becomes an
1293 New sequents to prove:
1295 _________________________________________________________
1302 change pattern with sterm
1305 Each subterm matched by the pattern must be convertible
1306 with the term t disambiguated in the context of the
1310 It replaces the subterms of the current sequent matched
1311 by patt with the new term t. For each subterm matched
1312 by the pattern, t is disambiguated in the context of
1315 New sequents to prove:
1317 _________________________________________________________
1327 The conclusion of the current sequent must be an
1328 inductive type or the application of an inductive type
1329 with at least n constructors.
1332 It applies the n-th constructor of the inductive type
1333 of the conclusion of the current sequent.
1335 New sequents to prove:
1336 It opens a new sequent for each premise of the
1337 constructor that can not be inferred by unification.
1338 For more details, see the apply tactic.
1339 _________________________________________________________
1349 There must be in the current context an hypothesis of
1353 It closes the current sequent by applying an hypothesis
1356 New sequents to prove:
1358 _________________________________________________________
1368 P must have type Prop.
1371 It closes the current sequent.
1373 New sequents to prove:
1374 It opens two new sequents. The first one has an extra
1375 hypothesis H:P. If H is omitted, the name of the
1376 hypothesis is automatically generated. The second
1377 sequent has conclusion P and hypotheses the hypotheses
1378 of the current sequent to prove.
1379 _________________________________________________________
1383 decompose (T[1] ... T[n]) H as H[1] ... H[m]
1386 decompose [( id⦠)] [id] [as idâ¦]
1389 H must inhabit one inductive type among T[1] ... T[n]
1390 and the types of a predefined list.
1393 Runs elim H H[1] ... H[m] , clears H and tries to run
1394 itself recursively on each new identifier introduced by
1395 elim in the opened sequents. If H is not provided tries
1396 this operation on each premise in the current context.
1398 New sequents to prove:
1399 The ones generated by all the elim tactics run.
1400 _________________________________________________________
1415 New sequents to prove:
1417 _________________________________________________________
1427 p must have type E[1] = E[2] where the two sides of the
1428 equality are possibly applied constructors of an
1432 The tactic recursively compare the two sides of the
1433 equality looking for different constructors in
1434 corresponding position. If two of them are found, the
1435 tactic closes the current sequent by proving the
1436 absurdity of p. Otherwise it adds a new hypothesis for
1437 each leaf of the formula that states the equality of
1438 the subformulae in the corresponding positions on the
1439 two sides of the equality.
1441 New sequents to prove:
1443 _________________________________________________________
1447 elim t using th hyps
1450 elim sterm [using sterm] intros-spec
1453 t must inhabit an inductive type and th must be an
1454 elimination principle for that inductive type. If th is
1455 omitted the appropriate standard elimination principle
1459 It proceeds by cases on the values of t, according to
1460 the elimination principle th.
1462 New sequents to prove:
1463 It opens one new sequent for each case. The names of
1464 the new hypotheses are picked by hyps, if provided. If
1465 hyps specifies also a number of hypotheses that is less
1466 than the number of new hypotheses for a new sequent,
1467 then the exceeding hypothesis will be kept as
1468 implications in the conclusion of the sequent.
1469 _________________________________________________________
1473 elimType T using th hyps
1476 elimType sterm [using sterm] intros-spec
1479 T must be an inductive type.
1482 TODO (severely bugged now).
1484 New sequents to prove:
1486 _________________________________________________________
1496 The type of p must be convertible with the conclusion
1497 of the current sequent.
1500 It closes the current sequent using p.
1502 New sequents to prove:
1504 _________________________________________________________
1514 The conclusion of the current sequent must be an
1515 inductive type or the application of an inductive type
1516 with at least one constructor.
1519 Equivalent to constructor 1.
1521 New sequents to prove:
1522 It opens a new sequent for each premise of the first
1523 constructor of the inductive type that is the
1524 conclusion of the current sequent. For more details,
1525 see the constructor tactic.
1526 _________________________________________________________
1539 This tactic always fail.
1541 New sequents to prove:
1543 _________________________________________________________
1550 fold reduction-kind sterm pattern
1553 The pattern must not specify the wanted term.
1556 First of all it locates all the subterms matched by
1557 patt. In the context of each matched subterm it
1558 disambiguates the term t and reduces it to its red
1559 normal form; then it replaces with t every occurrence
1560 of the normal form in the matched subterm.
1562 New sequents to prove:
1564 _________________________________________________________
1574 The conclusion of the current sequent must be a linear
1575 inequation over real numbers taken from standard
1576 library of Coq. Moreover the inequations in the
1577 hypotheses must imply the inequation in the conclusion
1578 of the current sequent.
1581 It closes the current sequent by applying the Fourier
1584 New sequents to prove:
1586 _________________________________________________________
1590 fwd H as H[0] ... H[n]
1593 fwd id [as id [id]â¦]
1596 The type of H must be the premise of a forward
1597 simplification theorem.
1600 This tactic is under development. It simplifies the
1601 current context by removing H using the following
1602 methods: forward application (by lapply) of a suitable
1603 simplification theorem, chosen automatically, of which
1604 the type of H is a premise, decomposition (by
1605 decompose), rewriting (by rewrite). H[0] ... H[n] are
1606 passed to the tactics fwd invokes, as names for the
1607 premise they introduce.
1609 New sequents to prove:
1610 The ones opened by the tactics fwd invokes.
1611 _________________________________________________________
1615 generalize patt as H
1618 generalize pattern [as id]
1621 All the terms matched by patt must be convertible and
1622 close in the context of the current sequent.
1625 It closes the current sequent by applying a stronger
1626 lemma that is proved using the new generated sequent.
1628 New sequents to prove:
1629 It opens a new sequent where the current sequent
1630 conclusion G is generalized to âx.G{x/t} where {x/t} is
1631 a notation for the replacement with x of all the
1632 occurrences of the term t matched by patt. If patt
1633 matches no subterm then t is defined as the wanted part
1635 _________________________________________________________
1648 This identity tactic does nothing without failing.
1650 New sequents to prove:
1652 _________________________________________________________
1662 The conclusion of the sequent to prove must be an
1663 implication or a universal quantification.
1666 It applies the right introduction rule for implication,
1667 closing the current sequent.
1669 New sequents to prove:
1670 It opens a new sequent to prove adding to the
1671 hypothesis the antecedent of the implication and
1672 setting the conclusion to the consequent of the
1673 implicaiton. The name of the new hypothesis is H if
1674 provided; otherwise it is automatically generated.
1675 _________________________________________________________
1685 If hyps specifies a number of hypotheses to introduce,
1686 then the conclusion of the current sequent must be
1687 formed by at least that number of imbricated
1688 implications or universal quantifications.
1691 It applies several times the right introduction rule
1692 for implication, closing the current sequent.
1694 New sequents to prove:
1695 It opens a new sequent to prove adding a number of new
1696 hypotheses equal to the number of new hypotheses
1697 requested. If the user does not request a precise
1698 number of new hypotheses, it adds as many hypotheses as
1699 possible. The name of each new hypothesis is either
1700 popped from the user provided list of names, or it is
1701 automatically generated when the list is (or becomes)
1703 _________________________________________________________
1713 The type of the term t must be an inductive type or the
1714 application of an inductive type.
1717 It proceeds by cases on t paying attention to the
1718 constraints imposed by the actual "right arguments" of
1721 New sequents to prove:
1722 It opens one new sequent to prove for each case in the
1723 definition of the type of t. With respect to a simple
1724 elimination, each new sequent has additional hypotheses
1725 that states the equalities of the "right parameters" of
1726 the inductive type with terms originally present in the
1728 _________________________________________________________
1732 lapply linear depth=d t to t[1], ..., t[n] as H
1735 lapply [linear] [depth=nat] sterm [to sterm [,stermâ¦]
1739 t must have at least d independent premises and n must
1740 not be greater than d.
1743 Invokes letin H â (t ? ... ?) with enough ?'s to reach
1744 the d-th independent premise of t (d is maximum if
1745 unspecified). Then istantiates (by apply) with t[1],
1746 ..., t[n] the ?'s corresponding to the first n
1747 independent premises of t. Usually the other ?'s
1748 preceding the n-th independent premise of t are
1749 istantiated as a consequence. If the linear flag is
1750 specified and if t, t[1], ..., t[n] are (applications
1751 of) premises in the current context, they are cleared.
1753 New sequents to prove:
1754 The ones opened by the tactics lapply invokes.
1755 _________________________________________________________
1765 The conclusion of the current sequent must be an
1766 inductive type or the application of an inductive type
1767 with at least one constructor.
1770 Equivalent to constructor 1.
1772 New sequents to prove:
1773 It opens a new sequent for each premise of the first
1774 constructor of the inductive type that is the
1775 conclusion of the current sequent. For more details,
1776 see the constructor tactic.
1777 _________________________________________________________
1790 It adds to the context of the current sequent to prove
1791 a new definition x â t.
1793 New sequents to prove:
1795 _________________________________________________________
1808 It replaces all the terms matched by patt with their
1811 New sequents to prove:
1813 _________________________________________________________
1826 It replaces all the terms matched by patt with their
1829 New sequents to prove:
1831 _________________________________________________________
1841 The conclusion of the current sequent must be t=t for
1845 It closes the current sequent by reflexivity of
1848 New sequents to prove:
1850 _________________________________________________________
1857 replace pattern with sterm
1863 It replaces the subterms of the current sequent matched
1864 by patt with the new term t. For each subterm matched
1865 by the pattern, t is disambiguated in the context of
1868 New sequents to prove:
1869 For each matched term t' it opens a new sequent to
1870 prove whose conclusion is t'=t.
1871 _________________________________________________________
1878 rewrite [<|>] sterm pattern
1881 p must be the proof of an equality, possibly under some
1885 It looks in every term matched by patt for all the
1886 occurrences of the left hand side of the equality that
1887 p proves (resp. the right hand side if dir is <). Every
1888 occurence found is replaced with the opposite side of
1891 New sequents to prove:
1892 It opens one new sequent for each hypothesis of the
1893 equality proved by p that is not closed by unification.
1894 _________________________________________________________
1904 The conclusion of the current sequent must be an
1905 inductive type or the application of an inductive type
1906 with at least two constructors.
1909 Equivalent to constructor 2.
1911 New sequents to prove:
1912 It opens a new sequent for each premise of the second
1913 constructor of the inductive type that is the
1914 conclusion of the current sequent. For more details,
1915 see the constructor tactic.
1916 _________________________________________________________
1926 The conclusion of the current sequent must be an
1927 equality over Coq's real numbers that can be proved
1928 using the ring properties of the real numbers only.
1931 It closes the current sequent veryfying the equality by
1932 means of computation (i.e. this is a reflexive tactic,
1933 implemented exploiting the "two level reasoning"
1936 New sequents to prove:
1938 _________________________________________________________
1951 It replaces all the terms matched by patt with other
1952 convertible terms that are supposed to be simpler.
1954 New sequents to prove:
1956 _________________________________________________________
1966 The conclusion of the current sequent must be an
1967 inductive type or the application of an inductive type
1968 with at least one constructor.
1971 Equivalent to constructor 1.
1973 New sequents to prove:
1974 It opens a new sequent for each premise of the first
1975 constructor of the inductive type that is the
1976 conclusion of the current sequent. For more details,
1977 see the constructor tactic.
1978 _________________________________________________________
1991 For each premise of the form H: x = t or H: t = x where
1992 x is a local variable and t does not depend on x, the
1993 tactic rewrites H wherever x appears clearing H and x
1996 New sequents to prove:
1997 The one opened by the applied tactics.
1998 _________________________________________________________
2010 The conclusion of the current proof must be an
2014 It swaps the two sides of the equalityusing the
2017 New sequents to prove:
2019 _________________________________________________________
2029 The conclusion of the current proof must be an
2033 It closes the current sequent by transitivity of the
2036 New sequents to prove:
2037 It opens two new sequents l=t and t=r where l and r are
2038 the left and right hand side of the equality in the
2039 conclusion of the current sequent to prove.
2040 _________________________________________________________
2047 unfold [sterm] pattern
2053 It finds all the occurrences of t (possibly applied to
2054 arguments) in the subterms matched by patt. Then it
2055 δ-expands each occurrence, also performing
2056 β-reduction of the obtained term. If t is omitted it
2057 defaults to each subterm matched by patt.
2059 New sequents to prove:
2061 _________________________________________________________
2074 It replaces all the terms matched by patt with their
2075 βδιζ-weak-head normal form.
2077 New sequents to prove:
2079 _________________________________________________________
2081 Chapter 8. Other commands
2085 alias id "s" = "def"
2087 alias symbol "s" (instance n) = "def"
2089 alias num (instance n) = "def"
2092 alias [id qstring = qstring | symbol qstring [(instance
2093 nat)] = qstring | num [(instance nat)] = qstring ]
2096 Used to give an hint to the disambiguating parser. When
2097 the parser is faced to the identifier (or symbol) s or
2098 to any number, it will prefer interpretations that "map
2099 s (or the number) to def". For identifiers, "def" is
2100 the URI of the interpretation. E.g.:
2101 cic:/matita/nat/nat.ind#xpointer(1/1/1) for the first
2102 constructor of the first inductive type defined in the
2103 block of inductive type(s) cic:/matita/nat/nat.ind. For
2104 symbols and numbers, "def" is the label used to mark
2105 the wanted interpretation.
2107 When a symbol or a number occurs several times in the
2108 term to be parsed, it is possible to give an hint only
2109 for the instance n. When the instance is omitted, the
2110 hint is valid for every occurrence.
2112 Hints are automatically inserted in the script by
2113 Matita every time the user is interactively asked a
2114 question to disambiguate a term. This way the user
2115 won't be posed the same question twice when the script
2116 will be executed again.
2117 _________________________________________________________
2127 Opens a CIC browser window that shows t together with
2128 its type. The command is immediately removed from the
2130 _________________________________________________________
2140 Declares u as an implicit coercion from the type of its
2141 last argument (source) to its codomain (target). Every
2142 time a term x of type source is used with expected type
2143 target, Matita automatically replaces x with (u ? ⦠?
2144 x) to avoid a typing error.
2146 Implicit coercions are not displayed to the user: (u ?
2147 ⦠? x) is rendered simply as x.
2149 When a coercion u is declared from source s to target t
2150 and there is already a coercion u' of target s or
2151 source t, a composite implicit coercion is
2152 automatically computed by Matita.
2153 _________________________________________________________
2157 default "s" u[1] ⦠u[n]
2160 default qstring uri [uri]â¦
2163 It registers a cluster of related definitions and
2164 theorems to be used by tactics and the rendering
2165 engine. Some functionalities of Matita are not
2166 available when some clusters have not been registered.
2167 Overloading a cluster registration is possible: the
2168 last registration will be the default one, but the
2169 previous ones are still in effect.
2171 s is an identifier of the cluster and u[1] ⦠u[n] are
2172 the URIs of the definitions and theorems of the
2173 cluster. The number n of required URIs depends on the
2174 cluster. The following clusters are supported.
2178 name expected object for 1st URI expected object for 2nd URI
2179 expected object for 3rd URI expected object for 4th URI
2180 expected object for 5th URI
2181 equality an inductive type (say, of type eq) of type âA:Type.A
2182 â Prop with one family parameter and one constructor of type
2183 âx:A.eq A x a theorem of type âA.âx,y:A.eq A x y â eq A y x a
2184 theorem of type âA.âx,y,z:A.eq A x y â eq A y z â eq A x z
2185 âA.âa.â P:A â Prop.P x â ây.eq A x y â P y âA.âa.â P:A â
2186 Prop.P x â ây.eq A y x â P y
2187 true an inductive type of type Prop with only one constructor
2188 that has no arguments
2189 false an inductive type of type Prop without constructors
2191 absurd a theorem of type âA:Prop.âB:Prop.A â Not A â B
2192 _________________________________________________________
2202 Displays a list of theorems that can be successfully
2203 applied to the current selected sequent. The command is
2204 removed from the script, but the window that displays
2205 the theorems allow to add to the script the application
2206 of the selected theorem.
2207 _________________________________________________________
2217 Every coercion, notation and interpretation that was
2218 active when the file s was compiled last time is made
2219 active. The same happens for declarations of default
2220 definitions and theorems and disambiguation hints
2221 (aliases). On the contrary, theorem and definitions
2222 declared in a file can be immediately used without
2225 The file s is automatically compiled if it is not
2226 compiled yet and if it is handled by a development.
2227 _________________________________________________________
2235 Not documented (TODO), do not use it.
2236 _________________________________________________________
2246 Sets to s the baseuri of all the theorems and
2247 definitions stated in the current file. The baseuri
2248 should be a/b/c/foo if the file is named foo and it is
2249 in the subtree a/b/c of the current development. This
2250 requirement is not enforced, but it could be in the
2253 Currently, baseuri is the only property that can be set
2254 even if the parser accepts arbitrary property names.
2255 _________________________________________________________
2270 whelp [locate qstring | hint term | elim term | match
2271 term | instance term ]
2274 Performs the corresponding query, showing the result in
2275 the CIC browser. The command is removed from the
2277 _________________________________________________________
2285 Saves and indexes the current interactive theorem or
2286 definition. In order to do this, the set of sequents
2287 still to be proved must be empty.
2288 _________________________________________________________
2292 Both Matita and this document are part of HELM, an
2293 Hypertextual, Electronic Library of Mathematics, developed at
2294 the Computer Science Department, University of Bologna, Italy.
2296 HELM is free software; you can redistribute it and/or modify
2297 it under the terms of the GNU General Public License as
2298 published by the Free Software Foundation; either version 2 of
2299 the License, or (at your option) any later version.
2301 HELM is distributed in the hope that it will be useful, but
2302 WITHOUT ANY WARRANTY; without even the implied warranty of
2303 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
2304 GNU General Public License for more details.
2306 You should have received a copy of the GNU General Public
2307 License along with HELM; if not, write to the Free Software
2308 Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
2309 02110-1301 USA. A copy of the GNU General Public License is
2310 available at this link.
2316 The name of the Development should be the name of the
2317 directory in which it lives. This is not a requirement, but
2318 the makefile automatically generated by matita in the root
2319 directory of the development will eventually generate a new
2320 Development with a name that follows this convention. Having
2321 more than one development for the same set of files is not an