Fnorm.v
(****************************************************************************
IEEE754 : Fnorm
Laurent Thery
*****************************************************************************
*)
Require Import Float.
Require Import Fcomp.
Require Import Fop.
Section Fbounded_Def.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).
Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Record
Fbound: Set := Bound {
vNum: nat;
dExp: nat }.
Definition
Fbounded :=
[b:Fbound] [d:float]
((Zle (Zopp (vNum b)) (Fnum d)) /\ (Zle (Fnum d) (vNum b))) /\
(Zle (Zopp (dExp b)) (Fexp d)).
Theorem
isBounded: (b:Fbound) (p:float){(Fbounded b p)}+{~ (Fbounded b p)}.
Intros b p; Case (Z_le_gt_dec (Fnum p) (vNum b)); Intros H'.
Case (Z_le_gt_dec (Zopp (vNum b)) (Fnum p)); Intros H'0.
Case (Z_le_gt_dec (Zopp (dExp b)) (Fexp p)); Intros H'1.
Left; Repeat Split; Auto.
Right; Red; Intros H'3; Absurd (Zgt (Zopp (dExp b)) (Fexp p)); Intuition;
Auto with zarith.
Right; Red; Intros H'1; Absurd (Zgt (Zopp (vNum b)) (Fnum p)); Intuition;
Auto with zarith.
Right; Red; Intros H'0; Absurd (Zgt (Fnum p) (vNum b)); Intuition;
Auto with zarith.
Qed.
Theorem
pBounded_absolu:
(b:Fbound) (p:float) (Fbounded b p) ->(le (absolu (Fnum p)) (vNum b)).
Intros b p; Unfold Fbounded; Case (Fnum p); Simpl; Auto with arith.
Intros p0 H'.
Apply ZleLe.
Rewrite (inject_nat_convert (POS p0)); Intuition.
Intros p0 H'; Apply ZleLe.
Rewrite (inject_nat_convert (POS p0)); Auto.
Apply Zle_Zopp_Inv; Simpl; Intuition.
Qed.
Theorem
FzeroisZero: (b:Fbound)<R> (Fzero (Zopp (dExp b)))==R0.
Intros b; Unfold FtoRradix FtoR; Simpl; AutoRewrite [Rsimpl]; Auto.
Qed.
Theorem
FboundedFzero: (b:Fbound)(Fbounded b (Fzero (Zopp (dExp b)))).
Intros b; Repeat (Split; Simpl).
Replace ZERO with (Zopp O); [Idtac | Simpl; Auto].
Apply Zle_Zopp; Apply inj_le; Auto with arith.
Replace ZERO with (inject_nat O); [Idtac | Simpl; Auto].
Apply inj_le; Auto with arith.
Auto with zarith.
Qed.
Theorem
oppBounded: (b:Fbound) (x:float) (Fbounded b x) ->(Fbounded b (Fopp x)).
Intros b x H'; Repeat Split; Simpl; Auto.
Apply Zle_Zopp; Intuition.
Rewrite <- (Zopp_Zopp (vNum b)); Apply Zle_Zopp; Intuition.
Intuition.
Qed.
Theorem
oppBoundedInv:
(b:Fbound) (x:float) (Fbounded b (Fopp x)) ->(Fbounded b x).
Intros b x H'; Rewrite <- (Fopp_Fopp x).
Apply oppBounded; Auto.
Qed.
Theorem
absFBounded:
(b:Fbound) (f:float) (Fbounded b f) ->(Fbounded b (Fabs f)).
Intros b f H'; Repeat Split; Simpl; Intuition.
Apply Zle_trans with (Zopp O).
Apply Zle_Zopp; Apply inj_le; Auto with arith.
Red; Case (Fnum f); Simpl; Intros; Red; Intros H'1; Discriminate.
Generalize H1 H2; Case (Fnum f); Simpl; Auto.
Intros p H' H'0.
Apply Zle_Zopp_Inv; Auto.
Qed.
Theorem
FboundedEqExpPos:
(b:Fbound)
(p, q:float)
(Fbounded b p) -> <R> p==q -> (Rle (Fexp p) (Fexp q)) -> (Rle R0 q) ->
(Fbounded b q).
Intros b p q H' H'0 H'1 H'2.
Split; [Split | Idtac].
Apply Zle_trans with (Zopp O); [Auto with zarith arith | Simpl].
Apply (LeR0Fnum radix); Auto with real arith.
Apply Zle_trans with (Fnum p); [Idtac | Intuition].
Apply Zle_trans with (Fnum (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q));
Auto.
Unfold Fshift; Simpl; Auto.
Case H'2; Intros E1.
Rewrite Zmult_sym; Pattern 1 (Fnum q);
Replace (Fnum q) with (Zmult (1) (Fnum q));
[Apply Zle_Zmult_right | Auto with zarith]; Auto.
Apply Zlt_gt.
Apply (LtR0Fnum radix); Auto with real arith.
Apply le_IZR.
Rewrite Zpower_nat_powerRZ; Auto.
Auto with real arith.
Simpl; Rewrite <- (powerRZ_O radix).
Apply Rle_powerRZ.
Replace R1 with (INR (1)); Auto with real arith.
Cut (Zle (Fexp p) (Fexp q)); [Intros E2 | Idtac].
Rewrite inj_abs; Unfold Zminus; Apply Zle_left; Auto with zarith.
Apply le_IZR; Auto.
Replace (Fnum q) with ZERO; Auto with zarith.
Apply sym_equal; Change (is_Fzero q).
Apply (is_Fzero_rep2 radix); Auto.
Apply le_IZR; Auto.
Apply (Rle_mult_anticompatibility_exp radix) with z := (Fexp p);
Auto with real arith.
Pattern 2 (Fexp p);
Replace (Fexp p)
with (Fexp (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q)); Auto.
Change (Rle (Fshift radix (absolu (Zminus (Fexp q) (Fexp p))) q) p).
Unfold FtoRradix; Rewrite FshiftCorrect; Auto.
Unfold FtoRradix in H'0; Rewrite H'0; Auto with real.
Unfold Fshift; Simpl.
Cut (Zle (Fexp p) (Fexp q)); [Intros E2 | Apply le_IZR]; Auto.
Rewrite inj_abs; [Ring | Idtac].
Unfold Zminus; Apply Zle_left; Auto with zarith.
Apply Zle_trans with (Fexp p); [Intuition | Apply le_IZR]; Auto.
Qed.
Theorem
FboundedEqExp:
(b:Fbound)
(p, q:float) (Fbounded b p) -> <R> p==q -> (Rle (Fexp p) (Fexp q)) ->
(Fbounded b q).
Intros b p q H' H'0 H'1.
Case (Rle_or_lt R0 q); Intros Rl1.
Apply FboundedEqExpPos with p := p; Auto.
Apply oppBoundedInv; Auto.
Apply FboundedEqExpPos with p := (Fopp p); Auto.
Apply oppBounded; Auto.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Auto; Unfold FtoRradix in H'0;
Rewrite H'0; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Auto.
Apply Rlt_le; Replace R0 with (Ropp R0); Auto with real.
Qed.
Theorem
eqExpLess:
(b:Fbound) (p, q:float) (Fbounded b p) -> <R> p==q ->
(Ex [r:float] (Fbounded b r) /\ (<R> r==q /\ (Rle (Fexp q) (Fexp r)))).
Intros b p q H' H'0.
Case (Rle_or_lt (Fexp q) (Fexp p)); Intros H'1.
Exists p; Repeat (Split; Auto).
Exists q; Split; [Idtac | Split]; Auto with real.
Apply FboundedEqExp with p := p; Auto.
Apply Rlt_le; Auto.
Qed.
Theorem
FboundAlt:
(b:Fbound)
(p:float) (Zle (Zabs (Fnum p)) (vNum b)) -> (Zle (Zopp (dExp b)) (Fexp p)) ->
(Fbounded b p).
Intros b p H' H'0; Repeat Split; Auto.
Generalize H'; Case (Fnum p); Simpl; Auto with zarith.
Intros p0 H'1; Apply Zle_trans with (Zopp O); Auto with zarith.
Red; Simpl; Red; Intros; Discriminate.
Intros p0 H'1; Replace (NEG p0) with (Zopp (POS p0)); Auto with zarith.
Generalize H'; Case (Fnum p); Simpl; Auto with zarith.
Intros p0 H'1; Apply Zle_trans with (Zopp O); Auto with zarith.
Red; Simpl; Red; Intros; Discriminate.
Qed.
Theorem
eqExpMax:
(b:Fbound)
(p, q:float) (Fbounded b p) -> (Fbounded b q) -> (Rle (Fabs p) q) ->
(Ex [r:float] (Fbounded b r) /\ (<R> r==p /\ (Zle (Fexp r) (Fexp q)))).
Intros b p q H' H'0 H'1; Case (Zle_or_lt (Fexp p) (Fexp q)); Intros Rl0.
Exists p; Auto.
Cut (Zminus (Fexp p) (absolu (Zminus (Fexp p) (Fexp q))))=(Fexp q);
[Intros Eq1 | Idtac].
Exists (Fshift radix (absolu (Zminus (Fexp p) (Fexp q))) p); Split;
[Idtac | Split].
Apply FboundAlt; Auto.
Apply Zle_trans with (Fnum q).
Replace (Zabs (Fnum (Fshift radix (absolu (Zminus (Fexp p) (Fexp q))) p)))
with (Fnum (Fabs (Fshift radix (absolu (Zminus (Fexp p) (Fexp q))) p)));
Auto.
Apply (Rle_Fexp_eq_Zle radix); Auto with arith.
Rewrite Fabs_correct; Auto with arith; Rewrite FshiftCorrect; Auto with arith;
Rewrite <- (Fabs_correct radix); Auto with arith.
Intuition.
Unfold Fshift; Simpl.
Rewrite Eq1; Auto.
Intuition.
Unfold FtoRradix; Apply FshiftCorrect; Auto.
Unfold Fshift; Simpl.
Rewrite Eq1; Auto with zarith.
Rewrite inj_abs; Auto with zarith.
Qed.
Theorem
maxFbounded:
(b:Fbound) (z:Z) (Zle (Zopp (dExp b)) z) ->(Fbounded b (Float (vNum b) z)).
Intros b z H'; Repeat Split; Simpl; Auto with zarith.
Qed.
Theorem
maxMax:
(b:Fbound) (p:float) (z:Z) (Fbounded b p) -> (Zle (Fexp p) z) ->
(Rle (Fabs p) (Float (vNum b) z)).
Intros b p z H' H'0; Unfold FtoRradix;
Rewrite <- (FshiftCorrect
? radixMoreThanOne (absolu (Zminus z (Fexp p)))
(Float (vNum b) z)); Unfold Fshift; Simpl.
Replace (Zminus z (absolu (Zminus z (Fexp p)))) with (Fexp p).
Unfold Fabs FtoR; Simpl.
Apply Rle_monotony_r; Auto with real arith.
Apply Rle_trans with (Rmult (inject_nat (vNum b)) (inject_nat (1))).
Replace (Rmult (inject_nat (vNum b)) (inject_nat (1))) with (IZR (vNum b)).
Apply Rle_IZR; Cut (Fbounded b (Fabs p)); [Intuition | Apply absFBounded]; Auto.
Ring.
Rewrite Rmult_IZR; Auto.
Apply Rle_monotony.
Replace R0 with (IZR (inject_nat O)); Auto with real zarith arith.
Rewrite Zpower_nat_powerRZ; Auto.
Replace (IZR (1)) with (powerRZ radix O); Auto with real.
Apply Rle_powerRZ; Auto with real zarith arith.
Replace R1 with (INR (1)); Auto with real arith.
Rewrite inj_abs; Auto with zarith.
Qed.
End Fbounded_Def.
Section Fnormalized_Def.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).
Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Variable b:Fbound.
Variable precision:nat.
Hypothesis precisionNotZero:~ precision=O.
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).
Theorem
lt_vNum: (lt O (vNum b)).
Rewrite pGivesBound.
Apply simpl_lt_plus_l with p := (1).
Rewrite <- le_plus_minus.
Rewrite plus_sym; Simpl.
Replace (1) with (exp radix O); Auto with zarith arith.
Replace (1) with (exp radix O); Auto with zarith arith.
Qed.
Theorem
digitVNumiSPrecision: (digit radix (vNum b))=precision.
Apply digitInv; Auto.
Rewrite pGivesBound; Auto.
Apply lt_n_Sm_le; Auto.
Rewrite minus_Sn_m; Simpl; Try Rewrite <- minus_n_O; Auto with arith.
Rewrite pGivesBound.
Generalize (expLess ? radixMoreThanOne precision); Case (exp radix precision);
Auto with arith.
Qed.
Theorem
pGivesDigit: (p:float) (Fbounded b p) ->(le (Fdigit radix p) precision).
Intros p; Case p; Unfold Fdigit Fbounded; Simpl.
Intros Fnum1 Fexp1 H'; Rewrite <- digitVNumiSPrecision.
Case (le_or_lt (absolu Fnum1) (vNum b)); Intros Le0.
Apply digit_monotone; Auto.
Case (Zle_or_lt ZERO Fnum1); Intros Le1.
Absurd (Zle Fnum1 (vNum b)); Auto with zarith.
Apply Zgt_not_le; Apply Zlt_gt.
Rewrite <- (inj_abs Fnum1); Auto with zarith.
Absurd (Zle Fnum1 (vNum b)); Auto with zarith.
Apply Zgt_not_le; Auto.
Apply Zlt_gt.
Rewrite <- (inj_abs Fnum1); Auto with zarith.
Cut (Zle (Zopp Fnum1) (vNum b)); Auto with zarith; Intros Le2.
Contradict Le2; Auto with zarith.
Apply Zgt_not_le; Auto.
Apply Zlt_gt.
Rewrite <- (inj_abs (Zopp Fnum1)); Auto with zarith.
Rewrite absolu_Zopp; Auto with zarith.
Qed.
Theorem
digitGivesBoundedNum:
(p:float) (le (Fdigit radix p) precision) ->
(Zle (Zopp (vNum b)) (Fnum p)) /\ (Zle (Fnum p) (vNum b)).
Intros p; Unfold Fdigit; Intros H0.
Cut (le (absolu (Fnum p)) (vNum b)).
Case (Fnum p); Simpl; Auto with zarith.
Intros p0 H'; Split; Auto with zarith.
Apply Zle_trans with m := ZERO; Auto with zarith.
Red; Simpl; Red; Intros; Discriminate.
Replace (POS p0) with (INZ (convert p0)); Auto with zarith.
Apply inject_nat_convert; Auto.
Intros p0 H'; Split; Auto with zarith.
Cut (Zle (Zopp (NEG p0)) (Zopp (Zopp (vNum b)))); Auto with zarith.
Simpl; Rewrite Zopp_Zopp.
Replace (POS p0) with (INZ (convert p0)); Auto with zarith.
Apply inject_nat_convert; Auto.
Apply Zle_trans with m := ZERO; Auto with zarith.
Red; Simpl; Red; Intros; Discriminate.
Rewrite pGivesBound.
Apply lt_n_Sm_le; Auto.
Replace (S (minus (exp radix precision) (1))) with (exp radix precision); Auto.
Case (le_lt_or_eq ? ? H0); Intros H1.
Apply lt_trans with m := (exp radix (digit radix (absolu (Fnum p))));
Auto with arith.
Rewrite <- H1; Auto with arith.
Rewrite minus_Sn_m; Auto with arith.
Qed.
Definition
Fnormal := [p:float](Fbounded b p) /\ (Fdigit radix p)=precision.
Theorem
FnormalNotZero: (p:float) (Fnormal p) ->~ (is_Fzero p).
Intros p; Case p; Unfold Fnormal Fdigit is_Fzero; Simpl.
Intros Fnum1 Fexp1 H'; Red; Intros H'0.
Absurd (digit radix (absolu Fnum1))=precision; Auto.
Rewrite H'0; Simpl; Auto.
Rewrite digitO; Auto.
Intuition.
Qed.
Theorem
FnormalUnique:
(p, q:float) (Fnormal p) -> (Fnormal q) -> <R> p==q ->p=q.
Intros p q H' H'0 H'1.
Apply (FdigitEq radix); Auto.
Apply FnormalNotZero; Auto.
Apply trans_equal with y := precision.
Intuition.
Intuition.
Qed.
Theorem
FnormalFop: (p:float) (Fnormal p) ->(Fnormal (Fopp p)).
Intros p H'; Repeat Split; Simpl; Replace (Fnum (Fopp p)) with (Zopp (Fnum p));
Try Apply Zle_Zopp; Auto; Intuition.
Rewrite <- H1; Case p; Unfold Fdigit; Simpl; Intros; Rewrite absolu_Zopp; Auto.
Qed.
Theorem
FnormalLtPos:
(p, q:float) (Fnormal p) -> (Fnormal q) -> (Rle R0 p) -> (Rlt p q) ->
(Zlt (Fexp p) (Fexp q)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).
Intros p q H' H'0 H'1 H'2.
Case (Zle_or_lt (Fexp q) (Fexp p)); Auto.
Intros H'3; Right.
Case (Zle_lt_or_eq ? ? H'3); Intros H'4.
2:Split; Auto.
2:Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with zarith.
Absurd (Zlt
(Fnum (Fshift radix (absolu (Zminus (Fexp p) (Fexp q))) p)) (Fnum q));
Auto.
2:Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with zarith.
2:Unfold FtoRradix; Rewrite FshiftCorrect; Auto.
2:Unfold Fshift; Simpl; Auto with zarith.
2:Replace (inject_nat (absolu (Zminus (Fexp p) (Fexp q))))
with (Zminus (Fexp p) (Fexp q)); Auto with zarith.
2:Cut (Zlt ZERO (Zminus (Fexp p) (Fexp q))); Auto with zarith.
2:Case (Zminus (Fexp p) (Fexp q)); Simpl; Auto with zarith.
2:Intros p0; Rewrite (inject_nat_convert (POS p0)); Auto with arith.
2:Intros p0 H'5; Discriminate.
Red; Intros H'5.
Absurd (le
(Fdigit radix (Fshift radix (absolu (Zminus (Fexp p) (Fexp q))) p))
(Fdigit radix q)); Auto with arith.
Rewrite FshiftFdigit; Auto with arith.
Replace (Fdigit radix p) with precision.
Replace (Fdigit radix q) with precision; Auto with zarith.
Cut (Zlt ZERO (Zminus (Fexp p) (Fexp q))); Auto with zarith.
Case (Zminus (Fexp p) (Fexp q)); Simpl; Auto with zarith.
Intros p0 H'6; Generalize (convert_not_O p0); Auto with zarith.
Intros p0 H'6; Discriminate.
Apply sym_equal; Intuition.
Apply sym_equal; Intuition.
Apply FnormalNotZero; Auto with arith.
Unfold Fdigit; Apply digit_monotone; Auto with arith.
Apply lt_le_weak; Apply lt_Zlt_inv.
Repeat Rewrite inj_abs; Auto with arith.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Apply Rle_trans with r2 := (FtoRradix p); Auto with real.
Apply Rlt_le; Auto.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Unfold FtoRradix; Rewrite FshiftCorrect; Auto.
Qed.
Theorem
FnormalLtNeg:
(p, q:float) (Fnormal p) -> (Fnormal q) -> (Rle q R0) -> (Rlt p q) ->
(Zlt (Fexp q) (Fexp p)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).
Intros p q H' H'0 H'1 H'2.
Cut (Zlt (Fexp (Fopp q)) (Fexp (Fopp p))) \/
(Fexp (Fopp q))=(Fexp (Fopp p)) /\ (Zlt (Fnum (Fopp q)) (Fnum (Fopp p))).
Simpl.
Intros H'3; Elim H'3; Clear H'3; Intros H'3;
[Idtac | Elim H'3; Clear H'3; Intros H'3 H'4]; Auto; Right; Split;
Auto with zarith.
Apply FnormalLtPos; Try Apply FnormalFop; Auto; Unfold FtoRradix;
Repeat Rewrite Fopp_correct; Replace R0 with (Ropp R0); Auto with real.
Qed.
Definition
nNormMin := (exp radix (pred precision)).
Theorem
nNormNotZero: ~ nNormMin=O.
Unfold nNormMin; Auto with arith.
Qed.
Theorem
digitnNormMin: (digit radix nNormMin)=precision.
Unfold nNormMin Fdigit; Simpl; Apply digitInv; Auto with zarith arith.
Qed.
Theorem
nNrMMimLevNum: (le nNormMin (vNum b)).
Rewrite pGivesBound.
Unfold nNormMin; Simpl; Auto with arith.
Qed.
Hints Resolve nNrMMimLevNum :arith.
Definition
firstNormalPos := (Float nNormMin (Zopp (dExp b))).
Theorem
firstNormalPosNormal: (Fnormal firstNormalPos).
Repeat Split; Unfold firstNormalPos; Simpl; Auto with zarith.
Rewrite pGivesBound.
Cut (lt (exp radix (pred precision)) (exp radix precision)).
Unfold nNormMin; Auto with zarith.
Apply exp_monotone_lt; Auto with arith.
Unfold Fdigit; Simpl.
Rewrite absolu_INR.
Apply digitnNormMin.
Qed.
Theorem
pNormal_absolu_min:
(p:float) (Fnormal p) ->(le nNormMin (absolu (Fnum p))).
Intros p H'; CaseEq nNormMin; Auto with arith.
Intros n H'0.
Apply lt_le_S.
Case (le_or_lt (absolu (Fnum p)) n); Auto.
Intros H'1.
Absurd (le (Fdigit radix p) (digit radix n)).
Replace (digit radix n) with (pred precision).
Replace (Fdigit radix p) with precision; Auto with arith.
Apply sym_equal; Intuition.
Apply sym_equal.
Replace n with (minus nNormMin (1)); Auto with zarith.
Unfold nNormMin; Apply digit_minus1; Auto with zarith.
Unfold Fdigit; Auto with arith.
Qed.
Theorem
maxMaxBis:
(p:float) (z:Z) (Fbounded b p) -> (Zlt (Fexp p) z) ->
(Rlt (Fabs p) (Float nNormMin z)).
Intros p z H' H'0;
Apply Rle_lt_trans with (FtoR radix (Float (vNum b) (Zpred z))).
Unfold FtoRradix; Apply maxMax; Auto with zarith; Unfold Zpred; Auto with zarith.
Unfold FtoRradix FtoR nNormMin; Simpl.
Pattern 2 z; Replace z with (Zs (Zpred z));
[Rewrite powerRZ_Zs; Auto with real arith | Unfold Zs Zpred; Ring].
Rewrite <- Rmult_assoc.
Apply Rlt_monotony_r; Auto with real arith.
Rewrite pGivesBound.
Repeat Rewrite <- INR_IZR_INZ; Rewrite <- Rmult_INR; Auto.
Rewrite mult_sym; Auto.
Replace (mult radix (exp radix (pred precision)))
with (exp radix (S (pred precision))); [Idtac | Simpl; Auto].
Replace (S (pred precision)) with precision.
Apply Rlt_INR.
Generalize (expLess ? radixMoreThanOne precision); Case (exp radix precision);
Simpl; Auto with arith; Intros n; Rewrite <- minus_n_O; Auto.
Generalize precisionNotZero; Case precision; Simpl; Auto with arith.
Intros H'1; Case H'1; Auto.
Qed.
Theorem
FnormalLtFirstNormalPos:
(p:float) (Fnormal p) -> (Rle R0 p) ->(Rle firstNormalPos p).
Intros p H' H'0.
Case (Rle_or_lt firstNormalPos p); Intros Lt0; Auto with real.
Case (FnormalLtPos p firstNormalPos); Auto.
Apply firstNormalPosNormal.
Intros H'1; Contradict H'1; Unfold firstNormalPos; Simpl.
Apply Zle_not_lt; Intuition.
Intros H'1; Elim H'1; Intros H'2 H'3; Contradict H'3.
Unfold firstNormalPos; Simpl.
Apply Zle_not_lt.
Rewrite <- (inj_abs (Fnum p)).
Apply inj_le; Auto.
Apply pNormal_absolu_min; Auto.
Apply LeR0Fnum with radix := radix; Auto with arith.
Qed.
Theorem
FnormalLtFirstNormalNeg:
(p:float) (Fnormal p) -> (Rle p R0) ->(Rle p (Fopp firstNormalPos)).
Intros p H' H'0.
Rewrite <- (Ropp_Ropp p); Unfold FtoRradix; Repeat Rewrite Fopp_correct.
Apply Rle_Ropp; Rewrite <- Fopp_correct.
Apply FnormalLtFirstNormalPos.
Apply FnormalFop; Auto.
Replace R0 with (Ropp R0); Unfold FtoRradix; Try Rewrite Fopp_correct;
Auto with real.
Qed.
Theorem
FnormalBoundAbs:
(p:float) (Fnormal p) ->(Rlt (Float (vNum b) (Zpred (Fexp p))) (Fabs p)).
Intros p H'; Unfold FtoRradix FtoR; Simpl.
Pattern 2 (Fexp p); Replace (Fexp p) with (Zs (Zpred (Fexp p)));
[Rewrite powerRZ_Zs; Auto with real arith | Unfold Zs Zpred; Ring].
Repeat Rewrite <- Rmult_assoc.
Apply Rlt_monotony_r; Auto with real arith.
Rewrite Zabs_absolu.
Repeat Rewrite <- INR_IZR_INZ.
Rewrite <- Rmult_INR.
Apply Rlt_INR.
Rewrite pGivesBound.
Apply digit_anti_monotone_lt with n := radix; Auto.
Pattern 4 radix; Replace radix with (exp radix (1));
[Idtac | Simpl; Auto with arith].
Rewrite digitAdd; Auto.
Case H'; Unfold Fdigit; Intros H'0 H'1; Unfold Fdigit; Rewrite H'1.
Rewrite digitInv with r := precision; Auto with arith.
Rewrite plus_sym; Auto with arith.
Case H'; Unfold Fdigit; Case (Fnum p); Simpl.
Rewrite digitO.
Intros H'0 H'1; Contradict H'1; Auto with zarith.
Intros p0 H'0 H'1; (Generalize (convert_not_O p0); Auto with zarith).
Intros p0 H'0 H'1; (Generalize (convert_not_O p0); Auto with zarith).
Qed.
Definition
Fsubnormal :=
[p:float]
(Fbounded b p) /\
((Fexp p)=(Zopp (dExp b)) /\ (lt (Fdigit radix p) precision)).
Theorem
FsubnormFopp: (p:float) (Fsubnormal p) ->(Fsubnormal (Fopp p)).
Intros p H'; Repeat Split; Simpl.
Apply Zle_Zopp; Intuition.
Replace (inject_nat (vNum b)) with (Zopp (Zopp (vNum b))).
Apply Zle_Zopp; Intuition.
Auto with zarith.
Intuition.
Intuition.
Intuition.
Unfold Fdigit; Simpl.
Rewrite absolu_Zopp; Intuition.
Qed.
Theorem
FsubnormalUnique:
(p, q:float) (Fsubnormal p) -> (Fsubnormal q) -> <R> p==q ->p=q.
Intros p q H' H'0 H'1.
Apply FtoREqInv2 with radix := radix; Auto.
Generalize H' H'0; Unfold Fsubnormal; Auto with zarith.
Qed.
Theorem
FsubnormalLt:
(p, q:float) (Fsubnormal p) -> (Fsubnormal q) -> (Rlt p q) ->
(Zlt (Fnum p) (Fnum q)).
Intros p q H' H'0 H'1.
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with zarith.
Apply trans_equal with (Zopp (dExp b)).
Intuition.
Apply sym_equal; Intuition.
Qed.
Theorem
LtFsubnormal:
(p, q:float) (Fsubnormal p) -> (Fsubnormal q) -> (Zlt (Fnum p) (Fnum q)) ->
(Rlt p q).
Intros p q H' H'0 H'1.
Case (total_order p q); Auto; Intros Test; Case Test; Clear Test; Intros Test;
Contradict H'1.
Unfold FtoRradix in Test; Rewrite sameExpEq with 2 := Test; Auto.
Auto with zarith.
Apply trans_equal with (Zopp (dExp b)).
Intuition.
Apply sym_equal; Intuition.
Apply Zle_not_lt.
Apply Zlt_le_weak.
Apply FsubnormalLt; Auto.
Qed.
Theorem
pSubnormal_absolu_min:
(p:float) (Fsubnormal p) ->(lt (absolu (Fnum p)) nNormMin).
Intros p H'.
Case (le_or_lt nNormMin (absolu (Fnum p))); Auto.
Intros H'1.
Absurd (le (digit radix nNormMin) (Fdigit radix p)).
Replace (digit radix nNormMin) with precision.
Apply lt_not_le; Intuition.
Apply sym_equal.
Apply digitnNormMin.
Unfold Fdigit; Auto with arith.
Qed.
Theorem
FsubnormalLtFirstNormalPos:
(p:float) (Fsubnormal p) -> (Rle R0 p) ->(Rlt p firstNormalPos).
Intros p H' H'0; Unfold FtoRradix FtoR firstNormalPos; Simpl.
Replace (Fexp p) with (Zopp (dExp b)).
2:Apply sym_equal; Intuition.
Apply Rlt_monotony_r; Auto with real arith.
Apply Rlt_IZR.
Rewrite <- (inj_abs (Fnum p)).
2:Apply LeR0Fnum with radix := radix; Auto with zarith.
Apply inj_lt.
Apply digit_anti_monotone_lt with n := radix; Auto.
Rewrite digitInv with q := (exp radix (pred precision)) r := precision;
Auto with arith.
Intuition.
Qed.
Theorem
FsubnormalnormalLtPos:
(p, q:float) (Fsubnormal p) -> (Fnormal q) -> (Rle R0 p) -> (Rle R0 q) ->
(Rlt p q).
Intros p q H' H'0 H'1 H'2.
Apply Rlt_le_trans with r2 := (FtoRradix firstNormalPos).
Apply FsubnormalLtFirstNormalPos; Auto.
Apply FnormalLtFirstNormalPos; Auto.
Qed.
Theorem
FsubnormalnormalLtNeg:
(p, q:float) (Fsubnormal p) -> (Fnormal q) -> (Rle p R0) -> (Rle q R0) ->
(Rlt q p).
Intros p q H' H'0 H'1 H'2.
Rewrite <- (Ropp_Ropp p); Rewrite <- (Ropp_Ropp q).
Apply Rgt_Ropp; Red.
Unfold FtoRradix; Repeat Rewrite <- Fopp_correct.
Apply FsubnormalnormalLtPos; Auto.
Apply FsubnormFopp; Auto.
Apply FnormalFop; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Replace R0 with (Ropp R0);
Auto with real.
Unfold FtoRradix; Rewrite Fopp_correct; Replace R0 with (Ropp R0);
Auto with real.
Qed.
Definition
Fnormalize :=
[p:float]
Cases (Z_zerop (Fnum p)) of
(left _) => (Float ZERO (Zopp (dExp b)))
| (right _) =>
(Fshift
radix
(min
(minus precision (Fdigit radix p))
(absolu (Zplus (dExp b) (Fexp p)))) p)
end.
Theorem
FnormalizeCorrect: (p:float)<R> (Fnormalize p)==p.
Intros p; Unfold Fnormalize.
Case (Z_zerop (Fnum p)).
Case p; Intros Fnum1 Fexp1 H'; Unfold FtoRradix FtoR; Rewrite H'; Simpl;
Auto with real.
Apply trans_eqT with R0; Auto with real.
Intros H'; Unfold FtoRradix; Apply FshiftCorrect; Auto.
Qed.
Theorem
Fnormalize_Fopp: (p:float)(Fnormalize (Fopp p))=(Fopp (Fnormalize p)).
Intros p; Case p; Unfold Fnormalize; Simpl.
Intros Fnum1 Fexp1; Case (Z_zerop Fnum1); Intros H'.
Rewrite H'; Simpl; Auto.
Case (Z_zerop ZERO); Intros H'0; Simpl; Auto.
Case H'0; Auto.
Case (Z_zerop (Zopp Fnum1)); Intros H'0; Simpl; Auto.
Case H'; Replace Fnum1 with (Zopp (Zopp Fnum1)); Auto with zarith.
Unfold Fopp Fshift Fdigit; Simpl.
Rewrite absolu_Zopp; Apply floatEq; Simpl; Auto with zarith.
Ring.
Qed.
Theorem
FnormalizeBounded:
(p:float) (Fbounded b p) ->(Fbounded b (Fnormalize p)).
Intros p H'; Red; Split.
Unfold Fnormalize; Case (Z_zerop (Fnum p)); Auto.
Simpl; Auto with zarith.
Intros H'0.
Apply digitGivesBoundedNum; Auto.
Unfold Fnormalize; Rewrite FshiftFdigit; Auto.
Apply le_trans
with m := (plus (Fdigit radix p) (minus precision (Fdigit radix p)));
Auto with arith.
Rewrite <- le_plus_minus; Auto.
Apply pGivesDigit; Auto.
Unfold Fnormalize; Case (Z_zerop (Fnum p)); Auto.
Simpl; Auto with zarith.
Generalize H'; Case p; Unfold Fbounded Fnormal Fdigit; Simpl.
Intros Fnum1 Fexp1 H'0 H'1.
Apply Zle_trans with m := (Zminus Fexp1 (absolu (Zplus (dExp b) Fexp1))).
Rewrite inj_abs; Auto with zarith.
Unfold Zminus; Apply Zle_reg_l; Auto.
Apply Zle_Zopp; Auto.
Apply inj_le; Auto with arith.
Qed.
Definition
Fcanonic := [a:float](Fnormal a) \/ (Fsubnormal a).
Theorem
FcanonicBound: (p:float) (Fcanonic p) ->(Fbounded b p).
Intuition.
Qed.
Theorem
pUCanonic_absolu:
(p:float) (Fcanonic p) ->(le (absolu (Fnum p)) (vNum b)).
Intros p H'; Apply pBounded_absolu.
Intuition.
Qed.
Theorem
FcanonicFopp: (p:float) (Fcanonic p) ->(Fcanonic (Fopp p)).
Intros p H'; Case H'; Intros H'1.
Left; Apply FnormalFop; Auto.
Right; Apply FsubnormFopp; Auto.
Qed.
Theorem
FcanonicFabs: (p:float) (Fcanonic p) ->(Fcanonic (Fabs p)).
Intros p H'; Case H'; Clear H'; Intros H'; Case H'.
Intros H'0 H'1; Left; Split.
Apply absFBounded; Auto.
Generalize H'1; Case p; Unfold Fdigit; Simpl.
Intros Fnum1 Fexp1 H'2; Replace (absolu (Zabs Fnum1)) with (absolu Fnum1); Auto.
Case Fnum1; Simpl; Auto with zarith.
Intros H'0 H'1; Elim H'1; Intros H'2 H'3; Right; Split; Clear H'1.
Apply absFBounded; Auto.
Split.
Generalize H'2; Case p; Simpl; Auto.
Generalize H'3; Case p; Unfold Fdigit; Simpl.
Intros Fnum1 Fexp1 H'4; Replace (absolu (Zabs Fnum1)) with (absolu Fnum1); Auto.
Case Fnum1; Simpl; Auto with zarith.
Qed.
Theorem
FnormalizeCanonic: (p:float) (Fbounded b p) ->(Fcanonic (Fnormalize p)).
Intros p H'.
Generalize (FnormalizeBounded p H').
Unfold Fnormalize; Case (Z_zerop (Fnum p)); Auto.
Intros H'0; Right; Repeat Split; Simpl; Auto with zarith.
Generalize precisionNotZero; Case precision; Unfold Fdigit; Simpl;
Rewrite digitO; Auto with arith.
Intros H'1.
Case (min_or
(minus precision (Fdigit radix p)) (absolu (Zplus (dExp b) (Fexp p))));
Intros Min; Case Min; Clear Min; Intros MinR MinL.
Intros H'2; Left; Split; Auto.
Rewrite MinR; Rewrite FshiftFdigit; Clear MinR; Auto with arith.
Rewrite <- le_plus_minus; Auto.
Apply pGivesDigit; Auto.
Intros H'0; Right; Split; Auto; Split.
Rewrite MinR; Clear MinR; Auto.
Cut (Zle (Zopp (dExp b)) (Fexp p));
[Idtac | Red in H'; Generalize H'; Intuition].
Case p; Simpl.
Intros Fnum1 Fexp1 H'2; Rewrite inj_abs; Auto with zarith.
Rewrite MinR; Generalize MinL; Case precision.
Simpl; Intros H'2; Absurd (lt (absolu (Zplus (dExp b) (Fexp p))) O);
Auto with arith.
Intros p' H'2.
Rewrite FshiftFdigit; Auto; Clear H'0 MinL MinR H'1 H'; Auto with zarith.
Qed.
Theorem
FcanonicLtPos:
(p, q:float) (Fcanonic p) -> (Fcanonic q) -> (Rle R0 p) -> (Rlt p q) ->
(Zlt (Fexp p) (Fexp q)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).
Intros p q H' H'0 H'1 H'2; Case H'; Case H'0.
Intros H'3 H'4; Apply FnormalLtPos; Auto.
Intros H'3 H'4; Absurd (Rlt p q); Auto.
Apply Rlt_antisym.
Apply FsubnormalnormalLtPos; Auto.
Apply Rle_trans with r2 := (FtoRradix p); Auto with real.
Apply Rlt_le; Auto.
Intros H'3 H'4; Case (Z_eq_dec (Fexp q) (Zopp (dExp b))); Intros H'5.
Right; Split.
Rewrite H'5; Intuition.
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with zarith.
Rewrite H'5; Intuition.
Left.
Replace (Fexp p) with (Zopp (dExp b)); [Idtac | Apply sym_equal; Intuition].
Case (Zle_lt_or_eq (Zopp (dExp b)) (Fexp q)); Auto with zarith.
Intuition.
Intros H'3 H'4; Right; Split.
Apply trans_equal with (Zopp (dExp b)).
Intuition.
Apply sym_equal; Intuition.
Apply FsubnormalLt; Auto.
Qed.
Theorem
FcanonicLtNeg:
(p, q:float) (Fcanonic p) -> (Fcanonic q) -> (Rle q R0) -> (Rlt p q) ->
(Zlt (Fexp q) (Fexp p)) \/ (Fexp p)=(Fexp q) /\ (Zlt (Fnum p) (Fnum q)).
Intros p q H' H'0 H'1 H'2.
Cut (Zlt (Fexp (Fopp q)) (Fexp (Fopp p))) \/
(Fexp (Fopp q))=(Fexp (Fopp p)) /\ (Zlt (Fnum (Fopp q)) (Fnum (Fopp p))).
Simpl.
Intros H'3; Elim H'3; Clear H'3; Intros H'3;
[Idtac | Elim H'3; Clear H'3; Intros H'3 H'4]; Auto; Right; Split;
Auto with zarith.
Apply FcanonicLtPos; Try Apply FcanonicFopp; Auto; Unfold FtoRradix;
Repeat Rewrite Fopp_correct; Replace R0 with (Ropp R0); Auto with real.
Qed.
Theorem
NormalNotSubNormal: (p:float)~ ((Fnormal p) /\ (Fsubnormal p)).
Intros p; Unfold Fsubnormal Fnormal.
Intuition.
Qed.
Theorem
NormalAndSubNormalNotEq:
(p, q:float) (Fnormal p) -> (Fsubnormal q) ->~ <R> p==q.
Intros p q H' H'0; Red; Intros H'1.
Case (total_order R0 p); Intros H'2.
Absurd (Rlt q p).
Rewrite <- H'1; Auto with real.
Apply FsubnormalnormalLtPos; Auto with real.
Rewrite <- H'1; Auto with real.
Apply Rlt_le; Auto.
Apply Rlt_le; Auto.
Absurd (Rlt p q).
Rewrite <- H'1; Auto with real.
Apply FsubnormalnormalLtNeg; Auto with real.
Rewrite <- H'1; Auto with real.
Elim H'2; Intros H'3; Try Rewrite <- H'3; Auto with real.
Apply Rlt_le; Auto with real.
Elim H'2; Intros H'3; Try Rewrite <- H'3; Auto with real.
Apply Rlt_le; Auto with real.
Qed.
Theorem
FcanonicUnique:
(p, q:float) (Fcanonic p) -> (Fcanonic q) -> <R> p==q ->p=q.
Intros p q H' H'0 H'1; Case H'; Case H'0; Intros H'2 H'3.
Apply FnormalUnique; Auto.
Contradict H'1; Apply NormalAndSubNormalNotEq; Auto.
Absurd <R> q==p; Auto; Apply NormalAndSubNormalNotEq; Auto.
Apply FsubnormalUnique; Auto.
Qed.
Theorem
FcanonicFormalizeEq: (p:float) (Fcanonic p) ->(Fnormalize p)=p.
Intros p H'.
Apply FcanonicUnique; Auto.
Apply FnormalizeCanonic; Auto.
Intuition.
Apply FnormalizeCorrect; Auto.
Qed.
Theorem
FcanonicPosFexpRlt:
(x, y:float)
(Rle R0 x) ->
(Rle R0 y) -> (Fcanonic x) -> (Fcanonic y) -> (Zlt (Fexp x) (Fexp y)) ->
(Rlt x y).
Intros x y H' H'0 H'1 H'2 H'3.
Case (Rle_or_lt y x); Auto.
Intros H'4; Case H'4; Clear H'4; Intros H'4.
Case FcanonicLtPos with p := y q := x; Auto.
Intros H'5; Contradict H'3; Auto with zarith.
Intros H'5; Elim H'5; Intros H'6 H'7; Clear H'5; Contradict H'3; Rewrite H'6;
Auto with zarith.
Contradict H'3.
Rewrite FcanonicUnique with p := x q := y; Auto with zarith.
Qed.
Theorem
FcanonicNegFexpRlt:
(x, y:float)
(Rle x R0) ->
(Rle y R0) -> (Fcanonic x) -> (Fcanonic y) -> (Zlt (Fexp x) (Fexp y)) ->
(Rlt y x).
Intros x y H' H'0 H'1 H'2 H'3.
Case (Rle_or_lt x y); Auto.
Intros H'4; Case H'4; Clear H'4; Intros H'4.
Case FcanonicLtNeg with p := x q := y; Auto.
Intros H'5; Contradict H'3; Auto with zarith.
Intros H'5; Elim H'5; Intros H'6 H'7; Clear H'5; Contradict H'3; Rewrite H'6;
Auto with zarith.
Contradict H'3.
Rewrite FcanonicUnique with p := x q := y; Auto with zarith.
Qed.
End Fnormalized_Def.
Hints Resolve
FboundedFzero oppBounded absFBounded FboundAlt maxFbounded FnormalNotZero
nNormNotZero nNrMMimLevNum firstNormalPosNormal FsubnormFopp
FsubnormalLtFirstNormalPos FnormalizeBounded FcanonicFopp FcanonicFabs
FnormalizeCanonic :float.
14/12/100, 14:26