Closest2Prop.v

Require Export ClosestProp.
Section F2.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.

Theorem TwoMoreThanOne: (lt (S O) (2)).
Auto.
Qed.
Hints Resolve TwoMoreThanOne.
Hypothesis precisionNotZero:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).

Theorem FevenNormMin: (Even (nNormMin (2) precision)).
Unfold nNormMin.
Generalize precisionNotZero; Case precision.
Intros H'2; Inversion H'2.
Intros n; Case n.
Intros H'2; Inversion H'2.
Inversion H0.
Intros n0 H'2; Replace (pred (S (S n0))) with (S n0).
Apply EvenExp with b := b radix := (2) precision := precision; Auto.
Apply EvenSS; Auto.
Apply EvenO; Auto.
Simpl; Auto.
Qed.

Theorem EvenFNSuccFNSuccMid:
  (p:float) (Fbounded b p) -> (FNeven b (2) precision p) ->
  <R>
    (Fminus
       (2) (FNSucc b (2) precision (FNSucc b (2) precision p))
       (FNSucc b (2) precision p))==(Fminus (2) (FNSucc b (2) precision p) p).
Intros p H' H'0.
Unfold FtoRradix; Apply FNSuccFNSuccMid; Auto.
Red; Intros H'1; Absurd (FNodd b (2) precision (FNSucc b (2) precision p)); Auto.
Unfold FNodd.
Rewrite FcanonicFormalizeEq; Auto with float arith.
Unfold Fodd.
Rewrite H'1.
Rewrite absolu_INR; Auto with float arith.
Apply EvenNOdd; Auto with float arith.
Apply FevenNormMin; Auto with float arith.
Apply FNevenSuc; Auto.
Red; Intros H'1; Absurd (FNodd b (2) precision (FNSucc b (2) precision p));
Auto with float arith.
Unfold FNodd.
Rewrite FcanonicFormalizeEq; Auto with float arith.
Unfold Fodd.
Rewrite H'1.
Rewrite absolu_Zopp; Rewrite absolu_INR.
Apply EvenNOdd.
Apply FevenNormMin.
Qed.

Theorem EvenD: (n:nat) (Even n) ->(Ex [m:nat] n=(mult (2) m)).
Intros n H'; Elim H'; Auto.
Exists O; Ring.
Intros n0 H'0 H'1; Elim H'1; Intros m E; Clear H'1.
Rewrite E; Exists (S m); Simpl; Repeat Rewrite (plus_sym m); Simpl;
Rewrite (plus_sym m (S m)); Simpl; Auto.
Qed.

Theorem FEvenD:
  (p:float) (Fbounded b p) -> (Feven p) ->
  (Ex [q:float] (Fbounded b q) /\ <R> p==(Rmult (2) q)).
Intros p H' H'0.
Case (EvenD (absolu (Fnum p))); Auto.
Intros x H'1.
Case (Zle_or_lt ZERO (Fnum p)); Intros Zle0.
Exists (Float x (Fexp p)); Split.
Repeat Split; Simpl; Auto.
Apply Zle_trans with (inject_nat O); Auto with zarith arith.
Apply Zle_trans with (inject_nat (mult (2) x)); Auto with zarith arith.
Rewrite <- H'1.
Replace (inject_nat O) with (Zopp (inject_nat O)); Auto with zarith arith.
Apply inj_le.
Apply ZleAbs; Auto; Intuition.
Intuition.
Unfold FtoRradix FtoR; Simpl.
Replace (Fnum p) with (inject_nat (mult (2) x)).
Simpl; AutoRewrite [Rsimpl].
Ring.
Rewrite <- H'1; Apply inj_abs; Auto.
Exists (Float (Zopp x) (Fexp p)); Split.
Repeat Split; Simpl; Auto.
Apply Zle_trans with (Zopp (mult (2) x)); Auto with zarith arith.
Rewrite <- H'1.
Apply Zle_Zopp; Apply inj_le.
Apply ZleAbs; Auto; Intuition.
Apply Zle_trans with (inject_nat O); Auto with zarith arith.
Intuition.
Unfold FtoRradix FtoR; Simpl.
Replace (Fnum p) with (Zopp (mult (2) x)).
Simpl; AutoRewrite [Rsimpl].
Ring.
Rewrite <- H'1.
Rewrite <- absolu_Zopp.
Rewrite inj_abs; Auto.
Ring.
Replace ZERO with (Zopp ZERO).
Apply Zle_Zopp; Auto with zarith.
Simpl; Auto.
Qed.

Theorem FNEvenD:
  (p:float) (Fbounded b p) -> (FNeven b (2) precision p) ->
  (Ex [q:float] (Fbounded b q) /\ <R> p==(Rmult (2) q)).
Intros p H' H'0; Case (FEvenD (Fnormalize (2) b precision p));
Auto with float arith.
Intros x H'1; Elim H'1; Intros H'2 H'3; Clear H'1; Exists x; Split; Auto.
Apply sym_eqT.
Rewrite <- H'3; Auto.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Qed.

Theorem AScal2:
  (p:float)<R> (Float (Fnum p) (Zplus (Fexp p) (1)))==(Rmult (2) p).
Intros p.
Unfold FtoRradix; Rewrite FvalScale; Auto.
Replace (powerRZ (2) (1)) with (INR (2)); [Idtac | Simpl; Ring]; Auto.
Qed.

Theorem div2IsBetween:
  (p:float)
  (min, max:float)
  (Fbounded b p) ->
  (isMin b (2) (Rmult (Rinv (2)) p) min) ->
  (isMax b (2) (Rmult (Rinv (2)) p) max) -><R> p==(Rplus min max).
Intros p min max H' H'0 H'1.
Cut (Rle min (Rmult (Rinv (2)) p));
[Intros Rle0; Case Rle0; Clear Rle0; Intros Rle0 | Intuition].
Cut (Fbounded b (Float (Fnum min) (Zplus (Fexp min) (1))));
[Intros Fb0 | Apply FBoundedScale; Auto; Intuition].
Cut (Rlt (Float (Fnum min) (Zplus (Fexp min) (1))) p); [Intros Rlt0 | Idtac].
2:Rewrite AScal2.
2:Replace (FtoRradix p) with (Rmult (2) (Rmult (Rinv (2)) p)).
2:Apply Rlt_monotony; Auto with real arith.
2:Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real arith.
Case (FNevenOrFNodd b (2) precision (Float (Fnum min) (Zplus (Fexp min) (1))));
Intros Fe0.
Unfold FtoRradix in Rlt0; Case (FNSuccProp b (2) precision) with 6 := Rlt0;
Auto with arith; Intros C0.
Case (FNEvenD
        (FNSucc
           b (2) precision
           (FNSucc b (2) precision (Float (Fnum min) (Zplus (Fexp min) (1))))));
Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Apply FNSuccCanonic; Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Apply FNoddSuc; Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Intros x H'2; Elim H'2; Intros H'3 H'4; Clear H'2.
Absurd (Rle x min).
Apply Rle_not.
Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto.
Rewrite <- H'4.
Rewrite <- AScal2.
Apply Rlt_trans
     with (FtoRradix
             (FNSucc b (2) precision (Float (Fnum min) (Zplus (Fexp min) (1)))));
Auto.
Unfold FtoRradix; Apply FNSuccLt; Auto with float arith.
Unfold FtoRradix; Apply FNSuccLt; Auto with float arith.
Simpl; Auto with real.
Case H'0.
Intros H'2 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Auto.
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real.
Unfold FtoRradix in H'4; Rewrite <- H'4.
Replace (Rmult R1 p) with (FtoRradix p); Auto with real float arith.
Unfold FtoRradix; Apply FNSuccProp; Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Cut (Rle (Rmult (Rinv (2)) p) max);
[Intros Rle1; Case Rle1; Clear Rle1; Intros Rle1 | Intuition].
Cut (Fbounded b (Float (Fnum max) (Zplus (Fexp max) (1))));
[Intros Fb1 | Apply FBoundedScale; Auto; Intuition].
Cut (Rlt p (Float (Fnum max) (Zplus (Fexp max) (1)))); [Intros Rlt0 | Idtac].
2:Rewrite AScal2.
2:Replace (FtoRradix p) with (Rmult (2) (Rmult (Rinv (2)) p)).
2:Apply Rlt_monotony; Auto with real arith.
2:Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real arith.
Unfold FtoRradix in Rlt1; Case (FNSuccProp b (2) precision) with 6 := Rlt1;
Auto with arith; Intros C1.
Case (FNEvenD (FNSucc b (2) precision p)); Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Apply FNoddSuc; Auto.
Apply FNoddEq
     with f1 :=
          (FNSucc b (2) precision (Float (Fnum min) (Zplus (Fexp min) (1))));
Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Intros x H'2; Elim H'2; Intros H'3 H'4; Clear H'2.
Absurd (Rle max x).
Apply Rle_not.
Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- H'4.
Rewrite <- AScal2; Auto.
Case H'1.
Intros H'2 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Auto.
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real.
Unfold FtoRradix in H'4; Rewrite <- H'4.
Replace (Rmult R1 p) with (FtoRradix p); Auto with real.
Apply Rlt_le.
Unfold FtoRradix; Auto with float arith.
Generalize (EvenFNSuccFNSuccMid (Float (Fnum min) (Zplus (Fexp min) (1)))).
Unfold FtoRradix; Repeat Rewrite Fminus_correct; Auto.
Replace (FtoR
           (2)
           (FNSucc
              b (2) precision
              (FNSucc b (2) precision (Float (Fnum min) (Zplus (Fexp min) (1))))))
     with (FtoR (2) (FNSucc b (2) precision p)).
Rewrite C1; Rewrite C0.
Repeat Rewrite AScal2; Auto.
Intros H'2.
Apply Rmult_anticompatibility with r1 := (INR (2)); Auto with real.
Rewrite Rmult_Rplus_distr.
Replace (Rmult (2) (FtoR (2) max))
     with (Rplus (Rminus (Rmult (2) max) (FtoR (2) p)) (FtoR (2) p)).
Rewrite H'2; Auto.
Simpl; Unfold FtoRradix.
Rewrite <- Rplus_assoc.
Replace (Rplus
           (Rmult (Rplus R1 R1) (FtoR (2) min))
           (Rminus (FtoR (2) p) (Rmult (Rplus R1 R1) (FtoR (2) min))))
     with (FtoR (2) p).
Ring.
Ring.
Ring.
Rewrite (FNSuccEq b (2) precision) with p :=
                                        (FNSucc
                                           b (2) precision
                                           (Float
                                              (Fnum min) (Zplus (Fexp min) (1))))
                                        q := p; Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Replace (FtoRradix min) with (FtoRradix max).
Rewrite <- Rle1.
Apply Rmult_anticompatibility with r1 := (INR (2)); Auto with real.
Rewrite Rmult_Rplus_distr.
Repeat Rewrite <- Rmult_assoc; Repeat Rewrite Rinv_r; Auto with real.
Simpl; Ring.
Unfold FtoRradix; Apply MinEq with b := b r := (Rmult (Rinv (2)) p); Auto.
Rewrite Rle1.
Apply RoundedModeProjectorIdem
     with 1 :=
          (MinRoundedModeP
             b (2) precision TwoMoreThanOne precisionNotZero pGivesBound); Auto.
Intuition.
Case (FNEvenD
        (FNSucc b (2) precision (Float (Fnum min) (Zplus (Fexp min) (1)))));
Auto with float arith.
Apply FcanonicBound with radix := (2) precision := precision;
Auto with float arith.
Intros x H'2; Elim H'2; Intros H'3 H'4; Clear H'2.
Absurd (Rle x min).
Apply Rle_not.
Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- H'4.
Rewrite <- AScal2; Auto with float arith.
Unfold FtoRradix; Auto with float arith.
Case H'0.
Intros H'2 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Auto.
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real.
Unfold FtoRradix in H'4; Rewrite <- H'4.
Replace (Rmult R1 p) with (FtoRradix p); Auto with real.
Unfold FtoRradix; Apply FNSuccProp; Auto with float arith.
Replace (FtoRradix max) with (FtoRradix min).
Rewrite Rle0.
Apply Rmult_anticompatibility with r1 := (INR (2)); Auto with real.
Rewrite Rmult_Rplus_distr.
Repeat Rewrite <- Rmult_assoc; Repeat Rewrite Rinv_r; Auto with real.
Simpl; Ring.
Unfold FtoRradix; Apply MaxEq with b := b r := (Rmult (Rinv (2)) p); Auto.
Rewrite <- Rle0.
Apply RoundedModeProjectorIdem
     with 1 :=
          (MaxRoundedModeP
             b (2) precision TwoMoreThanOne precisionNotZero pGivesBound); Auto.
Intuition.
Qed.

Theorem FmultRadixInv:
  (x, z:float)
  (y:R) (Fbounded b x) -> (Closest b (2) y z) -> (Rlt (Rmult (Rinv (2)) x) y) ->
  (Rle (Rmult (Rinv (2)) x) z).
Intros x z y H' H'0 H'1.
Case MinEx with r := (Rmult (Rinv (2)) x) 3 := pGivesBound; Auto with arith.
Intros min isMin.
Case MaxEx with r := (Rmult (Rinv (2)) x) 3 := pGivesBound; Auto with arith.
Intros max isMax.
Case (Rle_or_lt y max); Intros Rl1.
Case Rl1; Clear Rl1; Intros Rl1.
Replace (FtoRradix z) with (FtoRradix max).
Intuition.
Apply sym_eqT.
Unfold FtoRradix; Apply ClosestMaxEq with b := b r := y min := min; Auto.
Apply isMinComp with r1 := (Rmult (Rinv (2)) x) max := max; Auto.
Apply Rle_lt_trans with 2 := H'1; Auto.
Intuition.
Apply isMaxComp with r1 := (Rmult (Rinv (2)) x) min := min; Auto.
Apply Rle_lt_trans with 2 := H'1; Auto.
Intuition.
Replace (Rplus (FtoR (2) min) (FtoR (2) max)) with (FtoRradix x).
Apply Rlt_mult_anticompatibility with z := (Rinv (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_l; AutoRewrite [Rsimpl]; Auto with real.
Apply div2IsBetween; Auto.
Cut (Closest b (2) max z); [Intros C0 | Idtac].
Unfold FtoRradix; Unfold FtoRradix in C0; Rewrite <- ClosestIdem with 2 := C0;
Auto.
Unfold FtoRradix in Rl1; Rewrite <- Rl1; Auto.
Apply Rlt_le; Auto.
Intuition.
Apply (ClosestCompatible b (2) y max z z); Auto.
Intuition.
Apply Rle_trans with (FtoRradix max); Auto.
Intuition.
Apply (ClosestMonotone b (2) (FtoRradix max) y); Auto.
Apply (RoundedModeProjectorIdem b (2) (Closest b (2))); Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Intuition.
Qed.
End F2.
Hints Resolve FevenNormMin :float.

14/12/100, 17:14