Library Float.Expansions.Fexp
Require Export AllFloat.
Require Export List.
Section mf.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
Coercion Local FtoRradix := FtoR radix.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Inductive IsExpansion : list float -> Prop :=
| IsExpansionNil : IsExpansion nil
| IsExpansionSingle :
forall x : float, Fbounded b x -> IsExpansion (x :: nil)
| IsExpansionTop1 :
forall (x : float) (L : list float),
is_Fzero x -> Fbounded b x -> IsExpansion L -> IsExpansion (x :: L)
| IsExpansionTop2 :
forall (x y : float) (L : list float),
Fbounded b x ->
is_Fzero y ->
Fbounded b y -> IsExpansion (x :: L) -> IsExpansion (x :: y :: L)
| IsExpansionTop :
forall (x y : float) (L : list float),
~ is_Fzero x ->
~ is_Fzero y ->
Fbounded b x ->
Fbounded b y ->
(MSB radix x < LSB radix y)%Z ->
IsExpansion (y :: L) -> IsExpansion (x :: y :: L).
Theorem Zlt_MSB_LSB :
forall x y : float,
~ is_Fzero y -> (MSB radix x < LSB radix y)%Z -> (Fabs x < Fabs y)%R.
intros x y H' H'0; case (is_FzeroP x); intros F0.
replace (FtoRradix (Fabs x)) with 0%R.
case (Rabs_pos y).
unfold FtoRradix in |- *; rewrite Fabs_correct; auto with arith.
intros H'1; Contradict H'.
apply is_Fzero_rep2 with (radix := radix); auto.
generalize H'1; unfold Rabs in |- *; case (Rcase_abs y); auto with real.
intros H'2 H'3; replace 0%R with (-0)%R; [ rewrite H'3 | idtac ]; fold FtoRradix;ring.
unfold Fabs in |- *; rewrite F0; unfold FtoRradix, FtoR in |- *;
simpl in |- *; ring.
case (Rle_or_lt (Fabs y) (Fabs x)); auto.
intros H'1; Contradict H'0.
apply Zle_not_lt; auto.
apply Zle_trans with (MSB radix y).
apply LSB_le_MSB; auto.
apply MSB_monotone; auto.
Qed.
Theorem IsExpansion_comp1 :
forall (L : list float) (x y : float),
Fbounded b y -> x = y :>R -> IsExpansion (x :: L) -> IsExpansion (y :: L).
simple induction L.
intros x y H' H'0 H'1; apply IsExpansionSingle; auto.
intros a l H' x y H'0 H'1 H'2; inversion H'2.
apply IsExpansionTop1; auto.
apply (is_Fzero_rep2 radix); auto with arith; unfold FtoRradix in H'1;
rewrite <- H'1; apply is_Fzero_rep1; auto.
apply IsExpansionTop2; auto.
apply (H' x); auto.
apply IsExpansionTop; auto.
Contradict H2; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'1; rewrite H'1; apply is_Fzero_rep1;
auto.
rewrite (MSB_comp radix) with (y := x); auto.
Contradict H2; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'1; rewrite H'1; apply is_Fzero_rep1;
auto.
Qed.
Theorem IsExpansion_comp2 :
forall (L : list float) (x y z : float),
Fbounded b z ->
y = z :>R -> IsExpansion (x :: y :: L) -> IsExpansion (x :: z :: L).
intros L x y z H' H'0 H'1; inversion H'1.
apply IsExpansionTop1; auto; apply IsExpansion_comp1 with y; auto.
apply IsExpansionTop2; auto.
apply (is_Fzero_rep2 radix); auto with arith; unfold FtoRradix in H'0;
rewrite <- H'0; apply is_Fzero_rep1; auto.
apply IsExpansionTop; auto.
Contradict H3; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'0; rewrite H'0; apply is_Fzero_rep1;
auto.
rewrite (LSB_comp radix) with (y := y); auto.
Contradict H3; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'0; rewrite H'0; apply is_Fzero_rep1;
auto.
apply IsExpansion_comp1 with (x := y); auto.
Qed.
Fixpoint expValue (L : list float) : float :=
match L with
| nil => Fzero 0
| x :: L1 => Fplus radix x (expValue L1)
end.
Fixpoint expNormalize (L : list float) : list float :=
match L with
| nil => nil
| x :: L1 =>
match Fnum x with
| Z0 => expNormalize L1
| Zpos p => x :: expNormalize L1
| Zneg p => x :: expNormalize L1
end
end.
Theorem expInv :
forall (a : float) (L : list float), IsExpansion (a :: L) -> IsExpansion L.
intros a L; generalize a; clear a; elim L; auto.
intros a H'; apply IsExpansionNil.
intros a l H' a0 H'0; inversion H'0; auto.
apply IsExpansionTop1; auto.
apply (H' a0); auto.
Qed.
Theorem expBoundedInv :
forall (a : float) (L : list float), IsExpansion (a :: L) -> Fbounded b a.
intros a L H'; inversion H'; auto.
Qed.
Theorem expNormalizeCorrect :
forall L : list float, expValue L = expValue (expNormalize L) :>R.
intros L; elim L; simpl in |- *; auto.
intros a l H'; CaseEq (Fnum a); simpl in |- *; unfold FtoRradix in |- *;
repeat rewrite Fplus_correct; auto with arith; unfold FtoRradix in H';
rewrite H'; auto.
intros H'0; rewrite is_Fzero_rep1; auto; rewrite Rplus_0_l; auto.
Qed.
Theorem expNormalizeExp :
forall L : list float, IsExpansion L -> IsExpansion (expNormalize L).
intros L H'; elim H'; auto.
simpl in |- *; apply IsExpansionNil; auto.
simpl in |- *; intros a Ha; case (Fnum a); try apply IsExpansionNil; intros;
apply IsExpansionSingle; auto.
simpl in |- *; intros x L0 H'0 H'1 H'2 H'3; rewrite H'0; auto.
intros x y L0 H'0 H'1 H'2 H'3; case (is_FzeroP x); intros Z0.
simpl in |- *; rewrite Z0; rewrite H'1; auto.
generalize Z0; unfold is_Fzero in |- *; simpl in |- *; case (Fnum x);
try (intros tmp; case tmp; auto; fail); rewrite H'1;
auto.
intros x y L0 H'0 H'1 H'2 H'3 H'4 H'5; simpl in |- *; generalize H'0 H'1;
unfold is_Fzero in |- *; case (Fnum x);
try (intros tmp; case tmp; auto; fail); intros p H;
case (Fnum y); try (intros tmp; case tmp; auto; fail);
intros; apply IsExpansionTop; auto.
Qed.
Inductive IsNzExpansion : list float -> Prop :=
| IsNzExpansionNil : IsNzExpansion nil
| IsNzExpansionSingle :
forall x : float,
~ is_Fzero x -> Fbounded b x -> IsNzExpansion (x :: nil)
| IsNzExpansionTop :
forall (x y : float) (L : list float),
~ is_Fzero x ->
~ is_Fzero y ->
Fbounded b x ->
Fbounded b y ->
(MSB radix x < LSB radix y)%Z ->
IsNzExpansion (y :: L) -> IsNzExpansion (x :: y :: L).
Theorem isNzExpansionIsExpansion :
forall l : list float, IsNzExpansion l -> IsExpansion l.
intros l H'; elim H'; simpl in |- *; auto.
apply IsExpansionNil.
intros x H'0 H'1; apply IsExpansionSingle; auto.
intros x y L H'0 H'1 H'2 H'3 H'4 H'5 H'6.
apply IsExpansionTop; auto.
Qed.
Theorem IsNzExpansionInv :
forall (a : float) (l : list float),
IsNzExpansion (a :: l) -> IsNzExpansion l.
intros a l H'; inversion H'; auto.
apply IsNzExpansionNil; auto.
Qed.
Inductive IsNzExpansionR : list float -> Prop :=
| IsNzExpansionNilR : IsNzExpansionR nil
| IsNzExpansionSingleR :
forall x : float,
~ is_Fzero x -> Fbounded b x -> IsNzExpansionR (x :: nil)
| IsNzExpansionTopR :
forall (x y : float) (L : list float),
~ is_Fzero x ->
~ is_Fzero y ->
Fbounded b x ->
Fbounded b y ->
(MSB radix y < LSB radix x)%Z ->
IsNzExpansionR (y :: L) -> IsNzExpansionR (x :: y :: L).
Theorem isNzExpansionRIsNzExpansion :
forall l : list float, IsNzExpansionR l -> IsNzExpansion (rev l).
intros l H'; elim H'; simpl in |- *; auto.
apply IsNzExpansionNil.
exact IsNzExpansionSingle.
intros x y L H'0 H'1 H'2 H'3 H'4 H'5; elim (rev L); simpl in |- *.
intros H'6; apply IsNzExpansionTop; auto.
apply IsNzExpansionSingle; auto.
intros a l0; case l0; simpl in |- *.
intros H'6 H'7; apply IsNzExpansionTop; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
apply IsNzExpansionTop; auto.
apply IsNzExpansionSingle; auto.
intros f l1 H'6 H'7; apply IsNzExpansionTop; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
apply H'6.
inversion H'7; auto.
Qed.
Theorem IsNzExpansionRInv :
forall (a : float) (l : list float),
IsNzExpansionR (a :: l) -> IsNzExpansionR l.
intros a l H'; inversion H'; auto.
apply IsNzExpansionNilR; auto.
Qed.
Theorem mkIsNzAux :
forall (n : nat) (p : float),
(- dExp b <= LSB radix p)%Z ->
(MSB radix p < - dExp b + n)%Z ->
exists l : list float,
IsNzExpansionR l /\
p = expValue l :>R /\
match l with
| a :: _ => ToZeroP b radix p a
| nil => True
end.
intros n; elim n.
intros p H' H'0; case (is_FzeroP p); intros H'1.
exists (nil (A:=float)); repeat split; simpl in |- *; auto.
apply IsNzExpansionNilR.
replace (FtoRradix (Fzero 0)) with 0%R.
unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
absurd (LSB radix p <= MSB radix p)%Z.
apply Zlt_not_le.
apply Zlt_le_trans with (1 := H'0).
replace (- dExp b + 0%nat)%Z with (- dExp b)%Z; [ auto | ring ].
apply LSB_le_MSB; auto.
intros n0 H' p H'0 H'1.
case (is_FzeroP p); intros H'2.
exists (nil (A:=float)); repeat split; simpl in |- *; auto.
apply IsNzExpansionNilR.
replace (FtoRradix (Fzero 0)) with 0%R.
unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
cut (TotalP (ToZeroP b radix));
[ intros tmp1; case (tmp1 (FtoRradix p)); clear tmp1; intros a Ha
| apply ToZeroTotal with (precision := precision) ];
auto.
cut (~ is_Fzero a); [ intros Na | idtac ].
2: red in |- *; intros H'6; absurd (a = 0%R :>R).
2: apply
(MSBBoundNotZero b radix precision) with (P := ToZeroP b radix) (f1 := p);
auto.
2: apply ToZeroRoundedModeP with (precision := precision); auto.
2: Contradict H'2.
2: apply is_Fzero_rep2 with (radix := radix); auto.
2: apply Zle_trans with (1 := H'0).
2: apply LSB_le_MSB; auto.
2: unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
case (is_FzeroP (Fminus radix p a)); intros H'3.
exists (a :: nil); repeat split; auto.
apply IsNzExpansionSingleR; auto.
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
simpl in |- *.
replace (FtoRradix p) with (FtoRradix (Fplus radix (Fminus radix p a) a)).
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with real arith.
replace (FtoR radix (Fminus radix p a)) with 0%R.
replace (FtoR radix (Fzero 0)) with 0%R.
apply Rplus_comm.
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
apply sym_eq; apply is_Fzero_rep1; auto.
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with real arith;
repeat rewrite Fminus_correct; auto with real arith;
ring.
elim (H' (Fminus radix p a));
[ intros l E; elim E; intros H'7 H'8; elim H'8; intros H'9 H'10; clear H'8 E
| idtac
| idtac ]; auto.
exists (a :: l); repeat split; auto.
generalize H'7 H'10; case l.
intros H'4 H'5; apply IsNzExpansionSingleR; auto.
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
intros f l0 H'4 H'5.
apply IsNzExpansionTopR; auto.
inversion H'4; auto.
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
inversion H'4; auto.
replace (MSB radix f) with (MSB radix (Fminus radix p a)).
apply (MSBroundLSB b radix precision) with (P := ToZeroP b radix); auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
apply (MSBtoZero b radix precision); auto.
inversion H'4; auto.
simpl in |- *; unfold FtoRradix in |- *; rewrite Fplus_correct;
auto with arith.
unfold FtoRradix in H'9; rewrite <- H'9.
rewrite Fminus_correct; auto with arith; ring.
apply Zle_trans with (Zmin (LSB radix p) (LSB radix a)).
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp a).
cut (Fbounded b a); [ auto with float | idtac ].
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
apply Fexp_le_LSB; auto.
apply LSBMinus; auto.
apply Zlt_le_trans with (LSB radix a).
apply (MSBroundLSB b radix precision) with (P := ToZeroP b radix); auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
apply Zle_trans with (MSB radix a); auto.
apply LSB_le_MSB; auto.
rewrite <- (MSBtoZero b radix precision) with (f1 := p) (f2 := a); auto.
apply Zlt_succ_le.
replace (Zsucc (- dExp b + n0)) with (- dExp b + S n0)%Z; auto.
rewrite inj_S; unfold Zsucc in |- *; ring.
Qed.
Theorem expValueApp :
forall l1 l2 : list float,
expValue (l1 ++ l2) = (expValue l1 + expValue l2)%R :>R.
intros l1; elim l1; simpl in |- *; auto.
intros l2; unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
intros a l H' l2.
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with zarith.
rewrite H'; unfold FtoRradix in |- *; ring.
Qed.
Theorem expValueRev :
forall l : list float, expValue (rev l) = expValue l :>R.
intros l; elim l; simpl in |- *; auto.
intros a l0 H'; rewrite expValueApp; simpl in |- *.
rewrite H'.
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with zarith.
replace (FtoR radix (Fzero 0)) with 0%R; [ ring | idtac ].
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
Qed.
Theorem existExp :
forall p : float,
(- dExp b <= LSB radix p)%Z ->
exists l : list float, IsExpansion l /\ p = expValue l :>R.
intros p H'.
elim (mkIsNzAux ( Zabs_nat (dExp b)+1 + Zabs_nat (MSB radix p)) p);
[ intros l E; elim E; intros H'3 H'4; elim H'4; intros H'5 H'6; clear H'4 E
| idtac
| idtac ]; auto.
exists (rev l); split; auto.
apply isNzExpansionIsExpansion.
apply isNzExpansionRIsNzExpansion; auto.
rewrite expValueRev; auto.
apply Zle_lt_trans with (Z_of_nat (Zabs_nat (MSB radix p))).
rewrite <- Zabs_absolu.
case (MSB radix p); simpl in |- *; auto with zarith; intros;
unfold Zle in |- *; simpl in |- *; red in |- *; intros;
discriminate.
rewrite inj_plus.
rewrite inj_plus.
rewrite <- (Zabs_absolu (Z_of_N (dExp b))).
rewrite Zabs_eq; [idtac|case (dExp b)]; auto with zarith.
rewrite Zplus_assoc.
replace (- dExp b + (dExp b + S 0))%Z with (Zsucc 0).
auto with zarith.
ring.
Qed.
End mf.
Require Export List.
Section mf.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
Coercion Local FtoRradix := FtoR radix.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Inductive IsExpansion : list float -> Prop :=
| IsExpansionNil : IsExpansion nil
| IsExpansionSingle :
forall x : float, Fbounded b x -> IsExpansion (x :: nil)
| IsExpansionTop1 :
forall (x : float) (L : list float),
is_Fzero x -> Fbounded b x -> IsExpansion L -> IsExpansion (x :: L)
| IsExpansionTop2 :
forall (x y : float) (L : list float),
Fbounded b x ->
is_Fzero y ->
Fbounded b y -> IsExpansion (x :: L) -> IsExpansion (x :: y :: L)
| IsExpansionTop :
forall (x y : float) (L : list float),
~ is_Fzero x ->
~ is_Fzero y ->
Fbounded b x ->
Fbounded b y ->
(MSB radix x < LSB radix y)%Z ->
IsExpansion (y :: L) -> IsExpansion (x :: y :: L).
Theorem Zlt_MSB_LSB :
forall x y : float,
~ is_Fzero y -> (MSB radix x < LSB radix y)%Z -> (Fabs x < Fabs y)%R.
intros x y H' H'0; case (is_FzeroP x); intros F0.
replace (FtoRradix (Fabs x)) with 0%R.
case (Rabs_pos y).
unfold FtoRradix in |- *; rewrite Fabs_correct; auto with arith.
intros H'1; Contradict H'.
apply is_Fzero_rep2 with (radix := radix); auto.
generalize H'1; unfold Rabs in |- *; case (Rcase_abs y); auto with real.
intros H'2 H'3; replace 0%R with (-0)%R; [ rewrite H'3 | idtac ]; fold FtoRradix;ring.
unfold Fabs in |- *; rewrite F0; unfold FtoRradix, FtoR in |- *;
simpl in |- *; ring.
case (Rle_or_lt (Fabs y) (Fabs x)); auto.
intros H'1; Contradict H'0.
apply Zle_not_lt; auto.
apply Zle_trans with (MSB radix y).
apply LSB_le_MSB; auto.
apply MSB_monotone; auto.
Qed.
Theorem IsExpansion_comp1 :
forall (L : list float) (x y : float),
Fbounded b y -> x = y :>R -> IsExpansion (x :: L) -> IsExpansion (y :: L).
simple induction L.
intros x y H' H'0 H'1; apply IsExpansionSingle; auto.
intros a l H' x y H'0 H'1 H'2; inversion H'2.
apply IsExpansionTop1; auto.
apply (is_Fzero_rep2 radix); auto with arith; unfold FtoRradix in H'1;
rewrite <- H'1; apply is_Fzero_rep1; auto.
apply IsExpansionTop2; auto.
apply (H' x); auto.
apply IsExpansionTop; auto.
Contradict H2; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'1; rewrite H'1; apply is_Fzero_rep1;
auto.
rewrite (MSB_comp radix) with (y := x); auto.
Contradict H2; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'1; rewrite H'1; apply is_Fzero_rep1;
auto.
Qed.
Theorem IsExpansion_comp2 :
forall (L : list float) (x y z : float),
Fbounded b z ->
y = z :>R -> IsExpansion (x :: y :: L) -> IsExpansion (x :: z :: L).
intros L x y z H' H'0 H'1; inversion H'1.
apply IsExpansionTop1; auto; apply IsExpansion_comp1 with y; auto.
apply IsExpansionTop2; auto.
apply (is_Fzero_rep2 radix); auto with arith; unfold FtoRradix in H'0;
rewrite <- H'0; apply is_Fzero_rep1; auto.
apply IsExpansionTop; auto.
Contradict H3; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'0; rewrite H'0; apply is_Fzero_rep1;
auto.
rewrite (LSB_comp radix) with (y := y); auto.
Contradict H3; apply (is_Fzero_rep2 radix); auto with arith;
unfold FtoRradix in H'0; rewrite H'0; apply is_Fzero_rep1;
auto.
apply IsExpansion_comp1 with (x := y); auto.
Qed.
Fixpoint expValue (L : list float) : float :=
match L with
| nil => Fzero 0
| x :: L1 => Fplus radix x (expValue L1)
end.
Fixpoint expNormalize (L : list float) : list float :=
match L with
| nil => nil
| x :: L1 =>
match Fnum x with
| Z0 => expNormalize L1
| Zpos p => x :: expNormalize L1
| Zneg p => x :: expNormalize L1
end
end.
Theorem expInv :
forall (a : float) (L : list float), IsExpansion (a :: L) -> IsExpansion L.
intros a L; generalize a; clear a; elim L; auto.
intros a H'; apply IsExpansionNil.
intros a l H' a0 H'0; inversion H'0; auto.
apply IsExpansionTop1; auto.
apply (H' a0); auto.
Qed.
Theorem expBoundedInv :
forall (a : float) (L : list float), IsExpansion (a :: L) -> Fbounded b a.
intros a L H'; inversion H'; auto.
Qed.
Theorem expNormalizeCorrect :
forall L : list float, expValue L = expValue (expNormalize L) :>R.
intros L; elim L; simpl in |- *; auto.
intros a l H'; CaseEq (Fnum a); simpl in |- *; unfold FtoRradix in |- *;
repeat rewrite Fplus_correct; auto with arith; unfold FtoRradix in H';
rewrite H'; auto.
intros H'0; rewrite is_Fzero_rep1; auto; rewrite Rplus_0_l; auto.
Qed.
Theorem expNormalizeExp :
forall L : list float, IsExpansion L -> IsExpansion (expNormalize L).
intros L H'; elim H'; auto.
simpl in |- *; apply IsExpansionNil; auto.
simpl in |- *; intros a Ha; case (Fnum a); try apply IsExpansionNil; intros;
apply IsExpansionSingle; auto.
simpl in |- *; intros x L0 H'0 H'1 H'2 H'3; rewrite H'0; auto.
intros x y L0 H'0 H'1 H'2 H'3; case (is_FzeroP x); intros Z0.
simpl in |- *; rewrite Z0; rewrite H'1; auto.
generalize Z0; unfold is_Fzero in |- *; simpl in |- *; case (Fnum x);
try (intros tmp; case tmp; auto; fail); rewrite H'1;
auto.
intros x y L0 H'0 H'1 H'2 H'3 H'4 H'5; simpl in |- *; generalize H'0 H'1;
unfold is_Fzero in |- *; case (Fnum x);
try (intros tmp; case tmp; auto; fail); intros p H;
case (Fnum y); try (intros tmp; case tmp; auto; fail);
intros; apply IsExpansionTop; auto.
Qed.
Inductive IsNzExpansion : list float -> Prop :=
| IsNzExpansionNil : IsNzExpansion nil
| IsNzExpansionSingle :
forall x : float,
~ is_Fzero x -> Fbounded b x -> IsNzExpansion (x :: nil)
| IsNzExpansionTop :
forall (x y : float) (L : list float),
~ is_Fzero x ->
~ is_Fzero y ->
Fbounded b x ->
Fbounded b y ->
(MSB radix x < LSB radix y)%Z ->
IsNzExpansion (y :: L) -> IsNzExpansion (x :: y :: L).
Theorem isNzExpansionIsExpansion :
forall l : list float, IsNzExpansion l -> IsExpansion l.
intros l H'; elim H'; simpl in |- *; auto.
apply IsExpansionNil.
intros x H'0 H'1; apply IsExpansionSingle; auto.
intros x y L H'0 H'1 H'2 H'3 H'4 H'5 H'6.
apply IsExpansionTop; auto.
Qed.
Theorem IsNzExpansionInv :
forall (a : float) (l : list float),
IsNzExpansion (a :: l) -> IsNzExpansion l.
intros a l H'; inversion H'; auto.
apply IsNzExpansionNil; auto.
Qed.
Inductive IsNzExpansionR : list float -> Prop :=
| IsNzExpansionNilR : IsNzExpansionR nil
| IsNzExpansionSingleR :
forall x : float,
~ is_Fzero x -> Fbounded b x -> IsNzExpansionR (x :: nil)
| IsNzExpansionTopR :
forall (x y : float) (L : list float),
~ is_Fzero x ->
~ is_Fzero y ->
Fbounded b x ->
Fbounded b y ->
(MSB radix y < LSB radix x)%Z ->
IsNzExpansionR (y :: L) -> IsNzExpansionR (x :: y :: L).
Theorem isNzExpansionRIsNzExpansion :
forall l : list float, IsNzExpansionR l -> IsNzExpansion (rev l).
intros l H'; elim H'; simpl in |- *; auto.
apply IsNzExpansionNil.
exact IsNzExpansionSingle.
intros x y L H'0 H'1 H'2 H'3 H'4 H'5; elim (rev L); simpl in |- *.
intros H'6; apply IsNzExpansionTop; auto.
apply IsNzExpansionSingle; auto.
intros a l0; case l0; simpl in |- *.
intros H'6 H'7; apply IsNzExpansionTop; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
apply IsNzExpansionTop; auto.
apply IsNzExpansionSingle; auto.
intros f l1 H'6 H'7; apply IsNzExpansionTop; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
inversion H'7; auto.
apply H'6.
inversion H'7; auto.
Qed.
Theorem IsNzExpansionRInv :
forall (a : float) (l : list float),
IsNzExpansionR (a :: l) -> IsNzExpansionR l.
intros a l H'; inversion H'; auto.
apply IsNzExpansionNilR; auto.
Qed.
Theorem mkIsNzAux :
forall (n : nat) (p : float),
(- dExp b <= LSB radix p)%Z ->
(MSB radix p < - dExp b + n)%Z ->
exists l : list float,
IsNzExpansionR l /\
p = expValue l :>R /\
match l with
| a :: _ => ToZeroP b radix p a
| nil => True
end.
intros n; elim n.
intros p H' H'0; case (is_FzeroP p); intros H'1.
exists (nil (A:=float)); repeat split; simpl in |- *; auto.
apply IsNzExpansionNilR.
replace (FtoRradix (Fzero 0)) with 0%R.
unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
absurd (LSB radix p <= MSB radix p)%Z.
apply Zlt_not_le.
apply Zlt_le_trans with (1 := H'0).
replace (- dExp b + 0%nat)%Z with (- dExp b)%Z; [ auto | ring ].
apply LSB_le_MSB; auto.
intros n0 H' p H'0 H'1.
case (is_FzeroP p); intros H'2.
exists (nil (A:=float)); repeat split; simpl in |- *; auto.
apply IsNzExpansionNilR.
replace (FtoRradix (Fzero 0)) with 0%R.
unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
cut (TotalP (ToZeroP b radix));
[ intros tmp1; case (tmp1 (FtoRradix p)); clear tmp1; intros a Ha
| apply ToZeroTotal with (precision := precision) ];
auto.
cut (~ is_Fzero a); [ intros Na | idtac ].
2: red in |- *; intros H'6; absurd (a = 0%R :>R).
2: apply
(MSBBoundNotZero b radix precision) with (P := ToZeroP b radix) (f1 := p);
auto.
2: apply ToZeroRoundedModeP with (precision := precision); auto.
2: Contradict H'2.
2: apply is_Fzero_rep2 with (radix := radix); auto.
2: apply Zle_trans with (1 := H'0).
2: apply LSB_le_MSB; auto.
2: unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
case (is_FzeroP (Fminus radix p a)); intros H'3.
exists (a :: nil); repeat split; auto.
apply IsNzExpansionSingleR; auto.
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
simpl in |- *.
replace (FtoRradix p) with (FtoRradix (Fplus radix (Fminus radix p a) a)).
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with real arith.
replace (FtoR radix (Fminus radix p a)) with 0%R.
replace (FtoR radix (Fzero 0)) with 0%R.
apply Rplus_comm.
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
apply sym_eq; apply is_Fzero_rep1; auto.
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with real arith;
repeat rewrite Fminus_correct; auto with real arith;
ring.
elim (H' (Fminus radix p a));
[ intros l E; elim E; intros H'7 H'8; elim H'8; intros H'9 H'10; clear H'8 E
| idtac
| idtac ]; auto.
exists (a :: l); repeat split; auto.
generalize H'7 H'10; case l.
intros H'4 H'5; apply IsNzExpansionSingleR; auto.
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
intros f l0 H'4 H'5.
apply IsNzExpansionTopR; auto.
inversion H'4; auto.
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
inversion H'4; auto.
replace (MSB radix f) with (MSB radix (Fminus radix p a)).
apply (MSBroundLSB b radix precision) with (P := ToZeroP b radix); auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
apply (MSBtoZero b radix precision); auto.
inversion H'4; auto.
simpl in |- *; unfold FtoRradix in |- *; rewrite Fplus_correct;
auto with arith.
unfold FtoRradix in H'9; rewrite <- H'9.
rewrite Fminus_correct; auto with arith; ring.
apply Zle_trans with (Zmin (LSB radix p) (LSB radix a)).
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp a).
cut (Fbounded b a); [ auto with float | idtac ].
apply
RoundedModeBounded
with (radix := radix) (P := ToZeroP b radix) (r := FtoRradix p);
auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
apply Fexp_le_LSB; auto.
apply LSBMinus; auto.
apply Zlt_le_trans with (LSB radix a).
apply (MSBroundLSB b radix precision) with (P := ToZeroP b radix); auto.
apply ToZeroRoundedModeP with (precision := precision); auto.
apply Zle_trans with (MSB radix a); auto.
apply LSB_le_MSB; auto.
rewrite <- (MSBtoZero b radix precision) with (f1 := p) (f2 := a); auto.
apply Zlt_succ_le.
replace (Zsucc (- dExp b + n0)) with (- dExp b + S n0)%Z; auto.
rewrite inj_S; unfold Zsucc in |- *; ring.
Qed.
Theorem expValueApp :
forall l1 l2 : list float,
expValue (l1 ++ l2) = (expValue l1 + expValue l2)%R :>R.
intros l1; elim l1; simpl in |- *; auto.
intros l2; unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
intros a l H' l2.
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with zarith.
rewrite H'; unfold FtoRradix in |- *; ring.
Qed.
Theorem expValueRev :
forall l : list float, expValue (rev l) = expValue l :>R.
intros l; elim l; simpl in |- *; auto.
intros a l0 H'; rewrite expValueApp; simpl in |- *.
rewrite H'.
unfold FtoRradix in |- *; repeat rewrite Fplus_correct; auto with zarith.
replace (FtoR radix (Fzero 0)) with 0%R; [ ring | idtac ].
unfold FtoRradix, FtoR, Fzero in |- *; simpl in |- *; ring.
Qed.
Theorem existExp :
forall p : float,
(- dExp b <= LSB radix p)%Z ->
exists l : list float, IsExpansion l /\ p = expValue l :>R.
intros p H'.
elim (mkIsNzAux ( Zabs_nat (dExp b)+1 + Zabs_nat (MSB radix p)) p);
[ intros l E; elim E; intros H'3 H'4; elim H'4; intros H'5 H'6; clear H'4 E
| idtac
| idtac ]; auto.
exists (rev l); split; auto.
apply isNzExpansionIsExpansion.
apply isNzExpansionRIsNzExpansion; auto.
rewrite expValueRev; auto.
apply Zle_lt_trans with (Z_of_nat (Zabs_nat (MSB radix p))).
rewrite <- Zabs_absolu.
case (MSB radix p); simpl in |- *; auto with zarith; intros;
unfold Zle in |- *; simpl in |- *; red in |- *; intros;
discriminate.
rewrite inj_plus.
rewrite inj_plus.
rewrite <- (Zabs_absolu (Z_of_N (dExp b))).
rewrite Zabs_eq; [idtac|case (dExp b)]; auto with zarith.
rewrite Zplus_assoc.
replace (- dExp b + (dExp b + S 0))%Z with (Zsucc 0).
auto with zarith.
ring.
Qed.
End mf.