Theory "lift_ieee"

Signature

Definitions

error_def

⊢ ∀x. error (:τ # χ) x = float_to_real (round roundTiesToEven x) − x

normalizes_def

⊢ ∀x.
      normalizes (:τ # χ) x ⇔
      1 < INT_MAX (:χ) ∧ (2 pow (INT_MAX (:χ) − 1))⁻¹ ≤ abs x ∧
      abs x < threshold (:τ # χ)

Theorems

float_lt

⊢ ∀x y.
      float_is_finite x ∧ float_is_finite y ⇒
      (float_less_than x y ⇔ float_to_real x < float_to_real y)

float_le

⊢ ∀x y.
      float_is_finite x ∧ float_is_finite y ⇒
      (float_less_equal x y ⇔ float_to_real x ≤ float_to_real y)

float_gt

⊢ ∀x y.
      float_is_finite x ∧ float_is_finite y ⇒
      (float_greater_than x y ⇔ float_to_real x > float_to_real y)

float_ge

⊢ ∀x y.
      float_is_finite x ∧ float_is_finite y ⇒
      (float_greater_equal x y ⇔ float_to_real x ≥ float_to_real y)

float_eq

⊢ ∀x y.
      float_is_finite x ∧ float_is_finite y ⇒
      (float_equal x y ⇔ float_to_real x = float_to_real y)

float_eq_refl

⊢ ∀x. float_equal x x ⇔ ¬float_is_nan x

is_closest_exits

⊢ ∀x s. FINITE s ⇒ s ≠ ∅ ⇒ ∃a. is_closest s x a

closest_is_everything

⊢ ∀p s x.
      FINITE s ⇒
      s ≠ ∅ ⇒
      is_closest s x (closest_such p s x) ∧
      ((∃b. is_closest s x b ∧ p b) ⇒ p (closest_such p s x))

closest_in_set

⊢ ∀p s x. FINITE s ⇒ s ≠ ∅ ⇒ closest_such p s x ∈ s

closest_is_closest

⊢ ∀p s x. FINITE s ⇒ s ≠ ∅ ⇒ is_closest s x (closest_such p s x)

float_finite

⊢ FINITE 𝕌(:(τ, χ) float)

is_finite_finite

⊢ FINITE {a | float_is_finite a}

is_finite_nonempty

⊢ {a | float_is_finite a} ≠ ∅

is_finite_closest

⊢ ∀p x. float_is_finite (closest_such p {a | float_is_finite a} x)

float_to_real_finite

⊢ ∀x. float_is_finite x ⇒ abs (float_to_real x) ≤ largest (:τ # χ)

float_to_real_threshold

⊢ ∀x. float_is_finite x ⇒ abs (float_to_real x) < threshold (:τ # χ)

error_at_worst_lemma

⊢ ∀a x.
      abs x < threshold (:τ # χ) ∧ float_is_finite a ⇒
      abs (error (:τ # χ) x) ≤ abs (float_to_real a − x)

error_is_zero

⊢ ∀a x. float_is_finite a ∧ float_to_real a = x ⇒ error (:τ # χ) x = 0

relative_error

⊢ ∀x.
      normalizes (:τ # χ) x ⇒
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (round roundTiesToEven x) = x * (1 + e)

float_round_finite

⊢ ∀b x.
      abs x < threshold (:τ # χ) ⇒
      float_is_finite (float_round roundTiesToEven b x)

float_add

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      abs (float_to_real a + float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_add a) b)) ∧
      float_to_real (SND ((roundTiesToEven float_add a) b)) =
      float_to_real a + float_to_real b +
      error (:τ # χ) (float_to_real a + float_to_real b)

float_sub

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      abs (float_to_real a − float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_sub a) b)) ∧
      float_to_real (SND ((roundTiesToEven float_sub a) b)) =
      float_to_real a − float_to_real b +
      error (:τ # χ) (float_to_real a − float_to_real b)

float_mul

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      abs (float_to_real a * float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_mul a) b)) ∧
      float_to_real (SND ((roundTiesToEven float_mul a) b)) =
      float_to_real a * float_to_real b +
      error (:τ # χ) (float_to_real a * float_to_real b)

float_div

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
      abs (float_to_real a / float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_div a) b)) ∧
      float_to_real (SND ((roundTiesToEven float_div a) b)) =
      float_to_real a / float_to_real b +
      error (:τ # χ) (float_to_real a / float_to_real b)

float_sqrt

⊢ ∀a.
      float_is_finite a ∧ a.Sign = 0w ∧
      abs (sqrt (float_to_real a)) < threshold (:τ # χ) ⇒
      float_is_finite (SND (float_sqrt roundTiesToEven a)) ∧
      float_to_real (SND (float_sqrt roundTiesToEven a)) =
      sqrt (float_to_real a) + error (:τ # χ) (sqrt (float_to_real a))

float_mul_add

⊢ ∀a b c.
      float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
      abs (float_to_real a * float_to_real b − float_to_real c) <
      threshold (:τ # χ) ⇒
      float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
      float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
      float_to_real a * float_to_real b − float_to_real c +
      error (:τ # χ) (float_to_real a * float_to_real b − float_to_real c)

float_add_finite

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      abs (float_to_real a + float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_add a) b))

float_sub_finite

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      abs (float_to_real a − float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_sub a) b))

float_mul_finite

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      abs (float_to_real a * float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_mul a) b))

float_div_finite

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
      abs (float_to_real a / float_to_real b) < threshold (:τ # χ) ⇒
      float_is_finite (SND ((roundTiesToEven float_div a) b))

float_sqrt_finite

⊢ ∀a.
      float_is_finite a ∧ a.Sign = 0w ∧
      abs (sqrt (float_to_real a)) < threshold (:τ # χ) ⇒
      float_is_finite (SND (float_sqrt roundTiesToEven a))

float_mul_add_finite

⊢ ∀a b c.
      float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
      abs (float_to_real a * float_to_real b + float_to_real c) <
      threshold (:τ # χ) ⇒
      float_is_finite (SND (float_mul_add roundTiesToEven a b c))

float_mul_sub_finite

⊢ ∀a b c.
      float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
      abs (float_to_real a * float_to_real b − float_to_real c) <
      threshold (:τ # χ) ⇒
      float_is_finite (SND (float_mul_sub roundTiesToEven a b c))

float_add_relative

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      normalizes (:τ # χ) (float_to_real a + float_to_real b) ⇒
      float_is_finite (SND ((roundTiesToEven float_add a) b)) ∧
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (SND ((roundTiesToEven float_add a) b)) =
          (float_to_real a + float_to_real b) * (1 + e)

float_sub_relative

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      normalizes (:τ # χ) (float_to_real a − float_to_real b) ⇒
      float_is_finite (SND ((roundTiesToEven float_sub a) b)) ∧
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (SND ((roundTiesToEven float_sub a) b)) =
          (float_to_real a − float_to_real b) * (1 + e)

float_mul_relative

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧
      normalizes (:τ # χ) (float_to_real a * float_to_real b) ⇒
      float_is_finite (SND ((roundTiesToEven float_mul a) b)) ∧
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (SND ((roundTiesToEven float_mul a) b)) =
          float_to_real a * float_to_real b * (1 + e)

float_div_relative

⊢ ∀a b.
      float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
      normalizes (:τ # χ) (float_to_real a / float_to_real b) ⇒
      float_is_finite (SND ((roundTiesToEven float_div a) b)) ∧
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (SND ((roundTiesToEven float_div a) b)) =
          float_to_real a / float_to_real b * (1 + e)

float_sqrt_relative

⊢ ∀a.
      float_is_finite a ∧ a.Sign = 0w ∧
      normalizes (:τ # χ) (sqrt (float_to_real a)) ⇒
      float_is_finite (SND (float_sqrt roundTiesToEven a)) ∧
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (SND (float_sqrt roundTiesToEven a)) =
          sqrt (float_to_real a) * (1 + e)

float_mul_add_relative

⊢ ∀a b c.
      float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
      normalizes (:τ # χ)
        (float_to_real a * float_to_real b + float_to_real c) ⇒
      float_is_finite (SND (float_mul_add roundTiesToEven a b c)) ∧
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
          (float_to_real a * float_to_real b + float_to_real c) * (1 + e)

float_mul_sub_relative

⊢ ∀a b c.
      float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
      normalizes (:τ # χ)
        (float_to_real a * float_to_real b − float_to_real c) ⇒
      float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
      ∃e.
          abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
          (float_to_real a * float_to_real b − float_to_real c) * (1 + e)

finite_float_within_threshold

⊢ ∀f.
      float_is_finite f ⇒
      ¬(float_to_real f ≤ -threshold (:α # β)) ∧
      ¬(float_to_real f ≥ threshold (:α # β))

round_finite_normal_float_id

⊢ ∀f.
      float_is_finite f ∧ float_is_normal f ∧ ¬float_is_zero f ⇒
      round roundTiesToEven (float_to_real f) = f

real_to_float_finite_normal_id

⊢ ∀f.
      float_is_finite f ∧ float_is_normal f ∧ ¬float_is_zero f ⇒
      real_to_float roundTiesToEven (float_to_real f) = f

float_to_real_real_to_float_zero_id

⊢ float_to_real (real_to_float roundTiesToEven 0) = 0

non_representable_float_is_zero

⊢ ∀ff P.
      2 * abs ff ≤ ulp (:α # β) ⇒
      float_to_real (float_round roundTiesToEven P ff) = 0