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 alias symbol "covers" = "covers".
  32 ntheorem th2_3 :
  33   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
  34 #A; #a; #H; nelim H;
  35 ##[ #n; *;
  36 ##| #b; #i_star; #IH1; #IH2;
  37     ncases (EM … b i_star);
  38     ##[##2: (* nauto; *) #W; @i_star; napply W;
  39     ##| nauto;
  40     ##]
  41 ##]
  42 nqed.
  43
  44 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
  45 | refl1 : eq1 A A.
  46
  47 notation "hvbox( a break ∼ b)" non associative with precedence 40
  48 for @{ 'eqT $a $b }.
  49
  50 interpretation "eq between types" 'eqT a b = (eq1 a b).
  51
  52 ninductive unit : Type[0] ≝ one : unit.
  53
  54 nrecord uAx : Type[1] ≝ {
  55   uax_ : Ax;
  56   with_ : ∀a:uax_.𝐈 a ∼ unit
  57 }.
  58
  59 ndefinition uax : uAx → Ax.
  60 #A; @ (uax_ A) (λx.unit); #a; #_; napply (𝐂 a ?);  nlapply one; ncases (with_ A a); nauto;
  61 nqed.
  62
  63 ncoercion uax : ∀u:uAx. Ax ≝ uax on _u : uAx to Ax.
  64
  65 naxiom A: Type[0].
  66 naxiom S: A → Ω^A.
  67
  68 ndefinition axs: uAx.
  69 @; ##[ @ A (λ_.unit) (λa,x.S a); ##| #_; @; ##]
  70 nqed.
  71
  72 alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
  73 unification hint 0 ≔ ;
  74          x ≟ axs
  75   (* -------------- *) ⊢
  76          S x ≡ A.
  77
  78
  79 ntheorem col2_4 :
  80   ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##]
  81 #A; #a; #H; nelim H;
  82 ##[ #n; *;
  83 ##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); #H4; nauto;
  84 ##]
  85 nqed.
  86
  87 ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
  88
  89 ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
  90 #A; #a; #U; #V; #HUV; #H; nelim H;
  91 ##[ nauto;
  92 ##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##]
  93 nqed.
  94
  95 ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z.
  96 *; #a; *; #ZSa; #SaZ;
  97 ncut (a ◃ Z); ##[
  98   nlapply (axiom_cond … a one); #AxCon; nchange in AxCon with (a ◃ S a);
  99   (* nauto; *) napply (cover_monotone … AxCon); nassumption; ##] #H;
 100 ncut (a ◃ ∅); ##[ napply (transitivity … H); #x; #E; napply E; ##] #H1;
 101 ncut (¬ a ∈ S a); ##[ napply (col2_4 … H1); ##] #H2;
 102 ncut (a ∈ S a); ##[ napply ZSa; napply H1; ##] #H3;
 103 nauto;
 104 nqed.
 105
 106 include "nat/nat.ma".
 107
 108 naxiom phi : nat → nat → nat.
 109
 110 notation > "ϕ" non associative with precedence 90 for @{ 'phi }.
 111 interpretation "phi" 'phi = phi.
 112
 113 notation < "ϕ a i" non associative with precedence 90 for @{ 'phi2 $a $i}.
 114 interpretation "phi2" 'phi2 a i = (phi a i).
 115 notation < "ϕ a" non associative with precedence 90 for @{ 'phi1 $a }.
 116 interpretation "phi2" 'phi1 a = (phi a).
 117
 118 ndefinition caxs : uAx.
 119 @; ##[ @ nat (λ_.unit); #a; #_; napply { x | ϕ a x = O } ##| #_; @; ##]
 120 nqed.
 121
 122
 123 alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 124 unification hint 0 ≔ ;
 125          x ≟ caxs
 126   (* -------------- *) ⊢
 127          S x ≡ nat.
 128
 129 naxiom h : nat → nat.
 130
 131 alias symbol "eq" = "leibnitz's equality".
 132 alias symbol "eq" = "setoid1 eq".
 133 alias symbol "covers" = "covers".
 134 alias symbol "eq" = "leibnitz's equality".
 135 naxiom Ph :  ∀x.h x = O \liff  x ◃ ∅.
 136
 137 nlemma replace_char:
 138   ∀A:Ax.∀U,V.U ⊆ V → V ⊆ U → ∀a:A.a ◃ U → a ◃ V.
 139 #A; #U; #V;  #a; #H1; #H2; #E; nelim E;
 140 ##[ #b; #Hb; @; nauto;
 141 ##| #b; #i; #H3; #H4; @2 i; #c; #Hc; nauto; ##]
 142 nqed.
 143
 144 ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x.
 145 *; #a; #H;
 146 ncut (a ◃ { x | x ◃ ∅}); ##[
 147   napply (replace_char … { x | h x = O }); ##[ ##1,2: #x; ncases (Ph x);
 148      (* nauto; *) #H1; #H2; #H3; nauto; (* ??? *) ##]
 149   napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x);
 150      (* nauto; *) #E; napply E; ##]
 151   napply (axiom_cond … a one); ##] #H1;
 152 ncut (a ◃ ∅); ##[ napply (transitivity … H1); #x; nauto; ##] #H2;
 153 nlapply (col2_4 …H2); #H3;
 154 ncut (a ∈ 𝐂 a one); ##[
 155   nnormalize; ncases (Ph a); nrewrite > (H a); nauto; ##] #H4;
 156 nauto;
 157 nqed.
 158
 159