From Coq Require Import Psatz Reals ZArith.

Require Import Zaux.

Section Rmissing.

Theorem Rle_0_minus :
  ∀ x y, (x ≤ y)%R → (0 ≤ y - x)%R.

Theorem Rabs_eq_Rabs :
  ∀ x y : R,
  Rabs x = Rabs y → x = y ∨ x = Ropp y.

Theorem Rabs_minus_le:
  ∀ x y : R,
  (0 ≤ y)%R → (y ≤ 2×x)%R →
  (Rabs (x-y) ≤ x)%R.

Theorem Rabs_eq_R0 x : (Rabs x = 0 → x = 0)%R.

Theorem Rmult_lt_compat :
  ∀ r1 r2 r3 r4,
  (0 ≤ r1)%R → (0 ≤ r3)%R → (r1 < r2)%R → (r3 < r4)%R →
  (r1 × r3 < r2 × r4)%R.

Lemma Rmult_neq_reg_r :
  ∀ r1 r2 r3 : R, (r2 × r1 ≠ r3 × r1)%R → r2 ≠ r3.

Lemma Rmult_neq_compat_r :
  ∀ r1 r2 r3 : R,
  (r1 ≠ 0)%R → (r2 ≠ r3)%R →
  (r2 × r1 ≠ r3 × r1)%R.

Theorem Rmult_min_distr_r :
  ∀ r r1 r2 : R,
  (0 ≤ r)%R →
  (Rmin r1 r2 × r)%R = Rmin (r1 × r) (r2 × r).

Theorem Rmult_min_distr_l :
  ∀ r r1 r2 : R,
  (0 ≤ r)%R →
  (r × Rmin r1 r2)%R = Rmin (r × r1) (r × r2).

Lemma Rmin_opp: ∀ x y, (Rmin (-x) (-y) = - Rmax x y)%R.

Lemma Rmax_opp: ∀ x y, (Rmax (-x) (-y) = - Rmin x y)%R.

Theorem exp_le :
  ∀ x y : R,
  (x ≤ y)%R → (exp x ≤ exp y)%R.

Theorem Rinv_lt :
  ∀ x y,
  (0 < x)%R → (x < y)%R → (/y < /x)%R.

Theorem Rinv_le :
  ∀ x y,
  (0 < x)%R → (x ≤ y)%R → (/y ≤ /x)%R.

Theorem sqrt_ge_0 :
  ∀ x : R,
  (0 ≤ sqrt x)%R.

Lemma sqrt_neg : ∀ x, (x ≤ 0)%R → (sqrt x = 0)%R.

Lemma Rsqr_le_abs_0_alt :
  ∀ x y,
  (x² ≤ y² → x ≤ Rabs y)%R.

Theorem Rabs_le_inv :
  ∀ x y,
  (Rabs x ≤ y)%R → (-y ≤ x ≤ y)%R.

Theorem Rabs_ge :
  ∀ x y,
  (y ≤ -x ∨ x ≤ y)%R → (x ≤ Rabs y)%R.

Theorem Rabs_ge_inv :
  ∀ x y,
  (x ≤ Rabs y)%R → (y ≤ -x ∨ x ≤ y)%R.

Theorem Rabs_lt :
  ∀ x y,
  (-y < x < y)%R → (Rabs x < y)%R.

Theorem Rabs_lt_inv :
  ∀ x y,
  (Rabs x < y)%R → (-y < x < y)%R.

Theorem Rabs_gt :
  ∀ x y,
  (y < -x ∨ x < y)%R → (x < Rabs y)%R.

Theorem Rabs_gt_inv :
  ∀ x y,
  (x < Rabs y)%R → (y < -x ∨ x < y)%R.

End Rmissing.

Section IZR.

Theorem IZR_le_lt :
  ∀ m n p, (m ≤ n < p)%Z → (IZR m ≤ IZR n < IZR p)%R.

Theorem le_lt_IZR :
  ∀ m n p, (IZR m ≤ IZR n < IZR p)%R → (m ≤ n < p)%Z.

Theorem neq_IZR :
  ∀ m n, (IZR m ≠ IZR n)%R → (m ≠ n)%Z.

End IZR.

