working with finite sequences

Stream: general

[Kevin Buzzard]

Kenny and I will need to do some work with finite sequences to prove that affine schemes are schemes. Here is an example of the sorts of issues we are running into.

We have a definition generate (S : set alpha) -- for generating submodules of rings, but the same sort of question would arise for generating subgroups of groups or subspaces of vector spaces. Kenny has defined generate S to be { x | ∀ (T : set α) [is_submodule T], S ⊆ T → x ∈ T } which is fine mathematically but now we need the "concrete" definition of the module generated by S, that is, the x such that there exists some finite sequence s1,s2,..,sn of elements of S and some finite sequence r1,r2,...,rn of the underlying ring alpha such that x=r1*s1+r2*s2+...+rn*sn. I can think of lots of ways to implement this but I have no feeling as to which one is "right" in this situation. I definitely want to allow repeats amongst the r's, and they are ordered. Should we go with asserting the existence of two lists of size n, or a map from fin n to S, or a map from range n to S, or some other approach? I am pretty sure that any of these suggestions would work but I don't know which one is most idiomatic (is that the right word?) for Lean. We are going to want to do the sorts of things that mathematicians would do with these lists -- form the sum of ri*si over i, choose an element from the list with some property, concatenate two lists, prove that the sum up to n+1 is the sum up to n plus the last term, blah blah blah. Obviously we'll also want to prove that the two definitions of generate are equivalent.

If the answer is "tell us more specifically exactly what you want to do with these lists" then I could try to do that. Could it be the case that it doesn't really matter what we choose, and all methods should work fine?

[Johannes Hölzl]

so generate is span in algebra.linear_algebra?

[Kevin Buzzard]

Probably. We're using it for generating ideals of a ring here.

[Johannes Hölzl]

If you use span you already got a representation as finsupp, i.e. a map from the base ring into the module with finite support.

[Kevin Buzzard]

One of Leo's comments on some recent PR is "I think this is an anti-idiom." I am just trying to avoid being anti-idiomatic :-)

[Johannes Hölzl]

The nice thing of finsupp is that you can ignore the order, I usually do all the operations on it using the finsupp.sum operator.
I guess you do not really need a order on the elements?

[Kevin Buzzard]

No but we need a way to biject the r_i and the s_i

[Kevin Buzzard]

so we could have a map from an unordered finite type to R and a map from the same type to S, for example

[Kevin Buzzard]

On the other hand we might well sometimes want to prove things by induction on n, the size of the sequence

[Johannes Hölzl]

I think you don't need the index type at all! You can do induction directly on finsupp itself, (or on its support).
By avoiding this arbitrary index type you avoid a lot of data to carry around. It is common in mathematics to write down x_1 ... x_n and then go on to prove something by induction on n. But in many cases this is unnecessary, and much easier (and maybe more idiomatic) to do it in an unordered fashion. In you case you directly take a function R ->_0 S (the _0 indicates that it is a finsupp function), I would assume this encodes enough information for your proofs.

[Kevin Buzzard]

In the finsupp approach I seem to need a random index type X, so that if I have a ring R and a subset S then I can write down maps X->R and X->S with finite support. So I might not need n and fin n but surely I still need an index type, if this is what X is.

[Kevin Buzzard]

If the suggestion is that the span is the elements a in R such that there exists some type X and finsupp maps f : X -> R and g : X -> S such that a = sum f x * g x, then to add two such maps together I would need that if f1 : X -> R and f2 : Y -> R are finsupp maps then f1+f2 : X disjoint_union Y -> R is a finsupp. Presumably lemmas such as this are already there?

[Johannes Hölzl]

There is no need for an arbitrary index type. The idea is that you represent a span as R ->_0 S, there are no further index types. An element x \in span Sis represented as: \exists f : R ->_0 S, x = \sum_{(r, s) \in f} r * s

[Johannes Hölzl]

\sum_{(r, s) \in f} is actually written f.sum (\lam r s, ...) in lean.

[Johannes Hölzl]

So there is a special summation operator over the elements in f.

[Kevin Buzzard]

Aah I see! But this looks problematic because I don't see how to add the elements corresponding to two such maps. I would need maps S ->_0 R instead. Can you envisage this causing any problems?

[Kevin Buzzard]

I would also need lemmas of the form "if s is in S and if I define f : S ->_0 R by f(t)=ite (t=s) 1 0 then f.sum ... = s". Are these already there?

[Kevin Buzzard]

and things of the form "if f : S ->_0 R has image size n+1 then I can write it as g+h with g of image size n and h of image size 1".

[Kevin Buzzard]

What I am hoping for is being able to avoid writing all the infrastructure myself ;-)

[Johannes Hölzl]

I'm sorry, of course it would be S ->_0 R!

[Johannes Hölzl]

f(t) = ite (t=s) 1 0 is available for finsupp, it's called single s r, which maps s -> r and nothing else.

[Johannes Hölzl]

We can easily proof a special case statement saying essentially: f = 0 \/ \exists f' r s, r /= 0 /\ s \notin f' /\ f = f' + single s r

[Kevin Buzzard]

Thanks as ever for your comment Johannes. Although I don't really understand why finsupps are better than any of the approaches I outlined, I certainly trust your judgement and will use this approach.

[Johannes Hölzl]

What brings finsupp: it doesn't duplicate elements, it avoids any order on your elements, and there is only one data/variables etc to handle .

• Duplication might be very annoying in induction proofs, where you walk over your elements and then be sure that they do not appear at a later point. This might require removing them from the later list, and hence requiring a strong induction principle.
• The order is annoying when you create a linear combination. Depending on how you create them it might be a problem.

Does this give a better idea why finsupp is better than lists of pairs, multisets of pairs or two functions indexed by a finite type?

[Kevin Buzzard]

Thank you for these explanations. I can see that finsupp is fundamentally different to all my proposals, because for all the ways I suggested (1) I need an extra type and (2) I have an implicit order, neither of which are necessary. I guess what I don't really understand is how important these differences are in practice. I guess the point is that if I don't need some structure when implementing an idea then I should try and implement the idea without introducing the structure.

