CoRN.algebra.CSums



Require Export CAbGroups.
Require Export Peano_dec.

Sums

Let G be an abelian group.

Section Sums.

Variable G : CAbGroup.
Fixpoint Sumlist (l : list G) : G :=
  match l with
  | nil ⇒ [0]:G
  | cons x k ⇒ x[+]Sumlist k
  end.

Fixpoint Sumx n : (∀ i : nat, i < n → G) → G :=
  match n return ((∀ i : nat, i < n → G) → G) with
  | O ⇒ fun _ ⇒ [0]:G
  | S m ⇒ fun f ⇒ Sumx m (fun i l ⇒ f i (lt_S _ _ l)) [+]f m (lt_n_Sn m)
  end.

It is sometimes useful to view a function defined on {0, ... i-1} as a function on the natural numbers which evaluates to Zero when the input is greater than or equal to i.

Definition part_tot_nat_fun n (f : ∀ i, i < n → G) : nat → G.
Proof.
 intros i.
 elim (le_lt_dec n i).
  intro a; apply ([0]:G).
 intro b; apply (f i b).
Defined.

Lemma part_tot_nat_fun_ch1 : ∀ n (f : ∀ i, i < n → G),
 nat_less_n_fun f → ∀ i Hi, part_tot_nat_fun n f i [=] f i Hi.
Proof.
 intros n f Hf i Hi.
 unfold part_tot_nat_fun in |- ×.
 elim le_lt_dec; intro.
  elimtype False; apply (le_not_lt n i); auto.
 simpl in |- *; apply Hf; auto.
Qed.

Lemma part_tot_nat_fun_ch2 : ∀ n (f : ∀ i, i < n → G) i,
 n ≤ i → part_tot_nat_fun n f i [=] [0].
Proof.
 intros n f i Hi.
 unfold part_tot_nat_fun in |- ×.
 elim le_lt_dec; intro.
  simpl in |- *; algebra.
 elimtype False; apply (le_not_lt n i); auto.
Qed.

∑0 defines the sum for i=0..(n-1)

Fixpoint ∑0 (n:nat) (f : nat → G) {struct n} : G :=
  match n with
  | O ⇒ [0]:G
  | S m ⇒ ∑0 m f[+]f m
  end.

∑1 defines the sum for i=m..(n-1)

Definition ∑1 m n f := ∑0 n f[-]∑0 m f.

Definition ∑ m n : (nat → G) → G := ∑1 m (S n).

∑2 is similar to ∑1, but does not require the summand to be defined outside where it is being added.

Definition ∑2 m n (h : ∀ i : nat, m ≤ i → i ≤ n → G) : G.
Proof.
 apply (∑ m n).
 intro i.
 elim (le_lt_dec m i); intro H.
  elim (le_lt_dec i n); intro H0.
   apply (h i H H0).
  apply ([0]:G).
 apply ([0]:G).
Defined.

Lemma Sum_one : ∀ n f, ∑ n n f [=] f n.
Proof.
 intros n f.
 unfold ∑ in |- ×.
 unfold ∑1 in |- ×.
 simpl in |- ×.
 Step_final (f n[+]∑0 n f[-]∑0 n f).
Qed.

Hint Resolve Sum_one: algebra.

Lemma Sum_empty : ∀ n f, 0 < n → ∑ n (pred n) f [=] [0].
Proof.
 intros n f H.
 unfold ∑ in |- ×.
 rewrite <- (S_pred _ _ H).
 unfold ∑1 in |- *; algebra.
Qed.

Hint Resolve Sum_empty: algebra.

Lemma Sum_Sum : ∀ l m n f, ∑ l m f[+]∑ (S m) n f [=] ∑ l n f.
Proof.
 intros l m n f.
 unfold ∑ in |- ×.
 unfold ∑1 in |- ×.
 astepl (∑0 (S n) f[-]∑0 (S m) f[+] (∑0 (S m) f[-]∑0 l f)).
 astepl (∑0 (S n) f[-]∑0 (S m) f[+]∑0 (S m) f[-]∑0 l f).
 astepl (∑0 (S n) f[-] (∑0 (S m) f[-]∑0 (S m) f) [-]∑0 l f).
 astepl (∑0 (S n) f[-][0][-]∑0 l f).
 astepl (∑0 (S n) f[+] [--][0][-]∑0 l f).
 Step_final (∑0 (S n) f[+][0][-]∑0 l f).
