From Stdlib Require Import Reals.Reals.

Require Import Automation.
Require Import Libs.Negation.
Require Import Notations.Common.
Require Import Notations.Reals.
Require Import Notations.Sets.
Require Import Chains.
Require Import Tactics.

Waterproof Enable Automation RealsAndIntegers.

Open Scope R_scope.
Open Scope subset_scope.

Definition convergence {M : Metric_Space}
                       (a : ℕ → Base M)
                       (c : Base M) :=
  ∀ ε > 0,
    ∃ N1 ∈ ℕ, (∀ n ≥ N1,
      (dist M (a n) c < ε)%R)%nat.

Definition bounded {X : Metric_Space} (a : ℕ → Base X) :=
  ∃ q ∈ Base X,
    ∃ M > 0,
      ∀ n ∈ ℕ, dist X (a n) q ≤ M.

Declare Scope metric_scope.
Notation "a ⟶ c" := (convergence a c) (at level 20) : metric_scope.

Waterproof Disable Filter Errors.

Waterproof Register Expand "⟶";
  for convergence;
  as "Definition convergence".


Notation "a '_converges' 'to_' p" := (convergence a p) (at level 68) : metric_scope.
Notation "a 'converges' 'to' p" := (convergence a p) (at level 68, only parsing) : metric_scope.

Waterproof Register Expand "converges" "to";
  for convergence;
  as "Definition convergence".

Lemma relation_shift {X : Metric_Space} (a : nat -> Base X) (k : nat) (n : nat) (n_ge_k : (n ≥ k)%nat) :
  a ((n - k) + k)%nat = a n.
Proof.
We conclude that (a (n - k + k) = a n)%nat.
Qed.

#[export] Hint Resolve relation_shift : wp_integers.
#[export] Hint Extern 1 (_ = _) => (rewrite relation_shift) : wp_integers.

Close Scope R_scope.