FIX.v

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE. Section RND_FIX. Variable beta : radix. Notation bpow := (bpow beta). Variable emin : Z. Inductive FIX_format (x : R) : Prop := FIX_spec (f : float beta) : x = F2R f -> (Fexp f = emin)%Z -> FIX_format x. Definition FIX_exp (e : Z) := emin.

Instance FIX_exp_valid : Valid_exp FIX_exp.

beta:radix
emin:Z
Valid_exp FIX_exp

Proof.

beta:radix
emin:Z
Valid_exp FIX_exp

intros k.

beta:radix
emin, k:Z
((FIX_exp k < k)%Z -> (FIX_exp (k + 1) <= k)%Z) /\ ((k <= FIX_exp k)%Z -> (FIX_exp (FIX_exp k + 1) <= FIX_exp k)%Z /\ (forall l : Z, (l <= FIX_exp k)%Z -> FIX_exp l = FIX_exp k))

unfold FIX_exp.

beta:radix
emin, k:Z
((emin < k)%Z -> (emin <= k)%Z) /\ ((k <= emin)%Z -> (emin <= emin)%Z /\ (forall l : Z, (l <= emin)%Z -> emin = emin))

split ; intros H.

beta:radix
emin, k:Z
H:(emin < k)%Z
(emin <= k)%Z

beta:radix
emin, k:Z
H:(k <= emin)%Z
(emin <= emin)%Z /\ (forall l : Z, (l <= emin)%Z -> emin = emin)

now apply Zlt_le_weak.

beta:radix
emin, k:Z
H:(k <= emin)%Z
(emin <= emin)%Z /\ (forall l : Z, (l <= emin)%Z -> emin = emin)

split.

beta:radix
emin, k:Z
H:(k <= emin)%Z
(emin <= emin)%Z

beta:radix
emin, k:Z
H:(k <= emin)%Z
forall l : Z, (l <= emin)%Z -> emin = emin

apply Z.le_refl.

beta:radix
emin, k:Z
H:(k <= emin)%Z
forall l : Z, (l <= emin)%Z -> emin = emin

now intros _ _. Qed. Theorem generic_format_FIX : forall x, FIX_format x -> generic_format beta FIX_exp x.

beta:radix
emin:Z
forall x : R, FIX_format x -> generic_format beta FIX_exp x

Proof.

beta:radix
emin:Z
forall x : R, FIX_format x -> generic_format beta FIX_exp x

intros x [[xm xe] Hx1 Hx2].

beta:radix
emin:Z
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:Fexp {| Fnum := xm; Fexp := xe |} = emin
generic_format beta FIX_exp x

rewrite Hx1.

beta:radix
emin:Z
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:Fexp {| Fnum := xm; Fexp := xe |} = emin
generic_format beta FIX_exp (F2R {| Fnum := xm; Fexp := xe |})

now apply generic_format_canonical. Qed. Theorem FIX_format_generic : forall x, generic_format beta FIX_exp x -> FIX_format x.

beta:radix
emin:Z
forall x : R, generic_format beta FIX_exp x -> FIX_format x

Proof.

beta:radix
emin:Z
forall x : R, generic_format beta FIX_exp x -> FIX_format x

intros x H.

beta:radix
emin:Z
x:R
H:generic_format beta FIX_exp x
FIX_format x

rewrite H.

beta:radix
emin:Z
x:R
H:generic_format beta FIX_exp x
FIX_format (F2R {| Fnum := Ztrunc (scaled_mantissa beta FIX_exp x); Fexp := cexp beta FIX_exp x |})

eexists ; repeat split. Qed. Theorem FIX_format_satisfies_any : satisfies_any FIX_format.

beta:radix
emin:Z
satisfies_any FIX_format

Proof.

beta:radix
emin:Z
satisfies_any FIX_format

refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)).

beta:radix
emin:Z
forall x : R, generic_format beta FIX_exp x <-> FIX_format x

