Float.v

(****************************************************************************                                                                                         IEEE754  :  Float                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** ****************************************************** Module Float.v     Inspired by the Diadic of Patrick Loiseleur *******************************************************)
Require Export Omega.
Require Export Zcomplements.
Require Export Zpower.
Require Export Arith.
Require Export Compare.
Require Export Reals.
Require Export Rpower.
Require Export Faux.
Require Export NDiv.
Require Export Digit.
Require Export sTactic.
Section definitions.
Variable radix:nat.

Local zradix := (inject_nat radix).
Hypothesis radixMoreThanOne:(lt (S O) radix).

Theorem ltzbO: (Zlt ZERO zradix).
Change (Zlt (inject_nat O) (inject_nat radix)).
Apply inj_lt; Auto with arith.
Qed.
(* The type float represents the set of numbers who can be written:   x = n*b^p with  n and p in Z. (pdic numbers) n = Fnum and p = Fexp *)

Record float: Set := Float {
   Fnum: Z;
   Fexp: Z }.

Theorem floatEq: (p, q:float) (Fnum p)=(Fnum q) -> (Fexp p)=(Fexp q) ->p=q.
Intros p q; Case p; Case q; Simpl; Intros; Apply (f_equal2 Z Z); Auto.
Qed.

Theorem floatDec: (x, y:float){x=y}+{~ x=y}.
Intros x y; Case x; Case y; Intros Fnum2 Fexp2 Fnum1 Fexp1.
Case (Z_eq_dec Fnum1 Fnum2); Intros H1.
Case (Z_eq_dec Fexp1 Fexp2); Intros H2.
Left; Apply floatEq; Auto.
Right; Red; Intros H'; Contradict H2; Inversion H'; Auto.
Right; Red; Intros H'; Contradict H1; Inversion H'; Auto.
Qed.

Definition Fzero := [x:Z](Float ZERO x).

Definition is_Fzero := [x:float](Fnum x)=ZERO.

Theorem is_Fzero_or_not: (x:float)(is_Fzero x) \/ ~ (is_Fzero x).
Unfold is_Fzero; Intro; CaseEq (Fnum x); Intros;
(Right; Discriminate) Orelse (Left; Auto).
Qed.
Coercion IZR : Z >-> R.
Coercion INR : nat >-> R.
Coercion inject_nat : nat >-> Z.

Definition FtoR := [x:float](Rmult (Fnum x) (powerRZ (INR radix) (Fexp x))).
Coercion FtoR : float >-> R.

Theorem is_Fzero_rep1: (x:float) (is_Fzero x) -><R> x==R0.
Intros x H; Unfold FtoR.
Red in H; Rewrite H; Simpl; Auto with real.
Qed.

Theorem is_Fzero_rep2: (x:float) <R> x==R0 ->(is_Fzero x).
Intros x H'.
Case (without_div_Od ? ? H'); Simpl; Auto.
Case x; Simpl.
Intros Fnum Fexp H'0; Red; Simpl; Auto with real.
Apply eq_IZR_R0; Auto.
Intros H'0; Contradict H'0; Auto with real zarith.
Qed.

Theorem NisFzeroComp: (x, y:float) ~ (is_Fzero x) -> <R> x==y ->~ (is_Fzero y).
Intros x y H' H'0; Contradict H'.
Apply is_Fzero_rep2; Auto.
Rewrite H'0.
Apply is_Fzero_rep1; Auto.
Qed.

Theorem not_ZERO_IZR: (z:Z) ~ z=ZERO ->~ (IZR z)==R0.
Intros z H'; Red; Intros H'0; Case H'.
Apply eq_IZR; Auto.
Qed.
(* Some inegalities that will be helpful *)

Theorem Rlt_monotony_exp:
  (x, y:R) (z:Z) (Rlt x y) ->
  (Rlt (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))).
Intros x y z H'; Apply Rlt_monotony_r; Auto with real arith.
Qed.

Theorem Rle_monotone_exp:
  (x, y:R) (z:Z) (Rle x y) ->
  (Rle (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))).
Intros x y z H'; Apply Rle_monotony_r; Auto with real arith.
Qed.

Theorem Rlt_mult_anticompatibility_exp:
  (x, y:R)
  (z:Z) (Rlt (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))) ->
  (Rlt x y).
Intros x y z H'; Apply Rlt_mult_anticompatibility with z := (powerRZ radix z);
Auto with real arith.
Repeat Rewrite (Rmult_sym (powerRZ radix z)); Auto.
Qed.

Theorem Rle_mult_anticompatibility_exp:
  (x, y:R)
  (z:Z) (Rle (Rmult x (powerRZ radix z)) (Rmult y (powerRZ radix z))) ->
  (Rle x y).
Intros x y z H'; Apply Rle_mult_anticompatibility with z := (powerRZ radix z);
Auto with real arith.
Repeat Rewrite (Rmult_sym (powerRZ radix z)); Auto.
Qed.

Theorem FtoREqInv1:
  (p, q:float) ~ (is_Fzero p) -> <R> p==q -> (Fnum p)=(Fnum q) ->p=q.
Intros p q H' H'0 H'1.
Apply floatEq; Auto.
Unfold FtoR in H'0.
Apply Rpow_eq_inv with r := (INR radix); Auto with real zarith.
Apply imp_not_Req; Right.
Unfold Rabsolu; Case (case_Rabsolu radix).
Intros H'2; Contradict H'2; Auto with real.
Apply Rlt_antisym; Auto.
Replace R0 with (INR O); Auto.
Auto with real zarith.
Replace R1 with (INR (S O)); Auto.
Intros H'2; Red.
Auto with real zarith.
Apply r_Rmult_mult with r := (IZR (Fnum p)); Auto with real.
Pattern 2 (Fnum p); Rewrite H'1; Auto.
Apply not_ZERO_IZR; Auto.
Qed.

Theorem FtoREqInv2: (p, q:float) <R> p==q -> (Fexp p)=(Fexp q) ->p=q.
Intros p q H' H'0.
Apply floatEq; Auto.
Apply eq_IZR; Auto.
Apply r_Rmult_mult with r := (powerRZ radix (Fexp p)); Auto.
Repeat Rewrite (Rmult_sym (powerRZ radix (Fexp p))); Pattern 2 (Fexp p);
Rewrite H'0; Auto with real.
Apply powerRZ_NOR; Auto with real arith.
Qed.

Definition Fdigit := [p:float](digit radix (absolu (Fnum p))).

Definition Fshift :=
   [n:nat] [x:float]
   (Float (Zmult (Fnum x) (Zpower_nat zradix n)) (Zminus (Fexp x) n)).

Theorem sameExpEq: (p, q:float) <R> p==q -> (Fexp p)=(Fexp q) ->p=q.
Intros p q; Case p; Case q; Unfold FtoR; Simpl.
Intros Fnum1 Fexp1 Fnum2 Fexp2 H' H'0; Rewrite H'0; Rewrite H'0 in H'.
Cut Fnum1=Fnum2.
Intros H'1; Rewrite <- H'1; Auto.
Apply eq_IZR; Auto.
Apply r_Rmult_mult with r := (powerRZ radix Fexp1);
Repeat Rewrite (Rmult_sym (powerRZ radix Fexp1)); Auto.
Apply imp_not_Req; Right; Auto with real.
Red; Auto with real.
Apply powerRZ_lt; Auto with real.
Apply Rlt_trans with r2 := R1; Auto with real.
Qed.

Theorem FshiftFdigit:
  (n:nat) (x:float) ~ (is_Fzero x) ->(Fdigit (Fshift n x))=(plus (Fdigit x) n).
Intros n x; Case x; Unfold Fshift Fdigit is_Fzero; Simpl.
Intros p1 p2 H; Rewrite absolu_comp_mult; Auto.
Rewrite absolu_comp_Rpower.
Replace (absolu zradix) with radix; Auto.
Apply digitAdd; Auto with arith.
Generalize H; Case p1; Simpl; Auto with zarith.
Intros p H'; Generalize (convert_not_O p); Case (convert p); Auto with zarith.
Intros p H'; Generalize (convert_not_O p); Case (convert p); Auto with zarith.
Unfold zradix; Case radix; Simpl; Auto with zarith.
Intros; Rewrite bij1; Auto.
Qed.

Theorem FshiftCorrect: (n:nat) (x:float)<R> (Fshift n x)==x.
Intros n x; Unfold FtoR; Simpl.
Rewrite Rmult_IZR.
Unfold zradix; Rewrite Zpower_nat_powerRZ; Auto.
Repeat Rewrite Rmult_assoc.
Rewrite <- powerRZ_add; Auto with real arith.
Rewrite Zle_plus_minus; Auto.
Qed.

Theorem FshiftCorrectInv:
  (x, y:float) <R> x==y -> (Zle (Fexp x) (Fexp y)) ->
  (Fshift (absolu (Zminus (Fexp y) (Fexp x))) y)=x.
Intros x y H' H'0; Try Apply sameExpEq; Auto.
Apply trans_eqT with y := (FtoR y); Auto.
Apply FshiftCorrect.
Generalize H' H'0; Case x; Case y; Simpl; Clear H' H'0 x y.
Intros Fnum1 Fexp1 Fnum2 Fexp2 H' H'0; Rewrite inj_abs; Auto with zarith.
Qed.

Theorem FshiftO: (x:float)(Fshift O x)=x.
Intros x; Unfold Fshift; Apply floatEq; Simpl.
Replace (Zpower_nat zradix O) with (INZ (1)); Auto with zarith.
Simpl; Auto with zarith.
Auto with zarith.
Qed.

Theorem FshiftCorrectSym:
  (x, y:float) <R> x==y ->(Ex [n:nat] (Ex [m:nat] (Fshift n x)=(Fshift m y))).
Intros x y H'.
Case (Z_le_gt_dec (Fexp x) (Fexp y)); Intros H'1.
Exists O; Exists (absolu (Zminus (Fexp y) (Fexp x))).
Rewrite FshiftO.
Apply sym_equal.
Apply FshiftCorrectInv; Auto.
Exists (absolu (Zminus (Fexp x) (Fexp y))); Exists O.
Rewrite FshiftO.
Apply FshiftCorrectInv; Auto with zarith.
Qed.

