Library Flocq.Pff.Pff



Require Export Reals.
Require Export ZArith.
Require Export List.
Require Export Div2.
Require Export Even.
Require Import Psatz.






Ltac CaseEq name :=
  generalize (refl_equal name); pattern name at -1 in |- *; case name.

Ltac Casec name := case name; clear name.

Ltac Elimc name := elim name; clear name.


Theorem lt_next : n m : nat, n < m m = S n S n < m.

Theorem le_next : n m : nat, n m m = n S n m.

Theorem min_or :
  n m : nat, min n m = n n m min n m = m m < n.

Theorem minus_inv_lt_aux : n m : nat, n - m = 0 n - S m = 0.

Theorem minus_inv_lt : n m : nat, m n m - n = 0.

Theorem minus_le : m n p q : nat, m n p q m - q n - p.


Theorem convert_not_O : p : positive, nat_of_P p 0.

Theorem inj_abs :
  x : Z, (0 x)%Z Z_of_nat (Zabs_nat x) = x.

Theorem inject_nat_convert :
  (p : Z) (q : positive),
 p = Zpos q Z_of_nat (nat_of_P q) = p.

Theorem ZleLe : x y : nat, (Z_of_nat x Z_of_nat y)%Z x y.

Theorem Zcompare_EGAL :
  p q : Z, (p ?= q)%Z = Datatypes.Eq p = q.

Theorem Zlt_Zopp : x y : Z, (x < y)%Z (- y < - x)%Z.

Theorem Zle_Zopp : x y : Z, (x y)%Z (- y - x)%Z.

Theorem absolu_INR : n : nat, Zabs_nat (Z_of_nat n) = n.

Theorem Zabs_absolu : z : Z, Zabs z = Z_of_nat (Zabs_nat z).

Theorem Zmin_sym : m n : Z, Zmin n m = Zmin m n.

Theorem Zpower_nat_O : z : Z, Zpower_nat z 0 = Z_of_nat 1.

Theorem Zpower_nat_1 : z : Z, Zpower_nat z 1 = z.

Theorem Zmin_le1 : z1 z2 : Z, (z1 z2)%Z Zmin z1 z2 = z1.

Theorem Zmin_le2 : z1 z2 : Z, (z2 z1)%Z Zmin z1 z2 = z2.

Theorem Zmin_Zle :
  z1 z2 z3 : Z,
 (z1 z2)%Z (z1 z3)%Z (z1 Zmin z2 z3)%Z.

Theorem Zminus_n_predm :
  n m : Z, Zsucc (n - m) = (n - Zpred m)%Z.

Theorem Zopp_Zpred_Zs : z : Z, (- Zpred z)%Z = Zsucc (- z).

Theorem Zle_mult_gen :
  x y : Z, (0 x)%Z (0 y)%Z (0 x × y)%Z.

Definition Zmax : x_ x_ : Z, Z :=
  fun n m : Z
  match (n ?= m)%Z with
  | Datatypes.Eqm
  | Datatypes.Ltm
  | Datatypes.Gtn
  end.

Theorem ZmaxLe1 : z1 z2 : Z, (z1 Zmax z1 z2)%Z.

Theorem ZmaxSym : z1 z2 : Z, Zmax z1 z2 = Zmax z2 z1.

Theorem ZmaxLe2 : z1 z2 : Z, (z2 Zmax z1 z2)%Z.

Theorem Zeq_Zs :
  p q : Z, (p q)%Z (q < Zsucc p)%Z p = q.

Theorem Zmin_Zmax : z1 z2 : Z, (Zmin z1 z2 Zmax z1 z2)%Z.

Theorem Zabs_Zmult :
  z1 z2 : Z, Zabs (z1 × z2) = (Zabs z1 × Zabs z2)%Z.

Theorem Zle_Zmult_comp_r :
  x y z : Z, (0 z)%Z (x y)%Z (x × z y × z)%Z.

Theorem Zle_Zmult_comp_l :
  x y z : Z, (0 z)%Z (x y)%Z (z × x z × y)%Z.


Theorem Rlt_IZR : p q : Z, (p < q)%Z (IZR p < IZR q)%R.

Theorem Rle_IZR : x y : Z, (x y)%Z (IZR x IZR y)%R.

Theorem lt_Rlt : n m : nat, (INR n < INR m)%R n < m.

Theorem INR_inv : n m : nat, INR n = INR m n = m.

Theorem Rle_INR : x y : nat, x y (INR x INR y)%R.

Theorem le_Rle : n m : nat, (INR n INR m)%R n m.

Theorem absolu_Zs :
  z : Z, (0 z)%Z Zabs_nat (Zsucc z) = S (Zabs_nat z).

Theorem Zlt_next :
  n m : Z, (n < m)%Z m = Zsucc n (Zsucc n < m)%Z.

Theorem Zle_next :
  n m : Z, (n m)%Z m = n (Zsucc n m)%Z.

Theorem inj_pred :
  n : nat, n 0 Z_of_nat (pred n) = Zpred (Z_of_nat n).

Theorem Zle_abs : p : Z, (p Z_of_nat (Zabs_nat p))%Z.

Theorem lt_Zlt_inv : n m : nat, (Z_of_nat n < Z_of_nat m)%Z n < m.

Theorem NconvertO : p : positive, nat_of_P p 0.

Theorem absolu_lt_nz : z : Z, z 0%Z 0 < Zabs_nat z.

Theorem Rledouble : r : R, (0 r)%R (r INR 2 × r)%R.

Theorem Rltdouble : r : R, (0 < r)%R (r < INR 2 × r)%R.

Theorem Rle_Rinv : x y : R, (0 < x)%R (x y)%R (/ y / x)%R.

Theorem Zlt_Rlt : z1 z2 : Z, (IZR z1 < IZR z2)%R (z1 < z2)%Z.

Theorem Zle_Rle :
  z1 z2 : Z, (IZR z1 IZR z2)%R (z1 z2)%Z.

Theorem Zabs_eq_opp : x, (x 0)%Z Zabs x = (- x)%Z.

Theorem Zabs_Zs : z : Z, (Zabs (Zsucc z) Zsucc (Zabs z))%Z.

Theorem Zle_Zpred : x y : Z, (x < y)%Z (x Zpred y)%Z.

Theorem Zabs_Zopp : z : Z, Zabs (- z) = Zabs z.

Theorem Zle_Zabs : z : Z, (z Zabs z)%Z.

Theorem Zlt_mult_simpl_l :
  a b c : Z, (0 < c)%Z (c × a < c × b)%Z (a < b)%Z.

Fixpoint pos_eq_bool (a b : positive) {struct b} : bool :=
  match a, b with
  | xH, xHtrue
  | xI a', xI b'pos_eq_bool a' b'
  | xO a', xO b'pos_eq_bool a' b'
  | _, _false
  end.

Theorem pos_eq_bool_correct :
  p q : positive,
 match pos_eq_bool p q with
 | truep = q
 | falsep q
 end.

Definition Z_eq_bool a b :=
  match a, b with
  | Z0, Z0true
  | Zpos a', Zpos b'pos_eq_bool a' b'
  | Zneg a', Zneg b'pos_eq_bool a' b'
  | _, _false
  end.

Theorem Z_eq_bool_correct :
  p q : Z,
 match Z_eq_bool p q with
 | truep = q
 | falsep q
 end.

Theorem Zlt_mult_ZERO :
  x y : Z, (0 < x)%Z (0 < y)%Z (0 < x × y)%Z.

Theorem Zle_Zminus_ZERO :
  z1 z2 : Z, (z2 z1)%Z (0 z1 - z2)%Z.

Theorem Zle_Zpred_Zpred :
  z1 z2 : Z, (z1 z2)%Z (Zpred z1 Zpred z2)%Z.

Theorem Zle_ZERO_Zabs : z : Z, (0 Zabs z)%Z.

Theorem Zlt_Zabs_inv1 :
  z1 z2 : Z, (Zabs z1 < z2)%Z (- z2 < z1)%Z.

Theorem Zlt_Zabs_inv2 :
  z1 z2 : Z, (Zabs z1 < Zabs z2)%Z (z1 < Zabs z2)%Z.

Theorem Zle_Zabs_inv1 :
  z1 z2 : Z, (Zabs z1 z2)%Z (- z2 z1)%Z.

Theorem Zle_Zabs_inv2 :
  z1 z2 : Z, (Zabs z1 z2)%Z (z1 z2)%Z.

Theorem Zlt_Zabs_Zpred :
  z1 z2 : Z,
 (Zabs z1 < z2)%Z z1 Zpred z2 (Zabs (Zsucc z1) < z2)%Z.

