proposition: Theorem PminPos : forall p min : float, (0 <= p)%R -> Fbounded b p -> isMin b radix (/ 2 * p) min -> exists c : float, Fbounded b c /\ c = (p - min)%R :>R.
proof: Proof. intros p min H' H'0 H'1. cut (min <= / 2 * p)%R; [ intros Rl1; Casec Rl1; intros Rl1 | apply isMin_inv1 with (1 := H'1); auto ]. case (eqExpMax _ radixMoreThanOne b min p); auto. case H'1; auto. rewrite Fabs_correct; auto with arith. rewrite Rabs_right; auto. apply Rle_trans with (/ 2 * p)%R; auto. apply Rlt_le; auto. apply Rmult_le_reg_l with (r := 2); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_ne_r; auto with real. apply Rle_ge; apply RleMinR0 with (r := (/ 2 * p)%R); auto. apply Rmult_le_reg_l with (r := 2); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l; rewrite Rmult_0_r; auto with real. intros min' H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6; clear H'4 H'2. case (FboundNext _ radixMoreThanOne b precision) with (p := min'); auto with zarith; fold FtoRradix in |- *. intros Smin H'2; elim H'2; intros H'4 H'7; clear H'2. exists Smin; split; auto. rewrite H'7; auto. unfold FtoRradix in |- *. rewrite <- H'5; auto. replace (Float (Z.succ (Fnum min')) (Fexp min')) with (Float (Fnum (Fshift radix (Z.abs_nat (Fexp p - Fexp min')) p) - Fnum min') (Fexp min')); auto. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite <- Z_R_minus. rewrite (fun x y z : R => Rmult_comm (x - y) z); rewrite Rmult_minus_distr_l; repeat rewrite (fun x : Z => Rmult_comm (powerRZ radix x)). rewrite mult_IZR. rewrite Zpower_nat_powerRZ_absolu; auto with zarith. rewrite Rmult_assoc. rewrite <- (powerRZ_add radix); try apply IZR_neq; auto with real zarith. replace (Fexp p - Fexp min' + Fexp min')%Z with (Fexp p); [ auto | ring ]. apply floatEq; auto; simpl in |- *. apply Zle_antisym. apply Zlt_succ_le. apply Zplus_lt_reg_l with (p := Fnum min'); auto. cut (forall x y : Z, (x + (y - x))%Z = y); [ intros tmp; rewrite tmp; clear tmp | intros; ring ]. replace (Fnum min' + Z.succ (Z.succ (Fnum min')))%Z with (2 * Z.succ (Fnum min'))%Z. apply (Rlt_Float_Zlt radix) with (r := Fexp min'); auto; fold FtoRradix in |- *. replace (FtoRradix (Float (2 * Z.succ (Fnum min')) (Fexp min'))) with (2 * Float (Z.succ (Fnum min')) (Fexp min'))%R. rewrite <- H'7. replace (Float (Fnum p * Zpower_nat radix (Z.abs_nat (Fexp p - Fexp min'))) (Fexp min')) with (Fshift radix (Z.abs_nat (Fexp p - Fexp min')) p). unfold FtoRradix in |- *; rewrite FshiftCorrect; auto. apply Rmult_lt_reg_l with (r := (/ 2)%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; rewrite Rmult_1_l; auto with real. case (Rle_or_lt Smin (/ 2 * FtoR radix p)); auto. intros H'2; absurd (min < Smin)%R. apply Rle_not_lt. case H'1; auto. intros H'8 H'9; elim H'9; intros H'10 H'11; apply H'11; clear H'9; auto. rewrite H'7; unfold FtoRradix in |- *; rewrite <- H'5; auto. unfold FtoR in |- *; simpl in |- *; apply Rlt_monotony_exp; auto with real zarith. apply IZR_lt; lia. unfold Fshift in |- *; simpl in |- *. replace (Fexp p - Z.abs_nat (Fexp p - Fexp min'))%Z with (Fexp min'); auto. rewrite inj_abs; auto. ring. auto with zarith. replace (FtoRradix (Float (2 * Z.succ (Fnum min')) (Fexp min'))) with ((2 * Z.succ (Fnum min'))%Z * powerRZ radix (Fexp min'))%R. rewrite mult_IZR; auto. unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. simpl in |- *; auto. replace (Z_of_nat 2) with (Z.succ (Z.succ 0)). repeat rewrite <- Zmult_succ_l_reverse; unfold Z.succ in |- *; ring. simpl in |- *; auto. apply Zlt_le_succ; auto. apply Zplus_lt_reg_l with (p := Fnum min'); auto. cut (forall x y : Z, (x + (y - x))%Z = y); [ intros tmp; rewrite tmp; clear tmp | intros; ring ]. replace (Fnum min' + Fnum min')%Z with (2 * Fnum min')%Z. apply (Rlt_Float_Zlt radix) with (r := Fexp min'); auto; fold FtoRradix in |- *. replace (FtoRradix (Float (2 * Fnum min') (Fexp min'))) with (2 * Float (Fnum min') (Fexp min'))%R. replace (Float (Fnum p * Zpower_nat radix (Z.abs_nat (Fexp p - Fexp min'))) (Fexp min')) with (Fshift radix (Z.abs_nat (Fexp p - Fexp min')) p). unfold FtoRradix in |- *; rewrite FshiftCorrect; auto. apply Rmult_lt_reg_l with (r := (/ 2)%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; rewrite Rmult_1_l; auto with real. replace (FtoR radix (Float (Fnum min') (Fexp min'))) with (FtoR radix min); auto. unfold Fshift in |- *; simpl in |- *. replace (Fexp p - Z.abs_nat (Fexp p - Fexp min'))%Z with (Fexp min'); auto. rewrite inj_abs; auto. ring. auto with zarith. replace (FtoRradix (Float (2 * Fnum min') (Fexp min'))) with ((2 * Fnum min')%Z * powerRZ radix (Fexp min'))%R. rewrite mult_IZR; auto. unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. simpl in |- *; auto. ring. exists min; split; auto. case H'1; auto. rewrite Rl1. field. Qed.
imports: Reals ZArith List PeanoNat Psatz