Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.PathGroupoids.Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.PathGroupoids.
Require Import Types.Sigma.
Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring Algebra.Rings.Module.
Require Import Spaces.Nat.Core.
Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths.
Require Import abstract_algebra.

Local Open Scope mc_scope.

Local Set Universe Minimization ToSet.
Local Set Polymorphic Inductive Cumulativity.

(** * Vectors *)

(** A vector is simply a list with a specified length. This data structure has many uses, but here we will focus on lists of left module elements. *)

(** ** Definition *)

Definition Vector@{i|} (A : Type@{i}) (n : nat) : Type@{i}
  := { l : list A & length l = n }.

(** *** Constructors *)

Definition Build_Vector (A : Type) (n : nat)
  (f : forall (i : nat), (i < n)%nat -> A)
  : Vector A n
  := (Build_list n f; length_Build_list n f).

(** *** Projections *)

Definition entry {A : Type} {n : nat} (v : Vector A n) i {Hi : (i < n)%nat} : A
  := nth' (pr1 v) i ((pr2 v)^ # Hi).

(** *** Basic properties *)

Definition entry_Build_Vector {A : Type} {n}
  (f : forall (i : nat), (i < n)%nat -> A) i {Hi : (i < n)%nat}
  : entry (Build_Vector A n f) i = f i Hi.
A: Type
n: nat
f: forall i0 : nat, (i0 < n)%nat -> A
i: nat
Hi: (i < n)%nat
entry (Build_Vector A n f) i = f i Hi
Proof.
A: Type
n: nat
f: forall i0 : nat, (i0 < n)%nat -> A
i: nat
Hi: (i < n)%nat
entry (Build_Vector A n f) i = f i Hi
  snapply nth'_Build_list.
Defined.

