# Zulip Chat Archive

## 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
```

?

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

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 ?

#### Ruben Van de Velde (Nov 04 2023 at 21:39):

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