## Stream: general

### Topic: finite sum puzzle

#### Kevin Buzzard (Mar 29 2018 at 23:53):

import tactic.ring

theorem  finset_sum_is_list_sum (f : ℕ → ℕ) (n : ℕ) :
(finset.range n).sum f = ((list.range n).map f).sum :=  sorry


#### Kevin Buzzard (Mar 29 2018 at 23:53):

I've been thinking a lot about induction today.

#### Kevin Buzzard (Mar 29 2018 at 23:54):

@Mario Carneiro Is there some super-cute way of doing this already?

#### Kevin Buzzard (Mar 29 2018 at 23:55):

I have been trying to formalise quite an abstract approach to questions like these but for all I know this sort of thing is completely well-known. Note that a mathematician would say this proof was trivial and indeed it would be hard to explain to a mathematician why this needed a proof.

#### Mario Carneiro (Mar 29 2018 at 23:56):

It should be by definition, more or less

#### Mario Carneiro (Mar 29 2018 at 23:57):

does rfl work?

#### Mario Carneiro (Mar 29 2018 at 23:58):

Also, of course that needs a proof, stop thinking that proofs that are simple by induction are trivial enough to not need a proof

#### Ching-Tsun Chou (Mar 29 2018 at 23:58):

Don't you need the commutativity of "+" on natural numbers?

#### Mario Carneiro (Mar 29 2018 at 23:58):

that's on the same lines as saying commutativity of natural numbers is trivial

#### Mario Carneiro (Mar 30 2018 at 00:03):

Ah, it's not quite by definition, because multiset prod is not defined in terms of list prod but instead is defined using foldl. This works:

theorem finset_sum_is_list_sum (f : ℕ → ℕ) (n : ℕ) :
(finset.range n).sum f = ((list.range n).map f).sum :=
multiset.coe_sum _


#### Mario Carneiro (Mar 30 2018 at 00:05):

Here's a slightly less magical way to write it:

theorem finset_sum_is_list_sum (f : ℕ → ℕ) (n : ℕ) :
(finset.range n).sum f = ((list.range n).map f).sum :=
show ((list.range n).map f : multiset ℕ).sum = ((list.range n).map f).sum, from
multiset.coe_sum _


#### Kevin Buzzard (Mar 30 2018 at 00:06):

f can map to an add_comm_monoid

sure

#### Kevin Buzzard (Mar 30 2018 at 00:07):

that's what you need, I believe.

#### Mario Carneiro (Mar 30 2018 at 00:07):

the theorem you stated is not maximally general

#### Kevin Buzzard (Mar 30 2018 at 00:07):

So this one seems genuinely easier than Chris' problem?

#### Mario Carneiro (Mar 30 2018 at 00:08):

yes, because finset sum is defined as a multiset sum over the map

#### Kevin Buzzard (Mar 30 2018 at 00:15):

Here's three more trivial statements:

#### Kevin Buzzard (Mar 30 2018 at 00:15):

import tactic.ring
universe u
open nat

theorem list_range_map_sum_induction {X : Type u} [has_add X] [has_zero X] {n : ℕ} (f : ℕ → X) :
((list.range (succ n)).map f).sum = ((list.range n).map f).sum + f n := sorry

theorem finset_range_sum_induction {R : Type u} [add_comm_monoid R] {f : ℕ → R} {d : ℕ} :
(finset.range (succ d)).sum f = (finset.range d).sum f + f d := sorry

theorem finset_univ_sum_fin_induction {R : Type u} [add_comm_monoid R] {d : ℕ}
{f : fin (nat.succ d) → R} :
finset.univ.sum f =
finset.univ.sum (λ i : fin d, f ⟨i.val,lt_trans i.is_lt $nat.lt_succ_self d⟩) -- d or _? + f ⟨d,nat.lt_succ_self _⟩ -- is _ or d better style at the end? := sorry  #### Kevin Buzzard (Mar 30 2018 at 00:16): They all say the same trivial thing in maths #### Kevin Buzzard (Mar 30 2018 at 00:16): so I am really interested in the slickest possible proofs in Lean #### Kevin Buzzard (Mar 30 2018 at 00:17): because I suspect that occasionally my students will want statements like this to just go away #### Kevin Buzzard (Mar 30 2018 at 00:18): If these get unsorried then we get the following proof of Chris' problem from yesterday: #### Kevin Buzzard (Mar 30 2018 at 00:19): theorem chris_example (n : ℕ) (f : ℕ → ℕ) (g : fin n → ℕ) (h : ∀ i : fin n, f i.1 = g i) : (finset.range n).sum f = finset.univ.sum g := begin induction n with d Hd, refl, -- base case trivial -- for the inductive step it's handy to have notation for the restriction of g, let gres : fin d → ℕ := λ i,g ⟨i.val,lt_trans i.is_lt$ nat.lt_succ_self d⟩,
-- goal now of form "first kind of sum to succ d equals second kind"
rw finset_range_sum_induction,
rw finset_univ_sum_fin_induction,
-- goal now "first sum to d + f d = second sum to d + g d"
rw [(Hd gres (λ i, h ⟨i.val,_⟩))], -- first sum equals second sum
rw h ⟨d,_⟩, -- f d = g d -- so done
end