Section Rcompare.

Definition Rcompare x y :=
  match total_order_T x y with
  | inleft (left _) ⇒ Lt
  | inleft (right _) ⇒ Eq
  | inright _ ⇒ Gt
  end.

Inductive Rcompare_prop (x y : R) : comparison → Prop :=
  | Rcompare_Lt_ : (x < y)%R → Rcompare_prop x y Lt
  | Rcompare_Eq_ : x = y → Rcompare_prop x y Eq
  | Rcompare_Gt_ : (y < x)%R → Rcompare_prop x y Gt.

Theorem Rcompare_spec :
  ∀ x y, Rcompare_prop x y (Rcompare x y).

Global Opaque Rcompare.

Theorem Rcompare_Lt :
  ∀ x y,
  (x < y)%R → Rcompare x y = Lt.

Theorem Rcompare_Lt_inv :
  ∀ x y,
  Rcompare x y = Lt → (x < y)%R.

Theorem Rcompare_not_Lt :
  ∀ x y,
  (y ≤ x)%R → Rcompare x y ≠ Lt.

Theorem Rcompare_not_Lt_inv :
  ∀ x y,
  Rcompare x y ≠ Lt → (y ≤ x)%R.

Theorem Rcompare_Eq :
  ∀ x y,
  x = y → Rcompare x y = Eq.

Theorem Rcompare_Eq_inv :
  ∀ x y,
  Rcompare x y = Eq → x = y.

Theorem Rcompare_Gt :
  ∀ x y,
  (y < x)%R → Rcompare x y = Gt.

Theorem Rcompare_Gt_inv :
  ∀ x y,
  Rcompare x y = Gt → (y < x)%R.

Theorem Rcompare_not_Gt :
  ∀ x y,
  (x ≤ y)%R → Rcompare x y ≠ Gt.

Theorem Rcompare_not_Gt_inv :
  ∀ x y,
  Rcompare x y ≠ Gt → (x ≤ y)%R.

Theorem Rcompare_IZR :
  ∀ x y, Rcompare (IZR x) (IZR y) = Z.compare x y.

Theorem Rcompare_sym :
  ∀ x y,
  Rcompare x y = CompOpp (Rcompare y x).

Lemma Rcompare_opp :
  ∀ x y,
  Rcompare (- x) (- y) = Rcompare y x.

Theorem Rcompare_plus_r :
  ∀ z x y,
  Rcompare (x + z) (y + z) = Rcompare x y.

Theorem Rcompare_plus_l :
  ∀ z x y,
  Rcompare (z + x) (z + y) = Rcompare x y.

Theorem Rcompare_mult_r :
  ∀ z x y,
  (0 < z)%R →
  Rcompare (x × z) (y × z) = Rcompare x y.

Theorem Rcompare_mult_l :
  ∀ z x y,
  (0 < z)%R →
  Rcompare (z × x) (z × y) = Rcompare x y.

Theorem Rcompare_middle :
  ∀ x d u,
  Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).

Theorem Rcompare_half_l :
  ∀ x y, Rcompare (x / 2) y = Rcompare x (2 × y).

Theorem Rcompare_half_r :
  ∀ x y, Rcompare x (y / 2) = Rcompare (2 × x) y.

Theorem Rcompare_sqr :
  ∀ x y,
  Rcompare (x × x) (y × y) = Rcompare (Rabs x) (Rabs y).

Theorem Rmin_compare :
  ∀ x y,
  Rmin x y = match Rcompare x y with Lt ⇒ x | Eq ⇒ x | Gt ⇒ y end.

End Rcompare.

Section Rle_bool.

Definition Rle_bool x y :=
  match Rcompare x y with
  | Gt ⇒ false
  | _ ⇒ true
  end.

Inductive Rle_bool_prop (x y : R) : bool → Prop :=
  | Rle_bool_true_ : (x ≤ y)%R → Rle_bool_prop x y true
  | Rle_bool_false_ : (y < x)%R → Rle_bool_prop x y false.

Theorem Rle_bool_spec :
  ∀ x y, Rle_bool_prop x y (Rle_bool x y).

Theorem Rle_bool_true :
  ∀ x y,
  (x ≤ y)%R → Rle_bool x y = true.

Theorem Rle_bool_false :
  ∀ x y,
  (y < x)%R → Rle_bool x y = false.

End Rle_bool.

Section Rlt_bool.

Definition Rlt_bool x y :=
  match Rcompare x y with
  | Lt ⇒ true
  | _ ⇒ false
  end.

Inductive Rlt_bool_prop (x y : R) : bool → Prop :=
  | Rlt_bool_true_ : (x < y)%R → Rlt_bool_prop x y true
  | Rlt_bool_false_ : (y ≤ x)%R → Rlt_bool_prop x y false.

Theorem Rlt_bool_spec :
  ∀ x y, Rlt_bool_prop x y (Rlt_bool x y).

Theorem negb_Rlt_bool :
  ∀ x y,
  negb (Rle_bool x y) = Rlt_bool y x.

Theorem negb_Rle_bool :
  ∀ x y,
  negb (Rlt_bool x y) = Rle_bool y x.

Theorem Rlt_bool_true :
  ∀ x y,
  (x < y)%R → Rlt_bool x y = true.

Theorem Rlt_bool_false :
  ∀ x y,
  (y ≤ x)%R → Rlt_bool x y = false.

Lemma Rlt_bool_opp :
  ∀ x y,
  Rlt_bool (- x) (- y) = Rlt_bool y x.

End Rlt_bool.

Section Req_bool.

Definition Req_bool x y :=
  match Rcompare x y with
  | Eq ⇒ true
  | _ ⇒ false
  end.

Inductive Req_bool_prop (x y : R) : bool → Prop :=
  | Req_bool_true_ : (x = y)%R → Req_bool_prop x y true
  | Req_bool_false_ : (x ≠ y)%R → Req_bool_prop x y false.

Theorem Req_bool_spec :
  ∀ x y, Req_bool_prop x y (Req_bool x y).

Theorem Req_bool_true :
  ∀ x y,
  (x = y)%R → Req_bool x y = true.

Theorem Req_bool_false :
  ∀ x y,
  (x ≠ y)%R → Req_bool x y = false.

End Req_bool.

Section Floor_Ceil.

Definition Zfloor (x : R) := (up x - 1)%Z.

Theorem Zfloor_lb :
  ∀ x : R,
  (IZR (Zfloor x) ≤ x)%R.

Theorem Zfloor_ub :
  ∀ x : R,
  (x < IZR (Zfloor x) + 1)%R.

Theorem Zfloor_lub :
  ∀ n x,
  (IZR n ≤ x)%R →
  (n ≤ Zfloor x)%Z.

Theorem Zfloor_imp :
  ∀ n x,
  (IZR n ≤ x < IZR (n + 1))%R →
  Zfloor x = n.

Theorem Zfloor_IZR :
  ∀ n,
  Zfloor (IZR n) = n.

Theorem Zfloor_le :
  ∀ x y, (x ≤ y)%R →
  (Zfloor x ≤ Zfloor y)%Z.

Definition Zceil (x : R) := (- Zfloor (- x))%Z.

Theorem Zceil_ub :
  ∀ x : R,
  (x ≤ IZR (Zceil x))%R.

Theorem Zceil_lb :
  ∀ x : R,
  (IZR (Zceil x) < x + 1)%R.

Theorem Zceil_glb :
  ∀ n x,
  (x ≤ IZR n)%R →
  (Zceil x ≤ n)%Z.

Theorem Zceil_imp :
  ∀ n x,
  (IZR (n - 1) < x ≤ IZR n)%R →
  Zceil x = n.

Theorem Zceil_IZR :
  ∀ n,
  Zceil (IZR n) = n.

Theorem Zceil_le :
  ∀ x y, (x ≤ y)%R →
  (Zceil x ≤ Zceil y)%Z.

Theorem Zceil_floor_neq :
  ∀ x : R,
  (IZR (Zfloor x) ≠ x)%R →
  (Zceil x = Zfloor x + 1)%Z.

Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.

Theorem Ztrunc_IZR :
  ∀ n,
  Ztrunc (IZR n) = n.

Theorem Ztrunc_floor :
  ∀ x,
  (0 ≤ x)%R →
  Ztrunc x = Zfloor x.