Instance istrunc_vector@{i} (A : Type@{i}) (n : nat) k `{IsTrunc k.+2 A}
  : IsTrunc k.+2 (Vector A n).
A: Type
n: nat
k: trunc_index
IsTrunc0: IsTrunc k.+2 A
IsTrunc k.+2 (Vector A n)
Proof.
A: Type
n: nat
k: trunc_index
IsTrunc0: IsTrunc k.+2 A
IsTrunc k.+2 (Vector A n)
  rapply istrunc_sigma@{i i i}.
Defined.

Definition path_vector@{i} (A : Type@{i}) {n : nat} (v1 v2 : Vector@{i} A n)
  (H : forall i (H : (i < n)%nat), entry v1 i = entry v2 i)
  : v1 = v2.
A: Type
n: nat
v1, v2: Vector A n
H: forall (i : nat) (H0 : (i < n)%nat), entry v1 i = entry v2 i
v1 = v2
Proof.
A: Type
n: nat
v1, v2: Vector A n
H: forall (i : nat) (H0 : (i < n)%nat), entry v1 i = entry v2 i
v1 = v2
  rapply path_sigma_hprop@{i i i}.
A: Type
n: nat
v1, v2: Vector A n
H: forall (i : nat) (H0 : (i < n)%nat), entry v1 i = entry v2 i
v1.1 = v2.1
  snapply path_list_nth'.
A: Type
n: nat
v1, v2: Vector A n
H: forall (i : nat) (H0 : (i < n)%nat), entry v1 i = entry v2 i
length v1.1 = length v2.1
A: Type
n: nat
v1, v2: Vector A n
H: forall (i : nat) (H0 : (i < n)%nat), entry v1 i = entry v2 i
forall (n0 : nat) (H0 : (n0 < length v1.1)%nat),
nth' v1.1 n0 H0 = nth' v2.1 n0 (transport (Core.lt n0) ?p H0)
  1: exact (pr2 v1 @ (pr2 v2)^).
A: Type
n: nat
v1, v2: Vector A n
H: forall (i : nat) (H0 : (i < n)%nat), entry v1 i = entry v2 i
forall (n0 : nat) (H0 : (n0 < length v1.1)%nat),
nth' v1.1 n0 H0 = nth' v2.1 n0 (transport (Core.lt n0) (v1.2 @ (v2.2)^) H0)
  intros i Hi.
A: Type
n: nat
v1, v2: Vector A n
H: forall (i0 : nat) (H0 : (i0 < n)%nat), entry v1 i0 = entry v2 i0
i: nat
Hi: (i < length v1.1)%nat
nth' v1.1 i Hi = nth' v2.1 i (transport (Core.lt i) (v1.2 @ (v2.2)^) Hi)
  snrefine (_ @ H i (pr2 v1 # Hi) @ _).
A: Type
n: nat
v1, v2: Vector A n
H: forall (i0 : nat) (H0 : (i0 < n)%nat), entry v1 i0 = entry v2 i0
i: nat
Hi: (i < length v1.1)%nat
nth' v1.1 i Hi = entry v1 i
A: Type
n: nat
v1, v2: Vector A n
H: forall (i0 : nat) (H0 : (i0 < n)%nat), entry v1 i0 = entry v2 i0
i: nat
Hi: (i < length v1.1)%nat
entry v2 i = nth' v2.1 i (transport (Core.lt i) (v1.2 @ (v2.2)^) Hi)
  1, 2: apply nth'_nth'.
Defined.

Definition path_entry_vector {A : Type} {n : nat} (v : Vector A n)
  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) (p : i = j)
  : entry v i = entry v j.
A: Type
n: nat
v: Vector A n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
p: i = j
entry v i = entry v j
Proof.
A: Type
n: nat
v: Vector A n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
p: i = j
entry v i = entry v j
  destruct p.
A: Type
n: nat
v: Vector A n
i: nat
Hi, Hj: (i < n)%nat
entry v i = entry v i
  apply nth'_nth'.
Defined.

(** ** Operations *)

Definition vector_map {A B : Type} {n} (f : A -> B)
  : Vector A n -> Vector B n
  := fun v => Build_Vector B n (fun i _ => f (entry v i)).

Definition vector_map2 {A B C : Type} {n} (f : A -> B -> C)
  : Vector A n -> Vector B n -> Vector C n
  := fun v1 v2 => Build_Vector C n (fun i _ => f (entry v1 i) (entry v2 i)).

(** ** Abelian group structure *)

Section VectorAddition.

  Context (A : AbGroup) (n : nat).

  Definition vector_plus : Plus (Vector A n) := vector_map2 (+).

  Definition vector_zero : Zero (Vector A n)
    := Build_Vector A n (fun _ _ => 0).

  Definition vector_neg : Negate (Vector A n) := vector_map (-).

  Definition associative_vector_plus : Associative vector_plus.
A: AbGroup
n: nat
Associative vector_plus
  Proof.
A: AbGroup
n: nat
Associative vector_plus
    intros v1 v2 v3; apply path_vector; intros i Hi.
A: AbGroup
n: nat
v1, v2, v3: Vector A n
i: nat
Hi: (i < n)%nat
entry (vector_plus v1 (vector_plus v2 v3)) i =
entry (vector_plus (vector_plus v1 v2) v3) i
    rewrite 4 entry_Build_Vector.
A: AbGroup
n: nat
v1, v2, v3: Vector A n
i: nat
Hi: (i < n)%nat
entry v1 i + (entry v2 i + entry v3 i) = entry v1 i + entry v2 i + entry v3 i
    apply associativity.
  Defined.
  
  Definition commutative_vector_plus : Commutative vector_plus.
A: AbGroup
n: nat
Commutative vector_plus
  Proof.
A: AbGroup
n: nat
Commutative vector_plus
    intros v1 v2; apply path_vector; intros i Hi.
A: AbGroup
n: nat
v1, v2: Vector A n
i: nat
Hi: (i < n)%nat
entry (vector_plus v1 v2) i = entry (vector_plus v2 v1) i
    rewrite 2 entry_Build_Vector.
A: AbGroup
n: nat
v1, v2: Vector A n
i: nat
Hi: (i < n)%nat
entry v1 i + entry v2 i = entry v2 i + entry v1 i
    apply commutativity.
  Defined.

  Definition left_identity_vector_plus : LeftIdentity vector_plus vector_zero.
A: AbGroup
n: nat
LeftIdentity vector_plus vector_zero
  Proof.
A: AbGroup
n: nat
LeftIdentity vector_plus vector_zero
    intros v; apply path_vector; intros i Hi.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
entry (vector_plus vector_zero v) i = entry v i
    rewrite 2 entry_Build_Vector.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
0 + entry v i = entry v i
    apply left_identity.
  Defined.

  Definition right_identity_vector_plus : RightIdentity vector_plus vector_zero.
A: AbGroup
n: nat
RightIdentity vector_plus vector_zero
  Proof.
A: AbGroup
n: nat
RightIdentity vector_plus vector_zero
    intros v; apply path_vector; intros i Hi.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
entry (vector_plus v vector_zero) i = entry v i
    rewrite 2 entry_Build_Vector.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
entry v i + 0 = entry v i
    apply right_identity.
  Defined.

  Definition left_inverse_vector_plus
    : LeftInverse vector_plus vector_neg vector_zero.
A: AbGroup
n: nat
LeftInverse vector_plus vector_neg vector_zero
  Proof.
A: AbGroup
n: nat
LeftInverse vector_plus vector_neg vector_zero
    intros v; apply path_vector; intros i Hi.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
entry (vector_plus (vector_neg v) v) i = entry vector_zero i
    rewrite 3 entry_Build_Vector.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
- entry v i + entry v i = 0
    apply left_inverse.
  Defined.

  Definition right_inverse_vector_plus
    : RightInverse vector_plus vector_neg vector_zero.
A: AbGroup
n: nat
RightInverse vector_plus vector_neg vector_zero
  Proof.
A: AbGroup
n: nat
RightInverse vector_plus vector_neg vector_zero
    intros v; apply path_vector; intros i Hi.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
entry (vector_plus v (vector_neg v)) i = entry vector_zero i
    rewrite 3 entry_Build_Vector.
A: AbGroup
n: nat
v: Vector A n
i: nat
Hi: (i < n)%nat
entry v i - entry v i = 0
    apply right_inverse.
  Defined.

  Definition abgroup_vector : AbGroup.
A: AbGroup
n: nat
AbGroup
  Proof.
A: AbGroup
n: nat
AbGroup
    snapply Build_AbGroup.
A: AbGroup
n: nat
Group
A: AbGroup
n: nat
Commutative sg_op
    1: snapply Build_Group.
A: AbGroup
n: nat
Type
A: AbGroup
n: nat
SgOp ?G
A: AbGroup
n: nat
MonUnit ?G
A: AbGroup
n: nat
Inverse ?G
A: AbGroup
n: nat
IsGroup ?G
A: AbGroup
n: nat
Commutative sg_op
    5: repeat split.
A: AbGroup
n: nat
Type
A: AbGroup
n: nat
SgOp ?G
A: AbGroup
n: nat
MonUnit ?G
A: AbGroup
n: nat
Inverse ?G
A: AbGroup
n: nat
IsHSet ?G
A: AbGroup
n: nat
Associative sg_op
A: AbGroup
n: nat
LeftIdentity sg_op mon_unit
A: AbGroup
n: nat
RightIdentity sg_op mon_unit
A: AbGroup
n: nat
LeftInverse sg_op inv mon_unit
A: AbGroup
n: nat
RightInverse sg_op inv mon_unit
A: AbGroup
n: nat
Commutative sg_op
    -
A: AbGroup
n: nat
Type exact (Vector A n).
    -
A: AbGroup
n: nat
SgOp (Vector A n) exact vector_plus.
    -
A: AbGroup
n: nat
MonUnit (Vector A n) exact vector_zero.
    -
A: AbGroup
n: nat
Inverse (Vector A n) exact vector_neg.
    -
A: AbGroup
n: nat
IsHSet (Vector A n) exact _.
    -
A: AbGroup
n: nat
Associative sg_op exact associative_vector_plus.
    -
A: AbGroup
n: nat
LeftIdentity sg_op mon_unit exact left_identity_vector_plus.
    -
A: AbGroup
n: nat
RightIdentity sg_op mon_unit exact right_identity_vector_plus.
    -
A: AbGroup
n: nat
LeftInverse sg_op inv mon_unit exact left_inverse_vector_plus.
    -
A: AbGroup
n: nat
RightInverse sg_op inv mon_unit exact right_inverse_vector_plus.
    -
A: AbGroup
n: nat
Commutative sg_op exact commutative_vector_plus.
  Defined.

End VectorAddition.

Arguments vector_plus {A n} v1 v2.

(** ** Module structure *)

Section VectorScale.
  (** A vector of elements of an R-module is itself an R-module. A special case is when the R-module is the ring R itself. *)
  Context (M : AbGroup) (n : nat) {R : Ring} `{IsLeftModule R M}.

  Definition vector_lact (r : R) : Vector M n -> Vector M n
    := vector_map (lact r).
  
  Definition left_heterodistribute_vector_lact_plus
    : LeftHeteroDistribute vector_lact vector_plus vector_plus.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftHeteroDistribute vector_lact vector_plus vector_plus
  Proof.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftHeteroDistribute vector_lact vector_plus vector_plus
    intros r v1 v2; apply path_vector; intros i Hi.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
