Ryan Shao (Mar 20 2023 at 14:09): Ryan Shao (Mar 20 2023 at 14:09):I want to show fold (+) (map (λy. k choose y) [0..<Suc(k)]) 0 = (∑j≤k. k choose j). The method of proof I came up with is showing that there's a bijection between the list on the LHS and the set on the RHS, and then showing that the fold(+) (with identity 0) and Sum functions are equivalent. How do I do this, or how else can I approach the problem?
Jan van Brügge (Mar 20 2023 at 14:24):My intuition is to prove this by induction on k, but I think you have an error in the equality. j only appears on the right, I guess you wanted to use it in the lower bound in the list on the left as well?
Ryan Shao (Mar 20 2023 at 14:32):I might be wrong, but my idea was the (map (λy. k choose y) [0..<Suc(k)])) evaluates to [k choose 0, k choose 1 ... k choose k]. The summation on the right is also these elements. In particular, I thought the j <= k notation meant summing from 0 to k.
I don't think induction works (neatly) because the only equality I'm familiar with for going from (n choose m) to (n + 1 choose m) is ((n + 1) choose m) = n choose m + n choose (m - 1). I think it's possible to prove it this way, but I thought there would be a much simpler way because the terms on each side are all equal.
Maximilian Schaeffeler (Mar 20 2023 at 16:23):I used a helper lemma that shows fold (+) (map f xs) c = c + (∑i ∈ set xs. f i) when distinct xs.
Last updated: Apr 25 2024 at 20:15 UTC