Theorem Zle_n_Zpred :
  z1 z2 : Z, (Zpred z1 Zpred z2)%Z (z1 z2)%Z.

Theorem Zpred_Zopp_Zs : z : Z, Zpred (- z) = (- Zsucc z)%Z.

Theorem Zlt_1_O : z : Z, (1 z)%Z (0 < z)%Z.

Theorem Zlt_not_eq : p q : Z, (p < q)%Z p q.

Theorem Zlt_not_eq_rev : p q : Z, (q < p)%Z p q.

Theorem Zle_Zpred_inv :
  z1 z2 : Z, (z1 Zpred z2)%Z (z1 < z2)%Z.

Theorem Zabs_intro :
  (P : Z Prop) (z : Z), P (- z)%Z P z P (Zabs z).

Theorem Zpred_Zle_Zabs_intro :
  z1 z2 : Z,
 (- Zpred z2 z1)%Z (z1 Zpred z2)%Z (Zabs z1 < z2)%Z.

Theorem Zlt_ZERO_Zle_ONE : z : Z, (0 < z)%Z (1 z)%Z.

Theorem Zlt_Zabs_intro :
  z1 z2 : Z, (- z2 < z1)%Z (z1 < z2)%Z (Zabs z1 < z2)%Z.

Section Pdigit.
Variable n : Z.
Hypothesis nMoreThan1 : (1 < n)%Z.

Let nMoreThanOne := Zlt_1_O _ (Zlt_le_weak _ _ nMoreThan1).

Theorem Zpower_nat_less : q : nat, (0 < Zpower_nat n q)%Z.

Theorem Zpower_nat_monotone_S :
  p : nat, (Zpower_nat n p < Zpower_nat n (S p))%Z.

Theorem Zpower_nat_monotone_lt :
  p q : nat, p < q (Zpower_nat n p < Zpower_nat n q)%Z.

Theorem Zpower_nat_anti_monotone_lt :
  p q : nat, (Zpower_nat n p < Zpower_nat n q)%Z p < q.

Theorem Zpower_nat_monotone_le :
  p q : nat, p q (Zpower_nat n p Zpower_nat n q)%Z.


Fixpoint digitAux (v r : Z) (q : positive) {struct q} : nat :=
  match q with
  | xH ⇒ 0
  | xI q'
      match (n × r)%Z with
      | r'
          match (r ?= v)%Z with
          | Datatypes.Gt ⇒ 0
          | _S (digitAux v r' q')
          end
      end
  | xO q'
      match (n × r)%Z with
      | r'
          match (r ?= v)%Z with
          | Datatypes.Gt ⇒ 0
          | _S (digitAux v r' q')
          end
      end
  end.

Definition digit (q : Z) :=
  match q with
  | Z0 ⇒ 0
  | Zpos q'digitAux (Zabs q) 1 (xO q')
  | Zneg q'digitAux (Zabs q) 1 (xO q')
  end.

Theorem digitAux1 :
  p r, (Zpower_nat n (S p) × r)%Z = (Zpower_nat n p × (n × r))%Z.

Theorem Zcompare_correct :
  p q : Z,
 match (p ?= q)%Z with
 | Datatypes.Gt ⇒ (q < p)%Z
 | Datatypes.Lt ⇒ (p < q)%Z
 | Datatypes.Eqp = q
 end.

Theorem digitAuxLess :
  (v r : Z) (q : positive),
 match digitAux v r q with
 | S r' ⇒ (Zpower_nat n r' × r v)%Z
 | OTrue
 end.

Theorem digitLess :
  q : Z, q 0%Z (Zpower_nat n (pred (digit q)) Zabs q)%Z.

Fixpoint pos_length (p : positive) : nat :=
  match p with
  | xH ⇒ 0
  | xO p'S (pos_length p')
  | xI p'S (pos_length p')
  end.

Theorem digitAuxMore :
  (v r : Z) (q : positive),
 (0 < r)%Z
 (v < Zpower_nat n (pos_length q) × r)%Z
 (v < Zpower_nat n (digitAux v r q) × r)%Z.

Theorem pos_length_pow :
  p : positive, (Zpos p < Zpower_nat n (S (pos_length p)))%Z.

Theorem digitMore : q : Z, (Zabs q < Zpower_nat n (digit q))%Z.


Theorem digitInv :
  (q : Z) (r : nat),
 (Zpower_nat n (pred r) Zabs q)%Z
 (Zabs q < Zpower_nat n r)%Z digit q = r.


Theorem digit_monotone :
  p q : Z, (Zabs p Zabs q)%Z digit p digit q.


Theorem digitNotZero : q : Z, q 0%Z 0 < digit q.

Theorem digitAdd :
  (q : Z) (r : nat),
 q 0%Z digit (q × Zpower_nat n r) = digit q + r.

Theorem digit_abs : p : Z, digit (Zabs p) = digit p.

Theorem digit_anti_monotone_lt :
 (1 < n)%Z p q : Z, digit p < digit q (Zabs p < Zabs q)%Z.
End Pdigit.



Theorem pow_NR0 : (e : R) (n : nat), e 0%R (e ^ n)%R 0%R.

Theorem pow_add :
  (e : R) (n m : nat), (e ^ (n + m))%R = (e ^ n × e ^ m)%R.

Theorem pow_RN_plus :
  (e : R) (n m : nat),
 e 0%R (e ^ n)%R = (e ^ (n + m) × / e ^ m)%R.

Theorem pow_lt : (e : R) (n : nat), (0 < e)%R (0 < e ^ n)%R.

Theorem Rlt_pow_R1 :
  (e : R) (n : nat), (1 < e)%R 0 < n (1 < e ^ n)%R.

Theorem Rlt_pow :
  (e : R) (n m : nat), (1 < e)%R n < m (e ^ n < e ^ m)%R.

Theorem pow_R1 :
  (r : R) (n : nat), (r ^ n)%R = 1%R Rabs r = 1%R n = 0.

Theorem Zpower_NR0 :
  (e : Z) (n : nat), (0 e)%Z (0 Zpower_nat e n)%Z.

Theorem Zpower_NR1 :
  (e : Z) (n : nat), (1 e)%Z (1 Zpower_nat e n)%Z.



Theorem powerRZ_O : e : R, powerRZ e 0 = 1%R.

Theorem powerRZ_1 : e : R, powerRZ e (Zsucc 0) = e.

Theorem powerRZ_NOR : (e : R) (z : Z), e 0%R powerRZ e z 0%R.

Theorem powerRZ_add :
  (e : R) (n m : Z),
 e 0%R powerRZ e (n + m) = (powerRZ e n × powerRZ e m)%R.

Theorem powerRZ_Zopp :
  (e : R) (z : Z), e 0%R powerRZ e (- z) = (/ powerRZ e z)%R.

Theorem powerRZ_Zs :
  (e : R) (n : Z),
 e 0%R powerRZ e (Zsucc n) = (e × powerRZ e n)%R.

Theorem Zpower_nat_Z_powerRZ :
  (n : Z) (m : nat),
 IZR (Zpower_nat n m) = powerRZ (IZR n) (Z_of_nat m).

Theorem powerRZ_lt : (e : R) (z : Z), (0 < e)%R (0 < powerRZ e z)%R.

Theorem powerRZ_le :
  (e : R) (z : Z), (0 < e)%R (0 powerRZ e z)%R.

Theorem Rlt_powerRZ :
  (e : R) (n m : Z),
 (1 < e)%R (n < m)%Z (powerRZ e n < powerRZ e m)%R.

Theorem Zpower_nat_powerRZ_absolu :
  n m : Z,
 (0 m)%Z IZR (Zpower_nat n (Zabs_nat m)) = powerRZ (IZR n) m.

Theorem powerRZ_R1 : n : Z, powerRZ 1 n = 1%R.

Theorem Rle_powerRZ :
  (e : R) (n m : Z),
 (1 e)%R (n m)%Z (powerRZ e n powerRZ e m)%R.

Theorem Zlt_powerRZ :
  (e : R) (n m : Z),
 (1 e)%R (powerRZ e n < powerRZ e m)%R (n < m)%Z.

Theorem Zle_powerRZ :
  (e : R) (n m : Z),
 (1 < e)%R (powerRZ e n powerRZ e m)%R (n m)%Z.

Theorem Rinv_powerRZ :
  (e : R) (n : Z), e 0%R (/ powerRZ e n)%R = powerRZ e (- n).

Section definitions.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).


Record float : Set := Float {Fnum : Z; Fexp : Z}.

Theorem floatEq :
  p q : float, Fnum p = Fnum q Fexp p = Fexp q p = q.

Theorem floatDec : x y : float, {x = y} + {x y}.

Definition Fzero (x : Z) := Float 0 x.

