Require Export realbasis. Require Export proof_utils. Require Export real_facts. Require Export add_correct. Theorem mult_correct_body : forall mult_a' : stream idigit -> stream idigit*stream idigit -> stream idigit, (forall v1 v2 v3 x u u', (v3 <= 1/4)%R -> (v1 +v2*v3 <= 1)%R -> represents x v1 -> represents u v2 -> represents u' v3 -> represents (mult_a' x (u, u')) (v1+v2*v3)%R) -> forall v1 v2 v3 x u u', (v3 <= 1/4)%R -> (v1 +v2*v3 <= 1)%R -> represents x v1 -> represents u (2*v2) -> represents u' v3 -> represents (series_body _ mult_a' x (u, u')) (v1+v2*v3)%R. intros mult_a' mult_correct_body v1 v2 v3 x u u' Hv3lt Hsum Hv1 Hv2 Hv3. unfold series_body. assert (2*v2*v3 <= 1/4)%R. clear mult_correct_body. interval_from_represents Hv2; intros; dec_tac. interval_from_represents Hv3; intros; dec_tac. replace (1/4)%R with (1*(1/4))%R. apply Rmult_le_compat. fourier. fourier. fourier. fourier. ring. assert (0 <= 2*v2*v3)%R. intervals_from_represents Hv2 Hv3. apply Rmult_le_pos; assumption. destruct x as [ [ | | ] x1]. (* case x = L.. *) destruct x1 as [ [ | | ] x2]. (* case x = L::L.. *) inversion Hv1. match goal with id : represents (L::x2) _ |- _ => intervals_from_represents Hv1 id end. constructor';[idtac | clear mult_correct_body]. replace (2*(lift L r+v2*v3))%R with (r + 2*v2*v3)%R. apply mult_correct_body; clear mult_correct_body; auto. fourier. clear mult_correct_body; unfold lift, alpha; field; auto with real1. unfold lift, alpha; rewrite Rmult_plus_distr_l. intros; dec_tac. rewrite <- Rmult_assoc. split. apply Rplus_le_le_0_compat. autorewrite with real1; auto. fourier. autorewrite with real1; fourier. (*case : x = L::R.. *) inversion Hv1. match goal with id : represents (_::x2) _ |- _ => inversion id end. add_fact x2. constructor' ;[idtac | clear mult_correct_body]. match goal with |- represents _ ?a => replace a with (lift L r0 +(2*v2)*v3)%R end. apply mult_correct_body; clear mult_correct_body; auto. unfold lift, alpha; autorewrite with real1; dec_tac; fourier. clear mult_correct_body; unfold lift, alpha; field; auto with real1. match goal with |- (0 <= ?x <= 1)%R => replace x with (r0/2 + 2*v2*v3)%R end. dec_tac; split; fourier. unfold lift, alpha; field; auto with real1;fail. (* case : x = L::C.. *) inversion Hv1. match goal with id : represents (_::x2) _ |- _ => interval_from_represents id; intros; inversion id end. constructor';[idtac | clear mult_correct_body]. match goal with |- represents _ ?a => replace a with (r + 2*v2*v3)%R end. apply mult_correct_body; clear mult_correct_body; auto. subst r; unfold lift, alpha; autorewrite with real1. dec_tac; fourier. clear mult_correct_body; subst r; unfold lift, alpha; field; auto with real1. match goal with |- (0 <= ?a <= 1)%R => replace a with (r + 2*v2*v3)%R end. dec_tac; split; fourier. subst r; unfold lift, alpha; field; auto with real1. (* case x = R::.. *) inversion Hv1. assert (r+1+2*v2*v3 <= 2)%R. clear mult_correct_body. replace (r+1)%R with (2*v1)%R. rewrite Rmult_assoc. fourier. subst v1; unfold lift, alpha; field; auto with real1;fail. assert (r+2*v2*v3 <= 1)%R. clear mult_correct_body. fourier. constructor';[idtac | clear mult_correct_body]. match goal with |- represents _ ?a => replace a with (r + 2*v2*v3)%R end. apply mult_correct_body; clear mult_correct_body; auto. clear mult_correct_body. subst v1; unfold lift, alpha; field; auto with real1;fail. match goal with |- (0 <= ?a <= 1)%R => replace a with (r + 2*v2*v3)%R end. dec_tac; split; fourier. unfold lift, alpha; field; auto with real1. (* case x = C.. *) match goal with id : represents (C::_) _ |- _ => idtac | |- _ => fail "not the case x = C... as expected" end. destruct x1 as [ [ | | ] x2]. (* case x = C::L.. *) inversion Hv1. match goal with id : represents (L::x2) _ |- _ => intervals_from_represents Hv1 id end. constructor';[idtac | clear mult_correct_body]. match goal with |- represents _ ?a => replace a with (r + 2*v2*v3)%R end. apply mult_correct_body; clear mult_correct_body; auto. fourier. clear mult_correct_body; unfold lift, alpha; field; auto with real1;fail. match goal with |- (0 <= ?a <= 1)%R => replace a with (r + 2*v2*v3)%R end. dec_tac; unfold lift, alpha; autorewrite with real1; split; fourier. unfold lift, alpha; field; auto with real1;fail. (* case x= C::R.. *) match goal with id : represents (C::R::_) _ |- _ => idtac | |- _ => fail "not the case x = C::R... as expected" end. inversion Hv1. match goal with id : represents (_::x2) _ |- _ => inversion id end. add_fact x2. constructor';[idtac | clear mult_correct_body]. match goal with |- represents _ ?a => replace a with (lift L r0 + 2*v2*v3)%R end. apply mult_correct_body; clear mult_correct_body; auto. unfold lift, alpha; dec_tac; autorewrite with real1; fourier. unfold lift, alpha; field; auto with real1; fail. match goal with |- (0 <= ?a <= 1)%R => replace a with (r0/2 + 2*v2*v3)%R end. dec_tac; split; fourier. unfold lift, alpha; field; auto with real1; fail. (* case x = C::C.. *) inversion Hv1. match goal with id : represents (_::x2) _ |- _ => interval_from_represents id; intros; inversion id end. constructor';[idtac | clear mult_correct_body]. match goal with |- represents _ ?a => replace a with (r + 2*v2*v3)%R;[idtac | clear mult_correct_body] end. apply mult_correct_body; clear mult_correct_body; auto. unfold lift, alpha; autorewrite with real1; dec_tac; fourier. subst r; unfold lift, alpha; field; auto with real1; fail. match goal with |- (0 <= ?a <= 1)%R => replace a with (r + 2*v2*v3)%R end. dec_tac; unfold lift, alpha; autorewrite with real1; split; fourier. subst r; unfold lift, alpha; field; auto with real1. Defined. Ltac force_represents := match goal with id: represents ?x ?y |- represents ?x ?z => replace z with y;[assumption | unfold lift, alpha; field; auto with real1;fail] end. Theorem mult_a_correct : forall v1 v2 v3 x u u', (v3 <= 1/4)%R -> (v1 +v2*v3 <= 1)%R -> represents x v1 -> represents u v2 -> represents u' v3 -> represents (mult_a x (u, u')) (v1+v2*v3)%R. cofix. intros v1 v2 v3 x u u' Hv3lt Hsum Hv1 Hv2 Hv3. rewrite (str_dec_thm (mult_a x (u, u'))). lazy beta iota zeta delta [str_decompose mult_a]; fold mult_a. destruct u as [ [ | | ] u1]. fold (str_decompose (series_body (stream idigit * stream idigit) mult_a x (u1, u'))). rewrite <- str_dec_thm. apply mult_correct_body; (exact mult_a_correct || clear mult_a_correct); auto. inversion Hv2. force_represents. fold (str_decompose (series_body (stream idigit * stream idigit) mult_a (x + (L:: u')) (u1, u'))). rewrite <- str_dec_thm. inversion Hv2. match goal with |- represents _ ?a => replace a with ((v1+v3/2)+r/2*v3)%R; [idtac | clear mult_a_correct; unfold lift, alpha; field; auto with real1;fail] end. apply mult_correct_body; (exact mult_a_correct || clear mult_a_correct); auto. replace (v1 + v3/2 + r/2 *v3)%R with (v1 + v2*v3)%R; [assumption | subst v2; unfold lift, alpha; field; auto with real1;fail]. apply add_correct. assumption. constructor'. autorewrite with real1; assumption. interval_from_represents Hv3; autorewrite with real1; auto. apply Rle_trans with (2:= Hsum). apply Rplus_le_compat_l. replace (v3/2)%R with (1/2*v3)%R. apply Rmult_le_compat_r. interval_from_represents Hv3; intros; dec_tac; auto. subst v2; autorewrite with real1. dec_tac; unfold lift, alpha; autorewrite with real1; fourier. field; auto with real1;fail. force_represents. fold (str_decompose (series_body (stream idigit * stream idigit) mult_a (x + (L::L:: u')) (u1, u'))). rewrite <- str_dec_thm. inversion Hv2. match goal with |- represents _ ?a => replace a with ((v1+(v3/2/2))+r/2*v3)%R; [idtac | clear mult_a_correct; unfold lift, alpha; field; auto with real1;fail] end. apply mult_correct_body; (exact mult_a_correct || clear mult_a_correct);auto. replace (v1 + v3/2/2 + r/2 *v3)%R with (v1 + v2*v3)%R; [assumption | subst v2; unfold lift, alpha; field; auto with real1;fail]. apply add_correct. assumption. constructor'. constructor'. autorewrite with real1; assumption. interval_from_represents Hv3; autorewrite with real1; auto. interval_from_represents Hv3; intros; dec_tac; split; autorewrite with real1; fourier. apply Rle_trans with (2:= Hsum). apply Rplus_le_compat_l. replace (v3/2/2)%R with (1/4*v3)%R. apply Rmult_le_compat_r. interval_from_represents Hv3; intros; dec_tac; fourier. subst v2; autorewrite with real1. dec_tac; unfold lift, alpha; autorewrite with real1; fourier. field; auto with real1. force_represents. Qed. Theorem zero_correct : represents zero 0%R. cofix. rewrite (str_dec_thm zero); simpl. replace 0%R with (0/2)%R. constructor'. autorewrite with real1. apply zero_correct. clear zero_correct. split; fourier. clear zero_correct. unfold Rdiv; ring. Qed. Theorem mult_correct : forall x y vx vy, represents x vx -> represents y vy -> represents (x * y) (vx * vy). intros x y vx vy Hx Hy. replace (vx * vy)%R with (2*(2*(vx * (vy/2 /2))))%R. unfold mult. interval_from_represents Hx; interval_from_represents Hy; intros; dec_tac. assert (vx * (vy/2/2) <= 1/4)%R. replace (vy/2/2)%R with (1/4*vy)%R;[idtac|field;auto with real1;fail]. replace (1/4)%R with (1* (1/4*1))%R. apply Rmult_le_compat. assumption. repeat apply Rmult_le_pos. fourier. fourier. fourier. assumption. assumption. apply Rmult_le_compat. repeat apply Rmult_le_pos; fourier. assumption. rewrite Rmult_1_l; rewrite Rmult_1_r. auto with real;fail. assumption. ring. apply mult2_correct. split. repeat apply Rmult_le_pos; try fourier. auto with real1;fail. auto with real1;fail. apply mult2_correct. split. repeat apply Rmult_le_pos; try fourier. auto with real1;fail. auto with real1;fail. replace (vx * (vy / 2/2))%R with (0 + vx * (vy/2/2))%R;[idtac|ring]. apply mult_a_correct. replace (vy/2/2)%R with (1/4*vy)%R;[idtac | field; auto with real1]. fourier. fourier. apply zero_correct. assumption. constructor'. constructor'. autorewrite with real1; assumption. autorewrite with real1; auto with real1; fail. autorewrite with real1; auto with real1; fail. field; auto with real1; fail. Qed.