proposition: Theorem FTZ_format_generic : forall x, generic_format beta FTZ_exp x -> FTZ_format x.
proof: Proof. intros x Hx. destruct (Req_dec x 0) as [->|Hx3]. exists (Float beta 0 emin). apply sym_eq, F2R_0. intros H. now elim H. apply Z.le_refl. unfold generic_format, scaled_mantissa, cexp, FTZ_exp in Hx. destruct (mag beta x) as (ex, Hx4). simpl in Hx. specialize (Hx4 Hx3). generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx. case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2. elim Rlt_not_ge with (1 := proj2 Hx4). apply Rle_ge. rewrite Hx2, <- F2R_Zabs. rewrite <- (Rmult_1_l (bpow ex)). unfold F2R. simpl. apply Rmult_le_compat. now apply IZR_le. apply bpow_ge_0. apply IZR_le. apply (Zlt_le_succ 0). apply lt_IZR. apply Rmult_lt_reg_r with (bpow (emin + prec - 1)). apply bpow_gt_0. rewrite Rmult_0_l. change (0 < F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R. rewrite F2R_Zabs, <- Hx2. now apply Rabs_pos_lt. apply bpow_le. lia. rewrite Hx2. eexists ; repeat split ; simpl. apply le_IZR. rewrite IZR_Zpower. apply Rmult_le_reg_r with (bpow (ex - prec)). apply bpow_gt_0. rewrite <- bpow_plus. replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring. change (bpow (ex - 1) <= F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R. rewrite F2R_Zabs, <- Hx2. apply Hx4. apply Zle_minus_le_0. now apply (Zlt_le_succ 0). apply lt_IZR. rewrite IZR_Zpower. apply Rmult_lt_reg_r with (bpow (ex - prec)). apply bpow_gt_0. rewrite <- bpow_plus. replace (prec + (ex - prec))%Z with ex by ring. change (F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R. rewrite F2R_Zabs, <- Hx2. apply Hx4. now apply Zlt_le_weak. now apply Z.ge_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX