proposition: Theorem Axpy_aux1 : Fcanonic radix b u -> (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) <= / 4 * Fulp b radix precision (FPred b radix precision u))%R -> (0 < u)%R -> (4 * Rabs t <= Rabs u)%R -> (Rabs (y1 - y) + Rabs (a1 * x1 - a * x) < / 4 * Fulp b radix precision (FPred b radix precision u))%R -> MinOrMax radix b (a1 * x1 + y1) u.
proof: Proof. intros H Hblop H1 H2 H3. cut (Rabs (a1 * x1 + y1 - u) < / 2 * Fulp b radix precision (FPred b radix precision u) + Rabs (t + y - u))%R; [ intros H4 | idtac ]. case (Rle_or_lt (t + y) u); intros H5. apply MinOrMax1 with precision; auto with zarith arith. apply Rlt_le_trans with (1 := H4). apply Rplus_le_reg_l with (- (/ 2 * Fulp b radix precision (FPred b radix precision u)))%R. ring_simplify (- (/ 2 * Fulp b radix precision (FPred b radix precision u)) + (/ 2 * Fulp b radix precision (FPred b radix precision u) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u)))%R. apply Rle_trans with (/ 2 * Fulp b radix precision (FPred b radix precision u))%R; [ idtac | right ]. generalize uDef; unfold Closest in |- *; intros H6; elim H6; intros H7 H8; clear H6 H7. case (Rle_or_lt (Rabs (FtoRradix t + FtoRradix y - FtoRradix u)) (/ 2 * Fulp b radix precision (FPred b radix precision u))); auto; intros H6. cut (Rabs (FtoR radix u - (FtoRradix t + FtoRradix y)) <= Rabs (FtoR radix (FPred b radix precision u) - (FtoRradix t + FtoRradix y)))%R; [ intros H7 | apply H8 ]. 2: apply FBoundedPred; auto with zarith arith. contradict H7; apply Rlt_not_le. apply Rlt_le_trans with (Rabs (FtoRradix t + FtoRradix y - FtoRradix u)). 2: right; rewrite <- Rabs_Ropp. 2: replace (- (FtoRradix t + FtoRradix y - FtoRradix u))%R with (FtoR radix u - (FtoRradix t + FtoRradix y))%R; auto with real; ring. apply Rle_lt_trans with (2 := H6). rewrite Rabs_left1. apply Rplus_le_reg_l with (u - (FtoRradix t + FtoRradix y) - / 2 * Fulp b radix precision (FPred b radix precision u))%R. ring_simplify. fold FtoRradix in |- *; pattern (FtoRradix u) at 1 in |- *; replace (FtoRradix u) with (FtoRradix (FPred b radix precision u) + Fulp b radix precision (FPred b radix precision u))%R; [ idtac | unfold FtoRradix in |- *; apply FpredUlpPos; auto with zarith arith ]. apply Rle_trans with (Fulp b radix precision (FPred b radix precision u) - Fulp b radix precision (FPred b radix precision u) * / 2)%R; [ right; ring | idtac ]. apply Rle_trans with (/ 2 * Fulp b radix precision (FPred b radix precision u))%R. right; apply trans_eq with ((1 - / 2) * Fulp b radix precision (FPred b radix precision u))%R; [ ring | auto with real arith ]. field. apply Rlt_le; apply Rlt_le_trans with (1 := H6). rewrite Rabs_left1; [ right; ring | idtac ]. apply Rplus_le_reg_l with (FtoRradix u). ring_simplify; auto. fold FtoRradix in |- *; apply Rplus_le_reg_l with (Fulp b radix precision (FPred b radix precision u)). apply Rle_trans with (FtoRradix (FPred b radix precision u) + Fulp b radix precision (FPred b radix precision u) + - (FtoRradix t + FtoRradix y))%R; [ right; ring | unfold FtoRradix in |- *; rewrite FpredUlpPos; auto with zarith arith ]. ring_simplify (Fulp b radix precision (FPred b radix precision u) + 0)%R. apply Rle_trans with (Rabs (FtoRradix u + - (FtoRradix t + FtoRradix y))). apply RRle_abs. rewrite <- Rabs_Ropp. replace (- (FtoRradix u + - (FtoRradix t + FtoRradix y)))%R with (FtoRradix t + FtoRradix y - u)%R; [ idtac | ring ]. apply Rmult_le_reg_l with 2%R; auto with arith real. apply Rle_trans with (Fulp b radix precision u). unfold FtoRradix in |- *; apply ClosestUlp; auto with arith zarith. change 2%R with (IZR radix). apply FulpFPredLe; auto with zarith. apply trans_eq with ((1 - / 2) * Fulp b radix precision (FPred b radix precision u))%R; [ idtac | ring ]. field. case (Rle_or_lt (t + y) (u + / 2 * Fulp b radix precision (FPred b radix precision u))); intros H6. apply MinOrMax1 with precision; auto with arith zarith real. apply Rlt_le_trans with (1 := H4); rewrite Rabs_right. apply Rplus_le_reg_l with (u + - (/ 2 * Fulp b radix precision (FPred b radix precision u)))%R. ring_simplify. apply Rle_trans with (1 := H6). apply Rle_trans with (FtoRradix u + (Fulp b radix precision (FPred b radix precision u) + - (Fulp b radix precision (FPred b radix precision u) * / 2)))%R; [ apply Rplus_le_compat_l; right | right; ring ]. apply trans_eq with ((1 - / 2) * Fulp b radix precision (FPred b radix precision u))%R; [ idtac | ring ]. field. apply Rle_ge; apply Rplus_le_reg_l with (FtoRradix u); auto with real. ring_simplify; auto with real. apply MinOrMax2 with precision; auto with arith zarith real. apply Rlt_le_trans with (1 := H4). apply Rle_trans with (/ 2 * Fulp b radix precision u + Rabs (FtoRradix t + FtoRradix y - FtoRradix u))%R; [ apply Rplus_le_compat_r | idtac ]. apply Rmult_le_compat_l; auto with real arith. apply FulpFPredGePos; auto with arith zarith. apply Rle_trans with (/ 2 * Fulp b radix precision u + / 2 * Fulp b radix precision u)%R; [ apply Rplus_le_compat_l | right ]. apply Rmult_le_reg_l with 2%R; auto with real arith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith. ring_simplify (1 * Fulp b radix precision u)%R. unfold FtoRradix in |- *; apply ClosestUlp; auto with real arith zarith. field. cut (forall z z' : R, (Rabs z <= z')%R -> (- z' <= z)%R); [ intros V | idtac ]. replace (a1 * x1 + y1)%R with (a1 * x1 - a * x + (y1 - y) + (a * x - t + (t + y)))%R; [ fold FtoRradix in |- * | ring ]. replace (FtoRradix u) with (- (/ 4 * Fulp b radix precision (FPred b radix precision u)) + (- (/ 4 * Fulp b radix precision (FPred b radix precision u)) + (FtoRradix u + / 2 * Fulp b radix precision (FPred b radix precision u))))%R. apply Rplus_le_compat. apply V; auto with real. apply Rle_trans with (Rabs (y1 - FtoRradix y) + Rabs (a1 * x1 - FtoRradix a * FtoRradix x))%R; auto with real. rewrite Rplus_comm; apply Rabs_triang. apply Rplus_le_compat. apply V; auto with real. auto with real. apply trans_eq with (FtoRradix u + (- / 4 + (- / 4 + / 2)) * Fulp b radix precision (FPred b radix precision u))%R; [ ring | idtac ]. field. intros z z'; case (Rle_or_lt 0 z); intros P1 P2. apply Rle_trans with (-0)%R; [ apply Ropp_le_contravar | simpl in |- * ]; auto with real. apply Rle_trans with (Rabs z); try apply Rabs_pos; easy. now rewrite Ropp_0. apply Ropp_le_cancel; rewrite Ropp_involutive; rewrite <- Rabs_left; auto with real. replace (a1 * x1 + y1 - FtoRradix u)%R with (y1 - y + (a1 * x1 - a * x) + (a * x - t + (t + y - u)))%R; [ idtac | ring ]. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y + (a1 * x1 - FtoRradix a * FtoRradix x)) + Rabs (FtoRradix a * FtoRradix x - FtoRradix t + (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rabs_triang | idtac ]. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y + (a1 * x1 - FtoRradix a * FtoRradix x)) + (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rplus_le_compat_l; apply Rabs_triang | idtac ]. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y) + Rabs (a1 * x1 - FtoRradix a * FtoRradix x) + (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u)))%R. apply Rplus_le_compat_r; apply Rabs_triang. apply Rlt_le_trans with (/ 4 * Fulp b radix precision (FPred b radix precision u) + (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u)))%R; auto with real. apply Rle_trans with (/ 4 * Fulp b radix precision (FPred b radix precision u) + (/ 4 * Fulp b radix precision (FPred b radix precision u) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u)))%R; auto with real. lra. Qed.
imports: Reals ZArith List PeanoNat Psatz