Commit 02047e05 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Comments again

parent 69e7e659
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Necessary conditions to compute a*x+y faithfully *)
Require Import Fcore.
Section Axpy.
......@@ -26,12 +28,41 @@ Notation bpow e := (bpow beta e).
Variable prec : Z.
Variable Hp : Zlt 0 prec.
(* FLX ou FLT ou aussi FTZ ou ? *)
(* FLX first - probably correct in FLTand maybe FTZ? *)
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
Notation ulp := (ulp beta (FLX_exp prec)).
Theorem pred_gt_0: forall f,
format f -> (0 < f)%R -> (0 < pred beta (FLX_exp prec) f)%R.
intros f Hf Zf.
unfold pred, Fcore_ulp.ulp, canonic_exponent, FLX_exp.
destruct (ln_beta beta f) as (ef,Hef).
simpl.
assert (Zf2: (f <>0)%R) by now apply Rgt_not_eq.
specialize (Hef Zf2).
rewrite Rabs_right in Hef.
2: now apply Rgt_ge.
case (Zle_lt_or_eq 1 prec).
omega.
intros Hp1.
case Req_bool_spec; intros H; apply Rlt_Rminus;
apply Rlt_le_trans with (2:=proj1 Hef);
apply ->bpow_lt; omega.
(* special case for p = 1 *)
intros Hp1.
case Req_bool_spec; intros H; apply Rlt_Rminus.
apply Rlt_le_trans with (2:=proj1 Hef).
apply ->bpow_lt; omega.
rewrite <- Hp1.
case (proj1 Hef); trivial.
intros H'.
now contradict H.
Qed.
Definition MinOrMax x f :=
((f = round beta (FLX_exp prec) rndDN x)
\/ (f = round beta (FLX_exp prec) rndUP x)).
......@@ -67,13 +98,12 @@ rewrite Rabs_left1; trivial.
now apply Rle_minus.
Qed.
Theorem implies_MinOrMax_not_bpow:
Theorem MinOrMax_ulp_pred:
forall x f, format f ->
(0 < f)%R ->
f <> bpow (ln_beta beta f) ->
(Rabs (f-x) < ulp f)%R ->
(Rabs (f-x) < ulp (pred beta (FLX_exp prec) f))%R ->
MinOrMax x f.
intros x f Hf1 Hf2 Hf3 Hxf1.
intros x f Ff Zf Hf.
case (Rlt_or_le x f); intros Hxf2.
(* *)
(* assert (ulp (f-ulp f) = ulp f)%R.
......@@ -96,7 +126,16 @@ now apply Rle_minus.
admit.
(* *)
left.
apply implies_DN_lt_ulp; try split; easy.
apply implies_DN_lt_ulp; trivial.
now split.
apply Rlt_le_trans with (1:=Hf).
apply ulp_monotone.
clear; intros m n H.
unfold FLX_exp.
omega.
now apply pred_gt_0.
left.
apply pred_lt.
Qed.
......@@ -125,7 +164,83 @@ Hypothesis Hy: format y.
Notation t := (round beta (FLX_exp prec) (rndN choice) (a*x)).
Notation u := (round beta (FLX_exp prec) (rndN choice) (t+y)).
(*
Axpy_aux1 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
=> abs(y1-y+a1*x1-a*x) < Fulp(b)(Fpred(b)(u))/4
=> MinOrMax?(y1+a1*x1,u)
Axpy_aux1_aux1 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fnormal?(b)(t) => radix*abs(t) <= Fpred(b)(u)
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
Axpy_aux1_aux2 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fsubnormal?(b)(t) => 1-dExp(b) <= Fexp(Fpred(b)(u))
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
Axpy_aux2 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fsubnormal?(b)(t) => u=t+y
=> abs(y1-y+a1*x1-a*x) < Fulp(b)(Fpred(b)(u))/4
=> MinOrMax?(y1+a1*x1,u)
Axpy_aux3 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fsubnormal?(b)(t)
=> -dExp(b) = Fexp(Fpred(b)(u)) => 1-dExp(b) <= Fexp(u)
=> abs(y1-y+a1*x1-a*x) < Fulp(b)(Fpred(b)(u))/4
=> MinOrMax?(y1+a1*x1,u)
AxpyPos : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> (Fnormal?(b)(t) => radix*abs(t) <= Fpred(b)(u))
=> abs(y1-y+a1*x1-a*x) < Fulp(b)(Fpred(b)(u))/4
=> MinOrMax?(y1+a1*x1,u)
Axpy_opt_aux1_aux1 : lemma Fnormal?(b)(t) => Fnormal?(b)(u) => 0 < u
=> Prec(b) >= 3 =>
(1+radix*(1+1/(2*abs(Fnum(u))))*(1+1/abs(Fnum(Fpred(b)(u)))))/(1-1/(2*abs(Fnum(t))))
<= 1+radix+radix^(4-Prec(b))
Axpy_opt_aux1 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 3 => Fnormal?(b)(t)
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> radix*abs(t) <= Fpred(b)(u)
Axpy_opt_aux2 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 6 => Fnormal?(b)(t)
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y)*radix^(1-Prec(b))/(radix+1) < Fulp(b)(Fpred(b)(u))
Axpy_opt_aux3 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 3 => Fsubnormal?(b)(t)
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y)*radix^(1-Prec(b))/(radix+radix/2) <= Fulp(b)(Fpred(b)(u))
Axpy_optPos : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 6
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y1-y+a1*x1-a*x) < abs(y)*radix^(1-Prec(b))/(6*radix)
=> MinOrMax?(y1+a1*x1,u)
Axpy_optZero : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 = u
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y1-y+a1*x1-a*x) < abs(y)*radix^(1-Prec(b))/(6*radix)
=> MinOrMax?(y1+a1*x1,u)
Axpy_opt : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u)
=> Prec(b) >= 6
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y1-y+a1*x1-a*x) < abs(y)*radix^(1-Prec(b))/(6*radix)
=> MinOrMax?(y1+a1*x1,u)
Axpy_simpl : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u)
=> Prec(b) >= 24 => radix=2
=> (3+1/100000)*abs(a*x) <= abs(y)
=> abs(y1-y+a1*x1-a*x) < abs(y)*2^(1-Prec(b))/12
=> MinOrMax?(y1+a1*x1,u)
*)
Theorem Axpy_opt :
(6 <= prec)%Z ->
......
......@@ -33,7 +33,7 @@ Variable beta : radix.
Definition F2R (f : float beta) :=
(Z2R (Fnum f) * bpow beta (Fexp f))%R.
(** Requirements on a rounding mode property *)
(** Requirements on a rounding mode *)
Definition MonotoneP (rnd : R -> R) :=
forall x y : R,
(x <= y)%R -> (rnd x <= rnd y)%R.
......
......@@ -1282,7 +1282,7 @@ apply Rle_lt_trans with (2 := H).
now apply H3.
Qed.
(* ensures a real number can always be rounded *)
(** ensures a real number can always be rounded *)
Inductive satisfies_any (F : R -> Prop) :=
Satisfies_any :
F 0 -> ( forall x : R, F x -> F (-x) ) ->
......
......@@ -17,7 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Unit in the Last Place: our definition using fexp and its properties *)
(** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment