Library Float.Expansions.Fexp2
Require Export ThreeSumProps.
Require Export List.
Section Fexp2.
Variable b : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Hypothesis Ngd : (1 ≤ pPred (vNum b) × (1 - / radix))%R.
Hypothesis Ngd2 : (6%nat ≤ pPred (vNum b) × (1 - / radix × / radix))%R.
Inductive IsExp : list float → Prop :=
| IsExpNil : IsExp nil
| IsExpSingle : ∀ x : float, Fbounded b x → IsExp (x :: nil)
| IsExpTop :
∀ (x y : float) (L : list float),
Fbounded b x →
Fbounded b y →
(Fexp y ≤ Fexp x)%Z → IsExp (y :: L) → IsExp (x :: y :: L).
Hint Resolve IsExpNil IsExpSingle IsExpTop.
Inductive NearEqual : list float → list float → Prop :=
| IsEqual : ∀ x : list float, NearEqual x x
| OneMoreR :
∀ (x : list float) (e : float),
Fbounded b e → NearEqual x (e :: x).
Hint Resolve IsEqual OneMoreR.
Fixpoint sum (L : list float) : R :=
match L with
| nil ⇒ 0%R
| x :: L1 ⇒ (FtoRradix x + sum L1)%R
end.
Definition hdexp (L : list float) :=
match L with
| nil ⇒ (- dExp b)%Z
| x :: L1 ⇒ Fexp x
end.
Fixpoint lastexp (L : list float) : Z :=
match L with
| nil ⇒ (- dExp b)%Z
| x :: nil ⇒ Fexp x
| x :: L1 ⇒ lastexp L1
end.
Definition hd (L : list float) :=
match L with
| nil ⇒ Fzero (- dExp b)
| x :: L1 ⇒ x
end.
Theorem IsExpZle :
∀ (i : float) (L : list float), IsExp (i :: L) → (hdexp L ≤ Fexp i)%Z.
simple induction L; simpl in |- ×.
intros H; cut (Fbounded b i).
intros H'; case H'; auto.
inversion H; auto.
intros a l H H0; inversion H0; auto.
Qed.
Theorem isExpInv :
∀ (x y : float) (L : list float), IsExp (x :: y :: L) → IsExp (y :: L).
intros x y L H; inversion H; auto.
Qed.
Theorem isExpSkip :
∀ (x y : float) (L : list float), IsExp (x :: y :: L) → IsExp (x :: L).
intros x y L; case L; simpl in |- ×.
intros H1; apply IsExpSingle; inversion H1; auto.
intros f l H1; apply IsExpTop; inversion H1;
(cut (IsExp (y :: f :: l)); [ intros T2; inversion T2 | idtac ]);
auto.
apply Zle_trans with (Fexp y); auto.
Qed.
Theorem sum_IsExp :
∀ (L : list float) (x : float) (m : R),
IsExp (x :: L) →
(Float (pPred (vNum b)) (Fexp x) ≤ m)%R →
(Rabs (sum (x :: L)) ≤ length (x :: L) × m)%R.
intros L x m H H0.
replace (sum (x :: L)) with (x + sum L)%R;
[ idtac | simpl in |- *; auto with real ].
apply Rle_trans with (Rabs x + Rabs (sum L))%R;
[ apply Rabs_triang
| replace (INR (length (x :: L))) with (1 + length L)%R ].
replace ((1 + length L) × m)%R with (m + length L × m)%R; [ idtac | ring ].
apply Rle_trans with (m + Rabs (sum L))%R.
apply Rplus_le_compat_r.
apply Rle_trans with (FtoR radix (Float (pPred (vNum b)) (Fexp x)));
[ rewrite <- (Fabs_correct radix); auto with zarith; apply maxMax1;
auto with zarith
| idtac ]; auto.
inversion H; auto.
apply Rplus_le_compat_l.
induction L as [| a L HrecL].
simpl in |- *; rewrite Rabs_R0; auto with real.
replace (sum (a :: L)) with (a + sum L)%R;
[ idtac | simpl in |- *; auto with real ].
apply Rle_trans with (Rabs a + Rabs (sum L))%R;
[ apply Rabs_triang
| replace (INR (length (a :: L))) with (1 + length L)%R ].
replace ((1 + length L) × m)%R with (m + length L × m)%R; [ idtac | ring ].
apply Rle_trans with (m + Rabs (sum L))%R.
apply Rplus_le_compat_r.
apply Rle_trans with (FtoR radix (Float (pPred (vNum b)) (Fexp a)));
[ rewrite <- (Fabs_correct radix); auto with zarith; apply maxMax1;
auto with zarith
| idtac ]; auto.
inversion H; auto.
apply Rle_trans with (FtoRradix (Float (pPred (vNum b)) (Fexp x))); auto.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
apply Rmult_le_compat_l; auto with real zarith.
apply (Rle_IZRO 0); apply Zlt_le_weak;
apply (pPredMoreThanOne b radix) with (precision := precision);
auto with real zarith.
replace 2%R with (IZR radix); auto with real zarith.
inversion H; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rplus_le_compat_l.
apply HrecL.
apply isExpSkip with (y := a); auto.
rewrite (Rplus_comm 1 (length L)); simpl in |- *; auto with real arith.
case (length L); intros; auto with real arith.
rewrite (Rplus_comm 1 (length L)); simpl in |- *; auto with real arith.
case (length L); intros; auto with real arith.
Qed.
Inductive IsRleExp : list float → Prop :=
| IsRleExpNil : IsRleExp nil
| IsRleExpSingle : ∀ x : float, Fbounded b x → IsRleExp (x :: nil)
| IsRleExpTop :
∀ (x y : float) (L : list float),
Fbounded b x →
Fbounded b y →
(Rabs x ≤ Rabs y)%R → IsRleExp (y :: L) → IsRleExp (x :: y :: L).
Hint Resolve IsRleExpNil IsRleExpSingle IsRleExpTop.
Inductive EqListFloat : list float → list float → Prop :=
| EqListFloatnil : EqListFloat nil nil
| EqListFloatTop :
∀ (x y : float) (L L' : list float),
Fbounded b x →
Fbounded b y →
x = y :>R → EqListFloat L L' → EqListFloat (x :: L) (y :: L').
Hint Resolve EqListFloatnil EqListFloatTop.
Theorem sum_app :
∀ (L : list float) (x : float), (x + sum L)%R = sum (L ++ x :: nil) :>R.
intros L x; induction L as [| a L HrecL]; simpl in |- *; auto.
replace (x + (a + sum L))%R with (a + (x + sum L))%R;
[ rewrite HrecL | ring ]; auto.
Qed.
Theorem cons_neq :
∀ (x : float) (L : list float), x :: L ≠ L :>list float.
intros x L; red in |- *; intros H; absurd (length L < length (x :: L)).
rewrite H; auto with arith.
simpl in |- *; auto with arith.
Qed.
Definition endof (all part : list float) :=
∃ rest : list float, all = rest ++ part.
Theorem app_length :
∀ l1 l2 : list float, length (l1 ++ l2) = length l1 + length l2.
intros l1; induction l1 as [| a l1 Hrecl1]; simpl in |- *; auto.
Qed.
Theorem endof_length :
∀ L l : list float, endof L l → length l ≤ length L.
intros L l H; case H.
intros x H0; rewrite H0.
rewrite (app_length x l); auto with arith.
Qed.
Inductive IsCanExp : list float → Prop :=
| IsCanExpNil : IsCanExp nil
| IsCanExpTop :
∀ (x : float) (L : list float),
Fcanonic radix b x → IsCanExp L → IsCanExp (x :: L).
Hint Resolve IsCanExpNil IsCanExpTop.
Theorem IsCanExpBounded :
∀ (i : float) (L : list float), IsCanExp (i :: L) → Fbounded b i.
intros i L H; try apply FcanonicBound with radix.
inversion H; auto.
Qed.
Inductive IsRleExpRev : list float → Prop :=
| IsRleExpRevNil : IsRleExpRev nil
| IsRleExpRevSingle :
∀ x : float, Fbounded b x → IsRleExpRev (x :: nil)
| IsRleRevExpTop :
∀ (x y : float) (L : list float),
Fbounded b x →
Fbounded b y →
(Rabs y ≤ Rabs x)%R →
IsRleExpRev (y :: L) → IsRleExpRev (x :: y :: L).
Hint Resolve IsRleExpRevNil IsRleExpRevSingle IsRleRevExpTop.
Theorem IsRleExpRevComp :
∀ L1 L2, EqListFloat L1 L2 → IsRleExpRev L1 → IsRleExpRev L2.
intros L1 L2 H; elim H; auto.
intros x y L L' H0 H1 H2 H3; inversion H3; auto.
intros H10 H11; apply IsRleRevExpTop; auto.
rewrite <- H6; rewrite <- H2; inversion H11; auto.
inversion H11; auto.
Qed.
Theorem IsRleExpRevIsExp :
∀ L : list float,
IsRleExpRev L →
∃ L' : list float,
IsCanExp L' ∧ IsRleExpRev L' ∧ EqListFloat L L' ∧ IsExp L'.
intros L; induction L as [| a L HrecL].
intros H1; ∃ (nil (A:=float)); repeat split;
[ apply IsCanExpNil
| apply IsRleExpRevNil
| apply EqListFloatnil
| apply IsExpNil ].
intros H2; case HrecL; auto.
inversion H2; auto; apply IsRleExpRevNil.
intros L' (H'1, (H'2, (H'3, H'4))).
cut (Fbounded b a); [ intros Ba | inversion H2; auto ].
cut (Fcanonic radix b (Fnormalize radix b precision a));
[ intros CNa | apply FnormalizeCanonic; auto with zarith ].
cut (Fbounded b (Fnormalize radix b precision a));
[ intros BNa | apply FnormalizeBounded; auto with zarith ].
cut (Fnormalize radix b precision a = a :>R);
[ intros Eq1
| unfold FtoRradix in |- *; apply FnormalizeCorrect; auto with zarith ].
∃ (Fnormalize radix b precision a :: L'); repeat split; auto.
generalize H'2 H'3; case L'; simpl in |- *; auto.
intros f l H'0 H'5; apply IsRleRevExpTop; auto.
inversion H'0; auto.
rewrite Eq1; inversion H2.
cut (IsRleExpRev (a :: f :: l)); [ intros Z1; inversion Z1; auto | idtac ].
apply IsRleExpRevComp with (L1 := a :: L); auto.
cut (IsRleExpRev (a :: f :: l)); [ intros Z1; inversion Z1; auto | idtac ].
apply IsRleExpRevComp with (L1 := a :: L); auto.
generalize H'4 H'3 H'2 H'1; case L'; simpl in |- *; auto.
intros f l H'0 H'5 H'6 H'7; apply IsExpTop; auto.
inversion H'6; auto.
apply Fcanonic_Rle_Zle with radix b precision; auto with zarith.
inversion H'7; auto.
fold FtoRradix in |- *; rewrite Eq1.
cut (IsRleExpRev (a :: f :: l)); [ intros Z1; inversion Z1; auto | idtac ].
apply IsRleExpRevComp with (L1 := a :: L); auto.
Qed.
Fixpoint last (L : list float) : float :=
match L with
| nil ⇒ Fzero (- dExp b)
| x :: nil ⇒ x
| x :: L1 ⇒ last L1
end.
Theorem ExpRev_aux :
∀ (l : list float) (x : float),
Fbounded b x →
IsRleExpRev l → (Rabs x ≤ Rabs (last l))%R → IsRleExpRev (l ++ x :: nil).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
intros H x H0 H1 H2; simpl in |- *; auto.
apply IsRleRevExpTop; auto.
inversion H1; auto.
intros f l1 H x H0 H1 H2; simpl in |- *; auto.
apply IsRleRevExpTop; auto.
inversion H1; auto.
cut (IsRleExpRev (f :: l1)); [ intros Z1; inversion Z1 | inversion H1 ]; auto.
inversion H1; auto.
change (IsRleExpRev ((f :: l1) ++ x :: nil)) in |- *; apply H; auto.
inversion H1; auto.
Qed.
Theorem Exp_aux :
∀ (l : list float) (x : float),
Fbounded b x →
IsRleExp l → (Rabs (last l) ≤ Rabs x)%R → IsRleExp (l ++ x :: nil).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
intros H x H0 H1 H2; simpl in |- *; auto.
apply IsRleExpTop; auto.
inversion H1; auto.
intros f l1 H x H0 H1 H2; simpl in |- ×.
apply IsRleExpTop; auto.
inversion H1; auto.
cut (IsRleExp (f :: l1)); [ intros Z1; inversion Z1 | inversion H1 ]; auto.
inversion H1; auto.
change (IsRleExp ((f :: l1) ++ x :: nil)) in |- *; auto.
apply H; auto.
inversion H1; auto.
Qed.
Theorem last_hd : ∀ l : list float, last l = hd (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0; auto.
intros f l1 H; rewrite H; cut (rev (f :: l1) ≠ nil).
case (rev (f :: l1)); simpl in |- *; auto; intros Z1; case Z1; auto.
case l1; simpl in |- *; auto.
red in |- *; intros H0; discriminate.
intros f0 l2; case (rev l2); simpl in |- *; intros; red in |- *; intros;
discriminate.
Qed.
Theorem IsRleExpRev_IsRleExp :
∀ l : list float, IsRleExpRev l → IsRleExp (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
simpl in |- *; auto.
intros H H0; apply IsRleExpSingle; auto; inversion H0; auto.
intros f l1 H H0; apply Exp_aux; auto.
inversion H0; auto.
apply H; auto.
inversion H0; auto.
replace (last (rev (f :: l1))) with f; [ inversion H0; auto | auto ].
rewrite (last_hd (rev (f :: l1))).
rewrite (rev_involutive (f :: l1)); auto.
Qed.
Theorem IsRleExp_IsRleExpRev :
∀ l : list float, IsRleExp l → IsRleExpRev (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
intros H H0; simpl in |- *; apply IsRleExpRevSingle; inversion H0; auto.
intros f l1 H H0; apply ExpRev_aux; auto.
inversion H0; auto.
apply H.
inversion H0; auto.
replace (last (rev (f :: l1))) with f; [ inversion H0; auto | auto ].
rewrite (last_hd (rev (f :: l1))).
rewrite (rev_involutive (f :: l1)); auto.
Qed.
Theorem EqListFloat_length :
∀ l l' : list float, EqListFloat l l' → length l = length l'.
intros l l' H; elim H; simpl in |- *; auto.
Qed.
Theorem EqListFloat_sum :
∀ l l' : list float, EqListFloat l l' → sum l = sum l' :>R.
intros l l' H; elim H; simpl in |- *; auto.
intros x y L L' H0 H1 H2 H3 H4; rewrite H4; rewrite H2; auto.
Qed.
Theorem rev_sum : ∀ l : list float, sum l = sum (rev l) :>R.
intros l; elim l; simpl in |- *; auto.
intros a l0 H; rewrite H.
apply sum_app.
Qed.
Theorem rev_length : ∀ l : list float, length l = length (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0 H; rewrite H; rewrite app_length; simpl in |- *; ring.
Qed.
End Fexp2.
Require Export List.
Section Fexp2.
Variable b : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Hypothesis Ngd : (1 ≤ pPred (vNum b) × (1 - / radix))%R.
Hypothesis Ngd2 : (6%nat ≤ pPred (vNum b) × (1 - / radix × / radix))%R.
Inductive IsExp : list float → Prop :=
| IsExpNil : IsExp nil
| IsExpSingle : ∀ x : float, Fbounded b x → IsExp (x :: nil)
| IsExpTop :
∀ (x y : float) (L : list float),
Fbounded b x →
Fbounded b y →
(Fexp y ≤ Fexp x)%Z → IsExp (y :: L) → IsExp (x :: y :: L).
Hint Resolve IsExpNil IsExpSingle IsExpTop.
Inductive NearEqual : list float → list float → Prop :=
| IsEqual : ∀ x : list float, NearEqual x x
| OneMoreR :
∀ (x : list float) (e : float),
Fbounded b e → NearEqual x (e :: x).
Hint Resolve IsEqual OneMoreR.
Fixpoint sum (L : list float) : R :=
match L with
| nil ⇒ 0%R
| x :: L1 ⇒ (FtoRradix x + sum L1)%R
end.
Definition hdexp (L : list float) :=
match L with
| nil ⇒ (- dExp b)%Z
| x :: L1 ⇒ Fexp x
end.
Fixpoint lastexp (L : list float) : Z :=
match L with
| nil ⇒ (- dExp b)%Z
| x :: nil ⇒ Fexp x
| x :: L1 ⇒ lastexp L1
end.
Definition hd (L : list float) :=
match L with
| nil ⇒ Fzero (- dExp b)
| x :: L1 ⇒ x
end.
Theorem IsExpZle :
∀ (i : float) (L : list float), IsExp (i :: L) → (hdexp L ≤ Fexp i)%Z.
simple induction L; simpl in |- ×.
intros H; cut (Fbounded b i).
intros H'; case H'; auto.
inversion H; auto.
intros a l H H0; inversion H0; auto.
Qed.
Theorem isExpInv :
∀ (x y : float) (L : list float), IsExp (x :: y :: L) → IsExp (y :: L).
intros x y L H; inversion H; auto.
Qed.
Theorem isExpSkip :
∀ (x y : float) (L : list float), IsExp (x :: y :: L) → IsExp (x :: L).
intros x y L; case L; simpl in |- ×.
intros H1; apply IsExpSingle; inversion H1; auto.
intros f l H1; apply IsExpTop; inversion H1;
(cut (IsExp (y :: f :: l)); [ intros T2; inversion T2 | idtac ]);
auto.
apply Zle_trans with (Fexp y); auto.
Qed.
Theorem sum_IsExp :
∀ (L : list float) (x : float) (m : R),
IsExp (x :: L) →
(Float (pPred (vNum b)) (Fexp x) ≤ m)%R →
(Rabs (sum (x :: L)) ≤ length (x :: L) × m)%R.
intros L x m H H0.
replace (sum (x :: L)) with (x + sum L)%R;
[ idtac | simpl in |- *; auto with real ].
apply Rle_trans with (Rabs x + Rabs (sum L))%R;
[ apply Rabs_triang
| replace (INR (length (x :: L))) with (1 + length L)%R ].
replace ((1 + length L) × m)%R with (m + length L × m)%R; [ idtac | ring ].
apply Rle_trans with (m + Rabs (sum L))%R.
apply Rplus_le_compat_r.
apply Rle_trans with (FtoR radix (Float (pPred (vNum b)) (Fexp x)));
[ rewrite <- (Fabs_correct radix); auto with zarith; apply maxMax1;
auto with zarith
| idtac ]; auto.
inversion H; auto.
apply Rplus_le_compat_l.
induction L as [| a L HrecL].
simpl in |- *; rewrite Rabs_R0; auto with real.
replace (sum (a :: L)) with (a + sum L)%R;
[ idtac | simpl in |- *; auto with real ].
apply Rle_trans with (Rabs a + Rabs (sum L))%R;
[ apply Rabs_triang
| replace (INR (length (a :: L))) with (1 + length L)%R ].
replace ((1 + length L) × m)%R with (m + length L × m)%R; [ idtac | ring ].
apply Rle_trans with (m + Rabs (sum L))%R.
apply Rplus_le_compat_r.
apply Rle_trans with (FtoR radix (Float (pPred (vNum b)) (Fexp a)));
[ rewrite <- (Fabs_correct radix); auto with zarith; apply maxMax1;
auto with zarith
| idtac ]; auto.
inversion H; auto.
apply Rle_trans with (FtoRradix (Float (pPred (vNum b)) (Fexp x))); auto.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
apply Rmult_le_compat_l; auto with real zarith.
apply (Rle_IZRO 0); apply Zlt_le_weak;
apply (pPredMoreThanOne b radix) with (precision := precision);
auto with real zarith.
replace 2%R with (IZR radix); auto with real zarith.
inversion H; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rplus_le_compat_l.
apply HrecL.
apply isExpSkip with (y := a); auto.
rewrite (Rplus_comm 1 (length L)); simpl in |- *; auto with real arith.
case (length L); intros; auto with real arith.
rewrite (Rplus_comm 1 (length L)); simpl in |- *; auto with real arith.
case (length L); intros; auto with real arith.
Qed.
Inductive IsRleExp : list float → Prop :=
| IsRleExpNil : IsRleExp nil
| IsRleExpSingle : ∀ x : float, Fbounded b x → IsRleExp (x :: nil)
| IsRleExpTop :
∀ (x y : float) (L : list float),
Fbounded b x →
Fbounded b y →
(Rabs x ≤ Rabs y)%R → IsRleExp (y :: L) → IsRleExp (x :: y :: L).
Hint Resolve IsRleExpNil IsRleExpSingle IsRleExpTop.
Inductive EqListFloat : list float → list float → Prop :=
| EqListFloatnil : EqListFloat nil nil
| EqListFloatTop :
∀ (x y : float) (L L' : list float),
Fbounded b x →
Fbounded b y →
x = y :>R → EqListFloat L L' → EqListFloat (x :: L) (y :: L').
Hint Resolve EqListFloatnil EqListFloatTop.
Theorem sum_app :
∀ (L : list float) (x : float), (x + sum L)%R = sum (L ++ x :: nil) :>R.
intros L x; induction L as [| a L HrecL]; simpl in |- *; auto.
replace (x + (a + sum L))%R with (a + (x + sum L))%R;
[ rewrite HrecL | ring ]; auto.
Qed.
Theorem cons_neq :
∀ (x : float) (L : list float), x :: L ≠ L :>list float.
intros x L; red in |- *; intros H; absurd (length L < length (x :: L)).
rewrite H; auto with arith.
simpl in |- *; auto with arith.
Qed.
Definition endof (all part : list float) :=
∃ rest : list float, all = rest ++ part.
Theorem app_length :
∀ l1 l2 : list float, length (l1 ++ l2) = length l1 + length l2.
intros l1; induction l1 as [| a l1 Hrecl1]; simpl in |- *; auto.
Qed.
Theorem endof_length :
∀ L l : list float, endof L l → length l ≤ length L.
intros L l H; case H.
intros x H0; rewrite H0.
rewrite (app_length x l); auto with arith.
Qed.
Inductive IsCanExp : list float → Prop :=
| IsCanExpNil : IsCanExp nil
| IsCanExpTop :
∀ (x : float) (L : list float),
Fcanonic radix b x → IsCanExp L → IsCanExp (x :: L).
Hint Resolve IsCanExpNil IsCanExpTop.
Theorem IsCanExpBounded :
∀ (i : float) (L : list float), IsCanExp (i :: L) → Fbounded b i.
intros i L H; try apply FcanonicBound with radix.
inversion H; auto.
Qed.
Inductive IsRleExpRev : list float → Prop :=
| IsRleExpRevNil : IsRleExpRev nil
| IsRleExpRevSingle :
∀ x : float, Fbounded b x → IsRleExpRev (x :: nil)
| IsRleRevExpTop :
∀ (x y : float) (L : list float),
Fbounded b x →
Fbounded b y →
(Rabs y ≤ Rabs x)%R →
IsRleExpRev (y :: L) → IsRleExpRev (x :: y :: L).
Hint Resolve IsRleExpRevNil IsRleExpRevSingle IsRleRevExpTop.
Theorem IsRleExpRevComp :
∀ L1 L2, EqListFloat L1 L2 → IsRleExpRev L1 → IsRleExpRev L2.
intros L1 L2 H; elim H; auto.
intros x y L L' H0 H1 H2 H3; inversion H3; auto.
intros H10 H11; apply IsRleRevExpTop; auto.
rewrite <- H6; rewrite <- H2; inversion H11; auto.
inversion H11; auto.
Qed.
Theorem IsRleExpRevIsExp :
∀ L : list float,
IsRleExpRev L →
∃ L' : list float,
IsCanExp L' ∧ IsRleExpRev L' ∧ EqListFloat L L' ∧ IsExp L'.
intros L; induction L as [| a L HrecL].
intros H1; ∃ (nil (A:=float)); repeat split;
[ apply IsCanExpNil
| apply IsRleExpRevNil
| apply EqListFloatnil
| apply IsExpNil ].
intros H2; case HrecL; auto.
inversion H2; auto; apply IsRleExpRevNil.
intros L' (H'1, (H'2, (H'3, H'4))).
cut (Fbounded b a); [ intros Ba | inversion H2; auto ].
cut (Fcanonic radix b (Fnormalize radix b precision a));
[ intros CNa | apply FnormalizeCanonic; auto with zarith ].
cut (Fbounded b (Fnormalize radix b precision a));
[ intros BNa | apply FnormalizeBounded; auto with zarith ].
cut (Fnormalize radix b precision a = a :>R);
[ intros Eq1
| unfold FtoRradix in |- *; apply FnormalizeCorrect; auto with zarith ].
∃ (Fnormalize radix b precision a :: L'); repeat split; auto.
generalize H'2 H'3; case L'; simpl in |- *; auto.
intros f l H'0 H'5; apply IsRleRevExpTop; auto.
inversion H'0; auto.
rewrite Eq1; inversion H2.
cut (IsRleExpRev (a :: f :: l)); [ intros Z1; inversion Z1; auto | idtac ].
apply IsRleExpRevComp with (L1 := a :: L); auto.
cut (IsRleExpRev (a :: f :: l)); [ intros Z1; inversion Z1; auto | idtac ].
apply IsRleExpRevComp with (L1 := a :: L); auto.
generalize H'4 H'3 H'2 H'1; case L'; simpl in |- *; auto.
intros f l H'0 H'5 H'6 H'7; apply IsExpTop; auto.
inversion H'6; auto.
apply Fcanonic_Rle_Zle with radix b precision; auto with zarith.
inversion H'7; auto.
fold FtoRradix in |- *; rewrite Eq1.
cut (IsRleExpRev (a :: f :: l)); [ intros Z1; inversion Z1; auto | idtac ].
apply IsRleExpRevComp with (L1 := a :: L); auto.
Qed.
Fixpoint last (L : list float) : float :=
match L with
| nil ⇒ Fzero (- dExp b)
| x :: nil ⇒ x
| x :: L1 ⇒ last L1
end.
Theorem ExpRev_aux :
∀ (l : list float) (x : float),
Fbounded b x →
IsRleExpRev l → (Rabs x ≤ Rabs (last l))%R → IsRleExpRev (l ++ x :: nil).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
intros H x H0 H1 H2; simpl in |- *; auto.
apply IsRleRevExpTop; auto.
inversion H1; auto.
intros f l1 H x H0 H1 H2; simpl in |- *; auto.
apply IsRleRevExpTop; auto.
inversion H1; auto.
cut (IsRleExpRev (f :: l1)); [ intros Z1; inversion Z1 | inversion H1 ]; auto.
inversion H1; auto.
change (IsRleExpRev ((f :: l1) ++ x :: nil)) in |- *; apply H; auto.
inversion H1; auto.
Qed.
Theorem Exp_aux :
∀ (l : list float) (x : float),
Fbounded b x →
IsRleExp l → (Rabs (last l) ≤ Rabs x)%R → IsRleExp (l ++ x :: nil).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
intros H x H0 H1 H2; simpl in |- *; auto.
apply IsRleExpTop; auto.
inversion H1; auto.
intros f l1 H x H0 H1 H2; simpl in |- ×.
apply IsRleExpTop; auto.
inversion H1; auto.
cut (IsRleExp (f :: l1)); [ intros Z1; inversion Z1 | inversion H1 ]; auto.
inversion H1; auto.
change (IsRleExp ((f :: l1) ++ x :: nil)) in |- *; auto.
apply H; auto.
inversion H1; auto.
Qed.
Theorem last_hd : ∀ l : list float, last l = hd (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0; auto.
intros f l1 H; rewrite H; cut (rev (f :: l1) ≠ nil).
case (rev (f :: l1)); simpl in |- *; auto; intros Z1; case Z1; auto.
case l1; simpl in |- *; auto.
red in |- *; intros H0; discriminate.
intros f0 l2; case (rev l2); simpl in |- *; intros; red in |- *; intros;
discriminate.
Qed.
Theorem IsRleExpRev_IsRleExp :
∀ l : list float, IsRleExpRev l → IsRleExp (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
simpl in |- *; auto.
intros H H0; apply IsRleExpSingle; auto; inversion H0; auto.
intros f l1 H H0; apply Exp_aux; auto.
inversion H0; auto.
apply H; auto.
inversion H0; auto.
replace (last (rev (f :: l1))) with f; [ inversion H0; auto | auto ].
rewrite (last_hd (rev (f :: l1))).
rewrite (rev_involutive (f :: l1)); auto.
Qed.
Theorem IsRleExp_IsRleExpRev :
∀ l : list float, IsRleExp l → IsRleExpRev (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0; case l0.
intros H H0; simpl in |- *; apply IsRleExpRevSingle; inversion H0; auto.
intros f l1 H H0; apply ExpRev_aux; auto.
inversion H0; auto.
apply H.
inversion H0; auto.
replace (last (rev (f :: l1))) with f; [ inversion H0; auto | auto ].
rewrite (last_hd (rev (f :: l1))).
rewrite (rev_involutive (f :: l1)); auto.
Qed.
Theorem EqListFloat_length :
∀ l l' : list float, EqListFloat l l' → length l = length l'.
intros l l' H; elim H; simpl in |- *; auto.
Qed.
Theorem EqListFloat_sum :
∀ l l' : list float, EqListFloat l l' → sum l = sum l' :>R.
intros l l' H; elim H; simpl in |- *; auto.
intros x y L L' H0 H1 H2 H3 H4; rewrite H4; rewrite H2; auto.
Qed.
Theorem rev_sum : ∀ l : list float, sum l = sum (rev l) :>R.
intros l; elim l; simpl in |- *; auto.
intros a l0 H; rewrite H.
apply sum_app.
Qed.
Theorem rev_length : ∀ l : list float, length l = length (rev l).
intros l; elim l; simpl in |- *; auto.
intros a l0 H; rewrite H; rewrite app_length; simpl in |- *; ring.
Qed.
End Fexp2.