+(*D
+
+Inductively generated formal topologies in Matita
+=================================================
+
+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 Stefano Berardi and Silvio Valentini.
+
+The tutorial and the formalization are by Enrico Tassi.
+
+The reader should be familiar with inductively generated
+formal topologies and have some basic knowledge of type theory and λ-calculus.
+
+A considerable part of this tutorial is devoted to explain how to define
+notations that resemble the ones used in the original paper. We believe
+this is an important part of every formalization, not only from the aesthetic
+point of view, but also from the practical point of view. Being
+consistent allows to follow the paper in a pedantic way, and hopefully
+to make the formalization (at least the definitions and proved
+statements) readable to the author of the paper.
+
+The formalization uses the "new generation" version of Matita
+(that will be named 1.x when finally released).
+Last stable release of the "old" system is named 0.5.7; the ng system
+is coexisting with the old one in all development release
+(named "nightly builds" in the download page of Matita)
+with a version strictly greater than 0.5.7.
+
+To read this tutorial in HTML format, you need a decent browser
+equipped with a unicode capable font. Use the PDF format if some
+symbols are not displayed correctly.
+
+Orienteering
+------------
+
+The graphical interface of Matita is composed of three windows:
+the script window, on the left, is where you type; the sequent
+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 they request the system to:
+
+- go back to the beginning of the script
+- go back one step
+- go to the current cursor position
+- advance one step
+- advance to the end of the script
+
+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 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 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 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 ease the typing of mathematical symbols, the script window
+implements two unusual input facilities:
+
+- some TeX symbols can be typed using their TeX names, and are
+ automatically converted to UTF-8 characters. For a list of
+ the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
+ Moreover some ASCII-art is understood as well, like `=>` and `->`
+ to mean double or single arrows.
+ Here we recall some of these "shortcuts":
+
+ - ∀ can be typed with `\forall`
+ - λ can be typed with `\lambda`
+ - ≝ can be typed with `\def` or `:=`
+ - → can be typed with `\to` or `->`
+
+- some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
+ The user can cycle between variants typing one of them and then
+ pressing ALT-L. Note that also letters do have variants, for
+ example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
+ Variants are listed in the aforementioned TeX/UTF-8 table.
+
+The syntax of terms (and types) is the one of the λ-calculus CIC
+on which Matita is based. The main syntactical difference w.r.t.
+the usual mathematical notation is the function application, written
+`(f x y)` in place of `f(x,y)`.
+
+Pressing `F1` opens the Matita manual.
+
+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 impredicative sort
+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 occur 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 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 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.
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).
+
+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 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 label: constraints among
+universes are declared by the user. The standard library defines
+
+> Type[0] < Type[1] < Type[2]
+
+Matita implements a variant of CIC in which constructive and predicative proposition
+are distinguished from predicative data types.
+
+<object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
+
+For every `Type[i]` there is a corresponding level of predicative
+propositions `CProp[i]` (the C initial is due to historical reasons, and
+stands for constructive).
+A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
+with 0 or 1 constructors with propositional arguments, like `Id` and `And`
+but not like `Or`).
+
+The distinction between predicative propositions and predicative data types
+is a peculiarity of Matita (for example in CIC as implemented by Coq they are the
+same). The additional restriction of not allowing the elimination of a CProp
+toward a Type makes the theory of Matita minimal in the following sense:
+
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="600px"/>
+
+Theorems proved in CIC as implemented in Matita can be reused in a classical
+and impredicative framework (i.e. forcing Matita to collapse the hierarchy of
+constructive propositions and assuming the excluded middle on them).
+Alternatively, one can decide to collapse predicative propositions and
+predicative data types recovering the Axiom of Choice in the sense of Martin Löf
+(i.e. ∃ really holds a witness and can be eliminated to inhabit a type).
+
+This implementation of CIC is the result of the collaboration with Maietti M.,
+Sambin G. and Valentini S. of the University of Padua.
+
+Formalization choices
+---------------------
+
+There are many different ways of formalizing the same piece of mathematics
+in CIC, depending on what our interests are. There is usually a trade-off
+between the possibility of reuse the formalization we did and its complexity.
+
+In this work, our decisions mainly regarded the following two areas
+
+- Axiom of Choice: controlled use or not
+- Equality: Id or not
+
+### Axiom of Choice
+
+In this paper it is clear that the author is interested in using the Axiom
+of Choice, thus choosing to identify ∃ and Σ (i.e. working in the
+leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision
+(that is, the author of the paper would not complain we formalized something
+different from what he had in mind).
+
+Anyway, we may benefit from the minimality of CIC as implemented in Matita,
+"asking" the type system to ensure we do no use the Axiom of Choice elsewhere
+in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
+very beginning, the system will not complain if we use the Axiom of Choice at all.
+Moreover, the elimination of an inductive type (like ∃) is a so common operation
+that the syntax chosen for the elimination command is very compact and non
+informative, hard to spot for a human being
+(in fact it is just two characters long!).
+
+We decided to formalize the whole paper without identifying
+CProp and Type and assuming the Axiom of Choice as a real axiom
+(i.e. a black hole with no computational content, a function with no body).
+
+It is clear that this approach give us full control on when/where we really use
+the Axiom of Choice. But, what are we loosing? What happens to the computational
+content of the proofs if the Axiom of Choice gives no content back?
+
+It really
+depends on when we actually look at the computational content of the proof and
+we "run" that program. We can extract the content and run it before or after
+informing the system that our propositions are actually code (i.e. identifying
+∃ and Σ). If we run the program before, as soon as the computation reaches the
+Axiom of Choice it stops, giving no output. If we tell the system that CProp and
+Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection)
+and the extracted code would compute an output.
+
+Note that the computational
+content is there even if the Axiom of Choice is an axiom, the difference is
+just that we cannot use it (the typing rules inhibit the elimination of the
+existential). This is possible only thanks to the minimality of CIC as implemented
+in Matita.
+
+### Equality
+
+What we have to decide here is which models we admit. The paper does not
+mention quotiented sets, thus using an intensional equality is enough
+to capture the intended content of the paper. Nevertheless, the formalization
+cannot be reused in a concrete example where the (families of) sets
+that will build the axiom set are quotiented.
+
+Matita gives support for setoid rewriting under a context built with
+non dependent morphisms. As we will detail later, if we assume a generic
+equality over the carrier of our axiom set, a non trivial inductive
+construction over the ordinals has to be proved to respect extensionality
+(i.e. if the input is an extensional set, also the output is).
+The proof requires to rewrite under the context formed by the family of sets
+`I` and `D`, that have a dependent type. Declaring them as dependently typed
+morphisms is possible, but Matita does not provide an adequate support for them,
+and would thus need more effort than formalizing the whole paper.
+
+Anyway, in a preliminary attempt of formalization, we tried the setoid approach,
+reaching the end of the formalization, but we had to assume the proof
+of the extensionality of the `U_x` construction (while there is no
+need to assume the same property for `F_x`!).
+
+The current version of the formalization uses `Id`.
+
+The standard library and the `include` command
+----------------------------------------------
+
+Some basic notions, like subset, membership, intersection and union
+are part of the standard library of Matita.
+
+These notions come with some standard notation attached to them:
+
+- A ∪ B can be typed with `A \cup B`
+- A ∩ B can be typed with `A \cap B`
+- A ≬ B can be typed with `A \between B`
+- x ∈ A can be typed with `x \in A`
+- Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A`
+
+The `include` command tells Matita to load a part of the library,
+in particular the part that we will use can be loaded as follows:
+
+D*)
+
+include "sets/sets.ma".