FSucc.v
(****************************************************************************
IEEE754 : FSucc
Laurent Thery
*****************************************************************************
*)
Require Import PolyList.
Require Import Float.
Require Import Fnorm.
Require Import Fop.
Require Import Fcomp.
Section suc.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.
Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionNotZero:~ precision=O.
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).
Definition
FSucc :=
[x:float]
Cases (Z_eq_dec (Fnum x) (vNum b)) of
(left _) => (Float (nNormMin radix precision) (Zs (Fexp x)))
| (right _) =>
Cases (Z_eq_dec (Fnum x) (Zopp (nNormMin radix precision))) of
(left _) => Cases (Z_eq_dec (Fexp x) (Zopp (dExp b))) of
(left _) => (Float (Zs (Fnum x)) (Fexp x))
| (right _) =>
(Float (Zopp (vNum b)) (Zpred (Fexp x)))
end
| (right _) => (Float (Zs (Fnum x)) (Fexp x))
end
end.
Theorem
FSuccSimpl1:
(x:float) (Fnum x)=(vNum b) ->
(FSucc x)=(Float (nNormMin radix precision) (Zs (Fexp x))).
Intros x H'; Unfold FSucc.
Case (Z_eq_dec (Fnum x) (vNum b)); Auto.
Intros H'0; Contradict H'0; Auto.
Qed.
Theorem
FSuccSimpl2:
(x:float)
(Fnum x)=(Zopp (nNormMin radix precision)) -> ~ (Fexp x)=(Zopp (dExp b)) ->
(FSucc x)=(Float (Zopp (vNum b)) (Zpred (Fexp x))).
Intros x H' H'0; Unfold FSucc.
Case (Z_eq_dec (Fnum x) (vNum b)); Auto.
Intros H'0; Absurd (Zlt O (vNum b)); Auto with zarith arith.
Apply inj_lt; Apply lt_vNum with 3 := pGivesBound; Auto.
Intros H'1; Case (Z_eq_dec (Fnum x) (Zopp (nNormMin radix precision))).
Intros H'2; Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Auto.
Intros H'3; Contradict H'0; Auto.
Intros H'2; Contradict H'2; Auto.
Qed.
Theorem
FSuccSimpl3:
(FSucc (Float (Zopp (nNormMin radix precision)) (Zopp (dExp b))))=
(Float (Zs (Zopp (nNormMin radix precision))) (Zopp (dExp b))).
Unfold FSucc; Simpl.
Case (Z_eq_dec (Zopp (nNormMin radix precision)) (vNum b)); Auto.
Intros H'0; Absurd (Zlt O (vNum b)); Auto with zarith arith.
Apply inj_lt; Apply lt_vNum with 3 := pGivesBound; Auto.
Intros H';
Case (Z_eq_dec
(Zopp (nNormMin radix precision)) (Zopp (nNormMin radix precision))).
Intros H'0; Case (Z_eq_dec (Zopp (dExp b)) (Zopp (dExp b))); Auto.
Intros H'1; Contradict H'1; Auto.
Intros H'1; Contradict H'1; Auto.
Qed.
Theorem
FSuccSimpl4:
(x:float)
~ (Fnum x)=(vNum b) -> ~ (Fnum x)=(Zopp (nNormMin radix precision)) ->
(FSucc x)=(Float (Zs (Fnum x)) (Fexp x)).
Intros x H' H'0; Unfold FSucc.
Case (Z_eq_dec (Fnum x) (vNum b)); Auto.
Intros H'1; Contradict H'; Auto.
Intros H'1; Case (Z_eq_dec (Fnum x) (Zopp (nNormMin radix precision))); Auto.
Intros H'2; Contradict H'0; Auto.
Qed.
Theorem
FSuccDiff1:
(x:float) ~ (Fnum x)=(Zopp (nNormMin radix precision)) ->
<R> (Fminus radix (FSucc x) x)==(Float (1) (Fexp x)).
Intros x H'.
Case (Z_eq_dec (Fnum x) (vNum b)); Intros H'1.
Rewrite FSuccSimpl1; Auto.
Unfold FtoRradix FtoR Fminus Fopp Fplus; Simpl; Auto.
Repeat Rewrite Zmin_le2; Auto with zarith.
Rewrite <- Zminus_Sn_m; Repeat Rewrite <- Zminus_n_n.
Rewrite absolu_Zs; Auto with zarith; Simpl.
Rewrite Zpower_nat_O; Rewrite Zpower_nat_1.
Rewrite H'1; Rewrite pGivesBound; Unfold nNormMin.
Replace (Zmult (exp radix (pred precision)) radix)
with (inject_nat (exp radix precision)).
Replace (Zplus
(exp radix precision)
(Zmult (Zopp (minus (exp radix precision) (1))) (1)))
with (inject_nat (1)).
Simpl; Auto.
Rewrite Zmult_n_1; Rewrite inj_minus1; Auto with arith; Ring.
Rewrite <- inj_mult; Generalize precisionNotZero; Case precision; Simpl;
Auto with zarith arith.
Rewrite FSuccSimpl4; Auto.
Unfold FtoRradix FtoR Fminus Fopp Fplus; Simpl; Auto.
Repeat Rewrite Zmin_n_n; Repeat Rewrite <- Zminus_n_n; Simpl.
Rewrite Zpower_nat_O; Repeat Rewrite Zmult_n_1.
Replace (Zplus (Zs (Fnum x)) (Zopp (Fnum x))) with (inject_nat (1)).
Simpl; Auto.
Simpl; Unfold Zs; Ring.
Qed.
Theorem
FSuccDiff2:
(x:float)
(Fnum x)=(Zopp (nNormMin radix precision)) -> (Fexp x)=(Zopp (dExp b)) ->
<R> (Fminus radix (FSucc x) x)==(Float (1) (Fexp x)).
Intros x H' H'0; Replace x with (Float (Fnum x) (Fexp x)).
Rewrite H'; Rewrite H'0; Rewrite FSuccSimpl3; Auto.
Unfold FtoRradix FtoR Fminus Fopp Fplus; Simpl; Auto.
Repeat Rewrite Zmin_n_n; Repeat Rewrite <- Zminus_n_n; Auto with zarith.
Simpl; Rewrite Zpower_nat_O; Repeat Rewrite Zmult_n_1.
Rewrite Zplus_S_n; Rewrite Zplus_inverse_r; Simpl; Auto.
Case x; Simpl; Auto.
Qed.
Theorem
FSuccDiff3:
(x:float)
(Fnum x)=(Zopp (nNormMin radix precision)) -> ~ (Fexp x)=(Zopp (dExp b)) ->
<R> (Fminus radix (FSucc x) x)==(Float (1) (Zpred (Fexp x))).
Intros x H' H'1; Rewrite FSuccSimpl2; Auto.
Unfold FtoRradix FtoR Fminus Fopp Fplus; Simpl; Auto.
Repeat Rewrite Zmin_le1; Auto with zarith.
Rewrite <- Zminus_n_n; Rewrite <- Zminus_n_predm; Repeat Rewrite <- Zminus_n_n.
Rewrite absolu_Zs; Auto with zarith; Simpl.
Rewrite Zpower_nat_O; Rewrite Zpower_nat_1.
Rewrite H'; Rewrite pGivesBound; Unfold nNormMin.
Rewrite Zopp_Zopp; Rewrite Zmult_n_1.
Replace (Zmult (exp radix (pred precision)) radix)
with (inject_nat (exp radix precision)).
Replace (Zplus (Zopp (minus (exp radix precision) (1))) (exp radix precision))
with (inject_nat (1)).
Simpl; Auto.
Rewrite inj_minus1; Auto with arith; Ring.
Rewrite <- inj_mult; Generalize precisionNotZero; Case precision; Simpl;
Auto with arith zarith.
Apply Zle_pred_n.
Qed.
Theorem
FSuccNormPos:
(a:float) (Rle R0 a) -> (Fnormal radix b precision a) ->
(Fnormal radix b precision (FSucc a)).
Intros a H' H'0; Unfold FSucc.
Case (Z_eq_dec (Fnum a) (vNum b)); Auto.
Intros H'3; Repeat Split; Simpl; Auto.
Apply Zle_trans with m := (Zopp (INZ O)); Auto with zarith arith.
Replace (Zopp (INZ O)) with (INZ O); Auto with zarith arith.
Apply inj_le; Apply nNrMMimLevNum; Auto.
Apply Zle_trans with m := (Fexp a); Auto with zarith arith.
Intuition.
Unfold Fdigit; Simpl; Rewrite absolu_INR; Apply digitnNormMin with b := b; Auto.
Intros H'3; Case (Z_eq_dec (Fnum a) (Zopp (nNormMin radix precision))).
Intros H'4; Absurd (Zle ZERO (Fnum a)); Auto.
2:Apply LeR0Fnum with radix := radix; Auto with zarith.
Rewrite H'4; Auto.
Apply Zlt_not_le.
Replace ZERO with (Zopp O); Auto with zarith.
Apply Zlt_Zopp; Apply inj_lt.
Apply neq_O_lt; Apply sym_not_equal; Apply nNormNotZero; Auto.
Intros H'4; Repeat Split; Simpl; Auto with zarith arith.
Apply Zle_trans with m := (Fnum a); Auto with zarith arith.
Intuition.
Case (Zle_next (Fnum a) (vNum b)); Auto with zarith arith.
Intuition.
Intuition.
Unfold Fdigit; Simpl; Auto.
Apply digit_bound with x := (nNormMin radix precision) z := (vNum b); Auto.
Apply le_trans with m := (absolu (Fnum a)).
Apply pNormal_absolu_min with 3 := pGivesBound; Auto with zarith arith.
Rewrite absolu_Zs; Auto with zarith arith.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Rewrite absolu_Zs; Auto with zarith arith.
Case (le_next (absolu (Fnum a)) (vNum b)); Auto with arith.
Apply pBounded_absolu; Auto with zarith arith.
Intuition.
Intros H'5; Contradict H'3; Rewrite H'5; Auto with arith.
Rewrite inj_abs; Auto.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Apply digitnNormMin with 3 := pGivesBound; Auto.
Apply digitVNumiSPrecision; Auto.
Qed.
Theorem
FSuccSubnormNotNearNormMin:
(a:float)
(Fsubnormal radix b precision a) ->
~ (Fnum a)=(pred (nNormMin radix precision)) ->
(Fsubnormal radix b precision (FSucc a)).
Intros a H' H'0.
Unfold FSucc.
Case (Z_eq_dec (Fnum a) (vNum b)); Auto.
Intros H'2; Absurd (lt (Fdigit radix a) precision).
Unfold Fdigit; Rewrite H'2; Rewrite absolu_INR;
Rewrite digitVNumiSPrecision with 3 := pGivesBound; Auto with arith.
Intuition.
Intros H'3; Case (Z_eq_dec (Fnum a) (Zopp (nNormMin radix precision))).
Intros H'2; Absurd (lt (Fdigit radix a) precision).
Unfold Fdigit; Rewrite H'2.
Rewrite absolu_Zopp; Rewrite absolu_INR;
Rewrite digitnNormMin with 3 := pGivesBound; Auto with arith.
Intuition.
Intros H'4; Repeat Split; Simpl; Auto with zarith arith.
Apply Zle_trans with m := (Fnum a); Auto with zarith arith.
Intuition.
Case (Zlt_next (Fnum a) (nNormMin radix precision)); Auto with zarith arith.
Apply Zlt_absolu; Auto.
Apply pSubnormal_absolu_min with 3 := pGivesBound; Auto.
Intros H'1; Contradict H'0.
Replace (inject_nat (pred (nNormMin radix precision)))
with (Zpred (nNormMin radix precision)); Auto with zarith arith.
Rewrite H'1; Auto with zarith arith.
Apply Zpred_Sn.
Rewrite inj_pred; Auto.
Apply nNormNotZero; Auto.
Intros H'1; Apply Zle_trans with m := (inject_nat (nNormMin radix precision));
Auto with zarith.
Apply inj_le; Apply nNrMMimLevNum; Auto.
Intuition.
Intuition.
Apply le_lt_trans with m := (pred precision).
Case (Zle_or_lt ZERO (Fnum a)); Intros H'5.
Replace (pred precision) with (digit radix (pred (nNormMin radix precision))).
Unfold Fdigit; Simpl; Auto.
Apply digit_monotone; Auto.
Rewrite absolu_Zs; Auto.
Case (lt_next (absolu (Fnum a)) (nNormMin radix precision)).
Apply pSubnormal_absolu_min with 3 := pGivesBound; Auto.
Intros H'2; Contradict H'0; Rewrite H'2; Simpl; Auto.
Rewrite inj_abs; Auto.
Auto with arith.
Replace (pred (nNormMin radix precision))
with (minus (nNormMin radix precision) (1)).
Unfold nNormMin; Rewrite digit_minus1; Auto.
Case nNormMin; Simpl; Auto with arith.
Apply le_trans with m := (Fdigit radix a); Auto.
Unfold Fdigit; Simpl; Apply digit_monotone; Auto.
Rewrite <- (absolu_Zopp (Fnum a)); Rewrite <- (absolu_Zopp (Zs (Fnum a))).
Apply ZleLe.
Repeat Rewrite inj_abs; Auto with zarith.
Replace ZERO with (Zopp ZERO); Auto with zarith.
Replace ZERO with (Zopp ZERO); Auto with zarith.
Apply lt_le_pred; Intuition.
Generalize precisionNotZero; Auto with zarith.
Qed.
Theorem
FSuccSubnormNearNormMin:
(a:float)
(Fsubnormal radix b precision a) ->
(Fnum a)=(pred (nNormMin radix precision)) ->
(Fnormal radix b precision (FSucc a)).
Intros a H' H'0.
Unfold FSucc.
Case (Z_eq_dec (Fnum a) (vNum b)); Auto.
Intros H'1; Absurd (le (nNormMin radix precision) (vNum b)); Auto.
Replace (vNum b) with (pred (nNormMin radix precision)).
Apply lt_not_le.
Generalize (nNormNotZero ? radixMoreThanOne precision); Auto with zarith.
Apply inject_nat_eq; Auto.
Rewrite <- H'1; Auto.
Apply nNrMMimLevNum; Auto.
Intros H'3; Case (Z_eq_dec (Fnum a) (Zopp (nNormMin radix precision))).
Intros H'1;
Absurd (Zlt
(Zopp (nNormMin radix precision)) (pred (nNormMin radix precision))).
Rewrite <- H'1; Rewrite <- H'0; Auto with zarith.
Rewrite <- H'1.
Apply Zle_lt_trans with m := (inject_nat (absolu (Fnum a))); Auto.
Apply Zle_abs; Auto.
Case (Zlt_next (absolu (Fnum a)) (nNormMin radix precision));
Auto with zarith arith.
Apply inj_lt.
Apply pSubnormal_absolu_min with 3 := pGivesBound; Auto.
Intros H'4; Repeat Split; Simpl; Auto with zarith arith.
Apply Zle_trans with m := (inject_nat (nNormMin radix precision)); Auto.
Apply Zlt_n_Sm_le.
Apply Zlt_n_S.
Apply Zle_lt_trans with m := (inject_nat (absolu (Fnum a))).
Apply Zle_abs; Auto.
Apply inj_lt.
Apply pSubnormal_absolu_min with 3 := pGivesBound; Auto.
Apply inj_le.
Apply nNrMMimLevNum; Auto.
Intuition.
Intuition.
Unfold Fdigit; Simpl; Rewrite H'0.
Rewrite absolu_Zs.
Rewrite absolu_INR.
Replace (S (pred (nNormMin radix precision))) with (nNormMin radix precision).
Apply digitnNormMin with 3 := pGivesBound; Auto.
Generalize (nNormNotZero ? radixMoreThanOne precision);
Case (nNormMin radix precision); Auto.
Intros H'; Case H'; Auto.
Replace ZERO with (inject_nat O); Try Apply inj_le; Auto with arith zarith.
Qed.
Theorem
FBoundedSuc: (f:float) (Fbounded b f) ->(Fbounded b (FSucc f)).
Intros f H'; Unfold FSucc.
Case (Z_eq_dec (Fnum f) (vNum b)); Intros H'1.
Repeat Split; Simpl; Auto with zarith arith.
Generalize nNrMMimLevNum; Auto with zarith arith.
Apply Zle_trans with (Fexp f); Auto with zarith arith; Intuition.
Case (Z_eq_dec (Fnum f) (Zopp (nNormMin radix precision))); Intros H'2.
Case (Z_eq_dec (Fexp f) (Zopp (dExp b))); Intros H'3.
Repeat Split; Simpl; Auto with zarith arith.
Apply Zle_trans with (Fnum f); Auto with zarith arith; Intuition.
Repeat Split; Simpl; Auto with zarith arith.
Case (Zle_next (Zopp (dExp b)) (Fexp f)); Auto with zarith arith.
Intuition.
Unfold Zs Zpred; Auto with zarith arith.
Repeat Split; Simpl; Auto with zarith arith.
Apply Zle_trans with (Fnum f); Auto with zarith arith; Intuition.
Case (Zle_next (Fnum f) (vNum b)); Auto with zarith arith.
Intuition.
Intuition.
Qed.
Theorem
FSuccSubnormal:
(a:float) (Fsubnormal radix b precision a) ->
(Fcanonic radix b precision (FSucc a)).
Intros a H'; Case (Z_eq_dec (Fnum a) (pred (nNormMin radix precision)));
Intros H'1.
Left; Apply FSuccSubnormNearNormMin; Auto.
Right; Apply FSuccSubnormNotNearNormMin; Auto.
Qed.
Theorem
FSuccPosNotMax:
(a:float) (Rle R0 a) -> (Fcanonic radix b precision a) ->
(Fcanonic radix b precision (FSucc a)).
Intros a H' H'0; Case H'0; Intros H'2.
Left; Apply FSuccNormPos; Auto.
Apply FSuccSubnormal; Auto.
Qed.
Theorem
FSuccNormNegNotNormMin:
(a:float)
(Rle a R0) ->
(Fnormal radix b precision a) ->
~ a=(Float (Zopp (nNormMin radix precision)) (Zopp (dExp b))) ->
(Fnormal radix b precision (FSucc a)).
Intros a H' H'0 H'1.
Cut (Zle (Fnum a) ZERO); [Intros Z0 | Apply R0LeFnum with radix := radix];
Auto with zarith.
Case (Zle_lt_or_eq ? ? Z0); Intros Z1.
2:Absurd (Fdigit radix a)=precision.
2:Unfold Fdigit; Simpl; Rewrite Z1; Simpl; Rewrite digitO; Auto.
2:Intuition.
Unfold FSucc.
Case (Z_eq_dec (Fnum a) (vNum b)); Auto.
Intros H'2; Absurd (Zlt ZERO (Fnum a)); Auto with zarith arith.
Intros H'3; Case (Z_eq_dec (Fnum a) (Zopp (nNormMin radix precision))); Auto.
Intros H'2; Case (Z_eq_dec (Fexp a) (Zopp (dExp b))).
Intros H'3; Contradict H'1; Auto.
Apply floatEq; Auto.
Intros H'4; Repeat Split; Simpl; Auto with zarith.
2:Unfold Fdigit; Simpl; Auto.
2:Rewrite absolu_Zopp; Rewrite absolu_INR; Auto.
2:Rewrite digitVNumiSPrecision with 3 := pGivesBound; Auto.
Apply Zle_S_n; Auto with zarith.
Replace (Zs (Zpred (Fexp a))) with (Fexp a); Auto with zarith.
Case (Zle_next (Zopp (dExp b)) (Fexp a)); Auto with zarith.
Intuition.
Intros H'2; Repeat Split; Simpl; Auto with zarith arith.
Apply Zle_trans with m := (Fnum a); Auto with zarith.
Intuition.
Intuition.
Unfold Fdigit; Simpl.
Apply digit_bound with x := (nNormMin radix precision) z := (absolu (Fnum a));
Auto.
2:Rewrite <- (absolu_Zopp (Fnum a)); Rewrite <- (absolu_Zopp (Zs (Fnum a))).
2:Apply ZleLe.
2:Repeat Rewrite inj_abs; Auto with zarith.
2:Apply digitnNormMin with 3 := pGivesBound; Auto.
2:Intuition.
Rewrite <- (absolu_Zopp (Zs (Fnum a))).
Apply ZleLe.
Repeat Rewrite inj_abs; Auto with zarith.
Apply Zle_S_n.
Replace (Zs (Zopp (Zs (Fnum a)))) with (Zopp (Fnum a)); Auto with zarith.
Case (Zle_next (nNormMin radix precision) (Zopp (Fnum a))); Auto.
2:Intros H'4; Contradict H'2; Rewrite <- H'4; Auto with zarith.
Rewrite <- (inj_abs (Zopp (Fnum a))); Auto with zarith.
Rewrite absolu_Zopp.
Apply inj_le; Auto.
Apply pNormal_absolu_min with 3 := pGivesBound; Auto.
Qed.
Theorem
FSuccNormNegNormMin:
(Fsubnormal
radix b precision
(FSucc (Float (Zopp (nNormMin radix precision)) (Zopp (dExp b))))).
Unfold FSucc; Simpl.
Case (Z_eq_dec (Zopp (nNormMin radix precision)) (vNum b)); Intros H'; Auto.
Absurd (Zlt O (vNum b)); Auto.
Rewrite <- H'; Auto with zarith.
Apply inj_lt.
Apply lt_vNum with 3 := pGivesBound; Auto.
Case (Z_eq_dec
(Zopp (nNormMin radix precision)) (Zopp (nNormMin radix precision)));
Intros H'0.
2:Contradict H'0; Auto.
Case (Z_eq_dec (Zopp (dExp b)) (Zopp (dExp b))); Intros H'1.
2:Contradict H'1; Auto.
Repeat Split; Simpl; Auto with zarith.
Apply Zle_trans with m := (Zopp (nNormMin radix precision)); Auto with zarith.
Apply Zle_Zopp; Auto.
Apply inj_le.
Apply nNrMMimLevNum; Auto.
Unfold Fdigit; Simpl.
Replace (absolu (Zs (Zopp (nNormMin radix precision))))
with (minus (exp radix (pred precision)) (1)).
Rewrite digit_minus1; Auto with zarith.
Unfold nNormMin.
Cut (x, y:nat) (S x)=(S y) ->x=y; [Intros H'2; Apply H'2 | Auto with arith].
Rewrite absolu_Zs_neg.
Rewrite absolu_Zopp; Rewrite absolu_INR.
Rewrite minus_Sn_m; Simpl; Auto with zarith arith.
Replace ZERO with (Zopp (INZ O)); Auto with zarith arith.
Qed.
Theorem
FSuccNegCanonic:
(a:float) (Rle a R0) -> (Fcanonic radix b precision a) ->
(Fcanonic radix b precision (FSucc a)).
Intros a H' H'0; Case H'0; Intros H'1.
Case (floatDec a (Float (Zopp (nNormMin radix precision)) (Zopp (dExp b))));
Intros H'2.
Rewrite H'2; Right; Apply FSuccNormNegNormMin; Auto.
Left; Apply FSuccNormNegNotNormMin; Auto.
Apply FSuccSubnormal; Auto.
Qed.
Theorem
FSuccCanonic:
(a:float) (Fcanonic radix b precision a) ->
(Fcanonic radix b precision (FSucc a)).
Intros a H'.
Case (Rle_or_lt R0 a); Intros H'3.
Apply FSuccPosNotMax; Auto.
Apply FSuccNegCanonic; Auto with real.
Apply Rlt_le; Auto.
Qed.
Theorem
FSuccLt: (a:float)(Rlt a (FSucc a)).
Intros a; Unfold FSucc.
Case (Z_eq_dec (Fnum a) (vNum b)); Auto.
Intros H'; Unfold FtoRradix FtoR; Simpl; Rewrite H'.
Rewrite pGivesBound; Unfold nNormMin.
Rewrite powerRZ_Zs; Auto with real arith.
Repeat Rewrite <- Rmult_assoc.
Repeat Rewrite <- INR_IZR_INZ.
Replace (Rmult (exp radix (pred precision)) radix)
with (INR (exp radix precision)).
Apply Rlt_monotony_r; Auto with real arith.
Apply Rlt_INR.
Generalize (expLess ? radixMoreThanOne precision); Auto with zarith.
Pattern 1 precision; Replace precision with (S (pred precision)).
Simpl; AutoRewrite [Rsimpl].
Rewrite (Rmult_sym radix); Auto.
Generalize precisionNotZero; Auto with zarith.
Intros H'; Case (Z_eq_dec (Fnum a) (Zopp (nNormMin radix precision))).
Intros H'0; Case (Z_eq_dec (Fexp a) (Zopp (dExp b))).
Intros H'1; Unfold FtoRradix FtoR; Simpl.
Apply Rlt_monotony_r; Auto with real zarith.
Intros H'1; Unfold FtoRradix FtoR; Simpl; Rewrite H'0.
Pattern 1 (Fexp a); Replace (Fexp a) with (Zs (Zpred (Fexp a))).
Rewrite powerRZ_Zs; Auto with real arith.
Repeat Rewrite <- Rmult_assoc.
Apply Rlt_monotony_r; Auto with real zarith.
Rewrite pGivesBound.
Unfold nNormMin.
Simpl; AutoRewrite [Rsimpl]; Auto with arith.
Apply Rgt_Ropp; Red.
Rewrite <- minus_INR; Auto with real arith.
Rewrite <- Rmult_INR.
Apply Rlt_INR.
Replace (mult (exp radix (pred precision)) radix) with (exp radix precision).
Generalize (expLess ? radixMoreThanOne precision); Auto with zarith.
Generalize precisionNotZero; Case precision; Simpl; Auto with zarith arith.
Unfold Zs Zpred; Auto with zarith.
Intros H'1; Unfold FtoRradix FtoR; Simpl.
Apply Rlt_monotony_r; Auto with real zarith.
Qed.
Theorem
FSuccPropPos:
(x, y:float)
(Rle R0 x) ->
(Fcanonic radix b precision x) ->
(Fcanonic radix b precision y) -> (Rlt x y) ->(Rle (FSucc x) y).
Intros x y H' H'0 H'1 H'2.
Case FcanonicLtPos with p := x q := y 3 := pGivesBound; Auto.
Case (Z_eq_dec (Fnum x) (vNum b)); Intros H'4.
Rewrite FSuccSimpl1; Auto.
Intros H'5; Case (Zlt_next ? ? H'5); Intros H'6.
Replace y with (Float (Fnum y) (Fexp y)).
Rewrite H'6.
Generalize Fle_Zle; Unfold Fle FtoRradix; Intros H'7; Apply H'7; Clear H'7;
Auto with arith.
Rewrite <- (inj_abs (Fnum y)); Auto.
Apply inj_le; Auto.
Apply pNormal_absolu_min with 3 := pGivesBound; Auto.
Case H'1; Auto.
Intros H'7; Contradict H'5.
Apply Zle_not_lt.
Replace (Fexp y) with (Zopp (dExp b)).
Intuition.
Apply sym_equal; Intuition.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Apply Rle_trans with r2 := (FtoR radix x); Auto with real.
Apply Rlt_le; Auto.
Case y; Simpl; Auto.
Apply Rlt_le; Auto.
Unfold FtoRradix; Apply FcanonicPosFexpRlt with 3 := pGivesBound; Auto.
Apply LeFnumZERO with radix := radix; Auto with zarith.
Simpl; Auto with zarith.
Apply Rle_trans with r2 := (FtoR radix x); Auto with real.
Apply Rlt_le; Auto with real.
Rewrite <- FSuccSimpl1; Auto.
Apply FSuccCanonic; Auto.
Intros H'5; Apply Rlt_le.
Unfold FtoRradix; Apply FcanonicPosFexpRlt with 3 := pGivesBound; Auto.
Apply Rle_trans with r2 := (FtoR radix x); Auto.
Apply Rlt_le; Auto.
Apply FSuccLt; Auto.
Apply Rle_trans with r2 := (FtoR radix x); Auto with real.
Apply Rlt_le; Auto with real.
Apply FSuccCanonic; Auto.
Rewrite FSuccSimpl4; Auto.
Apply sym_not_equal; Apply Zlt_not_eq.
Apply Zlt_le_trans with m := ZERO; Auto with zarith.
Replace ZERO with (Zopp O); Auto with zarith.
Apply Zlt_Zopp.
Apply inj_lt; Auto.
Generalize (nNormNotZero ? radixMoreThanOne precision); Auto with zarith.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Intros H'4; Elim H'4; Intros H'5 H'6; Clear H'4.
Case (Z_eq_dec (Fnum x) (vNum b)); Intros H'4.
Contradict H'6; Auto.
Rewrite H'4; Auto.
Apply Zle_not_lt; Intuition.
Case (Zlt_next ? ? H'6); Intros H'7.
Rewrite FSuccSimpl4; Auto.
Rewrite <- H'7; Rewrite H'5; Unfold FtoRradix FtoR; Simpl; Auto with real.
Apply sym_not_equal; Apply Zlt_not_eq.
Apply Zlt_le_trans with m := ZERO; Auto with zarith.
Replace ZERO with (Zopp O); Auto with zarith.
Apply Zlt_Zopp.
Apply inj_lt; Auto.
Generalize (nNormNotZero ? radixMoreThanOne precision); Auto with zarith.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Apply Rlt_le; Auto with real.
Rewrite FSuccSimpl4; Auto.
Replace y with (Float (Fnum y) (Fexp y)).
Rewrite H'5.
Generalize Flt_Zlt; Unfold Flt FtoRradix; Intros H'8; Apply H'8; Auto with arith.
Case y; Simpl; Auto.
Apply sym_not_equal; Apply Zlt_not_eq.
Apply Zlt_le_trans with m := ZERO; Auto with zarith.
Replace ZERO with (Zopp O); Auto with zarith.
Apply Zlt_Zopp.
Apply inj_lt; Auto.
Generalize (nNormNotZero ? radixMoreThanOne precision); Auto with zarith.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Qed.
Theorem
R0RltRleSucc: (x:float) (Rlt x R0) ->(Rle (FSucc x) R0).
Intros a H'; Unfold FSucc.
Case (Z_eq_dec (Fnum a) (vNum b)); Auto.
Intros H'0; Absurd (Zlt (Fnum a) ZERO); Auto.
Rewrite H'0; Auto with zarith arith.
Apply R0LtFnum with radix := radix; Auto with zarith.
Case (Z_eq_dec (Fnum a) (Zopp (nNormMin radix precision))); Intros H'1.
Case (Z_eq_dec (Fexp a) (Zopp (dExp b))); Intros H'2.
Intros H'0.
Apply LeZEROFnum with radix := radix; Simpl; Auto with zarith.
Apply Zlt_le_S.
Apply R0LtFnum with radix := radix; Auto with zarith.
Intros H'0.
Apply LeZEROFnum with radix := radix; Simpl; Auto with zarith.
Intros H'0.
Apply LeZEROFnum with radix := radix; Simpl; Auto with zarith.
Apply Zlt_le_S.
Apply R0LtFnum with radix := radix; Auto with zarith.
Qed.
Theorem
FSuccPropNeg:
(x, y:float)
(Rlt x R0) ->
(Fcanonic radix b precision x) ->
(Fcanonic radix b precision y) -> (Rlt x y) ->(Rle (FSucc x) y).
Intros x y H' H'0 H'1 H'2.
Case (Rle_or_lt R0 y); Intros Rle0.
Apply Rle_trans with r2 := R0; Auto.
Apply R0RltRleSucc; Auto.
Cut ~ (Fnum x)=(vNum b);
[Intros N0 |
Apply Zlt_not_eq; Apply Zlt_trans with m := ZERO;
[Apply R0LtFnum with radix := radix |
Replace ZERO with (INZ O);
Generalize (lt_vNum ? radixMoreThanOne ? ? precisionNotZero pGivesBound)]];
Auto with zarith.
Case (Z_eq_dec (Fnum x) (Zopp (nNormMin radix precision))); Intros H'4.
Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Intros H'4.
Replace x with (Float (Fnum x) (Fexp x)).
Rewrite H'3; Rewrite H'4; Rewrite FSuccSimpl3; Auto.
Case FcanonicLtNeg with p := x q := y 3 := pGivesBound; Auto.
Apply Rlt_le; Auto with real.
Intros H'6; Contradict H'6; Rewrite H'3; Apply Zle_not_lt; Intuition.
Intros H'6; Elim H'6; Intros H'7 H'8; Clear H'6;
Replace y with (Float (Fnum y) (Fexp y)).
Rewrite <- H'7; Rewrite H'3.
Generalize Fle_Zle; Unfold Fle FtoRradix; Intros H'9; Apply H'9; Clear H'9;
Auto with arith.
Rewrite <- H'4; Auto with zarith.
Case y; Auto.
Case x; Auto.
Rewrite FSuccSimpl2; Auto.
Case FcanonicLtNeg with p := x q := y 3 := pGivesBound; Auto.
Apply Rlt_le; Auto with real.
Intros H'6; Replace y with (Float (Fnum y) (Fexp y)).
Case (Zlt_next ? ? H'6); Intros H'7.
Rewrite H'7.
Rewrite <- Zpred_Sn.
Generalize Fle_Zle; Unfold Fle FtoRradix; Intros H'8; Apply H'8; Clear H'8;
Auto with arith.
Intuition.
Apply Rlt_le; Auto with real.
Unfold FtoRradix; Apply FcanonicNegFexpRlt with 3 := pGivesBound; Auto.
Apply Rlt_le; Auto.
Rewrite <- FSuccSimpl2; Auto.
Apply R0RltRleSucc; Auto.
Rewrite <- FSuccSimpl2; Auto.
Apply FSuccCanonic; Auto.
Simpl; Auto.
Apply Zlt_S_n; Auto.
Rewrite <- Zs_pred; Auto with zarith.
Case y; Auto.
Intros H'6; Elim H'6; Intros H'7 H'8; Clear H'6; Apply Rlt_le.
Contradict H'8; Rewrite H'4.
Apply Zle_not_lt.
Replace (Fnum y) with (Zopp (absolu (Fnum y))).
Apply Zle_Zopp.
Apply inj_le.
Apply pNormal_absolu_min with 3 := pGivesBound; Auto.
Case H'1; Auto.
Intros H'6; Contradict H'3; Rewrite H'7.
Intuition.
Rewrite <- absolu_Zopp.
Rewrite inj_abs; Auto with zarith.
Replace ZERO with (Zopp ZERO); Auto with zarith.
Apply Zle_Zopp.
Apply R0LeFnum with radix := radix; Auto with zarith.
Apply Rlt_le; Auto.
Rewrite FSuccSimpl4; Auto.
Case FcanonicLtNeg with p := x q := y 3 := pGivesBound; Auto.
Apply Rlt_le; Auto with real.
Intros H'5; Apply Rlt_le; Auto.
Unfold FtoRradix; Apply FcanonicNegFexpRlt with 3 := pGivesBound; Auto.
Apply Rlt_le; Auto.
Rewrite <- FSuccSimpl4; Auto.
Apply R0RltRleSucc; Auto.
Rewrite <- FSuccSimpl4; Auto.
Apply FSuccCanonic; Auto.
Intros H'5; Elim H'5; Intros H'6 H'7; Clear H'5.
Replace y with (Float (Fnum y) (Fexp y)).
Rewrite H'6.
Generalize Fle_Zle; Unfold Fle FtoRradix; Intros H'8; Apply H'8; Clear H'8;
Auto with zarith arith.
Case y; Auto.
Qed.
Theorem
FSuccProp:
(x, y:float)
(Fcanonic radix b precision x) ->
(Fcanonic radix b precision y) -> (Rlt x y) ->(Rle (FSucc x) y).
Intros x y H' H'0 H'1; Case (Rle_or_lt R0 x); Intros H'2.
Apply FSuccPropPos; Auto.
Apply FSuccPropNeg; Auto.
Qed.
Theorem
Zeq_Zs: (p, q:Z) (Zle p q) -> (Zlt q (Zs p)) ->p=q.
Auto with zarith.
Qed.
Theorem
FSuccZleEq:
(p, q:float) (Rle p q) -> (Rlt q (FSucc p)) -> (Zle (Fexp p) (Fexp q)) ->
<R> p==q.
Intros p q H'.
Case (Z_eq_dec (Fnum p) (vNum b)); Intros H'0.
Rewrite FSuccSimpl1; Simpl; Auto with arith.
Intros H'1 H'2.
Replace p with (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q).
Unfold FtoRradix; Rewrite FshiftCorrect; Auto with real.
Cut (Fexp (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q))=(Fexp p);
[Intros Eq0 | Idtac].
Apply floatEq; Auto.
Apply sym_equal; Apply Zeq_Zs; Auto.
Apply Rle_Fexp_eq_Zle with radix := radix; Auto with arith.
Rewrite FshiftCorrect; Auto.
Replace (Zs (Fnum p)) with (Fnum (Fshift radix (1) (FSucc p))); Auto.
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with arith.
Repeat Rewrite FshiftCorrect; Auto.
Rewrite FSuccSimpl1; Simpl; Auto with arith.
Unfold Fshift; Simpl.
Rewrite FSuccSimpl1; Simpl; Auto with arith.
Rewrite inj_abs; Auto with zarith.
Unfold Fshift; Simpl.
Rewrite FSuccSimpl1; Simpl; Auto with arith.
Rewrite Zpower_nat_1.
Rewrite H'0.
Unfold nNormMin.
Rewrite <- inj_mult.
Rewrite pGivesBound; Auto.
Rewrite inj_minus1; Auto with zarith arith.
Pattern 2 precision; Replace precision with (S (pred precision));
Auto with zarith.
Simpl; Rewrite mult_sym; Auto with zarith.
Unfold Fshift; Simpl.
Rewrite inj_abs; Auto with zarith.
Case (Z_eq_dec (Fnum p) (Zopp (nNormMin radix precision))); Intros H'1.
Case (Z_eq_dec (Fexp p) (Zopp (dExp b))); Intros H'2.
Pattern 1 p; Replace p with (Float (Fnum p) (Fexp p)).
Rewrite H'1; Rewrite H'2.
Rewrite FSuccSimpl3; Auto with arith.
Intros H'3 H'4.
Replace p with (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q).
Unfold FtoRradix; Rewrite FshiftCorrect; Auto with real.
Cut (Fexp (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q))=(Fexp p);
[Intros Eq0 | Idtac].
Apply floatEq; Auto.
Apply sym_equal; Apply Zeq_Zs; Auto.
Apply Rle_Fexp_eq_Zle with radix := radix; Auto with arith.
Rewrite FshiftCorrect; Auto.
Replace (Zs (Fnum p)) with (Fnum (FSucc p)); Auto.
Pattern 2 p; Replace p with (Float (Fnum p) (Fexp p)).
Rewrite H'1; Rewrite H'2.
Rewrite FSuccSimpl3; Auto with arith.
Rewrite <- H'2.
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with arith.
Rewrite FshiftCorrect; Auto.
Rewrite H'2; Auto.
Case p; Simpl; Auto.
Pattern 1 p; Replace p with (Float (Fnum p) (Fexp p)).
Rewrite H'1; Rewrite H'2.
Rewrite FSuccSimpl3; Auto with arith.
Case p; Simpl; Auto.
Unfold Fshift; Simpl.
Rewrite inj_abs; Auto with zarith.
Case p; Simpl; Auto.
Rewrite FSuccSimpl2; Auto with arith.
Intros H'3 H'4.
Unfold FtoRradix; Rewrite <- FshiftCorrect with n := (1) x := p; Auto.
Replace (Fshift radix (1) p)
with (Fshift radix (S (absolu (Zminus (Fexp q) (Fexp p)))) q).
Repeat Rewrite FshiftCorrect; Auto with real.
Cut (Fexp (Fshift radix (S (absolu (Zminus (Fexp q) (Fexp p)))) q))=
(Fexp (Fshift radix (1) p)); [Intros Eq0 | Idtac].
Apply floatEq; Auto.
Apply sym_equal; Apply Zeq_Zs; Auto.
Apply Rle_Fexp_eq_Zle with radix := radix; Auto with arith.
Repeat Rewrite FshiftCorrect; Auto.
Replace (Zs (Fnum (Fshift radix (1) p))) with (Fnum (FSucc p)); Auto.
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with arith.
Repeat Rewrite FshiftCorrect; Auto.
Rewrite FSuccSimpl2; Auto with arith.
Rewrite FSuccSimpl2; Auto with arith.
Rewrite FSuccSimpl2; Auto with arith.
Unfold Fshift; Simpl.
Rewrite Zpower_nat_1; Auto.
Rewrite pGivesBound; Rewrite H'1; Unfold nNormMin.
Rewrite Zopp_Zmult.
Rewrite <- inj_mult.
Rewrite inj_minus1; Auto with zarith arith.
Pattern 1 precision; Replace precision with (S (pred precision));
Auto with zarith.
Simpl; Rewrite mult_sym; Auto with zarith.
Rewrite <- absolu_Zs; Auto with zarith.
Unfold Fshift; Simpl.
Rewrite inj_abs; Auto with zarith.
Rewrite FSuccSimpl4; Auto.
Intros H'2 H'3.
Replace p with (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q).
Unfold FtoRradix; Rewrite FshiftCorrect; Auto with real.
Cut (Fexp (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q))=(Fexp p);
[Intros Eq0 | Idtac].
Apply floatEq; Auto.
Apply sym_equal; Apply Zeq_Zs; Auto.
Apply Rle_Fexp_eq_Zle with radix := radix; Auto with arith.
Rewrite FshiftCorrect; Auto.
Replace (Zs (Fnum p)) with (Fnum (FSucc p)); Auto.
Rewrite FSuccSimpl4; Auto.
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with arith.
Repeat Rewrite FshiftCorrect; Auto.
Rewrite FSuccSimpl4; Auto.
Unfold Fshift; Simpl.
Rewrite inj_abs; Auto with zarith.
Qed.
Definition
FNSucc := [x:?](FSucc (Fnormalize radix b precision x)).
Theorem
FNSuccCanonic:
(a:float) (Fbounded b a) ->(Fcanonic radix b precision (FNSucc a)).
Intros a H'; Unfold FNSucc.
Apply FSuccCanonic; Auto with float.
Qed.
Theorem
FNSuccLt: (a:float)(Rlt a (FNSucc a)).
Intros a; Unfold FNSucc.
Unfold FtoRradix;
Rewrite <- (FnormalizeCorrect ? radixMoreThanOne b precision a).
Apply FSuccLt; Auto.
Qed.
Theorem
FNSuccProp:
(x, y:float) (Fbounded b x) -> (Fbounded b y) -> (Rlt x y) ->
(Rle (FNSucc x) y).
Intros x y H' H'0 H'1; Unfold FNSucc.
Replace (FtoRradix y) with (FtoRradix (Fnormalize radix b precision y)).
Apply FSuccProp; Auto with float.
Unfold FtoRradix; Repeat Rewrite FnormalizeCorrect; Auto.
Unfold FtoRradix; Repeat Rewrite FnormalizeCorrect; Auto.
Qed.
Theorem
FNSuccEq:
(p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==q ->
(FNSucc p)=(FNSucc q).
Intros p q H' H'0 H'1; Unfold FNSucc.
Replace (Fnormalize radix b precision p) with (Fnormalize radix b precision q);
Auto.
Apply FcanonicUnique with radix := radix b := b precision := precision;
Auto with float.
Repeat Rewrite FnormalizeCorrect; Auto.
Qed.
End suc.
Hints Resolve
FSuccNormPos FBoundedSuc FSuccSubnormal FSuccNegCanonic FSuccCanonic FSuccLt
FSuccPropPos R0RltRleSucc FSuccPropNeg FSuccProp FNSuccCanonic FNSuccLt :float.
Section suc1.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.
Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionNotZero:(lt (S O) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).
Theorem
nNormMimLtvNum: (lt (nNormMin radix precision) (vNum b)).
Rewrite pGivesBound; Unfold nNormMin.
Apply simpl_lt_plus_l with p := (1).
Rewrite <- le_plus_minus; Auto with arith.
Apply lt_le_trans with (mult radix (exp radix (pred precision))).
Apply lt_le_trans with (mult (2) (exp radix (pred precision))).
Replace (mult (2) (exp radix (pred precision)))
with (plus (exp radix (pred precision)) (exp radix (pred precision)));
[Idtac | Simpl]; Auto.
Apply lt_reg_r; Auto.
Apply le_lt_trans with (pred precision); Auto with arith.
Apply lte_comp_mult; Auto.
Generalize precisionNotZero; Case precision; Simpl; Auto.
Intros H'0; Inversion H'0.
Qed.
Theorem
FSucFSucMid:
(p:float)
~ (Fnum (FSucc b radix precision p))=(nNormMin radix precision) ->
~ (Fnum (FSucc b radix precision p))=(Zopp (nNormMin radix precision)) ->
<R>
(Fminus
radix (FSucc b radix precision (FSucc b radix precision p))
(FSucc b radix precision p))==
(Fminus radix (FSucc b radix precision p) p).
Intros p.
Case (Z_eq_dec (Fnum p) (Zopp (nNormMin radix precision))); Intros H'1.
Case (Z_eq_dec (Fexp p) (Zopp (dExp b))); Intros H'2.
Rewrite FSuccDiff2 with 4 := H'1; Auto with arith.
Replace p with (Float (Fnum p) (Fexp p)).
Repeat (Rewrite H'1; Rewrite H'2).
Rewrite FSuccSimpl3; Auto with arith.
Rewrite FSuccDiff1 with 3 := pGivesBound; Auto with arith.
Simpl; Auto with zarith.
Apply floatEq; Auto.
Unfold FtoRradix; Rewrite FSuccDiff3 with x := p 3 := pGivesBound;
Auto with arith.
Rewrite FSuccSimpl2; Auto with arith.
Rewrite FSuccDiff1; Simpl; Auto with arith.
Apply Zlt_not_eq; Auto.
Apply Zlt_Zopp; Auto.
Apply inj_lt.
Apply nNormMimLtvNum; Auto.
Unfold FtoRradix; Rewrite FSuccDiff1 with x := p; Simpl; Auto with arith.
Case (Z_eq_dec (Fnum p) (vNum b)); Intros H'2.
Rewrite FSuccSimpl1; Simpl; Auto with arith.
Intros H'; Case H'; Auto.
Rewrite FSuccSimpl4; Simpl; Auto with arith.
Intros H' H'0.
Rewrite FSuccDiff1; Simpl; Auto with arith.
Qed.
Theorem
FNSuccFNSuccMid:
(p:float)
(Fbounded b p) ->
~ (Fnum (FNSucc b radix precision p))=(nNormMin radix precision) ->
~ (Fnum (FNSucc b radix precision p))=(Zopp (nNormMin radix precision)) ->
<R>
(Fminus
radix (FNSucc b radix precision (FNSucc b radix precision p))
(FNSucc b radix precision p))==
(Fminus radix (FNSucc b radix precision p) p).
Intros p Fb; Unfold FNSucc.
Intros H' H'0.
Rewrite FcanonicFormalizeEq with p :=
(FSucc
b radix precision
(Fnormalize radix b precision p));
Auto with float arith.
Rewrite FSucFSucMid; Auto.
Unfold FtoRradix; Repeat Rewrite Fminus_correct; Auto with float arith.
Rewrite FnormalizeCorrect; Auto.
Qed.
End suc1.
Hints Resolve nNormMimLtvNum :float.
14/12/100, 14:52