From: Enrico Tassi Date: Tue, 13 Oct 2009 15:13:09 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3316 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50ab627986cbf241262e5969a757b1c6c95166f4;p=helm.git ... --- diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index a38e2eec7..a6d430cf1 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; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml index 3a1892cd4..8044ff2fa 100644 --- a/helm/software/matita/nlibrary/topology/preamble.xml +++ b/helm/software/matita/nlibrary/topology/preamble.xml @@ -4,15 +4,25 @@