Qed.

Hint Resolve Sum_Sum: algebra.

Lemma Sum_first : ∀ m n f, ∑ m n f [=] f m[+]∑ (S m) n f.
Proof.
 intros m n f.
 unfold ∑ in |- ×.
 unfold ∑1 in |- ×.
 astepr (f m[+]∑0 (S n) f[-]∑0 (S m) f).
 astepr (∑0 (S n) f[+]f m[-]∑0 (S m) f).
 astepr (∑0 (S n) f[+] (f m[-]∑0 (S m) f)).
 unfold cg_minus in |- ×.
 apply bin_op_wd_unfolded.
  algebra.
 simpl in |- ×.
 astepr (f m[+] [--] (f m[+]∑0 m f)).
 astepr (f m[+] ([--] (f m) [+] [--] (∑0 m f))).
 astepr (f m[+] [--] (f m) [+] [--] (∑0 m f)).
 astepr ([0][+] [--] (∑0 m f)).
 algebra.
Qed.

Lemma Sum_last : ∀ m n f, ∑ m (S n) f [=] ∑ m n f[+]f (S n).
Proof.
 intros m n f.
 unfold ∑ in |- ×.
 unfold ∑1 in |- ×.
 simpl in |- ×.
 unfold cg_minus in |- ×.
 astepl (∑0 n f[+]f n[+] (f (S n) [+] [--] (∑0 m f))).
 astepr (∑0 n f[+]f n[+] ([--] (∑0 m f) [+]f (S n))).
 algebra.
Qed.

Hint Resolve Sum_last: algebra.

Lemma Sum_last' : ∀ m n f, 0 < n → ∑ m n f [=] ∑ m (pred n) f[+]f n.
Proof.
 intros m n f H. induction n as [| n Hrecn].
 elim (lt_irrefl 0 H).
 apply Sum_last.
Qed.

We add some extensionality results which will be quite useful when working with integration.

