Require Import RingLike.Core.

From Stdlib Require Import Utf8 Arith.

Require Import Structures.
Require Import Order.
Require Import Add.
Require Import Mul.
Require Import Div.
Require Import Add_with_order.
Require Import Mul_with_order.
Require Import Div_with_order.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.

Record is_dist {A} (da : A → A → T) :=
  { dist_symmetry : ∀ a b, da a b = da b a;
    dist_separation : ∀ a b, da a b = 0%L ↔ a = b;
    dist_triangular : ∀ a b c, (da a c ≤ da a b + da b c)%L }.

Class distance A :=
  { d_dist : A → A → T;
    d_prop : is_dist d_dist }.

End a.

Arguments d_dist {T ro A distance} a b.
Arguments dist_separation {T ro A da} dist a b : rename.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.

Definition rngl_dist a b := rngl_abs (a - b)%L.

Theorem rngl_dist_is_dist :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  is_dist rngl_dist.
Definition rngl_distance Hop Hor :=
  {| d_dist := rngl_dist; d_prop := rngl_dist_is_dist Hop Hor |}.

Definition is_limit_when_seq_tends_to_inf {A} (da : A → A → T) u L :=
  ∀ ε, (0 < ε)%L → ∃ N, ∀ n, N ≤ n → (da (u n) L < ε)%L.

Definition is_limit_when_tending_to_neighbourhood (is_left : bool) {A B}
  (lt : A → A → Prop)
  (da : A → A → T) (db : B → B → T) (f : A → B) (x₀ : A) (L : B) :=
  (∀ ε : T, 0 < ε →
   ∃ η : T, (0 < η)%L ∧ ∀ x : A,
   (if is_left then lt x x₀ else lt x₀ x)
   → da x x₀ < η
   → db (f x) L < ε)%L.

Definition is_Cauchy_sequence {A} (da : A → A → T) (u : nat → A) :=
  ∀ ε : T, (0 < ε)%L →
  ∃ N : nat, ∀ p q : nat, N ≤ p → N ≤ q → (da (u p) (u q) < ε)%L.

Definition is_complete A (da : A → A → T) :=
  ∀ u, is_Cauchy_sequence da u
  → ∃ c, is_limit_when_seq_tends_to_inf da u c.

Definition left_or_right_continuous_at (is_left : bool) {A B} le
    da db (f : A → B) a :=
  is_limit_when_tending_to_neighbourhood is_left le da db f a (f a).

Definition left_continuous_at {A B} :=
  @left_or_right_continuous_at true A B.
Definition right_continuous_at {A B} :=
  @left_or_right_continuous_at false A B.

Definition is_continuous {A B} lt da db (f : A → B) :=
  ∀ a, left_continuous_at lt da db f a ∧ right_continuous_at lt da db f a.

Definition left_or_right_derivative_at (is_left : bool) {A} lt
    (da : A → A → T) (db : T → T → T) f a a' :=
  let σ := (if is_left then 1 else -1)%L in
  let g x := (σ × (f a - f x) / da x a)%L in
  is_limit_when_tending_to_neighbourhood is_left lt da db g a a'.

Definition left_derivative_at {A} := @left_or_right_derivative_at true A.
Definition right_derivative_at {A} := @left_or_right_derivative_at false A.

Definition is_derivative_at {A} lt
  (da : A → A → T) (db : T → T → T) f f' a :=
  let le x y := lt x y ∨ x = y in
  left_continuous_at le da db f a ∧
  right_continuous_at le da db f a ∧
  left_derivative_at lt da db f a (f' a) ∧
  right_derivative_at lt da db f a (f' a).

Definition is_derivative {A} lt (da : A → A → T) (db : T → T → T) f f' :=
  ∀ a, is_derivative_at lt da db f f' a.

Theorem dist_refl :
  ∀ A (dist : A → A → T) (Hid : is_dist dist) a, dist a a = 0%L.

Theorem dist_diag : ∀ {A} {da : A → A → T} (dist : is_dist da) a,
  da a a = 0%L.

Theorem dist_nonneg :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ {A} {da : A → A → T} (dist : is_dist da) a b, (0 ≤ da a b)%L.

Theorem rngl_limit_interv :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ {dt : T → T → T} (dist : is_dist dt),
  (∀ x y z, (x ≤ y ≤ z → dt x y ≤ dt x z)%L)
  → (∀ x y z, (x ≤ y ≤ z → dt y z ≤ dt x z)%L)
  → ∀ u a b c,
  (∀ i, (a ≤ u i ≤ b)%L)
  → is_limit_when_seq_tends_to_inf dt u c
  → (a ≤ c ≤ b)%L.
Theorem limit_unique :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ {A} {da : A → A → T} (dist : is_dist da) u lim1 lim2,
  is_limit_when_seq_tends_to_inf da u lim1
  → is_limit_when_seq_tends_to_inf da u lim2
  → lim1 = lim2.

Theorem limit_add :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ {dt : T → T → T} (dist : is_dist dt),
  (∀ a b c d, (dt (a + b) (c + d) ≤ dt a c + dt b d)%L)
  → ∀ u v limu limv,
  is_limit_when_seq_tends_to_inf dt u limu
  → is_limit_when_seq_tends_to_inf dt v limv
  → is_limit_when_seq_tends_to_inf dt (λ n, (u n + v n))%L (limu + limv)%L.

Theorem rngl_dist_add_add_le :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c d,
  (rngl_dist (a + b) (c + d) ≤ rngl_dist a c + rngl_dist b d)%L.

Theorem rngl_dist_left_mono :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c,
  (a ≤ b ≤ c)%L
  → (rngl_dist a b ≤ rngl_dist a c)%L.

Theorem rngl_dist_right_mono :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c,
  (a ≤ b ≤ c)%L
  → (rngl_dist b c ≤ rngl_dist a c)%L.

Theorem is_limit_neighbourhood_eq_compat :
  ∀ is_left {A B} (f g : A → B) lt₁ lt₂ da db a u,
  (∀ x, f x = g x)
  → (∀ x y, lt₂ x y → lt₁ x y)
  → is_limit_when_tending_to_neighbourhood is_left lt₁ da db f a u
  → is_limit_when_tending_to_neighbourhood is_left lt₂ da db g a u.

Theorem is_derivative_at_eq_compat :
  ∀ {A} (f f' g g' : A → T) lt da db a,
  (∀ x, f x = g x)
  → (∀ x, f' x = g' x)
  → is_derivative_at lt da db f f' a
  → is_derivative_at lt da db g g' a.
End a.

Arguments rngl_dist {T ro} (a b)%_L.