(****************************************************************************
                                                                             
          IEEE754  :  Float                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  ******************************************************
   Module Float.v 				   	
   Inspired by the Diadic of Patrick Loiseleur
  *******************************************************)
Require Export Omega.
Require Export Compare.
Require Export Rpow.
Section definitions.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
(* 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 :
 forall p q : float, Fnum p = Fnum q -> Fexp p = Fexp q -> p = q.
intros p q; case p; case q; simpl in |- *; intros;
 apply (f_equal2 (A1:=Z) (A2:=Z)); auto.
Qed.
 
Theorem floatDec : forall x y : float, {x = y} + {x <> y}.
(* Goal: forall x y : float, sumbool (@eq float x y) (not (@eq float x y)) *)
intros x y; case x; case y; intros Fnum2 Fexp2 Fnum1 Fexp1.
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
case (Z_eq_dec Fnum1 Fnum2); intros H1.
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
case (Z_eq_dec Fexp1 Fexp2); intros H2.
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
left; apply floatEq; auto.
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
right; red in |- *; intros H'; Contradict H2; inversion H'; auto.
(* Goal: sumbool (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2)) (not (@eq float (Float Fnum1 Fexp1) (Float Fnum2 Fexp2))) *)
right; red in |- *; intros H'; Contradict H1; inversion H'; auto.
Qed.
 
Definition Fzero (x : Z) := Float 0 x.
 
Definition is_Fzero (x : float) := Fnum x = 0%Z.
 
Theorem is_FzeroP : forall x : float, is_Fzero x \/ ~ is_Fzero x.
unfold is_Fzero in |- *; intro; CaseEq (Fnum x); intros;
 (right; discriminate) || (left; auto).
Qed.
Coercion IZR : Z >-> R.
Coercion INR : nat >-> R.
Coercion Z_of_nat : nat >-> Z.
 
Definition FtoR (x : float) := (Fnum x * powerRZ (IZR radix) (Fexp x))%R.
 
Local Coercion FtoR : float >-> R.
 
Theorem FzeroisReallyZero : forall z : Z, Fzero z = 0%R :>R.
(* Goal: forall z : Z, @eq R (FtoR (Fzero z)) (IZR Z0) *)
intros z; unfold FtoR in |- *; simpl in |- *; auto with real.
Qed.
 
Theorem is_Fzero_rep1 : forall x : float, is_Fzero x -> x = 0%R :>R.
(* Goal: forall (x : float) (_ : is_Fzero x), @eq R (FtoR x) (IZR Z0) *)
intros x H; unfold FtoR in |- *.
(* Goal: @eq R (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (IZR Z0) *)
red in H; rewrite H; simpl in |- *; auto with real.
Qed.
 
Theorem LtFnumZERO : forall x : float, (0 < Fnum x)%Z -> (0 < x)%R.
(* Goal: forall (x : float) (_ : Z.lt Z0 (Fnum x)), Rlt (IZR Z0) (FtoR x) *)
intros x; case x; unfold FtoR in |- *; simpl in |- *.
intros Fnum1 Fexp1 H'; replace 0%R with (Fnum1 * 0)%R;
 [ apply Rmult_lt_compat_l | ring ]; auto with real zarith.
Qed.
 
Theorem is_Fzero_rep2 : forall x : float, x = 0%R :>R -> is_Fzero x.
(* Goal: forall (x : float) (_ : @eq R (FtoR x) (IZR Z0)), is_Fzero x *)
intros x H'.
(* Goal: is_Fzero x *)
case (Rmult_integral _ _ H'); simpl in |- *; auto.
(* Goal: forall _ : @eq R (IZR (Fnum x)) (IZR Z0), is_Fzero x *)
(* Goal: forall _ : @eq R (powerRZ (IZR radix) (Fexp x)) (IZR Z0), is_Fzero x *)
case x; simpl in |- *.
(* Goal: forall (Fnum Fexp : Z) (_ : @eq R (IZR Fnum) (IZR Z0)), is_Fzero (Float Fnum Fexp) *)
(* Goal: forall _ : @eq R (powerRZ (IZR radix) (Fexp x)) (IZR Z0), is_Fzero x *)
intros Fnum1 Fexp1 H'0; red in |- *; simpl in |- *; auto with real zarith.
(* Goal: @eq Z Fnum1 Z0 *)
(* Goal: forall _ : @eq R (powerRZ (IZR radix) (Fexp x)) (IZR Z0), is_Fzero x *)
apply eq_IZR_R0; auto.
(* Goal: forall _ : @eq R (powerRZ (IZR radix) (Fexp x)) (IZR Z0), is_Fzero x *)
intros H'0; Contradict H'0; apply powerRZ_NOR; auto with real zarith.
Qed.
 
Theorem NisFzeroComp :
 forall x y : float, ~ is_Fzero x -> x = y :>R -> ~ is_Fzero y.
(* Goal: forall (x y : float) (_ : not (is_Fzero x)) (_ : @eq R (FtoR x) (FtoR y)), not (is_Fzero y) *)
intros x y H' H'0; Contradict H'.
(* Goal: is_Fzero x *)
apply is_Fzero_rep2; auto.
(* Goal: @eq R (FtoR x) (IZR Z0) *)
rewrite H'0.
(* Goal: @eq R (FtoR y) (IZR Z0) *)
apply is_Fzero_rep1; auto.
Qed.
(* Some inegalities that will be helpful *)
 
Theorem Rlt_monotony_exp :
 forall (x y : R) (z : Z),
 (x < y)%R -> (x * powerRZ radix z < y * powerRZ radix z)%R.
(* Goal: forall (x y : R) (z : Z) (_ : Rlt x y), Rlt (Rmult x (powerRZ (IZR radix) z)) (Rmult y (powerRZ (IZR radix) z)) *)
intros x y z H'; apply Rmult_lt_compat_r; auto with real zarith.
Qed.
 
Theorem Rle_monotone_exp :
 forall (x y : R) (z : Z),
 (x <= y)%R -> (x * powerRZ radix z <= y * powerRZ radix z)%R.
(* Goal: forall (x y : R) (z : Z) (_ : Rle x y), Rle (Rmult x (powerRZ (IZR radix) z)) (Rmult y (powerRZ (IZR radix) z)) *)
intros x y z H'; apply Rmult_le_compat_r; auto with real zarith.
Qed.
 
Theorem Rlt_monotony_contra_exp :
 forall (x y : R) (z : Z),
 (x * powerRZ radix z < y * powerRZ radix z)%R -> (x < y)%R.
intros x y z H'; apply Rmult_lt_reg_l with (r := powerRZ radix z);
 auto with real zarith.
(* Goal: Rle (Rmult (powerRZ (IZR radix) z) x) (Rmult (powerRZ (IZR radix) z) y) *)
repeat rewrite (Rmult_comm (powerRZ radix z)); auto.
Qed.
 
Theorem Rle_monotony_contra_exp :
 forall (x y : R) (z : Z),
 (x * powerRZ radix z <= y * powerRZ radix z)%R -> (x <= y)%R.
intros x y z H'; apply Rmult_le_reg_l with (r := powerRZ radix z);
 auto with real zarith.
(* Goal: Rle (Rmult (powerRZ (IZR radix) z) x) (Rmult (powerRZ (IZR radix) z) y) *)
repeat rewrite (Rmult_comm (powerRZ radix z)); auto.
Qed.
 
Theorem FtoREqInv1 :
 forall p q : float, ~ is_Fzero p -> p = q :>R -> Fnum p = Fnum q -> p = q.
(* Goal: forall (p q : float) (_ : not (is_Fzero p)) (_ : @eq R (FtoR p) (FtoR q)) (_ : @eq Z (Fnum p) (Fnum q)), @eq float p q *)
intros p q H' H'0 H'1.
(* Goal: @eq float p q *)
apply floatEq; auto.
(* Goal: @eq Z (Fexp p) (Fexp q) *)
unfold FtoR in H'0.
(* Goal: @eq Z (Fexp p) (Fexp q) *)
apply Rpow_eq_inv with (r := IZR radix); auto 6 with real zarith.
(* Goal: not (@eq R (Rabs (IZR radix)) (IZR (Zpos xH))) *)
(* Goal: @eq R (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Fexp q)) *)
apply Rlt_dichotomy_converse; right; red in |- *.
(* Goal: Rlt (IZR (Zpos xH)) (Rabs (IZR radix)) *)
(* Goal: @eq R (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Fexp q)) *)
unfold Rabs in |- *; case (Rcase_abs radix).
intros H'2; Contradict H'2; apply Rle_not_lt; apply Ropp_le_cancel;
 auto with real.
