naxiom Qdivides: Q → Q → Q.
naxiom Qle : Q → Q → Prop.
naxiom Qlt: Q → Q → Prop.
+naxiom Qmin: Q → Q → Q.
+naxiom Qmax: Q → Q → Q.
interpretation "Q plus" 'plus x y = (Qplus x y).
interpretation "Q minus" 'minus x y = (Qminus x y).
interpretation "Q times" 'times x y = (Qtimes x y).
#a; #b; #c; //; nqed.
naxiom Qle_refl: ∀q1. q1≤q1.
naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
+naxiom Qlt_trans: ∀x,y,z. x < y → y < z → x < z.
+naxiom Qle_lt_trans1: ∀x,y,z. x ≤ y → y < z → x < z.
+naxiom Qle_lt_trans2: ∀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.
naxiom Qmult_zero: ∀q:Q. 0 * q = 0.
nrecord pre_order (A: Type[0]) : Type[1] ≝
{ pre_r :2> A → A → CProp[0];
- pre_sym: reflexive … pre_r;
+ pre_refl: reflexive … pre_r;
pre_trans: transitive … pre_r
}.
#A; #F; #a; #H; ncases H; /2/.
nqed.
+(* XXX: disambiguation crazy *)
+alias id "I" = "cic:/matita/ng/topology/igft/I.fix(0,0,2)".
+nlet corec ftfish_coind
+ (A: Ax_pro) (F: Ω^A) (P: A → CProp[0])
+ (Hcorefl: ∀a:A. P a → a ∈ F)
+ (Hcoleqleft: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → P b)
+ (Hcoleqinfinity: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → ∀i:I A b. ∃x:A. x ∈ C A b i ↓ {(a)} ∧ P x)
+: ∀a:A. P a → a ⋉ F ≝ ?.
+ #a; #H; @
+ [ /2/
+ | #b; #H; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); /2/
+ | #b; #H1; #i; ncases (Hcoleqinfinity a H ? H1 i); #x; *; #H2; #H3;
+ @ x; @; //; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); //]
+nqed.
+
+(*CSC: non serve manco questo (vedi sotto)
+nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A).
+ #A; //.
+nqed.*)
+
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; #i; nlapply (ftcoleqinfinity … F … a … i); //; #H;
ncases H; #c; *; *; *; #b; *; #H1; #H2; #H3; #H4; @ b; @ [ napply H1 (*CSC: auto non va *)]
napply (ftcoleqleft … c); //.
-nqed.
\ No newline at end of file
+nqed.
+
+nrecord Pt (A: Ax_pro) : Type[1] ≝
+ { pt_set: Ω^A;
+ pt_inhabited: ∃a. a ∈ pt_set;
+ pt_filtering: ∀a,b. a ∈ pt_set → b ∈ pt_set → ∃c. c ∈ (singleton … a) ↓ (singleton … b) → c ∈ pt_set;
+ pt_closed: pt_set ⊆ {b | b ⋉ pt_set}
+ }.
+
+ndefinition Rd ≝ Pt Rax.
+
+naxiom daemon: False.
+
+ndefinition Q_to_R: Q → Rd.
+ #q; @
+ [ napply { c | fst … c < q ∧ q < snd … c }
+ | @ [ @ (Qminus q 1) (Qplus q 1) | ncases daemon ]
+##| #c; #d; #Hc; #Hd; @ [ @ (Qmin (fst … c) (fst … d)) (Qmax (snd … c) (snd … d)) | ncases daemon]
+##| #a; #H; napply (ftfish_coind Rax ? (λa. fst … a < q ∧ q < snd … a)); /2/
+ [ ncases daemon; ##| #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
+ [ #w; nnormalize; ncases daemon;
+ ##| nnormalize; ncases daemon;
+##]
+nqed.
+