Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Binomial Coefficient as Factorial

Email Gateway (Aug 19 2022 at 17:09):

From: Bob Fang <bf283@cam.ac.uk>
Dear all,

Hi, in Isabelle the definition we have for Binomial Coefficient is:

primrec binomial :: "nat ⇒ nat ⇒ nat" (infixl "choose" 65)

where

"0 choose k = (if k = 0 then 1 else 0)"

| "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose
k))"

But according to my (limited) number theory knowledge, n choose k can also
be calculated using factorials and n choose k = n! / k! *(n-k)!.

So I want to prove the following lemma:

fun fac :: "nat ⇒ nat" where

"fac 0 = Suc 0"

| "fac n = n * fac (n - 1)"

lemma bin_as_fac[simp]:"n choose k = fac n div ((fac k) * fac (n - k))"

try

When I typed try Isabelle quickly found a counter example for me,

n = 0

k = Suc 0

Evaluated terms:

n choose k = 0

fac n div (fac k * fac (n - k)) = Suc 0

I am just wondering where did things went wrong? Is the two calculation of
binomial coefficient not compatible with each other?

Thanks a lot.

Best,

Bob

Email Gateway (Aug 19 2022 at 17:09):

From: Manuel Eberl <eberlm@in.tum.de>
The problem is quite simply that these two definitions of the binomial
coefficient are only equivalent for 0 ≤ k ≤ n. You may be interested in
the lemma binomial_altdef_nat from the Isabelle library:

k ≤ n ⟹ n choose k = fact n div (fact k * fact (n - k))

Last updated: Nov 21 2024 at 12:39 UTC