Require Export realbasis.
Require Export proof_utils.
Require Export real_facts.

Open Scope stream_scope.

Ltac apply_half_sum_correct hyp_id :=
 match goal with 
  id : represents ?x' ?u' , id1 : represents ?y' ?v' |- 
  represents (half_sum ?x' ?y') ?b =>
  replace b with ((u' + v')/2)%R;
    [apply hyp_id;assumption|field; auto with real1]
 end.

Ltac add_fact x :=
  match goal with id: represents (Cons ?d1 x) _, id1 : represents x ?v1
  |- context [Cons ?d2 x] =>
    let v := constr: (d2=d1) in
    match v with
      (?d = ?d) => interval_from_represents id; intros
    | (?d = _) => assert(represents (Cons d x) (lift d v1))
    end;[constructor; assumption | idtac]
  | id: represents (Cons ?d1 x) _ |- context [Cons ?d1 x] =>
      interval_from_represents id; intros
  | _ => idtac
  end.

Theorem half_sum_correct :
  forall x y u v,
    represents x u -> represents y v -> represents (half_sum x y) ((u + v)/2).
cofix.
intros; rewrite (str_dec_thm (half_sum x y)); simpl.
destruct x as [ [ | | ] x']; destruct y as [[ | | ] y'];
try (constructor'; 
      [inversion H; inversion H0;
       apply_half_sum_correct half_sum_correct; 
       clear half_sum_correct; unfold lift, alpha; field; auto with real1|
       clear half_sum_correct; intervals_from_represents H H0; 
       autorewrite with real1; auto with real1]);
destruct x' as [ [ | | ] x'']; inversion H;
try (inversion H0; inversion_to_variable x''; constructor';[add_fact x''; 
     apply_half_sum_correct half_sum_correct; 
     clear half_sum_correct; unfold lift, alpha; field; auto with real1|
     clear half_sum_correct; unfold lift, alpha; autorewrite with real1;
     dec_tac; split; fourier]);
destruct y' as [ [ | | ] y'']; inversion_to_variable y''; add_fact y'';
 inversion_to_variable x''; add_fact x'';
 try (constructor';[apply_half_sum_correct half_sum_correct;
                    clear half_sum_correct; unfold lift, alpha; field;
                    auto with real1|
                    clear half_sum_correct; unfold lift, alpha;
                    autorewrite with real1; dec_tac; split; fourier]).
Qed.

Theorem add_correct :
  forall x y u v, represents x u -> represents y v -> (u+v <= 1)%R ->
    represents (x + y)%S (u + v)%R.
intros x y u v H H0 H1; replace (u+v)%R with (2*((u+v)/2))%R.
unfold add.
apply mult2_correct.
rewrite half_plus_distr.
generalize (represents_interval _ _ H) (represents_interval _ _ H0); 
intros; dec_tac; auto with real1.
apply half_sum_correct; assumption.
field; auto with real1.
Qed.