Definition is_Fzero (x : float) := Fnum x = 0%Z.

Coercion IZR : Z >-> R.
Coercion INR : nat >-> R.
Coercion Z_of_nat : nat >-> Z.

Definition FtoR (x : float) := (Fnum x × powerRZ (IZR radix) (Fexp x))%R.


Theorem FzeroisReallyZero : z : Z, Fzero z = 0%R :>R.

Theorem is_Fzero_rep1 : x : float, is_Fzero x x = 0%R :>R.

Theorem LtFnumZERO : x : float, (0 < Fnum x)%Z (0 < x)%R.

Theorem is_Fzero_rep2 : x : float, x = 0%R :>R is_Fzero x.

Theorem NisFzeroComp :
  x y : float, ¬ is_Fzero x x = y :>R ¬ is_Fzero y.

Theorem Rlt_monotony_exp :
  (x y : R) (z : Z),
 (x < y)%R (x × powerRZ radix z < y × powerRZ radix z)%R.

Theorem Rle_monotone_exp :
  (x y : R) (z : Z),
 (x y)%R (x × powerRZ radix z y × powerRZ radix z)%R.

Theorem Rlt_monotony_contra_exp :
  (x y : R) (z : Z),
 (x × powerRZ radix z < y × powerRZ radix z)%R (x < y)%R.

Theorem Rle_monotony_contra_exp :
  (x y : R) (z : Z),
 (x × powerRZ radix z y × powerRZ radix z)%R (x y)%R.

Theorem FtoREqInv2 :
  p q : float, p = q :>R Fexp p = Fexp q p = q.

Theorem Rlt_Float_Zlt :
  p q r : Z, (Float p r < Float q r)%R (p < q)%Z.


Theorem oneExp_le :
  x y : Z, (x y)%Z (Float 1%nat x Float 1%nat y)%R.

Theorem oneExp_Zlt :
  x y : Z, (Float 1%nat x < Float 1%nat y)%R (x < y)%Z.

Definition Fdigit (p : float) := digit radix (Fnum p).

Definition Fshift (n : nat) (x : float) :=
  Float (Fnum x × Zpower_nat radix n) (Fexp x - n).

Theorem sameExpEq : p q : float, p = q :>R Fexp p = Fexp q p = q.

Theorem FshiftFdigit :
  (n : nat) (x : float),
 ¬ is_Fzero x Fdigit (Fshift n x) = Fdigit x + n.

Theorem FshiftCorrect : (n : nat) (x : float), Fshift n x = x :>R.

Theorem FshiftCorrectInv :
  x y : float,
 x = y :>R
 (Fexp x Fexp y)%Z Fshift (Zabs_nat (Fexp y - Fexp x)) y = x.

Theorem FshiftO : x : float, Fshift 0 x = x.

Theorem FshiftCorrectSym :
  x y : float,
 x = y :>R n : nat, ( m : nat, Fshift n x = Fshift m y).

Theorem FdigitEq :
  x y : float,
 ¬ is_Fzero x x = y :>R Fdigit x = Fdigit y x = y.
End definitions.


Section comparisons.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Let FtoRradix := FtoR radix.


Definition Fle (x y : float) := (x y)%R.

Lemma Fle_Zle :
  n1 n2 d : Z, (n1 n2)%Z Fle (Float n1 d) (Float n2 d).


Theorem Rlt_Fexp_eq_Zlt :
  x y : float, (x < y)%R Fexp x = Fexp y (Fnum x < Fnum y)%Z.

Theorem Rle_Fexp_eq_Zle :
  x y : float, (x y)%R Fexp x = Fexp y (Fnum x Fnum y)%Z.

Theorem LtR0Fnum : p : float, (0 < p)%R (0 < Fnum p)%Z.

Theorem LeR0Fnum : p : float, (0 p)%R (0 Fnum p)%Z.

Theorem LeFnumZERO : x : float, (0 Fnum x)%Z (0 x)%R.

Theorem R0LtFnum : p : float, (p < 0)%R (Fnum p < 0)%Z.

Theorem R0LeFnum : p : float, (p 0)%R (Fnum p 0)%Z.

Theorem LeZEROFnum : x : float, (Fnum x 0)%Z (x 0)%R.
End comparisons.


Section operations.
Variable radix : Z.

Let FtoRradix := FtoR radix.

Hypothesis radixNotZero : (0 < radix)%Z.

Definition Fplus (x y : float) :=
  Float
    (Fnum x × Zpower_nat radix (Zabs_nat (Fexp x - Zmin (Fexp x) (Fexp y))) +
     Fnum y × Zpower_nat radix (Zabs_nat (Fexp y - Zmin (Fexp x) (Fexp y))))
    (Zmin (Fexp x) (Fexp y)).

Theorem Fplus_correct : x y : float, Fplus x y = (x + y)%R :>R.

Definition Fopp (x : float) := Float (- Fnum x) (Fexp x).

Theorem Fopp_correct : x : float, Fopp x = (- x)%R :>R.

Theorem Fopp_Fopp : p : float, Fopp (Fopp p) = p.

Theorem Fdigit_opp : x : float, Fdigit radix (Fopp x) = Fdigit radix x.

Definition Fabs (x : float) := Float (Zabs (Fnum x)) (Fexp x).

Theorem Fabs_correct1 :
  x : float, (0 FtoR radix x)%R Fabs x = x :>R.

Theorem Fabs_correct2 :
  x : float, (FtoR radix x 0)%R Fabs x = (- x)%R :>R.

Theorem Fabs_correct : x : float, Fabs x = Rabs x :>R.

Theorem RleFexpFabs :
  p : float, p 0%R :>R (Float 1%nat (Fexp p) Fabs p)%R.

Theorem Fabs_Fzero : x : float, ¬ is_Fzero x ¬ is_Fzero (Fabs x).

Theorem Fdigit_abs : x : float, Fdigit radix (Fabs x) = Fdigit radix x.

Definition Fminus (x y : float) := Fplus x (Fopp y).

Theorem Fminus_correct : x y : float, Fminus x y = (x - y)%R :>R.

Theorem Fopp_Fminus : p q : float, Fopp (Fminus p q) = Fminus q p.

Theorem Fopp_Fminus_dist :
  p q : float, Fopp (Fminus p q) = Fminus (Fopp p) (Fopp q).

Definition Fmult (x y : float) := Float (Fnum x × Fnum y) (Fexp x + Fexp y).

Definition Fmult_correct : x y : float, Fmult x y = (x × y)%R :>R.
Qed.

End operations.


Section Fbounded_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Let FtoRradix := FtoR radix.

Coercion Z_of_N: N >-> Z.

Record Fbound : Set := Bound {vNum : positive; dExp : N}.

Definition Fbounded (b : Fbound) (d : float) :=
  (Zabs (Fnum d) < Zpos (vNum b))%Z (- dExp b Fexp d)%Z.

Theorem FzeroisZero : b : Fbound, Fzero (- dExp b) = 0%R :>R.

Theorem FboundedFzero : b : Fbound, Fbounded b (Fzero (- dExp b)).

Theorem FboundedZeroSameExp :
  (b : Fbound) (p : float), Fbounded b p Fbounded b (Fzero (Fexp p)).

Theorem FBoundedScale :
  (b : Fbound) (p : float) (n : nat),
 Fbounded b p Fbounded b (Float (Fnum p) (Fexp p + n)).

Theorem FvalScale :
  (b : Fbound) (p : float) (n : nat),
 Float (Fnum p) (Fexp p + n) = (powerRZ radix n × p)%R :>R.

Theorem oppBounded :
  (b : Fbound) (x : float), Fbounded b x Fbounded b (Fopp x).

Theorem oppBoundedInv :
  (b : Fbound) (x : float), Fbounded b (Fopp x) Fbounded b x.

Theorem absFBounded :
  (b : Fbound) (f : float), Fbounded b f Fbounded b (Fabs f).

Theorem FboundedEqExp :
  (b : Fbound) (p q : float),
 Fbounded b p p = q :>R (Fexp p Fexp q)%R Fbounded b q.

Theorem eqExpLess :
  (b : Fbound) (p q : float),
 Fbounded b p
 p = q :>R
  r : float, Fbounded b r r = q :>R (Fexp q Fexp r)%R.

Theorem FboundedShiftLess :
  (b : Fbound) (f : float) (n m : nat),
 m n Fbounded b (Fshift radix n f) Fbounded b (Fshift radix m f).

Theorem eqExpMax :
  (b : Fbound) (p q : float),
 Fbounded b p
 Fbounded b q
 (Fabs p q)%R
  r : float, Fbounded b r r = p :>R (Fexp r Fexp q)%Z.

