Termination proof using Finset.range

Stream: new members

[Owen Anderson]

Does anyone I know speak enough Lean 4 to advise on how to complete this termination proof of the definition of the Bell numbers?

def bell_number : Nat → Nat
  | 0 => 1
  | n => (Finset.range n).sum (λ i => (Nat.choose (n-1) i) * (bell_number i))
decreasing_by {
  simp_wf
  rewrite [← Finset.mem_range]
  sorry
}

The goal is currently i ∈ Finset.range n which is obvious true to a human, but the proof context doesn't include the fact the derivation of i from Finset.range n. I feel like I need to "inline" the body of the lambda argument to Finset.sum in order to expose the source of I, but I'm struggling to find a tactic to achieve it.

[Eric Wieser]

It's probably better to use ∑ i : Fin n, ..., since then i.prop contains that proof

[Owen Anderson]

I spent a really long time trying to write it that way but could never get big operators to work for me. Lean 4 always rejected the open_locale command.

[Kyle Miller]

open_locale is not a Lean 4 command -- try open scoped BigOperators

[Kyle Miller]

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

def bell_number : Nat → Nat
  | 0 => 1
  | n => ∑ i : Fin n, Nat.choose (n - 1) i * bell_number i

[Kyle Miller]

Bigoperators are nice and make it more legible, but just so you know this is exactly the same as

def bell_number : Nat → Nat
  | 0 => 1
  | n => (Finset.univ : Finset (Fin n)).sum fun i => Nat.choose (n - 1) i * bell_number i

I.e., you sum over (Finset.univ : Finset (Fin n)) rather than Finset.range n.

[Eric Wieser]

You could also have summed over (Finset.range n).attach, which is essentially (but not quite) the same thing, and a more general solution to this problem

[Kevin Buzzard]

Is that natural subtraction correct BTW?

[Owen Anderson]

Kevin Buzzard said:

Is that natural subtraction correct BTW?

Yes? Nat.choose 0 0 is 1 so bell_number 1 = 1, which is correct.

[Ruben Van de Velde]

Why would you not write that as

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

def bell_number : Nat → Nat
  | 0 => 1
  | n + 1 => ∑ i : Fin (n + 1), Nat.choose n i * bell_number i

?

[Owen Anderson]

Seems the same?

[Kevin Buzzard]

No it's much better, because it doesn't involve natural subtraction which is a pathological function. Try proving theorems about the two versions if you're not convinced

[Kevin Buzzard]

But should it be Fin (n+1) @Ruben Van de Velde ?

[Ruben Van de Velde]

Yes, fixed

[Kevin Buzzard]

And maybe it's better to use range rather than Fin (again for ease of use later) because then you're not using unnecessary coercions which will also make your life harder.

[Kyle Miller]

@Kevin Buzzard The Fin is for the termination check. The alternative is using Finset.attach, which is no better.

[Kyle Miller]

One can prove that bell_number is equal to the range version though, and then you use that instead of the equation lemma

[Kevin Buzzard]

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

def bell_number : Nat → Nat
  | 0 => 1
  | n + 1 => ∑ i : Fin (n + 1), Nat.choose n i * bell_number i

lemma bell_number_succ (n : ℕ) :
    bell_number (n + 1) = ∑ i in Finset.range (n + 1), Nat.choose n i * bell_number i := by
  change ∑ i : Fin (n + 1), Nat.choose n i * bell_number i = _
  apply Finset.sum_bij (fun a _ => a.1)
  · rintro ⟨a, ha⟩ -
    rwa [Finset.mem_range]
  · intros; rfl
  · rintro ⟨a, ha⟩ ⟨b, hb⟩ - - ⟨⟩
    rfl
  · rintro b hb
    rw [Finset.mem_range] at hb
    exact ⟨b, by simp, by simp [Nat.mod_eq_of_lt hb]⟩

[Kyle Miller]

You beat me to it

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Set.Finite

open scoped BigOperators

def bell_number : Nat → Nat
  | 0 => 1
  | n + 1 => ∑ i : Fin (n + 1), Nat.choose n i * bell_number i

theorem Finset.sum_range_eq (α : Type*) [AddCommMonoid α] (f : Nat → α) (n : Nat) :
    ∑ i in Finset.range n, f i = ∑ i : Fin n, f i := by
  have : Fintype {i // i < n} := Set.fintypeLTNat n -- why doesn't this infer?
  rw [Finset.sum_subtype (F := this) (p := (· < n)) (Finset.range n) (by simp)]
  rw [Fintype.sum_equiv (Fin.equivSubtype)]
  simp

theorem bell_number_succ (n : Nat) :
    bell_number (n + 1) = ∑ i in Finset.range (n + 1), Nat.choose n i * bell_number i := by
  rw [bell_number, Finset.sum_range_eq]

[Kevin Buzzard]

Your proof is shorter though! I always fall back on sum_bij because I find it quite reliable :-)

[Kyle Miller]

Found the library lemma to make it shorter still:

import Mathlib.Data.Fintype.BigOperators

open scoped BigOperators

def bell_number : Nat → Nat
  | 0 => 1
  | n + 1 => ∑ i : Fin (n + 1), Nat.choose n i * bell_number i

theorem bell_number_succ (n : Nat) :
    bell_number (n + 1) = ∑ i in Finset.range (n + 1), Nat.choose n i * bell_number i := by
  rw [bell_number, ← Fin.sum_univ_eq_sum_range]

[Kevin Buzzard]

Ok that now looks pretty reasonable :-) So there's no termination_by trick to make the non-Fin definition work out of the box?

[Eric Wieser]

You could presumably rewrite back into the fin version in the termination_by somehow

[Kyle Miller]

By the way, for computing bell numbers this has much better runtime complexity:

def bell_number_aux (acc : Array Nat) : Nat → Array Nat
  | 0 => acc.push 1
  | n + 1 =>
    let acc := bell_number_aux acc n
    acc.push (∑ i in Finset.range (n + 1), Nat.choose n i * acc[i]!)

def bell_number (n : Nat) : Nat := (bell_number_aux #[] n)[n]!

(I wouldn't define the main bell_number this way! If you prove them equal, you can add a @[csimp] lemma. This version handles bell_number 100 instantly, where I got impatient with the other version.)