(* Goal: forall _ : Rge (IZR radix) (IZR Z0), Rlt (IZR (Zpos xH)) (IZR radix) *)
(* Goal: @eq R (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Fexp q)) *)
intros H'2; replace 1%R with (IZR 1); auto with real zarith.
(* Goal: @eq R (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Fexp q)) *)
apply Rmult_eq_reg_l with (r := IZR (Fnum p)); auto with real.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp q))) *)
pattern (Fnum p) at 2 in |- *; rewrite H'1; auto.
Qed.
 
Theorem FtoREqInv2 :
 forall p q : float, p = q :>R -> Fexp p = Fexp q -> p = q.
(* Goal: forall (p q : float) (_ : @eq R (FtoR p) (FtoR q)) (_ : @eq Z (Fexp p) (Fexp q)), @eq float p q *)
intros p q H' H'0.
(* Goal: @eq float p q *)
apply floatEq; auto.
(* Goal: @eq Z Fnum1 Fnum2 *)
apply eq_IZR; auto.
apply Rmult_eq_reg_l with (r := powerRZ radix (Fexp p));
 auto with real zarith.
repeat rewrite (Rmult_comm (powerRZ radix (Fexp p)));
 pattern (Fexp p) at 2 in |- *; rewrite H'0; auto with real zarith.
Qed.
 
Theorem Rlt_Float_Zlt :
 forall p q r : Z, (Float p r < Float q r)%R -> (p < q)%Z.
(* Goal: forall (p q r : Z) (_ : Rle (FtoR (Float p r)) (FtoR (Float q r))), Z.le p q *)
intros p q r H'.
(* Goal: Z.lt p q *)
apply lt_IZR.
(* Goal: Rlt (IZR p) (IZR q) *)
apply Rlt_monotony_contra_exp with (z := r); auto with real.
Qed.
 
Theorem Rle_Float_Zle :
 forall p q r : Z, (Float p r <= Float q r)%R -> (p <= q)%Z.
(* Goal: forall (p q r : Z) (_ : Rle (FtoR (Float p r)) (FtoR (Float q r))), Z.le p q *)
intros p q r H'.
(* Goal: Z.le p q *)
apply le_IZR.
(* Goal: Rle (IZR p) (IZR q) *)
apply Rle_monotony_contra_exp with (z := r); auto with real.
Qed.
(* Properties for floats with 1 as mantissa *)
 
Theorem oneExp_le :
 forall x y : Z, (x <= y)%Z -> (Float 1%nat x <= Float 1%nat y)%R.
(* Goal: forall (x y : Z) (_ : Z.lt x y), Rlt (FtoR (Float (Z.of_nat (S O)) x)) (FtoR (Float (Z.of_nat (S O)) y)) *)
intros x y H'; unfold FtoR in |- *; simpl in |- *.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) x)) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) y)) *)
repeat rewrite Rmult_1_l; auto with real zarith.
(* Goal: Rle (powerRZ (IZR radix) x) (powerRZ (IZR radix) y) *)
apply Rle_powerRZ; try replace 1%R with (IZR 1); auto with real zarith zarith.
Qed.
 
Theorem oneExp_lt :
 forall x y : Z, (x < y)%Z -> (Float 1%nat x < Float 1%nat y)%R.
(* Goal: forall (x y : Z) (_ : Z.lt x y), Rlt (FtoR (Float (Z.of_nat (S O)) x)) (FtoR (Float (Z.of_nat (S O)) y)) *)
intros x y H'; unfold FtoR in |- *; simpl in |- *.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) x)) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) y)) *)
repeat rewrite Rmult_1_l; auto with real zarith.
Qed.
 