r: R
v1, v2: Vector M n
i: nat
Hi: (i < n)%nat
entry (vector_lact r (vector_plus v1 v2)) i =
entry (vector_plus (vector_lact r v1) (vector_lact r v2)) i
    rewrite 5 entry_Build_Vector.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
r: R
v1, v2: Vector M n
i: nat
Hi: (i < n)%nat
lact r (entry v1 i + entry v2 i) = lact r (entry v1 i) + lact r (entry v2 i)
    apply distribute_l.
  Defined.

  Definition right_heterodistribute_vector_lact_plus
    : RightHeteroDistribute vector_lact (+) vector_plus.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
RightHeteroDistribute vector_lact plus vector_plus
  Proof.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
RightHeteroDistribute vector_lact plus vector_plus
    intros r1 r2 v; apply path_vector; intros i Hi.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
r1, r2: R
v: Vector M n
i: nat
Hi: (i < n)%nat
entry (vector_lact (r1 + r2) v) i =
entry (vector_plus (vector_lact r1 v) (vector_lact r2 v)) i
    rewrite 4 entry_Build_Vector.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
r1, r2: R
v: Vector M n
i: nat
Hi: (i < n)%nat
lact (r1 + r2) (entry v i) = lact r1 (entry v i) + lact r2 (entry v i)
    apply distribute_r.
  Defined.

  Definition heteroassociative_vector_lact_plus
    : HeteroAssociative vector_lact vector_lact vector_lact (.*.).
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
HeteroAssociative vector_lact vector_lact vector_lact mult
  Proof.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
