combinatorial calculations

Stream: general

[Jeremy Avigad]

This week, I want to show my students how to do "easy" combinatorial calculations with fintypes and finsets, so I gave this one a try:

import algebra.big_operators.fin
import tactic

open finset

example (n : ℕ) :
  card (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2)) = n * (n + 1) / 2 :=
...

To my dismay, it took me 30 lines. Can anyone show me the canonical way to do this?

[Yaël Dillies]

17 lines

import data.sym.card

namespace nat
variables {a b c : ℕ}

protected lemma eq_div_of_mul_eq_left (hb : 0 < b) (h : a * b = c) : a = c / b :=
(nat.div_eq_of_eq_mul_left hb h.symm).symm

protected lemma eq_div_of_mul_eq_right (hb : 0 < b) (h : b * a = c) : a = c / b :=
(nat.div_eq_of_eq_mul_right hb h.symm).symm

end nat

open finset

example (n : ℕ) :
  card (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2)) = n * (n + 1) / 2 :=
begin
  refine nat.eq_div_of_mul_eq_left zero_lt_two _,
  have : (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2)).card =
    (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.2 < p.1)).card,
  { rw ←finset.card_map ⟨prod.swap, prod.swap_injective⟩,
    congr' 1,
    convert map_filter.symm,
    { refl },
    { simp },
    { apply_instance } },
  rw mul_two,
  nth_rewrite 1 this,
  rw [←card_union_eq, ←filter_or],
  have : (λ (a : fin (n + 1) × fin (n + 1)), a.fst < a.snd ∨ a.snd < a.fst) = λ a, a.1 ≠ a.2 :=
    funext (λ _, propext lt_or_lt_iff_ne),
  simp_rw [this, ←univ_product_univ],
  exact (off_diag_card _).trans (by simp [add_mul]),
  { exact disjoint_filter.2 (λ x _, lt_asymm) }
end

[Yaël Dillies]

The pain points here are

• simp_rw isn't smart enough to rewrite p in the decidable_pred p of finset.filter, so you need to explicit it more
• docs#finset.map_filter doesn't seem to have a convenient variant for equiv

[Yaël Dillies]

Without those pain points I would be at 7 lines.

[Jeremy Avigad]

That solution is still surprisingly difficult, and it requires knowing about off_diag. My lower-tech solution is here:

longer proof

import algebra.big_operators.fin
import tactic

open finset

example (n : ℕ) :
card (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2)) = n * (n + 1) / 2 :=
begin
have : univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2) =
finset.bUnion univ
(λ j : fin (n + 1), finset.image (λ i : fin j, (⟨i.val, i.property.trans j.property⟩, j)) univ),
begin
ext x, simp [prod.ext_iff], split,
{ intro h, use ⟨x.fst, h⟩, simp },
rintros ⟨x', h⟩,
rw ←h,
apply x'.property
end,
rw [this, finset.card_bUnion],
clear this, swap,
{ intros x _ y _ xney z,
simp only [inf_eq_inter, mem_inter, mem_image, mem_univ, prod.ext_iff],
rintros ⟨⟨_, _, _, rfl⟩, ⟨_, _, _, rfl⟩⟩,
contradiction },
transitivity ((univ : finset (fin (n + 1))).sum (λ u, ↑u)),
{ congr,
ext x,
rw [finset.card_image_of_injective],
{ rw finset.card_fin },
intros i1 i2, simp [fin.ext_iff] },
symmetry,
apply nat.div_eq_of_eq_mul_left (show 0 < 2, by norm_num),
induction n with n ih,
{ simp },
rw [fin.sum_univ_cast_succ, add_mul],
simp only [fin.coe_cast_succ, fin.coe_last],
rw [←ih, nat.succ_eq_add_one],
ring
end

[Yaël Dillies]

Have you tried induction directly? I doubt it will be shorter, but who knows. The advantage is that the equivalences you need to prove should be easier.

