]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 23 Sep 2009 21:34:32 +0000 (21:34 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 23 Sep 2009 21:34:32 +0000 (21:34 +0000)
helm/software/matita/nlibrary/topology/igft.ma

index 2355838190e3beaac9a8b83acddf58d2d3ab66f2..3c97b9c25000735971c09018c1a1f4c42a6e86a3 100644 (file)
@@ -10,7 +10,7 @@ the formalization of the paper
 > explicit solution for the conditions for an
 > inductive generation of formal topologies
 
-by S.Berardi and S. Valentini. 
+by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi. 
 
 Orientering
 -----------
@@ -75,19 +75,47 @@ Some basic results that we will use are also part of the sets library:
 Defining Axiom set
 ------------------
 
-records, ...
+records, projections, types of projections..
 
 DOCEND*)
 
 nrecord Ax : Type[1] ≝ { 
-  S:> setoid;
-  I: S → Type[0];
-  C: ∀a:S. I a → Ω ^ S
+  S :> setoid;
+  I :  S → Type[0];
+  C :  ∀a:S. I a → Ω ^ S
 }.
 
 (*DOCBEGIN
 
-TODO: coercion S.
+Note that the field `S` was declared with `:>` instead of a simple `:`.
+This declares the `S` projection to be a coercion. A coercion is 
+a function case the system automatically inserts when it is needed.
+In that case, the projection `S` has type `Ax → setoid`, and whenever
+the expected type of a term is `setoid` while its type is `Ax`, the 
+system inserts the coercion around it, to make the whole term well types.
+
+When formalizing an algebraic structure, declaring the carrier as a 
+coercion is a common practice, since it allows to write statements like
+
+    ∀G:Group.∀x:G.x * x^-1 = 1 
+
+The quantification over `x` of type `G` is illtyped, since `G` is a term
+(of type `Group`) and thus not a type. Since the carrier projection 
+`carr` of `G` is a coercion, that maps a `Group` into the type of 
+its elements, the system automatically inserts `carr` around `G`, 
+obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
+when it displays a term.
+
+In this particular case, the coercion `S` allows to write
+
+    ∀A:Ax.∀a:A.…
+
+Since `A` is not a type, but it can be turned into a `setoid` by `S`
+and a `setoid` can be turned into a type by its `carr` projection, the 
+composed coercion `carr ∘ S` is silently inserted.
+
+Implicit arguments
+------------------
 
 Something that is not still satisfactory, in that the dependent type
 of `I` and `C` are abstracted over the Axiom set. To obtain the
@@ -102,8 +130,10 @@ DOCEND*)
 
 One would like to write `I a` and not `I A a` under a context where
 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
-mecanism simply `A`). Matita performs type inference, thus writing
-`I ? a` is enough, since the second argument of `I` is typed by the 
+mecanism simply `A`). In Matita, a question mark represents an implicit
+argument, i.e. a missing piece of information the system is asked to
+infer. Matita performs some sort of type inference, thus writing
+`I ? a` is enough: since the second argument of `I` is typed by the 
 first one, the first one can be inferred just computing the type of `a`.
 
 DOCEND*) 
@@ -112,19 +142,21 @@ DOCEND*)
 
 (*DOCBEGIN
 
-This is still not completely satisfactory, and to fix this minor issue
-we have to introduce the notational support built in Matita.
+This is still not completely satisfactory, since you have always type 
+`?`; to fix this minor issue we have to introduce the notational
+support built in Matita.
 
 Notation for I and C
 --------------------
 
-Matita is quipped qith a quite complex notational support,
+Matita is quipped with a quite complex notational support,
 allowing the user to define and use mathematical notations 
 ([From Notation to Semantics: There and Back Again][1]). 
 
 Since notations are usually ambiguous (e.g. the frequent overloading of 
 symbols) Matita distinguishes between the term level, the 
-content level, and the presentation level. 
+content level, and the presentation level, allowing multiple 
+mappings between the contenet and the term level. 
 
 The mapping between the presentation level (i.e. what is typed on the 
 keyboard and what is displayed in the sequent window) and the content
@@ -146,7 +178,7 @@ would be accepted, since identifiers have precedence 90, but
 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
 
 To obtain the `𝐈` is enough to type `I` and then cycle between its
-similar symbols with ALT-L. The same for `𝐂`. Notationa cannot use
+similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
 regular letters or the round parentheses, thus their variants (like the 
 bold ones) have to be used.