From: Claudio Sacerdoti Coen Date: Tue, 3 Jan 2023 16:32:48 +0000 (+0100) Subject: Manual(s) fixed and committed to avoid rebuilding them in dune X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d29fd4947ea4551f1fa078e56ed2a21b4515536f;p=helm.git Manual(s) fixed and committed to avoid rebuilding them in dune - fixed a bug in the XSLT that used wrong linkends - the HTML and PDF files are now committed to the repository Note: there is a now old (4 years!) but in yelp with links to other pages in XMLDOCs. Not my fault, but most hyperlinks are broken. --- diff --git a/matita/matita/help/C/WrtCoq.html b/matita/matita/help/C/WrtCoq.html new file mode 100644 index 000000000..458323776 --- /dev/null +++ b/matita/matita/help/C/WrtCoq.html @@ -0,0 +1,12 @@ + +Matita vs Coq
Matita vs Coq
Prev Chapter 1. Introduction Next

Matita vs Coq

+ The system shares a common look&feel with the Coq proof assistant + and its graphical user interface. The two systems have variants + of the same logic, + close proof languages and similar sets of tactics. + 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.

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

Prev Up Next
Chapter 1. Introduction Home Chapter 2. Installation
\ No newline at end of file diff --git a/matita/matita/help/C/authoring.html b/matita/matita/help/C/authoring.html new file mode 100644 index 000000000..1bfc17d9b --- /dev/null +++ b/matita/matita/help/C/authoring.html @@ -0,0 +1,50 @@ + +Authoring
Authoring
Prev Chapter 3. Getting started Next

Authoring

How to compile a script

+ Scripts are compiled to base URIs. Base URIs are of the form + "cic:/matita/path" and are given once for all for a set + of scripts using the "root" file. +

+ A "root" file has to be placed in the root of a script set, + for example, consider the following files and directories, and + assume you keep files in "list" separated from files + in "sort" (for example the former directory may contain + functions and proofs about lists, while latter sorting algorithms + for lists): +

+  list/
+    list.ma (* depending just on the standard library *)
+    utils/
+      swap.ma (* including list.ma *)
+  sort/
+    qsort.ma (* including utils/swap.ma *)
+

+ To be able to compile properly the contents of "list" + a file called root has to be placed in it. The file should be like + the following snippet. +

+  baseuri=cic:/matita/mydatastructures
+

+ This file tells Matita that objects generated by + "list.ma" have to be placed in + "cic:/matita/mydatastructures/list" while + objects generated by + "swap.ma" have to be placed in + "cic:/matita/mydatastructures/utils/swap". +

+ Once you created the root file, you must generate a depend file. + Enter the "list" directory (the root of yuor file set) + and type "matitadep". Remember to regenerate the depend file + every time you alter the dependencies of your files (for example + including other scripts). + You can now compile you files typing "matitac". +

+ To compile the "sort" directory, create a root file + in "sort/" like the following one and then run + "matitadep". +

+  baseuri=cic:/matita/myalgorithms
+  include_paths=../list
+

+ The include_paths field can declare a list of paths separated by space. + Please omit any "/" from the end of base URIs or paths. +

The authoring interface

TODO

Prev Up Next
Browsing and searching Home Chapter 4. Syntax
\ No newline at end of file diff --git a/matita/matita/help/C/axiom_definition_declaration.html b/matita/matita/help/C/axiom_definition_declaration.html new file mode 100644 index 000000000..46c879919 --- /dev/null +++ b/matita/matita/help/C/axiom_definition_declaration.html @@ -0,0 +1,57 @@ + +Definitions and declarations
Definitions and declarations
Prev Chapter 4. Syntax Next

Definitions and declarations

axiom id: term

axiom H: P

H is declared as an axiom that states P

definition id[: term] [≝ term]

definition f: T ≝ t

f is defined as t; + T is its type. An error is raised if the type of + t is not convertible to T.

T is inferred from t if + omitted.

t can be omitted only if T is + 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.

discriminator id

discriminator i

Defines a new discrimination (injectivity+conflict) principle à la + McBride for the inductive type i.

The principle will use John + Major's equality if such equality is defined, otherwise it will use + Leibniz equality; in the former case, it will be called + i_jmdiscr, in the latter, i_discr. + The command will fail if neither equality is available.

Discrimination principles are used by the destruct tactic and are + usually automatically generated by Matita during the definition of the + corresponding inductive type. This command is thus especially useful + when the correct equality was not loaded at the time of that + definition.

inverter id for id (path) [term]

inverter n for i (path) : s

Defines a new induction/inversion principle for the inductive type + i, called n.

