Library Flocq.Pff.Pff

Require Export Reals.
Require Export ZArith.
Require Export List.
Require Export PeanoNat.
Require Import Psatz.

Module Import Compat816.

Lemma Even_0 : Nat.Even 0.

Lemma Even_1 : ¬ Nat.Even 1.

Lemma Odd_0 : ¬ Nat.Odd 0.

Lemma Odd_1 : Nat.Odd 1.

Definition Even_Odd_double n :
  (Nat.Even n ↔ n = Nat.double (Nat.div2 n)) ∧ (Nat.Odd n ↔ n = S (Nat.double (Nat.div2 n))).

Definition Even_double n : Nat.Even n → n = Nat.double (Nat.div2 n).
Proof proj1 (proj1 (Even_Odd_double n)).

Definition Odd_double n : Nat.Odd n → n = S (Nat.double (Nat.div2 n)).
Proof proj1 (proj2 (Even_Odd_double n)).

Definition Rinv_mult_distr := Rinv_mult_distr.
Definition Rabs_Rinv := Rabs_Rinv.
Definition Rinv_pow := Rinv_pow.
Definition Rinv_involutive := Rinv_involutive.
Definition Rlt_Rminus := Rlt_Rminus.
Definition powerRZ_inv := powerRZ_inv.
Definition powerRZ_neg := powerRZ_neg.

End Compat816.

Module Import Compat819.

Definition IZR_neq := IZR_neq.

End Compat819.






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 min_or :
 ∀ n m : nat, min n m = n ∧ n ≤ m ∨ min n m = m ∧ m < n.


Theorem convert_not_O : ∀ p : positive, nat_of_P p ≠ 0.

Theorem inj_abs :
 ∀ x : Z, (0 ≤ x)%Z → Z_of_nat (Z.abs_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 Zlt_Zopp : ∀ x y : Z, (x < y)%Z → (- y < - x)%Z.

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

Theorem Zabs_absolu : ∀ z : Z, Z.abs z = Z_of_nat (Z.abs_nat z).

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_Zle :
 ∀ z1 z2 z3 : Z,
 (z1 ≤ z2)%Z → (z1 ≤ z3)%Z → (z1 ≤ Z.min z2 z3)%Z.

Theorem Zopp_Zpred_Zs : ∀ z : Z, (- Z.pred z)%Z = Z.succ (- z).

Definition Zmax : ∀ x_ x_ : Z, Z :=
  fun n m : Z ⇒
  match (n ?= m)%Z with
  | Datatypes.Eq ⇒ m
  | Datatypes.Lt ⇒ m
  | Datatypes.Gt ⇒ n
  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 < Z.succ p)%Z → p = q.