#### Kevin Buzzard (Mar 30 2018 at 00:19):

with not a pmap in sight

#### Kevin Buzzard (Mar 30 2018 at 00:21):

I would argue that this was a "natural" proof which hides away the abstraction.

#### Kevin Buzzard (Mar 30 2018 at 00:23):

@Chris Hughes Here's what another proof of your fin n question might look like.

#### Mario Carneiro (Mar 30 2018 at 00:23):

By the way, here's a(nother) proof of chris's theorem:

example (n : ℕ) (f : ℕ → ℕ) (g : fin n → ℕ) (h : ∀ i : fin n, f i.1 = g i) :
(finset.range n).sum f = finset.univ.sum g :=
show ((list.range n).map f : multiset ℕ).sum =
(((list.range n).pmap fin.mk _).map g : multiset ℕ).sum,
by rw [multiset.coe_sum, multiset.coe_sum, ← (funext h : _ = g),
list.map_pmap, ← list.pmap_eq_map]


#### Kevin Buzzard (Mar 30 2018 at 00:26):

What I don't like about your proofs is that they seem (to me) to involve knowing about some internal implementation of things. My proof is implementation-free. The library maintainer just creates those blah_sum_induction proofs (the three things sorried above) , and then the end user can construct proofs of Chris' theorem without having to worry about any other implementation.

#### Kevin Buzzard (Mar 30 2018 at 00:26):

Each of the induction laws gives rise to an abstraction which looks like this:

#### Mario Carneiro (Mar 30 2018 at 00:26):

I agree, chris has found a hole in the mathlib coverage here

#### Mario Carneiro (Mar 30 2018 at 00:27):

Your second theorem is provable by simp, but list.range doesn't break up nicely because the numbers are listed in increasing order

#### Mario Carneiro (Mar 30 2018 at 00:29):

I'm not a big fan of your statement of finset_univ_sum_fin_induction, it's all too complicated in the theorem statement

#### Kevin Buzzard (Mar 30 2018 at 00:29):

@[reducible] definition sum_map_range {R : Type u} [add_comm_monoid R] (addend : ℕ → R) : ℕ → R
| zero := (0 : R)
| (succ n) := sum_map_range n + addend n

theorem list_range_map_sum_abstraction {R : Type} [add_comm_monoid R]
(f : ℕ → R) (n : ℕ) : ((list.range n).map f).sum = sum_map_range f n := sorry

theorem finset_range_sum_abstraction {R : Type u} [add_comm_monoid R] (f : ℕ → R) (n : ℕ) :
(finset.range n).sum f = sum_map_range f n := sorry

theorem finset_univ_sum_fin_abstraction {R : Type u} [add_comm_monoid R] (f : ℕ → R) (n : ℕ) :
finset.univ.sum (λ i : fin n, f(i.val)) = sum_map_range f n := sorry


#### Kevin Buzzard (Mar 30 2018 at 00:29):

yes, the fin one stinks.

#### Kevin Buzzard (Mar 30 2018 at 00:30):

If you use lists or finsets then f is a function on N, but to do Chris' problem you had to use a function on fin n

#### Mario Carneiro (Mar 30 2018 at 00:30):

I think there are functions for raising fin n to fin (n+1). Alternatively, you could use fin2, which has a natural inductive construction instead of being a subtype of nat

#### Mario Carneiro (Mar 30 2018 at 00:31):

fin2 is not really developed much, but it is defined in dioph.lean

#### Kevin Buzzard (Mar 30 2018 at 00:32):

I specifically wanted to design functions which gave me the biggest chance of being covered for all variants of the following question:"this Lean statement is trivially true in maths because it says $f(0)+f(1)+\cdots+f(n-1)=f(0)+f(1)+\cdots+f(n-1)$, so how do you prove it in Lean?"

#### Kevin Buzzard (Mar 30 2018 at 00:33):

