X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2FR.ma;h=e113fabf3c5b3572fc9e33229a14f58a8cc770e5;hb=1439ced76cb62f9c5f5e638c53a005c3843870ae;hp=684514fcf135902276902bbc4cf638f5ccd5d7a4;hpb=f4d1feaa9cc24ef94f72fe32603a71f8d65acd01;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 684514fcf..e113fabf3 100644
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -20,46 +20,158 @@ ncoercion nat_to_Q : ∀x:nat.Q ≝ nat_to_Q on _x:nat to Q.
 naxiom Qplus: Q → Q → Q.
 naxiom Qtimes: Q → Q → Q.
 naxiom Qdivides: Q → Q → Q.
+naxiom Qle : Q → Q → Prop.
+naxiom Qlt: Q → Q → Prop.
 interpretation "Q plus" 'plus x y = (Qplus x y).
 interpretation "Q times" 'times x y = (Qtimes x y).
 interpretation "Q divides" 'divide x y = (Qdivides x y).
-naxiom Qtimes_distr: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
+interpretation "Q le" 'leq x y = (Qle x y).
+interpretation "Q lt" 'lt x y = (Qlt x y).
+naxiom Qtimes_plus: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
 naxiom Qmult_one: ∀q:Q. 1 * q = q.
 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
+naxiom Qtimes_distr: ∀q1,q2,q3:Q.(q3 * q1 + q3 * q2) = q3 * (q1 + q2).
+naxiom Qdivides_distr: ∀q1,q2,q3:Q.(q1 / q3 + q2 / q3) = (q1 + q2) / q3.
+naxiom Qplus_comm: ∀q1,q2. q1 + q2 = q2 + q1.
+naxiom Qplus_assoc: ∀q1,q2,q3. q1 + q2 + q3 = q1 + (q2 + q3).
+ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
+#a; #b; #c; //; nqed.
+naxiom Qle_refl: ∀q1. q1≤q1.
+naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
+naxiom Qle_plus_compat: ∀x,y,z,t. x≤y → z≤t → x+z ≤ y+t.
 
-(*ndefinition aaa ≝ Qtimes_distr.
-ndefinition bbb ≝ Qmult_one.
-ndefinition ccc ≝ Qdivides_mult.*)
 
