# Library Coqtail.Fresh.Reals.IZR

Require Import Raxiom Rconvenient.

Module IZR (Import T : CReals).

Module Rconvenient := Rconvenient T.
Import Rconvenient.

Open Scope R_scope.

Definition INR := fix f n := match n with OR0 | S n'R1 + f n' end.

Lemma INR_add : a b, INR (a + b) == INR a + INR b.
Proof.
intros a b; induction a.
simpl; rewrite IHa; ring.
Qed.

Lemma INR_S : n, INR (S n) == R1 + INR n.
Proof.
intros; reflexivity.
Qed.

Lemma INR_mul : a b, INR (a × b) == INR a × INR b.
Proof.
intros a b; induction a.
simpl; symmetry; apply Rmul_0_l.
Qed.

Lemma INR_IPR : p, INR (nat_of_P p) == IPR p.
Proof.
intros p.
induction p.
rewrite nat_of_P_xI, INR_S, INR_mul, IHp; simpl; ring.
rewrite nat_of_P_xO, INR_mul, IHp; simpl; ring.
simpl; ring.
Qed.

Lemma IZR_Zopp : z, IZR (- z) == - IZR z.
Proof.
intros z; induction z.
simpl; symmetry; apply Ropp_0.
reflexivity.
symmetry; apply Ropp_involutive.
Qed.

Lemma IZR_INR : n, IZR (Z_of_nat n) == INR n.
Proof.
intros n.
destruct n.
reflexivity.

rewrite
<- nat_of_P_o_P_of_succ_nat_eq_succ,
<- Zpos_eq_Z_of_nat_o_nat_of_P,
INR_IPR.
reflexivity.
Qed.

Lemma INR_sub : a b, le b aINR (a - b) == INR a - INR b.
Proof.
intros a b ab.
rewrite (le_plus_minus b a ab) at 2.
unfold Rsub.
reflexivity.
Qed.

Lemma Zopp_swap : a b, Zopp a = ba = Zopp b.
Proof.
intros a b H; rewrite <- H; ring.
Qed.

Lemma Zuminus : a b, (a + - b = a - b)%Z.
Proof.
intros; ring.
Qed.

Lemma Rpos_IPR : p, R0 < IPR p.
Proof.
intros p; induction p; simpl.
apply Rlt_trans with (R0 + R1).
apply Req_lt_compat_r with R1; [ symmetry; apply Radd_0_l | apply Rlt_0_1 ].

eapply Req_lt_compat_l; [ apply Rmul_0_r | ].
apply Rmul_lt_compat_l.
apply Rlt_0_2.
apply IHp.

eapply Req_lt_compat_l; [ apply Rmul_0_r | ].
apply Rmul_lt_compat_l.
apply Rlt_0_2.
apply IHp.

apply Rlt_0_1.
Qed.

Lemma Rdiscr_IPR_0 : p, IPR p ## R0.
Proof.
intros p; right; apply Rpos_IPR.
Qed.

Lemma IZR_opp : a, IZR (- a) == - IZR a.
Proof.
intros [ | p | p ]; simpl; symmetry.
apply Ropp_0.
reflexivity.
apply Ropp_involutive.
Qed.

Lemma IPR_psucc : a, IPR (Psucc a) == IPR a + R1.
Proof.
induction a.
simpl. rewrite IHa. now ring.

simpl. now ring.

simpl. ring.
Qed.

Lemma IPR_add_carry : a b, IPR (a + b) == IPR a + IPR b
IPR (Pplus_carry a b) == IPR a + IPR b + R1.
Proof.
induction a; simpl; intros.
destruct b.
simpl. destruct (IHa b) as [H1 H2]. rewrite H2. split.
now ring.

now ring.

simpl. destruct (IHa b) as [H1 H2]. rewrite H1, H2. split.
now ring.

now ring.

simpl. destruct (IHa 1%positive) as [H1 H2]. rewrite IPR_psucc. split.
now ring.

now ring.

destruct b; simpl.
destruct (IHa b) as [H1 H2]. split.
rewrite H1. now ring.

rewrite H2. now ring.

destruct (IHa b) as [H1 H2]. split.
rewrite H1. now ring.

rewrite H1. now ring.

destruct (IHa 1%positive) as [H1 H2 ]. split.
now intuition.

rewrite IPR_psucc. simpl. now ring.

destruct b.
simpl. split.
rewrite IPR_psucc. now ring.

rewrite IPR_psucc. now ring.

split.
simpl. now ring.

simpl. rewrite IPR_psucc. now ring.

simpl. split.
now ring.

ring.
Qed.

Lemma IPR_add : a b, IPR (a + b) == IPR a + IPR b.
Proof.
Qed.