Theorem Ztrunc_ceil :
  ∀ x,
  (x ≤ 0)%R →
  Ztrunc x = Zceil x.

Theorem Ztrunc_le :
  ∀ x y, (x ≤ y)%R →
  (Ztrunc x ≤ Ztrunc y)%Z.

Theorem Ztrunc_opp :
  ∀ x,
  Ztrunc (- x) = Z.opp (Ztrunc x).

Theorem Ztrunc_abs :
  ∀ x,
  Ztrunc (Rabs x) = Z.abs (Ztrunc x).

Theorem Ztrunc_lub :
  ∀ n x,
  (IZR n ≤ Rabs x)%R →
  (n ≤ Z.abs (Ztrunc x))%Z.

Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.

Theorem Zaway_IZR :
  ∀ n,
  Zaway (IZR n) = n.

Theorem Zaway_ceil :
  ∀ x,
  (0 ≤ x)%R →
  Zaway x = Zceil x.

Theorem Zaway_floor :
  ∀ x,
  (x ≤ 0)%R →
  Zaway x = Zfloor x.

Theorem Zaway_le :
  ∀ x y, (x ≤ y)%R →
  (Zaway x ≤ Zaway y)%Z.

Theorem Zaway_opp :
  ∀ x,
  Zaway (- x) = Z.opp (Zaway x).

Theorem Zaway_abs :
  ∀ x,
  Zaway (Rabs x) = Z.abs (Zaway x).

End Floor_Ceil.

Theorem Rcompare_floor_ceil_middle :
  ∀ x,
  IZR (Zfloor x) ≠ x →
  Rcompare (x - IZR (Zfloor x)) (/ 2) = Rcompare (x - IZR (Zfloor x)) (IZR (Zceil x) - x).

Theorem Rcompare_ceil_floor_middle :
  ∀ x,
  IZR (Zfloor x) ≠ x →
  Rcompare (IZR (Zceil x) - x) (/ 2) = Rcompare (IZR (Zceil x) - x) (x - IZR (Zfloor x)).

Theorem Zfloor_div :
  ∀ x y,
  y ≠ Z0 →
  Zfloor (IZR x / IZR y) = (x / y)%Z.

Theorem Ztrunc_div :
  ∀ x y, y ≠ 0%Z →
  Ztrunc (IZR x / IZR y) = Z.quot x y.

Section pow.

Variable r : radix.

Theorem radix_pos : (0 < IZR r)%R.

Definition bpow e :=
  match e with
  | Zpos p ⇒ IZR (Zpower_pos r p)
  | Zneg p ⇒ Rinv (IZR (Zpower_pos r p))
  | Z0 ⇒ 1%R
  end.

Theorem IZR_Zpower_pos :
  ∀ n m,
  IZR (Zpower_pos n m) = powerRZ (IZR n) (Zpos m).

Theorem bpow_powerRZ :
  ∀ e,
  bpow e = powerRZ (IZR r) e.

Theorem bpow_ge_0 :
  ∀ e : Z, (0 ≤ bpow e)%R.

Theorem bpow_gt_0 :
  ∀ e : Z, (0 < bpow e)%R.

Theorem bpow_plus :
  ∀ e1 e2 : Z, (bpow (e1 + e2) = bpow e1 × bpow e2)%R.

Theorem bpow_1 :
  bpow 1 = IZR r.

Theorem bpow_plus_1 :
  ∀ e : Z, (bpow (e + 1) = IZR r × bpow e)%R.

Theorem bpow_opp :
  ∀ e : Z, (bpow (-e) = /bpow e)%R.

Theorem IZR_Zpower_nat :
  ∀ e : nat,
  IZR (Zpower_nat r e) = bpow (Z_of_nat e).

Theorem IZR_Zpower :
  ∀ e : Z,
  (0 ≤ e)%Z →
  IZR (Zpower r e) = bpow e.

Theorem bpow_lt :
  ∀ e1 e2 : Z,
  (e1 < e2)%Z → (bpow e1 < bpow e2)%R.

Theorem lt_bpow :
  ∀ e1 e2 : Z,
  (bpow e1 < bpow e2)%R → (e1 < e2)%Z.

