Require Export realbasis. Require Export proof_utils. Definition str_decompose (A:Set)(x:stream A) := match x with Cons a tl => Cons a tl end. Implicit Arguments str_decompose. Theorem str_dec_thm : forall A:Set, forall x : stream A, x = str_decompose x. intros; case x; auto. Qed. Implicit Arguments str_dec_thm. Theorem R_interval : forall x y, represents (Cons R x) y -> (1/2 <= y <= 1)%R. intros; inversion H; unfold lift, alpha. rewrite half_plus_distr. dec_tac; auto with real1. Qed. Theorem L_interval : forall x y, represents (Cons L x) y -> (0 <= y <= 1/2)%R. intros; inversion H; unfold lift, alpha; dec_tac; auto with real1. Qed. Theorem C_interval : forall x y, represents (Cons C x) y -> (1/4 <= y <= 3/4)%R. intros; inversion H; unfold lift, alpha; dec_tac. rewrite half_plus_distr; auto with real1. Qed. Theorem represents_interval : forall x r, represents x r -> (0 <= r <= 1)%R. intros x r H; destruct x as [ [ | | ] x']; [generalize (L_interval _ _ H) | generalize (R_interval _ _ H) | generalize (C_interval _ _ H)]; intros; dec_tac; auto with real1. Qed. Open Scope R_scope. Definition anti_lift (d:idigit)(x:Rdefinitions.R) := match d with R => 2*x-1 | L => 2*x | C => 2*x-1/2 end. Theorem lift_anti_lift : forall d x, lift d (anti_lift d x) = x. intros; unfold lift, alpha, anti_lift; case d; field; auto with real1. Qed. Close Scope R_scope. Ltac prepare_represents_constructor := match goal with |- represents (Cons R ?a) (?b/2) => replace b with ((b - 1)+1)%R;[idtac | field ; auto with real1] | |- represents (Cons L ?a) (?b/2) => idtac | |- represents (Cons C ?a) (?b/2) => replace (b/2)%R with ((2*(b - 1/2)+1)/4)%R; [idtac | field; auto with real1] | |- _ => idtac end. Ltac interval_from_represents H := (generalize (R_interval _ _ H) || generalize (L_interval _ _ H) || generalize (C_interval _ _ H) || generalize (represents_interval _ _ H)). Ltac intervals_from_represents H H0 := interval_from_represents H; interval_from_represents H0; intros; dec_tac. Ltac inversion_to_variable x := match goal with | id : represents x _ |- _ => idtac | id : represents (Cons ?d x) _ |- context [Cons ?d x] => idtac | id : represents (Cons ?d1 x) _ |- context [Cons ?d2 x] => inversion id | id : represents (Cons ?d1 (Cons ?d2 x)) _ |- context [ Cons ?d3 x] => inversion id; inversion_to_variable x end. Ltac constructor' := match goal with |- represents (?d::_) ?v => rewrite <- (lift_anti_lift d v); unfold anti_lift; constructor end. Theorem represents_one : represents one 1%R. cofix. rewrite (str_dec_thm one); simpl. constructor'. replace (2*1-1)%R with 1%R. assumption. clear represents_one; ring. clear represents_one; split; fourier. Qed. Theorem mult2_correct : forall x u, (0 <= u <= 1/2)%R -> represents x u -> represents (mult2 x) (2*u)%R. cofix. intros. inversion H0. destruct d. clear mult2_correct. rewrite (str_dec_thm (mult2 (L::s))); simpl. unfold lift, alpha; replace (2*((r+0)/2))%R with r;[idtac|field; auto with real1]. generalize H1; case s; auto. clear mult2_correct. unfold lift,alpha in H4; rewrite half_plus_distr in H4. dec_tac. subst u. assert (r <= 0)%R. fourier. rewrite (str_dec_thm (mult2 (R::s))); simpl. change (R::one) with (str_decompose one). unfold lift, alpha. rewrite <- str_dec_thm; replace (2*((r+1)/2))%R with 1%R. apply represents_one. assert (Hr:(r=0)%R). apply Rle_antisym;assumption. rewrite Hr; field; auto with real1. rewrite (str_dec_thm (mult2 (C::s))); simpl. constructor';[idtac | clear mult2_correct]. match goal with |- represents _ ?x => replace x with (2 * r)%R; [idtac | clear mult2_correct; field; auto with real1] end. apply mult2_correct;clear mult2_correct. dec_tac. split. assumption. unfold lift, alpha in H4. replace r with (2*u -1/2)%R. fourier. subst u; field; auto with real1. assumption. unfold lift, alpha. field; auto with real1. split. replace (2*(2*lift C r))%R with (2*r+1)%R. dec_tac; fourier. unfold lift, alpha; field; auto with real1. rewrite H4; dec_tac. rewrite <- Rmult_assoc; fourier. Qed. Theorem rat_to_stream_correct : forall a b, 0 <= a <= b -> 0 < b -> represents (rat_to_stream a b) (IZR a/IZR b). cofix. intros a b Hdom Hden. rewrite (str_dec_thm (rat_to_stream a b)); unfold str_decompose, rat_to_stream; fold rat_to_stream. destruct (Z_le_gt_dec (2*a) b) as [Hle | Hgt]. constructor'. 2:clear rat_to_stream_correct. replace (2* (IZR a / IZR b))%R with (IZR (2*a)/IZR b)%R. apply rat_to_stream_correct; clear rat_to_stream_correct. omega. assumption. rewrite mult_IZR; simpl IZR; unfold Rdiv;ring. split; apply Rmult_le_reg_l with (IZR b). apply (IZR_lt 0);assumption. rewrite Rmult_0_r. match goal with |- (_ <= ?x)%R => replace x with (IZR (2 * a)) end. apply (IZR_le 0); omega. rewrite mult_IZR; simpl IZR; field. apply not_O_IZR. omega. apply (IZR_lt 0);assumption. match goal with |- (?x <= _)%R => replace x with (IZR (2 * a)) end. rewrite Rmult_1_r. apply IZR_le;assumption. rewrite mult_IZR; simpl IZR; field. apply not_O_IZR. omega. constructor'. replace (2*(IZR a/IZR b)-1)%R with (IZR (2*a -b)/IZR b)%R. apply rat_to_stream_correct;clear rat_to_stream_correct. omega. assumption. rewrite <- Z_R_minus; rewrite mult_IZR; simpl IZR; field. apply not_O_IZR. omega. replace (2*(IZR a / IZR b) -1)%R with (IZR (2* a -b)/IZR b)%R. split. unfold Rdiv; apply Rle_mult_inv_pos. apply (IZR_le 0). omega. apply (IZR_lt 0);assumption. apply Rmult_le_reg_l with (IZR b). apply (IZR_lt 0);assumption. rewrite Rmult_1_r. match goal with |- (?x <= _)%R => replace x with (IZR (2 * a - b)) end. apply IZR_le. omega. rewrite <- Z_R_minus; rewrite mult_IZR; simpl IZR; field. apply not_O_IZR. omega. rewrite <- Z_R_minus; rewrite mult_IZR; simpl IZR; field. apply not_O_IZR. omega. Qed.