X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=f1795462b29f2e7a0f70a885ba81266a35f6bf2a;hb=21e0138ea9ff36fcc85e21081aa996d8eb063fb3;hp=8bba1228176ee0eea57c91bb723636f196916928;hpb=1a4b02e346356b7e1be253f7660c1d617c1ffe0a;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 8bba12281..f1795462b 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -14,7 +14,7 @@ by S.Berardi and S. 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 -this a important part of every formalization, not only for the aesthetic +this is a 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 @@ -63,7 +63,7 @@ implements two unusual input facilities: - â can be typed with `\Forall` - λ can be typed with `\lambda` - â can be typed with `\def` or `:=` - - â can be typed with `to` 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 @@ -71,20 +71,43 @@ implements two unusual input facilities: example W has Ω, ð and ð, L has Î, ð, and ð, F has Φ, ⦠Variants are listed in the aforementioned TeX/UTF-8 table. +Pressing `F1` opens the Matita manual. + CIC (as implemented in Matita) 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 +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 +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 +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`). + +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). -Type is a set equipped with the Id equality (i.e. an intensional, +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 = symbols only to the equality of a setoid, +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. @@ -92,8 +115,6 @@ and Type[1] for classes. For every Type[i] there is a corresponding level of predicative propositions CProp[i]. -CIC is also equipped with an impredicative sort Prop that we will not -use in this tutorial. The standard library and the `include` command ---------------------------------------------- @@ -103,11 +124,11 @@ are part of the standard library of Matita. These notions come with some standard notation attached to them: -- A ⪠B `A \cup B` -- A â© B `A \cap B` -- A ⬠B `A \between B` -- x â A `x \in A` -- Ω^A, that is the type of the subsets of A, `\Omega ^ A` +- 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: @@ -116,26 +137,6 @@ D*) include "sets/sets.ma". -(*HIDE*) -(* move away *) -nlemma subseteq_intersection_l: âA.âU,V,W:Ω^A.U â W ⨠V â W â U â© V â W. -#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption; -nqed. - -nlemma subseteq_union_l: âA.âU,V,W:Ω^A.U â W â V â W â U ⪠V â W. -#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption; -nqed. - -nlemma subseteq_intersection_r: âA.âU,V,W:Ω^A.W â U â W â V â W â U â© V. -#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption; -nqed. - -ninductive sigma (A : Type[0]) (P : A â CProp[0]) : Type[0] â - sig_intro : âx:A.P x â sigma A P. - -interpretation "sigma" 'sigma \eta.p = (sigma ? p). -(*UNHIDE*) - (*D Some basic results that we will use are also part of the sets library: @@ -541,18 +542,18 @@ D*) nlet corec fish_rec (A:Ax) (U: Ω^A) (P: Ω^A) (H1: P â U) (H2: âa:A. a â P â âj: ð a. ð a j ⬠P): âa:A. âp: a â P. a â U â ?. - (** screenshot "def-fish-rec-1". *) -#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *) + (** screenshot "def-fish-rec-1". *) +#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *) ##[ nchange in H1 with (âb.bâP â bâU); (** screenshot "def-fish-rec-2-1". *) - napply H1; (** screenshot "def-fish-rec-3". *) + napply H1; (** screenshot "def-fish-rec-3". *) nassumption; -##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *) +##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *) - @; (** screenshot "def-fish-rec-6". *) + @; (** screenshot "def-fish-rec-6". *) ##[ napply x - ##| @; (** screenshot "def-fish-rec-7". *) + ##| @; (** screenshot "def-fish-rec-7". *) ##[ napply xC; - ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *) + ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *) nassumption; ##] ##] @@ -662,7 +663,7 @@ ndefinition cover_equation : âA:Ax.âU,X:Ω^A.CProp[0] â λA,U,X. ntheorem coverage_cover_equation : âA,U. cover_equation A U (âU). #A; #U; #a; @; #H; -##[ nelim H; #b; (* manca clear *) +##[ nelim H; #b; ##[ #bU; @1; nassumption; ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi); ##[ #E; @; napply E; @@ -755,25 +756,32 @@ The paper defines the image as > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) } -but this cannot be ..... MAIL +but this not so formal notation poses some problems. The image is +often used as the left hand side of the â predicate > Im[d(a,i)] â V -Allora ha una comoda interpretazione (che voi usate liberamente) +Of course this writing is interpreted by the authors as follows > âj:D(a,i). d(a,i,j) â V -Ma se voglio usare Im per definire C, che è un subset di S, devo per -forza (almeno credo) definire un subset, ovvero dire che +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 | ⦠}`. + +> Im[d(a,i)] = { y | âj:D(a,i). y = d(a,i,j) } -> Im[d(a,i)] = { y : S | â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. -Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua -uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si -scatenano i setoidi. Ovvero Im[d(a,i)] â V diventa il seguente +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. +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). D*) @@ -786,7 +794,10 @@ 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`. D*) @@ -823,18 +834,23 @@ interpretation "ordinals Succ" 'oS x = (oS ? x). (*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 system on which argument the function is (structurally) recursive. + +In the `oS` case we use a local definition to name the recursive call +since it is used twice. + Note that Matita does not support notation in the left hand side of a pattern match, and thus the names of the constructors have to be spelled out verbatim. -BLA let rec. Bla let_in. - D*) nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A â match x with [ oO â U - | oS y â let Un â famU A U y in Un ⪠{ x | âi.ðð¦[ð x i] â Un} + | oS y â let U_n â famU A U y in U_n ⪠{ x | âi.ðð¦[ð x i] â U_n} | oL a i f â { x | âj.x â famU A U (f j) } ]. notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }. @@ -873,8 +889,7 @@ infinity rule. D*) -nlemma ord_subset: - âA:nAx.âa:A.âi,f,U.âj:ð a i.Uâ½(f j) â Uâ½(Î f). +nlemma ord_subset: âA:nAx.âa:A.âi,f,U.âj:ð a i. Uâ½(f j) â Uâ½(Î f). #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption; nqed. @@ -894,9 +909,9 @@ 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 +> 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 @@ -904,8 +919,7 @@ tutorial and we thus assume it. D*) -naxiom setoidification : - âA:nAx.âa,b:A.âx.âU.a=b â b â Uâ½x â a â Uâ½x. +naxiom U_x_is_ext: âA:nAx.âa,b:A.âx.âU. a = b â b â Uâ½x â a â Uâ½x. (*D @@ -913,8 +927,7 @@ 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. D*) -ntheorem new_coverage_reflexive: - âA:nAx.âU:Ω^A.âa. a â U â a â U. +ntheorem new_coverage_reflexive: âA:nAx.âU:Ω^A.âa. a â U â a â U. #A; #U; #a; #H; @ (0); napply H; nqed. @@ -930,6 +943,8 @@ 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". *) @@ -942,7 +957,7 @@ ncut (âj.ð a i j â Uâ½(Î f)); @ (Î f+1); (** screenshot "n-cov-inf-7". *) @2; (** screenshot "n-cov-inf-8". *) @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *) -napply (setoidification ⦠Hd); napply Hf'; +napply (U_x_is_ext ⦠Hd); napply Hf'; nqed. (*D @@ -964,7 +979,12 @@ the `#` is a standard notation for the reflexivity property of the equality. D[n-cov-inf-4] Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and -its property. +its property. Note that the axiom `AC` was abstracted over `A,a,i,U` before +assuming `(âj:ð a i.âx:Ord A.ð a i j â Uâ½x)`. Thus the term that can be eliminated +is `AC ???? H'` where the system is able to infer every `?`. Matita provides +a facility to specify a number of `?` in a compact way, i.e. `â¦`. The system +expand `â¦` first to zero, then one, then two, three and finally four question +marks, "guessing" how may of them are needed. D[n-cov-inf-5] The paper proof does now a forward reasoning step, deriving (by the ord_subset @@ -987,7 +1007,7 @@ existential, obtaining `d` (of type `ð a i`) and the equation defining `x`. D[n-cov-inf-9] We just need to use the equational definition of `x` to obtain a conclusion -that can be proved with `Hf'`. We assumed that `U_x` is extensional for +that can be proved with `Hf'`. We assumed that `Uâ½x` is extensional for every `x`, thus we are allowed to use `Hd` and close the proof. D*) @@ -995,7 +1015,7 @@ D*) (*D The next proof is that â(U) is mininal. The hardest part of the proof -it to prepare the goal for the induction. The desiderata is to prove +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: @@ -1037,14 +1057,14 @@ D*) (*D -bla bla +The notion `Fâ½x` is again defined by recursion over the ordinal `x`. D*) nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A â match x with [ oO â F - | oS o â let Fo â famF A F o in Fo â© { x | âi:ð x.âj:ð x i.ð x i j â Fo } + | oS o â let F_o â famF A F o in F_o â© { x | âi:ð x.âj:ð x i.ð x i j â F_o } | oL a i f â { x | âj:ð a i.x â famF A F (f j) } ]. @@ -1058,11 +1078,10 @@ interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a). (*D The proof of compatibility uses this little result, that we -factored out. +proved outside the mail proof. D*) -nlemma co_ord_subset: - âA:nAx.âF:Ω^A.âa,i.âf:ð a i â Ord A.âj. Fâ½(Î f) â Fâ½(f j). +nlemma co_ord_subset: âA:nAx.âF:Ω^A.âa,i.âf:ð a i â Ord A.âj. Fâ½(Î f) â Fâ½(f j). #A; #F; #a; #i; #f; #j; #x; #H; napply H; nqed. @@ -1071,24 +1090,23 @@ nqed. We assume the dual of the axiom of choice, as in the paper proof. D*) -naxiom AC_dual : - âA:nAx.âa:A.âi,F. (âf:ð a i â Ord A.âx:ð a i.ð a i x â Fâ½(f x)) â âj:ð a i.âx:Ord A.ð a i j â Fâ½x. +naxiom AC_dual: âA:nAx.âa:A.âi,F. + (âf:ð a i â Ord A.âx:ð a i.ð a i x â Fâ½(f x)) â âj:ð a i.âx:Ord A.ð a i j â Fâ½x. (*D -Proving the anti-reflexivity property is simce, since the +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. D*) -ntheorem new_fish_antirefl: - âA:nAx.âF:Ω^A.âa. a â F â a â F. +ntheorem new_fish_antirefl: âA:nAx.âF:Ω^A.âa. a â F â a â F. #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo; nqed. (*D -bar +We now prove the compatibility property for the new fish relation. D*) ntheorem new_fish_compatible: @@ -1098,19 +1116,38 @@ napply AC_dual; #f; (** screenshot "n-f-compat-2". *) nlapply (aF (Îf+1)); #aLf; (** screenshot "n-f-compat-3". *) nchange in aLf with (a â Fâ½(Î f) ⧠âi:ð a.âj:ð a i.ð a i j â Fâ½(Î f)); (** screenshot "n-f-compat-4". *) -ncut (âj:ð a i.ð a i j â Fâ½(f j));##[ - ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *) - *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *) -napply aLf'; +ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *) +*; #j; #Hj; @j; (** screenshot "n-f-compat-6". *) +napply (co_ord_subset ⦠Hj); nqed. (*D D[n-f-compat-1] +After reducing to normal form the goal, we obseve it is exactly the conlusion of +the dual axiom of choice we just assumed. We thus apply it ad introduce the +fcuntion `f`. + D[n-f-compat-2] +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); +we thus explicitly give a convertible type for that hypothesis, corresponding +the computation of the `+1` step, plus the unfolding of `â©`. + D[n-f-compat-4] +We are interested in the right hand side of `aLf`, an in particular to +its intance where the generic index in `ð a` is `i`. + D[n-f-compat-5] +We then eliminate the existential, obtaining `j` and its property `Hj`. We provide +the same witness + D[n-f-compat-6] +What is left to prove is exactly the `co_ord_subset` lemma we factored out +of the main proof. D*) @@ -1120,9 +1157,12 @@ The proof that `â(F)` is maximal is exactly the dual one of the minimality of `â(U)`. Thus the main problem is to obtain `G â Fâ½o` before doing the induction over `o`. +Note that `G` is assumed to be of type `ð^A`, that means an extensional +subset of `S`, while `Ω^A` means just a subset (note that the former is bold). + D*) ntheorem max_new_fished: - âA:nAx.âG:ext_powerclass_setoid A.âF:Ω^A.G â F â (âa.a â G â âi.ðð¦[ð a i] ⬠G) â G â âF. + âA:nAx.âG:ð^A.âF:Ω^A.G â F â (âa.a â G â âi.ðð¦[ð a i] ⬠G) â G â âF. #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b; nchange with (G â Fâ½o); @@ -1130,14 +1170,41 @@ nelim o; ##[ napply GF; ##| #p; #IH; napply (subseteq_intersection_r ⦠IH); #x; #Hx; #i; ncases (H ⦠Hx i); #c; *; *; #d; #Ed; #cG; - @d; napply IH; + @d; napply IH; (** screenshot "n-f-max-1". *) alias symbol "prop2" = "prop21". -napply (. Ed^-1â¡#); napply cG; + napply (. Ed^-1â¡#); napply cG; ##| #a; #i; #f; #Hf; nchange with (G â { y | âx. y â Fâ½(f x) }); #b; #Hb; #d; napply (Hf d); napply Hb; ##] nqed. +(*D +D[n-f-max-1] +Here the situacion look 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 +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 +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). + +We want to rewrite the left hand side using `Ed` right-to-left (the default +is left-to-right). We thus write `Ed^-1`, that is a proof that `ð x i d = c`. + +The complete command is `napply (. Ed^-1â¡#)` that has to be read like: + +> perform some rewritings under a binary morphism, +> on the right do nothing, +> on the left rewrite with Ed right-to-left. + +After the rewriting step the goal is exactly the `cG` assumption. + +D*) + (*D
@@ -1175,6 +1242,7 @@ of the Curry-Howard isomorphism. Where `T_rect_CProp0` is the induction principle for the inductive type `T`. + Π⢠? : Q Q â¡ P nchange with Q; â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ Π⢠? : P @@ -1191,6 +1259,17 @@ computation). Î; H : P; Π⢠? : G + Î; H : Q; Π⢠? : G P â* Q + nnormalize in H; â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ + Î; H : P; Π⢠? : G + +Where `Q` is the normal form of `P` considering βδζιμν-reduction steps. + + + Π⢠? : Q P â* Q + nnormalize; â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ + Π⢠? : P + Π⢠?_2 : T â G Π⢠?_1 : T ncut T; â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ @@ -1206,6 +1285,10 @@ D*) (*D +