Require Import Rsequence_def.
Require Import Rsequence_facts.
Require Import Rseries_def.
Require Export Reals.
Require Import Fourier.

Open Local Scope Rseq_scope.

Ltac neq := fun n ⇒
  match goal with
    | id : (n ≠ 0)%R |- _ ⇒ constr: id
    | id : (n > 0) |- _ ⇒ constr: (Rgt_not_eq _ _ id)
    | id : (n < 0) |- _ ⇒ constr: (Rlt_not_eq _ _ id)
    | _ ⇒
      match constr:n with
      | Rabs ?a ⇒
        let H := neq a in constr: (Rabs_no_R0 _ H)
      end
  end.

Ltac rseq_fold Un := match constr:Un with
    | ?Vn ?c ?Wn ⇒ let Vn' := rseq_fold Vn in let Wn' := rseq_fold Wn in constr:(Vn' c Wn')
    | fun x : nat ⇒ ?Vn x ⇒ rseq_fold Vn
    | fun x : nat ⇒ (?Vn + ?Wn)%R ⇒ idtac "bla"
    
    | _ ⇒ constr:Un
end.

Ltac rseq_lim := fun Un ⇒ match goal with

    | id : Rseq_cv Un ?l |- _ ⇒ constr:id
    | id : Rseq_cv_pos_infty Un |- _ ⇒ constr:id
    | id : Rseq_cv_neg_infty Un |- _ ⇒ constr:id
    | _ ⇒

    match constr:Un with
      
      | (Rseq_constant ?a) ⇒ constr:(Rseq_constant_cv a)

      | (/ ?Vn) ⇒
        let H1 := rseq_lim Vn in
        match type of H1 with
          | Rseq_cv Vn ?l ⇒
            let H2 := neq l in
            constr:(Rseq_cv_inv_compat _ _ H1 H2)
          | Rseq_cv_pos_infty Vn ⇒
            constr:(Rseq_cv_pos_infty_inv_compat _ H1)
          | Rseq_cv_neg_infty Vn ⇒
            constr:(Rseq_cv_neg_infty_inv_compat _ H1) end

      | (?Vn/ ?Wn) ⇒
        let H1 := rseq_lim Vn in
        let H2 := rseq_lim Wn in
        match type of H1 with
          | Rseq_cv Vn ?lv ⇒ match type of H2 with
              | (Rseq_cv Wn ?lw) ⇒
                let H3 := neq lw in constr:(Rseq_cv_div_compat _ _ _ _ H1 H2 H3)
              | Rseq_cv_pos_infty Wn ⇒
                constr:(Rseq_cv_pos_infty_div_compat _ _ _ H2 H1)
              | Rseq_cv_neg_infty Wn ⇒
                constr:(Rseq_cv_neg_infty_div_compat _ _ _ H2 H1) end
          end

      | (- ?Vn) ⇒
        let H1 := rseq_lim Vn in
        match type of H1 with
          | Rseq_cv Vn ?l ⇒ constr:(Rseq_cv_opp_compat _ _ H1)
          | Rseq_cv_pos_infty Vn ⇒ constr:(Rseq_cv_pos_infty_opp_compat _ H1)
          | Rseq_cv_neg_infty Vn ⇒ constr:(Rseq_cv_neg_infty_opp_compat _ H1) end

      | (?Vn + ?Wn) ⇒
        let H1 := rseq_lim Vn in
        let H2 := rseq_lim Wn in
        match type of H1 with
          | Rseq_cv Vn ?lv ⇒ match type of H2 with
              | Rseq_cv _ ?lw ⇒ constr:(Rseq_cv_plus_compat _ _ _ _ H1 H2)
              | Rseq_cv_pos_infty _ ⇒ constr:(Rseq_cv_finite_plus_pos_infty_r _ _ _ H1 H2)
              | Rseq_cv_neg_infty _ ⇒ constr:(Rseq_cv_finite_plus_neg_infty_r _ _ _ H1 H2) end
          | Rseq_cv_pos_infty Vn ⇒ match type of H2 with
              | Rseq_cv _ ?lw ⇒ constr:(Rseq_cv_finite_plus_pos_infty_l _ _ _ H2 H1)
              | Rseq_cv_pos_infty _ ⇒ constr:(Rseq_cv_pos_infty_plus_compat _ _ H1 H2) end
              
          | Rseq_cv_neg_infty Vn ⇒ match type of H2 with
              | Rseq_cv _ ?lw ⇒ constr:(Rseq_cv_finite_plus_neg_infty_l _ _ _ H2 H1)
              | Rseq_cv_neg_infty _ ⇒ constr:(Rseq_cv_neg_infty_plus_compat _ _ H1 H2)
               end
              end

      | (?Vn - ?Wn) ⇒
        let H1 := rseq_lim Vn in
        let H2 := rseq_lim Wn in
        match type of H1 with
          | Rseq_cv Vn ?lv ⇒ match type of H2 with
              | (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_minus_compat _ _ _ _ H1 H2)
              | Rseq_cv_pos_infty Wn ⇒ constr:(Rseq_cv_finite_minus_pos_infty _ _ _ H1 H2)
              | Rseq_cv_neg_infty Wn ⇒ constr:(Rseq_cv_finite_plus_neg_infty_r _ _ _ H1 H2) end
          | Rseq_cv_pos_infty Vn ⇒ match type of H2 with
              | (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_finite_minus_pos_infty _ _ _ H2 H1)
              
              | Rseq_cv_neg_infty Wn ⇒ constr:(Rseq_cv_pos_minus_neg_infty _ _ H1 H2) end
          | Rseq_cv_neg_infty Vn ⇒ match type of H2 with
              | (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_finite_minus_neg_infty _ _ _ H2 H1)
              | Rseq_cv_pos_infty Wn ⇒ constr:(Rseq_cv_neg_minus_pos_infty _ _ H1 H2) end
              
              end

      | (?Vn × ?Wn) ⇒
        let H1 := rseq_lim Vn in
        let H2 := rseq_lim Wn in
        match type of H1 with
          | Rseq_cv Vn ?lv ⇒ match type of H2 with
              | (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_mult_compat _ _ _ _ H1 H2)
       end
          | Rseq_cv_pos_infty Vn ⇒ match type of H2 with

              | Rseq_cv_pos_infty Wn ⇒ constr:(Rseq_cv_pos_pos_infty_mult _ _ H1 H2)
              | Rseq_cv_neg_infty Wn ⇒ constr:(Rseq_cv_pos_neg_infty_mult _ _ H1 H2) end
          | Rseq_cv_neg_infty Vn ⇒ match type of H2 with

              | Rseq_cv_pos_infty Wn ⇒ constr:(Rseq_cv_neg_pos_infty_mult _ _ H1 H2) end
              | Rseq_cv_neg_infty Wn ⇒ constr:(Rseq_cv_neg_neg_infty_mult _ _ H1 H2)
              end


      | |?Vn| ⇒
        let H := rseq_lim Vn in fail





  end
