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 alias symbol "eq" = "leibnitz's equality".
 131 alias symbol "eq" = "setoid1 eq".
 132 alias symbol "covers" = "covers".
 133 naxiom Ph :  ∀x.h x = O \liff  x ◃ ∅.
 134
 135 nlemma replace_char:
 136   ∀A:Ax.∀U,V.U ⊆ V → V ⊆ U → ∀a:A.a ◃ U → a ◃ V.
 137 #A; #U; #V;  #a; #H1; #H2; #E; nelim E;
 138 ##[ #b; #Hb; @; nauto;
 139 ##| #b; #i; #H3; #H4; @2 i; #c; #Hc; nauto; ##]
 140 nqed.
 141
 142 ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x.
 143 *; #a; #H;
 144 ncut (a ◃ { x | x ◃ ∅}); ##[
 145   napply (replace_char … { x | h x = O }); ##[ ##1,2: #x; ncases (Ph x);
 146      (* nauto; *) #H1; #H2; #H3; nauto; (* ??? *) ##]
 147   napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x);
 148      (* nauto; *) #E; napply E; ##]
 149   napply (axiom_cond … a one); ##] #H1;
 150 ncut (a ◃ ∅); ##[ napply (transitivity … H1); #x; nauto; ##] #H2;
 151 nlapply (col2_4 …H2); #H3;
 152 ncut (a ∈ 𝐂 a one); ##[
 153   nnormalize; ncases (Ph a); nrewrite > (H a); nauto; ##] #H4;
 154 nauto;
 155 nqed.
 156
 157