Library Coqtail.Fresh.Reals.Rrealize

Require Raxiom.
Require Import ZArith.

Definition pow2 : natpositive := fix f n := match n with OxH | S n'xO (f n') end.

Definition Zseq_Cauchy (Un : natZ) : Type := neps : nat,
{N : nat & p q, (N p)%nat → (N q)%nat
(
Zneg (pow2 p × pow2 q)
((Un p) × Zpos (pow2 q) - (Un q) × Zpos (pow2 p)) × Zpos (pow2 neps)
Zpos (pow2 p × pow2 q)
)%Z
}.

Module Rrealize : Raxiom.CReals.

Record _R : Type := Rdef {
Rseq : natZ;
Rcauchy : Zseq_Cauchy Rseq
}.

Definition R := _R.

Program Definition Const (c : Z) := Rdef (fun n ⇒ (c × Zpos (pow2 n))%Z) _.
Next Obligation.
Proof.
intros neps.
O; intros p q _ _.
repeat rewrite <- Zmult_assoc.
rewrite (Zmult_comm (Zpos (pow2 p))).
rewrite Zminus_diag, Zmult_0_l.
split.
apply Zlt_le_weak, Zlt_neg_0.
apply Zle_0_pos.
Qed.

Definition R0 := Const Z0.
Definition R1 := Const 1%Z.

Require Import Max.

Program Definition Radd a b := Rdef (fun n ⇒ (Rseq a n + Rseq b n)%Z) _.
Next Obligation.
Proof.
destruct a as (u, Hu).
destruct b as (v, Hv).
intros neps.
destruct (Hu (S neps)) as (Nu, HNu).
destruct (Hv (S neps)) as (Nv, HNv).
(max Nu Nv).
intros p q Hp Hq.
assert (Hpu := max_lub_l _ _ _ Hp);
assert (Hpv := max_lub_r _ _ _ Hp);
assert (Hqu := max_lub_l _ _ _ Hq);
assert (Hqv := max_lub_r _ _ _ Hq); clear Hp Hq.
assert (U := HNu p q Hpu Hqu).
assert (V := HNv p q Hpv Hqv).
assert (HR : a b c d e f g, (((a + b) × c - (d + e) × f) × g = (a × c - d × f) × g + (b × c - e × f) × g)%Z)
by (intros; ring).
rewrite HR.
cut ( e f a b,
(Zneg e a × 2 × f Zpos e
Zneg e b × 2 × f Zpos e
Zneg e a × f + b × f Zpos e)%Z).
intros HA; apply HA; simpl pow2 in U, V; rewrite Zpos_xO, Zmult_assoc in U, V; assumption.
clear.
intros e f a b Ha Hb.
rewrite <- (Zopp_involutive (Zneg e)), Zopp_neg in ×.
repeat rewrite <- (Zmult_comm f), Zmult_assoc in *; rewrite <- (Zmult_comm f).
assert (He : (0 < Zpos e)%Z) by reflexivity.
remember (Zpos e) as Pe.
remember (f × a)%Z as fa.
remember (f × b)%Z as fb.
omega.
Qed.

Program Definition Rmul a b := Rdef (fun n ⇒ (Rseq a n × Rseq b n × Zpos (pow2 n))%Z) _.
Next Obligation.
Admitted.

Program Definition Ropp a := Rdef (fun n- Rseq a n)%Z _.
Next Obligation.
destruct a as (u, Hu).
intros neps.
destruct (Hu neps) as (N, HN).
N; intros p q Hp Hq.
pose proof HN p q Hp Hq.
cut ( e a a' b b' f, (Zneg e (a × a' - b × b') × f Zpos e
Zneg e (- a × a' - - b × b') × f Zpos e)%Z).
intros HA; apply HA; auto.