Theorem Zmin_Zmax : ∀ z1 z2 : Z, (Z.min z1 z2 ≤ Zmax z1 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 absolu_Zs :
 ∀ z : Z, (0 ≤ z)%Z → Z.abs_nat (Z.succ z) = S (Z.abs_nat z).

Theorem Zlt_next :
 ∀ n m : Z, (n < m)%Z → m = Z.succ n ∨ (Z.succ n < m)%Z.

Theorem Zle_next :
 ∀ n m : Z, (n ≤ m)%Z → m = n ∨ (Z.succ n ≤ m)%Z.

Theorem inj_pred :
 ∀ n : nat, n ≠ 0 → Z_of_nat (pred n) = Z.pred (Z_of_nat n).

Theorem Zle_abs : ∀ p : Z, (p ≤ Z_of_nat (Z.abs_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 < Z.abs_nat z.

Theorem Rledouble : ∀ r : R, (0 ≤ r)%R → (r ≤ 2 × r)%R.

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

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

Theorem Zabs_eq_opp : ∀ x, (x ≤ 0)%Z → Z.abs x = (- x)%Z.

Theorem Zabs_Zs : ∀ z : Z, (Z.abs (Z.succ z) ≤ Z.succ (Z.abs z))%Z.

Theorem Zle_Zpred : ∀ x y : Z, (x < y)%Z → (x ≤ Z.pred y)%Z.

Theorem Zabs_Zopp : ∀ z : Z, Z.abs (- z) = Z.abs z.

Theorem Zle_Zabs : ∀ z : Z, (z ≤ Z.abs z)%Z.

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


Definition Z_eq_bool := Z.eqb.

Theorem Z_eq_bool_correct :
 ∀ p q : Z,
 match Z_eq_bool p q with
 | true ⇒ p = q
 | false ⇒ p ≠ q
 end.

Theorem Zle_Zpred_Zpred :
 ∀ z1 z2 : Z, (z1 ≤ z2)%Z → (Z.pred z1 ≤ Z.pred z2)%Z.

Theorem Zlt_Zabs_inv1 :
 ∀ z1 z2 : Z, (Z.abs z1 < z2)%Z → (- z2 < z1)%Z.

Theorem Zle_Zabs_inv1 :
 ∀ z1 z2 : Z, (Z.abs z1 ≤ z2)%Z → (- z2 ≤ z1)%Z.

Theorem Zle_Zabs_inv2 :
 ∀ z1 z2 : Z, (Z.abs z1 ≤ z2)%Z → (z1 ≤ z2)%Z.

Theorem Zlt_Zabs_Zpred :
 ∀ z1 z2 : Z,
 (Z.abs z1 < z2)%Z → z1 ≠ Z.pred z2 → (Z.abs (Z.succ z1) < z2)%Z.

Theorem Zle_n_Zpred :
 ∀ z1 z2 : Z, (Z.pred z1 ≤ Z.pred z2)%Z → (z1 ≤ z2)%Z.

Theorem Zpred_Zopp_Zs : ∀ z : Z, Z.pred (- z) = (- Z.succ z)%Z.

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

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

Theorem Zle_Zpred_inv :
 ∀ z1 z2 : Z, (z1 ≤ Z.pred z2)%Z → (z1 < z2)%Z.

Theorem Zabs_intro :
 ∀ (P : Z → Prop) (z : Z), P (- z)%Z → P z → P (Z.abs z).

Theorem Zpred_Zle_Zabs_intro :
 ∀ z1 z2 : Z,
 (- Z.pred z2 ≤ z1)%Z → (z1 ≤ Z.pred z2)%Z → (Z.abs z1 < z2)%Z.

Theorem Zlt_Zabs_intro :
 ∀ z1 z2 : Z, (- z2 < z1)%Z → (z1 < z2)%Z → (Z.abs 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 (Z.abs q) 1 (xO q')
  | Zneg q' ⇒ digitAux (Z.abs 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.Eq ⇒ p = q
 end.

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

Theorem digitLess :
 ∀ q : Z, q ≠ 0%Z → (Zpower_nat n (pred (digit q)) ≤ Z.abs 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, (Z.abs q < Zpower_nat n (digit q))%Z.


Theorem digitInv :
 ∀ (q : Z) (r : nat),
 (Zpower_nat n (pred r) ≤ Z.abs q)%Z →
 (Z.abs q < Zpower_nat n r)%Z → digit q = r.


Theorem digit_monotone :
 ∀ p q : Z, (Z.abs p ≤ Z.abs 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 (Z.abs p) = digit p.

Theorem digit_anti_monotone_lt :
 (1 < n)%Z → ∀ p q : Z, digit p < digit q → (Z.abs p < Z.abs 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 (Z.succ 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 (Z.succ 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 (Z.abs_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 Z_of_nat : nat >-> Z.

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

Local Coercion FtoR : float >-> 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 x ≤ Float 1 y)%R.

Theorem oneExp_Zlt :
 ∀ x y : Z, (Float 1 x < Float 1 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 (Z.abs_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.
Local Coercion FtoRradix : float >-> R.


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.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixNotZero : (0 < radix)%Z.

Definition Fplus (x y : float) :=
  Float
    (Fnum x × Zpower_nat radix (Z.abs_nat (Fexp x - Z.min (Fexp x) (Fexp y))) +
     Fnum y × Zpower_nat radix (Z.abs_nat (Fexp y - Z.min (Fexp x) (Fexp y))))
    (Z.min (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 (Z.abs (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 (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.
Local Coercion FtoRradix : float >-> R.

Coercion Z_of_N: N >-> Z.

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

Definition Fbounded (b : Fbound) (d : float) :=
  (Z.abs (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 (Z.pred (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.
Local Coercion FtoRradix : float >-> R.

Variable b : Fbound.

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

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

End Fprop.



Fixpoint mZlist_aux (p : Z) (n : nat) {struct n} :
 list Z :=
  match n with
  | O ⇒ p :: nil
  | S n1 ⇒ p :: mZlist_aux (Z.succ 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
  | Z0 ⇒ p :: nil
  | Zpos d ⇒ mZlist_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
  | nil ⇒ nil
  | 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.
Local Coercion FtoRradix : float >-> R.
Variable b : Fbound.

Definition Fnormal (p : float) :=
  Fbounded b p ∧ (Zpos (vNum b) ≤ Z.abs (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 := Z.pred (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 ∧ (Z.abs (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 (Z.succ (Fnum p)) (Fexp p) :>R.

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

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

Theorem vNumPrecision :
 ∀ n : Z,
 digit radix n ≤ precision → (Z.abs n < Zpos (vNum b))%Z.

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

Theorem digitGivesBoundedNum :
 ∀ p : float,
 Fdigit radix p ≤ precision → (Z.abs (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,
 (Z.abs 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 ≤ Z.abs (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 → (Z.abs (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) (Z.abs_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.
Local Coercion FtoRradix : float >-> R.

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
  | true ⇒ Float (nNormMin radix precision) (Z.succ (Fexp x))
  | false ⇒
      match Z_eq_bool (Fnum x) (- nNormMin radix precision) with
      | true ⇒
          match Z_eq_bool (Fexp x) (- dExp b) with
          | true ⇒ Float (Z.succ (Fnum x)) (Fexp x)
          | false ⇒ Float (- pPred (vNum b)) (Z.pred (Fexp x))
          end
      | false ⇒ Float (Z.succ (Fnum x)) (Fexp x)
      end
  end.

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

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

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

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

Theorem FSuccDiff1 :
 ∀ x : float,
 Fnum x ≠ (- nNormMin radix precision)%Z →
 Fminus radix (FSucc x) x = Float 1 (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 (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 (Z.pred (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 ≠ Z.pred (nNormMin radix precision) → Fsubnormal radix b (FSucc a).

Theorem FSuccSubnormNearNormMin :
 ∀ a : float,
 Fsubnormal radix b a →
 Fnum a = Z.pred (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.
Local Coercion FtoRradix : float >-> R.

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.
Local Coercion FtoRradix : float >-> R.

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
  | true ⇒ Float (- nNormMin radix precision) (Z.succ (Fexp x))
  | false ⇒
      match Z_eq_bool (Fnum x) (nNormMin radix precision) with
      | true ⇒
          match Z_eq_bool (Fexp x) (- dExp b) with
          | true ⇒ Float (Z.pred (Fnum x)) (Fexp x)
          | false ⇒ Float (pPred (vNum b)) (Z.pred (Fexp x))
          end
      | false ⇒ Float (Z.pred (Fnum x)) (Fexp x)
      end
  end.

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

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

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

Theorem FPredSimpl4 :
 ∀ x : float,
 Fnum x ≠ (- pPred (vNum b))%Z →
 Fnum x ≠ nNormMin radix precision →
 FPred x = Float (Z.pred (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 (Fexp x) :>R.

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

Theorem FPredDiff3 :
 ∀ x : float,
 Fnum x = nNormMin radix precision →
 Fexp x ≠ (- dExp b)%Z →
 Fminus radix x (FPred x) = Float 1 (Z.pred (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.
Local Coercion FtoRradix : float >-> R.
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 (digit radix n).

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


Definition boundR (r : R) := boundNat (Z.abs_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 × Z ⇒ Float (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 (- 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.
Local Coercion FtoRradix : float >-> R.

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 (Z.succ n).

Theorem EvenSOdd : ∀ n : Z, Even n → Odd (Z.succ n).

Theorem OddSEvenInv : ∀ n : Z, Odd (Z.succ n) → Even n.

Theorem EvenSOddInv : ∀ n : Z, Even (Z.succ 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.
Local Coercion FtoRradix : float >-> R.

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 p ⇒ nat_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 z ⇒ Zpos z
  end.

Definition Zquotient (n m : Z) :=
  match n, m with
  | Z0, _ ⇒ 0%Z
  | _, Z0 ⇒ 0%Z
  | Zpos x, Zpos y ⇒ match Pdiv x y with
                      | (x, _) ⇒ oZ1 x
                      end
  | Zneg x, Zneg y ⇒ match Pdiv x y with
                      | (x, _) ⇒ oZ1 x
                      end
  | Zpos x, Zneg y ⇒ match Pdiv x y with
                      | (x, _) ⇒ (- oZ1 x)%Z
                      end
  | Zneg x, Zpos y ⇒ match 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 ∧
    (Z.abs (Zquotient m n × n) ≤ Z.abs m)%Z ∧ (Z.abs r < Z.abs 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 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 → (Z.abs m ≤ Z.abs 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.
Local Coercion FtoRradix : float >-> R.

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 (Z.abs v) p.

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

Definition MSB (x : float) := Z.pred (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 (Fexp x) ≤ Float 1 (LSB x))%R.

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

Theorem abs_lt_MSB :
 ∀ x : float, (Fabs x < Float 1 (Z.succ (MSB x)))%R.

Theorem LSB_le_abs :
 ∀ x : float, ¬ is_Fzero x → (Float 1 (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.
Local Coercion FtoRradix : float >-> R.
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 (Z.succ (- 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 (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 (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<