helm/software/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 naxiom Qplus: Q → Q → Q.
  21 naxiom Qtimes: Q → Q → Q.
  22 naxiom Qdivides: Q → Q → Q.
  23 naxiom Qle : Q → Q → Prop.
  24 naxiom Qlt: Q → Q → Prop.
  25 interpretation "Q plus" 'plus x y = (Qplus x y).
  26 interpretation "Q times" 'times x y = (Qtimes x y).
  27 interpretation "Q divides" 'divide x y = (Qdivides x y).
  28 interpretation "Q le" 'leq x y = (Qle x y).
  29 interpretation "Q lt" 'lt x y = (Qlt x y).
  30 naxiom Qtimes_plus: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
  31 naxiom Qmult_one: ∀q:Q. 1 * q = q.
  32 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
  33 naxiom Qtimes_distr: ∀q1,q2,q3:Q.(q3 * q1 + q3 * q2) = q3 * (q1 + q2).
  34 naxiom Qdivides_distr: ∀q1,q2,q3:Q.(q1 / q3 + q2 / q3) = (q1 + q2) / q3.
  35 naxiom Qplus_comm: ∀q1,q2. q1 + q2 = q2 + q1.
  36 naxiom Qplus_assoc: ∀q1,q2,q3. q1 + q2 + q3 = q1 + (q2 + q3).
  37 ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
  38 #a; #b; #c; //; nqed.
  39 naxiom Qle_refl: ∀q1. q1≤q1.
  40 naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
  41 naxiom Qle_plus_compat: ∀x,y,z,t. x≤y → z≤t → x+z ≤ y+t.
  42
  43
  44 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
  45
  46 ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
  47 #n; #q; ncut (plus n 1 = S n);##[//##]
  48 //; nqed.
  49
  50 ncoinductive locate : Q → Q → Prop ≝
  51    L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u
  52  | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u.
  53
  54 ndefinition locate_inv_ind ≝
  55 λx1,x2:Q.λP:Q → Q → Prop.
  56  λH1: ∀l',u'.x1≤l' → u'≤((2 * x1 + x2) / 3) → locate l' u' → P x1 x2.
  57  λH2: ∀l',u'. ((x1 + 2 * x2) / 3)≤l' → u'≤ x2 → locate l' u' → P x1 x2.
  58  λHterm:locate x1 x2.
  59   (λHcut:x1=x1 → x2=x2 → P x1 x2. Hcut (refl Q x1) (refl Q x2))
  60    match Hterm return λy1,y2.λp:locate y1 y2.
  61     x1=y1 → x2=y2 →P x1 x2
  62    with
  63     [ L l l' u' u Hle1 Hle2 r ⇒ ?(*H1 l l' u' u ?*)
  64     | H l l' u' u Hle1 Hle2 r ⇒ ?(*H2 l l' u' u ?*)].
  65 #a; #b; ##[ napply (H2 … r …) ##| napply (H1 … r …) ##] //.
  66 nqed.
  67
  68 ndefinition R ≝ ∃l,u:Q. locate l u.
  69
  70 nlet corec Q_to_locate q : locate q q ≝ L q q q q … (Q_to_locate q).
  71   //; nrewrite < (Qdivides_mult 3 q) in ⊢ (? % ?); //.
  72 nqed.
  73
  74 ndefinition Q_to_R : Q → R.
  75  #q; @ q; @q; //.
  76 nqed.
  77
  78 (*
  79 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
  80  locate (l1 + l2) (u1 + u2) ≝ ?.
  81  ninversion r1; ninversion r2; #l2'; #u2'; #leq2l; #leq2u; #r2;
  82  #l1'; #u1'; #leq1l; #leq1u; #r1
  83   [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
  84     ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
  85         ##4: napplyS (Qle_plus_compat …leq1l leq2l)
  86       |##*: /2/ ]
  87  ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
  88      ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
  89       ##[ @1 ? (l1''+l2'') (u1''+u2'');
  90       ##[ napply Qle_plus_compat; /3/;
  91         ##| ##3: /2/;
  92         ##| napplyS (Qle_plus_compat …leq1u' leq2u');
  93       .
  94
  95 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
  96  match disjoint l1 u1 l2 u2 with
  97   [ true ⇒ True
  98   | false ⇒
  99 *)
 100
 101 include "topology/igft.ma".
 102 include "datatypes/pairs.ma".
 103 include "datatypes/sums.ma".
 104
 105 nrecord pre_order (A: Type[0]) : Type[1] ≝
 106  { pre_r :2> A → A → CProp[0];
 107    pre_sym: reflexive … pre_r;
 108    pre_trans: transitive … pre_r
 109  }.
 110
 111 nrecord Ax_pro : Type[1] ≝
 112  { AAx :> Ax;
 113    Aleq: pre_order AAx
 114  }.
 115
 116 interpretation "Ax_pro leq" 'leq x y = (pre_r ? (Aleq ?) x y).
 117
 118 (*CSC: per auto per sotto, ma non sembra aiutare *)
 119 nlemma And_elim1: ∀A,B. A ∧ B → A.
 120  #A; #B; *; //.
 121 nqed.
 122
 123 nlemma And_elim2: ∀A,B. A ∧ B → B.
 124  #A; #B; *; //.
 125 nqed.
 126 (*CSC: /fine per auto per sotto *)
 127
 128 ndefinition Rax : Ax_pro.
 129  @
 130   [ @ (Q × Q)
 131     [ #p; napply (unit + sigma … (λc. fst … p < fst … c ∧ fst … c < snd … c ∧ snd … c < snd … p))
 132     | #c; *
 133       [ #_; napply {c' | fst … c < fst … c' ∧ snd … c' < snd … c}
 134       | *; #c'; #_; napply {d' | fst … d' = fst … c  ∧ snd … d' = fst … c'
 135                                ∨ fst … d' = snd … c' ∧ snd … d' = snd … c } ]##]
 136 ##| @ (λc,d. fst … d ≤ fst … c ∧ snd … c ≤ snd … d)
 137      [ /2/
 138      | nnormalize; #z; #x; #y; *; #H1; #H2; *; /3/; (*CSC: perche' non va? *) ##]
 139 nqed.
 140
 141 ndefinition downarrow: ∀S:Ax_pro. Ω \sup S → Ω \sup S ≝
 142  λS:Ax_pro.λU:Ω ^S.{a | ∃b:S. b ∈ U ∧ a ≤ b}.
 143
 144 interpretation "downarrow" 'downarrow a = (downarrow ? a).
 145
 146 ndefinition fintersects: ∀S:Ax_pro. Ω \sup S → Ω \sup S → Ω \sup S ≝
 147  λS.λU,V. ↓U ∩ ↓V.
 148
 149 interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
 150
 151 ndefinition singleton ≝ λA.λa:A.{b | b=a}.
 152
 153 interpretation "singleton" 'singl a = (singleton ? a).
 154
 155 ninductive ftcover (A : Ax_pro) (U : Ω^A) : A → CProp[0] ≝
 156 | ftreflexivity : ∀a. a ∈ U → ftcover A U a
 157 | ftleqinfinity : ∀a,b. a ≤ b → ∀i. (∀x. x ∈ 𝐂 b i ↓ (singleton … a) → ftcover A U x) → ftcover A U a
 158 | ftleqleft     : ∀a,b. a ≤ b → ftcover A U b → ftcover A U a.
 159
 160 interpretation "ftcovers" 'covers a U = (ftcover ? U a).
 161
 162 ntheorem ftinfinity: ∀A: Ax_pro. ∀U: Ω^A. ∀a. ∀i. (∀x. x ∈ 𝐂 a i → x ◃ U) → a ◃ U.
 163  #A; #U; #a; #i; #H;
 164  napply (ftleqinfinity … a … i); //;
 165  #x; *; *; #b; *; #H1; #H2; #H3; napply (ftleqleft … b); //;
 166  napply H; napply H1 (*CSC: auto non va! *).
 167 nqed.
 168
 169 ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝
 170 | ftfish : ∀a.
 171     a ∈ F →
 172     (∀b. a ≤ b → ftfish A F b) →
 173     (∀b. a ≤ b → ∀i:𝐈 b. ∃x.  x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftfish A F x) →
 174     ftfish A F a.
 175
 176 interpretation "fish" 'fish a U = (ftfish ? U a).
 177
 178 alias symbol "I" (instance 6) = "I".
 179 ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
 180  #A; #F; #a; #H; ncases H; #b; #_; #_; #H2; #i; ncases (H2 … i); //;
 181  #x; *; *; *; #y; *; #K2; #K3; #_; #K5; @y; @ K2; ncases K5 in K3; /2/.
 182 nqed.