From: Enrico Tassi Date: Wed, 14 Oct 2009 12:49:08 +0000 (+0000) Subject: tons of typo fixed X-Git-Tag: make_still_working~3307 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fe0042aeb03b19271cd61f402a44ec23e3100ea7;p=helm.git tons of typo fixed --- diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index f15bdfd4e..96f419aa3 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -78,10 +78,10 @@ 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 +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 occurr in types. +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 @@ -108,7 +108,7 @@ 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 will avoid using `Id` (Leibnitz equality), +not quotiented set). 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, @@ -116,7 +116,7 @@ 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. The index `i` is just a lable: constraints among +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] @@ -196,10 +196,10 @@ the alternative version of the axiom set. 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. +a "cast" function 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. +system inserts the coercion around it, to make the whole term well typed. When formalizing an algebraic structure, declaring the carrier as a coercion is a common practice, since it allows to write statements like @@ -208,12 +208,12 @@ coercion is a common practice, since it allows to write statements like The quantification over `x` of type `G` is ill-typed, 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 +`carr` 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. +obtaining `…∀x: carr G.…`. -In this particular case, the coercion `S` allows to write +Coercions are hidden by the system when it displays a term. +In this particular case, the coercion `S` allows to write (and read): ∀A:Ax.∀a:A.… @@ -230,8 +230,8 @@ precise type of a term, you can use the `ncheck` command as follows. D*) -(* ncheck I. *) -(* ncheck C. *) +(** ncheck I. *) (* shows: ∀A:Ax.A → Type[0] *) +(** ncheck C. *) (* shows: ∀A:Ax.∀a:A.A → I A a → Ω^A *) (*D @@ -239,17 +239,18 @@ 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 mechanism 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 +infer. Matita performs Hindley-Milner-style 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`. +first one, the first (omitted) argument can be inferred just +computing the type of `a` (that is `A`). D*) -(* ncheck (∀A:Ax.∀a:A.I ? a). *) +(** ncheck (∀A:Ax.∀a:A.I ? a). *) (* shows: ∀A:Ax.∀a:A.I A a *) (*D -This is still not completely satisfactory, since you have always type +This is still not completely satisfactory, since you have always to type `?`; to fix this minor issue we have to introduce the notational support built in Matita. @@ -355,7 +356,7 @@ predicate has to be carefully analyzed: The syntax separates with `:` abstractions that are fixed for every constructor (introduction rule) and abstractions that can change. In that -case the parameter `U` is abstracted once and forall in front of every +case the parameter `U` is abstracted once and for all in front of every constructor, and every occurrence of the inductive predicate is applied to `U` in a consistent way. Arguments abstracted on the right of `:` are not constant, for example the xcinfinity constructor introduces `a ◃ U`, @@ -376,7 +377,7 @@ This notion has to be abstracted over the cover relation (whose type is the arity of the inductive `xcover` predicate just defined). Then it has to be abstracted over the arguments of that cover relation, -i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`) +i.e. the axiom set and the set `U`, and the subset (in that case `𝐂 a i`) sitting on the left hand side of `◃`. D*) @@ -395,7 +396,7 @@ of the body. In that case all types are left implicit in the body. We now define the notation `a ◃ b`. Here the keywork `hvbox` and `break` tell the system how to wrap text when it does not -fit the screen (they can be safely ignore for the scope of +fit the screen (they can be safely ignored for the scope of this tutorial). We also add an interpretation for that notation, where the (abstracted) cover relation is implicit. The system will not be able to infer it from the other arguments `C` and `U` @@ -443,8 +444,8 @@ predicate we are defining, up to α-conversion); while the `nqed` command ends a definition or proof. We can now define the interpretation for the cover relation between an -element and a subset fist, then between two subsets (but this time -we fixed the relation `cover_set` is abstracted on). +element and a subset first, then between two subsets (but this time +we fix the relation `cover_set` is abstracted on). D*) @@ -455,10 +456,10 @@ interpretation "covers set" 'covers a U = (cover_set cover ? a U). We will proceed similarly for the fish relation, but before going on it is better to give a short introduction to the proof mode of Matita. -We define again the `cover_set` term, but this time we will build +We define again the `cover_set` term, but this time we build its body interactively. In the λ-calculus Matita is based on, CIC, proofs and terms share the same syntax, and it is thus possible to use the -commands devoted to build proof term to build regular definitions. +commands devoted to build proof term also to build regular definitions. A tentative semantics for the proof mode commands (called tactics) in terms of sequent calculus rules are given in the appendix. @@ -487,8 +488,9 @@ in the proof term. D[xcover-set-2] We have now to provide a proposition, and we exhibit it. We left a part of it implicit; since the system cannot infer it it will -ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition -whenever `?` is. +ask for it later. +Note that the type of `∀y:A.y ∈ C → ?` is a proposition +whenever `?` is a proposition. D[xcover-set-3] The proposition we want to provide is an application of the @@ -501,7 +503,7 @@ D[xcover-set-4] The system will now ask in turn the three implicit arguments passed to cover. The syntax `##[` allows to start a branching to tackle every sub proof individually, otherwise every command -is applied to every subrpoof. The command `##|` switches to the next +is applied to every subproof. The command `##|` switches to the next subproof and `##]` ends the branching. D*) @@ -534,8 +536,8 @@ interpretation "fish" 'fish a U = (fish ? U a). (*D -Introction rule for fish ------------------------- +Introduction rule for fish +--------------------------- Matita is able to generate elimination rules for inductive types, but not introduction rules for the coinductive case. @@ -546,7 +548,7 @@ D*) (*D -We thus have to define the introduction rule for fish by corecursion. +We thus have to define the introduction rule for fish by co-recursion. Here we again use the proof mode of Matita to exhibit the body of the corecursive function. @@ -609,10 +611,10 @@ both in `𝐂 a i` and `P`. D[def-fish-rec-5] We then introduce `x`, break the conjunction (the `*;` command is the equivalent of `ncases` but operates on the first hypothesis that can -be introduced. We then introduce the two sides of the conjunction. +be introduced). We then introduce the two sides of the conjunction. D[def-fish-rec-5-1] -The goal is now the existence of an a point in `𝐂 a i` fished by `U`. +The goal is now the existence of a point in `𝐂 a i` fished by `U`. We thus need to use the introduction rule for the existential quantifier. In CIC it is a defined notion, that is an inductive type with just one constructor (one introduction rule) holding the witness and the proof @@ -638,7 +640,7 @@ is already in the context. The right hand side needs to perform the co-recursive call. D[def-fish-rec-9] -The co-recursive call needs some arguments, but all of them live +The co-recursive call needs some arguments, but all of them are in the context. Instead of explicitly mention them, we use the `nassumption` tactic, that simply tries to apply every context item. @@ -651,7 +653,7 @@ Subset of covered/fished points We now have to define the subset of `S` of points covered by `U`. We also define a prefix notation for it. Remember that the precedence -of the prefix form of a symbol has to be lower than the precedence +of the prefix form of a symbol has to be higher than the precedence of its infix form. D*) @@ -665,7 +667,8 @@ interpretation "coverage cover" 'coverage U = (coverage ? U). (*D Here we define the equation characterizing the cover relation. -In the igft.ma file we proved that `◃U` is the minimum solution for +Even if it is not part of the paper, we proved that `◃(U)` is +the minimum solution for such equation, the interested reader should be able to reply the proof with Matita. @@ -696,8 +699,8 @@ nqed. (*D -We similarly define the subset of point fished by `F`, the -equation characterizing `⋉F` and prove that fish is +We similarly define the subset of points "fished" by `F`, the +equation characterizing `⋉(F)` and prove that fish is the biggest solution for such equation. D*) @@ -730,8 +733,8 @@ nqed. Part 2, the new set of axioms ----------------------------- -Since the name of objects (record included) has to unique -within the same script, we prefix every field name +Since the name of defined objects (record included) has to be unique +within the same file, we prefix every field name in the new definition of the axiom set with `n`. D*) @@ -746,9 +749,9 @@ nrecord nAx : Type[2] ≝ { (*D We again define a notation for the projections, making the -projected record an implicit argument. Note that since we already have -a notation for `𝐈` we just add another interpretation for it. The -system, looking at the argument of `𝐈`, will be able to use +projected record an implicit argument. Note that, since we already have +a notation for `𝐈`, we just add another interpretation for it. The +system, looking at the argument of `𝐈`, will be able to choose the correct interpretation. D*) @@ -765,6 +768,10 @@ interpretation "new I" 'I a = (nI ? a). (*D +The first result the paper presents to motivate the new formulation +of the axiom set is the possibility to define and old axiom set +starting from a new one and vice versa. The key definition for +such construction is the image of d(a,i). The paper defines the image as > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) } @@ -778,39 +785,41 @@ Of course this writing is interpreted by the authors as follows > ∀j:D(a,i). d(a,i,j) ∈ V -If we need to use the image to define 𝐂 (a subset of S) we are obliged to -form a subset, i.e. to place a single variable `{ here | … }`. +If we need to use the image to define `𝐂 ` (a subset of `S`) we are obliged to +form a subset, i.e. to place a single variable `{ here | … }` of type `S`. > Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) } This poses no theoretical problems, since `S` is a setoid and thus equipped with an equality. -Unless we difene two different images, one for stating the image is ⊆ of -something and another one to define 𝐂, we end up using always the latter. +Unless we define two different images, one for stating that the image is ⊆ of +something and another one to define `𝐂`, we end up using always the latter. Thus the statement `Im[d(a,i)] ⊆ V` unfolds to > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V -That up to rewriting with the equation defining `x` is what we mean. The -technical problem arises when `V` is a complex construction that has to -be proved extensional (i.e. ∀x,y. x = y → x ∈ V → y ∈ V). +That, up to rewriting with the equation defining `x`, is what we mean. +The technical problem arises later, when `V` will be a complex +construction that has to be proved extensional +(i.e. ∀x,y. x = y → x ∈ V → y ∈ V). D*) ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }. notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }. -notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }. +notation < "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }. interpretation "image" 'Im a i = (image ? a i). (*D -Thanks to our definition of image, we ca trivially a function mapping a -new axiom set to an old one and viceversa. Note that in the second -definition, when defining 𝐝, the projection of the Σ type is inlined -(constructed on the fly by `*;`) while in the paper it was named `fst`. +Thanks to our definition of image, we can define a function mapping a +new axiom set to an old one and vice versa. Note that in the second +definition, when we give the `𝐝` component, the projection of the +Σ-type is inlined (constructed on the fly by `*;`) +while in the paper it was named `fst`. D*) @@ -838,17 +847,18 @@ ninductive Ord (A : nAx) : Type[0] ≝ | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A. notation "0" non associative with precedence 90 for @{ 'oO }. -notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }. notation "x+1" non associative with precedence 50 for @{'oS $x }. +notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }. interpretation "ordinals Zero" 'oO = (oO ?). -interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f). interpretation "ordinals Succ" 'oS x = (oS ? x). +interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f). (*D -The dfinition of `U_x` is by recursion over the ordinal `x`. -We thus define a recursive function. The `on x` directive tells +The definition of `U⎽x` is by recursion over the ordinal `x`. +We thus define a recursive function using the `nlet rec` command. +The `on x` directive tells the system on which argument the function is (structurally) recursive. In the `oS` case we use a local definition to name the recursive call @@ -878,10 +888,10 @@ that is a character valid for identifier names, has been replaced by `⎽` that not. The symbol `⎽` can act as a separator, and can be typed as an alternative for `_` (i.e. pressing ALT-L after `_`). -The notion ◃(U) has to be defined as the subset of of y -belonging to U_x for some x. Moreover, we have to define the notion +The notion ◃(U) has to be defined as the subset of elements `y` +belonging to `U⎽x` for some `x`. Moreover, we have to define the notion of cover between sets again, since the one defined at the beginning -of the tutorial works only for the old axiom set definition. +of the tutorial works only for the old axiom set. D*) @@ -908,11 +918,11 @@ nqed. (*D -The proof of infinity uses the following form of the Axiom of choice, -that cannot be prove inside Matita, since the existential quantifier +The proof of infinity uses the following form of the Axiom of Choice, +that cannot be proved inside Matita, since the existential quantifier lives in the sort of predicative propositions while the sigma in the conclusion lives in the sort of data types, and thus the former cannot be eliminated -to provide the second. +to provide the witness for the second. D*) @@ -922,13 +932,13 @@ naxiom AC : ∀A,a,i,U. (*D In the proof of infinity, we have to rewrite under the ∈ predicate. -It is clearly possible to show that U⎽x is an extensional set: +It is clearly possible to show that `U⎽x` is an extensional set: > a = b → a ∈ U⎽x → b ∈ U⎽x -Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be -declared as morphisms. This poses to problem, but goes out of the scope of the -tutorial and we thus assume it. +Anyway this proof is a non trivial induction over x, that requires `𝐈` and `𝐃` to be +declared as morphisms. This poses no problem, but goes out of the scope of the +tutorial, since dependent morphisms are hard to manipulate, and we thus assume it. D*) @@ -936,8 +946,12 @@ naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ (*D -The reflexivity proof is trivial, it is enough to provide the ordinal 0 -as a witness, then ◃(U) reduces to U by definition, hence the conclusion. +The reflexivity proof is trivial, it is enough to provide the ordinal `0` +as a witness, then `◃(U)` reduces to `U` by definition, +hence the conclusion. Note that `0` is between `(` and `)` to +make it clear that it is a term (an ordinal) and not the number +of the constructor we want to apply (that is the first and only one +of the existential inductive type). D*) ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U. @@ -950,14 +964,8 @@ We now proceed with the proof of the infinity rule. D*) + alias symbol "covers" = "new covers set". -alias symbol "covers" = "new covers". -alias symbol "covers" = "new covers set". -alias symbol "covers" = "new covers". -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". *) @@ -976,18 +984,19 @@ nqed. (*D D[n-cov-inf-1] We eliminate the existential, obtaining an `i` and a proof that the -image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal +image of `𝐝 a i` is covered by U. The `nnormalize` tactic computes the normal form of `H`, thus expands the definition of cover between sets. D[n-cov-inf-2] -The paper proof considers `H` implicitly substitutes the equation assumed -by `H` in its conclusion. In Matita this step is not completely trivia. -We thus assert (`ncut`) the nicer form of `H`. +When the paper proof considers `H`, it implicitly substitutes assumed +equation defining `y` in its conclusion. +In Matita this step is not completely trivial. +We thus assert (`ncut`) the nicer form of `H` and prove it. D[n-cov-inf-3] After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`). What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that -becomes trivial is `j` is chosen to be `z`. In the command `napply #`, +becomes trivial if `j` is chosen to be `z`. In the command `napply #`, the `#` is a standard notation for the reflexivity property of the equality. D[n-cov-inf-4] @@ -1008,14 +1017,15 @@ To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`. D[n-cov-inf-7] The definition of `U⎽(…+1)` expands to the union of two sets, and proving -that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying -the second constructor `@2;` of the disjunction, we are left to prove that `a` -belongs to the right hand side. +that `a ∈ X ∪ Y` is, by definition, equivalent to prove that `a` is in `X` or `Y`. +Applying the second constructor `@2;` of the disjunction, +we are left to prove that `a` belongs to the right hand side of the union. D[n-cov-inf-8] -We thus provide `i`, introduce the element being in the image and we are -left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging -to the image means that there exists an object in the domain… we eliminate the +We thus provide `i` as the witness of the existential, introduce the +element being in the image and we are +left to prove that it belongs to `U⎽(Λf)`. In the meanwhile, since belonging +to the image means that there exists an object in the domain …, we eliminate the existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`. D[n-cov-inf-9] @@ -1027,7 +1037,7 @@ D*) (*D -The next proof is that ◃(U) is mininal. The hardest part of the proof +The next proof is that ◃(U) is minimal. The hardest part of the proof is to prepare the goal for the induction. The desiderata is to prove `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is, unfolding all definitions: @@ -1091,7 +1101,7 @@ interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a). (*D The proof of compatibility uses this little result, that we -proved outside the mail proof. +proved outside the main proof. D*) nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j). @@ -1110,7 +1120,7 @@ naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F. Proving the anti-reflexivity property is simple, since the assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0) -`a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis. +`a ∈ F⎽x`. If `x` is choose to be `0`, we obtain the thesis. D*) ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F. @@ -1136,7 +1146,7 @@ nqed. (*D D[n-f-compat-1] -After reducing to normal form the goal, we obseve it is exactly the conlusion of +After reducing to normal form the goal, we observe it is exactly the conclusion of the dual axiom of choice we just assumed. We thus apply it ad introduce the fcuntion `f`. @@ -1145,10 +1155,12 @@ The hypothesis `aF` states that `a⋉F⎽x` for every `x`, and we choose `Λf+1` D[n-f-compat-3] Since F_(Λf+1) is defined by recursion and we actually have a concrete input -`Λf+1` for that recursive function, it can compute. Anyway, using the `nnormalize` -tactic would reduce too much (both the `+1` and the `Λf` steps would be prformed); +`Λf+1` for that recursive function, it can be computed. +Anyway, using the `nnormalize` +tactic would reduce too much (both the `+1` and the `Λf` steps would be performed); we thus explicitly give a convertible type for that hypothesis, corresponding -the computation of the `+1` step, plus the unfolding of `∩`. +the computation of the `+1` step, plus the unfolding the definition of +the intersection. D[n-f-compat-4] We are interested in the right hand side of `aLf`, an in particular to @@ -1193,14 +1205,16 @@ nqed. (*D D[n-f-max-1] -Here the situacion look really similar to the one of the dual proof where +Here the situation looks really similar to the one of the dual proof where we had to apply the assumption `U_x_is_ext`, but here the set is just `G` -not `F_x`. Since we assumed `G` to be extensional we can employ the facilities +not `F_x`. Since we assumed `G` to be extensional we can +exploit the facilities Matita provides to perform rewriting in the general setting of setoids. -The lemma `.` simply triggers the mechanism, and the given argument has to -mimick the context under which the rewriting has to happen. In that case -we want to rewrite to the left of the binary morphism `∈`. The infix notation +The `.` notation simply triggers the mechanism, while the given argument has to +mimic the context under which the rewriting has to happen. In that case +we want to rewrite the left hand side of the binary morphism `∈`. +The infix notation to represent the context of a binary morphism is `‡`. The right hand side has to be left untouched, and the identity rewriting step is represented with `#` (actually a reflexivity proof for the subterm identified by the context).