## Stream: maths

### Topic: finite sums

#### Kevin Buzzard (Feb 19 2019 at 11:35):

The 1st years at Imperial are doing infinite sums in their analysis class. To do infinite sums, one has to be able to have a robust API for finite sums. Here are three possibilities:

import data.list.basic data.fintype

open nat

variables (R : Type*) [add_comm_monoid R]

definition my_sum_to_n (summand : ℕ → R) : ℕ → R
| 0 := 0
| (succ n) := my_sum_to_n n + summand n

definition my_sum_to_n' (summand : ℕ → R) : ℕ → R :=
λ n, ((list.range n).map summand).sum

definition my_sum_to_n'' (summand : ℕ → R) : ℕ → R :=
λ n, (finset.range n).sum summand


You can see them in action here:

https://github.com/kckennylau/Lean/blob/master/proofs_by_induction.lean

What is the "idiomatic" way to do this? @Chris Hughes have you worked with this stuff a lot? Note that first two (but not the third) work with add_monoid but I am only interested in R being the real or complex numbers right now.

#### Chris Hughes (Feb 19 2019 at 11:43):

I use (range n).sum but I don't like it. I think a better interface needs to be made. (range n).sum definitely gives you the best range of lemmas though.

#### Kevin Buzzard (Feb 19 2019 at 11:43):

Ooh, I also want to sum from a to b, not just from 0 to n-1. Did we have all this conversation once before, ages ago?

finset or list?

#### Kevin Buzzard (Feb 19 2019 at 11:45):

Are statements such as sum_to_n f N = sum_to_n (\lam x, f(N-1-x)) N in the library?

#### Chris Hughes (Feb 19 2019 at 11:47):

I don't think so. Scott's made a start on this though

#### Kevin Buzzard (Feb 19 2019 at 11:47):

Does "a better interface" mean "make a completely new file somewhere in mathlib called something like finite_sum.lean and define a new function sum_range f a b or something, and prove basic things about it?

#### Kevin Buzzard (Feb 19 2019 at 11:48):

Oh I remember Mario's suggestion that sum_range f a b should sum f(x) from x=a to x=a+b-1

#### Kevin Buzzard (Feb 19 2019 at 11:48):

But is this not yet implemented?

#### Chris Hughes (Feb 19 2019 at 11:50):

No. It means use finset.sum, but have a bunch of lemmas specific to sums over intervals as well, and maybe some nice notation.

#### Kevin Buzzard (Feb 19 2019 at 11:51):

Do we have the function sending a,b to the finset {a,a+1,...,a+b-1}?

#### Chris Hughes (Feb 19 2019 at 11:52):

I think so, it's got Ico in its name I think.

#### Kevin Buzzard (Feb 19 2019 at 11:53):

Many thanks. It's got nothing but Ico in its name, apparently.

#### Kevin Buzzard (Feb 19 2019 at 11:54):

Interval-closed-open

#### Kevin Buzzard (Feb 19 2019 at 11:54):

and there's list.Ico, multiset.Ico and finset.Ico

#### Kevin Buzzard (Feb 19 2019 at 11:56):

Apparently we opted for Ico n m = {n, n+1, ... , m-1}

#### Kevin Buzzard (Feb 19 2019 at 12:00):

Lines 1654 onwards in finset.lean contain a bunch of stuff. But where are the recursors?

#### Kevin Buzzard (Feb 19 2019 at 12:00):

How do I prove that | sum_{i=a}^b f(i) | <= sum_{i=a}^b |f(i)| ??

#### Kevin Buzzard (Feb 19 2019 at 12:01):

(triangle inequality for finite sums)

#### Kevin Buzzard (Feb 19 2019 at 12:01):

Oh -- this is a general finset thing, not a sum from a to b thing.

#### Kevin Buzzard (Feb 19 2019 at 12:01):

So I need to find the right recursor for finsets...