(path) must be in the form (# # # ... #), + where each # can be either ? or + %, and the number of symbols is equal to the number of + right parameters (indices) of i. Parentheses are + mandatory. If the j-th symbol is + %, Matita will generate a principle providing + equations for reasoning on the j-th index of i. If the + symbol is a ?, no corresponding equation will be + provided.

s, which must be a sort, is the target sort of the + induction/inversion principle and defaults to Prop.

letrec TODO

TODO

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

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.

Prev Up Next
Chapter 4. Syntax Home Proofs
\ No newline at end of file diff --git a/matita/matita/help/C/ch05s02.html b/matita/matita/help/C/ch05s02.html new file mode 100644 index 000000000..e54b1e9a4 --- /dev/null +++ b/matita/matita/help/C/ch05s02.html @@ -0,0 +1,27 @@ + +interpretation
interpretation
Prev Chapter 5. Extending the syntax Next

interpretation

interpretation "description" 'symbol p1 … pn = + rhs

+

Synopsis:

interpretation + qstring csymbol [interpretation_argument]… + = + interpretation_rhs +

Action:

It declares a bi-directional mapping {…} between the content-level AST 'symbol t1 … tn and the semantic term rhs[{t1}/p1;…;{tn}/pn] + (the simultaneous substitution in rhs of the + interpretation {…} of every content-level + actual argument ti for its + corresponding formal parameter + pi). The + description must be a textual description of the + meaning associated to 'symbol by this + interpretation, and is used by the user interface of Matita to + provide feedback on the interpretation of ambiguous terms. +

Interpretation arguments:

Table 5.11. interpretation_argument

interpretation_argument::=[η.]… idA formal parameter. If the name of the formal parameter is + prefixed by n symbols "η", then the mapping performs + (multiple) η-expansions to grant that the semantic actual + parameter begins with at least n λ-abstractions.

Table 5.12. interpretation_rhs

interpretation_rhs::=uriA constant, specified by its URI
 |idA constant, specified by its name, or a bound variable. If + the constant name is ambiguous, the one corresponding to the + last implicitly or explicitly specified alias is used.
 |?An implicit parameter
 |( + interpretation_rhs + [interpretation_rhs]… + )An application

+

Prev Up Next
Chapter 5. Extending the syntax Home Chapter 6. Tacticals
\ No newline at end of file diff --git a/matita/matita/help/C/cicbrowser.html b/matita/matita/help/C/cicbrowser.html new file mode 100644 index 000000000..83f228299 --- /dev/null +++ b/matita/matita/help/C/cicbrowser.html @@ -0,0 +1,18 @@ + +Browsing and searching
Browsing and searching
Prev Chapter 3. Getting started Next

Browsing and searching

The CIC browser is used to browse and search the library. + You can open a new CIC browser selecting "New Cic Browser" + from the "View" menu of Matita, or by pressing "F3". + The CIC browser is similar to a traditional Web browser.

Browsing the library

To browse the library, type in the location bar the absolute URI of + 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.

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

Prev Up Next
Chapter 3. Getting started Home Authoring
\ No newline at end of file diff --git a/matita/matita/help/C/command_check.html b/matita/matita/help/C/command_check.html new file mode 100644 index 000000000..022fea317 --- /dev/null +++ b/matita/matita/help/C/command_check.html @@ -0,0 +1,6 @@ + +check
check
Prev Chapter 9. Other commands Next

check

check t

+

Synopsis:

check sterm

Action:

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

+

Prev Up Next
Chapter 9. Other commands Home coercion
\ No newline at end of file diff --git a/matita/matita/help/C/command_coercion.html b/matita/matita/help/C/command_coercion.html new file mode 100644 index 000000000..a1a0b6841 --- /dev/null +++ b/matita/matita/help/C/command_coercion.html @@ -0,0 +1,52 @@ + +coercion
coercion
Prev Chapter 9. Other commands Next

coercion

coercion nocomposites c : ty ≝ u on s : S to T

+

Synopsis:

+ coercion + [ nocomposites ] id + [ : term ≝ term + on + id : term + to term ] +

Action:

Declares c as an implicit coercion. + If only c is given, u + is the constant named by c, + ty its declared type, + s the name of the last variable abstracted in + in ty, S the type of + this last variable and T the target of + ty. The user can specify all these component to + have full control on how the coercion is indexed. + The type of the body of the coercion u must be + convertible to the declared one ty. Let it be + ∀x1:T1. … ∀x(n-1):T(n-1).Tn. + Then s must be one of x1 … + xn (possibly prefixed by _ + if the product is non dependent). Let s + be xi in the following. + Then S must be Ti + where all bound variables are replaced by ?, + and T must be Tn + where all bound variable are replaced by ?. + For example the following command + declares a coercions from vectors of any length to lists of + natural numbers.

coercion nocomposites v2l : ∀n:nat.∀v:Vect nat n. + List nat ≝ l_of_v on _v : Vect nat ? to List nat

Every time a term x + of a type that matches S + (Vect nat ? here) + is used with an expected + type that matches T + (List nat here), Matita + automatically replaces x with + (u ? … ? x ? … ?) to avoid a typing error. + Note that the position of x is determined by + s.

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 unless nocomposites + is specified.

Note that Vect nat ? can be replaced with + Vect ? ? to index the coercion is a loose way.

+

Prev Up Next
check Home include
\ No newline at end of file diff --git a/matita/matita/help/C/command_include.html b/matita/matita/help/C/command_include.html new file mode 100644 index 000000000..52eb85bb6 --- /dev/null +++ b/matita/matita/help/C/command_include.html @@ -0,0 +1,17 @@ + +include
include
Prev Chapter 9. Other commands Next

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

+ If the file s was already included, either + directly or recursively, the commands does nothing. +

+

Prev Up Next
coercion Home include alias
\ No newline at end of file diff --git a/matita/matita/help/C/command_include_alias.html b/matita/matita/help/C/command_include_alias.html new file mode 100644 index 000000000..e3d105332 --- /dev/null +++ b/matita/matita/help/C/command_include_alias.html @@ -0,0 +1,8 @@ + +include alias
include alias
Prev Chapter 9. Other commands Next

include alias

include alias "s"

+

Synopsis:

include alias qstring

Action:

Every + interpretation + declared in the file s is re-declared + so to make it the preferred choice for disambiguation. +

+

Prev Up Next
include Home qed
\ No newline at end of file diff --git a/matita/matita/help/C/command_qed.html b/matita/matita/help/C/command_qed.html new file mode 100644 index 000000000..20cdfade2 --- /dev/null +++ b/matita/matita/help/C/command_qed.html @@ -0,0 +1,8 @@ + +qed
qed
Prev Chapter 9. Other commands Next

qed

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.

+

Prev Up Next
include alias Home qed-
\ No newline at end of file diff --git a/matita/matita/help/C/command_qed_minus.html b/matita/matita/help/C/command_qed_minus.html new file mode 100644 index 000000000..a0ea58391 --- /dev/null +++ b/matita/matita/help/C/command_qed_minus.html @@ -0,0 +1,9 @@ + +qed-
qed-
Prev Chapter 9. Other commands Next

qed-

qed-

+

Synopsis:

qed- +

Action:

Saves the current interactive theorem or + definition without indexing. Therefore automation will ignore + it. + In order to do this, the set of sequents still to be proved + must be empty.

+

Prev Up Next
qed Home unification hint
\ No newline at end of file diff --git a/matita/matita/help/C/command_unification_hint.html b/matita/matita/help/C/command_unification_hint.html new file mode 100644 index 000000000..a43f21e0f --- /dev/null +++ b/matita/matita/help/C/command_unification_hint.html @@ -0,0 +1,17 @@ + +unification hint
unification hint
Prev Chapter 9. Other commands Next

unification hint

unification hint n ≔ v1 : T1,… vi : Ti; h1 ≟ t1, … hn ≟ tn ⊢ tl ≡ tr.

+

Synopsis:

+ unification hint + nat + ≔ + [ id [ : term ] ,.. ] + ; + [ id ≟ term ,.. ] + ⊢ + term ≡ term +

Action:

Declares the hint at precedence n

The file hints_declaration.ma must be + included to declare hints with that syntax.

Unification hints are described in the paper + "Hints in unification" by + Asperti, Ricciotti, Sacerdoti and Tassi. +

+

Prev Up Next
qed- Home universe constraint
\ No newline at end of file diff --git a/matita/matita/help/C/command_universe_constraints.html b/matita/matita/help/C/command_universe_constraints.html new file mode 100644 index 000000000..5c7d8fa87 --- /dev/null +++ b/matita/matita/help/C/command_universe_constraints.html @@ -0,0 +1,2 @@ + +universe constraint
universe constraint
Prev Chapter 9. Other commands Next

universe constraint

TODO

Prev Up Next
unification hint Home Chapter 10. License
\ No newline at end of file diff --git a/matita/matita/help/C/declarative_tactics_quickref.xml b/matita/matita/help/C/declarative_tactics_quickref.xml index 1f16a4725..79ab7a534 100644 --- a/matita/matita/help/C/declarative_tactics_quickref.xml +++ b/matita/matita/help/C/declarative_tactics_quickref.xml @@ -1,6 +1,101 @@ tactics - + + + &tactic; + ::= + + = term [auto_params | using term | using once term | proof] [done] + + + + + | + assume id : + sterm + + + + | + by induction hypothesis we know term ( id ) + + + + | + case id [( id : term )] … [( id : term )] + + + + | + conclude term + + + + | + justification done + + + + | + justification let id + : term such that term + ( id ) + + + + | + let id = term + + + + | + obtain id term + + + + | + suppose term ( id + ) + + + + | + + that is equivalent to term + + + + + | + the thesis becomes term + + + + | + we need to prove term + [(id + )] + + + + + | + we proceed by cases on term to prove term + + + + | + we proceed by induction on term to prove term + + + + | + justification we proved term + [( id + )] + + +
diff --git a/matita/matita/help/C/index.html b/matita/matita/help/C/index.html new file mode 100644 index 000000000..2f15104d1 --- /dev/null +++ b/matita/matita/help/C/index.html @@ -0,0 +1,9 @@ + +Matita V0.99.5 User Manual (rev. 0.99.5 )
Matita V0.99.5 + User Manual (rev. 0.99.5 +)
   Next

Matita V0.99.5 + User Manual (rev. 0.99.5 +)

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 10, License for more information.

Revision: 0.99.5 +, 12/07/2006

Table of Contents

1. Introduction
Features
Matita vs Coq
2. Installation
Using the LiveCD
Creating the virtual machine
Sharing files with the real PC
Installing from sources
Getting the source code
Requirements
Compiling and installing
3. Getting started
How to type Unicode symbols
Browsing and searching
Browsing the library
Looking at a proof under development
Authoring
How to compile a script
The authoring interface
4. Syntax
Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
discriminator
inverter
TODO
(co)inductive types declaration
record
Proofs
theorem
corollary
lemma
fact
example
Tactic arguments
pattern
reduction-kind
auto-params
justification
5. Extending the syntax
notation
interpretation
6. Tacticals
Interactive proofs and definitions
The proof status
Tacticals
7. Tactics
Quick reference card
@
//
#
#_
##
-
%
*
>
applyS
assumption
cases
change
cut
destruct
elim
generalize
inversion
lapply
letin
normalize
whd
8. Declarative Tactics
Quick reference card
assume
suppose
letin
that is equivalent to
the thesis becomes
we need to prove
we proved
let such that
we have
we proceed by induction on
we proceed by cases on
case
by induction hypothesis we know
conclude
obtain
=
done
9. Other commands
alias
check
coercion
include
include alias
qed
qed-
unification hint
universe constraint
10. License

List of Figures

2.1. The brand new virtual machine
2.2. Mounting an ISO image
2.3. Choosing the ISO image
2.4. Choosing the ISO image
2.5. Set up a shared folder
2.6. Choosing the folder to share
2.7. Naming the shared folder
2.8. Using it from the virtual machine

List of Tables

4.1. qstring
4.2. id
4.3. nat
4.4. char
4.5. uri-step
4.6. uri
4.7. csymbol
4.8. symbol
4.9. Terms
4.10. Simple terms
4.11. Arguments
4.12. Pattern matching
4.13. pattern
4.14. path
4.15. reduction-kind
4.16. auto-params
4.17. simple-auto-param
4.18. justification
5.1. usage
5.2. associativity
5.3. notation_rhs
5.4. unparsed_ast
5.5. enriched_term
5.6. unparsed_meta
5.7. level2_meta
5.8. notation_lhs
5.9. layout
5.10. literal
5.11. interpretation_argument
5.12. interpretation_rhs
6.1. proof script
6.2. proof steps
6.3. tactics and LCF tacticals
7.1. tactics
8.1. tactics
   Next
   Chapter 1. Introduction
\ No newline at end of file diff --git a/matita/matita/help/C/inst_from_src.html b/matita/matita/help/C/inst_from_src.html new file mode 100644 index 000000000..dd4050c43 --- /dev/null +++ b/matita/matita/help/C/inst_from_src.html @@ -0,0 +1,89 @@ + +Installing from sources
Installing from sources
Prev Chapter 2. Installation Next

Installing from sources

Install Matita from the sources is hard, you have been warned! +

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.

+

Requirements

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

Note for Debian (and derivatives) users

If you are running a + Debian GNU/Linux + distribution, + or any of its derivative like Ubuntu, + you can use APT to install all the required tools and + libraries since they are all part of the Debian archive. +

+ apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev liblablgtk2-ocaml-dev liblablgtkmathview-ocaml-dev liblablgtksourceview-ocaml-dev libsqlite3-ocaml-dev libocamlnet-ocaml-dev libzip-ocaml-dev libhttp-ocaml-dev ocaml-ulex08 libexpat-ocaml-dev libmysql-ocaml-dev camlp5 +

+ An official debian package is going to be added to the + archive too. +

+ +

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

+ LablGTK + +

OCaml bindings for the GTK+ library + , version 2.6.0 or above

+ GtkSourceView + + , + LablGtkSourceView + +

extension for the GTK+ text widget (adding the typical + features of source code editors) and its OCaml bindings

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

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 +

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

Prev Up Next
Chapter 2. Installation Home Chapter 3. Getting started
\ No newline at end of file diff --git a/matita/matita/help/C/macro_intro.html b/matita/matita/help/C/macro_intro.html new file mode 100644 index 000000000..ff7a79ab7 --- /dev/null +++ b/matita/matita/help/C/macro_intro.html @@ -0,0 +1,7 @@ + +macro_input
macro_input
Prev Chapter 7. Tactics Next

macro_input

##

+

Synopsis:

##

Pre-conditions:

None.

Action:

This macro expands to the longest possible list of + #Hi tactics. The + names of the introduced hypotheses are automatically + generated.

+

Prev Up Next
intro_clear Home clear
\ No newline at end of file diff --git a/matita/matita/help/C/matita.pdf b/matita/matita/help/C/matita.pdf new file mode 100644 index 000000000..67cbf2b4e Binary files /dev/null and b/matita/matita/help/C/matita.pdf differ diff --git a/matita/matita/help/C/proofs.html b/matita/matita/help/C/proofs.html new file mode 100644 index 000000000..4eea6a61d --- /dev/null +++ b/matita/matita/help/C/proofs.html @@ -0,0 +1,7 @@ + +Proofs
Proofs
Prev Chapter 4. Syntax Next

Proofs

theorem id[: term] [≝ term]

theorem f: P ≝ p

Proves a new theorem f whose thesis is + P.

If p is provided, it must be a proof term for + P. Otherwise an interactive proof is started.

P can be omitted only if the proof is not + interactive.

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.

corollary id[: term] [≝ term]

corollary f: T ≝ t

Same as theorem f: T ≝ t

lemma id[: term] [≝ term]

lemma f: T ≝ t

Same as theorem f: T ≝ t

fact id[: term] [≝ term]

fact f: T ≝ t

Same as theorem f: T ≝ t

example id[: term] [≝ term]

example f: T ≝ t

Same as theorem f: T ≝ t, but the example + is not indexed nor used by automation.

Prev Up Next
Definitions and declarations Home Tactic arguments
\ No newline at end of file diff --git a/matita/matita/help/C/proofstatus.html b/matita/matita/help/C/proofstatus.html new file mode 100644 index 000000000..2eb55cd56 --- /dev/null +++ b/matita/matita/help/C/proofstatus.html @@ -0,0 +1,47 @@ + +The proof status
The proof status
Prev Chapter 6. Tacticals Next

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

Prev Up Next
Chapter 6. Tacticals Home Tacticals
\ No newline at end of file diff --git a/matita/matita/help/C/sec_commands.html b/matita/matita/help/C/sec_commands.html new file mode 100644 index 000000000..ec82fba4b --- /dev/null +++ b/matita/matita/help/C/sec_commands.html @@ -0,0 +1,30 @@ + +Chapter 9. Other commands
Chapter 9. Other commands
Prev   Next

Chapter 9. Other commands

Table of Contents

alias
check
coercion
include
include alias
qed
qed-
unification hint
universe constraint

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.

+

Prev   Next
done Home check
\ No newline at end of file diff --git a/matita/matita/help/C/sec_declarative_tactics.html b/matita/matita/help/C/sec_declarative_tactics.html new file mode 100644 index 000000000..bc750f282 --- /dev/null +++ b/matita/matita/help/C/sec_declarative_tactics.html @@ -0,0 +1,19 @@ + +Chapter 8. Declarative Tactics
Chapter 8. Declarative Tactics
Prev   Next

Chapter 8. Declarative Tactics

Table of Contents

Quick reference card
assume
suppose
letin
that is equivalent to
the thesis becomes
we need to prove
we proved
let such that
we have
we proceed by induction on
we proceed by cases on
case
by induction hypothesis we know
conclude
obtain
=
done

Quick reference card

+

Table 8.1. tactics

tactic::= + = term [auto_params | using term | using once term | proof] [done] +
 |assume id : + sterm
 |by induction hypothesis we know term ( id )
 |case id [( id : term )] … [( id : term )]
 |conclude term
 |justification done
 |justification let id + : term such that term + ( id )
 |let id = term
 |obtain id term
 |suppose term ( id + )
 | + that is equivalent to term +
 |the thesis becomes term
 |we need to prove term + [(id + )] +
 |we proceed by cases on term to prove term
 |we proceed by induction on term to prove term
 |justification we proved term + [( id + )] +


+ +

Prev   Next
whd Home assume
\ No newline at end of file diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml index 76acf5e0a..7ef8c7ee6 100644 --- a/matita/matita/help/C/sec_declarative_tactics.xml +++ b/matita/matita/help/C/sec_declarative_tactics.xml @@ -582,7 +582,7 @@ - + = = = t2 justification diff --git a/matita/matita/help/C/sec_gettingstarted.html b/matita/matita/help/C/sec_gettingstarted.html new file mode 100644 index 000000000..5644f20c3 --- /dev/null +++ b/matita/matita/help/C/sec_gettingstarted.html @@ -0,0 +1,30 @@ + +Chapter 3. Getting started
Chapter 3. Getting started
Prev   Next

Chapter 3. Getting started

Table of Contents

How to type Unicode symbols
Browsing and searching
Browsing the library
Looking at a proof under development
Authoring
How to compile a script
The authoring interface

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.

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 or an + ASCII art resembling the shape of the character. Pressing + "Alt+L" or Space or Enter just after the last character + of the name converts + the ligature to the Unicode symbol. + E.g. "\Delta" followed by Alt+L generates + "Δ", while pressing Alt-L after "=>" generates + "⇒"

  • Typing a symbol and rotating trough its equivalence class + with Alt-L. E.g. pressing Alt-L after an "l" + generates a "λ", while pressing Alt-L after an + "→" once generates "⇉" and pressing + Alt-L again generates "⇒". +

+ The comprehensive list of symbols names or shortcuts and their equivalence + classes is available clicking on the "TeX/UTF-8 table" item + of the "View" menu. +

+ There is a memory mechanism related to equivalence classes that + remembers your last choice, making it the default one. For example, + if you use "_" to generate "⎻" + (that is the third choice, after "⎽" and "⎼"), + the next time you type Alt-L + after "_" you immediately get "⎻". +

Prev   Next
Installing from sources Home Browsing and searching
\ No newline at end of file diff --git a/matita/matita/help/C/sec_install.html b/matita/matita/help/C/sec_install.html new file mode 100644 index 000000000..51e24426a --- /dev/null +++ b/matita/matita/help/C/sec_install.html @@ -0,0 +1,84 @@ + +Chapter 2. Installation
Chapter 2. Installation
Prev   Next

Chapter 2. Installation

Table of Contents

Using the LiveCD
Creating the virtual machine
Sharing files with the real PC
Installing from sources
Getting the source code
Requirements
Compiling and installing

+ Matita is a quite complex piece of software, we thus recommend + you to either install al precompiled version or use the LiveCD. + If you are running Debian GNU/Linux (or one of its derivatives + like Ubuntu), you can install matita typing + 

 aptitude install matita matita-standard-library

+ If you are running MacOSX or Windows, give the LiveCD a try before + trying to compile Matita from its sources. +

Using the LiveCD

+ In the following, we will assume you have installed + virtualbox + for your platform and downloaded the .iso image of the LiveCD +

Creating the virtual machine

+ Click on the New button, a wizard will popup, you should ask to + its questions as follows +

  1. + The name should be something like Matita, but can + be any meaningful string. +

  2. + The OS type should be Debian +

  3. + The base memory size can be 256 mega bytes, but you may + want to increase it if you are going to work with huge + formalizations. +

  4. + The boot hard disk should be no hard disk. It may complain + that this choice is not common, but it is right, since you + will run a LiveCD you do not need to emulate an hard drive. +

+ Now that you are done with the creation of the virtual machine, + you need to insert the LiveCD in the virtual cd reader unit. +

Figure 2.1. The brand new virtual machine

The breand new virtual machine

+ Click on CD/DVD-ROM (that should display something like: Not mouted). + Then click on mount CD/DVD drive and select the ISO image + option. The combo-box should display no available image, you need to + add the ISO image you downloaded from the Matita website clicking on + the button near the combo-box. + to start the virtual machine. +

Figure 2.2. Mounting an ISO image

Mounting an ISO image

+ In the newely opened window click + the Add button +

Figure 2.3. Choosing the ISO image

Choosing the ISO image

+ A new windows will pop-up: choose the file you downloaded + (usually matita-version.iso) and click open. +

Figure 2.4. Choosing the ISO image

Choosing the ISO image

+ Now select the new entry you just added as the CD image + you want to insert in the virtual CD drive. + You are now ready to start the virtual machine. +

Sharing files with the real PC

+ The virtual machine Matita will run on, has its own file + system, that is completely separated from the one of your + real PC (thus your files are not available in the + emulated environment) and moreover it is a non-presistent + file system (thus you data is lost every time you + turn off the virtual machine). +

+ Virtualbox allows you to share a real folder (beloging + to your real PC) with the emulated computer. Since this + folder is persistent, you are encouraged to put + your work there, so that it is not lost when the virtual + machine is powered off. +

+ The first step to set up a shared folder is to click + on the shared folder configuration entry + of the virtual machine. +

Figure 2.5. Set up a shared folder

Shared folder

+ Then you shuld add a shared folder clicking on the + plus icon on the right +

Figure 2.6. Choosing the folder to share

Shared folder

+ Then you have to specify the real PC folder you want to share + and name it. A reasonable folder to share is /home on + a standard Unix system, while /Users on MaxOSX. + The name you give to the share is important, you should + remember it. +

Figure 2.7. Naming the shared folder

Shared folder

+ Once your virtual machine is up and running, you can + mount (that meand have access to) the shared folder + by clicking on the Mount VirtualBox share icon, and typing + the name of the share. +

Figure 2.8. Using it from the virtual machine

Shared folder at work

+ A window will then pop-up, and its content will be the + the content of the real PC folder. +

Prev   Next
Matita vs Coq Home Installing from sources
\ No newline at end of file diff --git a/matita/matita/help/C/sec_intro.html b/matita/matita/help/C/sec_intro.html new file mode 100644 index 000000000..a967fff1a --- /dev/null +++ b/matita/matita/help/C/sec_intro.html @@ -0,0 +1,7 @@ + +Chapter 1. Introduction
Chapter 1. Introduction
Prev   Next

Chapter 1. Introduction

Table of Contents

Features
Matita vs Coq

Features

Matita is an interactive theorem prover + (or proof assistant) with the following characteristics:

  • It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.

  • It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.

  • It has a stand-alone graphical user interface (GUI) inspired by +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 via Unicode.

  • It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.

Prev   Next
Matita V0.99.5 + User Manual (rev. 0.99.5 +) Home Matita vs Coq
\ No newline at end of file diff --git a/matita/matita/help/C/sec_license.html b/matita/matita/help/C/sec_license.html new file mode 100644 index 000000000..72ca1d932 --- /dev/null +++ b/matita/matita/help/C/sec_license.html @@ -0,0 +1,13 @@ + +Chapter 10. License
Chapter 10. License
Prev   

Chapter 10. License

Both Matita and this document are part of HELM, an Hypertextual, + Electronic Library of Mathematics, developed at the Computer Science + Department, University of Bologna, Italy.

HELM is free software; you can redistribute it and/or modify it under + the terms of the GNU General Public License as published by the Free Software + Foundation; either version 2 of the License, or (at your option) any later + version.

HELM is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR + A PARTICULAR PURPOSE. See the GNU General Public License for more details. +

You should have received a copy of the GNU General Public License along + with HELM; if not, write to the Free Software Foundation, Inc., 51 Franklin + St, Fifth Floor, Boston, MA 02110-1301 USA. A copy of the GNU General + Public License is available at this link.

Prev   
universe constraint Home 
\ No newline at end of file diff --git a/matita/matita/help/C/sec_tacticals.html b/matita/matita/help/C/sec_tacticals.html new file mode 100644 index 000000000..f79c77c49 --- /dev/null +++ b/matita/matita/help/C/sec_tacticals.html @@ -0,0 +1,20 @@ + +Chapter 6. Tacticals
Chapter 6. Tacticals
Prev   Next

Chapter 6. Tacticals

Table of Contents

Interactive proofs and definitions
The proof status
Tacticals

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.

Prev   Next
interpretation Home The proof status
\ No newline at end of file diff --git a/matita/matita/help/C/sec_tactics.html b/matita/matita/help/C/sec_tactics.html new file mode 100644 index 000000000..c4f036674 --- /dev/null +++ b/matita/matita/help/C/sec_tactics.html @@ -0,0 +1,31 @@ + +Chapter 7. Tactics
Chapter 7. Tactics
Prev   Next

Chapter 7. Tactics

Table of Contents

Quick reference card
@
//
#
#_
##
-
%
*
>
applyS
assumption
cases
change
cut
destruct
elim
generalize
inversion
lapply
letin
normalize
whd

Quick reference card

+

Table 7.1. tactics

tactic::=@ sterm
 |applyS sterm auto_params
 | + + assumption + +
 |/auto_params/.
 | + cases + term pattern +
 |change pattern with sterm
 | + -id +
 |% [nat] [{sterm…}]
 |cut sterm
 | + * + [as id] +
 |destruct + [(id…)] [skip (id…)]
 |elim sterm pattern
 |generalize pattern
 | + # + + id + +
 | + #_ +
 |inversion sterm
 | + lapply + sterm +
 |letin id ≝ sterm
 | + ## +
 |normalize pattern + [nodelta]
 |[<|>] sterm pattern
 |whd pattern [nodelta]


+ +

Prev   Next
Tacticals Home apply
\ No newline at end of file diff --git a/matita/matita/help/C/sec_terms.html b/matita/matita/help/C/sec_terms.html new file mode 100644 index 000000000..151c909c8 --- /dev/null +++ b/matita/matita/help/C/sec_terms.html @@ -0,0 +1,53 @@ + +Chapter 4. Syntax
Chapter 4. Syntax
Prev   Next

Chapter 4. Syntax

Table of Contents

Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
discriminator
inverter
TODO
(co)inductive types declaration
record
Proofs
theorem
corollary
lemma
fact
example
Tactic arguments
pattern
reduction-kind
auto-params
justification

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_-]