clear.
intros e a a' b b' f Hab.
rewrite Zmult_minus_distr_r in ×.
repeat rewrite <- Zopp_mult_distr_l in ×.
rewrite <- (Zopp_involutive (Zneg e)), Zopp_neg in ×.
assert (He : (0 < Zpos e)%Z) by reflexivity.
remember (Zpos e) as Pe.
remember (a × a' × f)%Z as fa.
remember (b × b' × f)%Z as fb.
omega.
Qed.

Definition Rsub a b := Radd a (Ropp b).

Definition Rlt (a b : R) : Type := sigT (fun nepssigT (fun N
n, le N n
Rseq a n × Zpos (pow2 neps) + Zpos (pow2 n)
Rseq b n × Zpos (pow2 neps))%Z).

Definition Rgt (r1 r2 : R) := Rlt r2 r1.
Definition Rdiscr (r1 r2 : R) := sum (Rlt r1 r2) (Rlt r2 r1).
Definition Req (r1 r2 : R) := Rdiscr r1 r2False.
Definition Rle (r1 r2 : R) := sumor (Rlt r1 r2) (Req r1 r2).
Definition Rge (r1 r2 : R) := Rle r2 r1.

Program Definition Rinv (x : R) (_ : Rdiscr x R0) :=
Rdef (fun nZdiv (Zpos (pow2 n)) (Rseq x n))%Z _.
Next Obligation.
Let P2 := fun nZpos (pow2 n).
destruct x as (u, Cu).
destruct H as [ xneg | xpos ].
admit.

destruct xpos as (en, (Nen, Hen)).
simpl Rseq in Hen.
simpl.
intros neps.

Open Scope Z_scope.
assert (epscut : { N | ( p q, le N ple N q
((u q × P2 p - u p × P2 q) × P2 neps
u p × P2 p × u q × P2 q
(u q × P2 p - u p × P2 q) × P2 neps))
n, le N n → 0 < u n}).
admit.

destruct epscut as (N, (HN, upos)).
N.
intros p q Pp Pq.
specialize (HN p q Pp Pq); destruct HN as (HNl, HNu).
apply (Z_div_le _ _ (u p)) in HNl.
split.
admit.

unfold Zdiv.

Admitted.

Definition Rdiv x y (p : Rdiscr y R0) := Rmul x (Rinv y p).

Lemma Rlt_trans : x y z, Rlt x yRlt y zRlt x z.
Proof.
intros (x, Cx) (y, Cy) (z, Cz) (nxy, (Nxy, Hxy)) (nyz, (Nyz, Hyz)).
nxy; (max Nxy Nyz).
intros n Hn.
eapply Zle_trans.
apply Hxy; eapply max_lub_l; eauto.
cut (y n z n)%Z.
intros H.
apply Zmult_le_compat_r; auto.
apply Zlt_le_weak; reflexivity.

apply (Zmult_lt_0_le_reg_r _ _ (Zpos (pow2 nyz))).
reflexivity.
refine (Zle_trans _ _ _ _ (Hyz n (max_lub_r _ _ _ Hn))).
rewrite <- Zplus_0_r at 1.
apply Zplus_le_compat_l; apply Zlt_le_weak; reflexivity.
Qed.

Lemma Rlt_asym : x y : R, Rlt x yRlt y xFalse.
intros (x, Cx) (y, Cy) (nxy, (Nxy, Hxy)) (nyx, (Nyx, Hyx)).
simpl Rseq in ×.
pose (N := max Nxy Nyx).
assert (Zpospos : p, (0 < Zpos p)%Z) by reflexivity.
remember (Zpos (pow2 nxy)) as n1.
remember (Zpos (pow2 nyx)) as n2.
assert (Pn1 : (0 < n1)%Z) by (subst; reflexivity).
assert (Pn2 : (0 < n2)%Z) by (subst; reflexivity).
assert (XY := Hxy N (le_max_l _ _)).
assert (YX := Hyx N (le_max_r _ _)).
assert (XY2 := Zmult_le_compat_r _ _ n2 XY (Zlt_le_weak _ _ Pn2)).
assert (YX2 := Zmult_le_compat_r _ _ n1 YX (Zlt_le_weak _ _ Pn1)).
rewrite Zmult_plus_distr_l in ×.
repeat rewrite <- Zmult_assoc in ×.
rewrite <- (Zmult_comm n1) in ×.
repeat rewrite Zmult_assoc in ×.
cut ( a b p, (0 < pa + p × n1 bb + p × n2 aFalse)%Z).
intros HF; eapply (HF _ _ (Zpos (pow2 N)) (eq_refl _)); eauto.
clear -Pn1 Pn2.
intros.
assert (0 < p × n1)%Z by (apply Zmult_lt_0_compat; auto).
assert (0 < p × n2)%Z by (apply Zmult_lt_0_compat; auto).
set (p × n1)%Z in ×.
set (p × n2)%Z in ×.
omega.
Qed.

Lemma JOKER {P} : P.
Admitted.

Lemma Zneg_Zpos : p, Zneg p = Zopp (Zpos p).
Proof.
reflexivity.
Qed.

Lemma Req_lt_compat_l : a b c : R, Req a bRlt a cRlt b c.
Proof.
intros (a, Ca) (b, Cb) (c, Cc) Heq (nac, (Nac, Hac)).
assert (Q : {a b}, ((a + b) → False) → (aFalse))
by intuition; assert (Nltab := Q _ _ Heq); clear Heq.
set (neps := S (S nac)).
destruct (Ca neps) as (Na, HNa).
destruct (Cb neps) as (Nb, HNb).
destruct (Cc neps) as (Nc, HNc).
assert (Easy : sigT (fun N ⇒ (le Nac N × le Na N × le Nb N × le Nc N)%type)) by admit.
destruct Easy as (N, (((NNac, NNa), NNb), NNc)).
neps; N.
intros n Hn.
simpl Rseq.
assert (HNa' := HNa N n NNa JOKER).
assert (HNb' := HNb N n NNb JOKER).
assert (HNc' := HNc N n NNc JOKER).
assert (Hac' := Hac n JOKER).
simpl Rseq in ×.
unfold neps in *; simpl pow2 in *; rewrite Zpos_xO, (Zpos_xO (pow2 nac)) in ×.
rewrite Zneg_Zpos, Zpos_mult_morphism in ×.
set (DN := Zpos (pow2 N)) in ×.
set (Dn := Zpos (pow2 n)) in ×.
set (DE := Zpos (pow2 nac)) in ×.

destruct (Z_lt_le_dec (a N × 4 × DE + 2 × DN) (b N × 4 × DE)) as [AB | AB].
elimtype False.
apply Nltab.
nac; N; intros.
simpl Rseq.
fold DE.
assert (HNa'' := proj1 (HNa N n0 NNa JOKER)).
assert (HNb'' := HNb N n0 NNb JOKER).
rewrite Zneg_Zpos, Zpos_mult_morphism in ×.
set (Dn0 := Zpos (pow2 n0)) in *; fold DN in HNa'', HNb''.
apply Zmult_lt_0_le_reg_r with (4 × DN)%Z; [ reflexivity | ].
rewrite Zmult_plus_distr_l.
ring_simplify.
apply Zle_trans with (4 × a N × DE × Dn0 + 5 × Dn0 × DN)%Z.
apply Zplus_le_reg_r with (- 4 × a n0 × DE × DN - 5 × DN × Dn0)%Z.
ring_simplify.
assert (AP : a a' b b', a = a'b = b'Zle a bZle a' b')
by (intros; subst; auto).
refine (AP _ _ _ _ _ _ HNa''); ring.

apply Zle_trans with (4 × DE × Dn0 × b N - DN × Dn0)%Z.
replace (5 × Dn0 × DN)%Z with (5 × DN × Dn0)%Z by ring.
replace (4 × DE × Dn0 × b N)%Z with (4 × DE × b N × Dn0)%Z by ring.
rewrite <- Zmult_plus_distr_l.
rewrite <- Zmult_minus_distr_r.
apply Zmult_gt_0_le_compat_r; [ reflexivity | ].

clear HNa HNb HNc Hac.
ring_simplify.
replace (2 × (2 × DE))%Z with (4 × DE)%Z in × by ring.
remember (4 × DE)%Z as DE4.
rewrite Zmult_comm, Zmult_assoc, (Zmult_comm DE), <- HeqDE4.
rewrite <- Zmult_assoc, <- HeqDE4 in AB.

assert (I1 : (b n × DN × DE4 + Dn × DN b N × Dn × DE4)%Z).
admit.
assert (I2 : (b N × Dn × DE4 a N × Dn × DE4 + 2 × Dn × DN)%Z).
replace (b N × Dn × DE4)%Z with (Dn × (b N × DE4))%Z by ring.
replace (a N × Dn × DE4 + 2 × Dn × DN)%Z with (Dn × (a N × DE4 + 2 × DN))%Z by ring.
admit.
admit.
admit.
admit.
Qed.

Lemma Req_lt_compat_r : x1 x2 y : R, Req x1 x2Rlt y x1Rlt y x2.
Admitted.
Lemma Radd_lt_compat_l : x y1 y2 : R, Rlt y1 y2Rlt (Radd x y1) (Radd x y2).
Admitted.
Lemma Radd_eq_compat_l : x y1 y2, Req y1 y2Req (Radd x y1) (Radd x y2).
Admitted.
Lemma Rmul_lt_compat_l : x y1 y2 : R, Rlt R0 xRlt y1 y2Rlt (Rmul x y1) (Rmul x y2).
Admitted.
Lemma Rmul_eq_compat_l : x y1 y2, Req y1 y2Req (Rmul x y1) (Rmul x y2).
Admitted.
Lemma Rinv_0_lt_compat : (x : R) (pr : Rlt R0 x) (pr' : Rdiscr x R0), Rlt R0 (Rinv x pr').
Admitted.
Lemma Radd_comm : a b, Req (Radd a b) (Radd b a).
Admitted.
Lemma Radd_assoc : x y z, Req (Radd (Radd x y) z) (Radd x (Radd y z)).
Admitted.
Lemma Radd_opp_r : x, Req (Radd x (Ropp x)) R0.
Admitted.
Lemma Radd_0_l : x, Req (Radd R0 x) x.
Proof.
intros x [Lt | Lt]; destruct Lt as (NE, (N, HN));
assert (HNN := HN N (le_refl _));
simpl in HNN;
set (Rseq x N × Zpos (pow2 NE))%Z in *;
assert (0 < Zpos (pow2 N))%Z by reflexivity;
omega.
Qed.

Lemma Rmul_add_distr_l a b c : Req (Rmul a (Radd b c)) (Radd (Rmul a b) (Rmul a c)).
Admitted.
Lemma Rmul_comm : a b, Req (Rmul a b) (Rmul b a).
Proof.
intros a b [Lt | Lt]; destruct Lt as (NE, (N, HN));
assert (HNN := HN N (le_refl _));
simpl in HNN;
rewrite (Zmult_comm (Rseq b N)) in HNN;
set (Rseq a N × Rseq b N × Zpos (pow2 N) × Zpos (pow2 NE))%Z in *;
assert (0 < Zpos (pow2 N))%Z by reflexivity;
omega.
Qed.

Lemma Rmul_assoc : x y z, Req (Rmul (Rmul x y) z) (Rmul x (Rmul y z)).
Proof.
assert (BAH : a a' c, (a = a' → 0 < ca + c a'False)%Z) by (intros; omega).
intros a b c [Lt | Lt]; destruct Lt as (NE, (N, HN));
assert (HNN := HN N (le_refl _));
simpl in HNN;
(refine (BAH _ _ _ _ _ HNN); [ ring | reflexivity ]).
Qed.

Lemma Rmul_1_l : x, Req (Rmul R1 x) x.
Admitted.
Lemma Rinv_l : (x : R) (pr : Rdiscr x R0), Req (Rmul (Rinv x pr) x) R1.
Admitted.
Lemma Rlt_0_1 : Rlt R0 R1.
Proof.
O; O; intros n Hn.
simpl; rewrite Zpos_mult_morphism; omega.
Qed.

Fixpoint IPR (p : positive) : R :=
match p with
| xI pRadd (Rmul (Radd R1 R1) (IPR p)) R1
| xO pRmul (Radd R1 R1) (IPR p)
| xHR1
end.
Arguments Scope IPR [positive_scope].

Definition IZR (z : BinInt.Z) : R :=
match z with
| Z0R0
| Zpos pIPR p
| Zneg pRopp (IPR p)
end.
Arguments Scope IZR [Z_scope].

Definition Rdist x y d : Type := prod (Rlt (Rsub x y) d) (Rlt (Ropp d) (Rsub x y)).

Definition Rup (x : R) : Z := let (N, _) := Rcauchy x 1%nat in (Zdiv (Rseq x N) (Zpos (pow2 N))).

Lemma Rup_spec : r : R, Rdist r (IZR (Rup r)) R1.
Proof.
intros (u, Hu).
unfold Rup; simpl.
destruct (Hu 1%nat) as (N, HN).
split; O; N; intros n Hn.
destruct (HN N n (le_refl _) Hn) as (NS, NI).
simpl Hu.
assert (HNN := Hu 1%nat).
simpl Rup.

Admitted.

Definition Rseq_Cauchy (Un : natR) : Type := eps, Rlt R0 eps
{N : nat & p q, (N p)%nat → (N q)%natRdist (Un p) (Un q) eps}.

Definition Rseq_cv (Un : natR) (l : R) : Type := eps, Rlt R0 eps
{N : nat & n, (N n)%natRdist (Un n) l eps}.

Lemma Rcomplete : Un, Rseq_Cauchy Un{l : R & Rseq_cv Un l}.
Admitted.
End Rrealize.