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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14 (*
  15 include "arithmetics/nat.ma".
  16 *)
  17 include "datatypes/bool.ma".
  18
  19 (*
  20 ndefinition two ≝ S (S O).
  21 ndefinition natone ≝ S O.
  22 ndefinition four ≝ two * two.
  23 ndefinition eight ≝ two * four.
  24 ndefinition natS ≝ S.
  25 *)
  26 include "topology/igft.ma".
  27
  28 nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
  29 nnormalize; nauto;
  30 nqed.
  31
  32 ninductive Sigma (A: Type[0]) (P: A → CProp[0]) : Type[0] ≝
  33  mk_Sigma: ∀a:A. P a → Sigma A P.
  34
  35 (*<< To be moved in igft.ma *)
  36 ninductive ncover (A : nAx) (U : Ω^A) : A → CProp[0] ≝
  37 | ncreflexivity : ∀a. a ∈ U → ncover A U a
  38 | ncinfinity    : ∀a. ∀i. (∀y.Sigma ? (λj.y = 𝐝 a i j) → ncover A U y) → ncover A U a.
  39
  40 interpretation "ncovers" 'covers a U = (ncover ? U a).
  41
  42 ntheorem ncover_cover_ok: ∀A:nAx.∀U.∀a:A. a ◃ U → cover (Ax_of_nAx A) U a.
  43  #A; #U; #a; #H; nelim H
  44   [ #n; #H1; @1; nassumption
  45   | #a; #i; #IH; #H; @2 [ napply i ]
  46     nnormalize; #y; *; #j; #E; nrewrite > E;
  47     napply H;
  48     /2/ ]
  49 nqed.
  50
  51 ntheorem cover_ncover_ok: ∀A:Ax.∀U.∀a:A. a ◃ U → ncover (nAx_of_Ax A) U a.
  52  #A; #U; #a; #H; nelim H
  53   [ #n; #H1; @1; nassumption
  54   | #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
  55     napply H; nnormalize; nassumption.
  56 nqed.
  57
  58 ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
  59
  60 interpretation "ncoverage cover" 'coverage U = (ncoverage ? U).
  61
  62 (*>> To be moved in igft.ma *)
  63
  64 (*XXX
  65 nlemma ncover_ind':
  66  ∀A:nAx.∀U,P:Ω^A.
  67    (U ⊆ P) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. 𝐝 a i j ∈ P) → a ∈ P) →
  68     ◃ U ⊆ P.
  69  #A; #U; #P; #refl; #infty; #a; #H; nelim H
  70   [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2;
  71             napply infty; nauto; ##]
  72 nqed.
  73
  74 alias symbol "covers" (instance 3) = "ncovers".
  75 nlemma cover_ind'':
  76  ∀A:nAx.∀U:Ω^A.∀P:A → CProp[0].
  77   (∀a. a ∈ U → P a) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. P (𝐝 a i j)) → P a) →
  78    ∀b. b ◃ U → P b.
  79  #A; #U; #P; nletin V ≝ {x | P x}; napply (ncover_ind' … V).
  80 nqed.
  81 *)
  82
  83 (*********** from Cantor **********)
  84 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
  85 | refl1 : eq1 A A.
  86
  87 notation "hvbox( a break ∼ b)" non associative with precedence 40
  88 for @{ 'eqT $a $b }.
  89
  90 interpretation "eq between types" 'eqT a b = (eq1 a b).
  91
  92 ninductive unit : Type[0] ≝ one : unit.
  93
  94 ninductive option (A: Type[0]) : Type[0] ≝
  95    None: option A
  96  | Some: A → option A
  97  | Twice: A → A → option A.
  98
  99 nrecord uuAx : Type[1] ≝ {
 100   uuS : Type[0];
 101   uuC : uuS → option uuS
 102 }.
 103
 104 ndefinition uuax : uuAx → nAx.
 105 #A; @ (uuS A)
 106   [ #a; ncases (uuC … a) [ napply False | #_; napply unit | #_; #_; napply unit]
 107 ##| #a; ncases (uuC … a); nnormalize
 108      [ #H; napply (False_rect_Type1 … H)
 109      | #_; #_; napply unit
 110      | #_; #_; #_; napply bool ]
 111 ##| #a; ncases (uuC … a); nnormalize
 112      [ #H; napply (False_rect_Type1 … H)
 113      | #b; #_; #_; napply b
 114      | #b1; #b2; #_; * [ napply b1 | napply b2]##]##]
 115 nqed.
 116
 117 ncoercion uuax : ∀u:uuAx. nAx ≝ uuax on _u : uuAx to nAx.
 118
 119 nlemma eq_rect_Type0_r':
 120  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
 121  #A; #a; #x; #p; ncases p; nauto;
 122 nqed.
 123
 124 nlemma eq_rect_Type0_r:
 125  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
 126  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
 127 nqed.
 128
 129 nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
 130  { decide_mem:> A → bool;
 131    decide_mem_ok: ∀x. decide_mem x = true → x ∈ U;
 132    decide_mem_ko: ∀x. decide_mem x = false → ¬ (x ∈ U)
 133  }.
 134
 135 (*********** end from Cantor ********)
 136
 137 naxiom daemon: False.
 138
 139 nlemma csc_sym_eq: ∀A,x,y. eq A x y → eq A y x.
 140  #A; #x; #y; #H; ncases H; @1.
 141 nqed.
 142
 143 nlemma csc_eq_rect_CProp0_r':
 144  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. CProp[0]. P a → P x.
 145  #A; #a; #x; #p; #P; #H;
 146  napply (match csc_sym_eq ??? p return λa.λ_.P a with [ refl ⇒ H ]).
 147 nqed.
 148
 149 nlet rec cover_rect
 150  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
 151   (refl: ∀a:uuax A. a ∈ U → P a)
 152   (infty: ∀a:uuax A.∀i: 𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j.P (𝐝 a i j)) → P a)
 153    (b:uuax A) (p: b ◃ U) on p : P b
 154 ≝ ?.
 155  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
 156  ncases (decide_mem … memdec b)
 157   [ #_; #H; napply refl; nauto
 158   | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
 159     [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
 160       [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
 161     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
 162         nauto]
 163   ##| #a; #E;
 164       ncut (a ◃ U)
 165        [ nlapply E; nlapply (H ?) [nauto] ncases p
 166           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
 167         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
 168             nrewrite > E2; nnormalize; /2/ ]##]
 169       #Hcut;
 170       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
 171       napply (H2 one); #y
 172        [ napply Hcut
 173      ##| napply (cover_rect A U memdec P refl infty a); nauto ]
 174   ##| #a; #a1; #E;
 175       ncut (a ◃ U)
 176        [ nlapply E; nlapply (H ?) [nauto] ncases p
 177           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
 178         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
 179             nrewrite > E2; nnormalize; #_; @1 (true); /2/ ]##]
 180       #Hcut;
 181       ncut (a1 ◃ U)
 182        [ nlapply E; nlapply (H ?) [nauto] ncases p
 183           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
 184         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
 185             nrewrite > E2; nnormalize; #_; @1 (false); /2/ ]##]
 186       #Hcut1;
 187       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
 188       napply (H2 one); #y; ncases y; nnormalize
 189        [##1,2: nassumption
 190        | napply (cover_rect A U memdec P refl infty a); nauto
 191        | napply (cover_rect A U memdec P refl infty a1); nauto]
 192 nqed.
 193
 194 (********* Esempio:
 195    let rec skipfact n =
 196      match n with
 197       [ O ⇒ 1
 198       | S m ⇒ S m * skipfact (pred m) ]
 199 **)
 200
 201 ntheorem psym_plus: ∀n,m. n + m = m + n.
 202  #n; nelim n
 203   [ #m; nelim m; //; #n0; #H;
 204     nchange with (natS n0 = natS (n0 + O));
 205     nrewrite < H; //
 206   | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0);
 207     nrewrite > (H …);
 208     nelim m; //;
 209     #n1; #E; nrewrite > E; //]
 210 nqed.
 211
 212 nlemma easy1: ∀n:nat. two * (S n) = two + two * n.
 213  #n; nelim n;//;
 214  #n0; #H; nnormalize;
 215  nrewrite > (psym_plus ??);
 216  nrewrite > H; nnormalize;
 217  nrewrite > (psym_plus ??);
 218  //.
 219 nqed.
 220
 221 ndefinition skipfact_dom: uuAx.
 222  @ nat; #n; ncases n [ napply None | #m; napply (Some … (pred m)) ]
 223 nqed.
 224
 225 ntheorem skipfact_base_dec:
 226  memdec (uuax skipfact_dom) (mk_powerclass ? (λx: uuax skipfact_dom. x=O)).
 227  nnormalize; @ (λx. match x with [ O ⇒ true | S _ ⇒ false ]); #n; nelim n;
 228   nnormalize; //; #X; ndestruct; #Y; #Z; ndestruct; #W; ndestruct.
 229 nqed.
 230
 231 ntheorem skipfact_partial:
 232  ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
 233  #n; nelim n
 234   [ @1; nnormalize; @1
 235   | #m; #H; @2
 236      [ nnormalize; @1
 237      | nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m))));
 238        nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m);
 239        #E; nrewrite > E; nassumption ]##]
 240 nqed.
 241
 242 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
 243  #n; #D; napply (cover_rect … skipfact_base_dec … n D)
 244   [ #a; #_; napply natone
 245   | #a; ncases a
 246     [ nnormalize; #i; nelim i
 247     | #m; #i; nnormalize in i; #d; #H;
 248       napply (S m * H (pred m) …); //]
 249 nqed.
 250
 251 nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)]
 252  nnormalize; //.
 253 nqed.