helm/software/matita/nlibrary/topology/cantor.ma

   1
   2
   3 include "topology/igft.ma".
   4
   5 ntheorem axiom_cond: ∀A:Ax.∀a:A.∀i:𝐈 a.a ◃ 𝐂 a i.
   6 #A; #a; #i; @2 i; #x; #H; @; napply H;
   7 nqed.
   8
   9 nlemma hint_auto1 : ∀A,U,V. (∀x.x ∈ U → x ◃ V) → cover_set cover A U V.
  10 nnormalize; nauto.
  11 nqed.
  12
  13 alias symbol "covers" (instance 1) = "covers".
  14 alias symbol "covers" (instance 2) = "covers set".
  15 alias symbol "covers" (instance 3) = "covers".
  16 ntheorem transitivity: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
  17 #A; #a; #U; #V; #aU; #UV;
  18 nelim aU;
  19 ##[ #c; #H; nauto;
  20 ##| #c; #i; #HCU; #H; @2 i; nauto;
  21 ##]
  22 nqed.
  23
  24 ndefinition emptyset: ∀A.Ω^A ≝ λA.{x | False}.
  25
  26 notation "∅" non associative with precedence 90 for @{ 'empty }.
  27 interpretation "empty" 'empty = (emptyset ?).
  28
  29 naxiom EM : ∀A:Ax.∀a:A.∀i_star.(a ∈ 𝐂 a i_star) ∨ ¬( a ∈ 𝐂 a i_star).
  30
  31 ntheorem th2_3 :
  32   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
  33 #A; #a; #H; nelim H;
  34 ##[ #n; *;
  35 ##| #b; #i_star; #IH1; #IH2;
  36     ncases (EM … b i_star);
  37     ##[##2: (* nauto; *) #W; @i_star; napply W;
  38     ##| nauto;
  39     ##]
  40 ##]
  41 nqed.
  42
  43 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
  44 | refl1 : eq1 A A.
  45
  46 notation "hvbox( a break ∼ b)" non associative with precedence 40
  47 for @{ 'eqT $a $b }.
  48
  49 interpretation "eq between types" 'eqT a b = (eq1 a b).
  50
  51 ninductive unit : Type[0] ≝ one : unit.
  52
  53 nrecord uAx : Type[1] ≝ {
  54   uax_ : Ax;
  55   with_ : ∀a:uax_.𝐈 a ∼ unit
  56 }.
  57
  58 ndefinition uax : uAx → Ax.
  59 #A; @ (uax_ A) (λx.unit); #a; #_; napply (𝐂 a ?);  nlapply one; ncases (with_ A a); nauto;
  60 nqed.
  61
  62 ncoercion uax : ∀u:uAx. Ax ≝ uax on _u : uAx to Ax.
  63
  64 naxiom A: Type[0].
  65 naxiom S: A → Ω^A.
  66
  67 ndefinition axs: uAx.
  68 @; ##[ @ A (λ_.unit) (λa,x.S a); ##| #_; @; ##]
  69 nqed.
  70
  71 alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
  72 unification hint 0 ≔ ;
  73          x ≟ axs
  74   (* -------------- *) ⊢
  75          S x ≡ A.
  76
  77
  78 ntheorem col2_4 :
  79   ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##]
  80 #A; #a; #H; nelim H;
  81 ##[ #n; *;
  82 ##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); #H4; nauto;
  83 ##]
  84 nqed.
  85
  86 ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
  87
  88 ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
  89 #A; #a; #U; #V; #HUV; #H; nelim H;
  90 ##[ nauto;
  91 ##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##]
  92 nqed.
  93
  94 ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z.
  95 *; #a; *; #ZSa; #SaZ;
  96 ncut (a ◃ Z); ##[
  97   nlapply (axiom_cond … a one); #AxCon; nchange in AxCon with (a ◃ S a);
  98   (* nauto; *) napply (cover_monotone … AxCon); nassumption; ##] #H;
  99 ncut (a ◃ ∅); ##[ napply (transitivity … H); #x; #E; napply E; ##] #H1;
 100 ncut (¬ a ∈ S a); ##[ napply (col2_4 … H1); ##] #H2;
 101 ncut (a ∈ S a); ##[ napply ZSa; napply H1; ##] #H3;
 102 nauto;
 103 nqed.
 104
 105 include "nat/nat.ma".
 106
 107 naxiom phi : nat → nat → nat.
 108
 109 notation > "ϕ" non associative with precedence 90 for @{ 'phi }.
 110 interpretation "phi" 'phi = phi.
 111
 112 notation < "ϕ a i" non associative with precedence 90 for @{ 'phi2 $a $i}.
 113 interpretation "phi2" 'phi2 a i = (phi a i).
 114 notation < "ϕ a" non associative with precedence 90 for @{ 'phi1 $a }.
 115 interpretation "phi2" 'phi1 a = (phi a).
 116
 117 ndefinition caxs : uAx.
 118 @; ##[ @ nat (λ_.unit); #a; #_; napply { x | ϕ a x = O } ##| #_; @; ##]
 119 nqed.
 120
 121
 122 alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 123 unification hint 0 ≔ ;
 124          x ≟ caxs
 125   (* -------------- *) ⊢
 126          S x ≡ nat.
 127
 128 naxiom h : nat → nat.
 129
 130 naxiom Ph : ∀x.h x = O → x ◃ ∅.
 131
 132 ninductive eq2 (A : Type[1]) (a : A) : A → CProp[0] ≝
 133 | refl2 : eq2 A a a.
 134
 135 interpretation "eq2" 'eq T a b = (eq2 T a b).
 136
 137 ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x.
 138 *; #a; #H;
 139 ncut ((𝐂 a one) ⊆ { x | x ◃ ∅ }); (* bug *)
 140 nchange in xx with { x | h x
 141
 142
 143
 144
 145
 146
 147
 148
 149
 150
 151
 152
 153
 154
 155
 156
 157 ntheorem cantor: ∀a:axs. ¬ (Z ⊆ R a ∧ R a ⊆ Z).
 158 #a; *; #ZRa; #RaZ;
 159 ncut (a ◃ R a); ##[ @2; ##[ napply one; ##]  #x; #H; @; napply H; ##] #H1;
 160 ncut (a ◃ ∅); ##[
 161   napply (cover_trans … H1);
 162   #x; #H; nlapply (RaZ … H); #ABS; napply ABS; ##] #H2;
 163 ncut (a ∈ R a); ##[ napply ZRa; napply H2; ##] #H3;
 164 nelim H2 in H3;
 165 ##[ nauto.
 166 ##| nnormalize; nauto.  ##] (* se lo lancio su entrambi fallisce di width *)
 167 nqed.
 168
 169 ninductive deduct (A : nAx) (U : Ω^A) : A → CProp[0] ≝
 170 | drefl : ∀a.a ∈ U → deduct A U a
 171 | dcut  : ∀a.∀i:𝐈 a. (∀y:𝐃 a i.deduct A U (𝐝 a i y)) → deduct A U a.
 172
 173 notation " a ⊢ b " non associative with precedence 45 for @{ 'deduct $a $b }.
 174 interpretation "deduct" 'deduct a b = (deduct ? b a).
 175
 176 ntheorem th2_3_1 : ∀A:nAx.∀a:A.∀i:𝐈 a. a ⊢ 𝐈𝐦[𝐝 a i].
 177 #A; #a; #i;
 178 ncut (∀y:𝐃 a i.𝐝 a i y ⊢ 𝐈𝐦[𝐝 a i]); ##[ #y; @; @y; @; ##] #H1;
 179 napply (dcut … i); nassumption;
 180 nqed.
 181
 182 ntheorem th2_3_2 :
 183   ∀A:nAx.∀a:A.∀i:𝐈 a.∀U,V. a ⊢ U → (∀u.u ∈ U → u ⊢ V) → a ⊢ V.
 184 #A; #a; #i; #U; #V; #aU; #xUxV;
 185 nelim aU;
 186 ##[ nassumption;
 187 ##| #b; #i; #dU; #dV; @2 i; nassumption;
 188 ##]
 189 nqed.
 190
 191 ntheorem th2_3 :
 192   ∀A:nAx.
 193     (∀a:A.∀i_star.(∃y:𝐃 a i_star.𝐝 a i_star y = a) ∨ ¬(∃y:𝐃 a i_star.𝐝 a i_star y = a)) →
 194   ∀a:A. a ◃ ∅ → ∃i:𝐈 a. ¬ a \in Z
 195 #A; #EM; #a; #H; nelim H;
 196 ##[ #n; *;
 197 ##| #b; #i_star; #IH1; #IH2;
 198     ncases (EM b i_star);
 199     ##[##2: #W; @i_star; napply W;
 200     ##| *; #y_star; #E; nlapply (IH2 y_star); nrewrite > E; #OK; napply OK;
 201     ##]
 202 ##]
 203 nqed.
 204
 205 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
 206 | refl1 : eq1 A A.
 207
 208 notation "hvbox( a break ∼ b)" non associative with precedence 40
 209 for @{ 'eqT $a $b }.
 210
 211 interpretation "eq between types" 'eqT a b = (eq1 a b).
 212
 213 nrecord uAx : Type[1] ≝ {
 214   uax_ : Ax;
 215   with_ : ∀a:uax_.𝐈 a ∼ unit
 216 }.
 217
 218 ndefinition uax : uAx → Ax.
 219 *; #A; #E; @ A (λx.unit); #a; ncases (E a);
 220 ##[ #i; napply (𝐃 a i);
 221 ##| #i; nnormalize; #j; napply (𝐝 a i j);
 222 ##]
 223 nqed.
 224
 225 ncoercion uax : ∀u:unAx. nAx ≝ uax on _u : unAx to nAx.
 226
 227
 228 nlemma cor_2_5 : ∀A:unAx.∀a:A.∀i.a ⊢ ∅ → ¬(a ∈ 𝐈𝐦[𝐝 a i]).
 229 #A; #a; #i; #H; nelim H in i;
 230 ##[ #w; *;
 231 ##| #a; #i; #IH1; #IH2;
 232
 233
 234
 235