# Library Coqtail.Fresh.Reals.Rorder

Require Import Raxiom Rconvenient IZR Repsilon Rapprox.
Require Import Arith.

Module Rorder (Import T : CReals).
Module Rconvenient := Rconvenient T. Import Rconvenient.
Module IZR := IZR T. Import IZR.
Module Repsilon := Repsilon T. Import Repsilon.
Module Rapprox := Rapprox T. Import Rapprox.

Section weak_constructive_eps.
Inductive exT {A : Set} (P : AType) : Prop :=
exT_intro : a, P aexT P.

Variable P : natType.
Hypothesis P_weak_decidable : n : nat, P (S n) + (P nFalse).

Let R (x y : nat) : Prop := x = S (S y) (P yFalse).

Lemma P_Acc : n, P nAcc R n.
Proof.
intros; constructor.
intros [] []; tauto.
Qed.

Lemma P_later_Acc : n x, P (n + x) → Acc R x.
Proof.
intros n; induction n.
apply P_Acc.

intros x Pnx; constructor; intros y (exy, npx).
apply IHn; subst.
do 2 rewrite <- plus_n_Sm.

destruct (P_weak_decidable (S (n + x))); [ auto | ].
tauto.
Qed.

Corollary exT_Acc_0 : exT PAcc R O.
Proof.
intros (n, Hn).
apply (P_later_Acc n).
rewrite <- plus_n_O; assumption.
Qed.

Lemma Acc_0_sigT : Acc R 0%natsigT P.
Proof.
intros HO.
pattern O.
apply (@Fix_F _ R); auto.
clear HO; intros x IHx.
destruct (P_weak_decidable x) as [ px | npx ].
(S x); auto.
assert (Rx : R (S (S x)) x); unfold R; eauto.
Qed.

Lemma exT_sigT : exT PsigT P.
Proof.
intros exP; apply Acc_0_sigT, exT_Acc_0; auto.
Qed.

End weak_constructive_eps.

Section DiscretePos.
Variable x : R.
Hypothesis xpos : inhabited (Rlt R0 x).
Definition pos_nat : natType := fun nR1 < x × po n.

Lemma pos_nat_weak_decidable : n, (pos_nat (S n)) + (pos_nat nFalse).
Proof.
intros n.
unfold pos_nat.
pose (xn := x × po (S (S n))); fold xn.
pose proof Rup_spec xn as Hzn.
set (zn := Rup xn); fold zn in Hzn.
destruct Hzn as (uxn, lxn).
destruct (Z_dec zn 3%Z) as [ [ lzn | gzn ] | ezn ].
right.
apply Rlt_asym.
apply Rmul_lt_cancel_r with ((R1 + R1) + (R1 + R1)).
do 2 apply Radd_pos_compat; apply Rlt_0_1.

apply (Req_lt_compat xn (IZR 4)); simpl.
unfold xn, po; simpl; ring.
ring.
apply Rlt_trans with (R1 + IZR zn).
apply (Radd_lt_compat_r (IZR zn)) in uxn.
apply Rle_lt_trans with (xn - IZR zn + IZR zn).
right. ring. apply uxn.

IZRrel.

left.
apply Rmul_lt_cancel_r with (R1 + R1).
IZRrel.

apply (Req_lt_compat (IZR 2) xn); simpl.
apply Rmul_comm.
unfold xn, po; simpl; ring.
apply Rlt_trans with (IZR zn - R1).
IZRrel.

apply (Radd_lt_compat_l (IZR zn)) in lxn.
apply Rlt_le_trans with (IZR zn + (xn - IZR zn)).
apply lxn. right. ring.

subst.
rewrite ezn in ×.
left.
apply Rmul_lt_cancel_r with (R1 + R1).
IZRrel.

apply (Req_lt_compat (IZR 2) xn); simpl.
apply Rmul_comm.
unfold xn, po; simpl; ring.
apply Radd_lt_cancel_r with (- IZR 3).
eapply Req_lt_compat; [ | | apply lxn ]; simpl.
ring.

ring_simplify.
IZRrel.
Qed.

Lemma sigT_pos_nat : sigT pos_nat.
Proof.

apply exT_sigT.
apply pos_nat_weak_decidable.

destruct xpos as [ xposT ].
destruct (Rpos_witness _ xposT) as (n, Hn).
n; specialize (Hn n (le_n _)).
apply (Rmul_lt_compat_r (po n) _ _ (Rpos_IPR _)) in Hn.
unfold pos_nat.
eapply Req_lt_compat; [ | | apply Hn ]; simpl.
apply Rinv_l.
reflexivity.
Qed.

Lemma Rlt_0_x : Rlt R0 x.
Proof.
destruct sigT_pos_nat as (n, Hn); unfold pos_nat in ×.
apply Rmul_lt_cancel_r with (po n).
apply Rpos_IPR.

apply Rlt_trans with R1.
eapply Req_lt_compat_l; [ | apply Rlt_0_1 ]; symmetry; apply Rmul_0_l.
auto.
Qed.

End DiscretePos.

Theorem Rpos_witness : x, inhabited (R0 < x) → R0 < x.
Proof.
apply Rlt_0_x.
Qed.

Theorem Rlt_witness : x y, inhabited (x < y) → x < y.
Proof.
intros x y L.
apply Rpos_lt, Rpos_witness.
destruct L; constructor.
apply Rlt_pos; auto.
Qed.

End Rorder.