Commit 3e01dd65 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Mark the radix argument of operations as implicit.

parent 80196ef0
......@@ -34,7 +34,7 @@ now apply F2R_ge_0.
Qed.
Definition plus (x y : float beta) :=
let (m, e) := Fplus beta x y in
let (m, e) := Fplus x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
......@@ -46,7 +46,7 @@ Proof.
intros x y.
unfold plus.
rewrite <- F2R_plus.
destruct (Fplus beta x y) as [m e].
destruct (Fplus x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
......@@ -57,7 +57,7 @@ apply sym_eq, F2R_Zabs.
Qed.
Definition mult (x y : float beta) :=
let (m, e) := Fmult beta x y in
let (m, e) := Fmult x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
......@@ -69,7 +69,7 @@ Proof.
intros x y.
unfold mult.
rewrite <- F2R_mult.
destruct (Fmult beta x y) as [m e].
destruct (Fmult x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
......@@ -81,7 +81,7 @@ Qed.
Definition sqrt (x : float beta) :=
if Zlt_bool 0 (Fnum x) then
let '(m', e', l) := truncate beta fexp (Fsqrt beta fexp x) in
let '(m', e', l) := truncate beta fexp (Fsqrt fexp x) in
Float beta (choice false m' l) e'
else Float beta 0 0.
......@@ -92,7 +92,7 @@ Proof.
intros x.
unfold sqrt.
case Zlt_bool_spec ; intros Hm.
generalize (Fsqrt_correct beta fexp x (F2R_gt_0 _ _ Hm)).
generalize (Fsqrt_correct fexp x (F2R_gt_0 _ _ Hm)).
destruct Fsqrt as [[m' e'] l].
intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m' e' l).
......@@ -160,7 +160,7 @@ Qed.
Definition div (x y : float beta) :=
if Zeq_bool (Fnum x) 0 then Float beta 0 0
else
let '(m, e, l) := truncate beta fexp (Fdiv beta fexp (Fabs _ x) (Fabs _ y)) in
let '(m, e, l) := truncate beta fexp (Fdiv fexp (Fabs x) (Fabs y)) in
let s := xorb (Zlt_bool (Fnum x) 0) (Zlt_bool (Fnum y) 0) in
Float beta (cond_Zopp s (choice s m l)) e.
......@@ -178,16 +178,16 @@ case Zeq_bool_spec ; intros Hm.
unfold Rdiv.
rewrite Rmult_0_l.
now apply round_0.
assert (0 < F2R (Fabs _ x))%R as Hx.
assert (0 < F2R (Fabs x))%R as Hx.
destruct x as [mx ex].
now apply F2R_gt_0, Z.abs_pos.
assert (0 < F2R (Fabs _ y))%R as Hy'.
assert (0 < F2R (Fabs y))%R as Hy'.
destruct y as [my ey].
apply F2R_gt_0, Z.abs_pos.
contradict Hy.
rewrite Hy.
apply F2R_0.
generalize (Fdiv_correct beta fexp (Fabs _ x) (Fabs _ y) Hx Hy').
generalize (Fdiv_correct fexp _ _ Hx Hy').
destruct Fdiv as [[m e] l].
intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m e l).
......
......@@ -63,7 +63,7 @@ Lemma hombnd_plus :
forall m M u1 v1 b1 B1 u2 v2 b2 B2,
hombnd m M u1 v1 b1 B1 ->
hombnd m M u2 v2 b2 B2 ->
hombnd m M (u1 + u2) (v1 + v2) (Fplus radix2 b1 b2) (Fplus radix2 B1 B2).
hombnd m M (u1 + u2) (v1 + v2) (Fplus b1 b2) (Fplus B1 B2).
Proof.
intros m M u1 v1 b1 B1 u2 v2 b2 B2 [H11 [H12 H1]] [H21 [H22 H2]].
unfold hombnd.
......@@ -87,7 +87,7 @@ Lemma hombnd_minus :
forall m M u1 v1 b1 B1 u2 v2 b2 B2,
hombnd m M u1 v1 b1 B1 ->
hombnd m M u2 v2 b2 B2 ->
hombnd m M (u1 - u2) (v1 - v2) (Fplus radix2 b1 b2) (Fplus radix2 B1 B2).
hombnd m M (u1 - u2) (v1 - v2) (Fplus b1 b2) (Fplus B1 B2).
Proof.
intros m M u1 v1 b1 B1 u2 v2 b2 B2 H1 [H21 [H22 H2]].
apply hombnd_plus with (1 := H1).
......@@ -100,13 +100,13 @@ now split.
Qed.
Definition mult_err b1 B1 b2 B2 :=
Fplus radix2 (Fplus radix2 (Fmult radix2 b1 B2) (Fmult radix2 B1 b2)) (Fmult radix2 b1 b2).
Fplus (Fplus (Fmult b1 B2) (Fmult B1 b2)) (@Fmult radix2 b1 b2).
Lemma hombnd_mult :
forall m M1 u1 v1 b1 B1 M2 u2 v2 b2 B2,
hombnd m M1 u1 v1 b1 B1 ->
hombnd m M2 u2 v2 b2 B2 ->
hombnd m (M1 * M2) (u1 * u2) (v1 * v2) (mult_err b1 B1 b2 B2) (Fmult radix2 B1 B2).
hombnd m (M1 * M2) (u1 * u2) (v1 * v2) (mult_err b1 B1 b2 B2) (Fmult B1 B2).
Proof.
intros m M1 u1 v1 b1 B1 M2 u2 v2 b2 B2 [H11 [H12 H1]] [H21 [H22 H2]].
unfold hombnd, mult_err.
......@@ -147,7 +147,7 @@ now apply Rmult_le_compat ; try apply Rabs_pos.
Qed.
Definition round_err b B :=
Fplus radix2 (Fmult radix2 (Fplus radix2 b B) (Float radix2 1 (- prec))) b.
Fplus (Fmult (Fplus b B) (Float radix2 1 (- prec))) b.
Lemma hombnd_rnd :
forall m M u v b B,
......@@ -278,7 +278,7 @@ Lemma hombnd_add :
forall {m M u1 v1 b1 B1 u2 v2 b2 B2},
hombnd' m M u1 v1 b1 B1 ->
hombnd' m M u2 v2 b2 B2 ->
hombnd' m M (u1 + u2) (v1 + v2) (Fplus radix2 b1 b2) (Fplus radix2 B1 B2).
hombnd' m M (u1 + u2) (v1 + v2) (Fplus b1 b2) (Fplus B1 B2).
Proof.
apply hombnd_plus.
Qed.
......@@ -287,7 +287,7 @@ Lemma hombnd_sub :
forall {m M u1 v1 b1 B1 u2 v2 b2 B2},
hombnd' m M u1 v1 b1 B1 ->
hombnd' m M u2 v2 b2 B2 ->
hombnd' m M (u1 - u2) (v1 - v2) (Fplus radix2 b1 b2) (Fplus radix2 B1 B2).
hombnd' m M (u1 - u2) (v1 - v2) (Fplus b1 b2) (Fplus B1 B2).
Proof.
apply hombnd_minus.
Qed.
......@@ -296,7 +296,7 @@ Lemma hombnd_mul :
forall {m M1 u1 v1 b1 B1 M2 u2 v2 b2 B2},
hombnd' m M1 u1 v1 b1 B1 ->
hombnd' m M2 u2 v2 b2 B2 ->
hombnd' m (M1 * M2) (u1 * u2) (v1 * v2) (mult_err b1 B1 b2 B2) (Fmult radix2 B1 B2).
hombnd' m (M1 * M2) (u1 * u2) (v1 * v2) (mult_err b1 B1 b2 B2) (Fmult B1 B2).
Proof.
apply hombnd_mult.
Qed.
......
......@@ -21,6 +21,9 @@ COPYING file for more details.
Require Import Raux Defs Generic_fmt Float_prop Digits Bracket.
Set Implicit Arguments.
Set Strongly Strict Implicit.
Section Fcalc_div.
Variable beta : radix.
......
......@@ -20,6 +20,9 @@ COPYING file for more details.
(** Basic operations on floats: alignment, addition, multiplication *)
Require Import Raux Defs Float_prop.
Set Implicit Arguments.
Set Strongly Strict Implicit.
Section Float_ops.
Variable beta : radix.
......
......@@ -21,6 +21,9 @@ COPYING file for more details.
Require Import Raux Defs Digits Generic_fmt Float_prop Bracket.
Set Implicit Arguments.
Set Strongly Strict Implicit.
Section Fcalc_sqrt.
Variable beta : radix.
......
......@@ -42,7 +42,7 @@ rewrite H; apply generic_format_0.
rewrite Hx, Hy, <- F2R_plus.
apply generic_format_F2R.
intros _.
case_eq (Fplus beta fx fy).
case_eq (Fplus fx fy).
intros mz ez Hz.
rewrite <- Hz.
apply Zle_trans with (Zmin (Fexp fx) (Fexp fy)).
......@@ -84,7 +84,7 @@ destruct (canonical_generic_format _ _ x Hx) as (fx,(Hx1,Hx2)).
destruct (canonical_generic_format _ _ y Hy) as (fy,(Hy1,Hy2)).
destruct (canonical_generic_format beta (FLX_exp prec) (round beta (FLX_exp prec) rnd (x / y))) as (fr,(Hr1,Hr2)).
apply generic_format_round...
unfold Rminus; apply generic_format_plus_prec with fx (Fopp beta (Fmult beta fr fy)); trivial.
unfold Rminus; apply generic_format_plus_prec with fx (Fopp (Fmult fr fy)); trivial.
intros e; apply Zle_refl.
now rewrite F2R_opp, F2R_mult, <- Hr1, <- Hy1.
(* *)
......@@ -114,7 +114,7 @@ unfold FLX_exp.
ring_simplify.
apply Zle_refl.
(* *)
replace (Fexp (Fopp beta (Fmult beta fr fy))) with (Fexp fr + Fexp fy)%Z.
replace (Fexp (Fopp (Fmult fr fy))) with (Fexp fr + Fexp fy)%Z.
2: unfold Fopp, Fmult; destruct fr; destruct fy; now simpl.
replace (x + - (round beta (FLX_exp prec) rnd (x / y) * y))%R with
(y * (-(round beta (FLX_exp prec) rnd (x / y) - x/y)))%R.
......@@ -167,7 +167,7 @@ rewrite Hr; unfold Rsqr; ring_simplify (x-0*0)%R; assumption.
destruct (canonical_generic_format _ _ x Hx) as (fx,(Hx1,Hx2)).
destruct (canonical_generic_format beta (FLX_exp prec) (round beta (FLX_exp prec) (Znearest choice) (sqrt x))) as (fr,(Hr1,Hr2)).
apply generic_format_round...
unfold Rminus; apply generic_format_plus_prec with fx (Fopp beta (Fmult beta fr fr)); trivial.
unfold Rminus; apply generic_format_plus_prec with fx (Fopp (Fmult fr fr)); trivial.
intros e; apply Zle_refl.
unfold Rsqr; now rewrite F2R_opp,F2R_mult, <- Hr1.
(* *)
......@@ -225,7 +225,7 @@ apply a.
now apply Rgt_not_eq.
now apply Rgt_ge.
(* *)
replace (Fexp (Fopp beta (Fmult beta fr fr))) with (Fexp fr + Fexp fr)%Z.
replace (Fexp (Fopp (Fmult fr fr))) with (Fexp fr + Fexp fr)%Z.
2: unfold Fopp, Fmult; destruct fr; now simpl.
rewrite Hr1.
replace (x + - Rsqr (F2R fr))%R with (-((F2R fr - sqrt x)*(F2R fr + sqrt x)))%R.
......
......@@ -251,7 +251,6 @@ simpl; ring.
now apply sym_eq, Z.abs_0_iff, sym_eq.
Qed.
Theorem mult_error_FLT_ge_bpow :
forall x y e,
format x -> format y ->
......@@ -263,7 +262,7 @@ intros x y e.
set (f := (round beta (FLT_exp emin prec) rnd (x * y))).
intros Fx Fy H1.
unfold f; rewrite Fx, Fy, <- F2R_mult.
simpl (Fmult _ _ _).
simpl Fmult.
destruct (round_repr_same_exp beta (FLT_exp emin prec)
rnd (Ztrunc (scaled_mantissa beta (FLT_exp emin prec) x) *
Ztrunc (scaled_mantissa beta (FLT_exp emin prec) y))
......@@ -294,8 +293,4 @@ intros K'; contradict H1; apply Rlt_not_le.
rewrite K', Rmult_0_r, Rabs_R0; apply bpow_gt_0.
Qed.
End Fprop_mult_error_FLT.
......@@ -682,14 +682,16 @@ simpl; now rewrite Fexp_d.
Qed.
Lemma m_eq: (0 < F2R d)%R -> exists f:float beta,
F2R f = m /\ (Fexp f = fexp (mag beta x) -1)%Z.
Lemma m_eq :
(0 < F2R d)%R ->
exists f:float beta,
F2R f = m /\ (Fexp f = fexp (mag beta x) - 1)%Z.
Proof with auto with typeclass_instances.
intros Y.
specialize (Zeven_ex (radix_val beta)); rewrite Even_beta.
intros (b, Hb); rewrite Zplus_0_r in Hb.
destruct u'_eq as (u', (Hu'1,Hu'2)); trivial.
exists (Fmult beta (Float beta b (-1)) (Fplus beta d u'))%R.
exists (Fmult (Float beta b (-1)) (Fplus d u'))%R.
split.
rewrite F2R_mult, F2R_plus, Hu'1.
unfold m; rewrite Rmult_comm.
......@@ -700,9 +702,9 @@ simpl; field.
apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2).
rewrite Rmult_0_r, <- (mult_IZR 2), <-Hb.
apply radix_pos.
apply trans_eq with (-1+Fexp (Fplus beta d u'))%Z.
apply trans_eq with (-1+Fexp (Fplus d u'))%Z.
unfold Fmult.
destruct (Fplus beta d u'); reflexivity.
destruct (Fplus d u'); reflexivity.
rewrite Zplus_comm; unfold Zminus; apply f_equal2.
2: reflexivity.
rewrite Fexp_Fplus.
......@@ -717,7 +719,7 @@ Proof with auto with typeclass_instances.
intros Y.
specialize (Zeven_ex (radix_val beta)); rewrite Even_beta.
intros (b, Hb); rewrite Zplus_0_r in Hb.
exists (Fmult beta (Float beta b (-1)) u)%R.
exists (Fmult (Float beta b (-1)) u)%R.
split.
rewrite F2R_mult; unfold m; rewrite <- Y, Rplus_0_l.
rewrite Rmult_comm.
......
......@@ -66,14 +66,14 @@ rewrite Hx, Hy.
rewrite <- F2R_plus.
apply generic_format_F2R.
intros _.
case_eq (Fplus beta fx fy).
case_eq (Fplus fx fy).
intros mxy exy Pxy.
rewrite <- Pxy, F2R_plus, <- Hx, <- Hy.
unfold cexp.
replace exy with (fexp (Zmin ex ey)).
apply monotone_exp.
now apply mag_le_bpow.
replace exy with (Fexp (Fplus beta fx fy)) by exact (f_equal Fexp Pxy).
replace exy with (Fexp (Fplus fx fy)) by exact (f_equal Fexp Pxy).
rewrite Fexp_Fplus.
simpl. clear -monotone_exp.
apply sym_eq.
......
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