[Patrick Massot]

This S ->_0 R is a nice trick but it won't work for non commutative laws

[Patrick Massot]

So it's bad from the point of view of developing general idioms

[Patrick Massot]

Also, what about www-sop.inria.fr/marelle/bigops/main.pdf ? Did mathlib learn from this?

[Kenny Lau]

@Johannes Hölzl how does induction work on finsupp?

[Mario Carneiro]

The support of a finsupp is a finite set, so you can use finite.induction

[Kenny Lau]

@Mario Carneiro so I case it to get finite before I induction it?

[Kenny Lau]

but then how do I use the functions from finsupp?

[Mario Carneiro]

Maybe a better question is: what are you trying to prove? Are you sure you need to use induction? Most facts about finsupp that are proven by induction should already be lemmas

[Mario Carneiro]

and don't case the function, just use finsupp.support

[Kenny Lau]

I guess I don't need induction then

[Kenny Lau]

/-- `image f s` is the forward image of `s` under `f`. -/
def image (f : α → β) (s : finset α) : finset β := (s.1.map f).to_finset

is there a way for the function to know that the input is in s?

[Mario Carneiro]

you could precompose with finset.attach

[Johannes Hölzl]

we can also add a special induction rule for finsupp, which would be based on the induction on the support itself. However, it would give one a better view, i.e. look somehow like finsupp.induction_on {P : (S ->_0 R) -> Prop} (f : S ->_0 R) (h0 : P 0) (h1 : \all f s r, s \notin f -> P f -> P (f + single s r)) : P f . Then you got a induction rule which carries on the data as expected.

[Johannes Hölzl]

I think the idiom we want to have is: represent your data in the somehow optimal way. So if one works with commutative spaces, like modules, finsupp carries the least necessary information. If one is working in a non commutative setting they might want to use lists, or freely generated groups, or ordered maps etc.

[Johannes Hölzl]

@Patrick Massot indeed Coq has a nice and flexible big operator library. But it is very much based on canonical structures which is hard to copy in Lean itself. Also as Leans algebraic hierarchy will change in the future we will see how big operators might look like in the future.

[Patrick Massot]

I'm confused. I was under the impression that canonical structure was Coq's name for type class inference.

[Johannes Hölzl]

AFAIK Coq has two type class mechanisms, one is called type classes, and is similar to Lean's type class mechanism. And canonical structures, which are very different. I still don't understand canonical structures, but I think it works in a way that the unifier somehow creates a structure based on unification constraints, so from ?x.1 =?= A and ?x.2 =?= B it will create ?x =?= (A, B).

[Johannes Hölzl]

@Kevin Buzzard and @Kenny Lau I worked a little bit on finsupp: it got computable, i.e. the projection of the support of a finsupp are now rfl-lemmas. But more important: I added a induction lemma finsupp.induction_on.

[Kenny Lau]

thanks

[Kevin Buzzard]

Oh many thanks Johannes. I think I might understand Lean well enough to formulate precisely the statement I want from this finsupp approach. I really want to make working with finite objects easier for mathematicians. I was there when Chris told Kenny that he had formalised Lagrange's Theorem and Kenny was visibly impressed. Mathematicians use finite objects in certain ways which are natural to them but which seem to be hard to do (at least for me) in Lean.

[Kevin Buzzard]

Lagrange's theorem in mathematics (in the usual language of ZFC) says that if S is a finite set of size n, and if there's an equivalence relation on S such that all the equivalence classes have the same size d, then n is the product of d and the number m of equivalence classes.

[Kevin Buzzard]

Well, it is a related statement :-)

[Kevin Buzzard]

And this is a statement which is so obvious to a mathematician that it really doesn't need a proof, it should just be by some tactic because it is as obvious as the statement that if x y and z are real numbers then x * (y + z) = x * y + x * z, i.e. something which one can assume without any comment.

[Kevin Buzzard]

But in Lean I look at that statement and my first thought is that I can see about 10 ways of formalizing it and I have no idea which ones will be easy to use.

[Kevin Buzzard]

So in my mind this is an area which it would be really nice to work on.

[Kevin Buzzard]

In fact let me also state the original example from commutative ring theory which got me thinking about this whole issue. Here is an example of a statement and a proof from the Stacks Project (written in ZFC). The statement is this. Say R is a ring, and we have some n>=2 and some elements f1,f2...,fn of R and positive integers e1,e2,...,en such that (a) fi^ei*r=0 for all i and (b) there exists some r1,r2,...,rn in R such that the sum of ri*fi equals 1. Then r=0.

[Kevin Buzzard]

The proof is just by calc, and it goes:

[Kevin Buzzard]

1=sum ri * fi

[Kevin Buzzard]

=(sum ri * fi)^N where N is something big that we might not even bother to state if we were sloppy, but maybe we would say "Oh N=the sum of the ei should probably work" if we were being careful

[Kevin Buzzard]

and then say "so done by the multinomial theorem".

[Kevin Buzzard]

I know I can do that in Lean but I just look at it and it looks difficult to me.

[Kevin Buzzard]

it's not something I want to be stuck on or bothered with. I just defined sheaves on a topological space in Lean without batting an eyelid and that's a gazillion times more complicated to a mathematician

[Kevin Buzzard]

I don't want finite sets and sequences to be hard.

[Kevin Buzzard]

Maybe we would let the students "fill in the details as an exercise"

[Kevin Buzzard]

but if I saw anyone write just something like "(sum ri fi)^N=sum_{t_1,t_2,...,t_n nats with sum N}(multinomial (N) (t1,t2,...,tn))r1^t1 r2^t2..rn^tn f1^t1 f2^t2 .. fn^tn and each term annihiliates r because the sum of the ti is the sum of the ei so clearly ti>=ei for some i"

[Kevin Buzzard]

A mathematician wouldn't be expected to write much more than that. But why do I look at that and think that it needs some planning in Lean? I want to just be able to write that easily, i.e. formulate it in an idiomatic way in DTT and prove it with a tactic.

[Kevin Buzzard]

I know Chris has proved some version of the binomial theorem in Lean, it's on his github.