Theorem FshiftAdd:
  (n, m:nat) (p:float)(Fshift (plus n m) p)=(Fshift n (Fshift m p)).
Intros n m p; Case p; Unfold Fshift; Simpl.
Intros Fnum1 Fexp1; Apply floatEq; Simpl; Auto with zarith.
Rewrite Zpower_nat_is_exp; Auto with zarith.
Rewrite (Zmult_sym (Zpower_nat radix n)); Auto with zarith.
Rewrite <- (Zminus_Zplus_compatible (Zminus Fexp1 m) n m).
Replace (Zplus (Zminus Fexp1 m) m) with Fexp1; Auto with zarith.
Replace (inject_nat (plus n m)) with (Zplus n m); Auto with zarith arith.
Rewrite <- inj_plus; Auto.
Qed.

Theorem ReqGivesEqwithSameExp:
  (p, q:float)
  (Ex [r:float] (Ex [s:float] <R> p==r /\ (<R> q==s /\ (Fexp r)=(Fexp s)))).
Intros p q;
Exists (Fshift (absolu (Zminus (Fexp p) (Zmin (Fexp p) (Fexp q)))) p);
Exists (Fshift (absolu (Zminus (Fexp q) (Zmin (Fexp p) (Fexp q)))) q);
Repeat Split; Auto with real.
Rewrite FshiftCorrect; Auto.
Rewrite FshiftCorrect; Auto.
Simpl.
Replace (inject_nat (absolu (Zminus (Fexp p) (Zmin (Fexp p) (Fexp q)))))
     with (Zminus (Fexp p) (Zmin (Fexp p) (Fexp q))).
Replace (inject_nat (absolu (Zminus (Fexp q) (Zmin (Fexp p) (Fexp q)))))
     with (Zminus (Fexp q) (Zmin (Fexp p) (Fexp q))).
Case (Zmin_or (Fexp p) (Fexp q)); Intros H'; Rewrite H'; Auto with zarith.
Rewrite inj_abs; Auto.
Apply Zsimpl_le_plus_l with p := (Zmin (Fexp p) (Fexp q)); Auto with zarith.
Generalize (Zle_min_r (Fexp p) (Fexp q)); Auto with zarith.
Rewrite inj_abs; Auto.
Apply Zsimpl_le_plus_l with p := (Zmin (Fexp p) (Fexp q)); Auto with zarith.
Generalize (Zle_min_l (Fexp p) (Fexp q)); Auto with zarith.
Qed.

Theorem FdigitEq:
  (x, y:float) ~ (is_Fzero x) -> <R> x==y -> (Fdigit x)=(Fdigit y) ->x=y.
Intros x y H' H'0 H'1.
Cut ~ (is_Fzero y); [Intros NZy | Idtac].
2:Red; Intros H'2; Case H'.
2:Apply is_Fzero_rep2; Rewrite H'0; Apply is_Fzero_rep1; Auto.
Case (Zle_or_lt (Fexp x) (Fexp y)); Intros Eq1.
Case (Zle_lt_or_eq ? ? Eq1); Clear Eq1; Intros Eq1.
Absurd (Fdigit (Fshift (absolu (Zminus (Fexp y) (Fexp x))) y))=
       (plus (Fdigit y) (absolu (Zminus (Fexp y) (Fexp x)))).
Rewrite FshiftCorrectInv; Auto.
Rewrite <- H'1.
Red; Intros H'2.
Absurd O=(Zminus (Fexp y) (Fexp x)); Auto with arith.
Apply Zlt_not_eq; Auto with zarith.
Apply Zsimpl_lt_plus_l with p := (Fexp x).
Replace (Zplus (Fexp x) O) with (Fexp x); Auto with zarith.
Rewrite <- (inj_abs (Zminus (Fexp y) (Fexp x))); Auto with zarith.
Apply Zlt_le_weak; Auto.
Apply FshiftFdigit; Auto.
Apply sameExpEq; Auto.
Absurd (Fdigit (Fshift (absolu (Zminus (Fexp x) (Fexp y))) x))=
       (plus (Fdigit x) (absolu (Zminus (Fexp x) (Fexp y)))).
Rewrite FshiftCorrectInv; Auto.
Rewrite <- H'1.
Red; Intros H'2.
Absurd O=(Zminus (Fexp x) (Fexp y)); Auto with arith.
Apply Zlt_not_eq; Auto with zarith.
Apply Zsimpl_lt_plus_l with p := (Fexp y).
Replace (Zplus (Fexp y) O) with (Fexp y); Auto with zarith.
Rewrite <- (inj_abs (Zminus (Fexp x) (Fexp y))); Auto with zarith.
Apply Zlt_le_weak; Auto.
Apply FshiftFdigit; Auto.
Qed.
End definitions.
Hints Resolve Rlt_monotony_exp Rle_monotone_exp :real.

14/12/100, 02:08