-naxiom disjoint: Q → Q → Q → Q → bool.
+(* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
+
+ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
+#n; #q; ncut (plus n 1 = S n);##[//##]
+//; nqed.
 
 ncoinductive locate : Q → Q → Prop ≝
-   L: ∀l,u. locate l ((2 * l + u) / 3) → locate l u
- | H: ∀l,u. locate ((l + 2 * u) / 3) u → locate l u.
+   L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u
+ | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u.
+
+ndefinition locate_inv_ind':
+ ∀x1,x2:Q.∀P:Q → Q → Prop.
+  ∀H1: ∀l',u'.x1≤l' → u'≤((2 * x1 + x2) / 3) → locate l' u' → P x1 x2. 
+  ∀H2: ∀l',u'. ((x1 + 2 * x2) / 3)≤l' → u'≤ x2 → locate l' u' → P x1 x2.
+   locate x1 x2 → P x1 x2.
+ #x1; #x2; #P; #H1; #H2; #p; ninversion p; #l; #l'; #u'; #u; #Ha; #Hb; #E1;
+ #E2; #E3; ndestruct; /2/ width=5.
+nqed.
 
 ndefinition R ≝ ∃l,u:Q. locate l u.
 
-nlet corec Q_to_locate q : locate q q ≝ L q q ?.
- (*NOT WORKING: nrewrite < (Qmult_one q) in ⊢ (? ? %); *)
- ncut (locate q q = locate q ((2*q+q)/3))
-  [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
-  | napply eq_f;
-    ncut ((2 * q + q) = ((2 * q + 1 * q))); //; #H;    
-    ncut (q = ((2 * q + q) / 3)); //;
-    ncut ((2 * q + q) = ((2 * q + 1 * q))); //; #K;
-    ncut (2 * q + 1 * q = 3 * q); /4/ ]
+nlet corec Q_to_locate q : locate q q ≝ L q q q q … (Q_to_locate q).
+  //; nrewrite < (Qdivides_mult 3 q) in ⊢ (? % ?); //.
 nqed.
 
 ndefinition Q_to_R : Q → R.
  #q; @ q; @q; //.
 nqed.
 
+(*
 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
  locate (l1 + l2) (u1 + u2) ≝ ?.
- ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1
-  [ @1; napply locate_add;
+ napply (locate_inv_ind' … r1); napply (locate_inv_ind' … r2); #l2'; #u2'; #leq2l; #leq2u; #r2;
+ #l1'; #u1'; #leq1l; #leq1u; #r1
+  [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
+    ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
+        ##4: napplyS (Qle_plus_compat …leq1l leq2l)
+      |##*: /2/ ]
+ ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
+     ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
+      ##[ @1 ? (l1''+l2'') (u1''+u2''); 
+      ##[ napply Qle_plus_compat; /3/;
+        ##| ##3: /2/;
+        ##| napplyS (Qle_plus_compat …leq1u' leq2u');
+      .
  
 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
  match disjoint l1 u1 l2 u2 with
   [ true ⇒ True
-  | false ⇒ 
\ No newline at end of file
+  | false ⇒ 
+*)
+
+include "topology/igft.ma".
+include "datatypes/pairs.ma".
+include "datatypes/sums.ma".
+
+nrecord pre_order (A: Type[0]) : Type[1] ≝
+ { pre_r :2> A → A → CProp[0];
+   pre_sym: reflexive … pre_r;
+   pre_trans: transitive … pre_r
+ }.
+
+nrecord Ax_pro : Type[1] ≝
+ { AAx :> Ax;
+   Aleq: pre_order AAx
+ }.
+
+interpretation "Ax_pro leq" 'leq x y = (pre_r ? (Aleq ?) x y).
+
+(*CSC: per auto per sotto, ma non sembra aiutare *)
+nlemma And_elim1: ∀A,B. A ∧ B → A.
+ #A; #B; *; //.
+nqed.
+
+nlemma And_elim2: ∀A,B. A ∧ B → B.
+ #A; #B; *; //.
+nqed.
+(*CSC: /fine per auto per sotto *)
+
+ndefinition Rax : Ax_pro.
+ @
+  [ @ (Q × Q)
+    [ #p; napply (unit + sigma … (λc. fst … p < fst … c ∧ fst … c < snd … c ∧ snd … c < snd … p))
+    | #c; *
+      [ #_; napply {c' | fst … c < fst … c' ∧ snd … c' < snd … c}
+      | *; #c'; #_; napply {d' | fst … d' = fst … c  ∧ snd … d' = fst … c'
+                               ∨ fst … d' = snd … c' ∧ snd … d' = snd … c } ]##]
+##| @ (λc,d. fst … d ≤ fst … c ∧ snd … c ≤ snd … d)
+     [ /2/
+     | nnormalize; #z; #x; #y; *; #H1; #H2; *; /3/; (*CSC: perche' non va? *) ##]
+nqed.
+
+ndefinition downarrow: ∀S:Ax_pro. Ω \sup S → Ω \sup S ≝
+ λS:Ax_pro.λU:Ω ^S.{a | ∃b:S. b ∈ U ∧ a ≤ b}.
+
+interpretation "downarrow" 'downarrow a = (downarrow ? a).
+
+ndefinition fintersects: ∀S:Ax_pro. Ω \sup S → Ω \sup S → Ω \sup S ≝
+ λS.λU,V. ↓U ∩ ↓V.
+
+interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
+
+ndefinition singleton ≝ λA.λa:A.{b | b=a}.
+
+interpretation "singleton" 'singl a = (singleton ? a).
+
+ninductive ftcover (A : Ax_pro) (U : Ω^A) : A → CProp[0] ≝
+| ftreflexivity : ∀a. a ∈ U → ftcover A U a
+| ftleqinfinity : ∀a,b. a ≤ b → ∀i. (∀x. x ∈ 𝐂 b i ↓ (singleton … a) → ftcover A U x) → ftcover A U a
+| ftleqleft     : ∀a,b. a ≤ b → ftcover A U b → ftcover A U a.
+
+interpretation "ftcovers" 'covers a U = (ftcover ? U a).
+
+ntheorem ftinfinity: ∀A: Ax_pro. ∀U: Ω^A. ∀a. ∀i. (∀x. x ∈ 𝐂 a i → x ◃ U) → a ◃ U.
+ #A; #U; #a; #i; #H;
+ napply (ftleqinfinity … a … i); //;
+ #x; *; *; #b; *; #H1; #H2; #H3; napply (ftleqleft … b); //;
+ napply H; napply H1 (*CSC: auto non va! *).
+nqed.
+
+ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝
+| ftfish : ∀a.
+    a ∈ F →
+    (∀b. a ≤ b → ftfish A F b) →
+    (∀b. a ≤ b → ∀i:𝐈 b. ∃x.  x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftfish A F x) →
+    ftfish A F a.
+
+interpretation "fish" 'fish a U = (ftfish ? U a).
+
+alias symbol "I" (instance 6) = "I".
+ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
+ #A; #F; #a; #H; ncases H; #b; #_; #_; #H2; #i; ncases (H2 … i); //;
+ #x; *; *; *; #y; *; #K2; #K3; #_; #K5; @y; @ K2; ncases K5 in K3; /2/.
+nqed.
\ No newline at end of file