Lemma Sum0_strext : ∀ f g n, ∑0 n f [#] ∑0 n g → {i:nat | i < n | f i [#] g i}.
Proof.
 intros f g n H.
 induction n as [| n Hrecn].
  simpl in H.
  elim (ap_irreflexive_unfolded _ _ H).
 simpl in H.
 cut ({i : nat | i < n | f i [#] g i} or f n [#] g n).
  intro H0.
  elim H0; intro H1.
   elim H1; intros i H2 H3; ∃ i; auto with arith.
  ∃ n; auto with arith.
 cut (∑0 n f [#] ∑0 n g or f n [#] g n).
  intro H0; elim H0; intro H1.
   left; apply Hrecn; assumption.
  auto.
 apply bin_op_strext_unfolded with (csg_op (c:=G)).
 assumption.
Qed.

Lemma Sum_strext : ∀ f g m n, m ≤ S n →
 ∑ m n f [#] ∑ m n g → {i : nat | m ≤ i ∧ i ≤ n | f i [#] g i}.
Proof.
 intros f g m n H H0.
 induction n as [| n Hrecn].
  elim (le_lt_eq_dec _ _ H); intro H2.
   cut (m = 0).
    intro H1.
    rewrite H1; ∃ 0; auto.
    rewrite H1 in H0.
    astepl (∑ 0 0 f); astepr (∑ 0 0 g); assumption.
   inversion H2; [ auto | inversion H3 ].
  elimtype False.
  cut (0 = pred 1); [ intro H3 | auto ].
  rewrite H3 in H0.
  rewrite H2 in H0.
  apply (ap_irreflexive_unfolded G [0]).
  eapply ap_wdl_unfolded.
   eapply ap_wdr_unfolded.
    apply H0.
   apply Sum_empty; auto.
  apply Sum_empty; auto.
 elim (le_lt_eq_dec _ _ H); intro Hmn.
  cut (∑ m n f [#] ∑ m n g or f (S n) [#] g (S n)).
   intro H1; elim H1; intro H2.
    cut {i : nat | m ≤ i ∧ i ≤ n | f i [#] g i}.
     intro H3; elim H3; intros i H4 H5; elim H4; intros H6 H7; clear H1 H4.
     ∃ i; try split; auto with arith.
    apply Hrecn; auto with arith.
   ∃ (S n); try split; auto with arith.
  apply bin_op_strext_unfolded with (csg_op (c:=G)).
  astepl (∑ m (S n) f); astepr (∑ m (S n) g); assumption.
 clear Hrecn.
 elimtype False.
 cut (S n = pred (S (S n))); [ intro H1 | auto ].
 rewrite H1 in H0.
 rewrite Hmn in H0.
 apply (ap_irreflexive_unfolded G [0]).
 eapply ap_wdl_unfolded.
  eapply ap_wdr_unfolded.
   apply H0.
  apply Sum_empty; auto with arith.
 apply Sum_empty; auto with arith.
Qed.

Lemma Sumx_strext : ∀ n f g, nat_less_n_fun f → nat_less_n_fun g →
 Sumx _ f [#] Sumx _ g → {N : nat | {HN : N < n | f N HN [#] g N HN}}.
Proof.
 intro n; induction n as [| n Hrecn].
  intros f g H H0 H1.
  elim (ap_irreflexive_unfolded _ _ H1).
 intros f g H H0 H1.
 simpl in H1.
 elim (bin_op_strext_unfolded _ _ _ _ _ _ H1); clear H1; intro H1.
  cut (nat_less_n_fun (fun (i : nat) (l : i < n) ⇒ f i (lt_S _ _ l)));
    [ intro H2 | red in |- *; intros; apply H; assumption ].
  cut (nat_less_n_fun (fun (i : nat) (l : i < n) ⇒ g i (lt_S _ _ l)));
    [ intro H3 | red in |- *; intros; apply H0; assumption ].
  elim (Hrecn _ _ H2 H3 H1); intros N HN.
  elim HN; clear HN; intros HN H'.
  ∃ N. ∃ (lt_S _ _ HN).
  eapply ap_wdl_unfolded.
   eapply ap_wdr_unfolded.
    apply H'.
   algebra.
  algebra.
 ∃ n. ∃ (lt_n_Sn n).
 eapply ap_wdl_unfolded.
  eapply ap_wdr_unfolded.
   apply H1.
  algebra.
 algebra.
Qed.

Lemma Sum0_strext' : ∀ f g n, ∑0 n f [#] ∑0 n g → {i : nat | f i [#] g i}.
Proof.
 intros f g n H.
 elim (Sum0_strext _ _ _ H); intros i Hi Hi'; ∃ i; auto.
Qed.

Lemma Sum_strext' : ∀ f g m n, ∑ m n f [#] ∑ m n g → {i : nat | f i [#] g i}.
Proof.
 intros f g m n H.
 unfold ∑, ∑1 in H.
 elim (cg_minus_strext _ _ _ _ _ H); intro H1; elim (Sum0_strext _ _ _ H1);
   intros i Hi Hi'; ∃ i; assumption.
Qed.

Lemma Sum0_wd : ∀ m f f', (∀ i, f i [=] f' i) → ∑0 m f [=] ∑0 m f'.
Proof.
 intros m f f' H.
 elim m; simpl in |- *; algebra.
Qed.

Lemma Sum_wd : ∀ m n f f', (∀ i, f i [=] f' i) → ∑ m n f [=] ∑ m n f'.
Proof.
 intros m n f f' H.
 unfold ∑ in |- ×.
 unfold ∑1 in |- ×.
 unfold cg_minus in |- ×.
 apply bin_op_wd_unfolded.
  apply Sum0_wd; exact H.
 apply un_op_wd_unfolded.
 apply Sum0_wd; exact H.
Qed.

Lemma Sumx_wd : ∀ n f g, (∀ i H, f i H [=] g i H) → Sumx n f [=] Sumx n g.
Proof.
 intro n; elim n; intros; simpl in |- *; algebra.
Qed.

Lemma Sum_wd' : ∀ m n, m ≤ S n → ∀ f f',
 (∀ i, m ≤ i → i ≤ n → f i [=] f' i) → ∑ m n f [=] ∑ m n f'.
Proof.
 intros m n. induction n as [| n Hrecn]; intros H f f' H0.
 inversion H.
   unfold ∑ in |- ×. unfold ∑1 in |- ×. Step_final ([0]:G).
   inversion H2. astepl (f 0). astepr (f' 0). auto.
  elim (le_lt_eq_dec m (S (S n)) H); intro H1.
  astepl (∑ m n f[+]f (S n)).
  astepr (∑ m n f'[+]f' (S n)).
  apply bin_op_wd_unfolded; auto with arith.
 rewrite H1.
 unfold ∑ in |- ×. unfold ∑1 in |- ×. Step_final ([0]:G).
Qed.

Lemma Sum2_wd : ∀ m n, m ≤ S n → ∀ f g,
 (∀ i Hm Hn, f i Hm Hn [=] g i Hm Hn) → ∑2 m n f [=] ∑2 m n g.
Proof.
 intros m n H f g H0.
 unfold ∑2 in |- ×.
 apply Sum_wd'.
  assumption.
 intros i H1 H2.
 elim le_lt_dec; intro H3; [ simpl in |- × | elimtype False; apply (le_not_lt i n); auto ].
 elim le_lt_dec; intro H4; [ simpl in |- × | elimtype False; apply (le_not_lt m i); auto ].
 algebra.
Qed.

Lemma Sum0_plus_Sum0 : ∀ f g m, ∑0 m (fun i ⇒ f i[+]g i) [=] ∑0 m f[+]∑0 m g.
Proof.
 intros f g m.
 elim m.
  simpl in |- *; algebra.
 intros n H.
 simpl in |- ×.
 astepl (∑0 n f[+]∑0 n g[+] (f n[+]g n)).
 astepl (∑0 n f[+] (∑0 n g[+] (f n[+]g n))).
 astepl (∑0 n f[+] (∑0 n g[+]f n[+]g n)).
 astepl (∑0 n f[+] (f n[+]∑0 n g[+]g n)).
 astepl (∑0 n f[+] (f n[+]∑0 n g) [+]g n).
 Step_final (∑0 n f[+]f n[+]∑0 n g[+]g n).
Qed.
Hint Resolve Sum0_plus_Sum0: algebra.

Lemma Sum_plus_Sum : ∀ f g m n, ∑ m n (fun i ⇒ f i[+]g i) [=] ∑ m n f[+]∑ m n g.
Proof.
 intros f g m n.
 unfold ∑ in |- ×.
 unfold ∑1 in |- ×.
 astepl (∑0 (S n) f[+]∑0 (S n) g[-] (∑0 m f[+]∑0 m g)).
 astepl (∑0 (S n) f[+]∑0 (S n) g[-]∑0 m f[-]∑0 m g).
 unfold cg_minus in |- ×.
 astepr (∑0 (S n) f[+] [--] (∑0 m f) [+]∑0 (S n) g[+] [--] (∑0 m g)).
 apply bin_op_wd_unfolded.
  astepl (∑0 (S n) f[+] (∑0 (S n) g[+] [--] (∑0 m f))).
  astepl (∑0 (S n) f[+] ([--] (∑0 m f) [+]∑0 (S n) g)).
  algebra.
 algebra.
Qed.

Lemma Sumx_plus_Sumx : ∀ n f g, Sumx n f[+]Sumx n g [=] Sumx n (fun i Hi ⇒ f i Hi[+]g i Hi).
Proof.
 intro n; induction n as [| n Hrecn].
  intros; simpl in |- *; algebra.
 intros f g; simpl in |- ×.
 apply eq_transitive_unfolded with (Sumx _ (fun (i : nat) (l : i < n) ⇒ f i (lt_S i n l)) [+]
   Sumx _ (fun (i : nat) (l : i < n) ⇒ g i (lt_S i n l)) [+] (f n (lt_n_Sn n) [+]g n (lt_n_Sn n))).
  set (Sf := Sumx _ (fun (i : nat) (l : i < n) ⇒ f i (lt_S i n l))) in ×.
  set (Sg := Sumx _ (fun (i : nat) (l : i < n) ⇒ g i (lt_S i n l))) in ×.
  set (fn := f n (lt_n_Sn n)) in *; set (gn := g n (lt_n_Sn n)) in ×.
  astepl (Sf[+]fn[+]Sg[+]gn).
  astepl (Sf[+] (fn[+]Sg) [+]gn).
  astepl (Sf[+] (Sg[+]fn) [+]gn).
  Step_final (Sf[+]Sg[+]fn[+]gn).
 apply bin_op_wd_unfolded; algebra.
Qed.

Lemma Sum2_plus_Sum2 : ∀ m n, m ≤ S n → ∀ f g,
 ∑2 m n f[+]∑2 m n g [=] ∑2 _ _ (fun i Hm Hn ⇒ f i Hm Hn[+]g i Hm Hn).
Proof.
 intros m n H f g.
 unfold ∑2 in |- *; simpl in |- ×.
 apply eq_symmetric_unfolded.
 eapply eq_transitive_unfolded.
  2: apply Sum_plus_Sum.
 apply Sum_wd; intro i.
 elim le_lt_dec; intro H0; simpl in |- *; elim le_lt_dec; intro H1; simpl in |- *; algebra.
Qed.

Lemma inv_Sum0 : ∀ f n, ∑0 n (fun i ⇒ [--] (f i)) [=] [--] (∑0 n f).
Proof.
 intros f n.
 induction n as [| n Hrecn].
  simpl in |- *; algebra.
 simpl in |- ×.
 Step_final ([--] (∑0 n f) [+] [--] (f n)).
Qed.

Hint Resolve inv_Sum0: algebra.

Lemma inv_Sum : ∀ f m n, ∑ m n (fun i ⇒ [--] (f i)) [=] [--] (∑ m n f).
Proof.
 intros f a b.
 unfold ∑ in |- ×.
 unfold ∑1 in |- ×.
 astepl ([--] (∑0 (S b) f) [-][--] (∑0 a f)).
 astepl ([--] (∑0 (S b) f) [+] [--][--] (∑0 a f)).
 Step_final ([--] (∑0 (S b) f[+] [--] (∑0 a f))).
Qed.

Hint Resolve inv_Sum: algebra.

Lemma inv_Sumx : ∀ n f, [--] (Sumx n f) [=] Sumx _ (fun i Hi ⇒ [--] (f i Hi)).
Proof.
 intro n; induction n as [| n Hrecn].
  simpl in |- *; algebra.
 intro f; simpl in |- ×.
 astepl ([--] (Sumx _ (fun i (l : i < n) ⇒ f i (lt_S i n l))) [+] [--] (f n (lt_n_Sn n))).
 apply bin_op_wd_unfolded.
  apply Hrecn with (f := fun i (l : i < n) ⇒ f i (lt_S i n l)).
 algebra.
Qed.

Lemma inv_Sum2 : ∀ m n : nat, m ≤ S n → ∀ f,
 [--] (∑2 m n f) [=] ∑2 _ _ (fun i Hm Hn ⇒ [--] (f i Hm Hn)).
Proof.
 intros m n H f.
 unfold ∑2 in |- *; simpl in |- ×.
 apply eq_symmetric_unfolded.
 eapply eq_transitive_unfolded.
  2: apply inv_Sum.
 apply Sum_wd; intro i.
 elim le_lt_dec; intro; simpl in |- *; elim le_lt_dec; intro; simpl in |- *; algebra.
Qed.

Lemma Sum_minus_Sum : ∀ f g m n, ∑ m n (fun i ⇒ f i[-]g i) [=] ∑ m n f[-]∑ m n g.
Proof.
 intros f g a b.
 astepl (∑ a b (fun i : nat ⇒ f i[+] [--] (g i))).
 cut (∑ a b (fun i : nat ⇒ f i[+] (fun j : nat ⇒ [--] (g j)) i) [=]
   ∑ a b f[+]∑ a b (fun j : nat ⇒ [--] (g j))).
  intro H.
  astepl (∑ a b f[+]∑ a b (fun j : nat ⇒ [--] (g j))).
  Step_final (∑ a b f[+] [--] (∑ a b g)).
 change (∑ a b (fun i : nat ⇒ f i[+] (fun j : nat ⇒ [--] (g j)) i) [=]
   ∑ a b f[+]∑ a b (fun j : nat ⇒ [--] (g j))) in |- ×.
 apply Sum_plus_Sum.
Qed.

Hint Resolve Sum_minus_Sum: algebra.

Lemma Sumx_minus_Sumx : ∀ n f g,
 Sumx n f[-]Sumx n g [=] Sumx _ (fun i Hi ⇒ f i Hi[-]g i Hi).
Proof.
 intros n f g; unfold cg_minus in |- ×.
 eapply eq_transitive_unfolded.
  2: apply Sumx_plus_Sumx with (f := f) (g := fun i (Hi : i < n) ⇒ [--] (g i Hi)).
 apply bin_op_wd_unfolded; algebra.
 apply inv_Sumx.
Qed.

Lemma Sum2_minus_Sum2 : ∀ m n, m ≤ S n → ∀ f g,
 ∑2 m n f[-]∑2 m n g [=] ∑2 _ _ (fun i Hm Hn ⇒ f i Hm Hn[-]g i Hm Hn).
Proof.
 intros m n H f g; unfold cg_minus in |- ×.
 eapply eq_transitive_unfolded.
  2: apply Sum2_plus_Sum2 with (f := f) (g := fun i (Hm : m ≤ i) (Hn : i ≤ n) ⇒ [--] (g i Hm Hn));
    assumption.
 apply bin_op_wd_unfolded.
  algebra.
 apply inv_Sum2; assumption.
Qed.

Lemma Sum_apzero : ∀ f m n,
 m ≤ n → ∑ m n f [#] [0] → {i : nat | m ≤ i ∧ i ≤ n | f i [#] [0]}.
Proof.
 intros a k l H H0. induction l as [| l Hrecl].
 ∃ 0. split; auto. cut (k = 0).
   intro H'. rewrite H' in H0.
   astepl (∑ 0 0 a). auto.
   inversion H. auto.
  elim (le_lt_eq_dec k (S l) H); intro HH.
  cut (∑ k l a [#] [0] or a (S l) [#] [0]). intro H1.
   elim H1; clear H1; intro H1.
    elim Hrecl; auto with arith.
    intro i. intros H2 H6. ∃ i; auto.
    elim H2; intros H3 H4; auto.
   ∃ (S l); try split; auto with arith.
  apply cg_add_ap_zero.
  apply ap_wdl_unfolded with (∑ k (S l) a). auto.
   apply Sum_last.
 rewrite HH in H0.
 ∃ (S l); auto.
 astepl (∑ (S l) (S l) a). auto.
Qed.

Lemma Sum_zero : ∀ f m n, m ≤ S n →
 (∀ i, m ≤ i → i ≤ n → f i [=] [0]) → ∑ m n f [=] [0].
Proof.
 intros a k l H H0. induction l as [| l Hrecl].
 elim (le_lt_eq_dec _ _ H); clear H; intro H.
   replace k with 0. astepl (a 0). apply H0. auto.
    auto with arith. auto. inversion H. auto. inversion H2.
    rewrite H.
  unfold ∑ in |- ×. unfold ∑1 in |- ×. algebra.
  elim (le_lt_eq_dec k (S (S l)) H); intro HH.
  astepl (∑ k l a[+]a (S l)).
  astepr ([0][+] ([0]:G)).
  apply bin_op_wd_unfolded.
   apply Hrecl; auto with arith.
  apply H0; auto with arith.
 rewrite HH.
 unfold ∑ in |- ×. unfold ∑1 in |- ×. algebra.
Qed.

Lemma Sum_term : ∀ f m i n, m ≤ i → i ≤ n →
 (∀ j, m ≤ j → j ≠ i → j ≤ n → f j [=] [0]) → ∑ m n f [=] f i.
Proof.
 intros a k i0 l H H0 H1.
 astepl (∑ k i0 a[+]∑ (S i0) l a).
 astepr (a i0[+][0]).
 apply bin_op_wd_unfolded.
  elim (O_or_S i0); intro H2.
   elim H2; intros m Hm.
   rewrite <- Hm.
   astepl (∑ k m a[+]a (S m)).
   astepr ([0][+]a (S m)).
   apply bin_op_wd_unfolded.
    apply Sum_zero. rewrite Hm; auto.
     intros i H3 H4. apply H1. auto. omega. omega.
    algebra.
  rewrite <- H2 in H. rewrite <- H2.
  inversion H. algebra.
  apply Sum_zero. auto with arith.
  intros. apply H1. omega. omega. auto.
Qed.

Lemma Sum0_shift : ∀ f g n, (∀ i, f i [=] g (S i)) → g 0[+]∑0 n f [=] ∑0 (S n) g.
Proof.
 intros a b l H. induction l as [| l Hrecl].
 simpl in |- *; algebra.
 simpl in |- ×.
 astepl (b 0[+]∑0 l a[+]a l).
 Step_final (∑0 (S l) b[+]a l).
Qed.

Hint Resolve Sum0_shift: algebra.

Lemma Sum_shift : ∀ f g m n,
 (∀ i, f i [=] g (S i)) → ∑ m n f [=] ∑ (S m) (S n) g.
Proof.
 unfold ∑ in |- ×. unfold ∑1 in |- ×. intros a b k l H.
 astepl (∑0 (S l) a[+]b 0[-]b 0[-]∑0 k a).
 astepl (∑0 (S l) a[+]b 0[-] (b 0[+]∑0 k a)).
 Step_final (b 0[+]∑0 (S l) a[-] (b 0[+]∑0 k a)).
Qed.

Lemma Sum_big_shift : ∀ f g k m n, (∀ j, m ≤ j → f j [=] g (j + k)) →
 m ≤ S n → ∑ m n f [=] ∑ (m + k) (n + k) g.
Proof.
 do 3 intro; generalize f g; clear f g.
 induction k as [| k Hreck].
  intros f g n m. repeat rewrite <- plus_n_O.
  intros H H0.
  apply: Sum_wd'. auto.
   intros. set (Hi:= H i). rewrite <- (plus_n_O i) in Hi. apply: Hi. auto.
  intros; repeat rewrite <- plus_n_Sm.
 apply eq_transitive_unfolded with (∑ (m + k) (n + k) (fun n : nat ⇒ g (S n))).
  2: apply Sum_shift; algebra.
 apply Hreck.
  intros; rewrite plus_n_Sm; apply H; auto with arith.
 auto.
Qed.

Lemma Sumx_Sum0 : ∀ n f g,
 (∀ i Hi, f i Hi [=] g i) → Sumx n f [=] ∑0 n g.
Proof.
 intro; induction n as [| n Hrecn]; simpl in |- *; algebra.
Qed.

End Sums.

Implicit Arguments ∑ [G].
Implicit Arguments ∑0 [G].
Implicit Arguments Sumx [G n].
Implicit Arguments ∑2 [G m n].

The next results are useful for calculating some special sums, often referred to as ``Mengolli Sums''. Let G be an abelian group.

Section More_Sums.

Variable G : CAbGroup.

Lemma Mengolli_Sum : ∀ n (f : ∀ i, i ≤ n → G) (g : ∀ i, i < n → G),
 nat_less_n_fun' f → (∀ i H, g i H [=] f (S i) H[-]f i (lt_le_weak _ _ H)) →
 Sumx g [=] f n (le_n n) [-]f 0 (le_O_n n).
Proof.
 intro n; induction n as [| n Hrecn]; intros f g Hf H; simpl in |- ×.
  astepl (f 0 (le_n 0) [-]f 0 (le_n 0)).
  apply cg_minus_wd; algebra.
 apply eq_transitive_unfolded with (f _ (le_n (S n)) [-]f _ (le_S _ _ (le_n n)) [+]
   (f _ (le_S _ _ (le_n n)) [-]f 0 (le_O_n (S n)))).
  eapply eq_transitive_unfolded.
   apply cag_commutes_unfolded.
  apply bin_op_wd_unfolded.
   eapply eq_transitive_unfolded.
    apply H.
   apply cg_minus_wd; apply Hf; algebra.
  set (f' := fun i (H : i ≤ n) ⇒ f i (le_S _ _ H)) in ×.
  set (g' := fun i (H : i < n) ⇒ g i (lt_S _ _ H)) in ×.
  apply eq_transitive_unfolded with (f' n (le_n n) [-]f' 0 (le_O_n n)).
   apply Hrecn.
    red in |- *; intros; unfold f' in |- *; apply Hf; algebra.
   intros i Hi.
   unfold f' in |- *; unfold g' in |- ×.
   eapply eq_transitive_unfolded.
    apply H.
   apply cg_minus_wd; apply Hf; algebra.
  unfold f' in |- *; apply cg_minus_wd; apply Hf; algebra.
 astepr (f (S n) (le_n (S n)) [+][0][-]f 0 (le_O_n (S n))).
 astepr (f (S n) (le_n (S n)) [+] ([--] (f n (le_S _ _ (le_n n))) [+]f n (le_S _ _ (le_n n))) [-]
   f 0 (le_O_n (S n))).
 Step_final (f (S n) (le_n (S n)) [+] [--] (f n (le_S _ _ (le_n n))) [+]
   f n (le_S _ _ (le_n n)) [-]f 0 (le_O_n (S n))).
Qed.

Lemma Mengolli_Sum_gen : ∀ f g : nat → G, (∀ n, g n [=] f (S n) [-]f n) →
 ∀ m n, m ≤ S n → ∑ m n g [=] f (S n) [-]f m.
Proof.
 intros f g H m n; induction n as [| n Hrecn]; intro Hmn.
  elim (le_lt_eq_dec _ _ Hmn); intro H0.
   cut (m = 0); [ intro H1 | inversion H0; auto with arith; inversion H2 ].
   rewrite H1.
   eapply eq_transitive_unfolded; [ apply Sum_one | apply H ].
  cut (0 = pred 1); [ intro H1 | auto ].
  rewrite H0; astepr ([0]:G); rewrite H1; apply Sum_empty.
  auto with arith.
 simpl in Hmn; elim (le_lt_eq_dec _ _ Hmn); intro H0.
  apply eq_transitive_unfolded with (f (S (S n)) [-]f (S n) [+] (f (S n) [-]f m)).
   eapply eq_transitive_unfolded.
    apply Sum_last.
   eapply eq_transitive_unfolded.
    apply cag_commutes_unfolded.
   apply bin_op_wd_unfolded; [ apply H | apply Hrecn ].
   auto with arith.
  astepr (f (S (S n)) [+][0][-]f m).
  astepr (f (S (S n)) [+] ([--] (f (S n)) [+]f (S n)) [-]f m).
  Step_final (f (S (S n)) [+] [--] (f (S n)) [+]f (S n) [-]f m).
 rewrite H0.
 astepr ([0]:G).
 cut (S n = pred (S (S n))); [ intro H2 | auto ].
 rewrite H2; apply Sum_empty.
 auto with arith.
Qed.

Lemma str_Mengolli_Sum_gen : ∀ (f g : nat → G) m n, m ≤ S n →
 (∀ i, m ≤ i → i ≤ n → g i [=] f (S i) [-]f i) → ∑ m n g [=] f (S n) [-]f m.
Proof.
 intros f g m n H H0.
 apply eq_transitive_unfolded with (∑ m n (fun i : nat ⇒ f (S i) [-]f i)).
  apply Sum_wd'; assumption.
 apply Mengolli_Sum_gen; [ intro; algebra | assumption ].
Qed.

Lemma Sumx_to_Sum : ∀ n, 0 < n → ∀ f, nat_less_n_fun f →
 Sumx f [=] ∑ 0 (pred n) (part_tot_nat_fun G n f).
Proof.
 intro n; induction n as [| n Hrecn]; intros H f Hf.
  elimtype False; inversion H.
 cut (0 ≤ n); [ intro H0 | auto with arith ].
 elim (le_lt_eq_dec _ _ H0); clear H H0; intro H.
  simpl in |- ×.
  pattern n at 6 in |- *; rewrite → (S_pred _ _ H).
  eapply eq_transitive_unfolded.
   2: apply eq_symmetric_unfolded; apply Sum_last.
  apply bin_op_wd_unfolded.
   eapply eq_transitive_unfolded.
    apply Hrecn; auto.
    red in |- *; intros; apply Hf; auto.
   apply Sum_wd'.
    auto with arith.
   intros i H1 H2.
   cut (i < n); [ intro | omega ].
   eapply eq_transitive_unfolded.
    apply part_tot_nat_fun_ch1 with (Hi := H0).
    red in |- *; intros; apply Hf; auto.
   apply eq_symmetric_unfolded.
   eapply eq_transitive_unfolded.
    apply part_tot_nat_fun_ch1 with (Hi := lt_S _ _ H0).
    red in |- *; intros; apply Hf; auto.
   algebra.
  rewrite <- (S_pred _ _ H).
  apply eq_symmetric_unfolded; apply part_tot_nat_fun_ch1; auto.
 generalize f Hf; clear Hf f; rewrite <- H.
 simpl in |- *; intros f Hf.
 eapply eq_transitive_unfolded.
  2: apply eq_symmetric_unfolded; apply Sum_one.
 astepl (f 0 (lt_n_Sn 0)).
 apply eq_symmetric_unfolded; apply part_tot_nat_fun_ch1; auto.
Qed.

End More_Sums.

Hint Resolve Sum_one Sum_Sum Sum_first Sum_last Sum_last' Sum_wd
  Sum_plus_Sum: algebra.
Hint Resolve Sum_minus_Sum inv_Sum inv_Sum0: algebra.