diff options
Diffstat (limited to 'flocq/Calc/Fcalc_ops.v')
-rw-r--r-- | flocq/Calc/Fcalc_ops.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/flocq/Calc/Fcalc_ops.v b/flocq/Calc/Fcalc_ops.v index 7ece6832..e3b059d1 100644 --- a/flocq/Calc/Fcalc_ops.v +++ b/flocq/Calc/Fcalc_ops.v @@ -28,6 +28,8 @@ 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 @@ -38,7 +40,7 @@ Definition Falign (f1 f2 : float beta) := Theorem Falign_spec : forall f1 f2 : float beta, let '(m1, m2, e) := Falign f1 f2 in - F2R f1 = F2R (Float beta m1 e) /\ F2R f2 = F2R (Float beta m2 e). + F2R f1 = @F2R beta (Float m1 e) /\ F2R f2 = @F2R beta (Float m2 e). Proof. unfold Falign. intros (m1, e1) (m2, e2). @@ -61,9 +63,9 @@ case (Zmin_spec e1 e2); intros (H1,H2); easy. case (Zmin_spec e1 e2); intros (H1,H2); easy. Qed. -Definition Fopp (f1: float beta) := +Definition Fopp (f1 : float beta) : float beta := let '(Float m1 e1) := f1 in - Float beta (-m1)%Z e1. + Float (-m1)%Z e1. Theorem F2R_opp : forall f1 : float beta, @@ -72,9 +74,9 @@ intros (m1,e1). apply F2R_Zopp. Qed. -Definition Fabs (f1: float beta) := +Definition Fabs (f1 : float beta) : float beta := let '(Float m1 e1) := f1 in - Float beta (Zabs m1)%Z e1. + Float (Zabs m1)%Z e1. Theorem F2R_abs : forall f1 : float beta, @@ -83,9 +85,9 @@ intros (m1,e1). apply F2R_Zabs. Qed. -Definition Fplus (f1 f2 : float beta) := +Definition Fplus (f1 f2 : float beta) : float beta := let '(m1, m2 ,e) := Falign f1 f2 in - Float beta (m1 + m2) e. + Float (m1 + m2) e. Theorem F2R_plus : forall f1 f2 : float beta, @@ -104,7 +106,7 @@ Qed. Theorem Fplus_same_exp : forall m1 m2 e, - Fplus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 + m2) e. + Fplus (Float m1 e) (Float m2 e) = Float (m1 + m2) e. Proof. intros m1 m2 e. unfold Fplus. @@ -136,17 +138,17 @@ Qed. Theorem Fminus_same_exp : forall m1 m2 e, - Fminus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 - m2) e. + Fminus (Float m1 e) (Float m2 e) = Float (m1 - m2) e. Proof. intros m1 m2 e. unfold Fminus. apply Fplus_same_exp. Qed. -Definition Fmult (f1 f2 : float beta) := +Definition Fmult (f1 f2 : float beta) : float beta := let '(Float m1 e1) := f1 in let '(Float m2 e2) := f2 in - Float beta (m1 * m2) (e1 + e2). + Float (m1 * m2) (e1 + e2). Theorem F2R_mult : forall f1 f2 : float beta, |