Require Import RingLike.Lap_algebra.

From Stdlib Require Import Utf8 Arith.
Import List.ListNotations Init.Nat.
Open Scope list.

Require Import Core Misc Utils.
Require Import IterAdd.

Section a.

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


Fixpoint strip_0s la :=
  match la with
  | [] ⇒ []
  | a :: la' ⇒ if (a =? 0)%L then strip_0s la' else la
  end.

Definition lap_norm la := List.rev (strip_0s (List.rev la)).

Lemma strip_0s_app : ∀ la lb,
  strip_0s (la ++ lb) =
  match strip_0s la with
  | [] ⇒ strip_0s lb
  | lc ⇒ lc ++ lb
  end.


Definition lap_zero : list T := [].
Definition lap_one : list T := [1%L].


Definition lap_add la lb :=
  List_map2 rngl_add
    (la ++ List.repeat 0%L (length lb - length la))
    (lb ++ List.repeat 0%L (length la - length lb)).

Theorem fold_lap_add :
  ∀ la lb,
  List_map2 rngl_add (la ++ List.repeat 0%L (length lb - length la))
    (lb ++ List.repeat 0%L (length la - length lb)) =
  lap_add la lb.


Fixpoint lap_convol_mul la lb i len :=
  match len with
  | O ⇒ []
  | S len1 ⇒
      (∑ (j = 0, i), List.nth j la 0 × List.nth (i - j) lb 0)%L ::
      lap_convol_mul la lb (S i) len1
  end.

Definition lap_mul la lb :=
  match la with
  | [] ⇒ []
  | _ ⇒
      match lb with
      | [] ⇒ []
      | _ ⇒ lap_convol_mul la lb 0 (length la + length lb - 1)
      end
  end.

End a.

Declare Scope lap_scope.
Delimit Scope lap_scope with lap.

Arguments lap_add {T ro} (la lb)%_lap.
Arguments lap_convol_mul {T ro} (la lb)%_lap (i len)%_nat.
Arguments lap_mul {T ro} (la lb)%_lap.
Arguments lap_norm {T ro} la%_lap.

Notation "0" := lap_zero : lap_scope.
Notation "1" := lap_one : lap_scope.
Notation "a + b" := (lap_add a b) : lap_scope.
Notation "a * b" := (lap_mul a b) : lap_scope.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context (Heo : rngl_has_eq_dec_or_order T = true).

Theorem lap_add_0_l : ∀ la, (0 + la)%lap = la.

Theorem lap_add_0_r : ∀ la, (la + 0)%lap = la.

Theorem lap_mul_0_l : ∀ la, (0 × la = 0)%lap.

Theorem lap_mul_0_r : ∀ la, (la × 0 = 0)%lap.

Theorem eq_lap_mul_0 : ∀ la lb, (la × lb = 0)%lap → la = 0%lap ∨ lb = 0%lap.


Theorem lap_add_length : ∀ la lb,
  length (la + lb)%lap = max (length la) (length lb).


Definition lap_opt_opp_or_psub :
  option ((list T → list T) + (list T → list T → list T)) :=
  None.


Definition lap_opt_inv_or_pdiv :
  option ((list T → list T) + (list T → list T → list T)) :=
  None.


Fixpoint lap_all_0 zero (eqb : T → T → bool) (la : list T) :=
  match la with
  | [] ⇒ true
  | a :: la' ⇒ if eqb a zero then lap_all_0 zero eqb la' else false
  end.

Fixpoint lap_eqb zero (eqb : T → _) (la lb : list T) :=
  match la with
  | [] ⇒ lap_all_0 zero eqb lb
  | a :: la' ⇒
      match lb with
      | [] ⇒ lap_all_0 zero eqb la
      | b :: lb' ⇒ if eqb a b then lap_eqb zero eqb la' lb' else false
      end
  end.

