Matita Tutorial: inductively generated formal topologies
========================================================
-This is a not so short introduction to Matita, based on
+This is a not so short introduction to [Matita][2], based on
the formalization of the paper
> Between formal topology and game theory: an
> explicit solution for the conditions for an
> inductive generation of formal topologies
-by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
+by Stefano Berardi and Silvio Valentini.
+The tutorial is by Enrico Tassi.
The tutorial spends a considerable amount of effort in defining
notations that resemble the ones used in the original paper. We believe
window on the top right is where the system shows you the ongoing proof;
the error window, on the bottom right, is where the system complains.
On the top of the script window five buttons drive the processing of
-the proof script. From left to right the requesting the system to:
+the proof script. From left to right they request the system to:
- go back to the beginning of the script
- go back one step
When the system processes a command, it locks the part of the script
corresponding to the command, such that you cannot edit it anymore
-(without to go back). Locked parts are coloured in blue.
+(without going back). Locked parts are coloured in blue.
The sequent window is hyper textual, i.e. you can click on symbols
-to jump to their definition, or switch between different notation
+to jump to their definition, or switch between different notations
for the same expression (for example, equality has two notations,
one of them makes the type of the arguments explicit).
Everywhere in the script you can use the `ncheck (term).` command to
-ask for the type a given term. If you that in the middle of a proof,
+ask for the type a given term. If you do that in the middle of a proof,
the term is assumed to live in the current proof context (i.e. can use
variables introduced so far).
to mean double or single arrows.
Here we recall some of these "shortcuts":
- - ∀ can be typed with `\Forall`
+ - ∀ can be typed with `\forall`
- λ can be typed with `\lambda`
- ≝ can be typed with `\def` or `:=`
- → can be typed with `\to` or `->`
Pressing `F1` opens the Matita manual.
-CIC (as implemented in Matita) in a nutshell
---------------------------------------------
+CIC (as [implemented in Matita][3]) in a nutshell
+-------------------------------------------------
CIC is a full and functional Pure Type System (all products do exist,
and their sort is is determined by the target) with an impedicative sort
-Prop and a predicative sort Type. The environment can be populated with
+Prop and a predicative sort Type. It features both dependent types and
+polymorphism like the [Calculus of Constructions][4]. Proofs and terms share
+the same syntax, and they can occurr in types.
+
+The environment used for in the typing judgement can be populated with
well typed definitions or theorems, (co)inductive types validating positivity
conditions and recursive functions provably total by simple syntactical
-analysis (recursive call on structurally smaller subterms). Co-recursive
-functions can be defined as well, and must satisfy a dual condition, that is
+analysis (recursive calls are allowed only on structurally smaller subterms).
+Co-recursive
+functions can be defined as well, and must satisfy the dual condition, i.e.
performing the recursive call only after having generated a constructor (a piece
of output).
-The λ-calculus is equipped with a pattern matching construct (match) on inductive
-types defined in the environment that combined with the definable total
-structural recursive functions allows to define eliminators (or constructors)
-for (co)inductive types. The λ-calculus is also equipped with explicitly types
+The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment. This construct, together with the possibility to
+definable total recursive functions, allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly typed
local definitions (let in) that in the degenerate case work as casts (i.e.
the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
Since we are going to formalize constructive and predicative mathematics
in an intensional type theory like CIC, we try to establish some terminology.
-Type is the sort of sets equipped with the Id equality (i.e. an intensional,
-not quotiented set). We will avoid using Leibnitz equality Id,
-thus we will explicitly equip a set with an equality when needed.
-We will call this structure `setoid`. Note that we will
-attach the infix = symbol only to the equality of a setoid,
+Type is the sort of sets equipped with the `Id `equality (i.e. an intensional,
+not quotiented set). We will avoid using `Id` (Leibnitz equality),
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,
not to Id.
-We write Type[i] to mention a Type in the predicative hierarchy
-of types. To ease the comprehension we will use Type[0] for sets,
-and Type[1] for classes.
+We write `Type[i]` to mention a Type in the predicative hierarchy
+of types. To ease the comprehension we will use `Type[0]` for sets,
+and `Type[1]` for classes. The index `i` is just a lable: constraints among
+universes are declared by the user. The standard library defines
+
+> Type[0] < Type[1] < Type[2]
-For every Type[i] there is a corresponding level of predicative
-propositions CProp[i].
+For every `Type[i]` there is a corresponding level of predicative
+propositions `CProp[i]`. A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive type
+with 0 or 1 constructors with propositional arguments, like `Id` and `And`
+but not like `Or`).
The standard library and the `include` command
Defining Axiom set
------------------
-A set of axioms is made of a set S, a family of sets I and a
-family C of subsets of S indexed by elements a of S and I(a).
+A set of axioms is made of a set(oid) `S`, a family of sets `I` and a
+family `C` of subsets of `S` indexed by elements `a` of `S`
+and elements of `I(a)`.
It is desirable to state theorems like "for every set of axioms, …"
without explicitly mentioning S, I and C. To do that, the three
components have to be grouped into a record (essentially a dependently
typed tuple). The system is able to generate the projections
-of the record for free, and they are named as the fields of
-the record. So, given a axiom set `A` we can obtain the set
+of the record automatically, and they are named as the fields of
+the record. So, given an axiom set `A` we can obtain the set
with `S A`, the family of sets with `I A` and the family of subsets
with `C A`.
Note that `S` is declared to be a `setoid` and not a Type. The original
paper probably also considers I to generate setoids, and both I and C
-to be morphisms. For the sake of simplicity, we will "cheat" and use
+to be (dependent) morphisms. For the sake of simplicity, we will "cheat" and use
setoids only when strictly needed (i.e. where we want to talk about
equality). Setoids will play a role only when we will define
the alternative version of the axiom set.
</date>
[1]: http://upsilon.cc/~zack/research/publications/notation.pdf
+[2]: http://matita.cs.unibo.it
+[3]: http://www.cs.unibo.it/~tassi/smallcc.pdf
+[4]: http://www.inria.fr/rrrt/rr-0530.html
D*)
projects / helm.git / commitdiff