Theorem maxFbounded :
  (b : Fbound) (z : Z),
 (- dExp b z)%Z Fbounded b (Float (Zpred (Zpos (vNum b))) z).

Theorem maxMax :
  (b : Fbound) (p : float) (z : Z),
 Fbounded b p
 (Fexp p z)%Z (Fabs p < Float (Zpos (vNum b)) z)%R.
End Fbounded_Def.


Section Fprop.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let FtoRradix := FtoR radix.

Variable b : Fbound.

Theorem SterbenzAux :
  x y : float,
 Fbounded b x
 Fbounded b y
 (y x)%R (x 2%nat × y)%R Fbounded b (Fminus radix x y).

Theorem Sterbenz :
  x y : float,
 Fbounded b x
 Fbounded b y
 (/ 2%nat × y x)%R (x 2%nat × y)%R Fbounded b (Fminus radix x y).

End Fprop.


Fixpoint mZlist_aux (p : Z) (n : nat) {struct n} :
 list Z :=
  match n with
  | Op :: nil
  | S n1p :: mZlist_aux (Zsucc p) n1
  end.

Theorem mZlist_aux_correct :
  (n : nat) (p q : Z),
 (p q)%Z (q p + Z_of_nat n)%Z In q (mZlist_aux p n).

Theorem mZlist_aux_correct_rev1 :
  (n : nat) (p q : Z), In q (mZlist_aux p n) (p q)%Z.

Theorem mZlist_aux_correct_rev2 :
  (n : nat) (p q : Z),
 In q (mZlist_aux p n) (q p + Z_of_nat n)%Z.

Definition mZlist (p q : Z) : list Z :=
  match (q - p)%Z with
  | Z0p :: nil
  | Zpos dmZlist_aux p (nat_of_P d)
  | Zneg _nil (A:=Z)
  end.

Theorem mZlist_correct :
  p q r : Z, (p r)%Z (r q)%Z In r (mZlist p q).

Theorem mZlist_correct_rev1 :
  p q r : Z, In r (mZlist p q) (p r)%Z.

Theorem mZlist_correct_rev2 :
  p q r : Z, In r (mZlist p q) (r q)%Z.

Fixpoint mProd (A B C : Set) (l1 : list A) (l2 : list B) {struct l2} :
 list (A × B) :=
  match l2 with
  | nilnil
  | b :: l2'map (fun a : A(a, b)) l1 ++ mProd A B C l1 l2'
  end.

Theorem mProd_correct :
  (A B C : Set) (l1 : list A) (l2 : list B) (a : A) (b : B),
 In a l1 In b l2 In (a, b) (mProd A B C l1 l2).

Theorem mProd_correct_rev1 :
  (A B C : Set) (l1 : list A) (l2 : list B) (a : A) (b : B),
 In (a, b) (mProd A B C l1 l2) In a l1.

Theorem mProd_correct_rev2 :
  (A B C : Set) (l1 : list A) (l2 : list B) (a : A) (b : B),
 In (a, b) (mProd A B C l1 l2) In b l2.

Theorem in_map_inv :
  (A B : Set) (f : A B) (l : list A) (x : A),
 ( a b : A, f a = f b a = b) In (f x) (map f l) In x l.

Section Fnormalized_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Let FtoRradix := FtoR radix.
Variable b : Fbound.

Definition Fnormal (p : float) :=
  Fbounded b p (Zpos (vNum b) Zabs (radix × Fnum p))%Z.

Theorem FnormalBounded : p : float, Fnormal p Fbounded b p.

Theorem FnormalNotZero : p : float, Fnormal p ¬ is_Fzero p.

Theorem FnormalFop : p : float, Fnormal p Fnormal (Fopp p).

Theorem FnormalFabs : p : float, Fnormal p Fnormal (Fabs p).

Definition pPred x := Zpred (Zpos x).

Theorem maxMax1 :
  (p : float) (z : Z),
 Fbounded b p (Fexp p z)%Z (Fabs p Float (pPred (vNum b)) z)%R.

Definition Fsubnormal (p : float) :=
  Fbounded b p
  Fexp p = (- dExp b)%Z (Zabs (radix × Fnum p) < Zpos (vNum b))%Z.

Theorem FsubnormalFbounded : p : float, Fsubnormal p Fbounded b p.

Theorem FsubnormalFexp :
  p : float, Fsubnormal p Fexp p = (- dExp b)%Z.

Theorem FsubnormFopp : p : float, Fsubnormal p Fsubnormal (Fopp p).

Theorem FsubnormFabs : p : float, Fsubnormal p Fsubnormal (Fabs p).

Theorem FsubnormalUnique :
  p q : float, Fsubnormal p Fsubnormal q p = q :>R p = q.

Theorem FsubnormalLt :
  p q : float,
 Fsubnormal p Fsubnormal q (p < q)%R (Fnum p < Fnum q)%Z.

Definition Fcanonic (a : float) := Fnormal a Fsubnormal a.

Theorem FcanonicBound : p : float, Fcanonic p Fbounded b p.

Theorem FcanonicFopp : p : float, Fcanonic p Fcanonic (Fopp p).

Theorem FcanonicFabs : p : float, Fcanonic p Fcanonic (Fabs p).

Theorem MaxFloat :
  x : float,
 Fbounded b x (Rabs x < Float (Zpos (vNum b)) (Fexp x))%R.
Variable precision : nat.
Hypothesis precisionNotZero : precision 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Theorem FboundNext :
  p : float,
 Fbounded b p
  q : float, Fbounded b q q = Float (Zsucc (Fnum p)) (Fexp p) :>R.

Theorem digitPredVNumiSPrecision :
 digit radix (Zpred (Zpos (vNum b))) = precision.

Theorem digitVNumiSPrecision :
 digit radix (Zpos (vNum b)) = S precision.

Theorem vNumPrecision :
  n : Z,
 digit radix n precision (Zabs n < Zpos (vNum b))%Z.

Theorem pGivesDigit :
  p : float, Fbounded b p Fdigit radix p precision.

Theorem digitGivesBoundedNum :
  p : float,
 Fdigit radix p precision (Zabs (Fnum p) < Zpos (vNum b))%Z.

Theorem FboundedMboundPos :
  z m : Z,
 (0 m)%Z
 (m Zpower_nat radix precision)%Z
 (- dExp b z)%Z
  c : float, Fbounded b c c = (m × powerRZ radix z)%R :>R.

Theorem FboundedMbound :
  z m : Z,
 (Zabs m Zpower_nat radix precision)%Z
 (- dExp b z)%Z
  c : float, Fbounded b c c = (m × powerRZ radix z)%R :>R.

Theorem FnormalPrecision :
  p : float, Fnormal p Fdigit radix p = precision.

Theorem FnormalUnique :
  p q : float, Fnormal p Fnormal q p = q :>R p = q.

Theorem FnormalLtPos :
  p q : float,
 Fnormal p
 Fnormal q
 (0 p)%R
 (p < q)%R (Fexp p < Fexp q)%Z Fexp p = Fexp q (Fnum p < Fnum q)%Z.

Definition nNormMin := Zpower_nat radix (pred precision).

Theorem nNormPos : (0 < nNormMin)%Z.

Theorem digitnNormMin : digit radix nNormMin = precision.

Theorem nNrMMimLevNum : (nNormMin Zpos (vNum b))%Z.

Definition firstNormalPos := Float nNormMin (- dExp b).

Theorem firstNormalPosNormal : Fnormal firstNormalPos.

Theorem pNormal_absolu_min :
  p : float, Fnormal p (nNormMin Zabs (Fnum p))%Z.

Theorem maxMaxBis :
  (p : float) (z : Z),
 Fbounded b p (Fexp p < z)%Z (Fabs p < Float nNormMin z)%R.

Theorem FnormalLtFirstNormalPos :
  p : float, Fnormal p (0 p)%R (firstNormalPos p)%R.

Theorem FsubnormalDigit :
  p : float, Fsubnormal p Fdigit radix p < precision.

Theorem pSubnormal_absolu_min :
  p : float, Fsubnormal p (Zabs (Fnum p) < nNormMin)%Z.

Theorem FsubnormalLtFirstNormalPos :
  p : float, Fsubnormal p (0 p)%R (p < firstNormalPos)%R.

Theorem FsubnormalnormalLtPos :
  p q : float,
 Fsubnormal p Fnormal q (0 p)%R (0 q)%R (p < q)%R.

Theorem FsubnormalnormalLtNeg :
  p q : float,
 Fsubnormal p Fnormal q (p 0)%R (q 0)%R (q < p)%R.