intros x.

beta:radix
emin:Z
x:R
generic_format beta FIX_exp x <-> FIX_format x

split.

beta:radix
emin:Z
x:R
generic_format beta FIX_exp x -> FIX_format x

beta:radix
emin:Z
x:R
FIX_format x -> generic_format beta FIX_exp x

apply FIX_format_generic.

beta:radix
emin:Z
x:R
FIX_format x -> generic_format beta FIX_exp x

apply generic_format_FIX. Qed. Instance FIX_exp_monotone : Monotone_exp FIX_exp.

beta:radix
emin:Z
Monotone_exp FIX_exp

Proof.

beta:radix
emin:Z
Monotone_exp FIX_exp

intros ex ey H.

beta:radix
emin, ex, ey:Z
H:(ex <= ey)%Z
(FIX_exp ex <= FIX_exp ey)%Z

apply Z.le_refl. Qed. Theorem ulp_FIX : forall x, ulp beta FIX_exp x = bpow emin.

beta:radix
emin:Z
forall x : R, ulp beta FIX_exp x = bpow emin

Proof.

beta:radix
emin:Z
forall x : R, ulp beta FIX_exp x = bpow emin

intros x; unfold ulp.

beta:radix
emin:Z
x:R
(if Req_bool x 0 then match negligible_exp FIX_exp with | Some n => bpow (FIX_exp n) | None => 0%R end else bpow (cexp beta FIX_exp x)) = bpow emin

case Req_bool_spec; intros Zx.

beta:radix
emin:Z
x:R
Zx:x = 0%R
match negligible_exp FIX_exp with | Some n => bpow (FIX_exp n) | None => 0%R end = bpow emin

beta:radix
emin:Z
x:R
Zx:x <> 0%R
bpow (cexp beta FIX_exp x) = bpow emin

case (negligible_exp_spec FIX_exp).

beta:radix
emin:Z
x:R
Zx:x = 0%R
(forall n : Z, (FIX_exp n < n)%Z) -> 0%R = bpow emin

beta:radix
emin:Z
x:R
Zx:x = 0%R
forall n : Z, (n <= FIX_exp n)%Z -> bpow (FIX_exp n) = bpow emin

beta:radix
emin:Z
x:R
Zx:x <> 0%R
bpow (cexp beta FIX_exp x) = bpow emin

intros T; specialize (T (emin-1)%Z); contradict T.

beta:radix
emin:Z
x:R
Zx:x = 0%R
~ (FIX_exp (emin - 1) < emin - 1)%Z

beta:radix
emin:Z
x:R
Zx:x = 0%R
forall n : Z, (n <= FIX_exp n)%Z -> bpow (FIX_exp n) = bpow emin

beta:radix
emin:Z
x:R
Zx:x <> 0%R
bpow (cexp beta FIX_exp x) = bpow emin

unfold FIX_exp; omega.

beta:radix
emin:Z
x:R
Zx:x = 0%R
forall n : Z, (n <= FIX_exp n)%Z -> bpow (FIX_exp n) = bpow emin

beta:radix
emin:Z
x:R
Zx:x <> 0%R
bpow (cexp beta FIX_exp x) = bpow emin

intros n _; reflexivity.

beta:radix
emin:Z
x:R
Zx:x <> 0%R
bpow (cexp beta FIX_exp x) = bpow emin

reflexivity. Qed. Instance exists_NE_FIX : Exists_NE beta FIX_exp.

beta:radix
emin:Z
Exists_NE beta FIX_exp

Proof.

beta:radix
emin:Z
Exists_NE beta FIX_exp

unfold Exists_NE, FIX_exp; simpl.

beta:radix
emin:Z
Z.even beta = false \/ (forall e : Z, ((emin < e)%Z -> (emin < e)%Z) /\ ((e <= emin)%Z -> emin = emin))

right; split; auto. Qed. End RND_FIX.

Fixed-point format