[Jeremy Avigad]

I started, and got tired... but maybe I'll try again tomorrow.

[Kevin Buzzard]

Jeremy I think we have different opinions on this but I'll say again that I would never be showing nat.div to undergraduates simply on the basis that it's not the function they think it is. I always coerce to rat first, where clearing denominators doesn't require nat-specific tricks.

[Kevin Buzzard]

(btw you can write code in spoilers using four backticks)

[Kevin Buzzard]

I would expect this to be hard because the obvious proof is by picture :-(

[Mario Carneiro]

(and you can syntax highlight that code if you use lean after the four backticks)

[Johan Commelin]

Is the proof easier with rat.div? Can qify easily move from the nat.div to the rat.div version?

[Floris van Doorn]

The proof is not easier with rat.div (it is slightly harder), there is no pain in the proof from using nat.div (but I understand that you might want to avoid it for pedagogical reasons).

[Floris van Doorn]

@Jeremy Avigad your first have can be proven by simp with a little more information, by

{ ext x, simp [prod.ext_iff], simp [fin.exists_iff, fin.ext_iff] },

or as a single simp call, by

{ simp [finset.ext_iff, prod.ext_iff, fin.exists_iff, fin.ext_iff, @and.left_comm _ (_ = _)] },

Moreover, if you prefer a version with fewer casts, you can prove "the same" lemma using docs#finset.range:

example (n : ℕ) :
  card ((range (n+1) ×ˢ range (n+1)).filter (λ p, p.1 < p.2)) = n * (n + 1) / 2 :=
begin
  have : (range (n+1) ×ˢ range (n+1)).filter (λ p, p.1 < p.2) =
    (finset.range (n+1)).bUnion (λ j : ℕ, (range j).image $ λ i, (i, j)),
  { simp [finset.ext_iff, prod.ext_iff, @and.left_comm _ (_ = _), iff_true_intro lt_trans] },
  rw [this, finset.card_bUnion]; clear this,
  swap,
  { intros x _ y _ xney z,
    simp_rw [inf_eq_inter, mem_inter, mem_image, mem_range, prod.ext_iff],
    rintros ⟨⟨_, _, _, rfl⟩, ⟨_, _, _, rfl⟩⟩,
    contradiction },
  transitivity (∑ i in range (n+1), i),
  { congr,
    ext x,
    rw [finset.card_image_of_injective, card_range],
    intros i1 i2, simp },
  rw [finset.sum_range_id, add_tsub_cancel_right, mul_comm],
  -- if you want to do the induction proof:
  -- symmetry,
  -- apply nat.div_eq_of_eq_mul_left (show 0 < 2, by norm_num),
  -- induction n with n ih,
  -- { simp },
  -- rw [sum_range_succ, add_mul, ← ih, nat.succ_eq_add_one],
  -- ring
end

[Kevin Buzzard]

This is a great example of something which should be easy @Oliver Nash

[Jeremy Avigad]

Thanks! I take Floris' proof to be the canonical formalization of "it's just adding up the numbers from 1 to n." Over time, I'd like to see MIL grow with chapters that show people the idiomatic ways to carry out proofs in different areas, and this is perfect for a chapter on discrete math and combinatorics. Yaël's formalization is a pretty good formalization of the picture proof, and it is worth knowing the best way to formalize that too.

@Kevin Buzzard, I have no trouble telling students about division on nat and int. The class is about evenly split between math students and computer science students, and the computer science students are perfectly comfortable with div and mod on integers. Actually, mathematics students are generally familiar with it too, but in any case it only takes a minute to tell them what it is. We don't have to worry about the computer science corrupting the math students. They are adults. They can handle it. I do tell them that, for practical reasons, it is generally best to avoid subtraction on nat and division on nat and int, and you are right that in a library it might be better to state the version without division.

This is a teaching moment in another sense: I often tell students that Zulip is a good place to talk about things they are working on. I'll show them my original proof and then the ones by Yaël and Floris to underscore that point.

[Joanna Choules]

This is a proof – also summation-based – that I found; a little messy* but fairly short:

import algebra.big_operators.fin
import algebra.big_operators.intervals
import tactic

open finset

example (n : ℕ) :
  card (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2)) = n * (n + 1) / 2 :=
