Matita V0.5.9 User Manual (rev. 0.5.9 )
   Next

Matita V0.5.9 User Manual (rev. 0.5.9 )

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.5.9 , 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
(optional) MySQL setup
Compiling and installing
Configuring Matita
3. Getting started
How to type Unicode symbols
Browsing and searching
Browsing the library
Looking at a proof under development
Searching the library
Authoring
How to compile a script
The authoring interface
4. Syntax
Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
TODO
(co)inductive types declaration
record
Proofs
theorem
variant
lemma
fact
remark
Tactic arguments
intros-spec
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
absurd
apply
applyS
assumption
auto
cases
clear
clearbody
compose
change
constructor
contradiction
cut
decompose
demodulate
destruct
elim
elimType
exact
exists
fail
fold
fourier
fwd
generalize
id
intro
intros
inversion
lapply
left
letin
normalize
reflexivity
change
rewrite
right
ring
simplify
split
subst
symmetry
transitivity
unfold
whd
8. Declarative Tactics
Quick reference card
assume
by induction hypothesis we know
case
done
let such that
obtain
suppose
the thesis becomes
we need to prove
we have
we proceed by cases on
we proceed by induction on
we proved
9. Other commands
alias
check
eval
prefer coercion
coercion
default
hint
include
include' "s"
whelp
qed
inline
inline-params
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
2.9. Configuring the Databases

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. intros-spec
4.14. pattern
4.15. path
4.16. reduction-kind
4.17. auto-params
4.18. simple-auto-param
4.19. 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
9.1. clusters
9.2. inline-params
9.3. inline-param
   Next
   Chapter 1. Introduction