Fop.v

(****************************************************************************                                                                                         IEEE754  :  Fop                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import Float.
Section operations.
Variable radix:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixNotZero:~ radix=O.

Definition Fplus :=
   [x, y:float]
   (Float
      (Zplus
         (Zmult
            (Fnum x)
            (Zpower_nat
               (inject_nat radix)
               (absolu (Zminus (Fexp x) (Zmin (Fexp x) (Fexp y))))))
         (Zmult
            (Fnum y)
            (Zpower_nat
               (inject_nat radix)
               (absolu (Zminus (Fexp y) (Zmin (Fexp x) (Fexp y)))))))
      (Zmin (Fexp x) (Fexp y))).

Theorem Fplus_correct: (x, y:float)<R> (Fplus x y)==(Rplus x y).
Intros x y; Unfold Fplus Fshift FtoRradix FtoR; Simpl.
Rewrite plus_IZR.
Rewrite Rmult_sym; Rewrite Rmult_Rplus_distr; Auto.
Repeat Rewrite Rmult_IZR.
Repeat Rewrite (Rmult_sym (Fnum x)); Repeat Rewrite (Rmult_sym (Fnum y)).
Repeat Rewrite Zpower_nat_powerRZ; Auto.
Repeat Rewrite <- Rmult_assoc.
Repeat Rewrite <- powerRZ_add; Auto with real zarith arith.
Repeat Rewrite inj_abs; Auto with real zarith.
Repeat Rewrite Zle_plus_minus; Auto.
Unfold Zminus; Apply Zle_left; Auto with arith.
Apply Zle_min_r; Auto.
Unfold Zminus; Apply Zle_left; Auto with arith.
Apply Zle_min_l; Auto.
Qed.

Definition Fopp := [x:float](Float (Zopp (Fnum x)) (Fexp x)).

Theorem Fopp_correct: (x:float)<R> (Fopp x)==(Ropp x).
Unfold FtoRradix FtoR Fopp; Simpl.
Intros x.
Rewrite Ropp_Ropp_IZR; Auto with real.
Apply Ropp_mul1.
Qed.

Theorem Fopp_Fopp: (p:float)(Fopp (Fopp p))=p.
Intros p; Case p; Unfold Fopp; Simpl; Auto.
Intros; Rewrite Zopp_Zopp; Auto.
Qed.

Definition Fabs := [x:float](Float (Zabs (Fnum x)) (Fexp x)).

Theorem Fabs_correct1: (x:float) (Rle R0 (FtoR radix x)) -><R> (Fabs x)==x.
Intros x; Case x; Unfold FtoRradix FtoR; Simpl.
Intros Fnum1 Fexp1 H'.
Repeat Rewrite <- (Rmult_sym (powerRZ radix Fexp1)); Apply Rmult_mult_r; Auto.
Cut (Zle ZERO Fnum1).
Unfold Zabs Zle.
Case Fnum1; Simpl; Auto.
Intros p H'0; Case H'0; Auto.
Apply not_Zgt; Auto.
Contradict H'.
Apply Rle_not; Auto.
Rewrite Rmult_sym.
Replace R0 with (Rmult (powerRZ radix Fexp1) R0); Auto with real.
Apply Rlt_monotony; Auto with real arith.
Replace R0 with (IZR ZERO); Auto with real zarith arith.
Qed.

Theorem Fabs_correct2:
  (x:float) (Rle (FtoR radix x) R0) -><R> (Fabs x)==(Ropp x).
Intros x; Case x; Unfold FtoRradix FtoR; Simpl.
Intros Fnum1 Fexp1 H'.
Rewrite <- Ropp_mul1; Repeat Rewrite <- (Rmult_sym (powerRZ radix Fexp1));
Apply Rmult_mult_r; Auto.
Cut (Zle Fnum1 ZERO).
Unfold Zabs Zle.
Case Fnum1; Simpl; Auto with real.
Intros p H'0; Case H'0; Auto.
Intros p H'0; Rewrite Ropp_Ropp; Auto.
Apply not_Zgt; Auto.
Contradict H'.
Apply Rle_not; Auto.
Rewrite Rmult_sym.
Replace R0 with (Rmult (powerRZ radix Fexp1) R0); Auto with real.
Apply Rlt_monotony; Auto with real arith.
Replace R0 with (IZR ZERO); Auto with real zarith arith.
Qed.

Theorem Fabs_correct: (x:float)<R> (Fabs x)==(Rabsolu x).
Intros x; Unfold Rabsolu.
Case (case_Rabsolu x); Intros H1.
Unfold FtoRradix; Apply Fabs_correct2; Auto with arith.
Apply Rlt_le; Auto.
Unfold FtoRradix; Apply Fabs_correct1; Auto with arith.
Apply Rle_sym2; Auto.
Qed.

Theorem Fabs_Fzero: (x:float) ~ (is_Fzero x) ->~ (is_Fzero (Fabs x)).
Intros x; Case x; Unfold is_Fzero; Simpl.
Intros n m; Case n; Simpl; Auto with zarith; Intros; Red; Discriminate.
Qed.
Hints Resolve Fabs_Fzero :float.

Theorem Fdigit_abs: (x:float)(Fdigit radix (Fabs x))=(Fdigit radix x).
Intros x; Unfold Fabs Fdigit; Simpl.
Case (Fnum x); Auto.
Qed.

Definition Fminus := [x, y:float](Fplus x (Fopp y)).

Theorem Fminus_correct: (x, y:float)<R> (Fminus x y)==(Rminus x y).
Intros x y; Unfold Fminus.
Rewrite Fplus_correct.
Rewrite Fopp_correct; Auto.
Qed.

Theorem Fopp_Fminus: (p, q:float)(Fopp (Fminus p q))=(Fminus q p).
Intros p q; Case p; Case q; Unfold Fopp Fminus Fplus; Simpl; Auto.
Intros; Apply floatEq; Simpl; Repeat Rewrite (Zmin_sym Fexp0 Fexp);
Repeat Rewrite Zopp_Zmult; Auto with zarith.
Qed.

Theorem Fopp_Fminus_dist:
  (p, q:float)(Fopp (Fminus p q))=(Fminus (Fopp p) (Fopp q)).
Intros p q; Case p; Case q; Unfold Fopp Fminus Fplus; Simpl; Auto.
Intros; Apply floatEq; Simpl; Repeat Rewrite (Zmin_sym Fexp0 Fexp);
Repeat Rewrite Zopp_Zmult; Auto with zarith.
Qed.

Theorem minusSameExp:
  (x, y:float) (Fexp x)=(Fexp y) ->
  (Fminus x y)=(Float (Zminus (Fnum x) (Fnum y)) (Fexp x)).
Intros x y; Case x; Case y; Unfold Fminus Fplus Fopp; Simpl.
Intros Fnum1 Fexp1 Fnum2 Fexp2 H'; Rewrite <- H'.
Repeat Rewrite Zmin_n_n.
Apply floatEq; Simpl; Auto.
Replace (absolu (Zminus Fexp2 Fexp2)) with O; Auto with zarith arith.
Replace (Zpower_nat radix O) with (INZ (1)); Simpl; Auto with zarith arith.
Replace (Zminus Fexp2 Fexp2) with ZERO; Simpl; Auto with zarith arith.
Qed.

Definition Fmult :=
   [x, y:float](Float (Zmult (Fnum x) (Fnum y)) (Zplus (Fexp x) (Fexp y))).

Definition Fmult_correct: (x, y:float)<R> (Fmult x y)==(Rmult x y).
Intros x y; Unfold FtoRradix FtoR Fmult; Simpl; Auto.
Rewrite powerRZ_add; Auto with real.
Repeat Rewrite Rmult_IZR.
Repeat Rewrite Rmult_assoc.
Repeat Rewrite (Rmult_sym (Fnum y)).
Repeat Rewrite <- Rmult_assoc.
Repeat Rewrite Zmult_assoc_r; Auto.
Qed.
End operations.
Hints Resolve Fabs_Fzero :float.

14/12/100, 02:57