Basic operations on floats: alignment, addition, multiplication
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Section Float_ops.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Implicit Arguments Float [[
beta]].
Definition Falign (
f1 f2 :
float beta) :=
let '(
Float m1 e1) :=
f1 in
let '(
Float m2 e2) :=
f2 in
if Zle_bool e1 e2
then (
m1, (
m2 *
Zpower beta (
e2 -
e1))%
Z,
e1)
else ((
m1 *
Zpower beta (
e1 -
e2))%
Z,
m2,
e2).
Theorem Falign_spec :
forall f1 f2 :
float beta,
let '(
m1,
m2,
e) :=
Falign f1 f2 in
F2R f1 = @
F2R beta (
Float m1 e) /\
F2R f2 = @
F2R beta (
Float m2 e).
Proof.
Theorem Falign_spec_exp:
forall f1 f2 :
float beta,
snd (
Falign f1 f2) =
Zmin (
Fexp f1) (
Fexp f2).
Proof.
intros (
m1,
e1) (
m2,
e2).
unfold Falign;
simpl.
generalize (
Zle_cases e1 e2);
case (
Zle_bool e1 e2);
intros He.
case (
Zmin_spec e1 e2);
intros (
H1,
H2);
easy.
case (
Zmin_spec e1 e2);
intros (
H1,
H2);
easy.
Qed.
Definition Fopp (
f1 :
float beta) :
float beta :=
let '(
Float m1 e1) :=
f1 in
Float (-
m1)%
Z e1.
Theorem F2R_opp :
forall f1 :
float beta,
(
F2R (
Fopp f1) = -
F2R f1)%
R.
intros (
m1,
e1).
apply F2R_Zopp.
Qed.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.