[Kevin Buzzard]

But I don't know if it is the "right" version, or even whether it makes sense to ask that there is a "right" version of the binomial or multinomial theorems.

[Kevin Buzzard]

Somehow for a mathematician there is just one multinomial theorem, which might not even have been stated in the correct generality in your undergraduate class (the theorem states what the expansion of (x1+x2+...+xn)^N is, but what are those xi? The stats lecturer needs multinomial theorem to be covered ASAP because they need it for their course, so we do it in the first term, and I want to make the assertion that the x_i are a ring, but I can't because they don't know what a ring is. So I just say that x_i are real numbers because it will keep the stats person happy.

[Kevin Buzzard]

and then if anyone ever asks later on I just say "oh yeah of course it works for any ring, probably my proof generalizes"

[Kevin Buzzard]

We teach maths in the wrong order :-)

[Kevin Buzzard]

They do all this stuff in applied maths in year 1 where they're brutally re-arranging all sorts of sums and products on the basis that "one day you'll see that this was all rigorous after all, or at least most of it was, there was that bit in the Fourier Transform section that is actually a bit more complicated than you'd like"

[Kevin Buzzard]

I'll quote some stuff from earlier in the finite sequences thread and add some more stuff.

[Kevin Buzzard]

General Mathematical Principle 1): "If you partition a finite set up into m subsets of size d then your set has size m*d". The mathematician says "this is one of several equivalent definitions of multiplication, so done". In Lean we might formulate it like this: if S is a finite type of size n (i.e. there are exactly n distinct terms of type S), and if there's an equivalence relation on S such that all the equivalence classes have the same size d, then n is the product of d and the number m of equivalence classes. Already in Lean it seems to me that one has to make a decision about how to formalise this because there are several possibilities. Should S be a finset, a fintype, or a set S for which finite S is true? What if we are given S as a subtype and we don't even know it's finite, and want to prove this from the fact that we can partition it up into m subsets of size d? Would I be right in thinking that there is no one "idiomatic" way to prove a Lean version of General Mathematical Principle 1? Or might there be one general canonical way of expressing this principle in Lean such that all instances of the principle which mathematicians want to use can be deduced from this canonical formulation?

[Kevin Buzzard]

