Require Import Reals Lra Field List Lia Classical Utf8.
Set Implicit Arguments.
Open Scope R.

Fixpoint type_pow (n: nat) (x: Set): Set :=
  match n with
  | O => unit
  | 1 => x
  | S m => prod (type_pow m x) x
  end.
Notation "x ^ n" := (type_pow n x).

Definition vector_mult {n} (k: R) (x: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (k * x).
  + destruct x as [tx x]. exact (IHn tx, k * x).
Defined.

Definition vector_sum {n} (x y: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (x + y).
  + destruct x as [tx x], y as [ty y]. exact (IHn tx ty, x + y).
Defined.

Definition vector_difference {n} (x y: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (x - y).
  + destruct x as [tx x], y as [ty y]. exact (IHn tx ty, x - y).
Defined.

Definition elementwise_product {n} (x y: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (x * y).
  + destruct x as [tx x], y as [ty y]. exact (IHn tx ty, x * y).
Defined.

Definition vector_element_sum {n} (x: R^(S n)): R.
Proof.
  induction n.
  + exact x.
  + destruct x as [tx x]. exact (IHn tx + x).
Defined.

Definition scalar_mult {n} (x y: R^(S n)): R := vector_element_sum (elementwise_product x y).
Definition scalar_mult_S {n} (tx ty: R^(S n)) (x y: R): @scalar_mult (S n) (tx, x) (ty, y) = scalar_mult tx ty + x * y.
Proof.
  reflexivity.
Qed.

Definition squared_length {n} (x: R^(S n)): R := scalar_mult x x.
Definition squared_length_S {n} (tx: R^(S n)) (x: R): @squared_length (S n) (tx, x) = squared_length tx + x * x.
Proof.
  reflexivity.
Qed.

Definition squared_length_nonneg {n} (x: R^(S n)): 0 <= squared_length x.
Proof.
  induction n.
  + apply Rle_0_sqr.
  + destruct x as [tx x]. rewrite squared_length_S. pose proof (IHn tx). pose proof (Rle_0_sqr x). unfold Rsqr in H0. lra.
Qed.

Definition length {n} (x: R^(S n)): R :=
  Rsqrt (mknonnegreal _ (squared_length_nonneg x)).

Theorem squared_length_thm {n} (x: R^(S n)): squared_length x = length x * length x.
Proof.
  unfold length. rewrite Rsqrt_Rsqrt. simpl. auto.
Qed.

Theorem length_nonneg {n} (x: R^(S n)): 0 <= length x.
Proof.
  apply Rsqrt_positivity.
Qed.

Definition distance {n} (x y: R^(S n)): R := length (vector_difference x y).

Theorem distance_nonneg {n} (x y: R^(S n)): 0 <= distance x y.
Proof.
  apply Rsqrt_positivity.
Qed.

Theorem Rsqrt_of_square (x: R) (H: 0 <= x * x): Rsqrt (mknonnegreal (x * x) H) = Rabs x.
Proof.
  apply Rsqr_inj.
  + apply Rsqrt_positivity.
  + unfold Rabs. destruct Rcase_abs; lra.
  + unfold Rsqr. rewrite Rsqrt_Rsqrt. simpl. apply Rsqr_abs.
Qed.

Theorem Rsqrt_eq_zero_iff (x: R) (H: 0 <= x): Rsqrt (mknonnegreal x H) = 0 ↔ x = 0.
Proof.
  split; intros.
  + pose (Rsqrt_Rsqrt (mknonnegreal x H)). rewrite H0 in e. simpl in e. lra.
  + assert (x = 0 * 0) by (unfold Rsqr; lra). clear H0. subst. rewrite Rsqrt_of_square.
    unfold Rabs. destruct Rcase_abs; lra.
Qed.

Theorem distance_zero_iff {n: nat} (x y: R^(S n)): distance x y = 0 ↔ x = y.
Proof.
  split; intros.
  + induction n.
    - apply Rsqrt_eq_zero_iff in H. apply Rsqr_0_uniq in H. simpl in H. lra.
    - destruct x as [tx x], y as [ty y]. apply Rsqrt_eq_zero_iff in H.
      simpl in H. try rewrite squared_length_S in H.
Admitted.