Terms & co.

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]…)] 

Table 4.7. csymbol

csymbol::='id 

Table 4.8. symbol

symbol::=〈〈None of the above〉〉 

Terms

+

Table 4.9. Terms

term::=stermsimple or delimited term
 |term termapplication
 |λargs.termλ-abstraction
 |Πargs.termdependent product meant to define a datatype
 |∀args.termdependent product meant to define a proposition
 |term → termnon-dependent product (logical implication or function space)
 |let [id|(id: term)] ≝ term in termlocal definition
 | + let + [co]rec + rec_def + (co)recursive definitions
   + [and rec_def]… +  
   + in term +  
 |…user provided notation
rec_def::= + id [id|_|(id[,id]… :term)]… +  
   + [on id] + [: term] + ≝ term] +  


+ +

Table 4.10. Simple terms

sterm::=(term) 
 |id[\subst[ + id≔term + [;id≔term]… + ]] + identifier with optional explicit named substitution
 |uria qualified reference
 |Propthe impredicative sort of propositions
 |Setthe impredicate sort of datatypes
 |CPropone fixed predicative sort of constructive propositions
 |Typeone predicative sort of datatypes
 |?implicit argument
 |?n + [[ + [_|term]… + ]]metavariable
 |match term + [ in id ] + [ return term ] + with + case analysis
   + [ + match_branch[|match_branch]… + ] +  
 |(term:term)cast
 |…user provided notation at precedence 90