Definition Fnormalize (p : float) :=
  match Z_zerop (Fnum p) with
  | left _Float 0 (- dExp b)
  | right _
      Fshift radix
        (min (precision - Fdigit radix p) (Zabs_nat (dExp b + Fexp p))) p
  end.

Theorem FnormalizeCorrect : p : float, Fnormalize p = p :>R.

Theorem Fnormalize_Fopp :
  p : float, Fnormalize (Fopp p) = Fopp (Fnormalize p).

Theorem FnormalizeBounded :
  p : float, Fbounded b p Fbounded b (Fnormalize p).

Theorem FnormalizeCanonic :
  p : float, Fbounded b p Fcanonic (Fnormalize p).

Theorem NormalAndSubNormalNotEq :
  p q : float, Fnormal p Fsubnormal q p q :>R.

Theorem FcanonicUnique :
  p q : float, Fcanonic p Fcanonic q p = q :>R p = q.

Theorem FcanonicLeastExp :
  x y : float,
 x = y :>R Fbounded b x Fcanonic y (Fexp y Fexp x)%Z.

Theorem FcanonicLtPos :
  p q : float,
 Fcanonic p
 Fcanonic q
 (0 p)%R
 (p < q)%R (Fexp p < Fexp q)%Z Fexp p = Fexp q (Fnum p < Fnum q)%Z.

Theorem Fcanonic_Rle_Zle :
  x y : float,
 Fcanonic x Fcanonic y (Rabs x Rabs y)%R (Fexp x Fexp y)%Z.

Theorem FcanonicLtNeg :
  p q : float,
 Fcanonic p
 Fcanonic q
 (q 0)%R
 (p < q)%R (Fexp q < Fexp p)%Z Fexp p = Fexp q (Fnum p < Fnum q)%Z.

Theorem FcanonicFnormalizeEq :
  p : float, Fcanonic p Fnormalize p = p.

Theorem FcanonicPosFexpRlt :
  x y : float,
 (0 x)%R
 (0 y)%R Fcanonic x Fcanonic y (Fexp x < Fexp y)%Z (x < y)%R.

Theorem FcanonicNegFexpRlt :
  x y : float,
 (x 0)%R
 (y 0)%R Fcanonic x Fcanonic y (Fexp x < Fexp y)%Z (y < x)%R.

Theorem vNumbMoreThanOne : (1 < Zpos (vNum b))%Z.

Theorem PosNormMin : Zpos (vNum b) = (radix × nNormMin)%Z.

Theorem FnormalPpred :
  x : Z, (- dExp b x)%Z Fnormal (Float (pPred (vNum b)) x).

Theorem FcanonicPpred :
  x : Z,
 (- dExp b x)%Z Fcanonic (Float (pPred (vNum b)) x).

Theorem FnormalNnormMin :
  x : Z, (- dExp b x)%Z Fnormal (Float nNormMin x).

Theorem FcanonicNnormMin :
  x : Z, (- dExp b x)%Z Fcanonic (Float nNormMin x).

End Fnormalized_Def.
Section suc.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.

Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Hypothesis precisionNotZero : precision 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition FSucc (x : float) :=
  match Z_eq_bool (Fnum x) (pPred (vNum b)) with
  | trueFloat (nNormMin radix precision) (Zsucc (Fexp x))
  | false
      match Z_eq_bool (Fnum x) (- nNormMin radix precision) with
      | true
          match Z_eq_bool (Fexp x) (- dExp b) with
          | trueFloat (Zsucc (Fnum x)) (Fexp x)
          | falseFloat (- pPred (vNum b)) (Zpred (Fexp x))
          end
      | falseFloat (Zsucc (Fnum x)) (Fexp x)
      end
  end.

Theorem FSuccSimpl1 :
  x : float,
 Fnum x = pPred (vNum b)
 FSucc x = Float (nNormMin radix precision) (Zsucc (Fexp x)).

Theorem FSuccSimpl2 :
  x : float,
 Fnum x = (- nNormMin radix precision)%Z
 Fexp x (- dExp b)%Z
 FSucc x = Float (- pPred (vNum b)) (Zpred (Fexp x)).

Theorem FSuccSimpl3 :
 FSucc (Float (- nNormMin radix precision) (- dExp b)) =
 Float (Zsucc (- nNormMin radix precision)) (- dExp b).

Theorem FSuccSimpl4 :
  x : float,
 Fnum x pPred (vNum b)
 Fnum x (- nNormMin radix precision)%Z
 FSucc x = Float (Zsucc (Fnum x)) (Fexp x).

Theorem FSuccDiff1 :
  x : float,
 Fnum x (- nNormMin radix precision)%Z
 Fminus radix (FSucc x) x = Float 1%nat (Fexp x) :>R.

Theorem FSuccDiff2 :
  x : float,
 Fnum x = (- nNormMin radix precision)%Z
 Fexp x = (- dExp b)%Z Fminus radix (FSucc x) x = Float 1%nat (Fexp x) :>R.

Theorem FSuccDiff3 :
  x : float,
 Fnum x = (- nNormMin radix precision)%Z
 Fexp x (- dExp b)%Z
 Fminus radix (FSucc x) x = Float 1%nat (Zpred (Fexp x)) :>R.

Theorem ZltNormMinVnum : (nNormMin radix precision < Zpos (vNum b))%Z.

Theorem FSuccNormPos :
  a : float,
 (0 a)%R Fnormal radix b a Fnormal radix b (FSucc a).

Theorem FSuccSubnormNotNearNormMin :
  a : float,
 Fsubnormal radix b a
 Fnum a Zpred (nNormMin radix precision) Fsubnormal radix b (FSucc a).

Theorem FSuccSubnormNearNormMin :
  a : float,
 Fsubnormal radix b a
 Fnum a = Zpred (nNormMin radix precision) Fnormal radix b (FSucc a).

Theorem FBoundedSuc : f : float, Fbounded b f Fbounded b (FSucc f).

Theorem FSuccSubnormal :
  a : float, Fsubnormal radix b a Fcanonic radix b (FSucc a).

Theorem FSuccPosNotMax :
  a : float,
 (0 a)%R Fcanonic radix b a Fcanonic radix b (FSucc a).

Theorem FSuccNormNegNotNormMin :
  a : float,
 (a 0)%R
 Fnormal radix b a
 a Float (- nNormMin radix precision) (- dExp b)
 Fnormal radix b (FSucc a).

Theorem FSuccNormNegNormMin :
 Fsubnormal radix b (FSucc (Float (- nNormMin radix precision) (- dExp b))).

Theorem FSuccNegCanonic :
  a : float,
 (a 0)%R Fcanonic radix b a Fcanonic radix b (FSucc a).

Theorem FSuccCanonic :
  a : float, Fcanonic radix b a Fcanonic radix b (FSucc a).

Theorem FSuccLt : a : float, (a < FSucc a)%R.

Theorem FSuccPropPos :
  x y : float,
 (0 x)%R
 Fcanonic radix b x Fcanonic radix b y (x < y)%R (FSucc x y)%R.

Theorem R0RltRleSucc : x : float, (x < 0)%R (FSucc x 0)%R.

Theorem FSuccPropNeg :
  x y : float,
 (x < 0)%R
 Fcanonic radix b x Fcanonic radix b y (x < y)%R (FSucc x y)%R.

Theorem FSuccProp :
  x y : float,
 Fcanonic radix b x Fcanonic radix b y (x < y)%R (FSucc x y)%R.

Theorem FSuccZleEq :
  p q : float,
 (p q)%R (q < FSucc p)%R (Fexp p Fexp q)%Z p = q :>R.

Definition FNSucc x := FSucc (Fnormalize radix b precision x).

Theorem FNSuccCanonic :
  a : float, Fbounded b a Fcanonic radix b (FNSucc a).

Theorem FNSuccLt : a : float, (a < FNSucc a)%R.

Theorem FNSuccProp :
  x y : float,
 Fbounded b x Fbounded b y (x < y)%R (FNSucc x y)%R.

End suc.

Section suc1.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Theorem nNormMimLtvNum : (nNormMin radix precision < pPred (vNum b))%Z.

End suc1.

Section pred.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionNotZero : precision 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition FPred (x : float) :=
  match Z_eq_bool (Fnum x) (- pPred (vNum b)) with
  | trueFloat (- nNormMin radix precision) (Zsucc (Fexp x))
  | false
      match Z_eq_bool (Fnum x) (nNormMin radix precision) with
      | true
          match Z_eq_bool (Fexp x) (- dExp b) with
          | trueFloat (Zpred (Fnum x)) (Fexp x)
          | falseFloat (pPred (vNum b)) (Zpred (Fexp x))
          end
      | falseFloat (Zpred (Fnum x)) (Fexp x)
      end
  end.

