recursively defining binomial coefficients

Stream: new members

[Anand Rao]

Hello, I am trying to define binomial coefficients on $\mathbb{Z} \times \mathbb{Z}$ in LEAN using Pascal's relation. I want to keep the original definition on $\mathbb{N} \times \mathbb{N}$ and set it to $0$ everywhere else.
This is what I have done so far:

def binomial : ℕ → ℕ → ℕ
  | _ 0 := 1
  | 0 _ := 0
  | (n+1) (k+1) := binomial n (k+1) + binomial n k

def extendedbinomial : ℤ → ℤ → ℚ
  | (of_nat n) (of_nat k) := binomial n k
  | -[1+n] _ := 0
  | _ -[1+k] := 0

I am trying to condense this into a single definition, like this

def binomial : ℤ → ℤ → ℤ
  | (int.of_nat n) (int.of_nat k) :=
    match n, k with
      | 0, 0 := 1
      | 0, _ := 0
      | (n+1), k := binomial n (k-1) + binomial n k
    end
  | _ _ := 0

but this gives issues since LEAN cannot prove that this recurrence is well-founded. I would not like to split this into the cases 0 and k.succ to make it well-founded, since that unnecessarily complicates proofs. Is there any other way of defining the Pascal identity on $\mathbb{Z} \times \mathbb{Z}$?

[Mario Carneiro]

You need two definitions. This is easier in proofs in any case

[Mario Carneiro]

The other definition is basically naming that inner match statement in your combined definition, which will be extracted into an auxiliary anyway by lean

[Kevin Buzzard]

What about

open int

def extendedbinomial : ℤ → ℤ → ℕ
  | (of_nat n) (of_nat 0) := 1
  | (of_nat 0) _          := 0
  | (of_nat (n+1)) (of_nat (k+1)) := extendedbinomial (of_nat n) (of_nat (k + 1)) + extendedbinomial (of_nat n) (of_nat k)
  | -[1+n] _ := 0
  | _ -[1+k] := 0

?

[Mario Carneiro]

I don't think that will work, for the same reason it does work

[Mario Carneiro]

It's not structural recursive (although maybe it is well founded by the default metric)

[Anand Rao]

Kevin Buzzard said:

What about

open int

def extendedbinomial : ℤ → ℤ → ℕ
  | (of_nat n) (of_nat 0) := 1
  | (of_nat 0) _          := 0
  | (of_nat (n+1)) (of_nat (k+1)) := extendedbinomial (of_nat n) (of_nat (k + 1)) + extendedbinomial (of_nat n) (of_nat k)
  | -[1+n] _ := 0
  | _ -[1+k] := 0

?

Thank you, this seems to wrap both definitions into a common one.
I was also looking for a way to get the Pascal recurrence to apply to expressions of the form binomial n 0 (where n is an arbitrary natural number), instead of defining expressions of this form to be equal to 1. This makes proofs easier, since one doesn't have to distinguish between the k = 0 case and the k.succ case.

[Anand Rao]

Mario Carneiro said:

The other definition is basically naming that inner match statement in your combined definition, which will be extracted into an auxiliary anyway by lean

Actually with the inner match, I was trying to define the Pascal recurrence more generally so it applies to the k = 0 case as well.

[Anand Rao]

I tried the following definition as well with nbinomial n k = binomial (n-1) (k-1), but it didn't work

def nbinomial : ℤ → ℤ → ℤ
  | 0 _ := 0
  | n 0 := 0
  | 1 1 := 1
  | 1 _ := 0
  | _ 1 := 1
  | (n+2) (k+2) := nbinomial (n+1) (k+1) + nbinomial (n+1) (k+2)

[Mario Carneiro]

Anand Rao said:

I was also looking for a way to get the Pascal recurrence to apply to expressions of the form binomial n 0 (where n is an arbitrary natural number), instead of defining expressions of this form to be equal to 1. This makes proofs easier, since one doesn't have to distinguish between the k = 0 case and the k.succ case.

In that case, it would be more natural to not extend n to int and only do that for k. The recurrence is quite straightforward and structural recursive:

open int

def binomial : ℕ → ℤ → ℕ
| 0 0 := 1
| 0 _ := 0
| (n+1) k := binomial n (k-1) + binomial n k