+ +

Table 4.11. Arguments

args::= + _[: term] + ignored argument
 | + (_[: term]) + ignored argument
 |id[,id]…[: term] 
 |(id[,id]…[: term]) 
args2::=id 
 |(id[,id]…: term) 


+ +

Table 4.12. Pattern matching

match_branch::=match_pattern ⇒ term 
match_pattern::=id0-ary constructor
 |(id id [id]…)n-ary constructor (binds the n arguments)
 |id id [id]…n-ary constructor (binds the n arguments)
 |_any remaining constructor (ignoring its arguments)


+

Prev   Next
Authoring Home Definitions and declarations
\ No newline at end of file diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml index dbb6900d9..67603c55d 100644 --- a/matita/matita/help/C/sec_terms.xml +++ b/matita/matita/help/C/sec_terms.xml @@ -849,7 +849,6 @@ - diff --git a/matita/matita/help/C/sec_usernotation.html b/matita/matita/help/C/sec_usernotation.html new file mode 100644 index 000000000..804e99eff --- /dev/null +++ b/matita/matita/help/C/sec_usernotation.html @@ -0,0 +1,36 @@ + +Chapter 5. Extending the syntax
Chapter 5. Extending the syntax
Prev   Next

Chapter 5. Extending the syntax

Table of Contents

notation
interpretation

notation

notation usage "presentation" associativity with precedence p for content

+

Synopsis:

notation + [usage] "notation_lhs" [associativity] with precedence nat + for + notation_rhs +

Action:

Declares a mapping between the presentation + AST presentation and the content AST + content. The declared presentation AST fragment + presentation is at precedence level + p. The precedence level is used to determine where + parentheses must be inserted. In particular, the content AST fragment + content is actually a pattern, since it contains + placeholders (variables) for sub-ASTs. Every placeholder for a term + is given an expected precedence level. Parentheses must be inserted + around sub-ASTs having a precedence level strictly smaller than the + expected one.

If presentation describes a binary + infix operator and if no precedence level is explicitly given for the + operator arguments, an associativity declaration + can be given to automatically choose the right level for the operands. + Otherwise, no associativity can be given.

If direction is + omitted, the mapping is bi-directional and is used both during + parsing and pretty-printing of terms. If direction + is >, the mapping is used only during parsing; + if it is <, it is used only during + pretty-printing. Thus it is possible to use simple notations to type + for writing the term, and nicer ones for rendering it.

Notation arguments:

Table 5.1. usage

usage::=<Only for pretty-printing
 |>Only for parsing

Table 5.2. associativity

associativity::=left associativeLeft associative
 |right associativeRight associative
 |non associativeNon associative (default)

Table 5.3. notation_rhs

notation_rhs::=unparsed_astTODO
 |unparsed_metaTODO

Table 5.4. unparsed_ast

unparsed_ast::=@{enriched_term}A content level AST (a term which is parsed, but not disambiguated).
 |@id@id is just an abbreviation for @{id}
 |@csymbol@'symbol is just an abbreviation for @{'symbol}

Table 5.5. enriched_term

enriched_term::=〈〈A term that may contain occurrences of unparsed_meta, even as variable names in binders, and occurrences of csymbol〉〉TODO

Table 5.6. unparsed_meta

unparsed_meta::=${level2_meta}TODO
 |$id$id is just an abbreviation for ${id}
 |$_$_ is just an abbreviation for ${_}

Table 5.7. level2_meta

level2_meta::=unparsed_astTODO
 |term nat idTODO
 |number idTODO
 |ident idTODO
 |fresh idTODO
 |anonymousTODO
 |idTODO
 |fold [left|right] level2_meta rec id level2_metaTODO
 |default level2_meta level2_metaTODO
 |if level2_meta then level2_meta else level2_metaTODO
 |failTODO

Table 5.8. notation_lhs

notation_lhs::=layout [layout]… 

Table 5.9. layout

layout::=layout \sub layoutSubscript
 |layout \sup layoutSuperscript
 |layout \below layout 
 |layout \above layout 
 |layout \over layout 
 |layout \atop layout 
 |layout \frac layoutFraction
 |\infrule layout layout layoutInference rule (premises, conclusion, rule name)
 |\sqrt layoutSquare root
 |\root layout \of layoutGeneralized root
 |hbox ( layout [layout]… )Horizontal box
 |vbox ( layout [layout]… )Vertical box
 |hvbox ( layout [layout]… )Horizontal and vertical box
 |hovbox ( layout [layout]… )Horizontal or vertical box
 |breakBreakable space
 |( layout [layout]… )Group
 |idPlaceholder for a term with no explicit precedence
 |term nat idPlaceholder for a term with explicit expected precedence
 |number idPlaceholder for a natural number
 |ident idPlaceholder for an identifier
 |literalLiteral
 |opt layoutOptional layout (it can be omitted for parsing)
 |list0 layout + [sep literal]List of layouts separated by sep (default: + any blank)
 |list1 layout + [sep literal]Non empty list of layouts separated by sep + (default: any blank)
 |mstyle id value (layout) + Style attributes like color #ff0000
 |mpadded id value (layout) + padding attributes like width -150%
 |maction (layout) + [ (layout) … ] + Alternative notations (output only)

Table 5.10. literal

literal::=symbolUnicode symbol
 |natNatural number (a constant)
 |'id'New keyword for the lexer

+

Prev   Next
Tactic arguments Home interpretation
\ No newline at end of file diff --git a/matita/matita/help/C/tac_andelim.html b/matita/matita/help/C/tac_andelim.html new file mode 100644 index 000000000..10d9b1010 --- /dev/null +++ b/matita/matita/help/C/tac_andelim.html @@ -0,0 +1,11 @@ + +we have
we have
Prev Chapter 8. Declarative Tactics Next

we have

justification we have A (H1) and B (H2) +

+

Synopsis:

justification we have term + ( id ) and term + ( id )

Pre-condition:

+ None. +

Action:

+ It applies the left multiplicative introduction rule for the conjunction on the formula A ∧ B (in Natural Deduction this corresponds to the elimination rule for the conjunction). +

New sequent to prove:

A new sequent with A ∧ B as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses H1 : A and H2 : B are added to the context.

+

Prev Up Next
let such that Home we proceed by induction on
\ No newline at end of file diff --git a/matita/matita/help/C/tac_apply.html b/matita/matita/help/C/tac_apply.html new file mode 100644 index 000000000..f03834bcd --- /dev/null +++ b/matita/matita/help/C/tac_apply.html @@ -0,0 +1,12 @@ + +apply
apply
Prev Chapter 7. Tactics Next

apply

@t

+

Synopsis:

@ sterm

Pre-conditions:

t must have type + T1 → … → + Tn → 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 + Ti that is not + instantiated by unification. Ti is + the conclusion of the i-th new sequent to + prove.

+

Prev Up Next
Chapter 7. Tactics Home auto
\ No newline at end of file diff --git a/matita/matita/help/C/tac_applyS.html b/matita/matita/help/C/tac_applyS.html new file mode 100644 index 000000000..c0cf500b2 --- /dev/null +++ b/matita/matita/help/C/tac_applyS.html @@ -0,0 +1,25 @@ + +applyS
applyS
Prev Chapter 7. Tactics Next

applyS

applyS t auto_params

+

Synopsis:

applyS sterm auto_params

Pre-conditions:

t must have type + T1 → ... → + Tn → 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 + Ti that is not + instantiated by unification. Ti is + the conclusion of the i-th new sequent to + prove.

+

Prev Up Next
rewrite Home assumption
\ No newline at end of file diff --git a/matita/matita/help/C/tac_assume.html b/matita/matita/help/C/tac_assume.html new file mode 100644 index 000000000..3c3979b6c --- /dev/null +++ b/matita/matita/help/C/tac_assume.html @@ -0,0 +1,11 @@ + +assume
assume
Prev Chapter 8. Declarative Tactics Next

assume

assume x : T

+

Synopsis:

assume id : + sterm

Pre-conditions:

+ The conclusion of the sequent to prove must be a universal quantification. +

Action:

+ It applies the right introduction rule for the universal quantifier, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the quantifier). +

New sequents to prove:

+ It opens a new sequent to prove the quantified subformula adding x : T to the hypotheses. +

+

Prev Up Next
Chapter 8. Declarative Tactics Home suppose
\ No newline at end of file diff --git a/matita/matita/help/C/tac_assumption.html b/matita/matita/help/C/tac_assumption.html new file mode 100644 index 000000000..d971f84d8 --- /dev/null +++ b/matita/matita/help/C/tac_assumption.html @@ -0,0 +1,5 @@ + +assumption
assumption
Prev Chapter 7. Tactics Next

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

+

Prev Up Next
applyS Home cases
\ No newline at end of file diff --git a/matita/matita/help/C/tac_auto.html b/matita/matita/help/C/tac_auto.html new file mode 100644 index 000000000..e85c7e96f --- /dev/null +++ b/matita/matita/help/C/tac_auto.html @@ -0,0 +1,12 @@ + +auto
auto
Prev Chapter 7. Tactics Next

auto

/params/

+

Synopsis:

/auto_params/.

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 the optional params. + Moreover, only lemmas whose type signature is a subset of the + signature of the current sequent are considered. The signature of + a sequent is essentially the set of constats appearing in it. +

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

+

Prev Up Next
apply Home intro
\ No newline at end of file diff --git a/matita/matita/help/C/tac_bydone.html b/matita/matita/help/C/tac_bydone.html new file mode 100644 index 000000000..f2e34e1d4 --- /dev/null +++ b/matita/matita/help/C/tac_bydone.html @@ -0,0 +1,4 @@ + +done
done
Prev Chapter 8. Declarative Tactics Next

done

justification done

+

Synopsis:

justification done

Pre-condition:

The user is proving a sequent which was opened with the tactic we need to prove, or the user is proving a sequent which was opened with the tactic we proceed by induction/cases on, or the user is proving a chain of equalities that was started with either the tactic conclude or obtain.

Action:

It closes the current sequent with the given justification.

New sequents to prove:

None.

+

Prev Up Next
= Home Chapter 9. Other commands
\ No newline at end of file diff --git a/matita/matita/help/C/tac_byinduction.html b/matita/matita/help/C/tac_byinduction.html new file mode 100644 index 000000000..a1f038e58 --- /dev/null +++ b/matita/matita/help/C/tac_byinduction.html @@ -0,0 +1,4 @@ + +by induction hypothesis we know
by induction hypothesis we know
Prev Chapter 8. Declarative Tactics Next