Theorem oneExp_Zlt :
 forall x y : Z, (Float 1%nat x < Float 1%nat y)%R -> (x < y)%Z.
(* Goal: forall (x y : Z) (_ : Rlt (FtoR (Float (Z.of_nat (S O)) x)) (FtoR (Float (Z.of_nat (S O)) y))), Z.lt x y *)
intros x y H'; case (Zle_or_lt y x); auto; intros ZH; Contradict H'.
(* Goal: not (Rlt (FtoR (Float (Z.of_nat (S O)) x)) (FtoR (Float (Z.of_nat (S O)) y))) *)
apply Rle_not_lt; apply oneExp_le; auto.
Qed.
 
Theorem oneExp_Zle :
 forall x y : Z, (Float 1%nat x <= Float 1%nat y)%R -> (x <= y)%Z.
(* Goal: forall (x y : Z) (_ : Rle (FtoR (Float (Z.of_nat (S O)) x)) (FtoR (Float (Z.of_nat (S O)) y))), Z.le x y *)
intros x y H'; case (Zle_or_lt x y); auto; intros ZH; Contradict H'.
(* Goal: not (Rle (FtoR (Float (Z.of_nat (S O)) x)) (FtoR (Float (Z.of_nat (S O)) y))) *)
apply Rgt_not_le; red in |- *; apply oneExp_lt; auto.
Qed.
 
Definition Fdigit (p : float) := digit radix (Fnum p).
 
Definition Fshift (n : nat) (x : float) :=
  Float (Fnum x * Zpower_nat radix n) (Fexp x - n).
 
Theorem sameExpEq : forall p q : float, p = q :>R -> Fexp p = Fexp q -> p = q.
(* Goal: forall (p q : float) (_ : @eq R (FtoR p) (FtoR q)) (_ : @eq Z (Fexp p) (Fexp q)), @eq float p q *)
intros p q; case p; case q; unfold FtoR in |- *; simpl in |- *.
(* Goal: forall (Fnum Fexp Fnum0 Fexp0 : Z) (_ : @eq R (Rmult (IZR Fnum0) (powerRZ (IZR radix) Fexp0)) (Rmult (IZR Fnum) (powerRZ (IZR radix) Fexp))) (_ : @eq Z Fexp0 Fexp), @eq float (Float Fnum0 Fexp0) (Float Fnum Fexp) *)
intros Fnum1 Fexp1 Fnum2 Fexp2 H' H'0; rewrite H'0; rewrite H'0 in H'.
(* Goal: @eq float (Float Fnum2 Fexp1) (Float Fnum1 Fexp1) *)
cut (Fnum1 = Fnum2).
(* Goal: forall _ : @eq Z Fnum1 Fnum2, @eq float (Float Fnum2 Fexp1) (Float Fnum1 Fexp1) *)
(* Goal: @eq Z Fnum1 Fnum2 *)
intros H'1; rewrite <- H'1; auto.
(* Goal: @eq Z Fnum1 Fnum2 *)
apply eq_IZR; auto.
apply Rmult_eq_reg_l with (r := powerRZ radix Fexp1);
 repeat rewrite (Rmult_comm (powerRZ radix Fexp1)); 
 auto.
(* Goal: not (@eq R (powerRZ (IZR radix) Fexp1) (IZR Z0)) *)
apply Rlt_dichotomy_converse; right; auto with real.
(* Goal: Rgt (powerRZ (IZR radix) Fexp1) (IZR Z0) *)
red in |- *; auto with real.
Qed.
 
Theorem FshiftFdigit :
 forall (n : nat) (x : float),
 ~ is_Fzero x -> Fdigit (Fshift n x) = Fdigit x + n.
