proposition: Lemma pff_canonic_is_canonic: forall f, Fcanonic beta b f -> FtoR beta f <> 0 -> canonical beta (FLT_exp (- dExp b) p) (Float beta (Pff.Fnum f) (Pff.Fexp f)).
proof: Proof. intros f Hf1 Hf2; unfold canonical; simpl. assert (K:(F2R (Float beta (Pff.Fnum f) (Pff.Fexp f)) = FtoR beta f)). unfold FtoR, F2R; simpl. now rewrite bpow_powerRZ. unfold cexp, FLT_exp. rewrite K. destruct (mag beta (FtoR beta f)) as (e, He). simpl; destruct Hf1. destruct H as (H1,H2). cut (Pff.Fexp f = e-p)%Z. intros V; rewrite V. apply sym_eq; apply Zmax_left. rewrite <- V; destruct H1; auto with zarith. cut (e = Pff.Fexp f + p)%Z. lia. apply trans_eq with (mag beta (FtoR beta f)). apply sym_eq; apply mag_unique. apply He; assumption. apply mag_unique. rewrite <- K; unfold F2R; simpl. rewrite Rabs_mult. rewrite (Rabs_right (bpow beta (Pff.Fexp f))). 2: apply Rle_ge; apply bpow_ge_0. split. replace (Pff.Fexp f + p - 1)%Z with ((p-1)+Pff.Fexp f)%Z by ring. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rmult_le_reg_l with (IZR beta). apply IZR_lt. apply radix_gt_0. rewrite <- bpow_plus_1. replace (p-1+1)%Z with (Z_of_nat (Z.abs_nat p)). rewrite <- IZR_Zpower_nat. simpl; rewrite <- pGivesBound. rewrite Rabs_Zabs. rewrite <- mult_IZR. apply IZR_le. rewrite <- (Z.abs_eq (beta)). rewrite <- Zabs.Zabs_Zmult. assumption. apply Zlt_le_weak; apply radix_gt_0. rewrite inj_abs; try ring. lia. rewrite Zplus_comm, bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. rewrite <- (inj_abs p) by lia. rewrite <- IZR_Zpower_nat. simpl; rewrite <- pGivesBound. rewrite Rabs_Zabs. apply IZR_lt. destruct H1; assumption. destruct H as (H1,(H2,H3)). rewrite H2. apply sym_eq; apply Zmax_right. cut ((e-1) < p-dExp b)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (Rabs (FtoR beta f)). apply He; auto. apply Rlt_le_trans with (FtoR beta (firstNormalPos beta b (Z.abs_nat p))). rewrite <- Fabs_correct. 2: apply radix_gt_0. apply FsubnormalLtFirstNormalPos with (3 := pGivesBound). apply radix_gt_1. lia. apply FsubnormFabs; auto with zarith. apply radix_gt_1. split; [idtac|split]; assumption. rewrite Fabs_correct; auto with real zarith. apply Rabs_pos. apply radix_gt_0. unfold firstNormalPos, FtoR, nNormMin. simpl. replace (IZR (Zpower_nat beta (Peano.pred (Z.abs_nat p)))) with (bpow beta (p-1)). rewrite <- (bpow_powerRZ _). rewrite <- bpow_plus. apply bpow_le. lia. replace (p-1)%Z with (Z_of_nat (Peano.pred (Z.abs_nat p))). rewrite <- IZR_Zpower_nat. reflexivity. rewrite inj_pred; lia. Qed.
imports: Coq(Lia) Pff Core