Theorem FPredSimpl1 :
  x : float,
 Fnum x = (- pPred (vNum b))%Z
 FPred x = Float (- nNormMin radix precision) (Zsucc (Fexp x)).

Theorem FPredSimpl2 :
  x : float,
 Fnum x = nNormMin radix precision
 Fexp x (- dExp b)%Z FPred x = Float (pPred (vNum b)) (Zpred (Fexp x)).

Theorem FPredSimpl3 :
 FPred (Float (nNormMin radix precision) (- dExp b)) =
 Float (Zpred (nNormMin radix precision)) (- dExp b).

Theorem FPredSimpl4 :
  x : float,
 Fnum x (- pPred (vNum b))%Z
 Fnum x nNormMin radix precision
 FPred x = Float (Zpred (Fnum x)) (Fexp x).

Theorem FPredFopFSucc :
  x : float, FPred x = Fopp (FSucc b radix precision (Fopp x)).

Theorem FPredDiff1 :
  x : float,
 Fnum x nNormMin radix precision
 Fminus radix x (FPred x) = Float 1%nat (Fexp x) :>R.

Theorem FPredDiff2 :
  x : float,
 Fnum x = nNormMin radix precision
 Fexp x = (- dExp b)%Z Fminus radix x (FPred x) = Float 1%nat (Fexp x) :>R.

Theorem FPredDiff3 :
  x : float,
 Fnum x = nNormMin radix precision
 Fexp x (- dExp b)%Z
 Fminus radix x (FPred x) = Float 1%nat (Zpred (Fexp x)) :>R.

Theorem FBoundedPred : f : float, Fbounded b f Fbounded b (FPred f).

Theorem FPredCanonic :
  a : float, Fcanonic radix b a Fcanonic radix b (FPred a).

Theorem FPredLt : a : float, (FPred a < a)%R.

Theorem R0RltRlePred : x : float, (0 < x)%R (0 FPred x)%R.

Theorem FPredProp :
  x y : float,
 Fcanonic radix b x Fcanonic radix b y (x < y)%R (x FPred y)%R.

Definition FNPred (x : float) := FPred (Fnormalize radix b precision x).

Theorem FNPredFopFNSucc :
  x : float, FNPred x = Fopp (FNSucc b radix precision (Fopp x)).

Theorem FNPredCanonic :
  a : float, Fbounded b a Fcanonic radix b (FNPred a).

Theorem FNPredLt : a : float, (FNPred a < a)%R.

Theorem FPredSuc :
  x : float,
 Fcanonic radix b x FPred (FSucc b radix precision x) = x.

Theorem FSucPred :
  x : float,
 Fcanonic radix b x FSucc b radix precision (FPred x) = x.

End pred.
Section FMinMax.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Hypothesis precisionNotZero : precision 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition boundNat (n : nat) := Float 1%nat (digit radix n).

Theorem boundNatCorrect : n : nat, (n < boundNat n)%R.


Definition boundR (r : R) := boundNat (Zabs_nat (up (Rabs r))).

Theorem boundRCorrect1 : r : R, (r < boundR r)%R.

Theorem boundRrOpp : r : R, boundR r = boundR (- r).

Theorem boundRCorrect2 : r : R, (Fopp (boundR r) < r)%R.

Definition mBFloat (p : R) :=
  map (fun p : Z × ZFloat (fst p) (snd p))
    (mProd Z Z (Z × Z)
       (mZlist (- pPred (vNum b)) (pPred (vNum b)))
       (mZlist (- dExp b) (Fexp (boundR p)))).

Theorem mBFadic_correct1 :
  (r : R) (q : float),
 ¬ is_Fzero q
 (Fopp (boundR r) < q)%R
 (q < boundR r)%R Fbounded b q In q (mBFloat r).

Theorem mBFadic_correct3 : r : R, In (Fopp (boundR r)) (mBFloat r).

Theorem mBFadic_correct4 :
  r : R, In (Float 0%nat (- dExp b)) (mBFloat r).

Theorem mBPadic_Fbounded :
  (p : float) (r : R), In p (mBFloat r) Fbounded b p.


Definition ProjectorP (P : R float Prop) :=
   p q : float, Fbounded b p P p q p = q :>R.

Definition MonotoneP (P : R float Prop) :=
   (p q : R) (p' q' : float),
  (p < q)%R P p p' P q q' (p' q')%R.

Definition isMin (r : R) (min : float) :=
  Fbounded b min
  (min r)%R
  ( f : float, Fbounded b f (f r)%R (f min)%R).

Theorem isMin_inv1 : (p : float) (r : R), isMin r p (p r)%R.

Theorem ProjectMin : ProjectorP isMin.

Theorem MonotoneMin : MonotoneP isMin.

Definition isMax (r : R) (max : float) :=
  Fbounded b max
  (r max)%R
  ( f : float, Fbounded b f (r f)%R (max f)%R).

Theorem isMax_inv1 : (p : float) (r : R), isMax r p (r p)%R.

Theorem ProjectMax : ProjectorP isMax.

Theorem MonotoneMax : MonotoneP isMax.

Theorem MinEq :
  (p q : float) (r : R), isMin r p isMin r q p = q :>R.

Theorem MaxEq :
  (p q : float) (r : R), isMax r p isMax r q p = q :>R.

Theorem MinOppMax :
  (p : float) (r : R), isMin r p isMax (- r) (Fopp p).

Theorem MaxOppMin :
  (p : float) (r : R), isMax r p isMin (- r) (Fopp p).

Theorem MinMax :
  (p : float) (r : R),
 isMin r p r p :>R isMax r (FNSucc b radix precision p).

Theorem MinExList :
  (r : R) (L : list float),
 ( f : float, In f L (r < f)%R)
 ( min : float,
    In min L
    (min r)%R ( f : float, In f L (f r)%R (f min)%R)).

Theorem MinEx : r : R, min : float, isMin r min.

Theorem MaxEx : r : R, max : float, isMax r max.

Theorem FminRep :
  p q : float,
 isMin p q m : Z, q = Float m (Fexp p) :>R.

Theorem MaxMin :
  (p : float) (r : R),
 isMax r p r p :>R isMin r (FNPred b radix precision p).

Theorem FmaxRep :
  p q : float,
 isMax p q m : Z, q = Float m (Fexp p) :>R.

End FMinMax.


Section FOdd.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.

Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition Even (z : Z) : Prop := z1 : _, z = (2 × z1)%Z.

Definition Odd (z : Z) : Prop := z1 : _, z = (2 × z1 + 1)%Z.

Theorem OddSEven : n : Z, Odd n Even (Zsucc n).

Theorem EvenSOdd : n : Z, Even n Odd (Zsucc n).

Theorem OddSEvenInv : n : Z, Odd (Zsucc n) Even n.

Theorem EvenSOddInv : n : Z, Even (Zsucc n) Odd n.

Theorem EvenO : Even 0.

Theorem Odd1 : Odd 1.

Theorem OddOpp : z : Z, Odd z Odd (- z).

Theorem EvenOpp : z : Z, Even z Even (- z).

Theorem OddEvenDec : n : Z, {Odd n} + {Even n}.

Theorem OddNEven : n : Z, Odd n ¬ Even n.

Theorem EvenNOdd : n : Z, Even n ¬ Odd n.

Theorem EvenPlus1 : n m : Z, Even n Even m Even (n + m).

Theorem OddPlus2 : n m : Z, Even n Odd m Odd (n + m).

Theorem EvenMult1 : n m : Z, Even n Even (n × m).

Theorem EvenMult2 : n m : Z, Even m Even (n × m).

Theorem OddMult : n m : Z, Odd n Odd m Odd (n × m).

Theorem EvenMultInv : n m : Z, Even (n × m) Odd n Even m.

Theorem EvenExp :
  (n : Z) (m : nat), Even n Even (Zpower_nat n (S m)).

Theorem OddExp :
  (n : Z) (m : nat), Odd n Odd (Zpower_nat n m).

Definition Feven (p : float) := Even (Fnum p).

Definition Fodd (p : float) := Odd (Fnum p).

Theorem FevenOrFodd : p : float, Feven p Fodd p.

Theorem FevenSucProp :
  p : float,
 (Fodd p Feven (FSucc b radix precision p))
 (Feven p Fodd (FSucc b radix precision p)).

Theorem FoddSuc :
  p : float, Fodd p Feven (FSucc b radix precision p).

Theorem FevenSuc :
  p : float, Feven p Fodd (FSucc b radix precision p).

Theorem FevenFop : p : float, Feven p Feven (Fopp p).

Definition FNodd (p : float) := Fodd (Fnormalize radix b precision p).

Definition FNeven (p : float) := Feven (Fnormalize radix b precision p).