I feel like I have convinced myself that for any way of representing the set $\{0,1,...,n-1\}$ in Lean

#### Kevin Buzzard (Mar 30 2018 at 00:33):

there is an induction principle and an abstraction principle.

#### Kevin Buzzard (Mar 30 2018 at 00:33):

Do I have the right names for these things?

#### Kevin Buzzard (Mar 30 2018 at 00:35):

As you can see, the examples I have attempted to work out are list.range n, fin n and finset.range n

#### Kevin Buzzard (Mar 30 2018 at 00:36):

Sounds like I need to do fin2 n

#### Kevin Buzzard (Mar 30 2018 at 00:36):

I should say that I have not proved the induction hypotheses in all cases yet.

#### Mario Carneiro (Mar 30 2018 at 00:36):

It's mostly used for technical reasons; you can also define recursion principles on fin n with the same structure as fin2

#### Mario Carneiro (Mar 30 2018 at 00:37):

but I think that fz and fs are the right way to think about induction on fin n

#### Kevin Buzzard (Mar 30 2018 at 00:37):

But as a mathematician I would find a proof of these sorts of thing rather distasteful (they're all "obvious by induction")

#### Kevin Buzzard (Mar 30 2018 at 00:38):

so I feel like they should be hidden from view.

#### Mario Carneiro (Mar 30 2018 at 00:38):

It's always messy when the function is only partially defined, so that you can't even talk about it out of domain

#### Mario Carneiro (Mar 30 2018 at 00:38):

that's what makes list.pmap necessary, and also what makes it a pain to work with

#### Mario Carneiro (Mar 30 2018 at 00:39):

What makes Chris's problem hard is the usage of g : fin n -> N

#### Mario Carneiro (Mar 30 2018 at 00:39):

same for your induction principle, fin (succ n) -> N is even worse

#### Mario Carneiro (Mar 30 2018 at 00:40):

I get the sense that you want to put everything in the form map_sum_range of something, but that doesn't work for partial functions

Here's a 4th one

#### Kevin Buzzard (Mar 30 2018 at 00:45):

theorem multiset_sum_map_range_induction {X : Type u} [add_comm_monoid X] {n : ℕ} (f : ℕ → X) :
((multiset.range (succ n)).map f).sum =
((multiset.range n).map f).sum + f n := sorry


#### Kevin Buzzard (Mar 30 2018 at 00:46):

Corresponding to $\{0,1,\ldots,n-1\}$ = multiset.range n

#### Kevin Buzzard (Mar 30 2018 at 00:46):

Each model gives you a new induction principle

#### Kevin Buzzard (Mar 30 2018 at 00:47):

which I think mathlib could offer with a standard name

#### Kevin Buzzard (Mar 30 2018 at 00:48):

There are only a finite number of ways that a mathematician can say this trivial thing, and it would be nice if we could just pull a proof out of a hat for each one.

#### Kevin Buzzard (Mar 30 2018 at 00:48):

Could I even write a tactic which proves all these things? Just in some stupid way -- it just tries all the proofs and chooses the one that works.

#### Kevin Buzzard (Mar 30 2018 at 00:49):

aah, simp works on that one.

#### Mario Carneiro (Mar 30 2018 at 00:50):

I support the definition of your map_sum_range, which I and I think chris called series; it's on my to do list

#### Mario Carneiro (Mar 30 2018 at 00:50):

That would make your multiset_sum_map_range_induction theorem, which I might otherwise call multiset.range_succ_map_sum, just series_succ

#### Mario Carneiro (Mar 30 2018 at 00:51):

It's not called induction because it's not an induction principle

#### Mario Carneiro (Mar 30 2018 at 00:53):

As I've said, I think it will alleviate many of the issues you are having with these sums. If you urgently need it, why not try writing it yourself? Don't worry about connecting it to finset.range, just prove everything directly by induction. Then we can relate it to the other ways to talk about finite sums

#### Kevin Buzzard (Mar 30 2018 at 00:54):

simp does the multiset and finset variants, but not the list variant.

#### Kevin Buzzard (Mar 30 2018 at 00:55):

Can you tell me exactly what you are suggesting I prove? I am interested in getting this done ASAP and I have some time now, term finished.

#### Kevin Buzzard (Mar 30 2018 at 00:56):

I think your sketches above should enable me to prove everything

#### Kevin Buzzard (Mar 30 2018 at 00:57):

Sorry about the induction name. I thought carefully about the abstract syntax of the names but I seem to have used the wrong term.

#### Kevin Buzzard (Mar 30 2018 at 01:03):

I love dioph.lean

#### Kevin Buzzard (Mar 30 2018 at 01:03):

(D∃4 $D∃5$ D∃6 $D∃7$ D∃8 \$
D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧


#### Kevin Buzzard (Mar 30 2018 at 01:03):

who could fail to love that bit

#### Kevin Buzzard (Mar 30 2018 at 01:04):

whatever is going on in that file

#### Mario Carneiro (Mar 30 2018 at 01:07):

That's the closest lean comes to a domain specific language right now

#### Kevin Buzzard (Mar 30 2018 at 01:09):

So there is vector and vector3. Is there a vector2? I can't find it. (fin2 is used to build vector3)

#### Kevin Buzzard (Mar 30 2018 at 01:10):

I have a Masters student working on Matiesevich's theorem for their project, so I showed them dioph.lean. They know no Lean. I'm not sure they found it very helpful.

#### Mario Carneiro (Mar 30 2018 at 01:11):

There was once a vector2, but I deleted it because it wasn't needed. vector2 was inductively defined by

inductive vector2 (A : Type u) : nat -> Type u
| nil : vector2 0
| cons (n) : A -> vector2 n -> vector2 (succ n)


#### Mario Carneiro (Mar 30 2018 at 01:12):

From the names, you can guess that vector, vector2 and vector3 are all isomorphic

#### Mario Carneiro (Mar 30 2018 at 01:13):

I think you can find it in the file history of dioph.lean

#### Kevin Buzzard (Mar 30 2018 at 01:55):

I can't believe it. I feel like I have learnt something new about induction today, and I have been teaching it for 20 years.

what is it?

#### Kenny Lau (Mar 30 2018 at 01:56):

well there's always more to learn :P

#### Kevin Buzzard (Mar 30 2018 at 01:56):

yes but I'm usually trying to look nearer the top

#### Kevin Buzzard (Mar 30 2018 at 01:59):

There is one abstract principle of induction g := lam n, sum_to_n f

#### Kevin Buzzard (Mar 30 2018 at 02:00):

which you can prove assuming a hypothesis of the form \forall n, g (succ n) = g n + f n

#### Kevin Buzzard (Mar 30 2018 at 02:01):

but the problem is that there are several ways to encode sum_to_nin Lean

#### Kevin Buzzard (Mar 30 2018 at 02:01):

e.g. the "pure" way via an inductive type

#### Kevin Buzzard (Mar 30 2018 at 02:02):

or ways which create an auxiliary type along the way, like sum_to_n f = ((list.range n).map f).sum which at some point builds a list and then sums over it

#### Kevin Buzzard (Mar 30 2018 at 02:06):

and for each of these design decisions about how you're going to sum this series (e.g. a design decision that some other program has forced upon you) you are given a definition of sum_to_n : (ℕ → R) → (ℕ → R)

#### Kevin Buzzard (Mar 30 2018 at 02:07):

(e.g. λ f, λ n ((list.range n).map f).sum )

#### Kevin Buzzard (Mar 30 2018 at 02:08):

it's now your job to prove ∀ n, sum_to_n (succ n) = sum_to_n n + f n

#### Kevin Buzzard (Mar 30 2018 at 02:12):

And that's quite annoying because list doesn't deconstruct like that.

#### Kenny Lau (Mar 30 2018 at 02:24):

@Kevin Buzzard do you have a list of goals?

#### Kevin Buzzard (Mar 30 2018 at 02:25):

I'm writing a blog post about it. This has been a most enjoyable day.

#### Kenny Lau (Mar 30 2018 at 02:34):

it's now your job to prove ∀ n, sum_to_n (succ n) = sum_to_n n + f n

done

#### Kenny Lau (Mar 30 2018 at 02:34):

theorem sum_to_n.succ : sum_to_n (n+1) = sum_to_n n + f n :=
begin
dsimp [sum_to_n],
rw [list.range_concat],
rw [list.map_append],
rw [list.sum_append],
rw [list.map_singleton],
rw [list.sum_cons],
rw [list.sum_nil],
end


version 2

#### Kenny Lau (Mar 30 2018 at 02:42):

theorem sum_to_n.succ : sum_to_n (n+1) = sum_to_n n + f n :=
by simp [sum_to_n, list.range_concat]


#### Kevin Buzzard (Mar 30 2018 at 05:24):

https://wordpress.com/post/xenaproject.wordpress.com/1344

#### Kenny Lau (Mar 30 2018 at 05:29):

@Kevin Buzzard did you sleep?

#### Kevin Buzzard (Mar 30 2018 at 05:30):

@Chris Hughes or @Kenny Lau Feel free to leave comments if you have definitions for sum_to_n

#### Andrew Ashworth (Mar 30 2018 at 05:30):

but, unfortunately, because I fear that in practice people really might occasionally find themselves in a situation where they need a new kind of proof by induction

writing new recursion principles is common and expected, from what i've seen out there

#### Kenny Lau (Mar 30 2018 at 05:32):

“using the fucking ring tactic”

#### Andrew Ashworth (Mar 30 2018 at 05:34):

you can see some of this in mathlib, where new elimination lemmas are defined fairly frequently

#### Andrew Ashworth (Mar 30 2018 at 05:34):

if we go back to the nats, strong induction is commonplace yet requires a proof

#### Kevin Buzzard (Mar 30 2018 at 05:37):

In lean web editor link, tactic.ring is not available so I had to prove it the old skool way! Thank you @Mario Carneiro for tactic.ring. No, it appears I didn't go to sleep and now the sun is up. Crap. I'm behaving like a kid.

lol

i am shocked

#### Kevin Buzzard (Mar 30 2018 at 05:38):

writing new recursion principles is common and expected, from what i've seen out there

I realised that Chris could solve his problem with good recursion principles.

#### Kevin Buzzard (Mar 30 2018 at 05:39):

I don't have to be up at 7am though, because the kids have finished school now.

#### Kenny Lau (Mar 30 2018 at 05:39):

so the philosophy is to always write eliminators for the things you create?

#### Kevin Buzzard (Mar 30 2018 at 05:39):

If I don't get my act together I'll be up at 7am anyway.

#### Kevin Buzzard (Mar 30 2018 at 05:39):

I guess that might be what I am saying.

#### Andrew Ashworth (Mar 30 2018 at 05:39):

also as a matter of style, you could give names to your function variables as opposed to always lambda-ing them

#### Kevin Buzzard (Mar 30 2018 at 05:39):

Or some version of this.

#### Kenny Lau (Mar 30 2018 at 05:39):

i am still shocked :stuck_out_tongue:

#### Andrew Ashworth (Mar 30 2018 at 05:40):

for example def square : ℕ → ℕ := λ i, i ^ 2  could be def square n : nat := n ^ 2

#### Kenny Lau (Mar 30 2018 at 05:40):

fin has no eliminator though

#### Kenny Lau (Mar 30 2018 at 05:40):

hence the problem

#### Kevin Buzzard (Mar 30 2018 at 05:40):

yes, my approach with fin was not much fun.

#### Kevin Buzzard (Mar 30 2018 at 05:41):

But I need to sleep.

#### Kenny Lau (Mar 30 2018 at 05:41):

@Andrew Ashworth I think he decided he does not care about styles

#### Kevin Buzzard (Mar 30 2018 at 05:41):

I just wrote it in the way that appealed to me most.

#### Kevin Buzzard (Mar 30 2018 at 05:41):

I have also written three solutions to the problems.

#### Andrew Ashworth (Mar 30 2018 at 05:41):

when you're a professor, you can write your homework exercises however you like, haha

#### Kevin Buzzard (Mar 30 2018 at 05:42):

One of them is just "axiom axiom constant" etc etc, and it's very cool, you can still do the last part :-)

#### Kenny Lau (Mar 30 2018 at 05:42):

constant name : false

#### Kenny Lau (Mar 30 2018 at 05:42):

theorem RH : sorry := false.elim name

#### Kevin Buzzard (Mar 30 2018 at 05:42):

I might be a professor but I am still very much a learner at this game. I'd be happy for any more stylistic comments.

#### Andrew Ashworth (Mar 30 2018 at 05:44):

it's only really meaningful in large, complicated definitions

#### Andrew Ashworth (Mar 30 2018 at 05:44):

of which square does not count

#### Andrew Ashworth (Mar 30 2018 at 05:44):

i will continue to file nitpicking issues if i see them, though

#### Andrew Ashworth (Mar 30 2018 at 06:01):

actually later on you give summand a nice name so i take back everything i wrote, haha

#### Kevin Buzzard (Mar 30 2018 at 06:02):

In fact my initial draft had an error in which I only spotted when I tried to prove that my genuine summing function was equal the one I defined with constants and axioms

#### Chris Hughes (Mar 30 2018 at 10:08):

@Kevin Buzzard I did define sums and sums between nats here. https://github.com/dorhinj/lean/blob/master/sum_between_nats.lean The proofs aren't mathlib ready and I don't think series is a particularly good name. I proved various basic properties as well.

Last updated: May 11 2021 at 22:14 UTC