Theorem lap_eq_dec : ∀ la lb : list T, {la = lb} + {la ≠ lb}.
Definition lap_ring_like_op : ring_like_op (list T) :=
  {| rngl_zero := [];
     rngl_one := [1]%L;
     rngl_add := lap_add;
     rngl_mul := lap_mul;
     rngl_opt_opp_or_psub := lap_opt_opp_or_psub;
     rngl_opt_inv_or_pdiv := lap_opt_inv_or_pdiv;
     rngl_opt_is_zero_divisor := Some (λ _, True);
     rngl_opt_eq_dec := Some lap_eq_dec;
     rngl_opt_leb := None |}.


Theorem lap_add_comm : ∀ al1 al2,
  (al1 + al2)%lap = (al2 + al1)%lap.


Theorem List_map2_rngl_add_0_l :
  ∀ la, List_map2 rngl_add (List.repeat 0%L (length la)) la = la.

Theorem List_map2_rngl_add_0_r :
  ∀ la, List_map2 rngl_add la (List.repeat 0%L (length la)) = la.

Theorem lap_add_assoc : ∀ al1 al2 al3,
  (al1 + (al2 + al3))%lap = (al1 + al2 + al3)%lap.


Theorem eq_lap_norm_eq_length : ∀ la lb,
  lap_norm la = lap_norm lb
  → length la = length lb
  → la = lb.

Theorem lap_convol_mul_length : ∀ la lb i len,
  length (lap_convol_mul la lb i len) = len.

Theorem list_nth_lap_eq : ∀ la lb,
  (∀ i, (List.nth i la 0 = List.nth i lb 0)%L)
  → lap_norm la = lap_norm lb.
Theorem eq_lap_convol_mul_nil : ∀ la lb i len,
  lap_convol_mul la lb i len = [] → len = 0.

Theorem list_nth_lap_convol_mul_aux :
  rngl_has_opp_or_psub T = true →
  ∀ la lb n i len,
  List.length la + List.length lb - 1 = (i + len)%nat
  → (List.nth n (lap_convol_mul la lb i len) 0%L =
     ∑ (j = 0, n + i),
     List.nth j la 0 × List.nth (n + i - j) lb 0)%L.

Theorem list_nth_lap_convol_mul :
  rngl_has_opp_or_psub T = true →
  ∀ la lb i len,
  len = length la + length lb - 1
  → (List.nth i (lap_convol_mul la lb 0 len) 0 =
     ∑ (j = 0, i), List.nth j la 0 × List.nth (i - j) lb 0)%L.

Theorem summation_mul_list_nth_lap_convol_mul_r :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc k,
   (∑ (i = 0, k),
      List.nth i lc 0 ×
      List.nth (k - i) (lap_convol_mul la lb 0 (length la + length lb - 1))
        0 =
    ∑ (i = 0, k),
      List.nth (k - i) lc 0 ×
      ∑ (j = 0, i), List.nth j la 0 × List.nth (i - j) lb 0)%L.

Theorem summation_mul_list_nth_lap_convol_mul_l :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc k,
  ∑ (i = 0, k),
    List.nth i (lap_convol_mul la lb 0 (length la + length lb - 1)) 0 ×
    List.nth (k - i) lc 0 =
  ∑ (i = 0, k),
    (∑ (j = 0, i), List.nth j la 0 × List.nth (i - j) lb 0) ×
    List.nth (k - i) lc 0.

Theorem lap_norm_mul_assoc :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc, lap_norm (la × (lb × lc)) = lap_norm (la × lb × lc).

Theorem lap_mul_assoc :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc, (la × (lb × lc))%lap = (la × lb × lc)%lap.


Theorem lap_convol_mul_const_l :
  rngl_has_opp_or_psub T = true →
  ∀ a la i len,
  length la = i + len
  → lap_convol_mul [a] la i len =
    List.map (λ b, (a × b)%L) (List.skipn i la).