begin
  rw [card_eq_sum_ones, sum_filter,
      sum_finset_product_right _ (@univ _ (fin.fintype _)) (λ _, @univ _ (fin.fintype _))],
  swap, { simp, },
  simp_rw [sum_boole, nat.cast_id],
  conv { to_lhs,
         congr,
         skip,
         funext,
         rw [filter_gt_eq_Iio, Iio_eq_Ico, fin.card_Ico, fin.bot_eq_zero, fin.coe_zero, tsub_zero,
             ←id.def ↑x], },
  rw fin.sum_univ_eq_sum_range,
  simp_rw id.def,
  rw finset.sum_range_id,
  simp [mul_comm],
end

* I would especially have liked to trim down the conv block a bit by using conv in (card _), but for some reason this caused the rewrites not to stick.

[Alex J. Best]

I couldn't reproduce the issue yo mentioned about the conv block, the following golf works for me:

import algebra.big_operators.fin
import algebra.big_operators.intervals
import tactic

open finset

example (n : ℕ) :
  card (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2)) = n * (n + 1) / 2 :=
begin
  rw [card_eq_sum_ones, sum_filter,
      sum_finset_product_right _ (@univ _ (fin.fintype _)) (λ _, @univ _ (fin.fintype _))],
  swap, { simp, },
  simp_rw [sum_boole, nat.cast_id],
  conv in (card _) {
    rw [filter_gt_eq_Iio, Iio_eq_Ico, fin.card_Ico, fin.bot_eq_zero, fin.coe_zero], },
  erw fin.sum_univ_eq_sum_range id,
  simp [finset.sum_range_id, mul_comm],
end

[Joanna Choules]

Huh, and now I can't reproduce it either. I guess it must've only been when I was focusing filter _ _.

[Bhavik Mehta]

example (n : ℕ) :
  card (univ.filter (λ p : fin (n + 1) × fin (n + 1), p.1 < p.2)) = n * (n + 1) / 2 :=
begin
  rw [←univ_product_univ, card_eq_sum_ones, sum_filter, sum_product_right],
  simp only [sum_boole, nat.cast_id, filter_gt_eq_Iio, fin.card_Iio],
  erw fin.sum_univ_eq_sum_range id,
  simp [finset.sum_range_id, mul_comm],
end

[Bhavik Mehta]

I think the most annoying thing here is that I need to do this erw step

[Kevin Buzzard]

I guess "how few lines can an expert get it down to" is different to "do we expect an undergraduate to be able to knock this off easily" though. It would be lovely if this were easy even if you weren't an expert.

[Bhavik Mehta]

Agreed - I've done many calculations like this, especially for the unit fractions project

[Patrick Massot]

It also depends on whether this expertise is teachable. Bhavik, do you think you could write a MiL chapter about combinatorics that could allow people to learn how to do such proofs efficiently?

[Bhavik Mehta]

I could try, but I'm not confident yet that it'd be very helpful - I'd need to think seriously first about if there are techniques useful to teach or if it's just familiarity with what's in the library and experience, which might be harder to put into words

[Patrick Massot]

That's exactly the question indeed.

[Bhavik Mehta]

@Thomas Bloom I think you had a cheat sheet for some tricks we used a lot, though I don't remember how many of them apply here?

[Yaël Dillies]

I could certainly put together such a tutorial. I just had to teach this at Kevin's workshop.

[Bhavik Mehta]

Yeah I had to teach similar stuff, but I think it's hard to condense this into a useful tutorial