Require Import RingLike.IterMul.

Require Import Stdlib.Arith.Arith.
Import List.ListNotations.

Require Import Utf8 Core Misc Utils PermutationFun.

Notation "'∏' ( i = b , e ) , g" :=
  (iter_seq b e (λ c i, (c × g)%L) 1%L)
  (at level 35, 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) 1%L)
  (at level 35, i at level 0, l at level 60,
   right associativity,
   format "'[hv ' ∏ ( i ∈ l ) , '/' '[' g ']' ']'").

Section a.

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

Theorem fold_left_rngl_mul_fun_from_1 : ∀ 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 1)%L.
Theorem all_1_rngl_product_1 : ∀ b e f,
  (∀ i, b ≤ i ≤ e → f i = 1%L)
  → ∏ (i = b, e), f i = 1%L.
Theorem rngl_product_split_first : ∀ b k g,
  b ≤ k
  → ∏ (i = b, k), g i = (g b × ∏ (i = S b, k), g i)%L.
Theorem rngl_product_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_product_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_product_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_product_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_product_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_product_list_cons : ∀ A (a : A) la f,
  (∏ (i ∈ a :: la), f i = f a × ∏ (i ∈ la), f i)%L.

Theorem rngl_product_list_app : ∀ A (la lb : list A) f,
  ∏ (i ∈ la ++ lb), f i = (∏ (i ∈ la), f i × ∏ (i ∈ lb), f i)%L.

Theorem rngl_product_succ_succ : ∀ b k g,
  (∏ (i = S b, S k), g i = ∏ (i = b, k), g (S i))%L.

Theorem rngl_product_succ_succ' : ∀ b k g,
  (∏ (i = S b, S k), g (i - 1)%nat = ∏ (i = b, k), g i)%L.

Theorem rngl_product_list_empty : ∀ A g (l : list A),
  l = [] → ∏ (i ∈ l), g i = 1%L.

Theorem rngl_product_empty : ∀ g b k,
  k < b → (∏ (i = b, k), g i = 1)%L.

Theorem rngl_product_list_mul_distr :
  rngl_mul_is_comm 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_product_mul_distr :
  rngl_mul_is_comm T = true →
  ∀ g h b k,
  (∏ (i = b, k), (g i × h i) =
  (∏ (i = b, k), g i) × ∏ (i = b, k), h i)%L.
Theorem rngl_product_shift : ∀ s b g k,
  s ≤ b ≤ k
  → ∏ (i = b, k), g i = ∏ (i = b - s, k - s), g (s + i)%nat.

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

Theorem rngl_product_ub_mul_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_product_list_integral :
  rngl_has_opp_or_psub T = true →
  (rngl_is_integral_domain T ||
   rngl_has_inv_or_pdiv T && rngl_has_eq_dec_or_order T)%bool = true →
  rngl_characteristic T ≠ 1 →
  ∀ A (l : list A) f,
  (∏ (i ∈ l), f i)%L = 0%L
  → ∃ i, i ∈ l ∧ f i = 0%L.

Theorem rngl_product_integral :
  rngl_has_opp_or_psub T = true →
  (rngl_is_integral_domain T ||
     rngl_has_inv_or_pdiv T && rngl_has_eq_dec_or_order T)%bool = true →
  rngl_characteristic T ≠ 1 →
  ∀ b e f,
  (∏ (i = b, e), f i = 0)%L
  → ∃ i, b ≤ i ≤ e ∧ f i = 0%L.

Theorem rngl_product_list_permut : ∀ {A} {eqb : A → _},
  equality eqb →
  rngl_mul_is_comm T = true →
  ∀ (la lb : list A) f,
  permutation eqb la lb
  → ∏ (i ∈ la), f i = ∏ (i ∈ lb), f i.
Theorem rngl_product_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))%L.

Theorem rngl_inv_product_list :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  (rngl_is_integral_domain T || rngl_has_eq_dec_or_order T)%bool = true →
  ∀ A (l : list A) f,
  (∀ i, i ∈ l → f i ≠ 0%L)
  → ((∏ (i ∈ l), f i)⁻¹ = ∏ (i ∈ List.rev l), ((f i)⁻¹))%L.

Theorem rngl_inv_product :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  (rngl_is_integral_domain T || rngl_has_eq_dec_or_order T)%bool = true →
  ∀ b e f,
  (∀ i, b ≤ i ≤ e → f i ≠ 0%L)
  → ((∏ (i = b, e), f i)⁻¹ = ∏ (i = b, e), ((f (b + e - i)%nat)⁻¹))%L.

Theorem rngl_inv_product_list_comm : ∀ A (eqb : A → A → bool),
  equality eqb →
  rngl_has_opp_or_psub T = true →
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  (rngl_is_integral_domain T || rngl_has_eq_dec_or_order T)%bool = true →
  ∀ (l : list A) f,
  (∀ i, i ∈ l → f i ≠ 0%L)
  → ((∏ (i ∈ l), f i)⁻¹ = ∏ (i ∈ l), (( f i)⁻¹))%L.

Theorem rngl_inv_product_comm :
  rngl_has_opp_or_psub T = true →
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  (rngl_is_integral_domain T || rngl_has_eq_dec_or_order T)%bool = true →
  ∀ b e f,
  (∀ i, b ≤ i ≤ e → f i ≠ 0%L)
  → ((∏ (i = b, e), f i)⁻¹ = ∏ (i = b, e), ((f i)⁻¹))%L.

Theorem rngl_product_div_distr :
  rngl_has_opp_or_psub T = true →
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  (rngl_is_integral_domain T || rngl_has_eq_dec_or_order T)%bool = true →
  ∀ b e f g,
  (∀ i, b ≤ i ≤ e → g i ≠ 0%L)
  → (∏ (i = b, e), (f i / g i))%L =
    ((∏ (i = b, e), f i) / (∏ (i = b, e), g i))%L.

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

Theorem rngl_product_1_opp_1 :
  rngl_has_opp T = true →
  ∀ b e f,
  (∀ i, b ≤ i ≤ e → f i = 1%L ∨ f i = (-1)%L)
  → (∏ (i = b, e), f i = 1)%L ∨ (∏ (i = b, e), f i = -1)%L.
Theorem rngl_product_list_only_one : ∀ A g (a : A),
  (∏ (i ∈ [a]), g i = g a)%L.

Theorem rngl_product_only_one : ∀ g n, (∏ (i = n, n), g i = g n)%L.

End a.

Require Import IterAdd.

Section a.

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

Theorem rngl_product_summation_distr_cart_prod :
  rngl_has_opp_or_psub T = true →
  ∀ m n (f : nat → nat → T),
  m ≠ 0
  → ∏ (i = 1, m), (∑ (j = 1, n), f i j) =
    ∑ (l ∈ List_cart_prod (List.repeat (List.seq 1 n) m)),
      ∏ (i = 1, m), f i (List.nth (i - 1) l 0%nat).

End a.

Arguments rngl_product_list_permut {T ro rp} {A eqb} Heb Hic
  (la lb)%_list.