#### Kevin Buzzard (Feb 19 2019 at 12:11):

Why is finset.induction tagged @[recursor 6]?

#### Chris Hughes (Feb 19 2019 at 12:23):

I think it must already be there

#### Kevin Buzzard (Feb 19 2019 at 12:24):

I think all of M1P1 must already be there :-)

#### Kevin Buzzard (Feb 19 2019 at 12:30):

If I was summing from 0 to n-1 I could do induction on n and use the fact that finset (n +1) = finset n union {n}. But for a general finset I'm going to have to choose a random element. Maybe that's just life.

#### Kevin Buzzard (Feb 19 2019 at 12:38):

Oh I see, I just use finset.induction I think.

#### Kevin Buzzard (Feb 19 2019 at 12:40):

I don't know what any of that means, but can you explain to me why I might care?

#### Kevin Buzzard (Feb 19 2019 at 12:40):

[I'm open to the idea that I might care]

#### Patrick Massot (Feb 19 2019 at 13:03):

We already had this discussion many times. All those problems have been solved in Coq, and I made a tiny start at porting the solution at https://github.com/PatrickMassot/bigop. But nobody is willing to help because people on this chat think they know better than people who have thought about this for 30 years and formalized the 4 color theorem and Feit-Thompson.

#### Kenny Lau (Feb 19 2019 at 13:07):

type mismatch at field 'bind'
finset.bind
has type
Π {α β : Type u} [_inst_1 : decidable_eq β], finset α → (α → finset β) → finset β
but is expected to have type
Π {α β : Type u}, finset α → (α → finset β) → finset β


#### Kenny Lau (Feb 19 2019 at 13:07):

that's the answer to my question

#### Kenny Lau (Feb 19 2019 at 13:08):

I should build a "real" finset

#### Kevin Buzzard (Feb 19 2019 at 14:48):

Aah yes that's right -- I somehow fail to unify these finite set questions with the big operators work, and I even have a copy the Coq paper lying around on my desk somewhere.

#### Kenny Lau (Feb 19 2019 at 15:07):

import data.list.basic

universes u v

def finset.setoid (α : Type u) : setoid (list α) :=
{ r := λ L₁ L₂, ∀ x, x ∈ L₁ ↔ x ∈ L₂,
iseqv := ⟨λ L x, iff.rfl, λ L₁ L₂ H12 x, (H12 x).symm, λ L₁ L₂ L₃ H12 H23 x, (H12 x).trans (H23 x)⟩ }

local attribute [instance] finset.setoid

def finset (α : Type u) : Type u :=
quotient (finset.setoid α)

namespace finset

variables {α : Type u}

instance : has_mem α (finset α) :=
⟨λ x s, ∀ L : list α, ⟦L⟧ = s → x ∈ L⟩

@[simp] lemma mem_mk {x : α} {L : list α} : @has_mem.mem α (finset α) _ x ⟦L⟧ ↔ x ∈ L :=
⟨λ H, H L rfl, λ H L₂ H2, (quotient.exact H2 x).2 H⟩

@[extensionality] protected lemma ext {s t : finset α} (H : ∀ x, x ∈ s ↔ x ∈ t) : s = t :=
quotient.induction_on₂ s t (λ L₁ L₂ H, quotient.sound $λ x, by rw [← mem_mk, H x, mem_mk]) H lemma ext_iff {s t : finset α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t := ⟨λ H x, H ▸ iff.rfl, finset.ext⟩ def empty : finset α := ⟦[]⟧ @[simp] lemma not_mem_empty (x : α) : x ∉ (empty : finset α) := λ h, mem_mk.1 h def singleton (x : α) : finset α := ⟦[x]⟧ def union (s t : finset α) : finset α := quotient.lift_on₂ s t (λ L₁ L₂, ⟦L₁ ++ L₂⟧)$ λ L₁ L₂ L₃ L₄ H13 H24,
quotient.sound $λ x, by rw [list.mem_append, list.mem_append, H13 x, H24 x] @[simp] lemma mem_union {s t : finset α} (x : α) : x ∈ union s t ↔ x ∈ s ∨ x ∈ t := quotient.induction_on₂ s t$ λ L₁ L₂, by change x ∈ ⟦_⟧ ↔ _; simp only [mem_mk, list.mem_append]

variables {β : Type v}

def prebind (f : α → finset β) (L : list α) : finset β :=
L.foldr (λ x, union (f x)) empty

@[simp] lemma prebind_cons (f : α → finset β) (hd : α) (tl : list α) :
prebind f (hd :: tl) = union (f hd) (prebind f tl) := rfl

@[simp] lemma mem_prebind {L : list α} {f : α → finset β} {y : β} :
y ∈ prebind f L ↔ ∃ x ∈ L, y ∈ f x :=
list.rec_on L (iff_of_false (not_mem_empty y) $λ ⟨x, H, _⟩, H)$ λ hd tl ih,
by rw [prebind_cons, mem_union, ih];
simp only [exists_prop, list.mem_cons_iff, or_and_distrib_right, exists_or_distrib, exists_eq_left]

{ pure := λ α x, quotient.mk [x],
bind := λ α β s f, quotient.lift_on s (prebind f) $λ L₁ L₂ h, by ext x; simp only [mem_prebind, exists_prop, h _] } end finset  #### Kenny Lau (Feb 19 2019 at 15:07): done, the real finset is a monad #### Johan Commelin (Feb 19 2019 at 15:25): @Patrick Massot I agree that it is frustrating that we are having this discussion multiple times, and that we are reinventing the wheel. I haven't thought about this problem (finite sums) myself. I wouldn't mind if this could be turned into a student project; but I fear that there is not enough mathematical meat in it. At the moment I don't have much contact with the CS department here in Freiburg. It's something on my todo list. Maybe they would think that an bachelor thesis titled "Algorithms and data types for manipulating finite sums and proving identities between them" is interesting... #### Johan Commelin (Feb 19 2019 at 15:25): I would like to get better at recruiting people for library development. #### Kenny Lau (Feb 19 2019 at 21:14): import data.list.basic universes u v def finset.setoid (α : Type u) : setoid (list α) := { r := λ L₁ L₂, ∀ x, x ∈ L₁ ↔ x ∈ L₂, iseqv := ⟨λ L x, iff.rfl, λ L₁ L₂ H12 x, (H12 x).symm, λ L₁ L₂ L₃ H12 H23 x, (H12 x).trans (H23 x)⟩ } local attribute [instance] finset.setoid def finset (α : Type u) : Type u := quotient (finset.setoid α) namespace finset run_cmd mk_simp_attr "finset" variables {α : Type u} instance : has_mem α (finset α) := ⟨λ x s, ∀ L : list α, ⟦L⟧ = s → x ∈ L⟩ @[finset] lemma mem_mk {x : α} {L : list α} : @has_mem.mem α (finset α) _ x ⟦L⟧ ↔ x ∈ L := ⟨λ H, H L rfl, λ H L₂ H2, (quotient.exact H2 x).2 H⟩ @[extensionality] protected lemma ext {s t : finset α} (H : ∀ x, x ∈ s ↔ x ∈ t) : s = t := quotient.induction_on₂ s t (λ L₁ L₂ H, quotient.sound$ λ x, by rw [← mem_mk, H x, mem_mk]) H

lemma ext_iff {s t : finset α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
⟨λ H x, H ▸ iff.rfl, finset.ext⟩

def empty : finset α := ⟦[]⟧

@[finset] lemma not_mem_empty (x : α) : x ∉ (empty : finset α) :=
λ h, mem_mk.1 h

def singleton (x : α) : finset α := ⟦[x]⟧

def union (s t : finset α) : finset α :=
quotient.lift_on₂ s t (λ L₁ L₂, ⟦L₁ ++ L₂⟧) $λ L₁ L₂ L₃ L₄ H13 H24, quotient.sound$ λ x, by rw [list.mem_append, list.mem_append, H13 x, H24 x]

@[finset] lemma mem_union {s t : finset α} (x : α) : x ∈ union s t ↔ x ∈ s ∨ x ∈ t :=
quotient.induction_on₂ s t $λ L₁ L₂, by change x ∈ ⟦_⟧ ↔ _; simp only [list.mem_append] with finset section prebind variables {β : Type v} def prebind (f : α → finset β) (L : list α) : finset β := L.foldr (λ x, union (f x)) empty @[finset] lemma prebind_cons (f : α → finset β) (hd : α) (tl : list α) : prebind f (hd :: tl) = union (f hd) (prebind f tl) := rfl @[finset] lemma mem_prebind {L : list α} {f : α → finset β} {y : β} : y ∈ prebind f L ↔ ∃ x ∈ L, y ∈ f x := list.rec_on L (iff_of_false (not_mem_empty y)$ λ ⟨x, H, _⟩, H) $λ hd tl ih, by rw [prebind_cons, mem_union, ih]; simp only [exists_prop, list.mem_cons_iff, or_and_distrib_right, exists_or_distrib, exists_eq_left] end prebind variables {β : Type u} instance : monad finset.{u} := { pure := λ α x, quotient.mk [x], bind := λ α β s f, quotient.lift_on s (prebind f)$ λ L₁ L₂ h,
by ext x; simp only [exists_prop, h _] with finset }

@[finset] lemma mem_pure {x y : α} : x ∈ (pure y : finset α) ↔ x = y :=
mem_mk.trans list.mem_singleton

@[finset] lemma mem_bind {s : finset α} {f : α → finset β} {y : β} :
y ∈ s >>= f ↔ ∃ x ∈ s, y ∈ f x :=
quotient.induction_on s $λ L, show y ∈ prebind f L ↔ _, by simp only [exists_prop] with finset @[finset] lemma mem_map {f : α → β} {s : finset α} {y : β} : y ∈ f <$> s ↔ ∃ x ∈ s, y = f x :=
show y ∈ s >>= pure ∘ f ↔ _,
by simp only [function.comp_apply] with finset

@[finset] lemma mem_seq {f : finset (α → β)} {s : finset α} {y : β} :
y ∈ f <*> s ↔ ∃ φ ∈ f, ∃ x ∈ s, y = (φ : α → β) x :=
show y ∈ f >>= (<$> s) ↔ _, by simp only with finset instance : is_lawful_monad finset.{u} := { pure_bind := λ α β x f, finset.ext$ λ y, by simp only [exists_prop, exists_eq_left] with finset,
bind_assoc := λ α β γ s f g, finset.ext $λ y, by simp only [exists_prop, exists_and_distrib_left.symm, exists_and_distrib_right.symm, and_assoc] with finset; rw exists_swap, id_map := λ α s, finset.ext$ λ x, by simp only [id, exists_prop, exists_eq_right'] with finset }

end finset


#### Kevin Buzzard (Feb 19 2019 at 21:17):

Yeah but who is going to rewrite the 1700-line file finset.lean? What advantage does your approach have over the one in mathlib? Do you understand @Mario Carneiro and @Jeremy Avigad and @Simon Hudon 's approach via qpf's? Is it the same as yours or something else again?

#### Kenny Lau (Feb 19 2019 at 21:18):

well I've been told that the current finset in mathlib is faster in terms of computation

#### Kenny Lau (Feb 19 2019 at 21:18):

so it'll probably stay

#### Scott Morrison (Feb 19 2019 at 21:34):

@Patrick Massot, I disagree with your characterisation

because people on this chat think they know better than people who have thought about this for 30 year

#### Scott Morrison (Feb 19 2019 at 21:35):

I wanted a quick an dirty solution for reindexing sums by shifting right and left, and had no where near the time available to properly do a big operators library, so I did just that. There are now usable lemmas specifically for using finset.sum with Ico, and of course this is not meant to be a replacement for a good general solution later.

#### Scott Morrison (Feb 19 2019 at 21:39):

Further, and I suspect Mario will agree here, I don't think it's obvious that Coq's bigop library should be ported verbatim. We started a discussion about this earlier, and one example that came up was not understanding why they wanted to carry around both a domain for the sum, and a predicate selecting out some subset of that domain. To my eye that seems unnecessarily painful, and we should just change the domain to a subset when we want to do so. I couldn't find any explanation of this design decision in their paper, and as far as I can remember no one either justified it here, or wanted to talk about comparing the alternatives. As it didn't seem like there was much enthusiasm for discussion, I moved on to other things.

#### Mario Carneiro (Feb 19 2019 at 23:03):

@Kevin Buzzard The QPF stuff isn't presenting a new way to do finsets, it's just providing a way to use finset inside other inductive types, which is something we currently can't do

#### Mario Carneiro (Feb 19 2019 at 23:06):

The difference between Kenny's finsets and mathlib finsets is that Kenny's is a quotient over the multiplicity of an element, while mathlib's is a restriction on multisets so that they have multiplicity 0 or 1 in each element. Computationally it's worse than mathlib's finsets, but mathlib's finsets are already completely impractical and not how you should store finite sets of things anyway for computational purposes. The ordset type was intended to be more computational, and provides O(log n) operations for most things rather than linear time for everything

#### Kenny Lau (Feb 19 2019 at 23:07):

and my finsets don't need decidable_eq to be a monad :P

#### Mario Carneiro (Feb 19 2019 at 23:07):

One thing that Kenny's finsets doesn't support that mathlib's finsets do is card

#### Mario Carneiro (Feb 19 2019 at 23:08):

but Kenny's finsets support insert and union without decidable_eq, which is nice

déjà vu

#### Mario Carneiro (Feb 19 2019 at 23:08):

inter can't be done without decidable eq though

#### Kenny Lau (Feb 19 2019 at 23:10):

what's the best™ way to do finsets?

#### Kenny Lau (Feb 19 2019 at 23:11):

I recall ZF having 5 inequivalent definitions of finite?

#### Mario Carneiro (Feb 19 2019 at 23:12):

metamath has 8 (http://us2.metamath.org/mpeuni/mmtheorems83.html#mm8285s)

#### Kenny Lau (Feb 19 2019 at 23:15):

also why isn't multiset a monad?

#### Kenny Lau (Feb 19 2019 at 23:16):

import data.multiset

{ pure := λ α x, x :: 0,
map := @multiset.map,
bind := @multiset.bind }


good question

#### Mario Carneiro (Feb 19 2019 at 23:16):

is it lawful? I think it is

#### Kenny Lau (Feb 19 2019 at 23:17):

'course it's lawful, it's even commutative!

#### Kenny Lau (Feb 19 2019 at 23:17):

it's the free commutative monoid over a type

#### Patrick Massot (Feb 20 2019 at 20:36):

Further, and I suspect Mario will agree here, I don't think it's obvious that Coq's bigop library should be ported verbatim.

Of course we cannot port it verbatim. For instance we lack proper support for custom induction principle. We also lack SSReflect's powerful apply tactic. So we need to either first code more powerful tactics (which probably needs Lean 4) or write longer proofs (as I started to do).

We started a discussion about this earlier, and one example that came up was not understanding why they wanted to carry around both a domain for the sum, and a predicate selecting out some subset of that domain. To my eye that seems unnecessarily painful, and we should just change the domain to a subset when we want to do so. I couldn't find any explanation of this design decision in their paper, and as far as I can remember no one either justified it here, or wanted to talk about comparing the alternatives. As it didn't seem like there was much enthusiasm for discussion, I moved on to other things.

I'm not sure I understand what you mean here. Of course we want to be able to sum on various stuff, including using a predicate. Are you denying this happens in maths? There are several examples in the Coq bigop paper. Of course you can put the burden on the user, but this is not my understanding of what is library building. Let's take the simplest example. Say we have a sum indexed by integers, and we want to separate this into two sums: the sum over even integers in the summation range and the sum over odd integers, because you'll then do different manipulation depending on parity of the index. How would you like the interface to look like? Should is look like maths, where you get $\sum_{1 \le i \le n } u_i = \sum_{1 \le i \le n ; i \text{ even}} u_i + \sum_{1 \le i \le n ;i \text{ odd} } u_i$ after writing something like rw [bigop.split_using_predicate is_even, bigop.predicate_iff odd_iff_not_even or do you want to first prove lemmas about lists until it looks like a concatenation of lists etc? I really think the work should go into the library, and then the user enjoys. Note that the user doesn't need to see anything complicated until needed: you can define notation that do not mention the predicate when you don't need it (this is what bigop is doing, and what I've done right from the beginning).

#### Mario Carneiro (Feb 21 2019 at 04:32):

If you are doing something with complicated sums like these, I think the best option is to use finsets. They are much more compositional

#### Patrick Massot (Feb 21 2019 at 07:54):

finsets are unordered, hence they cannot be used for a general library.

#### Mario Carneiro (Feb 21 2019 at 07:55):

huh? That equation you gave doesn't even hold unless you can reorder the elements

#### Patrick Massot (Feb 21 2019 at 07:55):

What is the part of "general" that you don't understand?

#### Mario Carneiro (Feb 21 2019 at 07:56):

The part where finsets are already pretty general

#### Patrick Massot (Feb 21 2019 at 07:56):

bigop is a a general library, it handles all use case in a unified way

#### Patrick Massot (Feb 21 2019 at 07:57):

Assuming commutativity is extremely restrictive, it's not "pretty general"

#### Mario Carneiro (Feb 21 2019 at 07:57):

I'm saying that if it's not commutative, you have other options but that partition theorem isn't true

#### Mario Carneiro (Feb 21 2019 at 07:58):

Can we assume associativity?

#### Patrick Massot (Feb 21 2019 at 07:58):

Of course there are lemmas with assumptions, is that what you are trying to teach here?

#### Mario Carneiro (Feb 21 2019 at 07:58):

At some point you are just folding over the free magma

#### Patrick Massot (Feb 21 2019 at 07:58):

We don't have to assume associativity for all lemmas, although many of them will

#### Patrick Massot (Feb 21 2019 at 07:59):

I honestly don't understand how you can promote both semi-rings and big operations indexed by finite sets

#### Mario Carneiro (Feb 21 2019 at 08:00):

We have list.sum already

#### Mario Carneiro (Feb 21 2019 at 08:00):

I'm not seeing what we are missing

#### Mario Carneiro (Feb 21 2019 at 08:01):

We have an extensive collection of lemmas about ordered lists - that's list

#### Patrick Massot (Feb 21 2019 at 08:01):

list.sum is tied to addition, right?

#### Mario Carneiro (Feb 21 2019 at 08:01):

or list.prod, or list.foldr

#### Patrick Massot (Feb 21 2019 at 08:03):

and list.prod is tied to multiplication, so you are still missing a general purpose library

#### Patrick Massot (Feb 21 2019 at 08:03):

Of course list.foldr will be used in the implementation, but it doesn't give you the lemmas

Sure it does

#### Mario Carneiro (Feb 21 2019 at 08:03):

you can prove lemmas about list.foldr

#### Mario Carneiro (Feb 21 2019 at 08:04):

under appropriate assumptions about the function

#### Patrick Massot (Feb 21 2019 at 08:04):

And then you are finally writing a bigop library!

#### Patrick Massot (Feb 21 2019 at 08:04):

assuming you also setup good notations

#### Mario Carneiro (Feb 21 2019 at 08:04):

It's hard to make a notation for a function with four explicit parameters

#### Patrick Massot (Feb 21 2019 at 08:05):

And, in order to do that you can save time by having a look at what other did.

#### Patrick Massot (Feb 21 2019 at 08:05):

That's why you need several notations

#### Mario Carneiro (Feb 21 2019 at 08:06):

If I am specializing to +, that's already a function

#### Mario Carneiro (Feb 21 2019 at 08:06):

Using the same function for all of these doesn't make anything easier

#### Patrick Massot (Feb 21 2019 at 08:06):

The trick is that those notations are used by users, but all lemmas are proved once, in the most general setting

#### Patrick Massot (Feb 21 2019 at 08:07):

Of course it does make everything easier, that's what math is about: prove general results and gets many special cases for free

#### Mario Carneiro (Feb 21 2019 at 08:07):

Yeah but we've already done that

Where?

#### Mario Carneiro (Feb 21 2019 at 08:07):

Finset has loads of theorems, multiset has loads of theorems, list has loads of theorems, all in maximum generality for the statement

#### Patrick Massot (Feb 21 2019 at 08:09):

Seriously Mario, did you open that https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/bigop.v or are you waiting for the next time one of your papers will be rejected because you pay no attention to what the rest of the world is doing?

#### Johan Commelin (Feb 21 2019 at 08:11):

That is >200 lines of introducing notation. Wow!

#### Patrick Massot (Feb 21 2019 at 08:12):

Yes, those guys are pretty serious about building user interfaces

#### Johan Commelin (Feb 21 2019 at 08:12):

Patrick, do you know if that file was written by hand?

certainly it was

#### Johan Commelin (Feb 21 2019 at 08:12):

Parts of it look so regular that you would think one might want to generate it

#### Mario Carneiro (Feb 21 2019 at 08:13):

the answer to that question is no 90% of the time

#### Patrick Massot (Feb 21 2019 at 08:14):

Remember this is part of the project that proved Feit-Thompson. It's the same game that we play, except that it scales. So, yes, they are pretty rigorous and regular

#### Patrick Massot (Feb 21 2019 at 08:15):

I need to go, but I hope you'll think seriously about all that

#### Chris Hughes (Feb 21 2019 at 09:36):

I'm with Patrick here. list.prod doesn't have anywhere near the number of lemmas of finset.prod.

#### Mario Carneiro (Feb 21 2019 at 09:49):

Are there a lot of analogous theorems? I guess the noncommutative story is much simpler since most of the lemmas don't hold

#### Mario Carneiro (Feb 21 2019 at 10:03):

• finset.prod_empty -> list.prod_nil
• finset.prod_insert -> list.prod_cons
• finset.prod_singleton -> TODO, but provable by simp
• finset.prod_const_one -> TODO: list.prod_repeat_one : list.prod (list.repeat 1 n) = 1
• finset.prod_image -> unnecessary
• finset.prod_congr -> unnecessary
• finset.prod_union_inter -> inapplicable
• finset.prod_union -> list.prod_append
• finset.prod_sdiff -> inapplicable
• finset.prod_bind -> list.prod_join, TODO?
• finset.prod_product -> TODO
• finset.prod_sigma -> TODO
• finset.prod_image' -> ?
• finset.prod_mul_distrib -> inapplicable
• finset.prod_comm -> inapplicable
• finset.prod_hom -> TODO
• finset.prod_hom_rel -> TODO
• finset.prod_subset -> not sure how to state
• finset.prod_eq_single -> not sure how to state
• finset.prod_attach -> unnecessary
• finset.prod_bij -> inapplicable

The inapplicable ones only apply in a commutative setting, where I assume the finset notion works better. For some of the others, it may be better to have a version of fold that takes a binary operation and a function, similar to Patrick's apply_bigop but without the predicate

#### Scott Morrison (Feb 22 2019 at 09:41):

Of course we want to be able to sum on various stuff, including using a predicate. Are you denying this happens in maths?

Of course not...

I just don't understand why a big operations interface needs to know separately about some domain, and some predicate on it, when you could just use .filter (on whatever sort of object is representing the domain).

#### Mario Carneiro (Feb 22 2019 at 09:43):

I would say something similar about the similarities between sum_(i \in l) a_i and sum_(i=m..n) a_i. One is literally a special case of the other, so compositionality suggests to factor the definition

#### Patrick Massot (Feb 22 2019 at 14:07):

Again, Scott and Mario: of course the implementation uses filter and factor the definition of sum_(i \in l) a_i and sum_(i=m..n) a_i. But the user interface needs to do its job and hide all that.

#### Kevin Buzzard (Feb 24 2019 at 00:47):

I think that what might be happening here is similar to this whole "R is Noetherian and S is isomorphic to R so S is Noetherian" thing.

Patrick -- we have to remember that Mario is not actually a mathematician. We might see sums broken up into sums over even and odd indices quite a lot (or maybe much more complex things, like breaking sums over modules into sums over isomorphism classes or whatever), but maybe he just never really does. He knows that everything can be done with filter and fold and doesn't really see the problem. I run into issues when doing things like undergraduate analysis and think "isn't it annoying that this isn't there and I have to use filter and fold", but nobody actually writes the code which should be there because the mathematicians haven't got around to it and the computer scientists don't really seem to know what we want. It's all well and good saying "we want what's in Coq" but somehow in practice what we actually want is the tools necessary to do what we're trying to do right now this instant. I have become convinced that Mario isn't just being obstructive/lazy when he doesn't write me my tactic which will rewrite sensible mathematical statements along isomorphisms of rings, he just can't really see why it's necessary because I've not yet come up with the killer example. I think it's the same here. We occasionally say "we want to do this" and it is pointed out to us that this is actually possible and would in fact be easy if we had some CS training, but we want something else. Maybe we haven't formalised exactly what we want.

#### Mario Carneiro (Feb 24 2019 at 03:39):

In metamath I had to do several sums over unusual sets; for example a sum over group elements breaks into a sum over conjugacy classes or cosets, or into sets of size two. Then there are mobius sums, over the divisors of a number, that commute with regular sums in interesting ways. I handled all of these by essentially the same method, which like finset sum. (It was a sum over a general abelian group, so in some ways it's more general than the lean version because it's not as much of a pain to switch between multiplicative and additive.)

To prove stuff about partitioning a group sum, the proof obligation says that you have an indexed family of finsets which is disjoint (this is a definition on families of sets/finsets that says \all (i j : I) (z : A), z \in f i -> z \in f j -> i = j), then the sum breaks into a two dimensional sum indexed over I and then summing the finsets in f.

#### Chris Hughes (Feb 24 2019 at 12:36):

There's a danger in hiding the fact that it's based on finset.sum in the sense that you lose the interface and theorems you had for finset, or at least make it less obvious that they apply. Take $\sum_{j=0}^{n} \sum_{k=0}^j a_k b_{j-k} = \sum_{k=0}^{n} a_k \sum_{j=k}^n b_{j-k}$. This is hard to prove without using without using lemmas about finsets (and is stated without proof in any textbook). There are probably a few lemmas missing about intervals, but you still very much need the finset ones.

#### Kevin Buzzard (Feb 24 2019 at 15:18):

I always justify this in lectures by saying that it's the sum over 0 <= k <= j <= n

#### Chris Hughes (Feb 24 2019 at 15:21):

Exactly. That's the lean proof. But you have to use lemmas about sums over finsets for that. You don't want the finset to be hidden.

Last updated: May 18 2021 at 08:14 UTC