Theorem bpow_le :
  ∀ e1 e2 : Z,
  (e1 ≤ e2)%Z → (bpow e1 ≤ bpow e2)%R.

Theorem le_bpow :
  ∀ e1 e2 : Z,
  (bpow e1 ≤ bpow e2)%R → (e1 ≤ e2)%Z.

Theorem bpow_inj :
  ∀ e1 e2 : Z,
  bpow e1 = bpow e2 → e1 = e2.

Theorem bpow_exp :
  ∀ e : Z,
  bpow e = exp (IZR e × ln (IZR r)).

Lemma sqrt_bpow :
  ∀ e,
  sqrt (bpow (2 × e)) = bpow e.

Lemma sqrt_bpow_ge :
  ∀ e,
  (bpow (e / 2) ≤ sqrt (bpow e))%R.

Record mag_prop x := {
  mag_val :> Z ;
  _ : (x ≠ 0)%R → (bpow (mag_val - 1)%Z ≤ Rabs x < bpow mag_val)%R
}.

Definition mag :
  ∀ x : R, mag_prop x.

Theorem bpow_lt_bpow :
  ∀ e1 e2,
  (bpow (e1 - 1) < bpow e2)%R →
  (e1 ≤ e2)%Z.

Theorem bpow_unique :
  ∀ x e1 e2,
  (bpow (e1 - 1) ≤ x < bpow e1)%R →
  (bpow (e2 - 1) ≤ x < bpow e2)%R →
  e1 = e2.

Theorem mag_unique :
  ∀ (x : R) (e : Z),
  (bpow (e - 1) ≤ Rabs x < bpow e)%R →
  mag x = e :> Z.

Theorem mag_opp :
  ∀ x,
  mag (-x) = mag x :> Z.

Theorem mag_abs :
  ∀ x,
  mag (Rabs x) = mag x :> Z.

Theorem mag_unique_pos :
  ∀ (x : R) (e : Z),
  (bpow (e - 1) ≤ x < bpow e)%R →
  mag x = e :> Z.

Theorem mag_le_abs :
  ∀ x y,
  (x ≠ 0)%R → (Rabs x ≤ Rabs y)%R →
  (mag x ≤ mag y)%Z.

Theorem mag_le :
  ∀ x y,
  (0 < x)%R → (x ≤ y)%R →
  (mag x ≤ mag y)%Z.

Lemma lt_mag :
  ∀ x y,
  (0 < y)%R →
  (mag x < mag y)%Z → (x < y)%R.

Theorem mag_bpow :
  ∀ e, (mag (bpow e) = e + 1 :> Z)%Z.

Theorem mag_mult_bpow :
  ∀ x e, x ≠ 0%R →
  (mag (x × bpow e) = mag x + e :>Z)%Z.

Theorem mag_le_bpow :
  ∀ x e,
  x ≠ 0%R →
  (Rabs x < bpow e)%R →
  (mag x ≤ e)%Z.

Theorem mag_gt_bpow :
  ∀ x e,
  (bpow e ≤ Rabs x)%R →
  (e < mag x)%Z.

Theorem mag_ge_bpow :
  ∀ x e,
  (bpow (e - 1) ≤ Rabs x)%R →
  (e ≤ mag x)%Z.

Theorem bpow_mag_gt :
  ∀ x,
  (Rabs x < bpow (mag x))%R.

Theorem bpow_mag_le :
  ∀ x, (x ≠ 0)%R →
    (bpow (mag x-1) ≤ Rabs x)%R.

Theorem mag_le_Zpower :
  ∀ m e,
  m ≠ Z0 →
  (Z.abs m < Zpower r e)%Z→
  (mag (IZR m) ≤ e)%Z.

Theorem mag_gt_Zpower :
  ∀ m e,
  m ≠ Z0 →
  (Zpower r e ≤ Z.abs m)%Z →
  (e < mag (IZR m))%Z.

Lemma mag_mult :
  ∀ x y,
  (x ≠ 0)%R → (y ≠ 0)%R →
  (mag x + mag y - 1 ≤ mag (x × y) ≤ mag x + mag y)%Z.

