list.alternating_sum

Stream: general

[Johan Commelin]

import tactic
import data.fintype.card

namespace list

/-- The alternating sum of elements in a list. -/
def alternating_sum {G : Type*} [add_group G] : list G → G
| [] := 0
| (g :: []) := g
| (g :: h :: t) := g - h + alternating_sum t

open_locale big_operators

lemma alternating_sum_eq_finset_sum {R : Type*} [ring R] : ∀ (L : list R),
  alternating_sum L = ∑ i : fin L.length, (-1 : R) ^ (i : ℕ) * L.nth_le i i.2
| [] := by { rw [alternating_sum, finset.sum_eq_zero], rintro ⟨i, ⟨⟩⟩ }
| (g :: []) :=
begin
  rw [alternating_sum, finset.sum_eq_single (⟨0, dec_trivial⟩ : fin [g].length)],
  { simp, },
  { rintro ⟨i, hi⟩ h' h0, exfalso, apply h0, ext, dsimp at *, linarith },
  { intro h, exfalso, exact h (finset.mem_univ _) }
end
| (g :: h :: L) :=
calc g - h + L.alternating_sum
    = g - h + ∑ i : fin L.length, (-1 : R) ^ (i : ℕ) * L.nth_le i i.2 :
      congr_arg _ (alternating_sum_eq_finset_sum _)
... = ∑ i : fin (L.length + 2), (-1 : R) ^ (i : ℕ) * list.nth_le (g :: h :: L) i _ :
begin
  rw [fin.sum_univ_succ, fin.sum_univ_succ, sub_eq_add_neg, add_assoc],
  unfold_coes,
  simp [nat.succ_eq_add_one, pow_add]; refl,
end

end list

[Johan Commelin]

This gives me an error I haven't seen before

[Johan Commelin]

unexpected occurrence of recursive function

[Reid Barton]

Probably because simp used _fun_match or something.

[Johan Commelin]

Ooh, ok

[Johan Commelin]

open_locale big_operators
lemma alternating_sum_eq_finset_sum {R : Type*} [ring R] : ∀ (L : list R),
  alternating_sum L = ∑ i : fin L.length, (-1 : R) ^ (i : ℕ) * L.nth_le i i.2
| [] := by { rw [alternating_sum, finset.sum_eq_zero], rintro ⟨i, ⟨⟩⟩ }
| (g :: []) :=
begin
  rw [alternating_sum, finset.sum_eq_single (⟨0, dec_trivial⟩ : fin [g].length)],
  { show g = (-1:R)^0 * [g].nth_le 0 _, rw [pow_zero, one_mul], refl, },
  { rintro ⟨i, hi⟩ h' h0, exfalso, apply h0, ext, dsimp at *,
    clear h0 h',
    cases i, { refl }, { revert hi, exact dec_trivial -- this is the culprit
     } },
  { intro h, exfalso, exact h (finset.mem_univ _) }
end
| (g :: h :: L) :=
calc g - h + L.alternating_sum
    = g - h + ∑ i : fin L.length, (-1 : R) ^ (i : ℕ) * L.nth_le i i.2 :
      congr_arg _ (alternating_sum_eq_finset_sum _)
... = ∑ i : fin (L.length + 2), (-1 : R) ^ (i : ℕ) * list.nth_le (g :: h :: L) i _ :
begin
  rw [fin.sum_univ_succ, fin.sum_univ_succ, sub_eq_add_neg, add_assoc],
  unfold_coes,
  simp [nat.succ_eq_add_one, pow_add]; refl,
end

[Johan Commelin]

Somehow I'm not allowed to use hypothesis hi

[Johan Commelin]

this is crazy... I have an innocent i < 1 hypothesis, and lean will not allow me to mention it.

[Johan Commelin]

I "worked my way around it"

lemma alternating_sum_eq_finset_sum {R : Type*} [ring R] : ∀ (L : list R),
  alternating_sum L = ∑ i : fin L.length, (-1 : R) ^ (i : ℕ) * L.nth_le i i.2
| [] := by { rw [alternating_sum, finset.sum_eq_zero], rintro ⟨i, ⟨⟩⟩ }
| (g :: []) :=
begin
  show g = ∑ i : fin 1, (-1 : R) ^ (i : ℕ) * [g].nth_le i i.2,
  rw [fin.sum_univ_succ], simp,
end
| (g :: h :: L) :=
calc g - h + L.alternating_sum
    = g - h + ∑ i : fin L.length, (-1 : R) ^ (i : ℕ) * L.nth_le i i.2 :
      congr_arg _ (alternating_sum_eq_finset_sum _)
... = ∑ i : fin (L.length + 2), (-1 : R) ^ (i : ℕ) * list.nth_le (g :: h :: L) i _ :
begin
  rw [fin.sum_univ_succ, fin.sum_univ_succ, sub_eq_add_neg, add_assoc],
  unfold_coes,
  simp [nat.succ_eq_add_one, pow_add]; refl,
end

[Johan Commelin]

@Scott Morrison Shall I push this to your PR?

[Johan Commelin]

done