(* Goal: forall (n : nat) (x : float) (_ : not (is_Fzero x)), @eq nat (Fdigit (Fshift n x)) (Init.Nat.add (Fdigit x) n) *)
intros n x; case x; unfold Fshift, Fdigit, is_Fzero in |- *; simpl in |- *.
(* Goal: forall (Fnum _ : Z) (_ : not (@eq Z Fnum Z0)), @eq nat (digit radix (Z.mul Fnum (Zpower_nat radix n))) (Init.Nat.add (digit radix Fnum) n) *)
intros p1 p2 H; apply digitAdd; auto.
Qed.
 
Theorem FshiftCorrect : forall (n : nat) (x : float), Fshift n x = x :>R.
intros n x; unfold FtoR in |- *; simpl in |- *.
rewrite Rmult_IZR.
rewrite Zpower_nat_Z_powerRZ; auto.
repeat rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Zplus_minus; auto.
Qed.
 
Theorem FshiftCorrectInv :
 forall x y : float,
 x = y :>R ->
 (Fexp x <= Fexp y)%Z -> Fshift (Zabs_nat (Fexp y - Fexp x)) y = x.
(* Goal: forall (x y : float) (_ : @eq R (FtoR x) (FtoR y)) (_ : Z.le (Fexp x) (Fexp y)), @eq float (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y) x *)
intros x y H' H'0; try apply sameExpEq; auto.
(* Goal: @eq R (FtoR (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y)) (FtoR x) *)
(* Goal: @eq Z (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y)) (Fexp x) *)
apply trans_eq with (y := FtoR y); auto.
(* Goal: @eq R (FtoR (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y)) (FtoR y) *)
(* Goal: @eq Z (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y)) (Fexp x) *)
apply FshiftCorrect.
(* Goal: @eq Z (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y)) (Fexp x) *)
generalize H' H'0; case x; case y; simpl in |- *; clear H' H'0 x y.
(* Goal: forall (Fnum Fexp Fnum0 Fexp0 : Z) (_ : @eq R (FtoR (Float Fnum0 Fexp0)) (FtoR (Float Fnum Fexp))) (_ : Z.le Fexp0 Fexp), @eq Z (Z.sub Fexp (Z.of_nat (Z.abs_nat (Z.sub Fexp Fexp0)))) Fexp0 *)
intros Fnum1 Fexp1 Fnum2 Fexp2 H' H'0; rewrite inj_abs; auto with zarith.
Qed.
 
Theorem FshiftO : forall x : float, Fshift 0 x = x.
(* Goal: forall x : float, @eq float (Fshift O x) x *)
intros x; unfold Fshift in |- *; apply floatEq; simpl in |- *.
(* Goal: @eq Z (Z.mul (Fnum x) (Zpos xH)) (Fnum x) *)
(* Goal: @eq Z (Z.sub (Fexp x) Z0) (Fexp x) *)
replace (Zpower_nat radix 0) with 1%Z; auto with zarith.
(* Goal: @eq Z (Z.sub (Fexp x) Z0) (Fexp x) *)
simpl in |- *; auto with zarith.
Qed.
 
Theorem FshiftCorrectSym :
 forall x y : float,
 x = y :>R -> exists n : nat, (exists m : nat, Fshift n x = Fshift m y).
(* Goal: forall (x y : float) (_ : @eq R (FtoR x) (FtoR y)), @ex nat (fun n : nat => @ex nat (fun m : nat => @eq float (Fshift n x) (Fshift m y))) *)
intros x y H'.
(* Goal: @ex nat (fun n : nat => @ex nat (fun m : nat => @eq float (Fshift n x) (Fshift m y))) *)
case (Z_le_gt_dec (Fexp x) (Fexp y)); intros H'1.
(* Goal: @ex nat (fun n : nat => @ex nat (fun m : nat => @eq float (Fshift n x) (Fshift m y))) *)
(* Goal: @ex nat (fun n : nat => @ex nat (fun m : nat => @eq float (Fshift n x) (Fshift m y))) *)
exists 0; exists (Zabs_nat (Fexp y - Fexp x)).
(* Goal: @eq float (Fshift (Z.abs_nat (Z.sub (Fexp x) (Fexp y))) x) (Fshift O y) *)
rewrite FshiftO.
(* Goal: @eq float x (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y) *)
(* Goal: @ex nat (fun n : nat => @ex nat (fun m : nat => @eq float (Fshift n x) (Fshift m y))) *)
apply sym_equal.
(* Goal: @eq float (Fshift (Z.abs_nat (Z.sub (Fexp y) (Fexp x))) y) x *)
(* Goal: @ex nat (fun n : nat => @ex nat (fun m : nat => @eq float (Fshift n x) (Fshift m y))) *)
apply FshiftCorrectInv; auto.
(* Goal: @ex nat (fun n : nat => @ex nat (fun m : nat => @eq float (Fshift n x) (Fshift m y))) *)
exists (Zabs_nat (Fexp x - Fexp y)); exists 0.
(* Goal: @eq float (Fshift (Z.abs_nat (Z.sub (Fexp x) (Fexp y))) x) (Fshift O y) *)
rewrite FshiftO.
(* Goal: @eq float (Fshift (Z.abs_nat (Z.sub (Fexp x) (Fexp y))) x) y *)
apply FshiftCorrectInv; auto with zarith.
Qed.
 
Theorem FshiftAdd :
 forall (n m : nat) (p : float), Fshift (n + m) p = Fshift n (Fshift m p).
(* Goal: forall (n m : nat) (p : float), @eq float (Fshift (Init.Nat.add n m) p) (Fshift n (Fshift m p)) *)
intros n m p; case p; unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq Z (Z.sub (Fexp x) Z0) (Fexp x) *)
intros Fnum1 Fexp1; apply floatEq; simpl in |- *; auto with zarith.
(* Goal: @eq Z (Z.mul Fnum1 (Zpower_nat radix (Init.Nat.add n m))) (Z.mul (Z.mul Fnum1 (Zpower_nat radix m)) (Zpower_nat radix n)) *)
(* Goal: @eq Z (Z.sub Fexp1 (Z.of_nat (Init.Nat.add n m))) (Z.sub (Z.sub Fexp1 (Z.of_nat m)) (Z.of_nat n)) *)
rewrite Zpower_nat_is_exp; auto with zarith.
(* Goal: @eq Z (Z.mul Fnum1 (Z.mul (Zpower_nat radix n) (Zpower_nat radix m))) (Z.mul (Z.mul Fnum1 (Zpower_nat radix m)) (Zpower_nat radix n)) *)
(* Goal: @eq Z (Z.sub Fexp1 (Z.of_nat (Init.Nat.add n m))) (Z.sub (Z.sub Fexp1 (Z.of_nat m)) (Z.of_nat n)) *)
rewrite (Zmult_comm (Zpower_nat radix n)); auto with zarith.
(* Goal: @eq Z (Z.sub Fexp1 (Z.of_nat (Init.Nat.add n m))) (Z.sub (Z.sub Fexp1 (Z.of_nat m)) (Z.of_nat n)) *)
rewrite <- (Zminus_plus_simpl_r (Fexp1 - m) n m).
(* Goal: @eq Z (Z.sub Fexp1 (Z.of_nat (Init.Nat.add n m))) (Z.sub (Z.add (Z.sub Fexp1 (Z.of_nat m)) (Z.of_nat m)) (Z.add (Z.of_nat n) (Z.of_nat m))) *)
replace (Fexp1 - m + m)%Z with Fexp1; auto with zarith.
(* Goal: @eq Z (Z.sub Fexp1 (Z.of_nat (Init.Nat.add n m))) (Z.sub Fexp1 (Z.add (Z.of_nat n) (Z.of_nat m))) *)
replace (Z_of_nat (n + m)) with (n + m)%Z; auto with zarith arith.
(* Goal: @eq Z (Z.add (Z.of_nat n) (Z.of_nat m)) (Z.of_nat (Init.Nat.add n m)) *)
rewrite <- inj_plus; auto.
Qed.
 
Theorem ReqGivesEqwithSameExp :
 forall p q : float,
 exists r : float,
   (exists s : float, p = r :>R /\ q = s :>R /\ Fexp r = Fexp s).
intros p q; exists (Fshift (Zabs_nat (Fexp p - Zmin (Fexp p) (Fexp q))) p);
 exists (Fshift (Zabs_nat (Fexp q - Zmin (Fexp p) (Fexp q))) q); 
 repeat split; auto with real.
(* Goal: @eq R (FtoR q) (FtoR (Fshift (Z.abs_nat (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q)))) q)) *)
(* Goal: @eq Z (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q)))) p)) (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q)))) q)) *)
rewrite FshiftCorrect; auto.
(* Goal: @eq R (FtoR q) (FtoR (Fshift (Z.abs_nat (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q)))) q)) *)
(* Goal: @eq Z (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q)))) p)) (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q)))) q)) *)
rewrite FshiftCorrect; auto.
(* Goal: @eq Z (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q)))) p)) (Fexp (Fshift (Z.abs_nat (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q)))) q)) *)
simpl in |- *.
replace (Z_of_nat (Zabs_nat (Fexp p - Zmin (Fexp p) (Fexp q)))) with
 (Fexp p - Zmin (Fexp p) (Fexp q))%Z.
replace (Z_of_nat (Zabs_nat (Fexp q - Zmin (Fexp p) (Fexp q)))) with
 (Fexp q - Zmin (Fexp p) (Fexp q))%Z.
(* Goal: @eq Z (Z.sub (Fexp p) (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q)))) (Z.sub (Fexp q) (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q)))) *)
(* Goal: @eq Z (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q))) (Z.of_nat (Z.abs_nat (Z.sub (Fexp q) (Z.min (Fexp p) (Fexp q))))) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))))) *)
case (Zmin_or (Fexp p) (Fexp q)); intros H'; rewrite H'; auto with zarith.
(* Goal: forall _ : Z.le (Z.min (Fexp p) (Fexp q)) (Fexp q), @eq Z (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))))) *)
rewrite inj_abs; auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))) *)
apply Zplus_le_reg_l with (p := Zmin (Fexp p) (Fexp q)); auto with zarith.
(* Goal: @eq Z (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))))) *)
generalize (Zle_min_r (Fexp p) (Fexp q)); auto with zarith.
(* Goal: forall _ : Z.le (Z.min (Fexp p) (Fexp q)) (Fexp q), @eq Z (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))))) *)
rewrite inj_abs; auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Z.min (Fexp p) (Fexp q))) *)
apply Zplus_le_reg_l with (p := Zmin (Fexp p) (Fexp q)); auto with zarith.
Qed.
 
Theorem FdigitEq :
 forall x y : float,
 ~ is_Fzero x -> x = y :>R -> Fdigit x = Fdigit y -> x = y.
intros x y H' H'0 H'1.
cut (~ is_Fzero y); [ intros NZy | idtac ].
2: red in |- *; intros H'2; case H'.
(* Goal: @eq R (FtoR y) (IZR Z0) *)
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 (Zabs_nat (Fexp y - Fexp x)) y) =
  Fdigit y + Zabs_nat (Fexp y - Fexp x)).
rewrite FshiftCorrectInv; auto.
rewrite <- H'1.
red in |- *; intros H'2.
absurd (0%Z = (Fexp y - Fexp x)%Z); auto with zarith arith.
rewrite <- (inj_abs (Fexp y - Fexp x)); auto with zarith.
apply Zlt_le_weak; auto.
apply FshiftFdigit; auto.
apply sameExpEq; auto.
absurd
 (Fdigit (Fshift (Zabs_nat (Fexp x - Fexp y)) x) =
  Fdigit x + Zabs_nat (Fexp x - Fexp y)).
rewrite FshiftCorrectInv; auto.
rewrite <- H'1.
red in |- *; intros H'2.
absurd (0%Z = (Fexp x - Fexp y)%Z); auto with zarith arith.
rewrite <- (inj_abs (Fexp x - Fexp y)); auto with zarith.
apply Zlt_le_weak; auto.
apply FshiftFdigit; auto.
Qed.
End definitions.
Hint Resolve Rlt_monotony_exp Rle_monotone_exp: real.
Hint Resolve Zlt_not_eq Zlt_not_eq_rev: zarith.