Lemma IPR_sub : a b, Pcompare a b Eq = GtIPR (a - b) == IPR a - IPR b.
Proof.
intros a b Cab.
unfold Pminus.
remember (Pminus_mask a b) as pmab.
destruct (Pminus_mask_Gt _ _ Cab) as (z, (Hz, (eqz, Dz))).
destruct pmab as [ | p | ]; try congruence.
rewrite <- eqz.
unfold Rsub .
cut (p = z).
intro; subst; ring.
congruence.
Qed.

Lemma IZR_add : a b, IZR (a + b) == IZR a + IZR b.
Proof.
intros [ | a | a ] [ | b | b ]; simpl; try ring.

rewrite Z.pos_sub_spec; remember (a ?= b)%positive as Cab.
destruct Cab; simpl.
erewrite (Pcompare_Eq_eq a b); [ ring | ]; auto.
rewrite IPR_sub; [ ring | ]; apply ZC2; symmetry; assumption.
rewrite IPR_sub; [ ring | ]; auto.

rewrite Z.pos_sub_spec; remember (b ?= a)%positive as Cab.
destruct Cab; simpl.
erewrite (Pcompare_Eq_eq b a); [ ring | ]; auto.
rewrite IPR_sub; [ ring | ]; apply ZC2; symmetry; assumption.
rewrite IPR_sub; [ ring | ]; auto.

Qed.

Lemma IZR_sub : x y, IZR (x - y) == IZR x - IZR y.
Proof.
intros a b.
unfold Zminus, Rsub.
reflexivity.
Qed.

Lemma IZR_lt : x y, (x < y)%ZIZR x < IZR y.
Proof.
intros x y xy.
eapply Req_lt_compat_l; [ apply Radd_comm | ].
eapply Req_lt_compat_l; [ symmetry; apply Radd_opp_r | ].
eapply Req_lt_compat_r; [ apply Radd_comm | ].
eapply Req_lt_compat_r.
rewrite <- IZR_Zopp, <- IZR_add; reflexivity.

remember (y + - x)%Z as d.
assert (dp : (0 < d)%Z) by omega.
destruct d; try inversion dp.
simpl.
apply Rpos_IPR.
Qed.

Lemma IZR_le : x y, (x y)%ZIZR x IZR y.
Proof.
intros x y xy.
destruct (Z_le_lt_eq_dec _ _ xy).
left; apply IZR_lt; auto.
right; subst; apply Req_refl.
Qed.

Lemma IPR_mul : a b, IPR (a × b) == IPR a × IPR b.
Proof.
induction a.
simpl. intros. rewrite (IPR_add b ((a × b)~0)). simpl. rewrite IHa. now ring.

intros. simpl. rewrite IHa. now ring.

intros. simpl. ring.
Qed.

Lemma IZR_mul : a b, IZR (a × b) == IZR a × IZR b.
Proof.
intros [ | p | p ] [ | q | q ]; simpl; try rewrite IPR_mul; ring.
Qed.

Lemma IZR_eq : a b, a = bIZR a == IZR b.
Proof.
intros; subst; reflexivity.
Qed.

Ltac IZRify :=
replace R1 with (IZR 1) by reflexivity;
replace R0 with (IZR 0) by reflexivity;
repeat
rewrite <- IZR_sub ||
rewrite <- IZR_mul ||
rewrite <- IZR_opp);
apply IZR_eq || apply IZR_lt || apply IZR_le || idtac.

Ltac eq_lt_compat_r_tac t := eapply Req_lt_compat_r; [ t; reflexivity | ].
Ltac eq_lt_compat_l_tac t := eapply Req_lt_compat_l; [ t; reflexivity | ].
Ltac eq_le_compat_r_tac t := eapply Req_le_compat_r; [ t; reflexivity | ].
Ltac eq_le_compat_l_tac t := eapply Req_le_compat_l; [ t; reflexivity | ].
Ltac eq_eq_compat_l_tac t := eapply Req_trans; [ symmetry; t; reflexivity | ].
Ltac eq_eq_compat_r_tac t := symmetry; eapply Req_trans; [ symmetry; t; reflexivity | ]; symmetry.

Ltac eq_compat_l_tac t := match goal with
| |- _ == _eq_eq_compat_l_tac t
| |- _ < _eq_lt_compat_l_tac t
| |- _ _eq_le_compat_l_tac t end.

Ltac eq_compat_r_tac t := match goal with
| |- _ == _eq_eq_compat_r_tac t
| |- _ < _eq_lt_compat_r_tac t
| |- _ _eq_le_compat_r_tac t end.

Ltac IZRrel :=
eq_compat_r_tac IZRify;
eq_compat_l_tac IZRify;
match goal with
| |- _ == _try apply IZR_eq
| |- _ _try apply IZR_le
| |- _ < _try apply IZR_lt
end; try omega.

End IZR.