proposition: Theorem plusExact2Aux : forall p q r : float, (0 <= p)%R -> Fcanonic radix b p -> Fbounded b q -> Closest b radix (p + q) r -> (Fexp r < Z.pred (Fexp p))%Z -> r = (p + q)%R :>R.
proof: Proof. intros p q r H' H'0 H'1 H'2 H'3. apply plusExact1; auto. apply FcanonicBound with (1 := H'0); auto. case (Zle_or_lt (Fexp p) (Fexp q)); intros Zl1. rewrite Z.min_l; auto with zarith. apply Z.le_trans with (Z.pred (Fexp p)); auto with zarith. unfold Z.pred in |- *; auto with zarith. rewrite Z.min_r; auto with zarith. case (Zlt_next _ _ Zl1); intros Zl2. rewrite Zl2 in H'3. replace (Fexp q) with (Z.pred (Z.succ (Fexp q))); auto with zarith; unfold Z.pred, Z.succ in |- *; ring. case H'0; clear H'0; intros H'0. absurd (r < Float (nNormMin radix precision) (Z.pred (Fexp p)))%R. apply Rle_not_lt; auto. unfold FtoRradix in |- *; apply (ClosestMonotone b radix (Float (nNormMin radix precision) (Z.pred (Fexp p))) ( p + q)%R); auto; auto. cut (Float (nNormMin radix precision) (Fexp p) <= p)%R; [ intros Eq1 | idtac ]. case (Rle_or_lt 0 q); intros Rl1. apply Rlt_le_trans with (FtoRradix p). apply Rlt_le_trans with (FtoRradix (Float (nNormMin radix precision) (Fexp p))); auto. unfold FtoRradix, FtoR in |- *; simpl in |- *; auto. apply Rmult_lt_compat_l; auto with real arith. apply IZR_lt; apply nNormPos; auto with zarith. apply Rlt_powerRZ; try apply IZR_lt; lia. pattern (FtoRradix p) at 1 in |- *; replace (FtoRradix p) with (p + 0)%R; auto with real. apply Rplus_lt_reg_l with (r := (- q)%R); auto. replace (- q + (p + q))%R with (FtoRradix p); [ idtac | ring ]. apply Rlt_le_trans with (FtoRradix (Float (nNormMin radix precision) (Fexp p))); auto. apply Rlt_le_trans with (2 * Float (nNormMin radix precision) (Z.pred (Fexp p)))%R; auto. cut (forall r : R, (2 * r)%R = (r + r)%R); [ intros tmp; rewrite tmp; clear tmp | intros; simpl in |- *; ring ]. rewrite (Rplus_comm (- q)). apply Rplus_lt_compat_l. rewrite <- Rabs_left1; auto. rewrite <- (Fabs_correct radix); auto with arith. unfold FtoRradix in |- *; apply maxMaxBis with (b := b); auto with zarith. apply Rlt_le; auto. apply Rle_trans with (radix * Float (nNormMin radix precision) (Z.pred (Fexp p)))%R. apply Rmult_le_compat_r; auto. apply (LeFnumZERO radix); simpl in |- *; auto with arith. apply Zlt_le_weak; apply nNormPos; auto with zarith. apply IZR_le; simpl in |- *; cut (1 < radix)%Z; auto with real zarith. pattern (Fexp p) at 2 in |- *; replace (Fexp p) with (Z.succ (Z.pred (Fexp p))); [ idtac | unfold Z.succ, Z.pred in |- *; ring ]. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite powerRZ_Zs; auto with real zarith. repeat rewrite <- Rmult_assoc. rewrite (Rmult_comm radix); auto with real. apply IZR_neq; lia. unfold FtoRradix, FtoR in |- *; simpl in |- *; auto. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply IZR_le. rewrite <- (Z.abs_eq (Fnum p)); auto with zarith. apply pNormal_absolu_min with (b := b); auto with zarith. apply (LeR0Fnum radix); auto with arith. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. repeat split; simpl in |- *. rewrite Z.abs_eq; auto with zarith. apply ZltNormMinVnum; auto with zarith. apply Zlt_le_weak; apply nNormPos; auto with zarith. apply Z.le_trans with (Fexp q); auto with zarith; apply H'1. case (Rle_or_lt 0 r); intros Rl1. rewrite <- (Rabs_right r); auto with real. rewrite <- (Fabs_correct radix); auto with arith. unfold FtoRradix in |- *; apply maxMaxBis with (b := b); auto with zarith. apply RoundedModeBounded with (radix := radix) (P := Closest b radix) (r := (p + q)%R); auto. apply ClosestRoundedModeP with (precision := precision); auto with real. apply Rlt_le_trans with 0%R; auto. apply (LeFnumZERO radix); simpl in |- *; auto with arith. apply Zlt_le_weak; apply nNormPos; auto with zarith. absurd (- dExp b <= Fexp q)%Z; try apply H'1. apply Zlt_not_le. case H'0; intros Z1 (Z2, Z3); rewrite <- Z2; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz