(****************************************************************************
                                                                             
          IEEE754  :  Closest2Prop                                                   
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export ClosestProp.
Section F2.
Variable b : Fbound.
Variable precision : nat.
 
Let radix := 2%Z.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
 
Theorem TwoMoreThanOne : (1 < radix)%Z.
(* Goal: Z.lt (Zpos xH) radix *)
unfold radix in |- *; red in |- *; simpl in |- *; auto.
Qed.
Hint Resolve TwoMoreThanOne.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Theorem FevenNormMin : Even (nNormMin 2%nat precision).
(* Goal: Even (nNormMin (Z.of_nat (S (S O))) precision) *)
unfold nNormMin in |- *.
(* Goal: Even (Zpower_nat (Z.of_nat (S (S O))) (Init.Nat.pred precision)) *)
generalize precisionNotZero; case precision.
(* Goal: forall _ : lt (S O) (S O), Even (Zpower_nat (Z.of_nat (S (S O))) (Init.Nat.pred (S O))) *)
(* Goal: forall (n : nat) (_ : lt (S O) (S (S n))), Even (Zpower_nat (Z.of_nat (S (S O))) (Init.Nat.pred (S (S n)))) *)
intros H'2; Contradict H'2; auto with zarith.
(* Goal: forall (n : nat) (_ : lt (S O) (S n)), Even (Zpower_nat (Z.of_nat (S (S O))) (Init.Nat.pred (S n))) *)
intros n; case n.
(* Goal: forall _ : lt (S O) (S O), Even (Zpower_nat (Z.of_nat (S (S O))) (Init.Nat.pred (S O))) *)
(* Goal: forall (n : nat) (_ : lt (S O) (S (S n))), Even (Zpower_nat (Z.of_nat (S (S O))) (Init.Nat.pred (S (S n)))) *)
intros H'2; Contradict H'2; auto with zarith.
(* Goal: forall (n : nat) (_ : lt (S O) (S (S n))), Even (Zpower_nat (Z.of_nat (S (S O))) (Init.Nat.pred (S (S n)))) *)
intros n0 H'2; replace (pred (S (S n0))) with (S n0).
(* Goal: Even (Zpower_nat (Z.of_nat (S (S O))) (S n0)) *)
(* Goal: @eq nat (S n0) (Init.Nat.pred (S (S n0))) *)
apply EvenExp; auto.
(* Goal: Even (Z.of_nat (S (S O))) *)
(* Goal: @eq nat (S n0) (Init.Nat.pred (S (S n0))) *)
exists 1%Z; ring.
(* Goal: @eq nat (S n0) (Init.Nat.pred (S (S n0))) *)
simpl in |- *; auto.
Qed.
 
Theorem EvenFNSuccFNSuccMid :
 forall p : float,
 Fbounded b p ->
 FNeven b radix precision p ->
 Fminus radix (FNSucc b radix precision (FNSucc b radix precision p))
   (FNSucc b radix precision p) = Fminus radix (FNSucc b radix precision p) p
 :>R.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : FNeven b radix precision p), @eq R (FtoRradix (Fminus radix (FNSucc b radix precision (FNSucc b radix precision p)) (FNSucc b radix precision p))) (FtoRradix (Fminus radix (FNSucc b radix precision p) p)) *)
intros p H' H'0.
(* Goal: @eq R (FtoRradix (Fminus radix (FNSucc b radix precision (FNSucc b radix precision p)) (FNSucc b radix precision p))) (FtoRradix (Fminus radix (FNSucc b radix precision p) p)) *)
unfold FtoRradix in |- *; apply FNSuccFNSuccMid; auto.
red in |- *; intros H'1;
 absurd (FNodd b radix precision (FNSucc b radix precision p)); 
 auto.
(* Goal: not (FNodd b radix precision (FNSucc b radix precision p)) *)
unfold FNodd in |- *.
(* Goal: not (Fodd (Fnormalize radix b precision (FNSucc b radix precision p))) *)
rewrite FcanonicFnormalizeEq; auto with float arith.
(* Goal: not (Fodd (FNSucc b radix precision p)) *)
unfold Fodd in |- *.
(* Goal: not (Odd (Fnum (FNSucc b radix precision p))) *)
rewrite H'1.
(* Goal: not (Odd (nNormMin radix precision)) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision p) *)
(* Goal: not (@eq Z (Fnum (FNSucc b radix precision p)) (Z.opp (nNormMin radix precision))) *)
apply EvenNOdd; auto with float arith.
(* Goal: Even (nNormMin radix precision) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision p) *)
(* Goal: not (@eq Z (Fnum (FNSucc b radix precision p)) (Z.opp (nNormMin radix precision))) *)
apply FevenNormMin; auto with float arith.
(* Goal: FNodd b radix precision (FNSucc b radix precision p) *)
(* Goal: not (@eq Z (Fnum (FNSucc b radix precision p)) (Z.opp (nNormMin radix precision))) *)
apply FNevenSuc; auto.
red in |- *; intros H'1;
 absurd (FNodd b radix precision (FNSucc b radix precision p));
 auto with float arith.
(* Goal: not (FNodd b radix precision (FNSucc b radix precision p)) *)
unfold FNodd in |- *.
(* Goal: not (Fodd (Fnormalize radix b precision (FNSucc b radix precision p))) *)
rewrite FcanonicFnormalizeEq; auto with float arith.
(* Goal: not (Fodd (FNSucc b radix precision p)) *)
unfold Fodd in |- *.
(* Goal: not (Odd (Fnum (FNSucc b radix precision p))) *)
rewrite H'1.
(* Goal: not (Odd (Z.opp (nNormMin radix precision))) *)
apply EvenNOdd.
(* Goal: Even (Z.opp (nNormMin radix precision)) *)
apply EvenOpp; apply FevenNormMin.
Qed.
 
Theorem AScal2 :
 forall p : float, Float (Fnum p) (Fexp p + 1%nat) = (radix * p)%R :>R.
(* Goal: forall p : float, @eq R (FtoRradix (Float (Fnum p) (Z.add (Fexp p) (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix p)) *)
intros p.
(* Goal: @eq R (FtoRradix (Float (Fnum p) (Z.add (Fexp p) (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix p)) *)
unfold FtoRradix in |- *; rewrite FvalScale; auto.
replace (powerRZ radix 1%nat) with (INR 2); [ idtac | simpl in |- *; unfold radix; ring ];
 auto.
Qed.
End F2.
Hint Resolve FevenNormMin: float.