Require Import RingLike.IterAdd.

Require Import Stdlib.Arith.Arith.
Import ListDef.
Import List.ListNotations.
Open Scope list.

Require Import Utf8 Core Misc Utils PermutationFun.

Notation "'∑' ( i = b , e ) , g" :=
  (iter_seq b e (λ c i, (c + g)%L) 0%L)
  (at level 45, i at level 0, b at level 60, e at level 60,
   right associativity,
   format "'[hv ' ∑ ( i = b , e ) , '/' '[' g ']' ']'").

Notation "'∑' ( i ∈ l ) , g" :=
  (iter_list l (λ c i, (c + g)%L) 0%L)
  (at level 45, i at level 0, l at level 60,
   right associativity,
   format "'[hv ' ∑ ( i ∈ l ) , '/' '[' g ']' ']'").

Notation "'∑' ( ( i , j ) ∈ l ) , g" :=
  (iter_list l (λ c '(i, j), (c + g)%L) 0%L)
  (at level 45, l at level 60,
   right associativity,
   format "'[hv ' ∑ ( ( i , j ) ∈ l ) , '/' '[' g ']' ']'").

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context (Hos : rngl_has_opp_or_psub T = true).

Theorem fold_left_rngl_add_fun_from_0 : ∀ A a l (f : A → _),
  (List.fold_left (λ c i, c + f i) l a =
   a + List.fold_left (λ c i, c + f i) l 0)%L.

Theorem all_0_rngl_summation_list_0 : ∀ A l (f : A → T),
  (∀ i, i ∈ l → f i = 0%L)
  → ∑ (i ∈ l), f i = 0%L.

Theorem all_0_rngl_summation_0 : ∀ b e f,
  (∀ i, b ≤ i ≤ e → f i = 0%L)
  → ∑ (i = b, e), f i = 0%L.

Theorem rngl_summation_list_split_first : ∀ A (l : list A) d f,
  l ≠ []
  → ∑ (i ∈ l), f i = (f (List.hd d l) + ∑ (i ∈ List.tl l), f i)%L.

Theorem rngl_summation_list_split_last : ∀ A (l : list A) d f,
  l ≠ []
  → ∑ (i ∈ l), f i = (∑ (i ∈ List.removelast l), f i + f (List.last l d))%L.

Theorem rngl_summation_list_split : ∀ A (l : list A) f n,
  ∑ (i ∈ l), f i =
    (∑ (i ∈ List.firstn n l), f i + ∑ (i ∈ List.skipn n l), f i)%L.

Theorem rngl_summation_split_first : ∀ b k g,
  b ≤ k
  → ∑ (i = b, k), g i = (g b + ∑ (i = S b, k), g i)%L.

Theorem rngl_summation_split_last : ∀ b k g,
  b ≤ k
  → (∑ (i = b, k), g i = ∑ (i = S b, k), g (i - 1)%nat + g k)%L.

Theorem rngl_summation_split : ∀ j g b k,
  b ≤ S j ≤ S k
  → (∑ (i = b, k), g i = ∑ (i = b, j), g i + ∑ (i = j+1, k), g i)%L.

Theorem rngl_summation_split3 : ∀ j g b k,
  b ≤ j ≤ k
  → ∑ (i = b, k), g i =
       (∑ (i = S b, j), g (i - 1)%nat + g j + ∑ (i = j + 1, k), g i)%L.

Theorem rngl_summation_eq_compat : ∀ g h b k,
  (∀ i, b ≤ i ≤ k → (g i = h i)%L)
  → (∑ (i = b, k), g i = ∑ (i = b, k), h i)%L.

Theorem rngl_summation_list_eq_compat : ∀ A g h (l : list A),
  (∀ i, i ∈ l → (g i = h i)%L)
  → (∑ (i ∈ l), g i = ∑ (i ∈ l), h i)%L.

Theorem rngl_summation_succ_succ : ∀ b k g,
  (∑ (i = S b, S k), g i = ∑ (i = b, k), g (S i))%L.

Theorem rngl_summation_list_empty : ∀ A g (l : list A),
  l = [] → ∑ (i ∈ l), g i = 0%L.

Theorem rngl_summation_empty : ∀ g b k,
  k < b → (∑ (i = b, k), g i = 0)%L.

Theorem rngl_summation_list_add_distr :
  ∀ A g h (l : list A),
  (∑ (i ∈ l), (g i + h i) =
  (∑ (i ∈ l), g i) + ∑ (i ∈ l), h i)%L.

Theorem rngl_summation_add_distr : ∀ g h b k,
  (∑ (i = b, k), (g i + h i) =
   ∑ (i = b, k), g i + ∑ (i = b, k), h i)%L.

Theorem rngl_opp_summation_list :
  rngl_has_opp T = true →
  ∀ A (f : A → T) l, (- (∑ (i ∈ l), f i))%L = ∑ (i ∈ l), - f i.

Theorem rngl_summation_list_sub_distr :
  rngl_has_opp T = true →
  ∀ A g h (l : list A),
  (∑ (i ∈ l), (g i - h i) =
  (∑ (i ∈ l), g i) - ∑ (i ∈ l), h i)%L.

Theorem rngl_summation_shift : ∀ s b g k,
  s ≤ b ≤ k
  → ∑ (i = b, k), g i = ∑ (i = b - s, k - s), g (s + i)%nat.

Theorem rngl_summation_rshift : ∀ s b e f,
  ∑ (i = b, e), f i = ∑ (i = s + b, s + e), f (i - s)%nat.

Theorem rngl_opp_summation :
  rngl_has_opp T = true →
  ∀ b e f, ((- ∑ (i = b, e), f i) = ∑ (i = b, e), (- f i))%L.

Theorem rngl_summation_rtl : ∀ g b k,
  (∑ (i = b, k), g i = ∑ (i = b, k), g (k + b - i)%nat)%L.

Theorem mul_iter_list_distr_l_test : ∀ A B d
    (add mul : A → A → A)
    (add_0_l : ∀ x, add d x = x)
    (mul_add_distr_l : ∀ x y z, mul x (add y z) = add (mul x y) (mul x z)),
  ∀ a (la : list B) f,
  mul a (iter_list la (λ c i, add c (f i)) d) =
  if length la =? 0 then mul a d
  else iter_list la (λ c i, add c (mul a (f i))) d.

Theorem mul_iter_list_distr_l : ∀ A B a (la : list B) f
    (add mul : A → A → A) d
    (mul_add_distr_l : ∀ y z, mul a (add y z) = add (mul a y) (mul a z)),
  mul a (iter_list la (λ c i, add c (f i)) d) =
  iter_list la (λ c i, add c (mul a (f i))) (mul a d).

Theorem mul_iter_list_distr_r : ∀ A B a (la : list B) f
    (add mul : A → A → A) d
    (mul_add_distr_r : ∀ y z, mul (add y z) a = add (mul y a) (mul z a)),
  mul (iter_list la (λ c i, add c (f i)) d) a =
  iter_list la (λ c i, add c (mul (f i) a)) (mul d a).

Theorem rngl_mul_summation_list_distr_l : ∀ A a (la : list A) f,
  (a × (∑ (i ∈ la), f i) = ∑ (i ∈ la), a × f i)%L.

Theorem rngl_mul_summation_distr_l : ∀ a b e f,
  (a × (∑ (i = b, e), f i) = ∑ (i = b, e), a × f i)%L.

Theorem rngl_mul_summation_list_distr_r : ∀ A a (la : list A) f,
  ((∑ (i ∈ la), f i) × a = ∑ (i ∈ la), f i × a)%L.

Theorem rngl_mul_summation_distr_r : ∀ a b e f,
  ((∑ (i = b, e), f i) × a = ∑ (i = b, e), f i × a)%L.

Theorem rngl_summation_list_only_one : ∀ A g (a : A),
  (∑ (i ∈ [a]), g i = g a)%L.

Theorem rngl_summation_only_one : ∀ g n, ∑ (i = n, n), g i = g n.

Theorem rngl_summation_list_cons : ∀ A (a : A) la f,
  (∑ (i ∈ a :: la), f i = f a + ∑ (i ∈ la), f i)%L.

Theorem rngl_summation_list_app : ∀ A (la lb : list A) f,
  ∑ (i ∈ la ++ lb), f i = (∑ (i ∈ la), f i + ∑ (i ∈ lb), f i)%L.

Theorem rngl_summation_list_concat : ∀ A (ll : list (list A)) (f : A → T),
  ∑ (a ∈ List.concat ll), f a = ∑ (l ∈ ll), ∑ (a ∈ l), f a.

Theorem rngl_summation_list_map :
  ∀ A B (f : A → B) (g : B → _) l,
  ∑ (j ∈ List.map f l), g j = ∑ (i ∈ l), g (f i).

Theorem rngl_summation_list_flat_map A B (la : list A) f (g : B → T) :
  ∑ (i ∈ List.flat_map (λ i, map g (f i)) la), i =
  ∑ (b ∈ List.flat_map f la), g b.

Theorem rngl_summation_summation_list_flat_map :
  ∀ A B (la : list A) (f : A → list B) (g : B → T),
  ∑ (a ∈ la), ∑ (b ∈ f a), g b =
  ∑ (b ∈ List.flat_map f la), g b.

Theorem rngl_summation_summation_list_flat_map' :
  ∀ A B (la : list A) (f : A → B → T) (g : A → list B),
  ∑ (i ∈ la), ∑ (j ∈ g i), f i j =
  ∑ (i ∈ List.flat_map (λ i, map (f i) (g i)) la), i.

Theorem rngl_summation_summation_list_swap : ∀ A B la lb (f : A → B → T),
  ∑ (a ∈ la), (∑ (b ∈ lb), f a b) =
  ∑ (b ∈ lb), (∑ (a ∈ la), f a b).

Theorem rngl_summation_summation_list_exch {A B} : ∀ l1 l2 (g : A → B → _),
  (∑ (j ∈ l2), (∑ (i ∈ l1), g i j) =
   ∑ (i ∈ l1), ∑ (j ∈ l2), g i j)%L.

Theorem rngl_summation_summation_exch : ∀ a b m n g,
  (∑ (j = a, m), (∑ (i = b, n), g i j) =
   ∑ (i = b, n), ∑ (j = a, m), g i j)%L.

Theorem rngl_summation_depend_summation_exch : ∀ g k,
  (∑ (j = 0, k), (∑ (i = 0, j), g i j) =
   ∑ (i = 0, k), ∑ (j = i, k), g i j)%L.

Theorem fold_left_add_seq_add : ∀ a b len i g,
  List.fold_left (λ (c : T) (j : nat), (c + g i j)%L)
    (List.seq (b + i) len) a =
  List.fold_left (λ (c : T) (j : nat), (c + g i (i + j)%nat)%L)
    (List.seq b len) a.

Theorem rngl_summation_summation_shift : ∀ g k,
  (∑ (i = 0, k), (∑ (j = i, k), g i j) =
   ∑ (i = 0, k), ∑ (j = 0, k - i), g i (i + j)%nat)%L.

Theorem rngl_summation_ub_add_distr : ∀ a b f,
  (∑ (i = 0, a + b), f i)%L = (∑ (i = 0, a), f i + ∑ (i = S a, a + b), f i)%L.

Theorem rngl_summation_summation_distr : ∀ a b f,
  (∑ (i = 0, a), ∑ (j = 0, b), f i j)%L =
  (∑ (i = 0, (S a × S b - 1)%nat), f (i / S b)%nat (i mod S b))%L.
Theorem rngl_summation_list_permut : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ (la lb : list A) f,
  permutation eqb la lb
  → (∑ (i ∈ la), f i = ∑ (i ∈ lb), f i)%L.

Theorem rngl_summation_seq_summation : ∀ b len f,
  len ≠ 0
  → (∑ (i ∈ List.seq b len), f i = ∑ (i = b, b + len - 1), f i)%L.

Theorem rngl_summation_list_mul_summation_list :
  ∀ A B li lj (f : A → T) (g : B → T),
  ((∑ (i ∈ li), f i) × (∑ (j ∈ lj), g j))%L =
  ∑ (i ∈ li), (∑ (j ∈ lj), f i × g j).

Theorem rngl_summation_mul_summation : ∀ bi bj ei ej f g,
  ((∑ (i = bi, ei), f i) × (∑ (j = bj, ej), g j))%L =
  ∑ (i = bi, ei), (∑ (j = bj, ej), f i × g j).

Theorem rngl_summation_list_change_var : ∀ A B (l : list A) f g (h : _ → B),
  (∀ i, i ∈ l → g (h i) = i)
  → ∑ (i ∈ l), f i = ∑ (i ∈ List.map h l), f (g i).

Theorem rngl_summation_list_rev {A} (l : list A) f :
  ∑ (i ∈ List.rev l), f i = ∑ (i ∈ l), f i.

Theorem rngl_summation_change_var : ∀ A b e f g (h : _ → A),
  (∀ i, b ≤ i ≤ e → g (h i) = i)
  → ∑ (i = b, e), f i = ∑ (i ∈ List.map h (List.seq b (S e - b))), f (g i).

Theorem rngl_summation_list_le_compat {A} :
  rngl_is_ordered T = true →
  ∀ l (g h : A → T),
  (∀ i, i ∈ l → (g i ≤ h i)%L)
  → (∑ (i ∈ l), g i ≤ ∑ (i ∈ l), h i)%L.

Theorem rngl_summation_le_compat :
  rngl_is_ordered T = true →
  ∀ b e g h,
  (∀ i, b ≤ i ≤ e → (g i ≤ h i)%L)
  → (∑ (i = b, e), g i ≤ ∑ (i = b, e), h i)%L.

Theorem rngl_summation_nonneg :
  rngl_is_ordered T = true →
  ∀ b e f,
  (∀ i, b ≤ i ≤ e → (0 ≤ f i)%L)
  → (0 ≤ ∑ (i = b, e), f i)%L.

Theorem rngl_summation_filter : ∀ A l f (g : A → T),
  ∑ (a ∈ List.filter f l), g a = ∑ (a ∈ l), if f a then g a else 0%L.
Theorem rngl_summation_1 :
  ∀ b e,
  (∑ (i = b, e), 1 = rngl_of_nat (S e - b))%L.

Theorem rngl_summation_const :
  ∀ b e c,
  (∑ (i = b, e), c = rngl_of_nat (S e - b) × c)%L.

Theorem rngl_eval_polyn_is_summation :
  (0 + 0 × 1)%L = 0%L →
  ∀ (la : list T) x,
  (rngl_eval_polyn la x = ∑ (i = 0, length la - 1), la.[i] × x ^ i)%L.

Theorem rngl_summation_power :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ n x, x ≠ 1%L → ∑ (i = 0, n), x ^ i = ((x ^ S n - 1) / (x - 1))%L.

Theorem rngl_summation_list_pair :
  ∀ A l (f : A → A → T),
  ∑ ((x, y) ∈ l), f x y = ∑ (xy ∈ l), f (fst xy) (snd xy).

End a.