Require Import Basics.Overture Basics.Tactics.Require Import Basics.Overture Basics.Tactics.
Require Import Spaces.Nat.Core Spaces.Int.
Require Export Classes.interfaces.canonical_names (Commutative).
Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
Require Import AbelianGroup.

Local Open Scope mc_scope.
Local Open Scope mc_add_scope.

(** * Finite Sums *)

(** Indexed finite sum of abelian group elements. *)
Definition ab_sum {A : AbGroup} (n : nat) (f : forall k, (k < n)%nat -> A) : A.
A: AbGroup
n: nat
f: forall k : nat, (k < n)%nat -> A
A
Proof.
A: AbGroup
n: nat
f: forall k : nat, (k < n)%nat -> A
A
  induction n as [|n IHn].
A: AbGroup
f: forall k : nat, (k < 0)%nat -> A
A
A: AbGroup
n: nat
f: forall k : nat, (k < n.+1)%nat -> A
IHn: (forall k : nat, (k < n)%nat -> A) -> A
A
  -
A: AbGroup
f: forall k : nat, (k < 0)%nat -> A
A exact 0.
  -
A: AbGroup
n: nat
f: forall k : nat, (k < n.+1)%nat -> A
IHn: (forall k : nat, (k < n)%nat -> A) -> A
A refine (f n _ + IHn _).
A: AbGroup
n: nat
f: forall k : nat, (k < n.+1)%nat -> A
IHn: (forall k : nat, (k < n)%nat -> A) -> A
forall k : nat, (k < n)%nat -> A
    intros k Hk.
A: AbGroup
n: nat
f: forall k0 : nat, (k0 < n.+1)%nat -> A
IHn: (forall k0 : nat, (k0 < n)%nat -> A) -> A
k: nat
Hk: (k < n)%nat
A
    exact (f k _).
Defined.

(** If the function is constant in the range of a finite sum then the sum is equal to the constant times [n]. This is a group power in the underlying group. *)
Definition ab_sum_const {A : AbGroup} (n : nat) (a : A)
  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a)
  : ab_sum n f = ab_mul n a.
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n)%nat -> A
p: forall (k : nat) (Hk : (k < n)%nat), f k Hk = a
ab_sum n f = ab_mul n a
Proof.
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n)%nat -> A
p: forall (k : nat) (Hk : (k < n)%nat), f k Hk = a
ab_sum n f = ab_mul n a
  induction n as [|n IHn] in f, p |- *.
A: AbGroup
a: A
f: forall k : nat, (k < 0)%nat -> A
p: forall (k : nat) (Hk : (k < 0)%nat), f k Hk = a
ab_sum 0 f = ab_mul 0%nat a
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = a
IHn: forall f0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = a) ->
ab_sum n f0 = ab_mul n a
ab_sum n.+1 f = ab_mul n.+1%nat a
  -
A: AbGroup
a: A
f: forall k : nat, (k < 0)%nat -> A
p: forall (k : nat) (Hk : (k < 0)%nat), f k Hk = a
ab_sum 0 f = ab_mul 0%nat a reflexivity.
  -
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = a
IHn: forall f0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = a) ->
ab_sum n f0 = ab_mul n a
ab_sum n.+1 f = ab_mul n.+1%nat a rhs_V napply (ap@{Set _} _ (int_nat_succ n)).
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = a
IHn: forall f0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = a) ->
ab_sum n f0 = ab_mul n a
ab_sum n.+1 f = grp_pow a n.+1%int
    rhs napply grp_pow_succ.
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = a
IHn: forall f0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = a) ->
ab_sum n f0 = ab_mul n a
ab_sum n.+1 f = a + grp_pow a n
    simpl.
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = a
IHn: forall f0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = a) ->
ab_sum n f0 = ab_mul n a
f n (leq_refl n.+1) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k (leq_succ_r Hk)) =
a + grp_pow a n f_ap.
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = a
IHn: forall f0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = a) ->
ab_sum n f0 = ab_mul n a
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k (leq_succ_r Hk)) =
grp_pow a n
    apply IHn.
A: AbGroup
n: nat
a: A
f: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = a
IHn: forall f0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = a) ->
ab_sum n f0 = ab_mul n a
forall (k : nat) (Hk : (k < n)%nat), f k (leq_succ_r Hk) = a
    intros.
A: AbGroup
n: nat
a: A
f: forall k0 : nat, (k0 < n.+1)%nat -> A
p: forall (k0 : nat) (Hk0 : (k0 < n.+1)%nat), f k0 Hk0 = a
IHn: forall f0 : forall k0 : nat, (k0 < n)%nat -> A,
(forall (k0 : nat) (Hk0 : (k0 < n)%nat), f0 k0 Hk0 = a) ->
ab_sum n f0 = ab_mul n a
k: nat
Hk: (k < n)%nat
f k (leq_succ_r Hk) = a apply p.
Defined.

(** If the function is zero in the range of a finite sum then the sum is zero. *)
Definition ab_sum_zero {A : AbGroup} (n : nat)
  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = 0)
  : ab_sum n f = 0.