Theorem lap_convol_mul_const_r :
  rngl_has_opp_or_psub T = true →
  ∀ a la i len,
  length la = i + len
  → lap_convol_mul la [a] i len =
    List.map (λ b, (b × a)%L) (List.skipn i la).

Theorem lap_mul_const_l :
  rngl_has_opp_or_psub T = true →
  ∀ a la, ([a] × la)%lap = List.map (λ b : T, (a × b)%L) la.

Theorem lap_mul_const_r :
  rngl_has_opp_or_psub T = true →
  ∀ a la, (la × [a])%lap = List.map (λ b : T, (b × a)%L) la.


Fixpoint lap_convol_mul_add_l (al1 al2 al3 : list T) i len :=
  match len with
  | O ⇒ []
  | S len1 ⇒
      (∑ (j = 0, i),
       (List.nth j al1 0 + List.nth j al2 0) ×
       List.nth (i - j) al3 0)%L ::
       lap_convol_mul_add_l al1 al2 al3 (S i) len1
  end.

Fixpoint lap_convol_mul_add_r (al1 al2 al3 : list T) i len :=
  match len with
  | O ⇒ []
  | S len1 ⇒
      (∑ (j = 0, i),
       List.nth j al1 0 ×
       (List.nth (i - j) al2 0 + List.nth (i - j) al3 0))%L ::
       lap_convol_mul_add_r al1 al2 al3 (S i) len1
  end.

Theorem lap_convol_mul_succ : ∀ la lb i len,
  lap_convol_mul la lb i (S len) =
  lap_convol_mul la lb i len ++
    [∑ (j = 0, i + len),
     List.nth j la 0 × List.nth (i + len - j) lb 0]%L.

Theorem lap_norm_app_0_r : ∀ la lb,
  (∀ i, List.nth i lb 0%L = 0%L)
  → lap_norm (la ++ lb) = lap_norm la.

Theorem lap_convol_mul_more :
  rngl_has_opp_or_psub T = true →
  ∀ n la lb i len,
  length la + length lb - 1 ≤ i + len
  → lap_norm (lap_convol_mul la lb i len) =
    lap_norm (lap_convol_mul la lb i (len + n)).
Theorem lap_norm_List_map2_app_app_idemp_l :
  ∀ f, (∀ a, f a 0%L = a) →
  ∀ la lb,
  lap_norm
    (List_map2 f
       (lap_norm la ++ List.repeat 0%L (length lb - length (lap_norm la)))
       (lb ++ List.repeat 0%L (length (lap_norm la) - length lb))) =
  lap_norm
    (List_map2 f (la ++ List.repeat 0%L (length lb - length la))
       (lb ++ List.repeat 0%L (length la - length lb))).


Theorem lap_add_norm_idemp_l : ∀ la lb,
  lap_norm (lap_norm la + lb) = lap_norm (la + lb).

Theorem lap_add_norm_idemp_r : ∀ la lb,
  lap_norm (la + lap_norm lb) = lap_norm (la + lb).


Theorem list_nth_lap_add : ∀ k la lb,
  (List.nth k (lap_add la lb) 0 =
   List.nth k la 0 + List.nth k lb 0)%L.
Theorem lap_convol_mul_lap_add_r : ∀ la lb lc i len,
  lap_convol_mul la (lb + lc) i len = lap_convol_mul_add_r la lb lc i len.

Theorem lap_add_lap_convol_mul_r : ∀ la lb lc i len,
  (lap_convol_mul la lb i len + lap_convol_mul la lc i len)%lap =
  lap_convol_mul_add_r la lb lc i len.

Theorem lap_norm_mul_add_distr_l :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc, lap_norm (la × (lb + lc)) = lap_norm (la × lb + la × lc).

Theorem lap_mul_add_distr_l :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc, (la × (lb + lc))%lap = (la × lb + la × lc)%lap.


Theorem lap_convol_mul_comm :
  rngl_mul_is_comm T = true →
  ∀ l1 l2 i len,
  lap_convol_mul l1 l2 i len = lap_convol_mul l2 l1 i len.

