finite sum puzzle

Stream: general

[Kevin Buzzard]

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]

I've been thinking a lot about induction today.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

It should be by definition, more or less

[Mario Carneiro]

does rfl work?

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

f can map to an add_comm_monoid

[Mario Carneiro]

sure

[Kevin Buzzard]

that's what you need, I believe.

[Mario Carneiro]

the theorem you stated is not maximally general

[Kevin Buzzard]

So this one seems genuinely easier than Chris' problem?

[Mario Carneiro]

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

[Kevin Buzzard]

Here's three more trivial statements:

[Kevin Buzzard]

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]

They all say the same trivial thing in maths

[Kevin Buzzard]

so I am really interested in the slickest possible proofs in Lean

[Kevin Buzzard]

because I suspect that occasionally my students will want statements like this to just go away

[Kevin Buzzard]

If these get unsorried then we get the following proof of Chris' problem from yesterday:

[Kevin Buzzard]

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]

with not a pmap in sight

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

@[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]

yes, the fin one stinks.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

there is an induction principle and an abstraction principle.

[Kevin Buzzard]

Do I have the right names for these things?

[Kevin Buzzard]

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

[Kevin Buzzard]

Sounds like I need to do fin2 n

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

so I feel like they should be hidden from view.

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Here's a 4th one

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Each model gives you a new induction principle

[Kevin Buzzard]

which I think mathlib could offer with a standard name

[Kevin Buzzard]

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]

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]

aah, simp works on that one.

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

I think your sketches above should enable me to prove everything

[Kevin Buzzard]

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]

I love dioph.lean

[Kevin Buzzard]

(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]

who could fail to love that bit

[Kevin Buzzard]

whatever is going on in that file

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kenny Lau]

what is it?

[Kenny Lau]

well there's always more to learn :P

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

@Kevin Buzzard do you have a list of goals?

[Kevin Buzzard]

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

[Kenny Lau]

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

done

[Kenny Lau]

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],
  rw [add_zero]
end

[Kenny Lau]

version 2

[Kenny Lau]

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]

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

[Kenny Lau]

@Kevin Buzzard did you sleep?

[Kevin Buzzard]

Meh https://xenaproject.wordpress.com/2018/03/30/proofs-by-induction/ is better

[Kevin Buzzard]

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

[Andrew Ashworth]

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]

“using the fucking ring tactic”

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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.

[Kenny Lau]

lol

[Kenny Lau]

i am shocked

[Kevin Buzzard]

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]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I guess that might be what I am saying.

[Andrew Ashworth]

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

[Kevin Buzzard]

Or some version of this.

[Kenny Lau]

i am still shocked :stuck_out_tongue:

[Andrew Ashworth]

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

[Kenny Lau]

fin has no eliminator though

[Kenny Lau]

hence the problem

[Kevin Buzzard]

yes, my approach with fin was not much fun.

[Kevin Buzzard]

But I need to sleep.

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I have also written three solutions to the problems.

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kenny Lau]

constant name : false

[Kenny Lau]

theorem RH : sorry := false.elim name

[Kevin Buzzard]

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]

it's only really meaningful in large, complicated definitions

[Andrew Ashworth]

of which square does not count

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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]

@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.