Commit f3c3f037 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Avoided _aux theorems.

parent 4964a0d0
......@@ -32,7 +32,7 @@ Definition Fsqrt_FLT_ne (f : float beta) :=
let '(Float m e) := f in
if Zle_bool m 0 then Float beta 0 0
else
let '(m', e', l) := truncate beta (FLT_exp emin prec) (Fsqrt_aux beta prec m e) in
let '(m', e', l) := truncate beta (FLT_exp emin prec) (Fsqrt_core beta prec m e) in
Float beta (cond_incr (round_NE (Zeven m') l) m') e'.
Theorem Fsqrt_FLT_ne_correct :
......@@ -61,8 +61,8 @@ now apply F2R_lt_0_compat.
rewrite Hm', F2R_0.
now rewrite sqrt_0.
(* 0 < mx *)
generalize (Fsqrt_aux_correct beta prec mx ex (Zgt_lt _ _ Hm)).
destruct (Fsqrt_aux beta prec mx ex) as ((ms, es), ls).
generalize (Fsqrt_core_correct beta prec mx ex (Zgt_lt _ _ Hm)).
destruct (Fsqrt_core beta prec mx ex) as ((ms, es), ls).
intros (H1, H2).
assert (Hp : (0 < prec)%Z) by omega.
generalize (round_trunc_NE_correct beta _ (FLT_exp_correct emin prec Hp) (sqrt (F2R (Float beta mx ex))) ms es ls).
......
......@@ -43,7 +43,7 @@ The algorithm performs the following steps:
Complexity is fine as long as p1 <= 2p and p2 <= p.
*)
Definition Fdiv_aux prec m1 e1 m2 e2 :=
Definition Fdiv_core prec m1 e1 m2 e2 :=
let d1 := digits beta m1 in
let d2 := digits beta m2 in
let e := (e1 - e2)%Z in
......@@ -55,16 +55,16 @@ Definition Fdiv_aux prec m1 e1 m2 e2 :=
let '(q, r) := Zdiv_eucl m m2 in
(q, e', new_location m2 r loc_Exact).
Theorem Fdiv_aux_correct :
Theorem Fdiv_core_correct :
forall prec m1 e1 m2 e2,
(0 < prec)%Z ->
(0 < m1)%Z -> (1 < m2)%Z ->
let '(m, e, l) := Fdiv_aux prec m1 e1 m2 e2 in
let '(m, e, l) := Fdiv_core prec m1 e1 m2 e2 in
(prec <= digits beta m)%Z /\
inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
Proof.
intros prec m1 e1 m2 e2 Hprec Hm1 Hm2.
unfold Fdiv_aux.
unfold Fdiv_core.
set (d1 := digits beta m1).
set (d2 := digits beta m2).
case_eq
......
......@@ -150,7 +150,7 @@ The algorithm performs the following steps:
Complexity is fine as long as p1 <= 2p-1.
*)
Definition Fsqrt_aux prec m e :=
Definition Fsqrt_core prec m e :=
let d := digits beta m in
let s := Zmax (2 * prec - d) 0 in
let e' := (e - s)%Z in
......@@ -166,15 +166,15 @@ Definition Fsqrt_aux prec m e :=
else loc_Inexact (if Zle_bool r q then Lt else Gt) in
(q, Zdiv2 e'', l).
Theorem Fsqrt_aux_correct :
Theorem Fsqrt_core_correct :
forall prec m e,
(0 < m)%Z ->
let '(m', e', l) := Fsqrt_aux prec m e in
let '(m', e', l) := Fsqrt_core prec m e in
(prec <= digits beta m')%Z /\
inbetween_float beta m' e' (sqrt (F2R (Float beta m e))) l.
Proof.
intros prec m e Hm.
unfold Fsqrt_aux.
unfold Fsqrt_core.
set (d := digits beta m).
set (s := Zmax (2 * prec - d) 0).
(* . exponent *)
......
......@@ -63,7 +63,7 @@ Definition DN_UP_parity_prop :=
F2R xu = round beta fexp rndUP x ->
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
Theorem DN_UP_parity_aux :
Lemma DN_UP_parity_aux :
DN_UP_parity_pos_prop ->
DN_UP_parity_prop.
Proof.
......
......@@ -118,7 +118,7 @@ apply Rlt_le.
now apply Rnot_le_lt.
Qed.
Theorem sterbenz_aux :
Lemma sterbenz_aux :
forall x y, format x -> format y ->
(y <= x <= 2 * y)%R ->
format (x - y)%R.
......@@ -168,4 +168,4 @@ now apply Rlt_le.
exact Hxy2.
Qed.
End Fprop_Sterbenz.
\ No newline at end of file
End Fprop_Sterbenz.
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