end.

Ltac rser_lim := fun Un ⇒ match goal with
    | id : Rser_cv Un ?l |- _ ⇒ constr:id
    | id : Rser_cv_pos_infty Un |- _ ⇒ constr:id
    | id : Rser_cv_neg_infty Un |- _ ⇒ constr:id
    | _ ⇒ match constr:Un with
        | _ ⇒ idtac
 end
end.

Ltac rseq_cv_construct := intros; match goal with
    | |- {l | Rseq_cv ?Un l} ⇒
      let H := rseq_lim Un in
      match type of H with
        | Rseq_cv _ ?l ⇒ ∃ l ; apply H
      end
    | |- {l | Rser_cv ?Un l} ⇒
      let H := rser_lim Un in
      match type of H with
        | Rser_cv _ ?l ⇒ ∃ l ; apply H
      end
    | |- Rseq_cv ?Un ?l ⇒
      let H := rseq_lim Un in
      match type of H with
        | Rseq_cv _ ?l' ⇒ replace l with l' ; [apply H | subst; try reflexivity; try field; intuition]
      end
    | |- Rser_cv ?Un ?l ⇒
      let H := rser_lim Un in
      match type of H with
        | Rser_cv _ ?l' ⇒ replace l with l' ; [apply H | subst; try reflexivity; try field; intuition]
      end
    | |- Rseq_cv_pos_infty ?Un ⇒ let H := rseq_lim Un in apply H
    | |- Rseq_cv_neg_infty ?Un ⇒ let H := rseq_lim Un in apply H
end.