General Mathematical Principle 2) Obvious Finite Sum facts. Sum from i=a to i=b of f(i) plus sum from i=b+1 to i=c of f(i) equals sum from i=a to i=c of f(i). Sum from 0 to n of f(i) equals sum from 0 to n of f(n-i). Sum from a to n+1 of f(i) equals sum from a to n of f(i), plus f(n+1)`.

[Kevin Buzzard]

Again all of these things would be things a mathematician would write without even commenting on why these things were true. Again in Lean I see lots of ways of implementing the statements, based on whether we decide to sum over a list, or a different kind of finite object: there is finset.sum but summing from 0 or 1 to n is a very common use case in mathematics. Should I just implement these theorems myself using list.range and fold?

[Kevin Buzzard]

/-- sum_from_one_to n f sums f(i) for 1<=i<=n -/
definition sum_from_one_to {α : Type*} [has_add α] [has_zero α] (n : ℕ) (f : ℕ → α) : α := sorry

theorem sum_from_one_to.rec {α : Type*} [has_add α] [has_zero α]
  (n : ℕ) (f : ℕ → α) : sum_from_one_to (n+1) f = f (n+1) + sum_from_one_to n f  := sorry

/-- sum_from_zeo_to n f sums f(i) for 0<=i<=n -/
definition sum_from_zero_to {α : Type*} [has_add α] [has_zero α] (n : ℕ) (f : ℕ → α) : α := sorry

theorem sum_from_zero_to.rec {α : Type*} [has_add α] [has_zero α]
  (n : ℕ) (f : ℕ → α) : sum_from_zero_to (n+1) f = f (n+1) + sum_from_zero_to n f  := sorry

/-- sum_from_to a n f sums f(i) for a<=i<=n -/
definition sum_from_to {α : Type*} [has_add α] [has_zero α]
  (a : ℕ) (n : ℕ) (H : a ≤ n + 1) (f : ℕ → α) : α := sorry

theorem sum_from_to.rec {α : Type*} [has_add α] [has_zero α]
  (a : ℕ) (n : ℕ) (f : ℕ → α) : sum_from_to a (n+1) _ f = f (n+1) + sum_from_to a n _ f  := sorry

theorem sum_from_to_rec' {α : Type*} [has_add α] [has_zero α]
  (a : ℕ) (n : ℕ) (f : ℕ → α) : sum_from_to a n _ f = f a + sum_from_to (a+1) n _ f  := sorry

[Kevin Buzzard]

That sort of thing. Is that sufficiently close to something which is there already that I shouldn't bother? I want a mathematician-friendly interface for these things.

[Kevin Buzzard]

Oh also, summing f i j over i and then j should be the same as summing over j and then over i.

[Chris Hughes]

To prove S is finite from the partition, you could use set.fintype_Union. The combination of the following two lemmas, I wrote, should be enough to prove the stuff you're talking about, as I needed this stuff for Lagrange.

instance {α : Type*} [fintype α] (r : α → α → Prop) : fintype (quot r) :=
of_surjective (quot.mk r) (λ x, quot.exists_rep _)

lemma finset.sum_const {α β : Type*} [decidable_eq α] [add_comm_monoid β]
    (s : finset α) (b : β) : finset.sum s (λ a, b) = add_monoid.smul b (finset.card s) :=
finset.induction_on s (by simp) $ λ a s h hi,
by simp [finset.sum_insert h, finset.card_insert_of_not_mem h, hi, smul_succ]

theorem card_quot {α : Type*} [fintype α] (r : α → α → Prop) :
    card α = (finset.univ : finset (quot r)).sum (λ x, card {a // quot.mk r a = x}) :=
card_sigma (λ x, {a // quot.mk r a = x}) ▸
card_congr ⟨λ x, ⟨quot.mk r x, ⟨x, rfl⟩⟩, λ ⟨_, x, _⟩, x, λ _, rfl, λ ⟨_, _, ⟨_⟩⟩, rfl⟩

I think the final lemma might be easier to use with {a // quot.mk r a = x} substituted for {a // r a (quot.out x)}

[Kevin Buzzard]

I suspect that I can cobble together proofs of these things. Somehow I am asking something slightly different.

[Kevin Buzzard]

I am asking how to implement these general principles in such a way that mathematicians will be able to use them in a painless way.

[Kevin Buzzard]

For example, let's say I ask some mathematicians to prove that the sum of the first n integers is n(n+1)/2. If I asked them to prove this in an exam they would prove it by induction. They would observe that it's trivial for n=0 and then do the few lines of algebra which gets from n to n+1 and then say done by induction.

[Kevin Buzzard]

But in Lean they immediately need to make a call about how to formalise the statement and I can see several possibilities. And for each possibility there is a different theorem which supplies the fact that one can prove results of this kind by induction.

[Chris Hughes]

I had to do stuff similar to that for power series. My method was

local notation f ` ∑ ` : 90 n : 90  := finset.sum (finset.range n) f

lemma sum_range_succ : f ∑ succ n = f n + f ∑ n :=
have h : n ∉ finset.range n := by rw finset.mem_range; exact lt_irrefl _,
by rw [finset.range_succ, finset.sum_insert h]

and then you have the induction principle. This way I still get all the lemmas about finset.sum, like finset.sum_le_sum. Similar notation could be defined for sums between integers and products.
The main downside to this notation is it requires commutativity

[Kevin Buzzard]

Similarly, one could imagine being given a big group G, which is not finite, and then having a subtype H which is not yet known to be finite, and writing down a subgroup N of H and proving that N is finite and that there are only finitely many left cosets for N in H. That looks like quite a natural way to me of proving that H is finite. It is something I would let a student assume without comment if they wrote this in an exam.

[Kevin Buzzard]

So here you're summing from 0 to n-1, right?

[Chris Hughes]

yes, slightly annoying.

[Kevin Buzzard]

Although this is I am sure very pythonic, I think that in practice mathematicians often sum from either 0 to n or from 1 to n

[Kevin Buzzard]

So I think we need some notation for this plus a way of using it which is natural for mathematicians. Already when writing that sorried code above I noticed there was an issue with trying to figure out where the mathematician should insert the observation that a<=n+1 when summing from a to n (as otherwise this notation is not good).

[Kevin Buzzard]

Note that this is not an issue when a<=1.

[Chris Hughes]

For that stuff about groups, you could use
lemma group_equiv_cosets_times_subgroup (hs : is_subgroup s) : nonempty (α ≃ (cosets s × s)) in group_theory in mathlib, and fintype.of_equiv should do it quite easily.

[Patrick Massot]

@Kevin Buzzard did you read that Coq paper I linked to?

[Kevin Buzzard]

No, I've been really busy all week on other things. I was just trying to catch up with everything today. What Coq paper are you talking about?

[Kevin Buzzard]

The multinomial theorem is a particularly interesting example of a "finite sum fact" because the assertion is that (x1+x2+...+xn)^N is a sum over the "obviously finite" set of nats e1,e2,...,en whose sum is N. Somehow a mathematician does no work at all when proving that this set is finite, it is obvious because all the e_i are bounded by N. But in Lean I would have to think about how to implement this, which is not really what I want to do. What is the "correct" formulation of the multinomial theorem in Lean? n is typically fixed and the induction is on N in the normal proof -- if you try induction on n then you will get embroiled in more complicated multinomial coefficient identities. But maybe this doesn't even matter. Even proving the "obvious" statement that if e1+e2+...+en=N then e_i<=N seems like it might be some work. Is there any way of making some general theorems which mathematics students will be able to apply instinctively if they understand about nat but have no clue about fintype etc?

[Patrick Massot]

The one from this thread: www-sop.inria.fr/marelle/bigops/main.pdf

[Patrick Massot]

It's Coq's answer to your questions

[Patrick Massot]

But Johannes says it may use some magic that Lean doesn't have (yet?). @Sebastian Ullrich what do you think about this canonical instance thing? Is it already in Lean? Will it be in Lean 4?

[Andrew Ashworth]

i had no idea what a canonical structure was, but this paper was informative: https://hal.inria.fr/hal-00816703v1/document

[Andrew Ashworth]

from my 5-minute scanning of the paper, it seems like additional functionality for the type-class inference algorithm

[Sebastian Ullrich]

There are no plans to add canonical structures to Lean. I just read that paper as well (the conclusion at least), and it doesn't really list any advantages over type classes.

[Patrick Massot]

Then why does @Johannes Hölzl wrote this allows the big operators lib in Coq and it would be hard to do the same in Lean?

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/working.20with.20finite.20sequences/near/123533781

[Kevin Buzzard]

The "canonical big operators" paper that Patrick drew my attention to seems to be very relevant to some of the issues here, but it is always talking about canonical structures.

[Patrick Massot]

Maybe we should ping @Assia Mahboubi for more information here

[Kevin Buzzard]

So I am reading through her "Canonical Structures for the working Coq user" paper. The first example (bottom of p3, top of p4) seems to be easily solvable with type classes. I think it would be more helpful for me to see a problem which Canonical Structures solved naturally but which the type class system does not solve so naturally.

[Johannes Hölzl]

@Patrick Massot I don't know if canonical structures have an advantage over Lean's type classes. I also don't think so. The difference canonical structurs <-> type classes just means that we can not take the Coq approach to big operators one-to-one, but we need to see what a good approach in Lean is.

[Kevin Buzzard]

I am actively interested in this to the point that I am even trying to read the papers. I would love to hear @Assia Mahboubi 's thoughts on this issue. At the end of the day one of the things I am extremely interested in currently is trying to teach undergraduate mathematicians how to write undergraduate level mathematics in Lean. And the fact that Kenny Lau (who in a 2 week period wrote a bunch of Lean code to do MSc-level mathematics which localised an arbitrary ring at a multiplicative set and proved all the key lemmas which I needed for schemes), told me that he had real trouble proving Lagrange's theorem (which is a triviality to a mathematician) in Lean, makes me really think that there needs to be some progress here. How can I help? All I can see so far is that there are about three ways of formalising the underlying combinatorial statement because there are about three ways of working with the concept which the ZFC'ist knows as "a finite set". I am still not at all clear as to whether the best idea is to formalise all of them, or to formalise one of them and then to encourage the end users to use that one.

[Kevin Buzzard]

Could it really be the case that in practice in Lean, a mathematician might find that the finite group they are interested in today is a fintype, the one they are interested in tomorrow is a finset, and the one they are interested in the day after tomorrow is a group law on fin 60? Does that mean that they are doing it wrong, or does that mean that we need to be able to seamlessly translate all of these into one "canonical type for working with finite groups", or does that mean that the basic infrastructure needs to be written in all cases? These are fundamental questions and I do not have a clue as to what the best approach is.

[Mario Carneiro]

I'm actually a bit confused by your question and the purpose of your investigation. Mathlib already has a variety of mechanisms for dealing with finiteness in all its guises, and they are tested and used effectively in a variety of situations. What more do you want?

[Chris Hughes]

@Mario Carneiro I think the question is, there are loads of things dealing with finite sets, how do people know which one to use in which circumstance?

@Kevin Buzzard Finite groups always have to be a type, since group takes a type as an argument, and defining operations on finsets is messy. I tend to use finite sets mostly, and then coerce into a type whenever necessary, and not use finsets unless I'm doing finset.sum or I have to prove something 'obvious' about fintypes. I imagine finsets are better than finite sets for computability, which I don't really care about. There are things that I still don't really understand about finite sets like why for sets finite s and fintype sare both defined, given that the library doesn't usually try to avoid using choice. I always just use fintype s.

[Mario Carneiro]

Not using choice isn't the only reason to be constructive. Computable functions are literally evaluable by the VM, and mathlib is in part a programming library (reminder: it was once called stdlib)

[Mario Carneiro]

It's also often more convenient to work with a typeclass fintype rather than a predicate finite

[Mario Carneiro]

but they each have their uses, and after some discussion we decided to keep both

[Mario Carneiro]

If your theorem has a natural statement with both, then why not have two theorems?

[Chris Hughes]

I get that. What I don't understand is what is the advantage of finite over noncomputable fintype, given that neither is computable?

[Mario Carneiro]

finite is a Prop, so it has prop irrelevance stuff

[Mario Carneiro]

and it can be shoved into a set, etc

[Mario Carneiro]

Most of the time using the wrong notion will simply be a type error, and that's your hint at the different uses of each

[Mario Carneiro]

i.e. there is no finite.sum but there is finset.sum

[Chris Hughes]

That makes sense. I think the answer to @Kevin Buzzard 's question is that you just have to learn the differences between all the different forms of finite sets.

[Chris Hughes]

You can't really get away with trying to only use one of them

[Mario Carneiro]

right, they aren't alternatives, they are in complementary distribution

[Kevin Buzzard]

My question is this. Let's say I am about to write some teaching material to show 1st year undergraduate mathematicians how to formally verify the proof of Lagrange's theorem that they have seen in their undergraduate mathematics lectures. My goal is to make the Lean version of this proof look like the maths version, presented in a natural if somewhat pedantic way. If a student works through this material (which does not yet exist but I hope it will exist in the very near future) then at some point they will need to assert that some group or set is finite of size n. When they do this, I will have to teach them something about how Lean handles finite objects. Is there a natural "idiomatic" choice of how to model this situation in Lean, or should I simply write the teaching material for, say, finsets and fintypes? What I am trying to establish is whether somehow there is one "idiomatic" way to prove that if X is a finite object which has been broken up into m disjoint subobjects each of which have size d, then the size of X is m*d. What I am trying to stress is that in maths (i.e. in ZFC) this is _one theorem_. In Lean is it several theorems, and I should be expected to use whatever DTT-translation of this one ZFC theorem is appropriate given the way I have formalised the situation, or is there one DTT theorem that I should prove and then I should deduce the other variants from this theorem? If someone comes up in the future with a completely different DTT way of modelling finite sets, should I be expecting to port the proof of this one ZFC theorem to this new set-up? Is that how it works?

[Kevin Buzzard]

Similarly, there is only one multinomial theorem in ZFC. It says that if n is a nat and x1,x2,..,xn are n elements of a ring (or even a semiring) and if N is a nat, then (x1+x2+...+xn)^N is a sum, over the finite set of n-tuples (e1,e2,..,en) of nats such that the sum of the ei is N, of some multinomial coefficient times x1^e1 x2^e2 ... xn^en. If I were to formalise this in Lean I am going to have to make a call about what exactly I am summing over. So I have the same question. Is there some "canonical" answer to this in Lean, or should I consider all the multitude of ways that this finite set can be modelled in type theory and prove the multinomial theorem in every case, or should I consider all the multitude of ways that this finite set can be modelled in type theory, choose one of them, prove the multinomial theorem for that one, and then deduce it for the others using some low-tech stuff which I can be 100 percent sure that mathematicians won't be interested in because they don't care about applying the identity function in set theory.

[Kevin Buzzard]

The reason I am actively interested in these questions now is that I am going to write a lot of teaching materials for mathematics undergraduates, showing them how to do undergraduate level mathematics in Lean, so I really have to engage with the issue that whilst I can now do this kind of mathematics myself in Lean, I do not know the "best" way to do it, and I do not want to teach bad ways of doing things. I hope I have made my questions sufficiently precise that someone can say something illuminating about which path to take.

[Kevin Buzzard]

The tl;dr is basically "Formalise Lagrange's theorem in Lean, taking care to explain why you chose this way of doing it".

[Kevin Buzzard]

and similarly for the multinomial theorem

[Assia Mahboubi]

Hi @Kevin Buzzard , I have been away from zulip for a while, and I missed this very interesting discussion. I hope it's not too late to contribute. But there seem to be several interleaved topics here.
So I'll start with the trouble with the Lagrange trivial theorem. From my experience, there are two issues behind the formalization of this lemma. One is finiteness, but there is also a matter of avoiding to introduce "too many types" in the story.
At the end of the day, finite group theory is about studying the relative properties of subgroups, not much about the relative properties of the elements of a given group. So it should be easy to write (and not unreasonably difficult to prove) statements about groups (as opposed to statements about their elements). Therefore, it is a good idea to introduce a type for groups which can be easily combined, that is groups sharing the same law (and neutral element). And to reason about the (sub)groups of a same "domain".
As far as I can see, this is not the approach taken by @Johannes Hölzl here.
I was not able to find the proof by Chris that you mention, so may be you know all this very well already. Sorry for the noise in that case.
If not, and since you wrote that:

I am actively interested in this to the point that I am even trying to read the papers.

then I would suggest (sorry for the self recommendation) this note: https://hal.inria.fr/hal-00825074/file/main.pdf . Skip the beginning and start p.4.

In mathcomp, the "master" version of Lagrange theorem is here. I would suggest first looking to the statement rather than to the proof scripts. This one says that for any 2 (finite) groups G, H, the cardinal of the intersection of G and H, multiplied by the number of G-right cosets for elements in H (this is the index), is the cardinal of G. It is followed by a litany of variants and corollaries. The line where G and H are assumed to be sugroups of a same domain is here.

[Assia Mahboubi]

Should S be a finset, a fintype, or a set S for which finite S is true? What if we are given S as a subtype and we don't even know it's finite, and want to prove this from the fact that we can partition it up into m subsets of size d?

This one is easy: if this situation is really going to happen (proving finiteness from a presentation as a finite partition into finites), then S should be a non-necessarily finite set, and you would then add the finite S property to your conclusion.

[Kevin Buzzard]

Aah yes of course, if you don't know it's finite yet then it had better not be a type which is provably finite :-) What I am still confused about is whether one should prove three theorems (one for finsets, one for fintypes and one for finite sets) all of which say "if it's a disjoint union of X things of size Y, it has X*Y" or whether one should prove one theorem for one of them and deduce the analogous theorems for the other two. The reason this is troublesome for me is that in ZFC this is one theorem and some way I am still uncomfortable about making it three theorems in DTT.

[Andrew Ashworth]

this might be a dumb question, but shouldn't it be the case that if it holds for fintypes, it holds for finite sets and finsets?

[Andrew Ashworth]

the constructive interpretation is stronger than the classical ones

[Andrew Ashworth]

therefore if I knew a theorem was true and had a constructive interpretation I would prove that first and derive if for the others

[Assia Mahboubi]

There are no plans to add canonical structures to Lean. I just read that paper as well (the conclusion at least), and it doesn't really list any advantages over type classes.

Canonical structures/instances were implemented in Coq 10 years before type classes, by Amokrane Saïbi, who coined the name. The authors of the Coq type classes mechanism were not aware of canonical structures (which should really be called canonical instances). As far as I can tell, the "type class" vocabulary has been borrowed from the Haskell programming language, where it means something related but different though. The Mathematical components library started using canonical structures well before type classes became usable in Coq.

I am not sure that the exact difference between the two is very relevant to this thread. But for what it's worth the main advantage (a big one for my own usage) is that the user has full control on the instance searching strategy, for each class she declares. In Coq, instance look-up can become very subtle to control and result in seemingly non-terminating type-checking. Lean might very well be much better behaved in that respect, I have not tried enough. But it is difficult to illustrate this kind of trouble on toy examples, as one needs a non-trival hierarchy and a few instances populating it.

[Assia Mahboubi]

Then why does @Johannes Hölzl wrote this allows the big operators lib in Coq and it would be hard to do the same in Lean?

I do not Lean well enough to assess the feasibility of this transposition. @Johannes Hölzl is much more knowledgeable than I am... However I do not understand his post as saying that it would be hard but as saying that it would not be a straightforward direct transposition, as the inference mechanism used is a bit different. It might not be too hard though. Also, the big operators library uses its own, independent, hierarchy of structures (flavours of monoids) . Then operations of commutative rings for examples are declared as instances of these structures so that the corresponding infrastructure material becomes available. So in principle a big operator library on this model could start as an independent development.

[Andrew Ashworth]

@Kevin Buzzard it reminds me of your observation that "wow, lean developers really make metric spaces a subclass of topological spaces". all metric spaces are topological spaces, but not all topological spaces are metric-able . in the same way, (my poor understanding here is that) all fintypes can be considered as a finset or finite set, but the reverse isn't true

I think you could define it once for fintypes and then a tactic to move a proof on fintypes to a proof on finite sets

[Kevin Buzzard]

this might be a dumb question, but shouldn't it be the case that if it holds for fintypes, it holds for finite sets and finsets?

Well it holds for all of them so of course your assertion must be true :-) I don't know what "the constructive interpretation is stronger than the classical ones" actually means :-( because I have been classical for so long and have no feeling at all for constructive mathematics. But are you saying that I should prove it for fintypes and deduce it for the others? Johannes' proof doesn't use any finiteness at all, he just proves that G bijects with H x (G/H) in general, which is a stronger statement but I would imagine is not constructive (in fact I pretty much know for sure that it is not, if you had a given bijection then I imagine you would be able to choose an element in each coset, which surely requires the axiom of choice).

[Andrew Ashworth]

all I mean by stronger is that for all Propositions, if it holds for fintype, it must hold for a finite set

[Kevin Buzzard]

A mathematician wouldn't say "all metric spaces are topological spaces", they would say that there is a canonical construction that starts with a metric space and produces a completely different object, namely a topological space. It's easy to give examples of different metric spaces which give rise to the same topological space (e.g. take a metric space and then just double the metric, i.e. decree that every point is now twice as far from every other point as it used to be, like changing from miles to kilometres). My surprise was the fact that this construction had been embedded not as a functor from metric spaces to topological spaces, but as part of the definition of a metric space, when manifestly it is just extra junk which follows automatically from the definition of the functor and the axioms of a metric space. As a mathematician I am concerned about this, because in my normal working life I am interested in structures which are a bazillion times more complicated than topological spaces, and if we want every functor to be a forgetful functor then in Lean it sounds a priori that these objects will be terrifying. However since I have learnt about how Lean can be told to fill in structure fields automatically I am less concerned about this (although it still sounds like a very anti-computer-science thing to do: if I just defined you a metric space then why are you now going through the motions to define a topology on it when I might never be using it?)

[Andrew Ashworth]

this is because of how type-class inference works as a prolog-like search :)

[Andrew Ashworth]

if you imagine a hierarchy of types, it starts at the top and goes down

[Kevin Buzzard]

all I mean by stronger is that for all Propositions, if it holds for fintype, it must hold for a finite set

It might not be quite as easy -- e.g. if one proves that a subtype of a product of finitely many fintypes is a fintype, then it will be true that a subset of a product of finitely many finite sets is a finite set, but one can't just prove it by saying "every finite set is a fintype", one has to also prove that the functor from finite sets to fintypes commutes with a bunch of structures and furthermore that constructions on one side have some mirror on the other side.

[Andrew Ashworth]

it may not be trivial, but it can be automated

[Andrew Ashworth]

that's the whole point of the relator construction used in defining lean's integers (I think, somebody better at Lean than me correct me if I'm wrong).

[Kevin Buzzard]

And if my understanding is correct then if you want to do all this with the type class inference system then you are going to need to carry the fintype around as part of the structure of the finite set, and that might mean re-defining the finite set structure

[Kevin Buzzard]

My gut feeling is that you will need theorems such as "there's a bijection between the subsets of a finite set and the subtypes of a finite type, and the bijection preserves cardinality" -- that sort of thing. I am definitely not an expert in these matters and maybe it's all much easier than I am suggesting, but I hope I am getting my point across: currently I feel like every theorem about finite sets in ZFC seems to be translating into three theorems in DTT and I am still sort-of confused about which one I should be proving, or whether I should be proving all of them.

[Andrew Ashworth]

yes, exactly, you prove the bijection exists and a few other properties (i've never used relator) and then get a tactic out that moves proofs on fintype to finset

[Andrew Ashworth]

then, going forward, you write one proof for fintype and automatically get the other two

[Kevin Buzzard]

To go back to the other example, the multinomial theorem is a theorem that says (x1+x2+...+xn)^N = big finite sum of terms. In ZFC you just sum over the finite set {e1,e2,...,en} with ei all nats and their sum has to be N. If I formalise the multinomial theorem using a sum over a fintype, is it conceivable that someone in the future will want it but with a sum over a finite set instead? And if this happens, is it because they wrote bad code, or are they expected to deduce the formulation they want from the one I give them, or am I expected to prove three or four versions of the multinomial theorem? Here I could be summing over a finset, a fintype, a finite set or even a carefully-chosen finsupp type thing I suspect.

[Andrew Ashworth]

you could imagine defining a type class has_sum and providing instances for all of the above, that would make it easy to use, but not easy to write

[Andrew Ashworth]

but this is really getting above my paygrade, i feel like johannes or mario would have a more informed opinion

[Kevin Buzzard]

I should make clear my intentions here -- what I really really want to be able to do is to make things look easy for undergraduate mathematicians, who are used to the ZFC way. They only see one Lagrange theorem, and it's a theorem about finite groups, which are finite sets with some extra structure. They only see one multinomial theorem. When they sum from 1 to n (and they do, we often start at 1) they really do not care if [1...n] is a finset, fintype, list or whatever. They're just summing from 1 to n. I want to make Lean look like this to them because now I understand that this is possible -- I can tell them to type "import xena" on line 1 and then just do what I say to do all this sort of stuff. What I am unsure about is the best way of implementing it.

[Kevin Buzzard]

That is why I am asking all these weird questions. I want to write infrastructure which they will never see, cover it up with functions which I will point them to, and then hopefully deal with all their issues relatively easily.

[Kevin Buzzard]

And I just don't know if this is easy or unfeasible.

[Kevin Buzzard]

But I want to get on and write it.

[Kevin Buzzard]

Because it is in everyone's interests that mathematicians begin to think of these proof verification tools as normal, and easy to use.

[Kevin Buzzard]

And currently (for mathematicians) they are neither.

[Andrew Ashworth]

no need to edit that last sentence, it's true for cs as well

[Mario Carneiro]

@Kevin Buzzard I'm not sure you understood my point before, but let me say it this way: finset and finite are not interchangeable in any sense. They apply to completely different things - finset A is the collection of finite subsets of A, while finite s is a proof that s is a finite set. There are some obvious relations between these two, and they are all true, but "S is finite" and "the fin-powerset of A" just aren't the same concept and they need two different names.

[Mario Carneiro]

On the other hand, fintype is almost interchangeable with finite, in the sense that it is discussing roughly the same concept. Again there are applicability differences: fintype A takes a type, while finite s takes a set, and moreover the definition of finite s = nonempty (fintype s) should give you a strong hint at which is more generally applicable.

[Kevin Buzzard]

OK so fintype >> finite and now it's just between fintype and finset. Now the problem I envisage is that if someone puts a group structure on something of type fintype and then proves Lagrange's Theorem for it, can someone else now come along with a group structure on something of type finset and not be able to use it?

[Chris Hughes]

You can't define a group structure on something of type finset.

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

Can I get to "the underlying set"?

[Chris Hughes]

{x | x in s}

[Kevin Buzzard]

Oh meh the "underlying set" is an equivalence class of lists

[Chris Hughes]

There's a function in mathlib somewhere that does that, finset.to_set or something

[Kevin Buzzard]

your notation seems to work fine

[Kevin Buzzard]

it makes a set

[Kevin Buzzard]

def T := {x // x ∈ v} also works

[Chris Hughes]

\u s might even work

[Kevin Buzzard]

I stay away from \u

[Chris Hughes]

why?

[Mario Carneiro]

A "finite group" is a group whose elements are enumerated by a finset. That is fintype. There is no other reasonable interpretation here

[Kevin Buzzard]

I have always forgotten what it means 5 minutes after I use it

[Kevin Buzzard]

So the Lean word for "finite set" really is fintype? This is the type which I need to focus on when working with finite objects?

[Mario Carneiro]

a particular finset is not a type, so it can't have a group structure

[Chris Hughes]

Probably lots of useful stuff to put in docs. instances are on types, and function are generally on types.

[Kevin Buzzard]

I see. A finset is just a term, which has a type but which isn't a type

[Mario Carneiro]

If you have a finset s, then the type {x // x \in s} is a fintype, because it is enumerated by s

[Mario Carneiro]

One warning I should give is that fintype is in the "constructive fragment", which is to say that a construction of a fintype from other fintypes should be computable if possible

[Kevin Buzzard]

Some of my misunderstanding in this thread is because I have never worked with any of these finite objects before, so was asking questions which I could imagine could be well-formulated but in retrospect might not make any sense.

[Kevin Buzzard]

So I can't put a group structure "on a list", as it were. You see I am befuddled by all this set theory. everything is a set in set theory so you can attempt to put any structure on anything, in some sense.

[Mario Carneiro]

I think that once you work with these for a bit, you will notice the "complementary distribution" stuff I said: it's not actually a problem which to use in most cases, since they aren't interchangeable, so use the one that makes sense and it will probably be the right one

[Kevin Buzzard]

Not every term is a type.

[Kevin Buzzard]

use the one that makes sense and it will probably be the right one oh but I don't want to go back there.

[Kevin Buzzard]

That's exactly what starts getting me worried.

[Kevin Buzzard]

because it then sounds like someone else might be in some other situation where another choice is the right one for them, and then we will need two theorems that say the same thing, one for each choice. At least I can envisage that this might be the case. Does this simply not happen in practice?

[Mario Carneiro]

My point is that there is no choice, only one of them will make sense in a given situation

[Kevin Buzzard]

As I say, I think that to a certain extent it is my inexperience with type theory, and my attempt to push naive ideas over from set theory in an incorrect way, which have led me to this confusion. I am having to learn a new foundation for a subject which I know very well and for which I have have thought hard about foundational issues over the last few decades. Now I have to completely rewire myself. This is why I am so keen to teach students, because at the end of the day I don't think it matters what your foundation is.

[Kevin Buzzard]

but their minds haven't been polluted with ZFC yet.

[Mario Carneiro]

I think these issues come up in set theory too, which has enough soft typing to make sense of these ideas, if not formally

[Mario Carneiro]

If you have a list (x1, x2, x3), it's "elements" are some nonsense kuratowski stuff, that's not what you meant

[Kevin Buzzard]

No sure, it's the same with group theory, maybe a group is a 3-tuple or something, but we know what we mean by "elements" in any given case.

[Kevin Buzzard]

The point is that we can almost always coerce some elements out of the set, whereas in type theory it is just dawning on me that sometimes there is no "underlying type".

[Kevin Buzzard]

In set theory, even 4 is a set, so I could put a group law on it.

[Kevin Buzzard]

It's only just dawning on me that this doesn't even make sense in type theory.

[Kevin Buzzard]

Contrast my behaviour with Chris, who knows no set theory -- I am a professor and he is an undergraduate who has seen no set theory, and in some sense he has the advantage here because he realises what a nonsense idea it is to start putting a group structure on the number 4

[Kevin Buzzard]

whereas it's just something I've always known can be done but was junk.

[Kevin Buzzard]

But year after year after year in mathematics departments we are going to be teaching them either set theory, or no foundations at all. Any move to change this in the past would have been met with "but set theory is _fine_! It's worked for 100 years and who cares about the junk theorems".

[Kevin Buzzard]

I wonder if they teach type theory courses in the computer science department? Is that likely?

[Kevin Buzzard]

I know they teach Haskell in term 1 year 1

[Kevin Buzzard]

but I wonder if they take it any further.

[Kevin Buzzard]

https://psvg.doc.ic.ac.uk/2018/03/14/formal-methods-meets-js.html

[Kevin Buzzard]

https://psvg.doc.ic.ac.uk/2018/03/14/formal-methods-meets-js.html

[Kevin Buzzard]

happening about 50 metres from my office on Monday.

[Kevin Buzzard]

Do I care about javascript program verification?

[Kevin Buzzard]

https://psvg.doc.ic.ac.uk/teaching/separationlogic.html

[Kevin Buzzard]

any use for Lean?

[Kevin Buzzard]

I even know some of these people

[Simon Hudon]

That looks pretty useful. I started a separation logic package, in parts so that I can learn from it and in parts because it's useful

[Mario Carneiro]

In set theory, even 4 is a set, so I could put a group law on it.

The only difference between set theory and type theory here is that in type theory these are formally disallowed where in set theory they are just stupid things no one would ever bother to do. (In this case, 4 actually has a reasonable set theoretic interpretation, as the ordinal 4 = {0, 1, 2, 3}, and I can see at least one natural group on this set, but usually this isn't the case, you get some modeling specific thing that is "brittle" in the same sense as I've discussed with brittle proofs. It breaks an abstraction barrier.)

[Mario Carneiro]

The point I'm trying to make is that type theory should not be a major change from the mathematician's status quo. It is only disallowing things that we were all trying to avoid in the first place (i.e. junk theorems), so unless you were abusing the abstractions you shouldn't even notice the difference. (And if you were, well there are some coercions you will need to insert, like 4 -> fin 4.)

[Kenny Lau]

@Kevin Buzzard and @Kenny Lau I worked a little bit on finsupp: it got computable, i.e. the projection of the support of a finsupp are now rfl-lemmas. But more important: I added a induction lemma finsupp.induction_on.

I just realized that this breaks my tensor product, but I suppose it will make it easier

[Kenny Lau]

Do you see any easy proof of this?

theorem structural_theorem (f : free_abelian_group β γ) :
  ∃ S : finset (free_abelian_group β γ), (∀ g ∈ S, ∃ (x : β) (y : γ) (n : ℤ) (H : n ≠ 0), g = finsupp.single (x, y) n) ∧ S.sum id = f :=

[Kenny Lau]

nvm, I proved it