Finset vs Finite

Stream: general

[Jeremy Avigad]

I am finally gearing up to write a new chapter on discrete mathematics for Mathematics in Lean. This will be useful, in part, because students in an introductory course on formalization often choose projects in the area. I am thinking of writing one section on finsets and fintypes in which we show examples of how to do counting arguments with that API. Then I would write another section on Finite and give examples of proofs using that. For those I would look for examples like Lagrange's theorem where there is a general set- or type-based API that one wants to restrict to the finite realm.

@Yaël Dillies @Bhavik Mehta does this seem like the right approach? The goal is to write something useful for people who want to use Mathlib now, but we can try to anticipate where the library is going on the Finset / Finite issue if there is a direction that should be encouraged.

[Yaël Dillies]

Thanks Jeremy for the ping. Your description is a bit too vague for me to have an informed opinion about the specifics (eg will you introduce docs#Finset.sum and do some bijection arguments? will you show induction on a finset vs induction on a fintype/finite type?), but overall I completely back this MIL chapter idea.

[Yaël Dillies]

I should also mention that once life has settled a bit I am planning on writing:

• A combinatorics chapter for MIL
• A finiteness game for adam.math.hhu.de

[Bhavik Mehta]

Yaël Dillies said:

I should also mention that once life has settled a bit I am planning on writing:

• A combinatorics chapter for MIL
• A finiteness game for adam.math.hhu.de

Also planning to help out with this combinatorics chapter! In the meantime, though, the talk I gave on combi at LftCM 2023 might be useful as a starting point: https://lftcm2023.github.io/tutorial/index.html. I can also give you the lean (lean4.0.0, but hopefully good enough!) file for this if valuable. The key things here - other than the basics of finsets - are demonstrations of how one can use Finset.sum and finsets to practically do a double-counting argument, and how more complex pigeonhole arguments can be expressed and formalised

[Jeremy Avigad]

Yaël Dillies said:

(eg will you introduce docs#Finset.sum and do some bijection arguments? will you show induction on a finset vs induction on a fintype/finite type?)

I definitely planned to do the first. If you can think of a good example where it makes sense to do induction on a Finite type, that would be great. Also, I plan to focus on a few basic examples. A more focused tutorial on combinatorics would be great.

[Yaël Dillies]

All my examples of fintype induction are sadly either doable using finset induction or too complicated to be explained in MIL :sad: I guess an example of the former still makes sense as demonstration of how to do it, but not really as a demonstration of why sometimes you need it.

[Jeremy Avigad]

@Bhavik Mehta Thanks for the pointer! I'll take a look. Do you mind if I use some of those examples, of course, with attribution?

[Eric Wieser]

For fintype induction specifically, it would be nice to fix (and first, file) the Lean bug that means the induction keyword cannot be used (which relates to [] vs () arguments)

[Notification Bot]

25 messages were moved from this topic to #general > FinEnum by Kim Morrison.

[Notification Bot]

A message was moved from this topic to #general > Fintype Induction by Kyle Miller.

[Gareth Ma]

Not sure if this is still the correct thread to talk about this or maybe we start a new one, but is it possible for the MIL combinatorics chapter to contain material about enumerative combinatorics? (Maybe it's a subset of the stuff mentioned above.) Last year, there was a group of people working on formalising the book "102 Combinatorial Problems from the training of the USA IMO team" (probably can't link it here), and many of them were counting that's easy for humans (e.g. stars and bars) but quite hard to formalise. e.g. Problem 13 of the easy section might be nice to demonstrate.

Find the number of ordered quadruples $(x_1, x_2, x_3, x_4)$ of positive odd integers that satisfy $x_1 + x_2 + x_3 + x_4 = 98$

[Gareth Ma]

import Mathlib.Tactic

def F : Type := { v : Fin 4 → ℕ // ∑ i, v i = 98 ∧ ∀ i, Odd (v i) }

example : Nat.card (Set.univ : Set F) = 19600 := by
  sorry

Something like this I guess

[Yaël Dillies]

Yeah, that's typically the kind of material that would be covered, although I think it would possibly be even more appropriate for the discrete mathematics chapter

[Gareth Ma]

That sounds like a better chapter name yea

[Kyle Miller]

It's possible to brute force that one but get the result with #eval rather than proving it (ran into maxRecDepth...)

import Mathlib

/-
Find the number of ordered quadruples $$(x_1, x_2, x_3, x_4)$$
of positive odd integers that satisfy $$x_1 + x_2 + x_3 + x_4 = 98$$
-/

def solutionSet :=
  {(x1, x2, x3, x4) : ℕ × ℕ × ℕ × ℕ | Odd x1 ∧ Odd x2 ∧ Odd x3 ∧ Odd x4 ∧ x1 + x2 + x3 + x4 = 98}

-- Goal: find a way to convince Lean that this is a Finset.

def comp := (Finset.Iic 98).filter Odd

def solutionSet2 :=
  comp ×ˢ comp ×ˢ comp ×ˢ comp
  |>.filter fun (x1, x2, x3, x4) => x1 + x2 + x3 + x4 = 98

theorem solutionSetEq :
    solutionSet = solutionSet2 := by
  ext ⟨x1, x2, x3, x4⟩
  simp [solutionSet, solutionSet2, comp]
  constructor
  · simp (config := {contextual := true})
    intros
    omega
  · tauto

instance : Fintype solutionSet := Fintype.ofFinset solutionSet2 (by rw [solutionSetEq]; simp)

#eval Fintype.card solutionSet
-- 19600

-- ideally
example : Fintype.card solutionSet = 19600 := rfl

[Gareth Ma]

Ah that's nice, in the edit history you can find my attempt of also proving Fintype, but I only proved Finite, oops

[Eric Wieser]

I was hoping this might be fast enough to work with rfl, but alas not:

abbrev e : (ℕ × ℕ × ℕ × ℕ) ≃ (Fin 4 → ℕ) where
  toFun := fun (a, b, c, d) => #[a, b, c, d].get
  invFun f := (f 0, f 1, f 2, f 3)
  left_inv p := by ext ⟨a, b, c, d⟩ <;> rfl
  right_inv p := by ext i; fin_cases i <;> rfl

def solutionSet3 :=
  ((Finset.finAntidiagonal 4 98).filter (fun f => ∀ i, Odd (f i))).map e.symm.toEmbedding


theorem solutionSetEq3 :
    solutionSet = solutionSet3 := by
  ext ⟨a, b, c, d⟩; simp [solutionSet3, solutionSet, Fin.forall_fin_succ, e, Fin.exists_fin_succ_pi, Fin.sum_univ_four]
  aesop

[Eric Wieser]

(this has the advantage that the set being filtered is much smaller)