From 1a4b02e346356b7e1be253f7660c1d617c1ffe0a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Oct 2009 14:59:23 +0000 Subject: [PATCH] ... --- .../matita/nlibrary/sets/partitions.ma | 2 ++ helm/software/matita/nlibrary/sets/sets.ma | 20 ++++++++++--------- .../software/matita/nlibrary/topology/igft.ma | 4 +++- 3 files changed, 16 insertions(+), 10 deletions(-) diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 80648f4ea..b8bc9bffe 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -19,6 +19,7 @@ include "nat/minus.ma". include "datatypes/pairs.ma". alias symbol "eq" = "setoid eq". +alias symbol "eq" = "setoid1 eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: ext_powerclass support; @@ -147,6 +148,7 @@ nlemma partition_splits_card: nlapply (f_sur ???? (fi nindex) y ?) [ alias symbol "refl" = "refl". alias symbol "prop1" = "prop11". +alias symbol "prop2" = "prop21 mem". napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] *; #nindex2; *; #Hni21; #Hni22; nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2); diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 623f676e9..3d03887ec 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -116,7 +116,8 @@ unification hint 0 ≔ A; (* ----------------------------------------------------- *) ⊢ carr1 R ≡ ext_powerclass A. - +interpretation "prop21 mem" 'prop2 l r = (prop21 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? l r). + (* ncoercion ext_carr' : ∀A.∀x:ext_powerclass_setoid A. Ω^A ≝ ext_carr on _x : (carr1 (ext_powerclass_setoid ?)) to (Ω^?). @@ -159,7 +160,7 @@ unification hint 0 ≔ A,a,a' nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A. #A; #S; #S'; @ (S ∩ S'); - #a; #a'; #Ha; @; *; #H1; #H2; @ + #a; #a'; #Ha; @; *; #H1; #H2; @ [##1,2: napply (. Ha^-1‡#); nassumption; ##|##3,4: napply (. Ha‡#); nassumption] nqed. @@ -192,8 +193,7 @@ unification hint 0 ≔ fun21 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A) R B C ≡ intersect ? B C. -interpretation "prop21 mem" 'prop2 l r = (prop21 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ???? l r). -interpretation "prop21 ext" 'prop2 l r = (prop21 (ext_powerclass_setoid ?) (ext_powerclass_setoid ?) ? ???? l r). +interpretation "prop21 ext" 'prop2 l r = (prop21 (ext_powerclass_setoid ?) (ext_powerclass_setoid ?) ? ? ???? l r). nlemma intersect_is_ext_morph: ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A). @@ -231,12 +231,13 @@ unification hint 0 ≔ unification hint 0 ≔ A, B : CPROP ⊢ iff A B ≡ eq_rel1 ? (eq1 CPROP) A B. -*) nlemma test: ∀U.∀A,B:𝛀^U. A ∩ B = A → ∀x,y. x=y → x ∈ A → y ∈ A ∩ B. #U; #A; #B; #H; #x; #y; #K; #K2; -napply (. (prop21 ??? ? ???? K^-1 (H^-1‡#))); + alias symbol "prop2" = "prop21 mem". + alias symbol "invert" = "setoid1 symmetry". + napply (. K^-1‡H); nassumption; nqed. @@ -251,14 +252,16 @@ nlemma intersect_ok: ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_power ##|##3,4: napply (. Ha‡#); nassumption]##] ##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H [ alias symbol "invert" = "setoid1 symmetry". - napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption + alias symbol "refl" = "refl". +alias symbol "prop2" = "prop21". +napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption | napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##] nqed. (* unfold if intersect, exposing fun21 *) alias symbol "hint_decl" = "hint_decl_Type1". unification hint 0 ≔ - A : setoid, B,C : qpowerclass A ⊢ + A : setoid, B,C : ext_powerclass A ⊢ pc A (fun21 … (mk_binary_morphism1 … (λS,S':qpowerclass_setoid A.mk_qpowerclass ? (S ∩ S') (mem_ok' ? (intersect_ok ? S S'))) @@ -271,7 +274,6 @@ nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x #A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption. nqed. *) -*) ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝ λA,B:setoid.λf:carr A → carr B.λSa:Ω^A. diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index feccae478..8bba12281 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -929,6 +929,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". *) @@ -1130,7 +1131,8 @@ nelim o; ##| #p; #IH; napply (subseteq_intersection_r … IH); #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG; @d; napply IH; - napply (. Ed^-1‡#); napply cG; + alias symbol "prop2" = "prop21". +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; ##] -- 2.39.2