## Stream: new members

### Topic: Termination proof using Finset.range

#### Owen Anderson (Nov 04 2023 at 17:27):

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 (Nov 04 2023 at 17:38):

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

#### Owen Anderson (Nov 04 2023 at 17:41):

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 (Nov 04 2023 at 17:45):

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

#### Kyle Miller (Nov 04 2023 at 17:47):

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 (Nov 04 2023 at 17:48):

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 (Nov 04 2023 at 18:00):

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 (Nov 04 2023 at 19:36):

Is that natural subtraction correct BTW?

#### Owen Anderson (Nov 04 2023 at 20:07):

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 (Nov 04 2023 at 20:43):

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


?

Seems the same?

#### Kevin Buzzard (Nov 04 2023 at 21:37):

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 (Nov 04 2023 at 21:38):

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

Yes, fixed

#### Kevin Buzzard (Nov 04 2023 at 21:40):

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 (Nov 04 2023 at 21:44):

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

#### Kyle Miller (Nov 04 2023 at 21:45):

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 (Nov 04 2023 at 21:59):

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 (Nov 04 2023 at 22:00):

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 (Nov 04 2023 at 22:02):

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

#### Kyle Miller (Nov 04 2023 at 22:05):

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 (Nov 04 2023 at 22:06):

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 (Nov 04 2023 at 22:18):

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

#### Kyle Miller (Nov 04 2023 at 22:21):

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.)

Last updated: Dec 20 2023 at 11:08 UTC