by induction hypothesis we know

by induction hypothesis we know P (id)

+

Synopsis:

by induction hypothesis we know term ( id )

Pre-condition:

The user must have started proving a case for a proof by induction/case-analysis.

Action:

It introduces the inductive hypothesis.

New sequents to prove:

None.

+

Prev Up Next
case Home conclude
\ No newline at end of file diff --git a/matita/matita/help/C/tac_bytermweproved.html b/matita/matita/help/C/tac_bytermweproved.html new file mode 100644 index 000000000..ab5f4b1d8 --- /dev/null +++ b/matita/matita/help/C/tac_bytermweproved.html @@ -0,0 +1,14 @@ + +we proved
we proved
Prev Chapter 8. Declarative Tactics Next

we proved

justification we proved T [(id)]

+

Synopsis:

justification we proved term + [( id + )] +

Pre-condition:

+ None. +

Action:

+ If id is supplied, a logical cut on T is made. Otherwise, if T is identical to the current conclusion, it allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to. +

New sequent to prove:

+ If id is supplied, a new sequent with T as the conclusion is opened and then immediately closed using the supplied justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and a new hypotesis T is added to the context, with name id. + If id is not supplied, no new sequents are opened. +

+

Prev Up Next
we need to prove Home let such that
\ No newline at end of file diff --git a/matita/matita/help/C/tac_case.html b/matita/matita/help/C/tac_case.html new file mode 100644 index 000000000..e0327b094 --- /dev/null +++ b/matita/matita/help/C/tac_case.html @@ -0,0 +1,4 @@ + +case
case
Prev Chapter 8. Declarative Tactics Next

case

case id (id1:T1) … (idn:Tn)

+

Synopsis:

case id [( id : term )] … [( id : term )]

Pre-condition:

The user must have started a proof by induction/cases that has not been concluded yet, id must be a constructor for the inductive type of the term under induction/case-analysis, and the case must not have already been proved.

Action:

It starts the proof for the case id, where id1:T1,…,idn:Tn are the arguments of the constructor, each declared with its type.

New sequents to prove:

The sequent for the case id.

+

Prev Up Next
we proceed by cases on Home by induction hypothesis we know
\ No newline at end of file diff --git a/matita/matita/help/C/tac_cases.html b/matita/matita/help/C/tac_cases.html new file mode 100644 index 000000000..646281d84 --- /dev/null +++ b/matita/matita/help/C/tac_cases.html @@ -0,0 +1,23 @@ + +cases
cases
Prev Chapter 7. Tactics Next

cases

+ cases t pattern +

+

Synopsis:

+ cases + term pattern +

Pre-conditions:

+ t must inhabit an inductive type +

Action:

+ It proceed by cases on t. The new generated + hypothesis in each branch are named according to + hyps. + The elimintation predicate is restricted by + pattern. In particular, if some hypothesis + is listed in pattern, the hypothesis is + generalized and cleared before proceeding by cases on + t. Currently, we only support patterns of the + form H1 … Hn ⊢ %. This limitation will be lifted in the future. +

New sequents to prove:

One new sequent for each constructor of the type of + t. Each sequent has a new hypothesis for + each argument of the constructor.

+

Prev Up Next
assumption Home change
\ No newline at end of file diff --git a/matita/matita/help/C/tac_change.html b/matita/matita/help/C/tac_change.html new file mode 100644 index 000000000..e4d2fa648 --- /dev/null +++ b/matita/matita/help/C/tac_change.html @@ -0,0 +1,9 @@ + +change
change
Prev Chapter 7. Tactics Next

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.

+

Prev Up Next
cases Home cut
\ No newline at end of file diff --git a/matita/matita/help/C/tac_clear.html b/matita/matita/help/C/tac_clear.html new file mode 100644 index 000000000..0f41adbee --- /dev/null +++ b/matita/matita/help/C/tac_clear.html @@ -0,0 +1,12 @@ + +clear
clear
Prev Chapter 7. Tactics Next

clear

-H

+

Synopsis:

+ -id +

Pre-conditions:

+ H must be an hypothesis of the + current sequent to prove. +

Action:

+ It hides the hypothesis H + from the current sequent. +

New sequents to prove:

None

+

Prev Up Next
macro_input Home constructor
\ No newline at end of file diff --git a/matita/matita/help/C/tac_conclude.html b/matita/matita/help/C/tac_conclude.html new file mode 100644 index 000000000..de312a7b8 --- /dev/null +++ b/matita/matita/help/C/tac_conclude.html @@ -0,0 +1,6 @@ + +conclude
conclude
Prev Chapter 8. Declarative Tactics Next

conclude

conclude t1

+

Synopsis:

conclude term

Pre-condition:

+ The current conclusion must be an equality t1 = tk +

Action:

It starts an equality chain on the conclusion. It allows the user to apply the tactic = to continue the chain.

New sequent to prove:

None.

+

Prev Up Next
by induction hypothesis we know Home obtain
\ No newline at end of file diff --git a/matita/matita/help/C/tac_constructor.html b/matita/matita/help/C/tac_constructor.html new file mode 100644 index 000000000..f0818bbbf --- /dev/null +++ b/matita/matita/help/C/tac_constructor.html @@ -0,0 +1,11 @@ + +constructor
constructor
Prev Chapter 7. Tactics Next

constructor

%n {args}

+

Synopsis:

% [nat] [{sterm…}]

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 to + the arguments args. + If n is omitted, it defaults to 1.

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.

+

Prev Up Next
clear Home decompose
\ No newline at end of file diff --git a/matita/matita/help/C/tac_cut.html b/matita/matita/help/C/tac_cut.html new file mode 100644 index 000000000..7484b50ae --- /dev/null +++ b/matita/matita/help/C/tac_cut.html @@ -0,0 +1,8 @@ + +cut
cut
Prev Chapter 7. Tactics Next

cut

cut P

+

Synopsis:

cut sterm

Pre-conditions:

P must be a type.

Action:

It closes the current sequent.

New sequents to prove:

It opens two new sequents. The first one has conclusion + P → G where G is the + old conclusion. + The second sequent has conclusion P and + hypotheses the hypotheses of the current sequent to prove.

+

Prev Up Next
change Home destruct
\ No newline at end of file diff --git a/matita/matita/help/C/tac_decompose.html b/matita/matita/help/C/tac_decompose.html new file mode 100644 index 000000000..69618097b --- /dev/null +++ b/matita/matita/help/C/tac_decompose.html @@ -0,0 +1,18 @@ + +decompose
decompose
Prev Chapter 7. Tactics Next

decompose

+ * as H +

+

Synopsis:

+ * + [as id] +

Pre-conditions:

The current conclusion must be of the form + T → G where I is + an inductive type applied to its arguments, if any.

Action:

+ It introduces a new hypothesis H of type + T. Then it proceeds by cases over + H. Finally, if the name H + is not specified, it clears the new hypothesis from all contexts. +

New sequents to prove:

+ The ones generated by case analysis. +

+

Prev Up Next
constructor Home rewrite
\ No newline at end of file diff --git a/matita/matita/help/C/tac_destruct.html b/matita/matita/help/C/tac_destruct.html new file mode 100644 index 000000000..223234a83 --- /dev/null +++ b/matita/matita/help/C/tac_destruct.html @@ -0,0 +1,15 @@ + +destruct
destruct
Prev Chapter 7. Tactics Next

destruct

destruct (H0 ... Hn) skip (K0 ... Km)

+

Synopsis:

destruct + [(id…)] [skip (id…)]

Pre-conditions:

Each hypothesis Hi must be either a Leibniz or a John Major equality where the two sides of the equality are possibly applied constructors of an inductive type.

Action:

The tactic recursively compare the two sides of each 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. If the newly + added hypothesis is an equality between a variable and a term, + the variable is substituted for the term everywhere in the + sequent, except for the hypotheses Kj, and it is then cleared from the list of hypotheses. +

New sequents to prove:

None.

+

Prev Up Next
cut Home elim
\ No newline at end of file diff --git a/matita/matita/help/C/tac_elim.html b/matita/matita/help/C/tac_elim.html new file mode 100644 index 000000000..b2e7089d4 --- /dev/null +++ b/matita/matita/help/C/tac_elim.html @@ -0,0 +1,12 @@ + +elim
elim
Prev Chapter 7. Tactics Next

elim

elim t pattern

+

Synopsis:

elim sterm pattern

Pre-conditions:

t must inhabit an inductive type. +

Action:

It proceeds by cases on the values of t, + according to the most appropriate elimination principle for + the current goal. + The induction predicate is restricted by + pattern. In particular, if some hypothesis + is listed in pattern, the hypothesis is + generalized and cleared before eliminating t +

New sequents to prove:

It opens one new sequent for each case.

+

