Library Coqtail.Fresh.Reals.Rseq

Require Import Raxiom Rconvenient Repsilon.
Require Import ZArith.

Module Rsequence (Import T : CReals).
  Module Rconvenient := (Rconvenient T). Import Rconvenient.
  Module Repsilon := (Repsilon T). Import Repsilon.
  Open Scope R_scope.

  Definition Rseq := nat → R.

  Definition Rseq_add (a b : Rseq) : Rseq := fun n ⇒ a n + b n.
  Definition Rseq_mul (a b : Rseq) : Rseq := fun n ⇒ a n × b n.
  Definition Rseq_sub (a b : Rseq) : Rseq := fun n ⇒ a n - b n.
  Definition Rseq_opp (a : Rseq) : Rseq := fun n ⇒ - a n.

  Lemma Rseq_cv_unique : ∀ u l l',
    Rseq_cv u l → Rseq_cv u l' → l == l'.
  Proof.
    intros u l l' Cu Cu'.
    apply Rsub_lt_pos_eq; intros e epos.
    destruct (halfpos e epos) as (e', (e'pos, ee')).
    destruct (Cu e' e'pos) as (N, HN).
    destruct (Cu' e' e'pos) as (N', HN').
    pose (n := plus N N').
    destruct (HN n (le_plus_l _ _)) as (ule, eul).
    destruct (HN' n (le_plus_r _ _)) as (ul'e, eul').
    split.
      apply Rlt_trans with (u n + e' - l').
        apply Radd_lt_cancel_r with (l' - l - e').
        apply (Req_lt_compat (- e') (u n - l)); auto; ring_simplify; reflexivity.
        apply Req_lt_compat_r with (u n + e' - (u n - e')).
          rewrite ee'; ring.

          apply Radd_lt_cancel_r with (- e').
          apply (Req_lt_compat (u n - l') e'); auto; ring_simplify; reflexivity.

      apply Rlt_trans with (u n + e' - l).
        apply Radd_lt_cancel_r with (l - l' - e').
        apply (Req_lt_compat (- e') (u n - l')); auto; ring_simplify; reflexivity.

        apply Req_lt_compat_r with (u n + e' - (u n - e')).
          rewrite ee'; ring.

          apply Radd_lt_cancel_r with (- e').
          apply (Req_lt_compat (u n - l) e'); auto; ring_simplify; reflexivity.
  Qed.

  Lemma Rseq_add_cv_compat : ∀ u v lu lv,
    Rseq_cv u lu → Rseq_cv v lv → Rseq_cv (Rseq_add u v) (lu + lv).
  Proof.
    intros u v lu lv Hu Hv e epos.
    destruct (halfpos e epos) as (e', (e'pos, ee')).
    destruct (Hu e' e'pos) as (Nu, HNu).
    destruct (Hv e' e'pos) as (Nv, HNv).
    pose (N := plus Nu Nv).
    ∃ N; intros n Hn.
    unfold Rdist; unfold Rseq_add.
    split.
      apply (Req_lt_compat ((u n - lu) + (v n - lv)) (e' + e')).
        ring_simplify; reflexivity.
        rewrite ee'; reflexivity.
        apply Radd_lt_compat; apply HNu || apply HNv; unfold N in *; omega.
      apply (Req_lt_compat (- e' - e') ((u n - lu) + (v n - lv))).
        rewrite ee'; ring_simplify; reflexivity.
        ring_simplify; reflexivity.
        apply Radd_lt_compat; apply HNu || apply HNv; unfold N in *; omega.
  Qed.

  Lemma Rseq_opp_cv_compat : ∀ u l,
    Rseq_cv u l → Rseq_cv (Rseq_opp u) (- l).
  Proof.
    intros u l C.
    intros e ep; destruct (C e ep) as (N, HN); ∃ N; intros n Hn.
    destruct (HN n Hn) as (A, B); unfold Rdist, Rseq_opp.
    split; apply Ropp_lt_contravar_reciprocal; eapply Req_lt_compat;
      [ | | apply B | | | apply A ]; ring_simplify; reflexivity.
  Qed.

End Rsequence.