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

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)

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

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)

finite_float_within_threshold

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

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_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_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_add_relative_denorm

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

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_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_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_div_relative_denorm

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

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

float_finite

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

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_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_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_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_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_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_add roundTiesToEven a b c)) ∧
    (float_to_real (SND (float_mul_add 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_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_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_add_relative_denorm

⊢ ∀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) <
    2 pow 1 / 2 pow (INT_MAX (:χ) − 1) ∧
    abs (float_to_real a * float_to_real b + float_to_real c) <
    threshold (:τ # χ) ∧ 1 < INT_MAX (:χ) ⇒
    float_is_finite (SND (float_mul_add roundTiesToEven a b c)) ∧
    ∃e. abs e ≤ 1 / 2 pow (INT_MAX (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
         float_to_real a * float_to_real b + float_to_real c + e)

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_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_mul_relative_denorm

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

float_mul_sub

⊢ ∀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_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_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))

float_mul_sub_relative_denorm

⊢ ∀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) <
    2 pow 1 / 2 pow (INT_MAX (:χ) − 1) ∧
    abs (float_to_real a * float_to_real b − float_to_real c) <
    threshold (:τ # χ) ∧ 1 < INT_MAX (:χ) ⇒
    float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
    ∃e. abs e ≤ 1 / 2 pow (INT_MAX (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
         float_to_real a * float_to_real b − float_to_real c + e)

float_round_finite

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

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_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_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_sqrt_relative_denorm

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

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_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_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_sub_relative_denorm

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

float_to_real_finite

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

float_to_real_real_to_float_zero_id

⊢ float_to_real (real_to_float roundTiesToEven 0) = 0

float_to_real_threshold

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

is_closest_exits

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

is_finite_closest

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

is_finite_finite

⊢ FINITE {a | float_is_finite a}

is_finite_nonempty

⊢ {a | float_is_finite a} ≠ ∅

non_representable_float_is_zero

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

real_to_float_finite_normal_id

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

relative_error

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

round_finite_normal_float_id

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