Require Import Coq.Reals.Reals.

Require Import Automation.
Require Import Libs.Negation.
Require Import Notations.
Require Import Tactics.

Waterproof Enable Automation RealsAndIntegers.

Open Scope R_scope.

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

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

Declare Scope metric_scope.
Notation "a ⟶ c" := (convergence a c) (at level 20) : metric_scope.
Local Ltac2 unfold_convergence (statement : constr) := eval unfold convergence in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "⟶" x(opt(seq("in", constr))) :=
  wp_unfold unfold_convergence (Some "⟶") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "⟶" x(opt(seq("in", constr))) :=
  wp_unfold unfold_convergence (Some "⟶") false x.


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.
Ltac2 Notation "Expand" "the" "definition" "of" "converges" "to" x(opt(seq("in", constr))) :=
  wp_unfold unfold_convergence (Some "converges to") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "converges" "to" x(opt(seq("in", constr))) :=
  wp_unfold unfold_convergence (Some "converges to") false x.

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.