Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* This file was originally generated by why. It can be modified; only the generated parts will be overwritten. *) Require Export Why2Gappa. Require Export WhyFloatsStrictLegacy. Local Coercion FtoRradix: Float.float >-> R. (*Why type*) Definition int32: Set. Admitted. (*Why logic*) Definition integer_of_int32 : int32 -> Z. Admitted. (*Why logic*) Definition mkp : double -> double -> Z -> Prop. exact (fun (uc up:double) (N:Z) => (exists eps: nat -> R, (forall i:nat, (i<= N)%Z -> (Rabs (eps i) <= powerRZ radix (-53))%R) /\ (double_value up-double_exact up = sum_f_R0 (fun i:nat => (N-i)*(eps i)) (minus (Zabs_nat N) 1))%R /\ (double_value uc-double_exact uc = sum_f_R0 (fun i:nat => (N+1-i)*(eps i)) (Zabs_nat N))%R)). Defined. Lemma Le2errLe: forall (r:R), forall (f:float), (EvenClosest bdouble radix 53 r f) -> (Rabs r <= 15/8)%R -> (Rabs (r-FtoRradix f) <= powerRZ radix (-53))%R. intros. apply Rmult_le_reg_l with (INR 2); auto with real zarith. apply Rle_trans with (Fulp bdouble radix 53 f). unfold FtoRradix; apply ClosestUlp; try apply pdGivesBound; auto with zarith. elim H; trivial. replace (INR 2) with (powerRZ radix 1); [rewrite <- powerRZ_add; auto with real zarith| simpl; ring]. unfold Fulp; apply Rle_powerRZ. simpl; auto with real. apply Zle_trans with (Fexp (Float (15*Zpower_nat radix 49) (-52))); [idtac|simpl; auto with zarith]. apply Fcanonic_Rle_Zle with radix bdouble 53%nat; try apply pdGivesBound; auto with zarith. apply FnormalizeCanonic; try apply pdGivesBound; auto with zarith. elim H; intros (N1,N2) N3; auto. left; split; try split. rewrite pdGivesBound; apply Zle_lt_trans with (15 * Zpower_nat radix 49)%Z; auto with zarith. simpl; auto with zarith. rewrite pdGivesBound; apply Zle_trans with (2*(15 * Zpower_nat radix 49))%Z; auto with zarith. rewrite FnormalizeCorrect; try apply pdGivesBound; auto with zarith. rewrite <- Fabs_correct with radix (Float (15 * Zpower_nat radix 49) (-52));auto with zarith. apply RoundAbsMonotoner with bdouble 53%nat (EvenClosest bdouble radix 53) r; try apply pdGivesBound; auto with zarith. apply absFBounded; auto; split. rewrite pdGivesBound; apply Zle_lt_trans with (15 * Zpower_nat radix 49)%Z; auto with zarith. simpl; auto with zarith. apply Rle_trans with (1:=H0). right; unfold FtoR, Fabs. apply trans_eq with (Zabs (15 * Zpower_nat radix 49)* powerRZ radix (-52))%R; auto. rewrite Zabs_eq; auto with zarith. rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite Rmult_assoc. rewrite <- powerRZ_add; auto with real zarith. replace (49%nat +-52)%Z with (-3)%Z;simpl;[field|reflexivity]. Qed. Lemma mkp_rnd_error: forall (uc up: double), forall N:Z, (0 <= N)%Z -> (mkp uc up N) -> ((double_round_error uc) <= (N+1)*(N+2)*/2*powerRZ radix (-53))%R. unfold mkp; intros uc up N T (eps, (H1,(H2,H3))). unfold double_round_error. rewrite H3. apply Rle_trans with (1:=Rsum_abs (fun i : nat => ((N + 1 - i) * eps i)%R) (Zabs_nat N)). assert (Y:(N =Z_of_nat (Zabs_nat N))); auto with zarith. rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith. apply Rle_trans with (sum_f_R0 (fun l : nat => (Rabs ((N + 1 - l) * powerRZ radix (-53)))) (Zabs_nat N)). apply sum_Rle. intros n H; repeat rewrite Rabs_mult. apply Rmult_le_compat_l; auto with real. rewrite (Rabs_right (powerRZ radix (-53))); try apply Rle_ge; auto with real zarith. apply Rle_trans with (sum_f_R0 (fun l : nat => (((N + 1 - l) * powerRZ radix (-53))%R)) (Zabs_nat N)). apply sum_Rle. intros n H. repeat rewrite Rabs_right; auto with real. apply Rle_ge; apply Rmult_le_pos; auto with real zarith. assert (0 <= N+1-n)%Z; auto with real zarith. apply Rle_trans with (IZR (N+1-n)); auto with real zarith. unfold Zminus, Rminus; right; repeat rewrite plus_IZR; rewrite Ropp_Ropp_IZR. simpl; rewrite <- INR_IZR_INZ; auto. cut (forall n:nat, forall A:R, (sum_f_R0 (fun l : nat => (n + 1 - l) * A) n = (n + 1) * (n + 2) * / 2 * A)%R). intros P; right; pattern N at 1 3 4; rewrite Y. repeat rewrite <- INR_IZR_INZ;apply P. clear H1 H2 H3 Y. induction n; intros A. apply trans_eq with A;[simpl;ring|idtac]. rewrite 2!Rplus_0_l, Rmult_1_l, Rinv_r. now rewrite Rmult_1_l. auto with real. rewrite tech5. replace ((S n + 1 - S n) * A)%R with A;[idtac|ring]. rewrite Rplus_comm. apply trans_eq with (A+sum_f_R0 (fun l : nat => ((n + 1 - l) * A+ A)%R) n)%R. apply Rplus_eq_compat_l. apply sum_eq; intros. replace (INR (S n)) with (n+1)%R;[ring|auto with real zarith]. simpl; case n; auto with real zarith. apply trans_eq with (A+(sum_f_R0 (fun l : nat => ((n + 1 - l) * A)) n +sum_f_R0 (fun l : nat => A) n))%R. apply Rplus_eq_compat_l. rewrite <- sum_plus; auto with real. rewrite IHn. rewrite sum_cte. replace (INR (S n)) with (n+1)%R;[field;auto with real zarith|idtac]. simpl; case n; auto with real zarith. Qed. Lemma mkp_rnd_error2: forall (uc up: double), forall N:Z, (0 <= N)%Z -> (mkp uc up N) -> ((double_round_error up) <= N*(N+1)*/2*powerRZ radix (-53))%R. unfold mkp; intros uc up N T (eps, (H1,(H2,H3))). unfold double_round_error; rewrite H2. apply Rle_trans with (1:=Rsum_abs (fun i : nat => ((N - i) * eps i)%R) (Zabs_nat N-1)). assert (Y:(N =Z_of_nat (Zabs_nat N))); auto with zarith. rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith. apply Rle_trans with (sum_f_R0 (fun l : nat => (Rabs ((N - l) * powerRZ radix (-53)))) (Zabs_nat N-1)). apply sum_Rle. intros n H; repeat rewrite Rabs_mult. apply Rmult_le_compat_l; auto with real. rewrite (Rabs_right (powerRZ radix (-53))); try apply Rle_ge; auto with real zarith. apply Rle_trans with (sum_f_R0 (fun l : nat => (((N - l) * powerRZ radix (-53))%R)) (Zabs_nat N-1)). apply sum_Rle. intros n H. repeat rewrite Rabs_right; auto with real. apply Rle_ge; apply Rmult_le_pos; auto with real zarith. assert (0 <= N-n)%Z; auto with real zarith. apply Rle_trans with (IZR (N-n)); auto with real zarith. unfold Zminus, Rminus; right; repeat rewrite plus_IZR; rewrite Ropp_Ropp_IZR. simpl; rewrite <- INR_IZR_INZ; auto. cut (forall n:nat, forall A:R, (sum_f_R0 (fun l : nat => (n - l) * A) (n-1) = n * (n + 1) * / 2 * A)%R). intros P; right; pattern N at 1 3 4; rewrite Y. repeat rewrite <- INR_IZR_INZ;apply P. clear H1 H2 H3 Y. induction n; intros A. simpl; ring. clear IHn; induction n. simpl; field; auto with real. replace (S (S n) - 1)%nat with (S (S n -1)); auto with zarith. rewrite tech5. replace ((S (S n) - S (S n-1)) * A)%R with A. rewrite Rplus_comm. apply trans_eq with (A+sum_f_R0 (fun l : nat => ((S n - l) * A+ A)%R) n)%R. apply Rplus_eq_compat_l. replace (S n - 1)%nat with n; auto with zarith. apply sum_eq; intros. replace (INR (S (S n))) with (S n+1)%R;[ring|auto with real zarith]. apply trans_eq with (A+(sum_f_R0 (fun l : nat => ((S n - l) * A)) n +sum_f_R0 (fun l : nat => A) n))%R. apply Rplus_eq_compat_l. rewrite <- sum_plus; auto with real. pattern n at 2; replace n with (S n - 1)%nat; auto with zarith. rewrite IHn. rewrite sum_cte. replace (INR (S (S n))) with (S n+1)%R;[field;auto with real zarith|idtac]. apply trans_eq with (INR (S n +1)); auto with real zarith. rewrite plus_INR; simpl; auto with real. replace (INR (S (S n - 1))) with (S (S n) -1)%R; auto with real; [ring|idtac]. apply trans_eq with (INR ((S n -1)+1)); auto with zarith real. apply trans_eq with (INR ((S n +1)-1)); auto with zarith real. replace (S (S n)) with (S n+1)%nat; auto with real zarith. rewrite minus_INR; auto with real zarith. Qed. Lemma mkp_le_1: forall (uc up: double), forall N:Z, (0 <= N)%Z ->(IZR N <= Rpower (2)%R (26)%R)%R -> (mkp uc up N) -> (Rabs (double_exact uc) <= 1)%R -> (Rabs (double_value uc) <= 2)%R. intros. replace (double_value uc) with ((double_value uc - double_exact uc)+double_exact uc)%R by ring. apply Rle_trans with (1:=Rabs_triang _ _). fold (double_round_error uc). apply Rplus_le_compat;[idtac|assumption]. apply Rle_trans with (1:=mkp_rnd_error _ _ _ H H1). assert (N <= powerRZ radix 26)%R. apply Rle_trans with (1:=H0). replace 26%R with (INR 26). rewrite Rpower_pow. simpl; right; ring. auto with real. simpl; ring. apply Rle_trans with ((powerRZ radix 26 + 1) * (powerRZ radix 26 + 2) * / 2 * powerRZ radix (-53))%R. apply Rmult_le_compat_r; auto with real zarith. apply Rmult_le_compat_r; auto with real zarith. apply Rmult_le_compat; auto with real zarith. apply Rle_trans with (IZR N); auto with real. apply Rle_trans with (IZR N+1)%R; auto with real. replace (/2)%R with (powerRZ radix (-1)) by (simpl; field). rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with zarith real. replace 2%R with (powerRZ radix 1) by (simpl; ring). pattern 1%R at 1; replace 1%R with (powerRZ radix 0) by (simpl; ring). ring_simplify; unfold pow; rewrite Rmult_1_r. repeat rewrite <- powerRZ_add; auto with real zarith. ring_simplify ((26 + 26 + (-1 + -53)))%Z; ring_simplify (26 + 0 + (-1 + -53))%Z; ring_simplify ((26 + 1 + (-1 + -53)))%Z; ring_simplify (0 + 1 + (-1 + -53))%Z. apply Rle_trans with (powerRZ radix (-2)+powerRZ radix (-2)+powerRZ radix (-2)+powerRZ radix (-2))%R. repeat rewrite Rplus_assoc; apply Rplus_le_compat_l. repeat apply Rplus_le_compat; apply Rle_powerRZ; auto with real zarith. right; simpl; field. Qed. Lemma mkp_le_2: forall (uc up: double), forall N:Z, (0 <= N)%Z ->(IZR N <= Rpower (2)%R (26)%R)%R -> (mkp uc up N) -> (Rabs (double_exact up) <= 1)%R -> (Rabs (double_value up) <= 2)%R. intros. replace (double_value up) with ((double_value up - double_exact up)+double_exact up)%R by ring. apply Rle_trans with (1:=Rabs_triang _ _). fold (double_round_error up). apply Rplus_le_compat;[idtac|assumption]. apply Rle_trans with (1:=mkp_rnd_error2 _ _ _ H H1). assert (N <= powerRZ radix 26)%R. apply Rle_trans with (1:=H0). replace 26%R with (INR 26). rewrite Rpower_pow. simpl; right; ring. auto with real. simpl; ring. apply Rle_trans with ((powerRZ radix 26) * (powerRZ radix 26 + 1) * / 2 * powerRZ radix (-53))%R. apply Rmult_le_compat_r; auto with real zarith. apply Rmult_le_compat_r; auto with real zarith. replace (/2)%R with (powerRZ radix (-1)) by (simpl; field). rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with zarith real. pattern 1%R at 1; replace 1%R with (powerRZ radix 0) by (simpl; ring). ring_simplify; unfold pow; rewrite Rmult_1_r. repeat rewrite <- powerRZ_add; auto with real zarith. ring_simplify ((26 + 26 + (-1 + -53)))%Z; ring_simplify (26 + 0 + (-1 + -53))%Z. apply Rle_trans with (powerRZ radix (-1)+powerRZ radix (-1))%R. apply Rplus_le_compat; apply Rle_powerRZ; auto with real zarith. right; simpl; field. Qed. Open Local Scope Z_scope. (* Why obligation from file "rec_lin2.c", line 21, characters 21-27: *) (*Why goal*) Lemma comput_seq_ensures_default_po_1 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), (* JC_42 *) (* JC_37 *) 2 <= (integer_of_int32 i). Proof. intuition. rewrite HW_10, HW_9;auto with zarith. Save. (* Why obligation from file "rec_lin2.c", line 21, characters 31-39: *) (*Why goal*) Lemma comput_seq_ensures_default_po_2 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), (* JC_42 *) (* JC_38 *) (integer_of_int32 i) <= ((integer_of_int32 N) + 1). Proof. intuition. rewrite HW_10, HW_9; auto with zarith. Save. (* Why obligation from file "rec_lin2.c", line 22, characters 8-39: *) (*Why goal*) Lemma comput_seq_ensures_default_po_3 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), (* JC_42 *) (* JC_39 *) (eq (double_exact ucur) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i) - 1)) ( Rminus (double_value u1) (double_value u0))))). Proof. intuition. rewrite HW_8, HW_10,HW_9, H2. simpl; ring. Save. (* Why obligation from file "rec_lin2.c", line 23, characters 8-39: *) (*Why goal*) Lemma comput_seq_ensures_default_po_4 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), (* JC_42 *) (* JC_40 *) (eq (double_exact uprev) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i) - 2)) ( Rminus (double_value u1) (double_value u0))))). Proof. intuition. rewrite HW_10, HW_9, HW_7, H0. simpl; ring. Save. (* Why obligation from file "rec_lin2.c", line 24, characters 8-27: *) (*Why goal*) Lemma comput_seq_ensures_default_po_5 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), (* JC_42 *) (* JC_41 *) (mkp ucur uprev ((integer_of_int32 i) - 2)). Proof. intuition. rewrite HW_10,HW_9; simpl. unfold mkp. exists (fun n:nat => 0%R). split. intros; rewrite Rabs_R0; auto with real zarith. rewrite HW_7; rewrite HW_8; rewrite H0; rewrite H2; simpl; split; ring. Save. (* Why obligation from file "rec_lin2.c", line 28, characters 15-27: *) (*Why goal*) Lemma comput_seq_ensures_default_po_6 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (result1: double), forall (HW_15: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_16: tmp = result1), (* JC_47 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0))). Proof. intuition. unfold double_value; simpl. assert (FtoRradix (Float (Fnum (df ucur0)) (Fexp (df ucur0)+1))=2*FtoRradix (df ucur0))%R. unfold FtoRradix, FtoR; simpl. rewrite powerRZ_add; auto with real zarith. simpl; ring. rewrite <- H10. unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bdouble 53%nat (EvenClosest bdouble radix 53); try apply pdGivesBound; auto with zarith. assert (Fbounded bdouble (df ucur0)). apply FcanonicBound with radix; auto. destruct ucur0; auto. elim H13; intros; split;auto with zarith. apply Zle_trans with (1:=H15); simpl; auto with zarith. fold FtoRradix; rewrite H10. destruct HW_15; unfold round_double,round_double_aux, double_value in H13; simpl in H13. replace 2%R with (FtoRradix (df result0)); auto with float. rewrite HW_16. generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (FtoRradix (df result0) * FtoRradix (df ucur0))%R (RND_EvenClosest bdouble radix 53 (FtoRradix(df result0) * FtoRradix (df ucur0))); try apply pdGivesBound; auto with zarith; clear T. apply FcanonicBound with radix. destruct result1; assumption. Save. (* Why obligation from file "rec_lin2.c", line 21, characters 21-27: *) (*Why goal*) Lemma comput_seq_ensures_default_po_7 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (result1: double), forall (HW_15: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_16: tmp = result1), forall (HW_17: (* JC_47 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (result2: double), forall (HW_18: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_19: tmp0 = result2), forall (uprev1: double), forall (HW_20: uprev1 = ucur0), forall (ucur1: double), forall (HW_21: ucur1 = tmp0), forall (result3: int32), forall (HW_22: (integer_of_int32 result3) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_23: i1 = result3), (* JC_42 *) (* JC_37 *) 2 <= (integer_of_int32 i1). Proof. intuition. rewrite HW_23, HW_22; auto with zarith. Save. (* Why obligation from file "rec_lin2.c", line 21, characters 31-39: *) (*Why goal*) Lemma comput_seq_ensures_default_po_8 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (result1: double), forall (HW_15: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_16: tmp = result1), forall (HW_17: (* JC_47 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (result2: double), forall (HW_18: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_19: tmp0 = result2), forall (uprev1: double), forall (HW_20: uprev1 = ucur0), forall (ucur1: double), forall (HW_21: ucur1 = tmp0), forall (result3: int32), forall (HW_22: (integer_of_int32 result3) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_23: i1 = result3), (* JC_42 *) (* JC_38 *) (integer_of_int32 i1) <= ((integer_of_int32 N) + 1). Proof. intuition. rewrite HW_23, HW_22; auto with zarith. Save. (* Why obligation from file "rec_lin2.c", line 22, characters 8-39: *) (*Why goal*) Lemma comput_seq_ensures_default_po_9 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (result1: double), forall (HW_15: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_16: tmp = result1), forall (HW_17: (* JC_47 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (result2: double), forall (HW_18: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_19: tmp0 = result2), forall (uprev1: double), forall (HW_20: uprev1 = ucur0), forall (ucur1: double), forall (HW_21: ucur1 = tmp0), forall (result3: int32), forall (HW_22: (integer_of_int32 result3) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_23: i1 = result3), (* JC_42 *) (* JC_39 *) (eq (double_exact ucur1) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i1) - 1)) ( Rminus (double_value u1) (double_value u0))))). Proof. intuition. why2float. rewrite H17,H23,H10. rewrite H26,H14, H11. rewrite HW_23,HW_22. rewrite H5,H7. ring_simplify (integer_of_int32 i0 + 1 - 1)%Z. unfold Zminus; rewrite 2!plus_IZR. simpl; ring. Save. (* Why obligation from file "rec_lin2.c", line 23, characters 8-39: *) (*Why goal*) Lemma comput_seq_ensures_default_po_10 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (result1: double), forall (HW_15: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_16: tmp = result1), forall (HW_17: (* JC_47 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (result2: double), forall (HW_18: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_19: tmp0 = result2), forall (uprev1: double), forall (HW_20: uprev1 = ucur0), forall (ucur1: double), forall (HW_21: ucur1 = tmp0), forall (result3: int32), forall (HW_22: (integer_of_int32 result3) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_23: i1 = result3), (* JC_42 *) (* JC_40 *) (eq (double_exact uprev1) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i1) - 2)) ( Rminus (double_value u1) (double_value u0))))). Proof. intuition. rewrite HW_20, H5. replace (integer_of_int32 i1 - 2)%Z with (integer_of_int32 i0 - 1)%Z; try reflexivity. rewrite HW_23, HW_22; ring. Save. (* Why obligation from file "rec_lin2.c", line 24, characters 8-27: *) (*Why goal*) Lemma comput_seq_ensures_default_po_11 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (result1: double), forall (HW_15: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_16: tmp = result1), forall (HW_17: (* JC_47 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (result2: double), forall (HW_18: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_19: tmp0 = result2), forall (uprev1: double), forall (HW_20: uprev1 = ucur0), forall (ucur1: double), forall (HW_21: ucur1 = tmp0), forall (result3: int32), forall (HW_22: (integer_of_int32 result3) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_23: i1 = result3), (* JC_42 *) (* JC_41 *) (mkp ucur1 uprev1 ((integer_of_int32 i1) - 2)). Proof. intuition. elim H9; intros eps (N6,(N7,N8)). unfold mkp. exists (fun i:nat => if (Z_eq_dec i (integer_of_int32 i1-2)) then (-(df tmp-df uprev0-df tmp0))%R else (eps i)). split. intros. case (Z_eq_dec i2 (integer_of_int32 i1 - 2)); intros. rewrite Rabs_Ropp. apply Le2errLe. destruct HW_18. apply EvenClosestCompatible with (df tmp - df uprev0)%R (RND_EvenClosest bdouble radix 53 (df tmp - df uprev0)); try apply pdGivesbound; auto with zarith. fold FtoRradix; rewrite HW_19. unfold double_value in H13; rewrite H13. reflexivity. apply FcanonicBound with radix; destruct tmp0; assumption. replace (df tmp -df uprev0)%R with ( (double_value u0 + integer_of_int32 i0 * (double_value u1 - double_value u0)) + 2*(double_value ucur0 - double_exact ucur0) + -(double_value uprev0 - double_exact uprev0) )%R. 2: unfold double_value in HW_17; rewrite HW_17. 2: rewrite H5, H7. 2: unfold Zminus, double_value; repeat rewrite plus_IZR. 2: simpl; ring. apply Rle_trans with (Rabs (double_value u0 + integer_of_int32 i0 * (double_value u1 - double_value u0) + 2 * (double_value ucur0 - double_exact ucur0)) + Rabs (- (double_value uprev0 - double_exact uprev0)))%R;[apply Rabs_triang|idtac]. apply Rle_trans with (Rabs (double_value u0 + integer_of_int32 i0 * (double_value u1 - double_value u0)) + Rabs (2 * (double_value ucur0 - double_exact ucur0)) + Rabs (- (double_value uprev0 - double_exact uprev0)))%R; [apply Rplus_le_compat_r; apply Rabs_triang|idtac]. apply Rle_trans with (1+2*((integer_of_int32 i0-1)*integer_of_int32 i0*/2*powerRZ radix (-53))+ ((integer_of_int32 i0-2)*(integer_of_int32 i0-1)*/2*powerRZ radix (-53)))%R. apply Rplus_le_compat. apply Rplus_le_compat. apply H4; auto with zarith. rewrite Rabs_mult. rewrite Rabs_right;[idtac|apply Rle_ge; auto with real]. apply Rmult_le_compat_l; auto with real. unfold double_round_error. apply Rle_trans with (((integer_of_int32 i0 - 2)%Z+1) * ((integer_of_int32 i0-2)%Z+2) * / 2 * powerRZ radix (-53))%R. apply mkp_rnd_error with uprev0; auto with zarith. unfold Zminus; repeat rewrite plus_IZR; simpl; right; ring. apply Rle_trans with (double_round_error uprev0). unfold double_round_error. rewrite Rabs_Ropp; right; reflexivity. apply Rle_trans with (((integer_of_int32 i0 - 2)%Z) * ((integer_of_int32 i0-2)%Z+1) * / 2 * powerRZ radix (-53))%R. apply mkp_rnd_error2 with ucur0; auto with zarith. unfold Zminus; repeat rewrite plus_IZR; simpl; right; ring. assert (integer_of_int32 i0 <= powerRZ radix 26)%R. apply Rle_trans with (integer_of_int32 N). apply Rle_IZR; apply HW_13. apply Rle_trans with (1:=H1). replace 26%R with (INR 26). rewrite Rpower_pow. simpl; right; ring. auto with real. simpl; ring. apply Rle_trans with (1 + 2 * ((powerRZ radix 26) * (powerRZ radix 26+1) * / 2 * powerRZ radix (-53)) + powerRZ radix 26 * powerRZ radix 26 * / 2 * powerRZ radix (-53))%R. apply Rplus_le_compat. apply Rplus_le_compat_l; apply Rmult_le_compat_l; auto with real. repeat apply Rmult_le_compat_r; auto with real zarith. apply Rmult_le_compat; auto with real zarith. apply Rle_trans with (IZR (integer_of_int32 i0 - 1)); auto with real zarith. unfold Zminus; rewrite plus_IZR; auto with real zarith. apply Rle_trans with (2:=H13). apply Rle_trans with (integer_of_int32 i0 - 0)%R; auto with real. apply Rplus_le_compat_l; auto with real. apply Rle_trans with (1:=H13); auto with real. repeat apply Rmult_le_compat_r; auto with real zarith. apply Rmult_le_compat; auto with real zarith. apply Rle_trans with (IZR( integer_of_int32 i0-2)); auto with real zarith. replace R0 with (IZR 0) by reflexivity. apply Rle_IZR; auto with zarith. unfold Zminus; rewrite plus_IZR; simpl; right; ring. apply Rle_trans with (IZR( integer_of_int32 i0-1)); auto with real zarith. unfold Zminus; rewrite plus_IZR; simpl; right; ring. apply Rle_trans with (2:=H13). apply Rle_trans with (integer_of_int32 i0 - 0)%R; auto with real. apply Rplus_le_compat_l; auto with real. apply Rle_trans with (2:=H13). apply Rle_trans with (integer_of_int32 i0 - 0)%R; auto with real. apply Rplus_le_compat_l; auto with real. replace (/2)%R with (powerRZ radix (-1));[idtac|simpl; field; auto with real]. 2: assert (0 < 4)%R; auto with real. 2: apply Rlt_le_trans with 2%R; auto with real. repeat rewrite <- powerRZ_add; auto with real zarith. rewrite Rmult_plus_distr_l. replace (powerRZ radix 26 * 1)%R with (powerRZ radix 26);[idtac|ring]. rewrite Rmult_plus_distr_r; rewrite Rmult_plus_distr_r; rewrite Rmult_plus_distr_r. repeat rewrite <- powerRZ_add; auto with real zarith. replace (26 + 26 + -1 + -53)%Z with (-2)%Z;[idtac|ring]. replace (26 + -1 + -53)%Z with (-28)%Z;[idtac|ring]. apply Rle_trans with (1+3*powerRZ radix (-2)+2* powerRZ radix (-28))%R;[right; ring|idtac]. apply Rle_trans with (1+3*powerRZ radix (-2)+2* powerRZ radix (-4))%R. apply Rplus_le_compat_l; apply Rmult_le_compat_l; auto with real zarith. apply Rle_powerRZ; unfold radix; simpl; auto with real zarith. simpl; right; field. apply N6; auto with zarith. replace (integer_of_int32 i0) with (integer_of_int32 i1-1); auto with zarith. rewrite HW_23, HW_22; ring. split. rewrite HW_20; rewrite N8. replace (Zabs_nat (integer_of_int32 i1 - 2) - 1)%nat with (Zabs_nat (integer_of_int32 i0 - 2)). apply sum_eq. intros. assert (i2 <= Zabs_nat (integer_of_int32 i1 - 3))%nat. rewrite HW_23, HW_22; apply le_trans with (1:=H10). ring_simplify (integer_of_int32 i0 + 1 - 3); apply le_refl. assert (i2 <= integer_of_int32 i1 - 3)%Z. rewrite <- (Zabs_eq (integer_of_int32 i1 - 3)). rewrite <- inj_Zabs_nat. now apply inj_le. rewrite HW_23, HW_22; auto with zarith. case Z_eq_dec. intros T; absurd (i2 <= integer_of_int32 i1 - 3)%Z; auto with zarith. intros; rewrite HW_23, HW_22. unfold Zminus; repeat rewrite plus_IZR;simpl; ring. rewrite HW_23, HW_22; auto with zarith. assert (Z_of_nat (Zabs_nat (integer_of_int32 i0 - 2)) = (Zabs_nat (integer_of_int32 i0 +1 - 2) - 1))%Z; auto with zarith. repeat rewrite <- Zabs_absolu; repeat rewrite Zabs_eq; auto with zarith. case (Zle_lt_or_eq 2 (integer_of_int32 i0)); auto with zarith; intros. cut ((Zabs_nat (integer_of_int32 i1 - 2)= S((Zabs_nat (integer_of_int32 i1 - 3)))));[intros Y|idtac]. rewrite Y; rewrite tech5. replace (((integer_of_int32 i1 - 2)%Z +1 - S (Zabs_nat (integer_of_int32 i1 - 3))) * (if Z_eq_dec (S (Zabs_nat (integer_of_int32 i1 - 3))) (integer_of_int32 i1 - 2) then (-(df tmp - df uprev0 - df tmp0))%R else eps (S (Zabs_nat (integer_of_int32 i1 - 3)))))%R with (-(df tmp - df uprev0 - df tmp0))%R. 2: replace (((integer_of_int32 i1 - 2)%Z +1 - S (Zabs_nat (integer_of_int32 i1 - 3))))%R with 1%R. 2: replace (Z_of_nat (S (Zabs_nat (integer_of_int32 i1 - 3)))) with (integer_of_int32 i1-2)%Z; auto with zarith. 2: case Z_eq_dec; simpl. 2: intros; ring. 2: intros U; absurd (integer_of_int32 i1 - 2 =integer_of_int32 i1 - 2)%Z; auto with zarith. 2: rewrite <- Y; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith. 2: rewrite HW_23, HW_22; auto with zarith. 2: rewrite <- Y. 2: replace (INR (Zabs_nat (integer_of_int32 i1 - 2))) with (IZR (Z_of_nat (Zabs_nat (integer_of_int32 i1 - 2)))). 2:rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith real. 2: ring. 2: rewrite HW_23, HW_22; auto with zarith. 2:rewrite INR_IZR_INZ; auto with zarith. replace (sum_f_R0 (fun i2 : nat => (((integer_of_int32 i1 - 2)%Z + 1 - i2) * (if Z_eq_dec i2 (integer_of_int32 i1 - 2) then (-(df tmp - df uprev0 - df tmp0))%R else eps i2))%R) (Zabs_nat (integer_of_int32 i1 - 3))) with (sum_f_R0 (fun i2 : nat => (((integer_of_int32 i1 - 2)%Z + 1 - i2) *(eps i2))%R) (Zabs_nat (integer_of_int32 i1 - 3))). 2:apply sum_eq; auto with zarith. 2: intros j Hm; case Z_eq_dec; auto with zarith. 2: intros H'; Contradict Hm; auto with zarith. 2:assert ( Zabs_nat (integer_of_int32 i1 - 3) < j)%nat; auto with zarith. 2:assert ( Zabs_nat (integer_of_int32 i1 - 3) < j)%Z; auto with zarith. 2:rewrite H'; rewrite <- Zabs_absolu; rewrite Zabs_eq;auto with zarith. 2: rewrite HW_23, HW_22; auto with zarith. replace (Zabs_nat (integer_of_int32 i1 - 3)) with (Zabs_nat (integer_of_int32 i0 - 2)). replace (sum_f_R0 (fun i2 : nat => (((integer_of_int32 i1 - 2)%Z + 1 - i2) * eps i2)%R) (Zabs_nat (integer_of_int32 i0 - 2))) with (sum_f_R0 (fun i2 : nat => ((integer_of_int32 i0 - 2)%Z + 1 - i2) * eps i2) (Zabs_nat (integer_of_int32 i0 - 2)) - (sum_f_R0 (fun i2 : nat => (-eps i2)%R) (Zabs_nat (integer_of_int32 i0 - 2))))%R. 2: apply sym_eq; apply tech11. 2: intros; rewrite HW_23, HW_22. 2: unfold Zminus; repeat rewrite plus_IZR;simpl; ring. 2: rewrite HW_23, HW_22; replace (integer_of_int32 i0 + 1 - 3)%Z with (integer_of_int32 i0-2)%Z; auto with zarith. rewrite <- N8. rewrite HW_21, HW_19; destruct HW_18 as (K1,(K2,K3)); rewrite K2. unfold double_value. destruct HW_15 as (K4,(K5,K6)). rewrite HW_16,K5, H11. replace (FtoRradix (df result1)) with (2 * df ucur0)%R. apply Rplus_eq_reg_l with (-(df result2)+ double_exact ucur0+df ucur0 - double_exact uprev0)%R. apply trans_eq with (df ucur0- double_exact ucur0)%R;[ring|idtac]. apply trans_eq with ((df uprev0 - double_exact uprev0) - sum_f_R0 (fun i2 : nat => - eps i2) (Zabs_nat (integer_of_int32 i0 - 2)))%R;[idtac|simpl; ring]. replace (FtoRradix (df ucur0)) with (double_value ucur0); auto. replace (FtoRradix (df uprev0)) with (double_value uprev0); auto. rewrite N7; rewrite N8. replace (integer_of_int32 i0 - 2 - 1)%Z with (integer_of_int32 i0-3)%Z; auto with zarith. cut ((Zabs_nat (integer_of_int32 i0 - 2)=S ((Zabs_nat (integer_of_int32 i0 - 2) -1))));[intros Y'|idtac]. pattern (Zabs_nat (integer_of_int32 i0 - 2)) at 1;rewrite Y'; rewrite tech5. pattern (Zabs_nat (integer_of_int32 i0 - 2)) at 5;rewrite Y'; rewrite tech5. apply trans_eq with ((sum_f_R0 (fun i2 : nat => ((integer_of_int32 i0 - 2)%Z - i2) * eps i2) (Zabs_nat (integer_of_int32 i0 - 2)-1) - (sum_f_R0 (fun i2 : nat => - eps i2) (Zabs_nat (integer_of_int32 i0 - 2)-1))) + eps (S (Zabs_nat (integer_of_int32 i0 - 2)-1)))%R;[idtac|ring]. replace ((sum_f_R0 (fun i2 : nat => (((integer_of_int32 i0 - 2)%Z - i2) * eps i2)%R) (Zabs_nat (integer_of_int32 i0 - 2)-1) - (sum_f_R0 (fun i2 : nat => (- eps i2)%R) (Zabs_nat (integer_of_int32 i0 - 2)-1))))%R with (sum_f_R0 (fun i2 : nat => (((integer_of_int32 i0 - 2)%Z + 1 - i2) * eps i2))%R (Zabs_nat (integer_of_int32 i0 - 2)-1)). replace ((integer_of_int32 i0 - 2)%Z + 1 - S (Zabs_nat (integer_of_int32 i0 - 2)-1))%R with 1%R. ring. rewrite <- Y'; rewrite INR_IZR_INZ. rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith real; ring. apply tech11. intros; unfold Zminus; rewrite plus_IZR; simpl; ring. apply trans_eq with (S (Peano.pred (Zabs_nat (integer_of_int32 i0 - 2))))%nat; auto with zarith. assert (0 < Zabs_nat (integer_of_int32 i0 - 2))%nat; auto with zarith. assert (0 < Zabs_nat (integer_of_int32 i0 - 2))%Z; auto with zarith. rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith. unfold double_value in HW_17; rewrite <- HW_17. now rewrite HW_16. apply trans_eq with (Zabs_nat (integer_of_int32 i1 - 3)+1)%nat; auto with zarith. assert (Z_of_nat (Zabs_nat (integer_of_int32 i1 - 2)) = Zabs_nat (integer_of_int32 i1 - 3) + 1)%Z; auto with zarith. repeat rewrite <- Zabs_absolu; repeat rewrite Zabs_eq; auto with zarith. rewrite HW_23, HW_22; auto with zarith. rewrite HW_23, HW_22; auto with zarith. rewrite HW_23, HW_22; rewrite <- H10; simpl. rewrite HW_21. destruct HW_18 as (K1,(K2,K3)). rewrite HW_19 at 2; rewrite K2. replace (FtoRradix (df tmp)) with (2 * df ucur0)%R; auto. unfold double_value; replace (double_exact tmp) with (2*double_exact ucur0)%R. apply Rplus_eq_reg_l with (-(df tmp0)- double_exact uprev0 +2* df ucur0)%R. apply trans_eq with (2*(double_value ucur0 - double_exact ucur0))%R. unfold double_value; ring. apply trans_eq with ((double_value uprev0 - double_exact uprev0)+2* eps 0%nat)%R; [idtac|unfold double_value; simpl;ring]. rewrite N7; rewrite N8. rewrite <- H10; simpl; ring. rewrite HW_16; destruct HW_15 as (K4,(K5,K6)). rewrite K5; now rewrite H11. Save. (* Why obligation from file "rec_lin2.c", line 10, characters 12-41: *) (*Why goal*) Lemma comput_seq_ensures_default_po_12 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_24: (integer_of_int32 i0) > (integer_of_int32 N)), forall (why__return: double), forall (HW_25: why__return = ucur0), (* JC_17 *) (* JC_15 *) (eq (double_exact why__return) (Rplus (double_value u0) (Rmult (IZR (integer_of_int32 N)) ( Rminus (double_value u1) ( double_value u0))))). Proof. intuition. rewrite HW_25; rewrite H5. replace (integer_of_int32 i0 - 1)%Z with (integer_of_int32 N); auto with real zarith. Save. (* Why obligation from file "rec_lin2.c", line 11, characters 13-61: *) (*Why goal*) Lemma comput_seq_ensures_default_po_13 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_42 *) ((* JC_37 *) 2 <= (integer_of_int32 i0) /\ (* JC_38 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_39 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_40 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_41 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_24: (integer_of_int32 i0) > (integer_of_int32 N)), forall (why__return: double), forall (HW_25: why__return = ucur0), (* JC_17 *) (* JC_16 *) (Rle (double_round_error why__return) (Rmult (Rdiv (Rmult (IZR (integer_of_int32 N)) (Rplus (IZR (integer_of_int32 N)) (1)%R)) (2)%R) ( powerRZ (2)%R (-53)))). Proof. intuition. rewrite HW_25. assert (integer_of_int32 i0=integer_of_int32 N+1)%Z; auto with zarith. apply Rle_trans with ((Z.pred (integer_of_int32 N) +1) * (Z.pred (integer_of_int32 N) +2)* / 2 * powerRZ radix (- 53))%R. apply mkp_rnd_error with uprev0; auto with zarith. replace (Z.pred (integer_of_int32 N)) with (integer_of_int32 i0-2)%Z; auto with zarith. apply Rmult_le_compat_r; auto with real zarith. unfold Rdiv; apply Rmult_le_compat_r; auto with real zarith. unfold Zpred, Zminus; repeat rewrite plus_IZR; simpl; right; ring. Save. (* Why obligation from file "rec_lin2.c", line 27, characters 8-14: *) (*Why goal*) Lemma comput_seq_safety_po_1 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_30 *) True), forall (HW_12: (* JC_28 *) ((* JC_23 *) 2 <= (integer_of_int32 i0) /\ (* JC_24 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_25 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_26 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_27 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), (no_overflow_double nearest_even (Rmult (double_value result0) (double_value ucur0))). Proof. intuition. rewrite H8. assert (Rabs (double_value ucur0) <= 2)%R. apply mkp_le_1 with (3:=H9); auto with real zarith. apply Rle_trans with (2:=H1); apply Rle_IZR; auto with zarith. rewrite H5; apply H4; auto with zarith. why2gappa. gappa. Save. (* Why obligation from file "rec_lin2.c", line 29, characters 4-14: *) (*Why goal*) Lemma comput_seq_safety_po_2 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_30 *) True), forall (HW_12: (* JC_28 *) ((* JC_23 *) 2 <= (integer_of_int32 i0) /\ (* JC_24 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_25 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_26 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_27 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (HW_15: (no_overflow_double nearest_even (Rmult (double_value result0) (double_value ucur0)))), forall (result1: double), forall (HW_16: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_17: tmp = result1), forall (HW_18: (* JC_33 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), (no_overflow_double nearest_even (Rminus (double_value tmp) (double_value uprev0))). Proof. intuition. rewrite HW_18. assert (Rabs (double_value ucur0) <= 2)%R. apply mkp_le_1 with (3:=H9); auto with real zarith. apply Rle_trans with (2:=H1); apply Rle_IZR; auto with zarith. rewrite H5; apply H4; auto with zarith. assert (Rabs (double_value uprev0) <= 2)%R. apply mkp_le_2 with (3:=H9); auto with real zarith. apply Rle_trans with (2:=H1); apply Rle_IZR; auto with zarith. rewrite H7; apply H4; auto with zarith. why2gappa. gappa. Save. (* Why obligation from file "rec_lin2.c", line 26, characters 18-21: *) (*Why goal*) Lemma comput_seq_safety_po_3 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_30 *) True), forall (HW_12: (* JC_28 *) ((* JC_23 *) 2 <= (integer_of_int32 i0) /\ (* JC_24 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_25 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_26 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_27 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (HW_15: (no_overflow_double nearest_even (Rmult (double_value result0) (double_value ucur0)))), forall (result1: double), forall (HW_16: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_17: tmp = result1), forall (HW_18: (* JC_33 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (HW_19: (no_overflow_double nearest_even (Rminus (double_value tmp) (double_value uprev0)))), forall (result2: double), forall (HW_20: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_21: tmp0 = result2), forall (uprev1: double), forall (HW_22: uprev1 = ucur0), forall (ucur1: double), forall (HW_23: ucur1 = tmp0), (-2147483648) <= ((integer_of_int32 i0) + 1). Proof. intuition. Save. (* Why obligation from file "rec_lin2.c", line 26, characters 18-21: *) (*Why goal*) Lemma comput_seq_safety_po_4 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_30 *) True), forall (HW_12: (* JC_28 *) ((* JC_23 *) 2 <= (integer_of_int32 i0) /\ (* JC_24 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_25 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_26 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_27 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (HW_15: (no_overflow_double nearest_even (Rmult (double_value result0) (double_value ucur0)))), forall (result1: double), forall (HW_16: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_17: tmp = result1), forall (HW_18: (* JC_33 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (HW_19: (no_overflow_double nearest_even (Rminus (double_value tmp) (double_value uprev0)))), forall (result2: double), forall (HW_20: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_21: tmp0 = result2), forall (uprev1: double), forall (HW_22: uprev1 = ucur0), forall (ucur1: double), forall (HW_23: ucur1 = tmp0), ((integer_of_int32 i0) + 1) <= 2147483647. Proof. intuition. apply Zle_trans with (Zpower_nat 2 26 + 1). apply Zplus_le_compat_r. apply Zle_trans with (1:=HW_13). apply le_IZR. apply Rle_trans with (1:=H1). right; replace 26%R with (INR 26) by (simpl; ring). rewrite Zpower_nat_Z_powerRZ. rewrite Rpower_pow; auto with real. simpl; auto with zarith. Save. (* Why obligation from file "rec_lin2.c", line 25, characters 19-22: *) (*Why goal*) Lemma comput_seq_safety_po_5 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_30 *) True), forall (HW_12: (* JC_28 *) ((* JC_23 *) 2 <= (integer_of_int32 i0) /\ (* JC_24 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_25 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_26 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_27 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (HW_15: (no_overflow_double nearest_even (Rmult (double_value result0) (double_value ucur0)))), forall (result1: double), forall (HW_16: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_17: tmp = result1), forall (HW_18: (* JC_33 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (HW_19: (no_overflow_double nearest_even (Rminus (double_value tmp) (double_value uprev0)))), forall (result2: double), forall (HW_20: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_21: tmp0 = result2), forall (uprev1: double), forall (HW_22: uprev1 = ucur0), forall (ucur1: double), forall (HW_23: ucur1 = tmp0), forall (HW_24: (-2147483648) <= ((integer_of_int32 i0) + 1) /\ ((integer_of_int32 i0) + 1) <= 2147483647), forall (result3: int32), forall (HW_25: (integer_of_int32 result3) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_26: i1 = result3), 0 <= ((* JC_36 *) ((integer_of_int32 N) - (integer_of_int32 i0))). Proof. intuition. Save. (* Why obligation from file "rec_lin2.c", line 25, characters 19-22: *) (*Why goal*) Lemma comput_seq_safety_po_6 : forall (u0: double), forall (u1: double), forall (N: int32), forall (HW_1: (* JC_13 *) ((* JC_8 *) 2 <= (integer_of_int32 N) /\ (* JC_9 *) (Rle (IZR (integer_of_int32 N)) (Rpower (2)%R (26)%R)) /\ (* JC_10 *) (eq (double_exact u0) (double_value u0)) /\ (* JC_11 *) (eq (double_exact u1) (double_value u1)) /\ (* JC_12 *) (forall (k:Z), (0 <= k /\ k <= (integer_of_int32 N) -> (Rle (Rabs (Rplus (double_value u0) (Rmult (IZR k) (Rminus (double_value u1) (double_value u0))))) (1)%R))))), forall (uprev: double), forall (HW_7: uprev = u0), forall (ucur: double), forall (HW_8: ucur = u1), forall (result: int32), forall (HW_9: (integer_of_int32 result) = 2), forall (i: int32), forall (HW_10: i = result), forall (i0: int32), forall (ucur0: double), forall (uprev0: double), forall (HW_11: (* JC_30 *) True), forall (HW_12: (* JC_28 *) ((* JC_23 *) 2 <= (integer_of_int32 i0) /\ (* JC_24 *) (integer_of_int32 i0) <= ((integer_of_int32 N) + 1) /\ (* JC_25 *) (eq (double_exact ucur0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 1)) (Rminus ( double_value u1) ( double_value u0))))) /\ (* JC_26 *) (eq (double_exact uprev0) (Rplus (double_value u0) (Rmult (IZR ((integer_of_int32 i0) - 2)) ( Rminus (double_value u1) ( double_value u0))))) /\ (* JC_27 *) (mkp ucur0 uprev0 ((integer_of_int32 i0) - 2)))), forall (HW_13: (integer_of_int32 i0) <= (integer_of_int32 N)), forall (result0: double), forall (HW_14: (eq (double_value result0) (2)%R) /\ (eq (double_exact result0) (2)%R) /\ (eq (double_model result0) (2)%R)), forall (HW_15: (no_overflow_double nearest_even (Rmult (double_value result0) (double_value ucur0)))), forall (result1: double), forall (HW_16: (mul_double_post nearest_even result0 ucur0 result1)), forall (tmp: double), forall (HW_17: tmp = result1), forall (HW_18: (* JC_33 *) (eq (double_value tmp) (Rmult (2)%R (double_value ucur0)))), forall (HW_19: (no_overflow_double nearest_even (Rminus (double_value tmp) (double_value uprev0)))), forall (result2: double), forall (HW_20: (sub_double_post nearest_even tmp uprev0 result2)), forall (tmp0: double), forall (HW_21: tmp0 = result2), forall (uprev1: double), forall (HW_22: uprev1 = ucur0), forall (ucur1: double), forall (HW_23: ucur1 = tmp0), forall (HW_24: (-2147483648) <= ((integer_of_int32 i0) + 1) /\ ((integer_of_int32 i0) + 1) <= 2147483647), forall (result3: int32), forall (HW_25: (integer_of_int32 result3) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_26: i1 = result3), ((* JC_36 *) ((integer_of_int32 N) - (integer_of_int32 i1))) < ((* JC_36 *) ((integer_of_int32 N) - (integer_of_int32 i0))). Proof. intuition. rewrite HW_26, HW_25. auto with zarith. Save.