Commit d3cd302b by Guillaume Melquiond

### Renamed some helpers. Imported float_distribution from Gappa.

parent e5dfbe02
 ... ... @@ -5,66 +5,158 @@ Section Float_prop. Variable beta : radix. Notation bpow := (epow beta). Notation bpow e := (epow beta e). Theorem F2R_ge_0_imp_Fnum : forall f : float beta, (0 <= F2R f)%R -> (0 <= Fnum f)%Z. Theorem F2R_ge_0_reg : forall m e : Z, (0 <= F2R (Float beta m e))%R -> (0 <= m)%Z. Proof. intros f H. intros m e H. apply le_Z2R. apply Rmult_le_reg_l with (bpow (Fexp f)). apply Rmult_le_reg_r with (bpow e). apply epow_gt_0. rewrite Rmult_0_r. now rewrite Rmult_comm. now rewrite Rmult_0_l. Qed. Theorem F2R_le_0_imp_Fnum : forall f : float beta, (F2R f <= 0)%R -> (Fnum f <= 0)%Z. Theorem F2R_le_0_reg : forall m e : Z, (F2R (Float beta m e) <= 0)%R -> (m <= 0)%Z. Proof. intros f H. intros m e H. apply le_Z2R. apply Ropp_le_cancel. apply Rmult_le_reg_l with (bpow (Fexp f)). apply Rmult_le_reg_r with (bpow e). apply epow_gt_0. simpl (Z2R 0). rewrite Ropp_0. rewrite Rmult_0_r. rewrite Ropp_mult_distr_r_reverse. rewrite Rmult_0_l. rewrite Ropp_mult_distr_l_reverse. rewrite <- Ropp_0. apply Ropp_le_contravar. now rewrite Rmult_comm. now apply Ropp_le_contravar. Qed. Theorem F2R_gt_0_imp_Fnum : Theorem F2R_gt_0_reg : forall m e : Z, (0 < F2R (Float beta m e))%R -> (0 < m)%Z. Proof. intros m e H. apply lt_Z2R. apply Rmult_lt_reg_r with (bpow e). apply epow_gt_0. now rewrite Rmult_0_l. Qed. Theorem F2R_gt_0_compat : forall f : float beta, (0 < F2R f)%R -> (0 < Fnum f)%Z. (0 < Fnum f)%Z -> (0 < F2R f)%R. Proof. intros f Hm. unfold F2R. apply Rmult_lt_0_compat. now apply (Z2R_lt 0). apply epow_gt_0. Qed. Theorem F2R_le_reg : forall e m1 m2 : Z, (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R -> (m1 <= m2)%Z. Proof. intros e m1 m2 H. apply le_Z2R. apply Rmult_le_reg_r with (bpow e). apply epow_gt_0. exact H. Qed. Theorem F2R_le_compat : forall m1 m2 e : Z, (m1 <= m2)%Z -> (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R. Proof. intros m1 m2 e H. unfold F2R. simpl. apply Rmult_le_compat_r. apply epow_ge_0. now apply Z2R_le. Qed. Theorem F2R_lt_reg : forall e m1 m2 : Z, (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R -> (m1 < m2)%Z. Proof. intros f H. intros e m1 m2 H. apply lt_Z2R. apply Rmult_lt_reg_l with (bpow (Fexp f)). apply Rmult_lt_reg_r with (bpow e). apply epow_gt_0. rewrite Rmult_0_r. now rewrite Rmult_comm. exact H. Qed. Theorem F2R_lt_compat : forall e m1 m2 : Z, (m1 < m2)%Z -> (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R. Proof. intros e m1 m2 H. unfold F2R. simpl. apply Rmult_lt_compat_r. apply epow_gt_0. now apply Z2R_lt. Qed. Theorem epow_le_F2R : forall f : float beta, (0 < F2R f)%R -> (bpow (Fexp f) <= F2R f)%R. forall m e : Z, (0 < m)%Z -> (bpow e <= F2R (Float beta m e))%R. Proof. intros f H. rewrite <- (Rmult_1_l (bpow (Fexp f))). intros m e H. rewrite <- (Rmult_1_l (bpow e)). unfold F2R. simpl. apply Rmult_le_compat_r. apply epow_ge_0. apply (Z2R_le 1). apply (Zlt_le_succ 0). now apply F2R_gt_0_imp_Fnum. now apply (Zlt_le_succ 0). Qed. Theorem F2R_p1_le_epow : forall m e1 e2 : Z, (0 < m)%Z -> (F2R (Float beta m e1) < bpow e2)%R -> (F2R (Float beta (m + 1) e1) <= bpow e2)%R. Proof. intros m e1 e2 Hm. intros H. assert (He : (e1 <= e2)%Z). (* . *) apply <- (epow_le beta). apply Rle_trans with (F2R (Float beta m e1)). unfold F2R. simpl. rewrite <- (Rmult_1_l (bpow e1)) at 1. apply Rmult_le_compat_r. apply epow_ge_0. apply (Z2R_le 1). now apply (Zlt_le_succ 0). now apply Rlt_le. (* . *) revert H. replace e2 with (e2 - e1 + e1)%Z by ring. rewrite epow_add. unfold F2R. simpl. rewrite <- (Z2R_Zpower beta (e2 - e1)). intros H. apply Rmult_le_compat_r. apply epow_ge_0. apply Rmult_lt_reg_r in H. apply Z2R_le. apply Zlt_le_succ. now apply lt_Z2R. apply epow_gt_0. now apply Zle_minus_le_0. Qed. Theorem abs_F2R : ... ... @@ -130,4 +222,86 @@ now apply Z2R_lt. exact Hp. Qed. Theorem ln_beta_F2R : forall m e : Z, m <> Z0 -> (projT1 (ln_beta beta (F2R (Float beta m e))) = projT1 (ln_beta beta (Z2R m)) + e)%Z. Proof. intros m e H. destruct (ln_beta beta (Z2R m)) as (d, Hd). simpl. specialize (Hd (Z2R_neq _ _ H)). apply ln_beta_unique. rewrite abs_F2R. unfold F2R. simpl. rewrite Rabs_Z2R in Hd. split. replace (d + e - 1)%Z with (d - 1 + e)%Z by ring. rewrite epow_add. apply Rmult_le_compat_r. apply epow_ge_0. apply Hd. rewrite epow_add. apply Rmult_lt_compat_r. apply epow_gt_0. apply Hd. Qed. Theorem float_distribution_pos : forall m1 e1 m2 e2 : Z, (0 < m1)%Z -> (F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R -> (e2 < e1)%Z /\ (e1 + projT1 (ln_beta beta (Z2R m1)) = e2 + projT1 (ln_beta beta (Z2R m2)))%Z. Proof. intros m1 e1 m2 e2 Hp1 (H12, H21). assert (He: (e2 < e1)%Z). (* . *) apply Znot_ge_lt. intros H0. elim Rlt_not_le with (1 := H21). apply Zge_le in H0. apply (F2R_change_exp e1 m2 e2) in H0. rewrite H0. apply F2R_le_compat. apply Zlt_le_succ. apply (F2R_lt_reg e1). now rewrite <- H0. (* . *) split. exact He. rewrite (Zplus_comm e1), (Zplus_comm e2). assert (Hp2: (0 < m2)%Z). apply (F2R_gt_0_reg m2 e2). apply Rlt_trans with (2 := H12). now apply F2R_gt_0_compat. rewrite <- 2!ln_beta_F2R. destruct (ln_beta beta (F2R (Float beta m1 e1))) as (e1', H1). simpl. apply sym_eq. apply ln_beta_unique. assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R). rewrite <- (Zabs_eq m1), <- abs_F2R. apply H1. apply Rgt_not_eq. apply Rlt_gt. unfold F2R. simpl. apply Rmult_lt_0_compat. now apply (Z2R_lt 0). apply epow_gt_0. now apply Zlt_le_weak. clear H1. rewrite abs_F2R, Zabs_eq. split. apply Rlt_le. apply Rle_lt_trans with (2 := H12). apply H2. apply Rlt_le_trans with (1 := H21). now apply F2R_p1_le_epow. now apply Zlt_le_weak. apply sym_not_eq. now apply Zlt_not_eq. apply sym_not_eq. now apply Zlt_not_eq. Qed. End Float_prop.
 ... ... @@ -556,7 +556,8 @@ apply Rle_trans with (bpow (fexp ex)). now apply -> epow_le. rewrite <- Hg2. rewrite Hg1 in Hg3. apply epow_le_F2R with (1 := Hg3). apply epow_le_F2R. apply F2R_gt_0_reg with (1 := Hg3). apply epow_lt_epow with beta. apply Rlt_le_trans with (bpow ex). apply Rle_lt_trans with (2 := proj2 Hx). ... ... @@ -619,7 +620,8 @@ apply Rlt_not_le with (1 := Hgp). rewrite <- (proj2 (proj2 (prop_exp ex) He) eg). rewrite <- Hg2. rewrite Hg1. apply (epow_le_F2R _ (Float beta gm ge)). apply epow_le_F2R. apply F2R_gt_0_reg with beta ge. rewrite <- Hg1. apply Rlt_le_trans with (2 := Hgx). apply Rlt_le_trans with (2 := proj1 Hx). ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!