Library Flocq.Pff.Pff

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

Module Import Compat.

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)).

End Compat.






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 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 × 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 × p) min →
 isMax b radix (/ 2 × p) max → p = (min + max)%R :>R.

Theorem div2IsBetween :
 ∀ p min max : float,
 Fbounded b p →
 isMin b radix (/ 2 × p) min →
 isMax b radix (/ 2 × p) max → p = (min + max)%R :>R.

Theorem RoundedModeMultAbs :
 ∀ P,
 RoundedModeP b radix P →
 ∀ (r : R) (q q' : float),
 P r q →
 Fbounded b q' → (Rabs r ≤ radix × q')%R → (Rabs q ≤ radix × q')%R.

Theorem isMinComp :
 ∀ (r1 r2 : R) (min max : float),
 isMin b radix r1 min →
 isMax b radix r1 max → (min < r2)%R → (r2 < max)%R → isMin b radix r2 min.

Theorem isMaxComp :
 ∀ (r1 r2 : R) (min max : float),
 isMin b radix r1 min →
 isMax b radix r1 max → (min < r2)%R → (r2 < max)%R → isMax b radix r2 max.

Theorem RleBoundRoundl :
 ∀ P,
 RoundedModeP b radix P →
 ∀ (p q : float) (r : R),
 Fbounded b p → (p ≤ r)%R → P r q → (p ≤ q)%R.

Theorem RleBoundRoundr :
 ∀ P,
 RoundedModeP b radix P →
 ∀ (p q : float) (r : R),
 Fbounded b p → (r ≤ p)%R → P r q → (q ≤ p)%R.

Theorem RoundAbsMonotoner :
 ∀ (P : R → float → Prop) (p : R) (q r : float),
 RoundedModeP b radix P →
 Fbounded b r → P p q → (Rabs p ≤ r)%R → (Rabs q ≤ r)%R.

Theorem RoundAbsMonotonel :
 ∀ (P : R → float → Prop) (p : R) (q r : float),
 RoundedModeP b radix P →
 Fbounded b r → P p q → (r ≤ Rabs p)%R → (r ≤ Rabs q)%R.


Theorem FUlp_Le_LSigB :
 ∀ x : float, Fbounded b x → (Fulp x ≤ Float 1 (LSB radix x))%R.

End FRoundP.


Section FRoundPP.
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.

Theorem errorBoundedMultMin :
 ∀ p q fmin : float,
 Fbounded b p →
 Fbounded b q →
 (0 ≤ p)%R →
 (0 ≤ q)%R →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 isMin b radix (p × q) fmin →
 ∃ r : float,
   r = (p × q - fmin)%R :>R ∧ Fbounded b r ∧ Fexp r = (Fexp p + Fexp q)%Z.

Theorem errorBoundedMultMax :
 ∀ p q fmax : float,
 Fbounded b p →
 Fbounded b q →
 (0 ≤ p)%R →
 (0 ≤ q)%R →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 isMax b radix (p × q) fmax →
 ∃ r : float,
   FtoRradix r = (p × q - fmax)%R ∧
   Fbounded b r ∧ Fexp r = (Fexp p + Fexp q)%Z.

Theorem multExpUpperBound :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q pq : float,
 P (p × q)%R pq →
 Fbounded b p →
 Fbounded b q →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 ∃ r : float,
   Fbounded b r ∧ r = pq :>R ∧ (Fexp r ≤ precision + (Fexp p + Fexp q))%Z.

Theorem errorBoundedMultPos :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q f : float,
 Fbounded b p →
 Fbounded b q →
 (0 ≤ p)%R →
 (0 ≤ q)%R →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 P (p × q)%R f →
 ∃ r : float,
   r = (p × q - f)%R :>R ∧ Fbounded b r ∧ Fexp r = (Fexp p + Fexp q)%Z.

Theorem errorBoundedMultNeg :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q f : float,
 Fbounded b p →
 Fbounded b q →
 (p ≤ 0)%R →
 (0 ≤ q)%R →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 P (p × q)%R f →
 ∃ r : float,
   r = (p × q - f)%R :>R ∧ Fbounded b r ∧ Fexp r = (Fexp p + Fexp q)%Z.

Theorem errorBoundedMult :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q f : float,
 Fbounded b p →
 Fbounded b q →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 P (p × q)%R f →
 ∃ r : float,
   r = (p × q - f)%R :>R ∧ Fbounded b r ∧ Fexp r = (Fexp p + Fexp q)%Z.

Theorem errorBoundedMultExp_aux :
 ∀ n1 n2 : Z,
 (Z.abs n1 < Zpos (vNum b))%Z →
 (Z.abs n2 < Zpos (vNum b))%Z →
 (∃ ny : Z,
    (∃ ey : Z,
       (n1 × n2)%R = (ny × powerRZ radix ey)%R :>R ∧
       (Z.abs ny < Zpos (vNum b))%Z)) →
 ∃ nx : Z,
   (∃ ex : Z,
      (n1 × n2)%R = (nx × powerRZ radix ex)%R :>R ∧
      (Z.abs nx < Zpos (vNum b))%Z ∧
      (0 ≤ ex)%Z ∧ (ex ≤ precision)%Z).

Theorem errorBoundedMultExpPos :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q pq : float,
 Fbounded b p →
 Fbounded b q →
 (0 ≤ p)%R →
 (0 ≤ q)%R →
 P (p × q)%R pq →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 ex
   (fun r : float ⇒
    ex
      (fun s : float ⇒
       Fbounded b r ∧
       Fbounded b s ∧
       r = pq :>R ∧
       s = (p × q - r)%R :>R ∧
       Fexp s = (Fexp p + Fexp q)%Z :>Z ∧
       (Fexp s ≤ Fexp r)%Z ∧ (Fexp r ≤ precision + (Fexp p + Fexp q))%Z)).

Theorem errorBoundedMultExp :
 ∀ P, (RoundedModeP b radix P) →
 ∀ p q pq : float,
  (Fbounded b p) → (Fbounded b q) →
  (P (p × q)%R pq) →
   (-(dExp b) ≤ Fexp p + Fexp q)%Z →
   ∃ r : float,
   ∃ s : float,
      (Fbounded b r) ∧ (Fbounded b s) ∧
       r = pq :>R ∧ s = (p × q - r)%R :>R ∧
       (Fexp s = Fexp p + Fexp q)%Z ∧
       (Fexp s ≤ Fexp r)%Z ∧
       (Fexp r ≤ precision + (Fexp p + Fexp q))%Z.

End FRoundPP.
Section Fclosest.
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 Closest (r : R) (p : float) :=
  Fbounded b p ∧
  (∀ f : float, Fbounded b f → (Rabs (p - r) ≤ Rabs (f - r))%R).

Theorem ClosestTotal : TotalP Closest.

Theorem ClosestCompatible : CompatibleP b radix Closest.

Theorem ClosestMin :
 ∀ (r : R) (min max : float),
 isMin b radix r min →
 isMax b radix r max → (2 × r ≤ min + max)%R → Closest r min.

Theorem ClosestMax :
 ∀ (r : R) (min max : float),
 isMin b radix r min →
 isMax b radix r max → (min + max ≤ 2 × r)%R → Closest r max.

Theorem ClosestMinOrMax : MinOrMaxP b radix Closest.

Theorem ClosestMinEq :
 ∀ (r : R) (min max p : float),
 isMin b radix r min →
 isMax b radix r max →
 (2 × r < min + max)%R → Closest r p → p = min :>R.

Theorem ClosestMaxEq :
 ∀ (r : R) (min max p : float),
 isMin b radix r min →
 isMax b radix r max →
 (min + max < 2 × r)%R → Closest r p → p = max :>R.

Theorem ClosestMonotone : MonotoneP radix Closest.

Theorem ClosestRoundedModeP : RoundedModeP b radix Closest.

Definition EvenClosest (r : R) (p : float) :=
  Closest r p ∧
  (FNeven b radix precision p ∨ (∀ q : float, Closest r q → q = p :>R)).

Theorem EvenClosestTotal : TotalP EvenClosest.

Theorem EvenClosestCompatible : CompatibleP b radix EvenClosest.

Theorem EvenClosestMinOrMax : MinOrMaxP b radix EvenClosest.

Theorem EvenClosestMonotone : MonotoneP radix EvenClosest.

Theorem EvenClosestRoundedModeP : RoundedModeP b radix EvenClosest.

Theorem EvenClosestUniqueP : UniqueP radix EvenClosest.

Theorem ClosestSymmetric : SymmetricP Closest.

Theorem EvenClosestSymmetric : SymmetricP EvenClosest.
End Fclosest.

Section Fclosestp2.
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.

Theorem ClosestOpp :
 ∀ (p : float) (r : R),
 Closest b radix r p → Closest b radix (- r) (Fopp p).

Theorem ClosestFabs :
 ∀ (p : float) (r : R),
 Closest b radix r p → Closest b radix (Rabs r) (Fabs p).

Theorem ClosestUlp :
 ∀ (p : R) (q : float),
 Closest b radix p q → (2 × Rabs (p - q) ≤ Fulp b radix precision q)%R.

Theorem ClosestExp :
 ∀ (p : R) (q : float),
 Closest b radix p q → (2 × Rabs (p - q) ≤ powerRZ radix (Fexp q))%R.

Theorem ClosestErrorExpStrict :
 ∀ (p q : float) (x : R),
 Fbounded b p →
 Fbounded b q →
 Closest b radix x p →
 q = (x - p)%R :>R → q ≠ 0%R :>R → (Fexp q < Fexp p)%Z.

Theorem ClosestIdem :
 ∀ p q : float, Fbounded b p → Closest b radix p q → p = q :>R.

Theorem FmultRadixInv :
 ∀ (x z : float) (y : R),
 Fbounded b x →
 Closest b radix y z → (/ 2 × x < y)%R → (/ 2 × x ≤ z)%R.

Theorem ClosestErrorBound :
 ∀ (p q : float) (x : R),
 Fbounded b p →
 Closest b radix x p →
 q = (x - p)%R :>R → (Rabs q ≤ Float 1 (Fexp p) × / 2)%R.

Theorem ClosestErrorBoundNormal_aux :
 ∀ (x : R) (p : float),
 Closest b radix x p →
 Fnormal radix b (Fnormalize radix b precision p) →
 (Rabs (x - p) ≤ Rabs p × (/ 2 × (radix × / Zpos (vNum b))))%R.

Theorem ClosestErrorBoundNormal :
 ∀ (x : R) (p : float),
 Closest b radix x p →
 Fnormal radix b (Fnormalize radix b precision p) →
 (Rabs (x - p) ≤ Rabs p × (/ 2 × powerRZ radix (Z.succ (- precision))))%R.

Theorem FpredUlpPos :
 ∀ x : float,
 Fcanonic radix b x →
 (0 < x)%R →
 (FPred b radix precision x +
  Fulp b radix precision (FPred b radix precision x))%R = x.

Theorem FulpFPredLe :
 ∀ f : float,
 Fbounded b f →
 Fcanonic radix b f →
 (Fulp b radix precision f ≤
  radix × Fulp b radix precision (FPred b radix precision f))%R.

End Fclosestp2.


Section FRoundPM.
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.

Theorem errorBoundedMultClosest_aux :
 ∀ p q pq : float,
 Fbounded b p →
 Fbounded b q →
 Closest b radix (p × q) pq →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 (p × q - pq)%R ≠ 0%R :>R →
 ex
   (fun r : float ⇒
    ex
      (fun s : float ⇒
       Fcanonic radix b r ∧
       Fbounded b r ∧
       Fbounded b s ∧
       r = pq :>R ∧
       s = (p × q - r)%R :>R ∧
       Fexp s = (Fexp p + Fexp q)%Z :>Z ∧
       (Fexp s ≤ Fexp r)%Z ∧ (Fexp r ≤ precision + (Fexp p + Fexp q))%Z)).

Theorem errorBoundedMultClosest :
 ∀ p q pq : float,
 Fbounded b p →
 Fbounded b q →
 Closest b radix (p × q) pq →
 (- dExp b ≤ Fexp p + Fexp q)%Z →
 (- dExp b ≤ Fexp (Fnormalize radix b precision pq) - precision)%Z →
 ex
   (fun r : float ⇒
    ex
      (fun s : float ⇒
       Fcanonic radix b r ∧
       Fbounded b r ∧
       Fbounded b s ∧
       r = pq :>R ∧
       s = (p × q - r)%R :>R ∧ Fexp s = (Fexp r - precision)%Z :>Z)).
End FRoundPM.

Section finduct.
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 Fweight (p : float) :=
  (Fnum p + Fexp p × Zpower_nat radix precision)%Z.

Theorem FweightLt :
 ∀ p q : float,
 Fcanonic radix b p →
 Fcanonic radix b q → (0 ≤ p)%R → (p < q)%R → (Fweight p < Fweight q)%Z.

Theorem FweightEq :
 ∀ p q : float,
 Fcanonic radix b p →
 Fcanonic radix b q → p = q :>R → Fweight p = Fweight q.

Theorem FweightZle :
 ∀ p q : float,
 Fcanonic radix b p →
 Fcanonic radix b q → (0 ≤ p)%R → (p ≤ q)%R → (Fweight p ≤ Fweight q)%Z.

Theorem FinductNegAux :
 ∀ (P : float → Prop) (p : float),
 (0 ≤ p)%R →
 Fcanonic radix b p →
 P p →
 (∀ q : float,
  Fcanonic radix b q →
  (0 < q)%R → (q ≤ p)%R → P q → P (FPred b radix precision q)) →
 ∀ x : Z,
 (0 ≤ x)%Z →
 ∀ q : float,
 x = (Fweight p - Fweight q)%Z →
 Fcanonic radix b q → (0 ≤ q)%R → (q ≤ p)%R → P q.

Theorem FinductNeg :
 ∀ (P : float → Prop) (p : float),
 (0 ≤ p)%R →
 Fcanonic radix b p →
 P p →
 (∀ q : float,
  Fcanonic radix b q →
  (0 < q)%R → (q ≤ p)%R → P q → P (FPred b radix precision q)) →
 ∀ q : float, Fcanonic radix b q → (0 ≤ q)%R → (q ≤ p)%R → P q.

Theorem radixRangeBoundExp :
 ∀ p q : float,
 Fcanonic radix b p →
 Fcanonic radix b q →
 (0 ≤ p)%R →
 (p < q)%R → (q < radix × p)%R → Fexp p = Fexp q ∨ Z.succ (Fexp p) = Fexp q.
End finduct.

Section FRoundPN.
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.

Theorem plusExpMin :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q pq : float,
 P (p + q)%R pq →
 ∃ s : float,
   Fbounded b s ∧ s = pq :>R ∧ (Z.min (Fexp p) (Fexp q) ≤ Fexp s)%Z.

Theorem plusExpUpperBound :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q pq : float,
 P (p + q)%R pq →
 Fbounded b p →
 Fbounded b q →
 ∃ r : float,
   Fbounded b r ∧ r = pq :>R ∧ (Fexp r ≤ Z.succ (Zmax (Fexp p) (Fexp q)))%Z.

Theorem plusExpBound :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q pq : float,
 P (p + q)%R pq →
 Fbounded b p →
 Fbounded b q →
 ∃ r : float,
   Fbounded b r ∧
   r = pq :>R ∧
   (Z.min (Fexp p) (Fexp q) ≤ Fexp r)%Z ∧
   (Fexp r ≤ Z.succ (Zmax (Fexp p) (Fexp q)))%Z.

Theorem minusRoundRep :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q qmp qmmp : float,
 (0 ≤ p)%R →
 (p ≤ q)%R →
 P (q - p)%R qmp →
 Fbounded b p →
 Fbounded b q → ∃ r : float, Fbounded b r ∧ r = (q - qmp)%R :>R.

Theorem ExactMinusIntervalAux :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q : float,
 (0 < p)%R →
 (2 × p < q)%R →
 Fcanonic radix b p →
 Fcanonic radix b q →
 (∃ r : float, Fbounded b r ∧ r = (q - p)%R :>R) →
 ∀ r : float,
 Fcanonic radix b r →
 (2 × p < r)%R →
 (r ≤ q)%R → ∃ r' : float, Fbounded b r' ∧ r' = (r - p)%R :>R.

Theorem ExactMinusIntervalAux1 :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q : float,
 (0 ≤ p)%R →
 (p ≤ q)%R →
 Fcanonic radix b p →
 Fcanonic radix b q →
 (∃ r : float, Fbounded b r ∧ r = (q - p)%R :>R) →
 ∀ r : float,
 Fcanonic radix b r →
 (p ≤ r)%R →
 (r ≤ q)%R → ∃ r' : float, Fbounded b r' ∧ r' = (r - p)%R :>R.

Theorem ExactMinusInterval :
 ∀ P,
 RoundedModeP b radix P →
 ∀ p q : float,
 (0 ≤ p)%R →
 (p ≤ q)%R →
 Fbounded b p →
 Fbounded b q →
 (∃ r : float, Fbounded b r ∧ r = (q - p)%R :>R) →
 ∀ r : float,
 Fbounded b r →
 (p ≤ r)%R →
 (r ≤ q)%R → ∃ r' : float, Fbounded b r' ∧ r' = (r - p)%R :>R.

Theorem MSBroundLSB :
 ∀ P : R → float → Prop,
 RoundedModeP b radix P →
 ∀ f1 f2 : float,
 P f1 f2 →
 ¬ is_Fzero (Fminus radix f1 f2) →
 (MSB radix (Fminus radix f1 f2) < LSB radix f2)%Z.

Theorem LSBMinus :
 ∀ p q : float,
 ¬ is_Fzero (Fminus radix p q) →
 (Z.min (LSB radix p) (LSB radix q) ≤ LSB radix (Fminus radix p q))%Z.

Theorem LSBPlus :
 ∀ p q : float,
 ¬ is_Fzero (Fplus radix p q) →
 (Z.min (LSB radix p) (LSB radix q) ≤ LSB radix (Fplus radix p q))%Z.

End FRoundPN.

Section ClosestP.
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.

Theorem errorBoundedPlusLe :
 ∀ p q pq : float,
 Fbounded b p →
 Fbounded b q →
 (Fexp p ≤ Fexp q)%Z →
 Closest b radix (p + q) pq →
 ∃ error : float,
   error = Rabs (p + q - pq) :>R ∧
   Fbounded b error ∧ Fexp error = Z.min (Fexp p) (Fexp q).

Theorem errorBoundedPlusAbs :
 ∀ p q pq : float,
 Fbounded b p →
 Fbounded b q →
 Closest b radix (p + q) pq →
 ∃ error : float,
   error = Rabs (p + q - pq) :>R ∧
   Fbounded b error ∧ Fexp error = Z.min (Fexp p) (Fexp q).

Theorem errorBoundedPlus :
 ∀ p q pq : float,
 (Fbounded b p) →
 (Fbounded b q) →
 (Closest b radix (p + q) pq) →
 ∃ error : float,
   error = (p + q - pq)%R :>R ∧
   (Fbounded b error) ∧ (Fexp error) = (Z.min (Fexp p) (Fexp q)).

Theorem plusExact1 :
 ∀ p q r : float,
 Fbounded b p →
 Fbounded b q →
 Closest b radix (p + q) r →
 (Fexp r ≤ Z.min (Fexp p) (Fexp q))%Z → r = (p + q)%R :>R.

Theorem plusExact2Aux :
 ∀ p q r : float,
 (0 ≤ p)%R →
 Fcanonic radix b p →
 Fbounded b q →
 Closest b radix (p + q) r →
 (Fexp r < Z.pred (Fexp p))%Z → r = (p + q)%R :>R.

Theorem plusExact2 :
 ∀ p q r : float,
 Fcanonic radix b p →
 Fbounded b q →
 Closest b radix (p + q) r →
 (Fexp r < Z.pred (Fexp p))%Z → r = (p + q)%R :>R.

Theorem plusExactR0 :
 ∀ p q r : float,
 Fbounded b p →
 Fbounded b q →
 Closest b radix (p + q) r → r = 0%R :>R → r = (p + q)%R :>R.

Theorem pPredMoreThanOne : (0 < pPred (vNum b))%Z.

Theorem pPredMoreThanRadix : (radix < pPred (vNum b))%Z.

Theorem plusExactExp :
 ∀ p q pq : float,
 Fbounded b p →
 Fbounded b q →
 Closest b radix (p + q) pq →
 ex
   (fun r : float ⇒
    ex
      (fun s : float ⇒
       Fbounded b r ∧
       Fbounded b s ∧
       s = pq :>R ∧
       r = (p + q - s)%R :>R ∧
       Fexp r = Z.min (Fexp p) (Fexp q) :>Z ∧
       (Fexp r ≤ Fexp s)%Z ∧ (Fexp s ≤ Z.succ (Zmax (Fexp p) (Fexp q)))%Z)).

End ClosestP.


Section MinOrMax_def.
Variable radix : Z.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable precision : nat.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition MinOrMax (z : R) (f : float) :=
  isMin b radix z f ∨ isMax b radix z f.

Theorem MinOrMax_Fopp :
 ∀ (x : R) (f : float), MinOrMax (- x) (Fopp f) → MinOrMax x f.

Theorem MinOrMax1 :
 ∀ (z : R) (p : float),
 Fbounded b p →
 Fcanonic radix b p →
 (0 < p)%R →
 (Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R →
 MinOrMax z p.

Theorem MinOrMax2 :
 ∀ (z : R) (p : float),
 Fbounded b p →
 Fcanonic radix b p →
 (0 < p)%R →
 (Rabs (z - p) < Fulp b radix precision p)%R → (p ≤ z)%R → MinOrMax z p.

Theorem MinOrMax3_aux :
 ∀ (z : R) (p : float),
 Fbounded b p →
 Fcanonic radix b p →
 0%R = p →
 (z ≤ 0)%R →
 (- z < Fulp b radix precision (FPred b radix precision p))%R → MinOrMax z p.

Theorem MinOrMax3 :
 ∀ (z : R) (p : float),
 Fbounded b p →
 Fcanonic radix b p →
 0%R = p →
 (Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R →
 MinOrMax z p.
End MinOrMax_def.

Section AxpyMisc.

Let radix := 2%Z.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable precision : nat.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Theorem FulpLeGeneral :
 ∀ p : float,
 Fbounded b p →
 (Fulp b radix precision p ≤
  Rabs (FtoRradix p) × powerRZ radix (Z.succ (- precision)) +
  powerRZ radix (- dExp b))%R.

Theorem RoundLeGeneral :
 ∀ (p : float) (z : R),
 Fbounded b p →
 Closest b radix z p →
 (Rabs p ≤
  Rabs z × / (1 - powerRZ radix (- precision)) +
  powerRZ radix (Z.pred (- dExp b)) × / (1 - powerRZ radix (- precision)))%R.

Theorem ExactSum_Near :
 ∀ p q f : float,
 Fbounded b p →
 Fbounded b q →
 Fbounded b f →
 Closest b radix (p + q) f →
 Fexp p = (- dExp b)%Z →
 (Rabs (p + q - f) < powerRZ radix (- dExp b))%R → (p + q)%R = f.

End AxpyMisc.

Section AxpyAux.

Let radix := 2%Z.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable precision : nat.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Variables a1 x1 y1 : R.
Variables a x y t u r : float.
Hypothesis Fa : Fbounded b a.
Hypothesis Fx : Fbounded b x.
Hypothesis Fy : Fbounded b y.
Hypothesis Ft : Fbounded b t.
Hypothesis Fu : Fbounded b u.
Hypothesis tDef : Closest b radix (a × x) t.
Hypothesis uDef : Closest b radix (t + y) u.
Hypothesis rDef : isMin b radix (a1 × x1 + y1) r.

Theorem Axpy_aux1 :
 Fcanonic radix b u →
 (Rabs (FtoRradix a × FtoRradix x - FtoRradix t) ≤
  / 4 × Fulp b radix precision (FPred b radix precision u))%R →
 (0 < u)%R →
 (4 × Rabs t ≤ Rabs u)%R →
 (Rabs (y1 - y) + Rabs (a1 × x1 - a × x) <
  / 4 × Fulp b radix precision (FPred b radix precision u))%R →
 MinOrMax radix b (a1 × x1 + y1) u.

Theorem Axpy_aux1_aux1 :
 Fnormal radix b t →
 Fcanonic radix b u →
 (0 < u)%R →
 (4 × Rabs t ≤ Rabs u)%R →
 (Rabs (FtoRradix a × FtoRradix x - FtoRradix t) ≤
  / 4 × Fulp b radix precision (FPred b radix precision u))%R.

Theorem Axpy_aux2 :
 Fcanonic radix b u →
 Fsubnormal radix b t →
 (0 < u)%R →
 FtoRradix u = (t + y)%R →
 (Rabs (y1 - y) + Rabs (a1 × x1 - a × x) <
  / 4 × Fulp b radix precision (FPred b radix precision u))%R →
 MinOrMax radix b (a1 × x1 + y1) u.

Theorem Axpy_aux1_aux3 :
 Fsubnormal radix b t →
 Fcanonic radix b u →
 (0 < u)%R →
 (Z.succ (- dExp b) ≤ Fexp (FPred b radix precision u))%Z →
 (Rabs (FtoRradix a × FtoRradix x - FtoRradix t) ≤
  / 4 × Fulp b radix precision (FPred b radix precision u))%R.

Theorem Axpy_aux3 :
 Fcanonic radix b u →
 Fsubnormal radix b t →
 (0 < u)%R →
 Fexp (FPred b radix precision u) = (- dExp b)%Z →
 (Z.succ (- dExp b) ≤ Fexp u)%Z →
 (Rabs (y1 - y) + Rabs (a1 × x1 - a × x) <
  / 4 × Fulp b radix precision (FPred b radix precision u))%R →
 MinOrMax radix b (a1 × x1 + y1) u.

Theorem AxpyPos :
 Fcanonic radix b u →
 Fcanonic radix b t →
 (0 < u)%R →
 (4 × Rabs t ≤ Rabs u)%R →
 (Rabs (y1 - y) + Rabs (a1 × x1 - a × x) <
  / 4 × Fulp b radix precision (FPred b radix precision u))%R →
 MinOrMax radix b (a1 × x1 + y1) u.

Definition FLess (p : float) :=
  match Rcase_abs p with
  | left _ ⇒ FSucc b radix precision p
  | right _ ⇒ FPred b radix precision p
  end.

Theorem UlpFlessuGe_aux :
 ∀ p : float,
 Fbounded b p →
 Fcanonic radix b p →
 (Rabs p - Fulp b radix precision p ≤ Rabs (FLess p))%R.

Theorem UlpFlessuGe :
 Fcanonic radix b u →
 (/
  (4 × (powerRZ radix precision - 1) × (1 + powerRZ radix (- precision))) ×
  ((1 - powerRZ radix (Z.succ (- precision))) × Rabs y) +
  -
  (/
   (4 × (powerRZ radix precision - 1) × (1 + powerRZ radix (- precision)) ×
    (1 - powerRZ radix (- precision))) ×
   ((1 - powerRZ radix (Z.succ (- precision))) × Rabs (a × x))) +
  -
  (powerRZ radix (Z.pred (- dExp b)) ×
   (/ (2 × (powerRZ radix precision - 1)) +
    /
    (4 × (powerRZ radix precision - 1) ×
     (1 + powerRZ radix (- precision)) × (1 - powerRZ radix (- precision))) ×
    (1 - powerRZ radix (Z.succ (- precision))))) ≤
  / 4 × Fulp b radix precision (FLess u))%R.

Theorem UlpFlessuGe2 :
 Fcanonic radix b u →
 (powerRZ radix (Z.pred (Z.pred (- precision))) ×
  (1 - powerRZ radix (Z.succ (- precision))) × Rabs y +
  - (powerRZ radix (Z.pred (Z.pred (- precision))) × Rabs (a × x)) +
  - powerRZ radix (Z.pred (Z.pred (- dExp b))) <
  / 4 × Fulp b radix precision (FLess u))%R.

End AxpyAux.

Section Axpy.

Let radix := 2%Z.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable precision : nat.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Theorem Axpy_tFlessu :
 ∀ (a1 x1 y1 : R) (a x y t u : float),
 Fbounded b a →
 Fbounded b x →
 Fbounded b y →
 Fbounded b t →
 Fbounded b u →
 Closest b radix (a × x) t →
 Closest b radix (t + y) u →
 Fcanonic radix b u →
 Fcanonic radix b t →
 (4 × Rabs t ≤ Rabs u)%R →
 (Rabs (y1 - y) + Rabs (a1 × x1 - a × x) <
  / 4 × Fulp b radix precision (FLess b precision u))%R →
 MinOrMax radix b (a1 × x1 + y1) u.

Theorem Axpy_opt :
 ∀ (a1 x1 y1 : R) (a x y t u : float),
 (Fbounded b a) → (Fbounded b x) → (Fbounded b y) →
 (Fbounded b t) → (Fbounded b u) →
 (Closest b radix (a × x) t) →
 (Closest b radix (t + y) u) →
 (Fcanonic radix b u) → (Fcanonic radix b t) →
 ((5 + 4 × (powerRZ radix (- precision))) ×
    / (1 - powerRZ radix (- precision)) ×
    (Rabs (a × x) + (powerRZ radix (Z.pred (- dExp b))))
    ≤ Rabs y)%R →
 (Rabs (y1 - y) + Rabs (a1 × x1 - a × x) ≤
    (powerRZ radix (Z.pred (Z.pred (- precision)))) ×
    (1 - powerRZ radix (Z.succ (- precision))) × Rabs y +
    - (powerRZ radix (Z.pred (Z.pred (- precision))) × Rabs (a × x)) +
    - powerRZ radix (Z.pred (Z.pred (- dExp b))))%R →
         (MinOrMax radix b (a1 × x1 + y1) u).

End Axpy.

Section Generic.
Variable b : Fbound.
Variable radix : Z.
Variable p : 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 pGivesBound : Zpos (vNum b) = Zpower_nat radix p.

Theorem FboundedMbound2Pos :
 (0 < p) →
 ∀ z m : Z,
 (0 ≤ m)%Z →
 (m ≤ Zpower_nat radix p)%Z →
 (- dExp b ≤ z)%Z →
 ∃ c : float, Fbounded b c ∧ c = (m × powerRZ radix z)%R :>R ∧ (z ≤ Fexp c)%Z.

Theorem FboundedMbound2 :
 (0 < p) →
 ∀ z m : Z,
 (Z.abs m ≤ Zpower_nat radix p)%Z →
 (- dExp b ≤ z)%Z →
 ∃ c : float, Fbounded b c ∧ c = (m × powerRZ radix z)%R :>R ∧ (z ≤ Fexp c)%Z.

Hypothesis precisionGreaterThanOne : 1 < p.

Variable z:R.
Variable f:float.
Variable e:Z.

Hypothesis Bf: Fbounded b f.
Hypothesis Cf: Fcanonic radix b f.
Hypothesis zGe: (powerRZ radix (e+p-1) ≤ z)%R.
Hypothesis zLe: (z ≤ powerRZ radix (e+p))%R.
Hypothesis fGe: (powerRZ radix (e+p-1) ≤ f)%R.
Hypothesis eGe: (- dExp b ≤ e)%Z.

Theorem ClosestSuccPred: (Fcanonic radix b f)
 → (Rabs(z-f) ≤ Rabs(z-(FSucc b radix p f)))%R
 → (Rabs(z-f) ≤ Rabs(z-(FPred b radix p f)))%R
 → Closest b radix z f.

Theorem ImplyClosest: (Rabs(z-f) ≤ (powerRZ radix e)/2)%R
  → Closest b radix z f.

Theorem ImplyClosestStrict: (Rabs(z-f) < (powerRZ radix e)/2)%R
  → (∀ g: float, Closest b radix z g → (FtoRradix f=g)%R ).

Theorem ImplyClosestStrict2: (Rabs(z-f) < (powerRZ radix e)/2)%R
  → (Closest b radix z f) ∧ (∀ g: float, Closest b radix z g → (FtoRradix f=g)%R ).

End Generic.

Section Generic2.
Variable b : Fbound.
Variable radix : Z.
Variable p : 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 < p.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix p.

Variable z m:R.
Variable f h:float.

Theorem ClosestImplyEven: (EvenClosest b radix p z f) →
   (∃ g: float, (z=g+(powerRZ radix (Fexp g))/2)%R ∧ (Fcanonic radix b g) ∧ (0 ≤ Fnum g)%Z)
       → (FNeven b radix p f).

Theorem ClosestImplyEven_int: (Even radix)%Z
   → (EvenClosest b radix p z f) → (Fcanonic radix b f) → (0 ≤ f)%R
   → (z=(powerRZ radix (Fexp f))*(m+1/2))%R → (∃ n:Z, IZR n=m)
   → (FNeven b radix p f).

End Generic2.
Section Velt.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.
Variables p x q hx: float.

Let b' := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s).
Hypothesis SGe: (s ≤ t-2).
Hypothesis Fx: Fbounded b x.
Hypothesis pDef: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis qDef: (Closest b radix (x-p)%R q).
Hypothesis hxDef:(Closest b radix (q+p)%R hx).
Hypothesis xPos: (0 < x)%R.
Hypothesis Np: Fnormal radix b p.
Hypothesis Nq: Fnormal radix b q.
Hypothesis Nx: Fnormal radix b x.

Lemma p'GivesBound: Zpos (vNum b')=(Zpower_nat radix (minus t s)).

Lemma pPos: (0 ≤ p)%R.

Lemma qNeg: (q ≤ 0)%R.

Lemma RleRRounded: ∀ (f : float) (z : R),
   Fnormal radix b f → Closest b radix z f → (Rabs z ≤ (Rabs f)*(1+(powerRZ radix (1-t))/2))%R.

Lemma hxExact: (FtoRradix hx=p+q)%R.

Lemma eqLeep: (Fexp q ≤ Fexp p)%Z.

Lemma epLe: (Fexp p ≤s+1+Fexp x)%Z.

Lemma eqLe: (Fexp q ≤ s+ Fexp x)%Z ∨
  ((FtoRradix q= - powerRZ radix (t+s+Fexp x))%R ∧(Rabs (x - hx) ≤ (powerRZ radix (s + Fexp x))/2)%R).

Lemma eqGe: (s+ Fexp x ≤ Fexp q)%Z.

Lemma eqEqual: (Fexp q=s+Fexp x)%Z ∨
  ((FtoRradix q= - powerRZ radix (t+s+Fexp x))%R ∧
     (Rabs (x - hx) ≤ (powerRZ radix (s + Fexp x))/2)%R).

Lemma Veltkamp_aux_aux: ∀ v:float, (FtoRradix v=hx) → Fcanonic radix b' v →
  (Rabs (x-v) ≤ (powerRZ radix (s+Fexp x)) /2)%R
  → (powerRZ radix (t-1+Fexp x) ≤ v)%R.

Lemma Veltkamp_aux:
   (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
   (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
    ∧ (s+Fexp x ≤ Fexp hx')%Z).

Hypothesis pDefEven: (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p).
Hypothesis qDefEven: (EvenClosest b radix t (x-p)%R q).
Hypothesis hxDefEven:(EvenClosest b radix t (q+p)%R hx).

Lemma VeltkampEven1: (Even radix)
   ->(∃ hx':float, (FtoRradix hx'=hx)
    ∧ (EvenClosest b' radix (t-s) x hx')).

Lemma VeltkampEven2: (Odd radix)
   → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).

End Velt.
Section VeltN.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s).
Hypothesis SGe: (s ≤ t-2).

Lemma Veltkamp_pos: ∀ x p q hx:float,
     Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (0 < x)%R
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
       ∧ (s+Fexp x ≤ Fexp hx')%Z).

Lemma VeltkampN_aux: ∀ x p q hx:float,
      Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
       ∧ (s+Fexp x ≤ Fexp hx')%Z).

Lemma VeltkampN: ∀ x p q hx:float,
      Fnormal radix b x
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
       ∧ (s+Fexp x ≤ Fexp hx')%Z).

Lemma VeltkampEven_pos: ∀ x p q hx:float,
      Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (0 < x)%R
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).

Lemma VeltkampEvenN_aux: ∀ x p q hx:float,
      Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).

Lemma VeltkampEvenN: ∀ x p q hx:float,
      Fnormal radix b x
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).

End VeltN.
Section VeltS.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Definition plusExp (b:Fbound):=
   Bound
     (vNum b)
     (Nplus (dExp b) (Npos (P_of_succ_nat (pred (pred t))))).

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s).
Hypothesis SGe: (s ≤ t-2).

Lemma bimplybplusNorm: ∀ f:float,
   Fbounded b f → (FtoRradix f ≠ 0)%R →
    (∃ g:float, (FtoRradix g=f)%R ∧
      Fnormal radix (plusExp b) g).

Lemma Closestbplusb: ∀ b0:Fbound, ∀ z:R, ∀ f:float,
   (Closest (plusExp b0) radix z f) → (Fbounded b0 f) → (Closest b0 radix z f).

Lemma Closestbbplus: ∀ b0:Fbound, ∀ n:nat, ∀ fext f:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
   (-dExp b0 ≤ Fexp fext)%Z →
    (Closest b0 radix fext f) → (Closest (plusExp b0) radix fext f).

Lemma EvenClosestbplusb: ∀ b0:Fbound, ∀ n:nat, ∀ fext f:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
   (-dExp b0 ≤ Fexp fext)%Z →
   (EvenClosest (plusExp b0) radix n fext f) → (Fbounded b0 f)
      → (EvenClosest b0 radix n fext f).

Lemma ClosestClosest: ∀ b0:Fbound, ∀ n:nat, ∀ z:R, ∀ f1 f2:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
    (Closest b0 radix z f1) → (Closest b0 radix z f2)
    → Fnormal radix b0 f2 → (Fexp f1 ≤ Fexp f2 -2)%Z
    → False.

Lemma EvenClosestbbplus: ∀ b0:Fbound, ∀ n:nat, ∀ fext f:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
   (-dExp b0 ≤ Fexp fext)%Z →
    (EvenClosest b0 radix n fext f) → (EvenClosest (plusExp b0) radix n fext f).

Lemma VeltkampS: ∀ x p q hx:float,
     Fsubnormal radix b x
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')).

Lemma VeltkampEvenS: ∀ x p q hx:float,
      Fsubnormal radix b x
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).

End VeltS.
Section VeltUlt.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s).
Hypothesis SGe: (s ≤ t-2).

Theorem Veltkamp: ∀ x p q hx:float,
     (Fbounded b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
      (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
         ∧ ((Fnormal radix b x) → (s+Fexp x ≤ Fexp hx')%Z)).

Theorem VeltkampEven: ∀ x p q hx:float,
     (Fbounded b x)
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).

End VeltUlt.
Section VeltTail.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let bt := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix s))))
    (dExp b).

Let bt2 := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus s 1)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s).
Hypothesis SGe: (s ≤ t-2).

Theorem Veltkamp_tail_aux: ∀ x p q hx tx:float,
     (Fcanonic radix b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (∃ v:float, (FtoRradix v=hx) ∧
     (Fexp (Fminus radix x v) = Fexp x) ∧
      (Z.abs (Fnum (Fminus radix x v)) ≤ (powerRZ radix s)/2)%R).

Theorem Veltkamp_tail: ∀ x p q hx tx:float,
     (Fbounded b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (∃ tx':float, (FtoRradix tx'=tx) ∧
         (hx+tx'=x)%R ∧ (Fbounded bt tx') ∧
         (Fexp (Fnormalize radix b t x) ≤ Fexp tx')%Z).

Theorem Veltkamp_tail2: ∀ x p q hx tx:float,
     (radix=2)%Z
  → (Fbounded b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (∃ tx':float, (FtoRradix tx'=tx) ∧
         (hx+tx'=x)%R ∧ (Fbounded bt2 tx') ∧
         (Fexp (Fnormalize radix b t x) ≤ Fexp tx')%Z).

End VeltTail.

Section VeltUtile.
Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let bt := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix s))))
    (dExp b).

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s).
Hypothesis SGe: (s ≤ t-2).

Theorem VeltkampU: ∀ x p q hx tx:float,
     (Fcanonic radix b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (FtoRradix x=hx+tx)%R ∧

     (∃ hx':float, (FtoRradix hx'=hx)%R
                     ∧ (Fbounded b' hx')
                     ∧ ((Fnormal radix b x) → (s+Fexp x ≤ Fexp hx')%Z)) ∧

     (∃ tx':float, (FtoRradix tx'=tx)%R
                     ∧ (Fbounded bt tx')
                     ∧ (Fexp x ≤ Fexp tx')%Z).

End VeltUtile.

Section GenericDek.
Variable b : Fbound.
Variable radix : Z.
Variable p : 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 pGivesBound : Zpos (vNum b) = Zpower_nat radix p.
Hypothesis precisionGreaterThanOne : 1 < p.

Theorem BoundedL: ∀ (r:R) (x:float) (e:Z),
   (e ≤Fexp x)%Z → (-dExp b ≤ e)%Z → (FtoRradix x=r)%R →
   (Rabs r < powerRZ radix (e+p))%R →
       (∃ x':float, (FtoRradix x'=r) ∧ (Fbounded b x') ∧ Fexp x'=e).

Theorem ClosestZero: ∀ (r:R) (x:float),
  (Closest b radix r x) → (r=0)%R → (FtoRradix x=0)%R.

Theorem Closestbbext: ∀ bext:Fbound, ∀ fext f:float,
    (vNum bext=vNum b) → (dExp b < dExp bext)%Z →
    (-dExp b ≤ Fexp fext)%Z →
    (Closest b radix fext f) → (Closest bext radix fext f).

Variable b' : Fbound.

Definition Underf_Err (a a' : float) (ra n:R) :=
   (Closest b radix ra a) ∧ (Fbounded b' a') ∧
   (Rabs (a-a') ≤ n×powerRZ radix (-(dExp b)))%R ∧
   ( ((-dExp b) ≤ Fexp a')%Z → (FtoRradix a =a')%R).

Theorem Underf_Err1: ∀ (a' a:float),
    vNum b=vNum b' → (dExp b ≤ dExp b')%Z →
   (Fbounded b' a') → (Closest b radix a' a) →
   (Underf_Err a a' (FtoRradix a') (/2)%R).

Theorem Underf_Err2_aux: ∀ (r:R) (x1:float),
    vNum b=vNum b' → (dExp b ≤ dExp b')%Z →
    (Fcanonic radix b x1) →
    (Closest b radix r x1) →
    (∃ x2:float, (Underf_Err x1 x2 r (3/4)%R) ∧ (Closest b' radix r x2)).

Theorem Underf_Err2: ∀ (r:R) (x1:float),
    vNum b=vNum b' → (dExp b ≤ dExp b')%Z →
    (Closest b radix r x1) →
    (∃ x2:float, (Underf_Err x1 x2 r (3/4)%R) ∧ (Closest b' radix r x2)).

Theorem Underf_Err3: ∀ (x x' y y' z' z:float) (rx ry epsx epsy:R),
    vNum b=vNum b' → (dExp b ≤ dExp b')%Z →
   (Underf_Err x x' rx epsx) → (Underf_Err y y' ry epsy) →
   (epsx+epsy ≤ (powerRZ radix (p-1) -1))%R →
   (Fbounded b' z') → (FtoRradix z'=x'-y')%R →
   (Fexp z' ≤ Fexp x')%Z → (Fexp z' ≤ Fexp y')%Z →
   (Closest b radix (x-y) z) →
   (Underf_Err z z' (x-y) (epsx+epsy)%R).

Theorem Underf_Err3_bis: ∀ (x x' y y' z' z:float) (rx ry epsx epsy:R),
   (4 ≤ p) →
    vNum b=vNum b' → (dExp b ≤ dExp b')%Z →
   (Underf_Err x x' rx epsx) → (Underf_Err y y' ry epsy) →
   (epsx+epsy ≤ 7)%R →
   (Fbounded b' z') → (FtoRradix z'=x'-y')%R →
   (Fexp z' ≤ Fexp x')%Z → (Fexp z' ≤ Fexp y')%Z →
   (Closest b radix (x-y) z) →
   (Underf_Err z z' (x-y) (epsx+epsy)%R).

End GenericDek.

Section Sec1.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let bt := Bound
    (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix s))))
    (dExp b).

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).

Hypothesis SLe: (2 ≤ s).
Hypothesis SGe: (s ≤ t-2).

Hypothesis Hst1: (t-1 ≤ s+s)%Z.
Hypothesis Hst2: (s+s ≤ t+1)%Z.

Variables x x1 x2 y y1 y2 r e: float.

Hypotheses Nx: Fnormal radix b x.
Hypotheses Ny: Fnormal radix b y.

Hypothesis K: (-dExp b ≤ Fexp x +Fexp y)%Z.

Hypotheses rDef: Closest b radix (x×y) r.

Hypotheses eeq: (x×y=r+e)%R.
Hypotheses Xeq: (FtoRradix x=x1+x2)%R.
Hypotheses Yeq: (FtoRradix y=y1+y2)%R.

Hypotheses x2Le: (Rabs x2 ≤ (powerRZ radix (s+Fexp x)) /2)%R.
Hypotheses y2Le: (Rabs y2 ≤ (powerRZ radix (s+Fexp y)) /2)%R.
Hypotheses x1Exp: (s+Fexp x ≤ Fexp x1)%Z.
Hypotheses y1Exp: (s+Fexp y ≤ Fexp y1)%Z.
Hypotheses x2Exp: (Fexp x ≤ Fexp x2)%Z.
Hypotheses y2Exp: (Fexp y ≤ Fexp y2)%Z.

Lemma x2y2Le: (Rabs (x2×y2) ≤ (powerRZ radix (2×s+Fexp x+Fexp y)) /4)%R.

Lemma x2y1Le: (Rabs (x2×y1) < (powerRZ radix (t+s+Fexp x+Fexp y)) /2
          + (powerRZ radix (2×s+Fexp x+Fexp y)) /4)%R.

Lemma x1y2Le: (Rabs (x1×y2) < (powerRZ radix (t+s+Fexp x+Fexp y)) /2
          + (powerRZ radix (2×s+Fexp x+Fexp y)) /4)%R.

Lemma eLe: (Rabs e ≤ (powerRZ radix (t+Fexp x+Fexp y)) /2)%R.

Lemma rExp: (t - 1 + Fexp x + Fexp y ≤ Fexp r)%Z.

Lemma powerRZSumRle: ∀ (e1 e2:Z),
  (e2≤ e1)%Z →
  (powerRZ radix e1 + powerRZ radix e2 ≤ powerRZ radix (e1+1))%R.

Lemma Boundedt1: (∃ x':float, (FtoRradix x'=r-x1×y1)%R ∧ (Fbounded b x')
                   ∧ (Fexp x'=t-1+Fexp x+Fexp y)%Z).

Lemma Boundedt2: (∃ x':float, (FtoRradix x'=r-x1×y1-x1×y2)%R ∧ (Fbounded b x')
                   ∧ (Fexp x'=s+Fexp x+Fexp y)%Z).

Lemma Boundedt3: (∃ x':float, (FtoRradix x'=r-x1×y1-x1×y2-x2×y1)%R ∧ (Fbounded b x')
                   ∧ (Fexp x'=s+Fexp x+Fexp y)%Z).

Lemma Boundedt4: (∃ x':float, (FtoRradix x'=r-x1×y1-x1×y2-x2×y1-x2×y2)%R ∧ (Fbounded b x')).

Lemma Boundedt4_aux: (∃ x':float, (FtoRradix x'=r-x1×y1-x1×y2-x2×y1-x2×y2)%R ∧ (Fbounded b x')
  ∧ (Fexp x'=Fexp x+Fexp y)%Z).

Hypotheses Fx1: Fbounded b' x1.
Hypotheses Fx2: Fbounded bt x2.
Hypotheses Fy1: Fbounded b' y1.
Hypotheses Fy2: Fbounded bt y2.
Hypothesis Hst3: (t ≤ s+s)%Z.

Lemma p''GivesBound: Zpos (vNum bt)=(Zpower_nat radix s).

Lemma Boundedx1y1_aux: (∃ x':float, (FtoRradix x'=x1×y1)%R ∧ (Fbounded b x')
  ∧ (Fexp x'=Fexp x1+Fexp y1)%Z ).

Lemma Boundedx1y1: (∃ x':float, (FtoRradix x'=x1×y1)%R ∧ (Fbounded b x')).

Lemma Boundedx1y2_aux: (∃ x':float, (FtoRradix x'=x1×y2)%R ∧ (Fbounded b x')
   ∧ (Fexp x'=Fexp x1+Fexp y2)%Z ).

Lemma Boundedx1y2: (∃ x':float, (FtoRradix x'=x1×y2)%R ∧ (Fbounded b x')).

Lemma Boundedx2y1_aux: (∃ x':float, (FtoRradix x'=x2×y1)%R ∧ (Fbounded b x')
   ∧ (Fexp x'=Fexp x2+Fexp y1)%Z ).

Lemma Boundedx2y1: (∃ x':float, (FtoRradix x'=x2×y1)%R ∧ (Fbounded b x')).

End Sec1.

Section Algo.

Variable radix : Z.
Variable b : Fbound.
Variables t: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 pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypotheses pGe: (4 ≤ t).

Variables x y p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 r t1 t2 t3 t4:float.

Hypothesis Cx: (Fnormal radix b x).
Hypothesis Cy: (Fnormal radix b y).

Hypothesis Expoxy: (-dExp b ≤ Fexp x+Fexp y)%Z.

Let s:= t- Nat.div2 t.

Hypothesis A1: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis A2: (Closest b radix (x-p)%R q).
Hypothesis A3: (Closest b radix (q+p)%R hx).
Hypothesis A4: (Closest b radix (x-hx)%R tx).

Hypothesis B1: (Closest b radix (y*((powerRZ radix s)+1))%R p').
Hypothesis B2: (Closest b radix (y-p')%R q').
Hypothesis B3: (Closest b radix (q'+p')%R hy).
Hypothesis B4: (Closest b radix (y-hy)%R ty).

Hypothesis C1: (Closest b radix (hx×hy)%R x1y1).
Hypothesis C2: (Closest b radix (hx×ty)%R x1y2).
Hypothesis C3: (Closest b radix (tx×hy)%R x2y1).
Hypothesis C4: (Closest b radix (tx×ty)%R x2y2).

Hypothesis D1: (Closest b radix (x×y)%R r).
Hypothesis D2: (Closest b radix (r-x1y1)%R t1).
Hypothesis D3: (Closest b radix (t1-x1y2)%R t2).
Hypothesis D4: (Closest b radix (t2-x2y1)%R t3).
Hypothesis D5: (Closest b radix (t3-x2y2)%R t4).

Lemma SLe: (2 ≤ s).

Lemma SGe: (s ≤ t-2).

Lemma s2Ge: (t ≤ s + s)%Z.

Lemma s2Le: (s + s ≤ t + 1)%Z.

Theorem Dekker_aux: (∃ x':float, (FtoRradix x'=tx×ty)%R ∧ (Fbounded b x'))
    → (x×y=r-t4)%R.

Theorem Boundedx2y2: (radix=2)%Z ∨ (Nat.Even t) →
    (∃ x':float, (FtoRradix x'=tx×ty)%R ∧ (Fbounded b x') ∧ (Fexp x+Fexp y ≤ Fexp x')%Z).

Theorem DekkerN: (radix=2)%Z ∨ (Nat.Even t) → (x×y=r-t4)%R.

End Algo.

Section AlgoS1.

Variable radix : Z.
Variable b : Fbound.
Variables t: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 pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypotheses pGe: (4 ≤ t).

Variables x y p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 r t1 t2 t3 t4:float.

Hypothesis Cx: (Fnormal radix b x).
Hypothesis Cy: (Fsubnormal radix b y).

Hypothesis Expoxy: (-dExp b ≤ Fexp x+Fexp y)%Z.

Let s:= t- Nat.div2 t.

Hypothesis A1: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis A2: (Closest b radix (x-p)%R q).
Hypothesis A3: (Closest b radix (q+p)%R hx).
Hypothesis A4: (Closest b radix (x-hx)%R tx).

Hypothesis B1: (Closest b radix (y*((powerRZ radix s)+1))%R p').
Hypothesis B2: (Closest b radix (y-p')%R q').
Hypothesis B3: (Closest b radix (q'+p')%R hy).
Hypothesis B4: (Closest b radix (y-hy)%R ty).

Hypothesis C1: (Closest b radix (hx×hy)%R x1y1).
Hypothesis C2: (Closest b radix (hx×ty)%R x1y2).
Hypothesis C3: (Closest b radix (tx×hy)%R x2y1).
Hypothesis C4: (Closest b radix (tx×ty)%R x2y2).

Hypothesis D1: (Closest b radix (x×y)%R r).
Hypothesis D2: (Closest b radix (r-x1y1)%R t1).
Hypothesis D3: (Closest b radix (t1-x1y2)%R t2).
Hypothesis D4: (Closest b radix (t2-x2y1)%R t3).
Hypothesis D5: (Closest b radix (t3-x2y2)%R t4).

Theorem DekkerS1: (radix=2)%Z ∨ (Nat.Even t) → (x×y=r-t4)%R.

End AlgoS1.

Section AlgoS2.

Variable radix : Z.
Variable b : Fbound.
Variables t: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 pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypotheses pGe: (4 ≤ t).

Variables x y p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 r t1 t2 t3 t4:float.

Hypothesis Cx: (Fsubnormal radix b x).
Hypothesis Cy: (Fnormal radix b y).

Hypothesis Expoxy: (-dExp b ≤ Fexp x+Fexp y)%Z.

Let s:= t- Nat.div2 t.

Hypothesis A1: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis A2: (Closest b radix (x-p)%R q).
Hypothesis A3: (Closest b radix (q+p)%R hx).
Hypothesis A4: (Closest b radix (x-hx)%R tx).

Hypothesis B1: (Closest b radix (y*((powerRZ radix s)+1))%R p').
Hypothesis B2: (Closest b radix (y-p')%R q').
Hypothesis B3: (Closest b radix (q'+p')%R hy).
Hypothesis B4: (Closest b radix (y-hy)%R ty).

Hypothesis C1: (Closest b radix (hx×hy)%R x1y1).
Hypothesis C2: (Closest b radix (hx×ty)%R x1y2).
Hypothesis C3: (Closest b radix (tx×hy)%R x2y1).
Hypothesis C4: (Closest b radix (tx×ty)%R x2y2).

Hypothesis D1: (Closest b radix (x×y)%R r).
Hypothesis D2: (Closest b radix (r-x1y1)%R t1).
Hypothesis D3: (Closest b radix (t1-x1y2)%R t2).
Hypothesis D4: (Closest b radix (t2-x2y1)%R t3).
Hypothesis D5: (Closest b radix (t3-x2y2)%R t4).

Theorem DekkerS2: (radix=2)%Z ∨ (Nat.Even t) → (x×y=r-t4)%R.

End AlgoS2.

Section Algo1.

Variable radix : Z.
Variable b : Fbound.
Variables t: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 pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypotheses pGe: (4 ≤ t).

Variables x y p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 r t1 t2 t3 t4:float.

Hypothesis Cx: (Fcanonic radix b x).
Hypothesis Cy: (Fcanonic radix b y).

Hypothesis Expoxy: (-dExp b ≤ Fexp x+Fexp y)%Z.

Let s:= t- Nat.div2 t.

Hypothesis A1: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis A2: (Closest b radix (x-p)%R q).
Hypothesis A3: (Closest b radix (q+p)%R hx).
Hypothesis A4: (Closest b radix (x-hx)%R tx).

Hypothesis B1: (Closest b radix (y*((powerRZ radix s)+1))%R p').
Hypothesis B2: (Closest b radix (y-p')%R q').
Hypothesis B3: (Closest b radix (q'+p')%R hy).
Hypothesis B4: (Closest b radix (y-hy)%R ty).

Hypothesis C1: (Closest b radix (hx×hy)%R x1y1).
Hypothesis C2: (Closest b radix (hx×ty)%R x1y2).
Hypothesis C3: (Closest b radix (tx×hy)%R x2y1).
Hypothesis C4: (Closest b radix (tx×ty)%R x2y2).

Hypothesis D1: (Closest b radix (x×y)%R r).
Hypothesis D2: (Closest b radix (r-x1y1)%R t1).
Hypothesis D3: (Closest b radix (t1-x1y2)%R t2).
Hypothesis D4: (Closest b radix (t2-x2y1)%R t3).
Hypothesis D5: (Closest b radix (t3-x2y2)%R t4).

Hypothesis dExpPos: ¬(Z_of_N(dExp b)=0)%Z.

Theorem Dekker1: (radix=2)%Z ∨ (Nat.Even t) → (x×y=r-t4)%R.

End Algo1.
Section Algo2.

Variable radix : Z.
Variable b : Fbound.
Variables t: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 pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypotheses pGe: (4 ≤ t).
Let s:= t- Nat.div2 t.

Variables x y:float.

Let b' := Bound (vNum b) (Nplus (N.double (dExp b)) (N.double (Npos (P_of_succ_nat t)))).

Theorem Veltkampb': ∀ (f pf qf hf tf:float),
  (dExp b < dExp b')%Z →
  (Fbounded b f) →
  Closest b radix (f × (powerRZ radix s + 1)) pf → Closest b radix (f - pf) qf →
  Closest b radix (qf + pf) hf → Closest b radix (f - hf) tf →
  Closest b' radix (f × (powerRZ radix s + 1)) pf ∧
  Closest b' radix (f - pf) qf ∧ Closest b' radix (qf + pf) hf ∧
  Closest b' radix (f - hf) tf.

Variables p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 r t1 t2 t3 t4:float.

Hypothesis Cx: (Fcanonic radix b x).
Hypothesis Cy: (Fcanonic radix b y).

Hypothesis Expoxy: (Fexp x+Fexp y < -dExp b)%Z.

Hypothesis A1: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis A2: (Closest b radix (x-p)%R q).
Hypothesis A3: (Closest b radix (q+p)%R hx).
Hypothesis A4: (Closest b radix (x-hx)%R tx).

Hypothesis B1: (Closest b radix (y*((powerRZ radix s)+1))%R p').
Hypothesis B2: (Closest b radix (y-p')%R q').
Hypothesis B3: (Closest b radix (q'+p')%R hy).
Hypothesis B4: (Closest b radix (y-hy)%R ty).

Hypothesis C1: (Closest b radix (hx×hy)%R x1y1).
Hypothesis C2: (Closest b radix (hx×ty)%R x1y2).
Hypothesis C3: (Closest b radix (tx×hy)%R x2y1).
Hypothesis C4: (Closest b radix (tx×ty)%R x2y2).

Hypothesis D1: (Closest b radix (x×y)%R r).
Hypothesis D2: (Closest b radix (r-x1y1)%R t1).
Hypothesis D3: (Closest b radix (t1-x1y2)%R t2).
Hypothesis D4: (Closest b radix (t2-x2y1)%R t3).
Hypothesis D5: (Closest b radix (t3-x2y2)%R t4).

Theorem dExpPrim: (dExp b < dExp b')%Z.

Theorem dExpPrimEq: (Z_of_N (N.double (dExp b) + Npos (xO (P_of_succ_nat t)))
   =2*(dExp b)+2×t+2)%Z.

Theorem NormalbPrim: ∀ (f:float), Fcanonic radix b f → (FtoRradix f ≠0) →
   (∃ f':float, (Fnormal radix b' f') ∧ FtoRradix f'=f ∧ (-t-dExp b ≤ Fexp f')%Z).

Theorem Dekker2_aux:
  (FtoRradix x ≠0) → (FtoRradix y ≠0) →
  (radix=2)%Z ∨ (Nat.Even t) → (Rabs (x×y-(r-t4)) ≤ (7/2)*powerRZ radix (-(dExp b)))%R.

Theorem Dekker2:
  (radix=2)%Z ∨ (Nat.Even t) → (Rabs (x×y-(r-t4)) ≤ (7/2)*powerRZ radix (-(dExp b)))%R.

End Algo2.

Section AlgoT.

Variable radix : Z.
Variable b : Fbound.
Variables t: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 pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypotheses pGe: (4 ≤ t).

Variables x y p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 r t1 t2 t3 t4:float.

Hypothesis Cx: (Fcanonic radix b x).
Hypothesis Cy: (Fcanonic radix b y).

Let s:= t- Nat.div2 t.

Hypothesis A1: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis A2: (Closest b radix (x-p)%R q).
Hypothesis A3: (Closest b radix (q+p)%R hx).
Hypothesis A4: (Closest b radix (x-hx)%R tx).

Hypothesis B1: (Closest b radix (y*((powerRZ radix s)+1))%R p').
Hypothesis B2: (Closest b radix (y-p')%R q').
Hypothesis B3: (Closest b radix (q'+p')%R hy).
Hypothesis B4: (Closest b radix (y-hy)%R ty).

Hypothesis C1: (Closest b radix (hx×hy)%R x1y1).
Hypothesis C2: (Closest b radix (hx×ty)%R x1y2).
Hypothesis C3: (Closest b radix (tx×hy)%R x2y1).
Hypothesis C4: (Closest b radix (tx×ty)%R x2y2).

Hypothesis D1: (Closest b radix (x×y)%R r).
Hypothesis D2: (Closest b radix (-r+x1y1)%R t1).
Hypothesis D3: (Closest b radix (t1+x1y2)%R t2).
Hypothesis D4: (Closest b radix (t2+x2y1)%R t3).
Hypothesis D5: (Closest b radix (t3+x2y2)%R t4).

Hypothesis dExpPos: ¬(Z_of_N (dExp b)=0)%Z.

Theorem Dekker: (radix=2)%Z ∨ (Nat.Even t) →
  ((-dExp b ≤ Fexp x+Fexp y)%Z → (x×y=r+t4)%R) ∧
    (Rabs (x×y-(r+t4)) ≤ (7/2)*powerRZ radix (-(dExp b)))%R.

End AlgoT.