Lemma mag_plus :
  ∀ x y,
  (0 < y)%R → (y ≤ x)%R →
  (mag x ≤ mag (x + y) ≤ mag x + 1)%Z.

Lemma mag_minus :
  ∀ x y,
  (0 < y)%R → (y < x)%R →
  (mag (x - y) ≤ mag x)%Z.

Lemma mag_minus_lb :
  ∀ x y,
  (0 < x)%R → (0 < y)%R →
  (mag y ≤ mag x - 2)%Z →
  (mag x - 1 ≤ mag (x - y))%Z.

Theorem mag_plus_ge :
  ∀ x y,
  (x ≠ 0)%R →
  (mag y ≤ mag x - 2)%Z →
  (mag x - 1 ≤ mag (x + y))%Z.

Lemma mag_div :
  ∀ x y : R,
  x ≠ 0%R → y ≠ 0%R →
  (mag x - mag y ≤ mag (x / y) ≤ mag x - mag y + 1)%Z.

Lemma mag_sqrt :
  ∀ x,
  (0 < x)%R →
  mag (sqrt x) = Z.div2 (mag x + 1) :> Z.

Lemma mag_1 : mag 1 = 1%Z :> Z.

End pow.

Section Bool.

Theorem eqb_sym :
  ∀ x y, Bool.eqb x y = Bool.eqb y x.

Theorem eqb_false :
  ∀ x y, x = negb y → Bool.eqb x y = false.

Theorem eqb_true :
  ∀ x y, x = y → Bool.eqb x y = true.

End Bool.

Section cond_Ropp.

Definition cond_Ropp (b : bool) m := if b then Ropp m else m.

Theorem IZR_cond_Zopp :
  ∀ b m,
  IZR (cond_Zopp b m) = cond_Ropp b (IZR m).

Theorem abs_cond_Ropp :
  ∀ b m,
  Rabs (cond_Ropp b m) = Rabs m.

Theorem cond_Ropp_Rlt_bool :
  ∀ m,
  cond_Ropp (Rlt_bool m 0) m = Rabs m.

Theorem Rlt_bool_cond_Ropp :
  ∀ x sx, (0 < x)%R →
  Rlt_bool (cond_Ropp sx x) 0 = sx.

Theorem cond_Ropp_involutive :
  ∀ b x,
  cond_Ropp b (cond_Ropp b x) = x.

Theorem cond_Ropp_inj :
  ∀ b x y,
  cond_Ropp b x = cond_Ropp b y → x = y.

Theorem cond_Ropp_mult_l :
  ∀ b x y,
  cond_Ropp b (x × y) = (cond_Ropp b x × y)%R.

Theorem cond_Ropp_mult_r :
  ∀ b x y,
  cond_Ropp b (x × y) = (x × cond_Ropp b y)%R.

Theorem cond_Ropp_plus :
  ∀ b x y,
  cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R.

End cond_Ropp.

Theorem LPO_min :
  ∀ P : nat → Prop, (∀ n, P n ∨ ¬ P n) →
  {n : nat | P n ∧ ∀ i, (i < n)%nat → ¬ P i} + {∀ n, ¬ P n}.

Theorem LPO :
  ∀ P : nat → Prop, (∀ n, P n ∨ ¬ P n) →
  {n : nat | P n} + {∀ n, ¬ P n}.

Lemma LPO_Z : ∀ P : Z → Prop, (∀ n, P n ∨ ¬P n) →
  {n : Z| P n} + {∀ n, ¬ P n}.

Ltac bpow_simplify :=
  
  repeat
    match goal with
      | |- context [(bpow _ _ × bpow _ _)] ⇒
        rewrite <- bpow_plus
      | |- context [(?X1 × bpow _ _ × bpow _ _)] ⇒
        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
      | |- context [(?X1 × (?X2 × bpow _ _) × bpow _ _)] ⇒
        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
        rewrite <- bpow_plus
    end;
  
  repeat
    match goal with
      | |- context [(bpow _ ?X)] ⇒
        progress ring_simplify X
    end;
  
  change (bpow _ 0) with 1;
  repeat
    match goal with
      | |- context [(_ × 1)] ⇒
        rewrite Rmult_1_r
    end.