HeteroAssociative vector_lact vector_lact vector_lact mult
    intros r s v; apply path_vector; intros i Hi.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
r, s: R
v: Vector M n
i: nat
Hi: (i < n)%nat
entry (vector_lact r (vector_lact s v)) i = entry (vector_lact (r * s) v) i
    rewrite 3 entry_Build_Vector.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
r, s: R
v: Vector M n
i: nat
Hi: (i < n)%nat
lact r (lact s (entry v i)) = lact (r * s) (entry v i)
    apply associativity.
  Defined.

  Definition left_identity_vector_lact : LeftIdentity vector_lact 1.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftIdentity vector_lact 1
  Proof.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftIdentity vector_lact 1
    intros v; apply path_vector; intros i Hi.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
v: Vector M n
i: nat
Hi: (i < n)%nat
entry (vector_lact 1 v) i = entry v i
    rewrite entry_Build_Vector.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
v: Vector M n
i: nat
Hi: (i < n)%nat
lact 1 (entry v i) = entry v i
    apply left_identity.
  Defined.

  Definition isleftmodule_isleftmodule_vector
    : IsLeftModule R (abgroup_vector M n).
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
IsLeftModule R (abgroup_vector M n)
  Proof.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
IsLeftModule R (abgroup_vector M n)
    snapply Build_IsLeftModule.
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
R -> abgroup_vector M n -> abgroup_vector M n
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftHeteroDistribute ?lact plus plus
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
RightHeteroDistribute ?lact plus plus
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
HeteroAssociative ?lact ?lact ?lact mult
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftIdentity ?lact 1
    -
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
R -> abgroup_vector M n -> abgroup_vector M n exact vector_lact.
    -
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftHeteroDistribute vector_lact plus plus exact left_heterodistribute_vector_lact_plus.
    -
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
RightHeteroDistribute vector_lact plus plus exact right_heterodistribute_vector_lact_plus.
    -
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
HeteroAssociative vector_lact vector_lact vector_lact mult exact heteroassociative_vector_lact_plus.
    -
M: AbGroup
n: nat
R: Ring
H: IsLeftModule R M
LeftIdentity vector_lact 1 exact left_identity_vector_lact.
  Defined.

End VectorScale.

Arguments vector_lact {M n R _} r v.