From 29e086f94af4db8ee89dd87cd4ea03e0d4687ac6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 2 Nov 2009 20:14:37 +0000 Subject: [PATCH] Simplified proofs. --- src/Flocq_float_prop.v | 12 +++-------- src/Flocq_rnd_FLX.v | 8 +++---- src/Flocq_rnd_generic.v | 46 ++++++++++++++--------------------------- src/Flocq_ulp.v | 12 ++++------- 4 files changed, 25 insertions(+), 53 deletions(-) diff --git a/src/Flocq_float_prop.v b/src/Flocq_float_prop.v index 40168b1..44aa284 100644 --- a/src/Flocq_float_prop.v +++ b/src/Flocq_float_prop.v @@ -159,11 +159,8 @@ Theorem bpow_le_F2R : (bpow e <= F2R (Float beta m e))%R. Proof. intros m e H. -rewrite <- (Rmult_1_l (bpow e)). -unfold F2R. simpl. -apply Rmult_le_compat_r. -apply bpow_ge_0. -apply (Z2R_le 1). +rewrite <- F2R_bpow. +apply F2R_le_compat. now apply (Zlt_le_succ 0). Qed. @@ -328,10 +325,7 @@ 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 bpow_gt_0. +now apply F2R_gt_0_compat. now apply Zlt_le_weak. clear H1. rewrite abs_F2R, Zabs_eq. diff --git a/src/Flocq_rnd_FLX.v b/src/Flocq_rnd_FLX.v index b6afeea..f649d89 100644 --- a/src/Flocq_rnd_FLX.v +++ b/src/Flocq_rnd_FLX.v @@ -94,8 +94,7 @@ split ; intros H ; rewrite Hx. apply generic_format_0. exists (Float beta 0 0). split. -unfold F2R. simpl. -now rewrite Rmult_0_l. +now rewrite F2R_0. apply Zpower_gt_0. now apply Zlt_le_trans with (2 := radix_prop beta). now apply Zlt_le_weak. @@ -144,12 +143,11 @@ destruct (Z_eq_dec xm 0) as [H3|H3]. exists (Float beta 0 0). split. rewrite H1, H3. -unfold F2R. simpl. -now rewrite 2!Rmult_0_l. +now rewrite 2!F2R_0. intros H. elim H. rewrite H1, H3. -apply Rmult_0_l. +apply F2R_0. destruct (ln_beta beta (Z2R xm)) as (d,H4). specialize (H4 (Z2R_neq _ _ H3)). assert (H5: (0 <= prec - d)%Z). diff --git a/src/Flocq_rnd_generic.v b/src/Flocq_rnd_generic.v index 3c74333..3e3d0e9 100644 --- a/src/Flocq_rnd_generic.v +++ b/src/Flocq_rnd_generic.v @@ -28,6 +28,13 @@ Definition generic_format (x : R) := exists f : float beta, canonic x f. +Theorem generic_format_0 : + generic_format 0. +Proof. +exists (Float beta 0 _) ; repeat split. +now rewrite F2R_0. +Qed. + Theorem generic_DN_pt_large_pos_ge_pow : forall x ex, (fexp ex < ex)%Z -> @@ -109,10 +116,7 @@ rewrite ln_beta_unique with (1 := H) in Hg2. simpl in Hg2. apply Rlt_not_le with (1 := Hrg). rewrite Hg1, Hg2. -unfold F2R. simpl. -apply Rmult_le_compat_r. -apply bpow_ge_0. -apply Z2R_le. +apply F2R_le_compat. apply Zfloor_lub. apply Rmult_le_reg_r with (bpow (fexp ex)). apply bpow_gt_0. @@ -127,12 +131,9 @@ now rewrite <- Hg1. (* - positive too small *) replace (Zfloor (x * bpow (- fexp ex))) with Z0. (* - . rounded *) -unfold F2R. simpl. -rewrite Rmult_0_l. +rewrite F2R_0. split. -exists (Float beta Z0 _) ; repeat split. -unfold F2R. simpl. -now rewrite Rmult_0_l. +exact generic_format_0. split. apply Rle_trans with (2 := Hx1). apply bpow_ge_0. @@ -158,18 +159,11 @@ apply Rle_lt_trans with (2 := Hx2). apply Rle_trans with (2 := Hgx). exact (proj1 Hg4). rewrite Hg1. -unfold F2R. simpl. -pattern (bpow ge) at 1 ; rewrite <- Rmult_1_l. -apply Rmult_le_compat_r. -apply bpow_ge_0. -apply (Z2R_le 1). +rewrite <- F2R_bpow. +apply F2R_le_compat. apply (Zlt_le_succ 0). -apply lt_Z2R. -apply Rmult_lt_reg_r with (bpow ge). -apply bpow_gt_0. -rewrite Rmult_0_l. -unfold F2R in Hg1. simpl in Hg1. -now rewrite <- Hg1. +apply F2R_lt_reg with beta ge. +now rewrite F2R_0, <- Hg1. now apply Rlt_le. (* - . . *) apply sym_eq. @@ -433,14 +427,6 @@ apply bpow_gt_0. exact Hx. Qed. -Theorem generic_format_0 : - generic_format 0. -Proof. -exists (Float beta 0 _) ; repeat split. -unfold F2R. simpl. -now rewrite Rmult_0_l. -Qed. - Theorem canonic_unicity : forall x f1 f2, canonic x f1 -> @@ -532,9 +518,7 @@ Theorem generic_DN_pt_small_pos : Proof. intros x ex Hx He. split. -exists (Float beta 0 _) ; repeat split. -unfold F2R. simpl. -now rewrite Rmult_0_l. +exact generic_format_0. split. apply Rle_trans with (2 := proj1 Hx). apply bpow_ge_0. diff --git a/src/Flocq_ulp.v b/src/Flocq_ulp.v index 639bb4f..2a8f920 100644 --- a/src/Flocq_ulp.v +++ b/src/Flocq_ulp.v @@ -219,13 +219,11 @@ rewrite Rnd_N_pt_idempotent with (1 := Hxr). unfold Rminus. rewrite Rplus_opp_r. rewrite Rabs_R0. -unfold ulp, F2R. simpl. -rewrite Rmult_1_l. apply Rmult_le_pos. apply Rlt_le. apply Rinv_0_lt_compat. now apply (Z2R_lt 0 2). -apply bpow_ge_0. +now apply F2R_ge_0_compat. apply Hd. Qed. @@ -237,8 +235,7 @@ Theorem ulp_monotone : Proof. intros Hm x y Hx Hxy. unfold ulp. -unfold F2R. simpl. -rewrite 2!Rmult_1_l. +rewrite 2!F2R_bpow. apply -> bpow_le. apply Hm. now apply ln_beta_monotone. @@ -249,14 +246,13 @@ Theorem ulp_bpow : intros e. unfold ulp. rewrite (ln_beta_unique beta (bpow e) (e + 1)). -unfold F2R. -now rewrite Rmult_1_l. +apply F2R_bpow. rewrite Rabs_pos_eq. split. apply -> bpow_le. omega. apply -> bpow_lt. -omega. +apply Zlt_succ. apply bpow_ge_0. Qed. -- GitLab