Prev Up Next
destruct Home generalize
\ No newline at end of file diff --git a/matita/matita/help/C/tac_existselim.html b/matita/matita/help/C/tac_existselim.html new file mode 100644 index 000000000..939f714fe --- /dev/null +++ b/matita/matita/help/C/tac_existselim.html @@ -0,0 +1,11 @@ + +let such that
let such that
Prev Chapter 8. Declarative Tactics Next

let such that

justification let x:T such that P (H) +

+

Synopsis:

justification let id + : term such that term + ( id )

Pre-condition:

+ None. +

Action:

+ It applies the left introduction rule of the existential quantifier on the formula ∃ x. P(x) (in Natural Deduction this corresponds to the elimination rule for the quantifier). +

New sequent to prove:

A new sequent with ∃ x. P(x) as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses x : T and H : P are added to the context.

+

Prev Up Next
we proved Home we have
\ No newline at end of file diff --git a/matita/matita/help/C/tac_generalize.html b/matita/matita/help/C/tac_generalize.html new file mode 100644 index 000000000..bfe134dcb --- /dev/null +++ b/matita/matita/help/C/tac_generalize.html @@ -0,0 +1,13 @@ + +generalize
generalize
Prev Chapter 7. Tactics Next

generalize

generalize patt

+

Synopsis:

generalize pattern

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.

+

Prev Up Next
elim Home inversion
\ No newline at end of file diff --git a/matita/matita/help/C/tac_intro.html b/matita/matita/help/C/tac_intro.html new file mode 100644 index 000000000..6c09618e2 --- /dev/null +++ b/matita/matita/help/C/tac_intro.html @@ -0,0 +1,9 @@ + +intro
intro
Prev Chapter 7. Tactics Next

intro

#H

+

Synopsis:

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

+

Prev Up Next
auto Home intro_clear
\ No newline at end of file diff --git a/matita/matita/help/C/tac_intro_clear.html b/matita/matita/help/C/tac_intro_clear.html new file mode 100644 index 000000000..21ce7a54a --- /dev/null +++ b/matita/matita/help/C/tac_intro_clear.html @@ -0,0 +1,7 @@ + +intro_clear
intro_clear
Prev Chapter 7. Tactics Next

intro_clear

#_

+

Synopsis:

#_

Pre-conditions:

The conclusion of the sequent to prove must be an implication. +

Action:

It applies the ``a fortiori'' rule for implication, + closing the current sequent.

New sequents to prove:

It opens a new sequent whose conclusion is the conclusion + of the implication of the original sequent.

+

Prev Up Next
intro Home macro_input
\ No newline at end of file diff --git a/matita/matita/help/C/tac_inversion.html b/matita/matita/help/C/tac_inversion.html new file mode 100644 index 000000000..8e4d54ffa --- /dev/null +++ b/matita/matita/help/C/tac_inversion.html @@ -0,0 +1,13 @@ + +inversion
inversion
Prev Chapter 7. Tactics Next

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. It uses either Leibniz or John Major equality + for the new hypotheses, according to the included files.

+

Prev Up Next
generalize Home lapply
\ No newline at end of file diff --git a/matita/matita/help/C/tac_lapply.html b/matita/matita/help/C/tac_lapply.html new file mode 100644 index 000000000..90cf83c61 --- /dev/null +++ b/matita/matita/help/C/tac_lapply.html @@ -0,0 +1,17 @@ + +lapply
lapply
Prev Chapter 7. Tactics Next

lapply

+ lapply t +

+

Synopsis:

+ lapply + sterm +

Pre-conditions:

None.

Action:

+ It generalizes the conclusion of the current goal + adding as a premise the type of t, + closing the current goal. +

New sequents to prove:

+ The new sequent has conclusion T → G where + T is the type of t + and G the old conclusion. +

+

Prev Up Next
inversion Home letin
\ No newline at end of file diff --git a/matita/matita/help/C/tac_let.html b/matita/matita/help/C/tac_let.html new file mode 100644 index 000000000..57fb71050 --- /dev/null +++ b/matita/matita/help/C/tac_let.html @@ -0,0 +1,4 @@ + +letin
letin
Prev Chapter 8. Declarative Tactics Next

letin

let x := T

+

Synopsis:

let id = term

Pre-condition:

None

Action:

It adds a new local definition x := T to the context of the sequent to prove.

New sequents to prove:

None.

+

Prev Up Next
suppose Home that is equivalent to
\ No newline at end of file diff --git a/matita/matita/help/C/tac_letin.html b/matita/matita/help/C/tac_letin.html new file mode 100644 index 000000000..278542ffa --- /dev/null +++ b/matita/matita/help/C/tac_letin.html @@ -0,0 +1,5 @@ + +letin
letin
Prev Chapter 7. Tactics Next

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.

+

Prev Up Next
lapply Home normalize
\ No newline at end of file diff --git a/matita/matita/help/C/tac_normalize.html b/matita/matita/help/C/tac_normalize.html new file mode 100644 index 000000000..60cf39ffd --- /dev/null +++ b/matita/matita/help/C/tac_normalize.html @@ -0,0 +1,7 @@ + +normalize
normalize
Prev Chapter 7. Tactics Next

normalize

normalize patt nodelta

+

Synopsis:

normalize pattern + [nodelta]

Pre-conditions:

None.

Action:

It replaces all the terms matched by patt + with their βδιζ-normal form. If nodelta is + specified, δ-expansions are not performed.

New sequents to prove:

None.

+

Prev Up Next
letin Home whd
\ No newline at end of file diff --git a/matita/matita/help/C/tac_obtain.html b/matita/matita/help/C/tac_obtain.html new file mode 100644 index 000000000..c26c009ae --- /dev/null +++ b/matita/matita/help/C/tac_obtain.html @@ -0,0 +1,6 @@ + +obtain
obtain
Prev Chapter 8. Declarative Tactics Next

obtain

obtain H t1

+

Synopsis:

obtain id term

Pre-condition:

+ None. +

Action:

It starts an equality chain t1 = ?, which, when concluded, will be added to hypoteses of the current sequent. It allows the user to apply the tactic = to continue the chain.

New sequent to prove:

A new sequent for t1 = ? is opened, a new sequent for ? is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H: t1 = ? added to its hypotheses. This hypotesis will be changed when the equality chain is concluded with H: t1 = tk, where tk is the last term of the equality chain. The goal for ? can be safely ignored, as it will be automatically closed when the equality chain is concluded.

+

Prev Up Next
conclude Home =
\ No newline at end of file diff --git a/matita/matita/help/C/tac_rewrite.html b/matita/matita/help/C/tac_rewrite.html new file mode 100644 index 000000000..dc43ad673 --- /dev/null +++ b/matita/matita/help/C/tac_rewrite.html @@ -0,0 +1,12 @@ + +rewrite
rewrite
Prev Chapter 7. Tactics Next

rewrite

> p patt

+

Synopsis:

[<|>] 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 < is used). + 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.

+

Prev Up Next
decompose Home applyS
\ No newline at end of file diff --git a/matita/matita/help/C/tac_rewrite_step.html b/matita/matita/help/C/tac_rewrite_step.html new file mode 100644 index 000000000..3875796c8 --- /dev/null +++ b/matita/matita/help/C/tac_rewrite_step.html @@ -0,0 +1,12 @@ + +=
=
Prev Chapter 8. Declarative Tactics Next

=

= t2 justification

+

Synopsis:

+ = term [auto_params | using term | using once term | proof] [done] +

Pre-condition:

+ The user must have started an equality chain with conclude or obtain that has not been concluded yet. +

Action:

+ It applies the transitivity of = on the left-hand-side of the current conclusion, t2, and the right-hand-side of the current conclusion, using the given justification. If done is supplied, this represents the last step in the equality chain. +

New sequent to prove:

+ A new sequent for lhs = t2 is opened and then immediately closed using the given justification. A new sequent with the conclusion t2 = rhs is opened. +

+

Prev Up Next
obtain Home done
\ No newline at end of file diff --git a/matita/matita/help/C/tac_suppose.html b/matita/matita/help/C/tac_suppose.html new file mode 100644 index 000000000..7307692da --- /dev/null +++ b/matita/matita/help/C/tac_suppose.html @@ -0,0 +1,11 @@ + +suppose
suppose
Prev Chapter 8. Declarative Tactics Next

suppose

suppose A (H)

+

Synopsis:

suppose term ( id + )

Pre-condition:

+ The conclusion of the sequent to prove must be an implication. +

Action:

+ It applies the right introduction rule for the implication, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the implication). +

New sequents to prove:

+ It opens a new sequent to prove the consequent of the implication adding the antecedent A to the hypotheses. The name of the new hypothesis is H. +

+

Prev Up Next
assume Home letin
\ No newline at end of file diff --git a/matita/matita/help/C/tac_thatisequivalentto.html b/matita/matita/help/C/tac_thatisequivalentto.html new file mode 100644 index 000000000..4ef638aa6 --- /dev/null +++ b/matita/matita/help/C/tac_thatisequivalentto.html @@ -0,0 +1,14 @@ + +that is equivalent to
that is equivalent to
Prev Chapter 8. Declarative Tactics Next

