matita/matita/nlibrary/arithmetics/R.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 naxiom Q: Type[0].
  18 naxiom nat_to_Q: nat → Q.
  19 ncoercion nat_to_Q : ∀x:nat.Q ≝ nat_to_Q on _x:nat to Q.
  20 ndefinition bool_to_nat ≝ λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
  21 ncoercion bool_to_nat : ∀b:bool.nat ≝ bool_to_nat on _b:bool to nat.
  22 naxiom Qplus: Q → Q → Q.
  23 naxiom Qminus: Q → Q → Q.
  24 naxiom Qtimes: Q → Q → Q.
  25 naxiom Qdivides: Q → Q → Q.
  26 naxiom Qle : Q → Q → Prop.
  27 naxiom Qlt: Q → Q → Prop.
  28 naxiom Qmin: Q → Q → Q.
  29 naxiom Qmax: Q → Q → Q.
  30 interpretation "Q plus" 'plus x y = (Qplus x y).
  31 interpretation "Q minus" 'minus x y = (Qminus x y).
  32 interpretation "Q times" 'times x y = (Qtimes x y).
  33 interpretation "Q divides" 'divide x y = (Qdivides x y).
  34 interpretation "Q le" 'leq x y = (Qle x y).
  35 interpretation "Q lt" 'lt x y = (Qlt x y).
  36 naxiom Qtimes_plus: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
  37 naxiom Qmult_one: ∀q:Q. 1 * q = q.
  38 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
  39 naxiom Qtimes_distr: ∀q1,q2,q3:Q.(q3 * q1 + q3 * q2) = q3 * (q1 + q2).
  40 naxiom Qdivides_distr: ∀q1,q2,q3:Q.(q1 / q3 + q2 / q3) = (q1 + q2) / q3.
  41 naxiom Qplus_comm: ∀q1,q2. q1 + q2 = q2 + q1.
  42 naxiom Qplus_assoc: ∀q1,q2,q3. q1 + q2 + q3 = q1 + (q2 + q3).
  43 ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
  44 #a; #b; #c; //; nqed.
  45 naxiom Qle_refl: ∀q1. q1≤q1.
  46 naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
  47 naxiom Qlt_trans: ∀x,y,z. x < y → y < z → x < z.
  48 naxiom Qle_lt_trans1: ∀x,y,z. x ≤ y → y < z → x < z.
  49 naxiom Qle_lt_trans2: ∀x,y,z. x < y → y ≤ z → x < z.
  50 naxiom Qle_plus_compat: ∀x,y,z,t. x≤y → z≤t → x+z ≤ y+t.
  51 naxiom Qmult_zero: ∀q:Q. 0 * q = 0.
  52
  53 naxiom phi: Q. (* the golden number *)
  54 naxiom golden: phi = phi * phi + phi * phi * phi.
  55
  56 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
  57
  58 ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
  59 #n; #q; ncut (plus n 1 = S n);##[//##]
  60 //; nqed.
  61
  62 ntheorem Qplus_zero: ∀q:Q. 0 + q = q. //. nqed.
  63
  64 ncoinductive locate : Q → Q → Prop ≝
  65    L: ∀l,u. locate l ((1 - phi) * l + phi * u) → locate l u
  66  | H: ∀l,u. locate (phi * l + (1 - phi) * u) u → locate l u.
  67
  68 ndefinition locate_inv_ind':
  69  ∀l,u:Q.∀P:Q → Q → Prop.
  70   ∀H1: locate l ((1 - phi) * l + phi * u) → P l u.
  71   ∀H2: locate (phi * l + (1 - phi) * u) u → P l u.
  72    locate l u → P l u.
  73  #l; #u; #P; #H1; #H2; #p; ninversion p; #l; #u; #H; #E1; #E2;
  74  ndestruct; /2/.
  75 nqed.
  76
  77 ndefinition R ≝ ∃l,u:Q. locate l u.
  78
  79 (*
  80 nlet corec Q_to_locate q : locate q q ≝ L q q … (Q_to_locate q).
  81   //; nrewrite < (Qdivides_mult 3 q) in ⊢ (? % ?); //.
  82 nqed.
  83
  84 ndefinition Q_to_R : Q → R.
  85  #q; @ q; @q; //.
  86 nqed.
  87 *)
  88
  89 nlemma help_auto1: ∀q:Q. false * q = 0. #q; nnormalize; //. nqed.
  90
  91 (*
  92 nlet corec locate_add (l,u:?) (r1,r2: locate l u) (c1,c2:bool) :
  93  locate (l + l + c1 * phi + c2 * phi * phi) (u + u + c1 * phi + c2 * phi * phi) ≝ ?.
  94  napply (locate_inv_ind' … r1); napply (locate_inv_ind' … r2);
  95  #r2'; #r1'; ncases c1; ncases c2
  96   [ ##4: nnormalize; @1;
  97     nlapply (locate_add … r1' r2' false false); nnormalize;
  98     nrewrite > (Qmult_zero …); nrewrite > (Qmult_zero …); #K; nauto demod;
  99      #K;
 100     nnormalize in K; nrewrite > (Qmult_zero …) in K; nnormalize; #K;
 101     napplyS K;
 102
 103
 104
 105
 106   [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
 107     ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
 108         ##4: napplyS (Qle_plus_compat …leq1l leq2l)
 109       |##*: /2/ ]
 110  ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
 111      ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
 112       ##[ @1 ? (l1''+l2'') (u1''+u2'');
 113       ##[ napply Qle_plus_compat; /3/;
 114         ##| ##3: /2/;
 115         ##| napplyS (Qle_plus_compat …leq1u' leq2u');
 116
 117 (*
 118 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
 119  locate (l1 + l2) (u1 + u2) ≝ ?.
 120  napply (locate_inv_ind' … r1); napply (locate_inv_ind' … r2); #l2'; #u2'; #leq2l; #leq2u; #r2;
 121  #l1'; #u1'; #leq1l; #leq1u; #r1
 122   [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
 123     ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
 124         ##4: napplyS (Qle_plus_compat …leq1l leq2l)
 125       |##*: /2/ ]
 126  ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
 127      ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
 128       ##[ @1 ? (l1''+l2'') (u1''+u2'');
 129       ##[ napply Qle_plus_compat; /3/;
 130         ##| ##3: /2/;
 131         ##| napplyS (Qle_plus_compat …leq1u' leq2u');
 132       .
 133
 134 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
 135  match disjoint l1 u1 l2 u2 with
 136   [ true ⇒ True
 137   | false ⇒
 138 *)
 139 *)
 140
 141 include "topology/igft.ma".
 142 include "datatypes/pairs.ma".
 143 include "datatypes/sums.ma".
 144
 145 nrecord pre_order (A: Type[0]) : Type[1] ≝
 146  { pre_r :2> A → A → CProp[0];
 147    pre_refl: reflexive … pre_r;
 148    pre_trans: transitive … pre_r
 149  }.
 150
 151 nrecord Ax_pro : Type[1] ≝
 152  { AAx :> Ax;
 153    Aleq: pre_order AAx
 154  }.
 155
 156 interpretation "Ax_pro leq" 'leq x y = (pre_r ? (Aleq ?) x y).
 157
 158 (*CSC: per auto per sotto, ma non sembra aiutare *)
 159 nlemma And_elim1: ∀A,B. A ∧ B → A.
 160  #A; #B; *; //.
 161 nqed.
 162
 163 nlemma And_elim2: ∀A,B. A ∧ B → B.
 164  #A; #B; *; //.
 165 nqed.
 166 (*CSC: /fine per auto per sotto *)
 167
 168 ndefinition Rax : Ax_pro.
 169  @
 170   [ @ (Q × Q)
 171     [ #p; napply (unit + sigma … (λc. fst … p < fst … c ∧ fst … c < snd … c ∧ snd … c < snd … p))
 172     | #c; *
 173       [ #_; napply {c' | fst … c < fst … c' ∧ snd … c' < snd … c}
 174       | *; #c'; #_; napply {d' | fst … d' = fst … c  ∧ snd … d' = fst … c'
 175                                ∨ fst … d' = snd … c' ∧ snd … d' = snd … c } ]##]
 176 ##| @ (λc,d. fst … d ≤ fst … c ∧ snd … c ≤ snd … d)
 177      [ /2/
 178      | nnormalize; #z; #x; #y; *; #H1; #H2; *; /3/; (*CSC: perche' non va? *) ##]
 179 nqed.
 180
 181 ndefinition downarrow: ∀S:Ax_pro. Ω \sup S → Ω \sup S ≝
 182  λS:Ax_pro.λU:Ω ^S.{a | ∃b:S. b ∈ U ∧ a ≤ b}.
 183
 184 interpretation "downarrow" 'downarrow a = (downarrow ? a).
 185
 186 ndefinition fintersects: ∀S:Ax_pro. Ω \sup S → Ω \sup S → Ω \sup S ≝
 187  λS.λU,V. ↓U ∩ ↓V.
 188
 189 interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
 190
 191 ndefinition singleton ≝ λA.λa:A.{b | b=a}.
 192
 193 interpretation "singleton" 'singl a = (singleton ? a).
 194
 195 ninductive ftcover (A : Ax_pro) (U : Ω^A) : A → CProp[0] ≝
 196 | ftreflexivity : ∀a. a ∈ U → ftcover A U a
 197 | ftleqinfinity : ∀a,b. a ≤ b → ∀i. (∀x. x ∈ 𝐂 b i ↓ (singleton … a) → ftcover A U x) → ftcover A U a
 198 | ftleqleft     : ∀a,b. a ≤ b → ftcover A U b → ftcover A U a.
 199
 200 interpretation "ftcovers" 'covers a U = (ftcover ? U a).
 201
 202 ntheorem ftinfinity: ∀A: Ax_pro. ∀U: Ω^A. ∀a. ∀i. (∀x. x ∈ 𝐂 a i → x ◃ U) → a ◃ U.
 203  #A; #U; #a; #i; #H;
 204  napply (ftleqinfinity … a … i); //;
 205  #b; *; *; #b; *; #H1; #H2; #H3; napply (ftleqleft … b); //;
 206  napply H; napply H1 (*CSC: auto non va! *).
 207 nqed.
 208
 209 ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝
 210 | ftfish : ∀a.
 211     a ∈ F →
 212     (∀b. a ≤ b → ftfish A F b) →
 213     (∀b. a ≤ b → ∀i:𝐈 b. ∃x.  x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftfish A F x) →
 214     ftfish A F a.
 215
 216 interpretation "fish" 'fish a U = (ftfish ? U a).
 217
 218 nlemma ftcoreflexivity: ∀A: Ax_pro.∀F.∀a:A. a ⋉ F → a ∈ F.
 219  #A; #F; #a; #H; ncases H; //.
 220 nqed.
 221
 222 nlemma ftcoleqinfinity:
 223  ∀A: Ax_pro.∀F.∀a:A. a ⋉ F →
 224   ∀b. (a ≤ b → ∀i. (∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ x ⋉ F)).
 225  #A; #F; #a; #H; ncases H; /2/.
 226 nqed.
 227
 228 nlemma ftcoleqleft:
 229  ∀A: Ax_pro.∀F.∀a:A. a ⋉ F →
 230   (∀b. a ≤ b → b ⋉ F).
 231  #A; #F; #a; #H; ncases H; /2/.
 232 nqed.
 233
 234 alias symbol "I" (instance 7) = "I".
 235 alias symbol "I" (instance 18) = "I".
 236 alias symbol "I" (instance 18) = "I".
 237 alias symbol "I" (instance 18) = "I".
 238 nlet corec ftfish_coind
 239  (A: Ax_pro) (F: Ω^A) (P: A → CProp[0])
 240  (Hcorefl: ∀a. P a → a ∈ F)
 241  (Hcoleqleft: ∀a. P a → ∀b. a ≤ b → P b)
 242  (Hcoleqinfinity: ∀a. P a → ∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ P x)
 243 : ∀a:A. P a → a ⋉ F ≝ ?.
 244  #a; #H; @
 245   [ /2/
 246   | #b; #H; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); /2/
 247   | #b; #H1; #i; ncases (Hcoleqinfinity a H ? H1 i); #x; *; #H2; #H3;
 248     @ x; @; //; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); //]
 249 nqed.
 250
 251 (*CSC: non serve manco questo (vedi sotto) *)
 252 nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A).
 253  #A; //.
 254 nqed.
 255
 256 alias symbol "I" (instance 6) = "I".
 257 ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
 258  #A; #F; #a; #H; #i; nlapply (ftcoleqinfinity … F … a … i); //; #H;
 259  ncases H; #c; *; *; *; #b; *; #H1; #H2; #H3; #H4; @ b; @ [ napply H1 (*CSC: auto non va *)]
 260  napply (ftcoleqleft … c); //.
 261 nqed.
 262
 263 nrecord Pt (A: Ax_pro) : Type[1] ≝
 264  { pt_set: Ω^A;
 265    pt_inhabited: ∃a. a ∈ pt_set;
 266    pt_filtering: ∀a,b. a ∈ pt_set → b ∈ pt_set → ∃c. c ∈ (singleton … a) ↓ (singleton … b) → c ∈ pt_set;
 267    pt_closed: pt_set ⊆ {b | b ⋉ pt_set}
 268  }.
 269
 270 ndefinition Rd ≝ Pt Rax.
 271
 272 naxiom daemon: False.
 273
 274 ndefinition Q_to_R: Q → Rd.
 275  #q; @
 276   [ napply { c | fst … c < q ∧ q < snd … c  }
 277   | @ [ @ (Qminus q 1) (Qplus q 1) | ncases daemon ]
 278 ##| #c; #d; #Hc; #Hd; @ [ @ (Qmin (fst … c) (fst … d)) (Qmax (snd … c) (snd … d)) | ncases daemon]
 279 ##| #a; #H; napply (ftfish_coind Rax ? (λa. fst … a < q ∧ q < snd … a)); /2/
 280     [ /5/ | #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
 281       [ #w; nnormalize;
 282     ##| nnormalize;
 283   ]
 284 nqed.
 285