proposition: Theorem ExactMinusIntervalAux : forall P, RoundedModeP b radix P -> forall p q : float, (0 < p)%R -> (2 * p < q)%R -> Fcanonic radix b p -> Fcanonic radix b q -> (exists r : float, Fbounded b r /\ r = (q - p)%R :>R) -> forall r : float, Fcanonic radix b r -> (2 * p < r)%R -> (r <= q)%R -> exists r' : float, Fbounded b r' /\ r' = (r - p)%R :>R.
proof: Proof. intros P H' p q H'0 H'1 H'2 H'3 H'4 r H'5 H'6 H'7. cut (0 <= p)%R; [ intros Rle0 | apply Rlt_le; auto ]. cut (0 <= r)%R; [ intros Rle1 | apply Rle_trans with (2 * p)%R; auto ]. 2: apply Rle_trans with (FtoRradix p); auto with zarith. 2: apply Rledouble; auto. 2: apply Rlt_le; auto. generalize H'6; clear H'6; pattern r in |- *; apply (FinductNeg b radix precision) with (p := q); auto with zarith. apply Rle_trans with (FtoRradix r); auto. intros q0 H'6 H'8 H'9 H'10 H'11. elim H'10; [ intros r' E; elim E; intros H'13 H'14; clear E H'10 | clear H'10 ]; auto. 2: apply Rlt_trans with (1 := H'11); auto; apply (FPredLt b radix precision); auto with zarith. cut (0 <= Fnormalize radix b precision r')%R; [ intros Rle2 | idtac ]. 2: rewrite (FnormalizeCorrect radix); auto with arith. 2: unfold FtoRradix in H'14; rewrite H'14. 2: apply Rplus_le_reg_l with (r := FtoR radix p). 2: replace (FtoR radix p + 0)%R with (FtoR radix p); [ idtac | ring ]. 2: replace (FtoR radix p + (FtoR radix q0 - FtoR radix p))%R with (FtoR radix q0); [ idtac | ring ]. 2: apply Rle_trans with (2 * p)%R; auto. 2: apply Rledouble; auto with real zarith. 2: apply Rlt_le; apply Rlt_trans with (1 := H'11); auto. 2: apply (FPredLt b radix precision); auto with zarith. cut (Fnormalize radix b precision r' < q0)%R; [ intros Rle3 | idtac ]. 2: rewrite (FnormalizeCorrect radix); auto with arith. 2: unfold FtoRradix in H'14; rewrite H'14. 2: apply Rplus_lt_reg_l with (r := (- q0)%R). 2: replace (- q0 + (FtoR radix q0 - FtoR radix p))%R with (- p)%R; [ idtac | unfold FtoRradix in |- *; ring; ring ]. 2: replace (- q0 + q0)%R with (-0)%R; [ auto with real | ring ]. case radixRangeBoundExp with (b:=b) (radix:=radix) (precision:=precision) (p := Fnormalize radix b precision r') (q := q0); auto with zarith; fold FtoRradix in |- *. apply FnormalizeCanonic; auto with zarith. rewrite (FnormalizeCorrect radix); auto with arith. apply Rlt_le_trans with (2 * r')%R; auto. rewrite H'14. rewrite Rmult_minus_distr_l. pattern (FtoRradix q0) at 1 in |- *; (replace (FtoRradix q0) with (2 * q0 - q0)%R; [ idtac | simpl in |- *; ring ]). unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_contravar. apply Rlt_trans with (1 := H'11). apply (FPredLt b radix precision); auto with zarith. apply Rmult_le_compat_r; auto with real arith. unfold FtoRradix in Rle2; rewrite (FnormalizeCorrect radix) in Rle2; auto with arith. apply IZR_le; simpl; lia. intros H'10. case (FcanonicLtPos _ radixMoreThanOne b precision) with (p := Fnormalize radix b precision r') (q := q0); auto with zarith. apply FnormalizeCanonic; auto with zarith. intros; contradict H'10; auto with zarith. intros H'12; elim H'12; intros H'15 H'16; clear H'12. exists (Float (Z.pred (Fnum (Fnormalize radix b precision r'))) (Fexp (Fnormalize radix b precision r'))). split. cut (Fbounded b (Fnormalize radix b precision r')); [ intros Fb0 | idtac ]. repeat split; simpl in |- *; auto. case Rle2; intros Z1. apply Z.le_lt_trans with (Z.abs (Fnum (Fnormalize radix b precision r'))); auto with zarith. repeat rewrite Z.abs_eq; auto with zarith. apply (LeR0Fnum radix); auto with zarith. apply Zle_Zpred; apply (LtR0Fnum radix); auto with zarith. apply Fb0. replace (Fnum (Fnormalize radix b precision r')) with 0%Z; simpl in |- *; auto with zarith. apply (vNumbMoreThanOne radix) with (precision := precision); auto with zarith. apply sym_equal; change (is_Fzero (Fnormalize radix b precision r')) in |- *; apply (is_Fzero_rep2 radix); auto with zarith. apply FcanonicBound with (radix := radix); auto. apply FnormalizeCanonic; auto with zarith. apply FnormalizeBounded; auto with zarith. replace (Float (Z.pred (Fnum (Fnormalize radix b precision r'))) (Fexp (Fnormalize radix b precision r'))) with (Fminus radix (Fnormalize radix b precision r') (Fminus radix q0 (FPred b radix precision q0))). repeat rewrite (Fopp_correct radix); repeat rewrite (Fminus_correct radix); auto with arith. rewrite (FnormalizeCorrect radix); auto with arith. unfold FtoRradix in H'14; rewrite H'14. unfold FtoRradix in |- *; ring; ring. replace (FPred b radix precision q0) with (Float (Z.pred (Fnum q0)) (Fexp q0)); auto. unfold Fminus, Fopp, Fplus in |- *; simpl in |- *. repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; simpl in |- *; auto. rewrite H'10. repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; simpl in |- *; auto. repeat rewrite Zmult_1_r. apply floatEq; simpl in |- *; auto; unfold Z.pred in |- *; ring. case (Z.eq_dec (Fnum q0) (nNormMin radix precision)); intros Zeq2. case (Z.eq_dec (Fexp q0) (- dExp b)); intros Zeq1. rewrite Zeq1; rewrite Zeq2; rewrite <- (FPredSimpl3 b radix); auto with zarith; rewrite <- Zeq1; rewrite <- Zeq2; auto. contradict H'16. apply Zle_not_lt. rewrite Zeq2. rewrite <- (Z.abs_eq (Fnum (Fnormalize radix b precision r'))); auto with zarith. apply pNormal_absolu_min with (b := b); auto with zarith. cut (Fcanonic radix b (Fnormalize radix b precision r')); [ intros Ca1; case Ca1; auto | apply FnormalizeCanonic; auto with zarith ]. intros H'12; case Zeq1; rewrite <- H'10. apply H'12. apply (LeR0Fnum radix); auto. rewrite FPredSimpl4; auto. contradict H'16; rewrite H'16. apply Zle_not_lt. unfold pPred in |- *; rewrite Zopp_Zpred_Zs; apply Zlt_le_succ. apply Zlt_Zabs_inv1. cut (Fbounded b (Fnormalize radix b precision r')); [ intros T; apply T | idtac ]. apply FnormalizeBounded; auto with zarith. intros H'10. case (Z.eq_dec (Fnum q0) (nNormMin radix precision)); intros Zeq2. exists (Float (Z.pred (Fnum (Fnormalize radix b precision r'))) (Fexp (Fnormalize radix b precision r'))). cut (Fbounded b (Fnormalize radix b precision r')); [ intros Fb1 | idtac ]. repeat split; simpl in |- *; auto with zarith. case Rle2; intros Z1. apply Z.lt_trans with (Z.abs (Fnum (Fnormalize radix b precision r'))). repeat rewrite Z.abs_eq; auto with zarith. apply (LeR0Fnum radix); auto. apply Zle_Zpred; apply (LtR0Fnum radix); auto. case Fb1; auto. replace (Fnum (Fnormalize radix b precision r')) with 0%Z. simpl in |- *; apply (vNumbMoreThanOne radix) with (precision := precision); auto with zarith. apply sym_equal; change (is_Fzero (Fnormalize radix b precision r')) in |- *; apply (is_Fzero_rep2 radix); auto with zarith. apply Fb1. rewrite FPredSimpl2; auto with zarith. rewrite <- H'10. cut (forall z : Z, Z.pred (Z.succ z) = z); [ intros tmp; rewrite tmp; clear tmp | intros; unfold Z.succ, Z.pred in |- *; ring ]. unfold FtoRradix, FtoR in |- *; simpl in |- *. cut (forall x : Z, Z.pred x = (x - 1)%Z); [ intros tmp; rewrite tmp; clear tmp | intros; unfold Z.pred in |- *; simpl in |- *; ring ]. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite <- Z_R_minus; auto. rewrite (fun x y => Rmult_comm (x - y)); rewrite Rmult_minus_distr_l; repeat rewrite (fun x y => Rmult_comm (powerRZ x y)). replace (Fnum (Fnormalize radix b precision r') * powerRZ radix (Fexp (Fnormalize radix b precision r')))%R with (FtoRradix (Fnormalize radix b precision r')). rewrite (FnormalizeCorrect radix); auto. unfold FtoRradix in H'14; rewrite H'14. unfold FtoR in |- *; simpl in |- *. pattern (Fexp q0) at 1 in |- *; rewrite <- H'10. rewrite Zeq2; rewrite powerRZ_Zs. 2: apply IZR_neq; lia. rewrite <- Rmult_assoc. replace (nNormMin radix precision * radix)%R with (powerRZ radix precision). unfold pPred, nNormMin, Z.pred in |- *; rewrite pGivesBound. rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ; simpl in |- *; try ring. rewrite <- Zpower_nat_Z_powerRZ; auto with zarith; rewrite <- mult_IZR; rewrite Zmult_comm; rewrite <- (PosNormMin radix b precision); auto with real zarith. rewrite pGivesBound; easy. auto. red in |- *; intros H'12; absurd (- dExp b <= Fexp (Fnormalize radix b precision r'))%Z; auto with zarith. apply Fb1. apply FnormalizeBounded; auto with zarith. exists (Float (Fnum (Fnormalize radix b precision r') - radix) (Fexp (Fnormalize radix b precision r'))). cut (Fbounded b (Fnormalize radix b precision r')); [ intros Fb1 | idtac ]. repeat split; simpl in |- *; auto with zarith; try apply Fb1. case (Zle_or_lt (Fnum (Fnormalize radix b precision r')) radix); intros Z1. apply Z.le_lt_trans with radix. rewrite Zabs_eq_opp; auto with zarith. cut (0 <= Fnum (Fnormalize radix b precision r'))%Z; auto with zarith. apply (LeR0Fnum radix); auto. rewrite <- (Zpower_nat_1 radix); rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_lt; lia. apply Z.le_lt_trans with (Z.abs (Fnum (Fnormalize radix b precision r'))). repeat rewrite Z.abs_eq; auto with zarith. case Fb1; auto. rewrite FPredSimpl4; auto with arith. rewrite <- H'10. unfold FtoRradix, FtoR in |- *; simpl in |- *. cut (forall x : Z, Z.pred x = (x - 1)%Z); [ intros tmp; rewrite tmp; clear tmp | intros; unfold Z.pred in |- *; simpl in |- *; ring ]. repeat rewrite <- Z_R_minus; auto. repeat rewrite (fun x y => Rmult_comm (x - y)); repeat rewrite Rmult_minus_distr_l; repeat rewrite (fun x y => Rmult_comm (powerRZ x y)). replace (Fnum (Fnormalize radix b precision r') * powerRZ radix (Fexp (Fnormalize radix b precision r')))%R with (FtoRradix (Fnormalize radix b precision r')). rewrite (FnormalizeCorrect radix); auto. unfold FtoRradix in H'14; rewrite H'14. unfold FtoR in |- *; simpl in |- *. rewrite <- H'10. repeat rewrite powerRZ_Zs. ring. apply IZR_neq; lia. auto with real zarith. unfold FtoR in |- *; simpl in |- *. red in |- *; intros H'12; absurd (0 <= Fnum q0)%Z; auto. apply Zlt_not_le. rewrite H'12. change 0%Z with (- 0)%Z; apply Zlt_Zopp. unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *; auto with zarith. apply (vNumbMoreThanOne radix) with (precision := precision); auto with zarith. apply (LeR0Fnum radix); auto. apply Rlt_le; auto. apply (FcanonicBound radix b); auto with arith. apply FnormalizeCanonic; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz