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=a38e2eec7ddfd6ebc16ccdbdea0409be46433ff9;hpb=3e068a777bc4bda55d3c7eedc2eb8368e8acb6da;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index a38e2eec7..f1795462b 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -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,6 +71,8 @@ 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 -------------------------------------------- @@ -907,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 @@ -917,7 +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 @@ -942,6 +944,7 @@ 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". *) @@ -954,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 @@ -976,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 @@ -999,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*) @@ -1049,7 +1057,7 @@ D*) (*D -The notion `F_x` is again defined by recursion over the ordinal `x`. +The notion `Fâ½x` is again defined by recursion over the ordinal `x`. D*) @@ -1098,7 +1106,7 @@ nqed. (*D -bar +We now prove the compatibility property for the new fish relation. D*) ntheorem new_fish_compatible: @@ -1108,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*) @@ -1130,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); @@ -1140,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
@@ -1185,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 @@ -1201,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; â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ @@ -1216,6 +1285,10 @@ D*) (*D +