Theorem lap_mul_comm :
  rngl_mul_is_comm T = true →
  ∀ la lb, (la × lb)%lap = (lb × la)%lap.

Theorem lap_opt_mul_comm :
  if rngl_mul_is_comm T then ∀ a b : list T, (a × b)%lap = (b × a)%lap
  else not_applicable.


Theorem lap_mul_1_l : let rol := lap_ring_like_op in
  rngl_has_opp_or_psub T = true →
  ∀ la : list T, (1 × la)%L = la.

Theorem lap_opt_mul_1_r : let rol := lap_ring_like_op in
  rngl_has_opp_or_psub T = true →
  if rngl_mul_is_comm T then not_applicable
  else ∀ la : list T, (la × 1)%L = la.


Theorem lap_convol_mul_lap_add_l : ∀ la lb lc i len,
  lap_convol_mul (la + lb) lc i len = lap_convol_mul_add_l la lb lc i len.

Theorem lap_add_lap_convol_mul_l : ∀ la lb lc i len,
  (lap_convol_mul la lc i len + lap_convol_mul lb lc i len)%lap =
  lap_convol_mul_add_l la lb lc i len.

Theorem lap_norm_mul_add_distr_r :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc : list T,
  lap_norm ((la + lb) × lc) = lap_norm (la × lc + lb × lc).

Theorem lap_mul_add_distr_r :
  rngl_has_opp_or_psub T = true →
  ∀ la lb lc, ((la + lb) × lc)%lap = (la × lc + lb × lc)%lap.

Theorem lap_opt_mul_add_distr_r :
  rngl_has_opp_or_psub T = true →
  if rngl_mul_is_comm T then not_applicable
  else ∀ a b c, ((a + b) × c)%lap = (a × c + b × c)%lap.


Theorem lap_polyn_integral :
  let rol := lap_ring_like_op in
  ∀ la lb : list T,
  (la × lb)%L = 0%L
  → la = 0%L ∨ lb = 0%L ∨ rngl_is_zero_divisor la ∨ rngl_is_zero_divisor lb.


Theorem lap_characteristic_prop :
  let rol := lap_ring_like_op in
  ∀ i : nat, rngl_of_nat (S i) ≠ 0%L.


Definition lap_ring_like_prop (Hos : rngl_has_opp_or_psub T = true) :
    ring_like_prop (list T) :=
  let rol := lap_ring_like_op in
  {| rngl_mul_is_comm := rngl_mul_is_comm T;
     rngl_is_archimedean := false;
     rngl_is_alg_closed := false;
     rngl_characteristic := 0;
     rngl_add_comm := lap_add_comm;
     rngl_add_assoc := lap_add_assoc;
     rngl_add_0_l := lap_add_0_l;
     rngl_mul_assoc := lap_mul_assoc Hos;
     rngl_mul_1_l := lap_mul_1_l Hos;
     rngl_mul_add_distr_l := lap_mul_add_distr_l Hos;
     rngl_opt_mul_comm := lap_opt_mul_comm;
     rngl_opt_mul_1_r := lap_opt_mul_1_r Hos;
     rngl_opt_mul_add_distr_r := lap_opt_mul_add_distr_r Hos;
     rngl_opt_add_opp_diag_l := NA;
     rngl_opt_add_sub := NA;
     rngl_opt_sub_add_distr := NA;
     rngl_opt_sub_0_l := NA;
     rngl_opt_mul_inv_diag_l := NA;
     rngl_opt_mul_inv_diag_r := NA;
     rngl_opt_mul_div := NA;
     rngl_opt_integral := lap_polyn_integral;
     rngl_opt_alg_closed := NA;
     rngl_opt_characteristic_prop := lap_characteristic_prop;
     rngl_opt_ord := NA;
     rngl_opt_archimedean := NA |}.

End a.