A: AbGroup
n: nat
f: forall k : nat, (k < n)%nat -> A
p: forall (k : nat) (Hk : (k < n)%nat), f k Hk = 0
ab_sum n f = 0
Proof.
A: AbGroup
n: nat
f: forall k : nat, (k < n)%nat -> A
p: forall (k : nat) (Hk : (k < n)%nat), f k Hk = 0
ab_sum n f = 0
  lhs exact (ab_sum_const _ 0 f p).
A: AbGroup
n: nat
f: forall k : nat, (k < n)%nat -> A
p: forall (k : nat) (Hk : (k < n)%nat), f k Hk = 0
ab_mul n 0 = 0
  apply grp_pow_unit.
Defined.

(** Finite sums distribute over addition. *)
Definition ab_sum_plus {A : AbGroup} (n : nat) (f g : forall k, (k < n)%nat -> A)
  : ab_sum n (fun k Hk => f k Hk + g k Hk)
    = ab_sum n (fun k Hk => f k Hk) + ab_sum n (fun k Hk => g k Hk).
A: AbGroup
n: nat
f, g: forall k : nat, (k < n)%nat -> A
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k Hk + g k Hk) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k Hk) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g k Hk)
Proof.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n)%nat -> A
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k Hk + g k Hk) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k Hk) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g k Hk)
  induction n as [|n IHn].
A: AbGroup
f, g: forall k : nat, (k < 0)%nat -> A
ab_sum 0 (fun (k : nat) (Hk : (k < 0)%nat) => f k Hk + g k Hk) =
ab_sum 0 (fun (k : nat) (Hk : (k < 0)%nat) => f k Hk) +
ab_sum 0 (fun (k : nat) (Hk : (k < 0)%nat) => g k Hk)
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk + g0 k Hk) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g0 k Hk)
ab_sum n.+1 (fun (k : nat) (Hk : (k < n.+1)%nat) => f k Hk + g k Hk) =
ab_sum n.+1 (fun (k : nat) (Hk : (k < n.+1)%nat) => f k Hk) +
ab_sum n.+1 (fun (k : nat) (Hk : (k < n.+1)%nat) => g k Hk)
  1: by rewrite grp_unit_l.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk + g0 k Hk) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g0 k Hk)
ab_sum n.+1 (fun (k : nat) (Hk : (k < n.+1)%nat) => f k Hk + g k Hk) =
ab_sum n.+1 (fun (k : nat) (Hk : (k < n.+1)%nat) => f k Hk) +
ab_sum n.+1 (fun (k : nat) (Hk : (k < n.+1)%nat) => g k Hk)
  simpl.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk + g0 k Hk) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g0 k Hk)
f n (leq_refl n.+1) + g n (leq_refl n.+1) +
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   f k (leq_succ_r Hk) + g k (leq_succ_r Hk)) =
f n (leq_refl n.+1) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k (leq_succ_r Hk)) +
(g n (leq_refl n.+1) +
 ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g k (leq_succ_r Hk)))
  rewrite <- !grp_assoc; f_ap.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk + g0 k Hk) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g0 k Hk)
g n (leq_refl n.+1) +
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   f k (leq_succ_r Hk) + g k (leq_succ_r Hk)) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k (leq_succ_r Hk)) +
(g n (leq_refl n.+1) +
 ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g k (leq_succ_r Hk)))
  rewrite IHn, abgroup_commutative, <- grp_assoc; f_ap.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk + g0 k Hk) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f0 k Hk) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g0 k Hk)
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g k (leq_succ_r Hk)) +
g n (leq_refl n.+1) =
g n (leq_refl n.+1) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => g k (leq_succ_r Hk))
  by rewrite abgroup_commutative.
Defined.

(** Double finite sums commute. *)
Definition ab_sum_sum {A : AbGroup} (m n : nat)
  (f : forall i j, (i < m)%nat -> (j < n)%nat -> A)
  : ab_sum m (fun i Hi => ab_sum n (fun j Hj => f i j Hi Hj))
   = ab_sum n (fun j Hj => ab_sum m (fun i Hi => f i j Hi Hj)).
A: AbGroup
m, n: nat
f: forall i j : nat, (i < m)%nat -> (j < n)%nat -> A
ab_sum m
  (fun (i : nat) (Hi : (i < m)%nat) =>
   ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => f i j Hi Hj)) =
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   ab_sum m (fun (i : nat) (Hi : (i < m)%nat) => f i j Hi Hj))
Proof.
A: AbGroup
m, n: nat
f: forall i j : nat, (i < m)%nat -> (j < n)%nat -> A
ab_sum m
  (fun (i : nat) (Hi : (i < m)%nat) =>
   ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => f i j Hi Hj)) =
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   ab_sum m (fun (i : nat) (Hi : (i < m)%nat) => f i j Hi Hj))
  induction n as [|n IHn] in m, f |- *.
A: AbGroup
m: nat
f: forall i j : nat, (i < m)%nat -> (j < 0)%nat -> A
ab_sum m
  (fun (i : nat) (Hi : (i < m)%nat) =>
   ab_sum 0 (fun (j : nat) (Hj : (j < 0)%nat) => f i j Hi Hj)) =
