(*D
-Matita Tutorial: inductively generated formal topologies
-========================================================
+Inductively generated formal topologies in Matita
+=================================================
This is a not so short introduction to [Matita][2], based on
the formalization of the paper
The tutorial is by Enrico Tassi.
-The tutorial spends a considerable amount of effort in defining
+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 a important part of every formalization, not only from the aesthetic
+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 ng (new generation) version of Matita
+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 every development release
+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.
with 0 or 1 constructors with propositional arguments, like `Id` and `And`
but not like `Or`).
-The distintion between predicative propositions and predicative data types
+The distinction between predicative propositions and predicative data types
is a peculirity 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="500px"/>
-Theorems proved in this setting can be reused in a classical framwork (forcing
-Matita to collapse the hierarchy of constructive propositions). Alternatively,
-one can decide to collapse predicative propositions and datatypes recovering the
-Axiom of Choice (i.e. ∃ really holds a content and can thus be eliminated to
-provide a witness for a Σ).
+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
+datatypes 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 tradeoff
+between the possibility of reuse the formalization we did and its complexity.
+
+In this work, our decisions mainly regarded the following two areas
+
+- Equality: Id or not
+- Axiom of Choice: controlled use or not
+
+### Equality
+
+TODO
We will avoid using `Id` (Leibniz 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.
-
+### 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
+diffrent 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 elswhere
+in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
+very beginnig, 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.
The standard library and the `include` command
----------------------------------------------
alias symbol "covers" = "new covers set".
alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
ntheorem new_coverage_infinity:
∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
#A; #U; #a; (** screenshot "n-cov-inf-1". *)
projects / helm.git / blobdiff