Require Import Utf8.
Require Import Core.

Class real_like_prop T {ro : ring_like_op T} {rp : ring_like_prop T} :=
  { rl_nth_root : nat → T → T;
    rl_nth_root_pow : ∀ n a, (0 ≤ a → rl_nth_root n a ^ n = a)%L;
    rl_nth_root_mul :
      ∀ n a b, (0 ≤ a)%L → (0 ≤ b)%L →
      (rl_nth_root n (a × b) = rl_nth_root n a × rl_nth_root n b)%L;
    rl_nth_root_inv :
      ∀ n a, (0 < a → rl_nth_root n a⁻¹ = (rl_nth_root n a)⁻¹)%L;
    rl_sqrt_nonneg : ∀ a, (0 ≤ a → 0 ≤ rl_nth_root 2 a)%L }.

Section a.

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

Definition rl_sqrt a := rl_nth_root 2 a.

End a.

Arguments rl_sqrt {T ro rp rl} a%_L.
Notation "'√' a" := (rl_sqrt a) (at level 2, format "√ a").

Section a.

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

Theorem rngl_squ_sqrt :
  ∀ a, (0 ≤ a)%L → rngl_squ (√a) = a.

Theorem rngl_abs_sqrt :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 ≤ a)%L → rngl_abs (√a) = (√a)%L.

Theorem rl_sqrt_mul :
  ∀ a b,
  (0 ≤ a)%L
  → (0 ≤ b)%L
  → rl_sqrt (a × b)%L = (rl_sqrt a × rl_sqrt b)%L.

Theorem rl_sqrt_div :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (0 ≤ a)%L → (0 < b)%L → (√(a / b) = √a / √b)%L.

Theorem rl_sqrt_squ :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a, (√a²)%L = rngl_abs a.
Theorem rl_sqrt_0 :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  (rngl_is_integral_domain T || rngl_has_inv_or_pdiv T)%bool = true →
  rl_sqrt 0%L = 0%L.

Theorem eq_rl_sqrt_0 :
  rngl_has_opp_or_psub T = true →
  ∀ a, (0 ≤ a)%L → rl_sqrt a = 0%L → a = 0%L.

Definition rl_modl x y := (√(x² + y²))%L.

Theorem fold_rl_modl : ∀ x y, √(x² + y²) = rl_modl x y.

Theorem rl_modl_add_le :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b c d, (rl_modl (a + c) (b + d) ≤ rl_modl a b + rl_modl c d)%L.

Theorem euclidean_distance_triangular :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_totally_ordered T = true →
  ∀ x1 y1 x2 y2 x3 y3,
  (rl_modl (x3 - x1) (y3 - y1)
   ≤ rl_modl (x2 - x1) (y2 - y1) + rl_modl (x3 - x2) (y3 - y2))%L.

Theorem rl_sqrt_le_rl_sqrt :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b,
  (0 ≤ a)%L
  → (a ≤ b)%L
  → (√ a ≤ √ b)%L.

Theorem rl_sqrt_lt_rl_sqrt :
  rngl_is_totally_ordered T = true →
  ∀ a b,
  (0 ≤ a)%L
  → (a < b)%L
  → (√ a < √ b)%L.

Theorem rl_sqrt_pos :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 < a)%L → (0 < √a)%L.

Theorem rl_sqrt_1 :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_totally_ordered T = true →
  rl_sqrt 1%L = 1%L.

End a.

Arguments rl_modl {T ro rp rl} (x y)%_L.