ab_sum 0
  (fun (j : nat) (Hj : (j < 0)%nat) =>
   ab_sum m (fun (i : nat) (Hi : (i < m)%nat) => f i j Hi Hj))
A: AbGroup
m, n: nat
f: forall i j : nat, (i < m)%nat -> (j < n.+1)%nat -> A
IHn: forall (m0 : nat) (f0 : forall i j : nat, (i < m0)%nat -> (j < n)%nat -> A),
ab_sum m0
  (fun (i : nat) (Hi : (i < m0)%nat) =>
   ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => f0 i j Hi Hj)) =
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   ab_sum m0 (fun (i : nat) (Hi : (i < m0)%nat) => f0 i j Hi Hj))
ab_sum m
  (fun (i : nat) (Hi : (i < m)%nat) =>
   ab_sum n.+1 (fun (j : nat) (Hj : (j < n.+1)%nat) => f i j Hi Hj)) =
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   ab_sum m (fun (i : nat) (Hi : (i < m)%nat) => f i j Hi Hj))
  1: by napply ab_sum_zero.
A: AbGroup
m, n: nat
f: forall i j : nat, (i < m)%nat -> (j < n.+1)%nat -> A
IHn: forall (m0 : nat) (f0 : forall i j : nat, (i < m0)%nat -> (j < n)%nat -> A),
ab_sum m0
  (fun (i : nat) (Hi : (i < m0)%nat) =>
   ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => f0 i j Hi Hj)) =
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   ab_sum m0 (fun (i : nat) (Hi : (i < m0)%nat) => f0 i j Hi Hj))
ab_sum m
  (fun (i : nat) (Hi : (i < m)%nat) =>
   ab_sum n.+1 (fun (j : nat) (Hj : (j < n.+1)%nat) => f i j Hi Hj)) =
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   ab_sum m (fun (i : nat) (Hi : (i < m)%nat) => f i j Hi Hj))
  lhs napply ab_sum_plus; cbn; f_ap.
Defined.

(** Finite sums are equal if the functions are equal in the range. *)
Definition path_ab_sum {A : AbGroup} {n : nat} {f g : forall k, (k < n)%nat -> A}
  (p : forall k Hk, f k Hk = g k Hk)
  : ab_sum n f = ab_sum n g.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n)%nat -> A
p: forall (k : nat) (Hk : (k < n)%nat), f k Hk = g k Hk
ab_sum n f = ab_sum n g
Proof.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n)%nat -> A
p: forall (k : nat) (Hk : (k < n)%nat), f k Hk = g k Hk
ab_sum n f = ab_sum n g
  induction n as [|n IHn].
A: AbGroup
f, g: forall k : nat, (k < 0)%nat -> A
p: forall (k : nat) (Hk : (k < 0)%nat), f k Hk = g k Hk
ab_sum 0 f = ab_sum 0 g
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = g k Hk
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = g0 k Hk) ->
ab_sum n f0 = ab_sum n g0
ab_sum n.+1 f = ab_sum n.+1 g
  1: reflexivity.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = g k Hk
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = g0 k Hk) ->
ab_sum n f0 = ab_sum n g0
ab_sum n.+1 f = ab_sum n.+1 g
  cbn; f_ap.
A: AbGroup
n: nat
f, g: forall k : nat, (k < n.+1)%nat -> A
p: forall (k : nat) (Hk : (k < n.+1)%nat), f k Hk = g k Hk
IHn: forall f0 g0 : forall k : nat, (k < n)%nat -> A,
(forall (k : nat) (Hk : (k < n)%nat), f0 k Hk = g0 k Hk) ->
ab_sum n f0 = ab_sum n g0
nat_rect (fun n0 : nat => (forall k : nat, (k < n0)%nat -> A) -> A)
  (fun _ : forall k : nat, (k < 0)%nat -> A => 0)
  (fun (n0 : nat) (IHn0 : (forall k : nat, (k < n0)%nat -> A) -> A)
     (f0 : forall k : nat, (k < n0.+1)%nat -> A) =>
   f0 n0 (leq_refl n0.+1) +
   IHn0 (fun (k : nat) (Hk : (k < n0)%nat) => f0 k (leq_succ_r Hk)))
  n (fun (k : nat) (Hk : (k < n)%nat) => f k (leq_succ_r Hk)) =
nat_rect (fun n0 : nat => (forall k : nat, (k < n0)%nat -> A) -> A)
  (fun _ : forall k : nat, (k < 0)%nat -> A => 0)
  (fun (n0 : nat) (IHn0 : (forall k : nat, (k < n0)%nat -> A) -> A)
     (f0 : forall k : nat, (k < n0.+1)%nat -> A) =>
   f0 n0 (leq_refl n0.+1) +
   IHn0 (fun (k : nat) (Hk : (k < n0)%nat) => f0 k (leq_succ_r Hk)))
  n (fun (k : nat) (Hk : (k < n)%nat) => g k (leq_succ_r Hk))
  by apply IHn.
Defined.