Theorem FNoddEq :
  f1 f2 : float,
 Fbounded b f1 Fbounded b f2 f1 = f2 :>R FNodd f1 FNodd f2.

Theorem FNevenEq :
  f1 f2 : float,
 Fbounded b f1 Fbounded b f2 f1 = f2 :>R FNeven f1 FNeven f2.

Theorem FNevenFop : p : float, FNeven p FNeven (Fopp p).

Theorem FNoddSuc :
  p : float,
 Fbounded b p FNodd p FNeven (FNSucc b radix precision p).

Theorem FNevenSuc :
  p : float,
 Fbounded b p FNeven p FNodd (FNSucc b radix precision p).

Theorem FNevenOrFNodd : p : float, FNeven p FNodd p.

Theorem FnOddNEven : n : float, FNodd n ¬ FNeven n.

End FOdd.

Section FRound.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition TotalP (P : R float Prop) :=
   r : R, p : float, P r p.

Definition UniqueP (P : R float Prop) :=
   (r : R) (p q : float), P r p P r q p = q :>R.

Definition CompatibleP (P : R float Prop) :=
   (r1 r2 : R) (p q : float),
  P r1 p r1 = r2 p = q :>R Fbounded b q P r2 q.

Definition MinOrMaxP (P : R float Prop) :=
   (r : R) (p : float), P r p isMin b radix r p isMax b radix r p.

Definition RoundedModeP (P : R float Prop) :=
  TotalP P CompatibleP P MinOrMaxP P MonotoneP radix P.

Theorem RoundedModeP_inv2 : P, RoundedModeP P CompatibleP P.

Theorem RoundedModeP_inv4 : P, RoundedModeP P MonotoneP radix P.

Theorem RoundedProjector : P, RoundedModeP P ProjectorP b radix P.

Theorem MinCompatible : CompatibleP (isMin b radix).

Theorem MinRoundedModeP : RoundedModeP (isMin b radix).

Theorem MaxCompatible : CompatibleP (isMax b radix).

Theorem MaxRoundedModeP : RoundedModeP (isMax b radix).

Theorem MinUniqueP : UniqueP (isMin b radix).

Theorem MaxUniqueP : UniqueP (isMax b radix).

Theorem MinOrMaxRep :
  P,
 MinOrMaxP P
  p q : float, P p q m : Z, q = Float m (Fexp p) :>R.

Theorem RoundedModeRep :
  P,
 RoundedModeP P
  p q : float, P p q m : Z, q = Float m (Fexp p) :>R.

Definition SymmetricP (P : R float Prop) :=
   (r : R) (p : float), P r p P (- r)%R (Fopp p).

End FRound.

Inductive Option (A : Set) : Set :=
  | Some : x : A, Option A
  | None : Option A.


Fixpoint Pdiv (p q : positive) {struct p} :
 Option positive × Option positive :=
  match p with
  | xH
      match q with
      | xH(Some _ 1%positive, None _)
      | xO r(None _, Some _ p)
      | xI r(None _, Some _ p)
      end
  | xI p'
      match Pdiv p' q with
      | (None, None)
          match (1 - Zpos q)%Z with
          | Z0(Some _ 1%positive, None _)
          | Zpos r'(Some _ 1%positive, Some _ r')
          | Zneg r'(None _, Some _ 1%positive)
          end
      | (None, Some r1)
          match (Zpos (xI r1) - Zpos q)%Z with
          | Z0(Some _ 1%positive, None _)
          | Zpos r'(Some _ 1%positive, Some _ r')
          | Zneg r'(None _, Some _ (xI r1))
          end
      | (Some q1, None)
          match (1 - Zpos q)%Z with
          | Z0(Some _ (xI q1), None _)
          | Zpos r'(Some _ (xI q1), Some _ r')
          | Zneg r'(Some _ (xO q1), Some _ 1%positive)
          end
      | (Some q1, Some r1)
          match (Zpos (xI r1) - Zpos q)%Z with
          | Z0(Some _ (xI q1), None _)
          | Zpos r'(Some _ (xI q1), Some _ r')
          | Zneg r'(Some _ (xO q1), Some _ (xI r1))
          end
      end
  | xO p'
      match Pdiv p' q with
      | (None, None)(None _, None _)
      | (None, Some r1)
          match (Zpos (xO r1) - Zpos q)%Z with
          | Z0(Some _ 1%positive, None _)
          | Zpos r'(Some _ 1%positive, Some _ r')
          | Zneg r'(None _, Some _ (xO r1))
          end
      | (Some q1, None)(Some _ (xO q1), None _)
      | (Some q1, Some r1)
          match (Zpos (xO r1) - Zpos q)%Z with
          | Z0(Some _ (xI q1), None _)
          | Zpos r'(Some _ (xI q1), Some _ r')
          | Zneg r'(Some _ (xO q1), Some _ (xO r1))
          end
      end
  end.

Definition oZ h := match h with
                   | None ⇒ 0
                   | Some pnat_of_P p
                   end.

Theorem Pdiv_correct :
  p q,
 nat_of_P p =
 oZ (fst (Pdiv p q)) × nat_of_P q + oZ (snd (Pdiv p q))
 oZ (snd (Pdiv p q)) < nat_of_P q.

Transparent Pdiv.

Definition oZ1 (x : Option positive) :=
  match x with
  | None ⇒ 0%Z
  | Some zZpos z
  end.

Definition Zquotient (n m : Z) :=
  match n, m with
  | Z0, _ ⇒ 0%Z
  | _, Z0 ⇒ 0%Z
  | Zpos x, Zpos ymatch Pdiv x y with
                      | (x, _)oZ1 x
                      end
  | Zneg x, Zneg ymatch Pdiv x y with
                      | (x, _)oZ1 x
                      end
  | Zpos x, Zneg ymatch Pdiv x y with
                      | (x, _) ⇒ (- oZ1 x)%Z
                      end
  | Zneg x, Zpos ymatch Pdiv x y with
                      | (x, _) ⇒ (- oZ1 x)%Z
                      end
  end.

Theorem inj_oZ1 : z, oZ1 z = Z_of_nat (oZ z).

Theorem ZquotientProp :
  m n : Z,
 n 0%Z
 ex
   (fun r : Z
    m = (Zquotient m n × n + r)%Z
    (Zabs (Zquotient m n × n) Zabs m)%Z (Zabs r < Zabs n)%Z).

Theorem ZquotientPos :
  z1 z2 : Z, (0 z1)%Z (0 z2)%Z (0 Zquotient z1 z2)%Z.

Definition Zdivides (n m : Z) := q : Z, n = (m × q)%Z.

Theorem ZdividesZquotient :
  n m : Z, m 0%Z Zdivides n m n = (Zquotient n m × m)%Z.

Theorem ZdividesZquotientInv :
  n m : Z, n = (Zquotient n m × m)%Z Zdivides n m.

Theorem ZdividesMult :
  n m p : Z, Zdivides n m Zdivides (p × n) (p × m).

Theorem Zeq_mult_simpl :
  a b c : Z, c 0%Z (a × c)%Z = (b × c)%Z a = b.

Theorem ZdividesDiv :
  n m p : Z, p 0%Z Zdivides (p × n) (p × m) Zdivides n m.

Definition ZdividesP : n m : Z, {Zdivides n m} + {¬ Zdivides n m}.
Defined.

Theorem Zdivides1 : m : Z, Zdivides m 1.

Theorem Zabs_eq_case :
  z1 z2 : Z, Zabs z1 = Zabs z2 z1 = z2 z1 = (- z2)%Z.

Theorem NotDividesDigit :
  r v : Z,
 (1 < r)%Z v 0%Z ¬ Zdivides v (Zpower_nat r (digit r v)).

Theorem ZDividesLe :
  n m : Z, n 0%Z Zdivides n m (Zabs m Zabs n)%Z.


Section mf.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Let FtoRradix := FtoR radix.

Fixpoint maxDiv (v : Z) (p : nat) {struct p} : nat :=
  match p with
  | O ⇒ 0
  | S p'
      match ZdividesP v (Zpower_nat radix p) with
      | left _p
      | right _maxDiv v p'
      end
  end.

Theorem maxDivLess : (v : Z) (p : nat), maxDiv v p p.

Theorem maxDivLt :
  (v : Z) (p : nat),
 ¬ Zdivides v (Zpower_nat radix p) maxDiv v p < p.

Theorem maxDivCorrect :
  (v : Z) (p : nat), Zdivides v (Zpower_nat radix (maxDiv v p)).

Theorem maxDivSimplAux :
  (v : Z) (p q : nat),
 p = maxDiv v (S (q + p)) p = maxDiv v (S p).