that is equivalent to

that is equivalent to t

+

Synopsis:

+ that is equivalent to term +

Pre-condition:

+ The user must have applied one of the following tactics immediately before applying this tactic: assume, suppose, we need to prove, by just we proved,the thesis becomes, that is equivalent to. +

Action:

+ If the tactic that was applied before this introduced a new hypothesis in the context, this tactic works on this hypothesis; otherwise, it works on the conclusion. Either way, if the term t is beta-equivalent to the term t1 on which this tactic is working (i.e. they can be reduced to a common term), t1 is changed with t. + + If the tactic that was applied before this tactic was that is equivalent to, and that tactic was working on a term t1, this tactic keeps working on t1. +

New sequent to prove:

+ If this tactic is working on the conclusion, a new sequent with the same hypotheses and the conclusion changed to t is opened. If this tactic is working on the last introduced hypotesis, a new sequent with the same conclusion is opened. The hypotheses of this sequent are the same, except for the one on which the tactic is working on, which is changed with t. +

+

Prev Up Next
letin Home the thesis becomes
\ No newline at end of file diff --git a/matita/matita/help/C/tac_thesisbecomes.html b/matita/matita/help/C/tac_thesisbecomes.html new file mode 100644 index 000000000..7529ed0a7 --- /dev/null +++ b/matita/matita/help/C/tac_thesisbecomes.html @@ -0,0 +1,4 @@ + +the thesis becomes
the thesis becomes
Prev Chapter 8. Declarative Tactics Next

the thesis becomes

the thesis becomes P

+

Synopsis:

the thesis becomes term

Pre-condition:

The provided term P must be identical to the current conclusion.

Action:

It allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to, after stating the current conclusion.

New sequent to prove:

None.

+

Prev Up Next
that is equivalent to Home we need to prove
\ No newline at end of file diff --git a/matita/matita/help/C/tac_weneedtoprove.html b/matita/matita/help/C/tac_weneedtoprove.html new file mode 100644 index 000000000..d77643518 --- /dev/null +++ b/matita/matita/help/C/tac_weneedtoprove.html @@ -0,0 +1,8 @@ + +we need to prove
we need to prove
Prev Chapter 8. Declarative Tactics Next

we need to prove

we need to prove T [(H)]

+

Synopsis:

we need to prove term + [(id + )] +

Pre-condition:

None.

Action:

If id is provided, it applies a logical cut on T. Otherwise, it allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to. +

New sequents to prove:

If id is supplied, a new sequent with T as the conclusion is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H:T added to the hypotheses.

+

Prev Up Next
the thesis becomes Home we proved
\ No newline at end of file diff --git a/matita/matita/help/C/tac_weproceedbycases.html b/matita/matita/help/C/tac_weproceedbycases.html new file mode 100644 index 000000000..7b364b17c --- /dev/null +++ b/matita/matita/help/C/tac_weproceedbycases.html @@ -0,0 +1,6 @@ + +we proceed by cases on
we proceed by cases on
Prev Chapter 8. Declarative Tactics Next

we proceed by cases on

we proceed by cases on t to prove P

+

Synopsis:

we proceed by cases on term to prove term

Pre-condition:

The type of t must be an inductive type and P must be identical to the current conclusion. +

Action:

It proceeds by case-analysis on t

New sequents to prove:

It opens one new sequent for each constructor of the + type of t, each with the conclusion P instantiated for the constructor.

+

Prev Up Next
we proceed by induction on Home case
\ No newline at end of file diff --git a/matita/matita/help/C/tac_weproceedbyinduction.html b/matita/matita/help/C/tac_weproceedbyinduction.html new file mode 100644 index 000000000..d10d151a2 --- /dev/null +++ b/matita/matita/help/C/tac_weproceedbyinduction.html @@ -0,0 +1,5 @@ + +we proceed by induction on
we proceed by induction on
Prev Chapter 8. Declarative Tactics Next

we proceed by induction on

we proceed by induction on t to prove P

+

Synopsis:

we proceed by induction on term to prove term

Pre-condition:

The type of t must be an inductive type and P must be identical to the current conclusion. +

Action:

It applies the induction principle on t to prove P.

New sequents to prove:

It opens a new sequent for each constructor of the type of t, each with the conclusion P instantiated for the constructor. For the inductive constructors (i.e. if the inductive type is T, constructors with an argument of type T), the conclusion is a logical implication, where the antecedent is the inductive hypothesis for the constructor, and the consequent is P.

+

Prev Up Next
we have Home we proceed by cases on
\ No newline at end of file diff --git a/matita/matita/help/C/tac_whd.html b/matita/matita/help/C/tac_whd.html new file mode 100644 index 000000000..0e0b14a97 --- /dev/null +++ b/matita/matita/help/C/tac_whd.html @@ -0,0 +1,5 @@ + +whd
whd
Prev Chapter 7. Tactics Next

whd

whd patt nodelta

+

Synopsis:

whd pattern [nodelta]

Pre-conditions:

None.

Action:

It replaces all the terms matched by patt + with their βδιζ-weak-head normal form. If nodelta is specified, δ-expansions are not performed.

New sequents to prove:

None.

+

Prev Up Next
normalize Home Chapter 8. Declarative Tactics
\ No newline at end of file diff --git a/matita/matita/help/C/tacticals.html b/matita/matita/help/C/tacticals.html new file mode 100644 index 000000000..afff712b7 --- /dev/null +++ b/matita/matita/help/C/tacticals.html @@ -0,0 +1,65 @@ + +Tacticals
Tacticals
Prev Chapter 6. Tacticals Next

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-tacticalThe 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. +
 |skipAccept 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::=tacticApplies the specified tactic.
 |LCF-tactical ; LCF-tacticalApplies 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 + TODO
 |repeat + LCF-tactical + TODO
 | + first [ + [LCF-tactical] + [| LCF-tactical]… + ] + TODO
 |try LCF-tacticalTODO
 | + solve [ + [LCF-tactical] + [| LCF-tactical]… + ] + TODO
 |(LCF-tactical)Used for grouping during parsing.

Prev Up Next
The proof status Home Chapter 7. Tactics
\ No newline at end of file diff --git a/matita/matita/help/C/tacticargs.html b/matita/matita/help/C/tacticargs.html new file mode 100644 index 000000000..4896638be --- /dev/null +++ b/matita/matita/help/C/tacticargs.html @@ -0,0 +1,94 @@ + +Tactic arguments
Tactic arguments
Prev Chapter 4. Syntax Next

Tactic arguments

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

pattern

Table 4.13. pattern

pattern::=in + [id[: path]]… + [⊢ path]];simple pattern
 |in match path + [in + [id[: path]]… + [⊢ path]];full pattern

Table 4.14. path

path::=〈〈any sterm without 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 ?. +

Warning: the format for a path for a match … with + expression is restricted to: match path + with + [ + _ + ⇒ + path + | … + | + _ + ⇒ + path + ] + Its semantics is the following: the n-th + "_ + ⇒ + path" branch is matched against the n-th constructor of the + inductive data type. The head λ-abstractions of path are matched + against the corresponding constructor arguments. +

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 + { 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 + { 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"

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.15. reduction-kind

reduction-kind::=normalize [nodelta]Computes the βδιζ-normal form. If nodelta + is specified, δ-expansions are not performed.
 |whd [nodelta]Computes the βδιζ-weak-head normal form. If nodelta + is specified, δ-expansions are not performed.

auto-params

Table 4.16. auto-params

auto_params::=[nat] [simple_auto_param]… + [by + [sterm… | _]] + The natural number, which defaults to 1, gives a bound to + the depth of the search tree. The terms listed is the only + knowledge base used by automation together with all indexed factual + and equational theorems in the included library. If the list of terms + is empty, only equational theorems and facts in the library are + used. If the list is omitted, it defaults to all indexed theorems + in the library. Finally, if the list is _, + the automation command becomes a macro that is expanded in a new + automation command where _ is replaced with the + list of theorems required to prove the sequent. +

Table 4.17. simple-auto-param

simple_auto_param::=width=natThe maximal width of the search tree
 |size=natThe maximal number of nodes in the proof
 |demodSimplifies the current sequent using the current set of + equations known to automation +
 |paramodTry to close the goal performing unit-equality paramodulation +
 |fast_paramodA bounded version of paramod that is granted to terminate quickly +

justification

Table 4.18. justification

justification::=using termProof term manually provided
 |auto_paramsCall automation

Prev Up Next
Proofs Home Chapter 5. Extending the syntax
\ No newline at end of file diff --git a/matita/matita/help/C/xsl/tactic_quickref.xsl b/matita/matita/help/C/xsl/tactic_quickref.xsl index 3a46261e0..b324bc40f 100644 --- a/matita/matita/help/C/xsl/tactic_quickref.xsl +++ b/matita/matita/help/C/xsl/tactic_quickref.xsl @@ -27,6 +27,9 @@ + + + @@ -54,8 +57,7 @@ - tac_ - +