Theorem maxDivSimpl :
  (v : Z) (p q : nat),
 p < q p = maxDiv v q p = maxDiv v (S p).

Theorem maxDivSimplInvAux :
  (v : Z) (p q : nat),
 p = maxDiv v (S p) p = maxDiv v (S (q + p)).

Theorem maxDivSimplInv :
  (v : Z) (p q : nat),
 p < q p = maxDiv v (S p) p = maxDiv v q.

Theorem maxDivUnique :
  (v : Z) (p : nat),
 p = maxDiv v (S p)
 Zdivides v (Zpower_nat radix p) ¬ Zdivides v (Zpower_nat radix (S p)).

Theorem maxDivUniqueDigit :
  v : Z,
 v 0
 Zdivides v (Zpower_nat radix (maxDiv v (digit radix v)))
 ¬ Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))).

Theorem maxDivUniqueInverse :
  (v : Z) (p : nat),
 Zdivides v (Zpower_nat radix p)
 ¬ Zdivides v (Zpower_nat radix (S p)) p = maxDiv v (S p).

Theorem maxDivUniqueInverseDigit :
  (v : Z) (p : nat),
 v 0
 Zdivides v (Zpower_nat radix p)
 ¬ Zdivides v (Zpower_nat radix (S p)) p = maxDiv v (digit radix v).

Theorem maxDivPlus :
  (v : Z) (n : nat),
 v 0
 maxDiv (v × Zpower_nat radix n) (digit radix v + n) =
 maxDiv v (digit radix v) + n.

Definition LSB (x : float) :=
  (Z_of_nat (maxDiv (Fnum x) (Fdigit radix x)) + Fexp x)%Z.

Theorem LSB_shift :
  (x : float) (n : nat), ¬ is_Fzero x LSB x = LSB (Fshift radix n x).

Theorem LSB_comp :
  (x y : float) (n : nat), ¬ is_Fzero x x = y :>R LSB x = LSB y.

Theorem maxDiv_opp :
  (v : Z) (p : nat), maxDiv v p = maxDiv (- v) p.

Theorem LSB_opp : x : float, LSB x = LSB (Fopp x).

Theorem maxDiv_abs :
  (v : Z) (p : nat), maxDiv v p = maxDiv (Zabs v) p.

Theorem LSB_abs : x : float, LSB x = LSB (Fabs x).

Definition MSB (x : float) := Zpred (Z_of_nat (Fdigit radix x) + Fexp x).

Theorem MSB_shift :
  (x : float) (n : nat), ¬ is_Fzero x MSB x = MSB (Fshift radix n x).

Theorem MSB_comp :
  (x y : float) (n : nat), ¬ is_Fzero x x = y :>R MSB x = MSB y.

Theorem MSB_opp : x : float, MSB x = MSB (Fopp x).

Theorem MSB_abs : x : float, MSB x = MSB (Fabs x).

Theorem LSB_le_MSB : x : float, ¬ is_Fzero x (LSB x MSB x)%Z.

Theorem Fexp_le_LSB : x : float, (Fexp x LSB x)%Z.

Theorem Ulp_Le_LSigB :
  x : float, (Float 1%nat (Fexp x) Float 1%nat (LSB x))%R.

Theorem MSB_le_abs :
  x : float, ¬ is_Fzero x (Float 1%nat (MSB x) Fabs x)%R.

Theorem abs_lt_MSB :
  x : float, (Fabs x < Float 1%nat (Zsucc (MSB x)))%R.

Theorem LSB_le_abs :
  x : float, ¬ is_Fzero x (Float 1%nat (LSB x) Fabs x)%R.

Theorem MSB_monotoneAux :
  x y : float,
 (Fabs x Fabs y)%R Fexp x = Fexp y (MSB x MSB y)%Z.

Theorem MSB_monotone :
  x y : float,
 ¬ is_Fzero x ¬ is_Fzero y (Fabs x Fabs y)%R (MSB x MSB y)%Z.

Theorem LSB_rep_min :
  p : float, z : Z, p = Float z (LSB p) :>R.
End mf.

Section FRoundP.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).

Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition Fulp (p : float) :=
  powerRZ radix (Fexp (Fnormalize radix b precision p)).

Theorem FulpComp :
  p q : float,
 Fbounded b p Fbounded b q p = q :>R Fulp p = Fulp q.

Theorem FulpLe :
  p : float, Fbounded b p (Fulp p Float 1 (Fexp p))%R.

Theorem Fulp_zero :
  x : float, is_Fzero x Fulp x = powerRZ radix (- dExp b).

Theorem FulpLe2 :
  p : float,
 Fbounded b p
 Fnormal radix b (Fnormalize radix b precision p)
 (Fulp p Rabs p × powerRZ radix (Zsucc (- precision)))%R.

Theorem FulpGe :
  p : float,
 Fbounded b p (Rabs p (powerRZ radix precision - 1) × Fulp p)%R.

Theorem LeFulpPos :
  x y : float,
 Fbounded b x
 Fbounded b y (0 x)%R (x y)%R (Fulp x Fulp y)%R.

Theorem FulpSucCan :
  p : float,
 Fcanonic radix b p (FSucc b radix precision p - p Fulp p)%R.

Theorem FulpSuc :
  p : float,
 Fbounded b p (FNSucc b radix precision p - p Fulp p)%R.

Theorem FulpPredCan :
  p : float,
 Fcanonic radix b p (p - FPred b radix precision p Fulp p)%R.

Theorem FulpPred :
  p : float,
 Fbounded b p (p - FNPred b radix precision p Fulp p)%R.

Theorem FSuccDiffPos :
  x : float,
 (0 x)%R
 Fminus radix (FSucc b radix precision x) x = Float 1%nat (Fexp x) :>R.

Theorem FulpFPredGePos :
  f : float,
 Fbounded b f
 Fcanonic radix b f
 (0 < f)%R (Fulp (FPred b radix precision f) Fulp f)%R.

Theorem CanonicFulp :
  p : float, Fcanonic radix b p Fulp p = Float 1%nat (Fexp p).

Theorem FSuccUlpPos :
  x : float,
 Fcanonic radix b x
 (0 x)%R Fminus radix (FSucc b radix precision x) x = Fulp x :>R.

Theorem FulpFabs : f : float, Fulp f = Fulp (Fabs f) :>R.

Theorem RoundedModeUlp :
  P,
 RoundedModeP b radix P
  (p : R) (q : float), P p q (Rabs (p - q) < Fulp q)%R.

Theorem RoundedModeErrorExpStrict :
  P,
 RoundedModeP b radix P
  (p q : float) (x : R),
 Fbounded b p
 Fbounded b q
 P x p q = (x - p)%R :>R q 0%R :>R (Fexp q < Fexp p)%Z.

Theorem RoundedModeProjectorIdem :
  P (p : float), RoundedModeP b radix P Fbounded b p P p p.

Theorem RoundedModeBounded :
  P (r : R) (q : float),
 RoundedModeP b radix P P r q Fbounded b q.

Theorem RoundedModeProjectorIdemEq :
  (P : R float Prop) (p q : float),
 RoundedModeP b radix P Fbounded b p P (FtoR radix p) q p = q :>R.

Theorem RoundedModeMult :
  P,
 RoundedModeP b radix P
  (r : R) (q q' : float),
 P r q Fbounded b q' (r radix × q')%R (q radix × q')%R.

Theorem RoundedModeMultLess :
  P,
 RoundedModeP b radix P
  (r : R) (q q' : float),
 P r q Fbounded b q' (radix × q' r)%R (radix × q' q)%R.

Theorem RleMinR0 :
  (r : R) (min : float),
 (0 r)%R isMin b radix r min (0 min)%R.

Theorem RleRoundedR0 :
  (P : R float Prop) (p : float) (r : R),
 RoundedModeP b radix P P r p (0 r)%R (0 p)%R.

Theorem RleMaxR0 :
  (r : R) (max : float),
 (r 0)%R isMax b radix r max (max 0)%R.

Theorem RleRoundedLessR0 :
  (P : R float Prop) (p : float) (r : R),
 RoundedModeP b radix P P r p (r 0)%R (p 0)%R.

Theorem PminPos :
  p min : float,
 (0 p)%R
 Fbounded b p
 isMin b radix (/ 2%nat × p) min
  c : float, Fbounded b c c = (p - min)%R :>R.

Theorem div2IsBetweenPos :
  p min max : float,
 (0 p)%R
 Fbounded b p
 isMin b radix (/ 2%nat × p) min
 isMax b radix (/ 2%nat × p) max p = (min + max)%R :>R.

Theorem div2IsBetween :
  p min max : float,
 Fbounded b p
 isMin b radix (