Lean, 66 bytes
def s:_->nat->nat|(m+1)(n+1):=(n+1)*(s m n+s m(n+1))|0 0:=1|_ _:=0
Try it online!
Proof of correctness
Try it online!
Explanation
Let us ungolf the function:
def s : nat->nat->nat
| (m+1) (n+1) := (n+1)*(s m n + s m (n+1))
| 0 0 := 1
| _ _ := 0
The function is defined by pattern matching and recursion, both of which have built-in support.
We define s(m+1, n+1) = (n+1) * (s(m, n) + s(m, n+1)
and s(0, 0) = 1
, which leaves open s(m+1, 0)
and s(0, n+1)
, both of which are defined to be 0
by the last case.
Lean uses lamdba calculus syntax, so s m n
is s(m, n)
.
Now, the proof of correctness: I stated it in two ways:
def correctness : ∀ m n, fin (s m n) ≃ { f : fin m → fin n // function.surjective f } :=
λ m, nat.rec_on m (λ n, nat.cases_on n s_zero_zero (λ n, s_zero_succ n)) $
λ m ih n, nat.cases_on n (s_succ_zero m) $ λ n,
calc fin (s (nat.succ m) (nat.succ n))
≃ (fin (n + 1) × (fin (s m n + s m (n + 1)))) :
(fin_prod _ _).symm
... ≃ (fin (n + 1) × (fin (s m n) ⊕ fin (s m (n + 1)))) :
equiv.prod_congr (equiv.refl _) (fin_sum _ _).symm
... ≃ (fin (n + 1) × ({f : fin m → fin n // function.surjective f} ⊕
{f : fin m → fin (n + 1) // function.surjective f})) :
equiv.prod_congr (equiv.refl _) (equiv.sum_congr (ih n) (ih (n + 1)))
... ≃ {f // function.surjective f} : s_aux m n
def correctness_2 (m n : nat) : s m n = fintype.card { f : fin m → fin n // function.surjective f } :=
by rw fintype.of_equiv_card (correctness m n); simp
The first one is what is really going on: a bijection between [0 ... s(m, n)-1]
and the surjections from [0 ... m-1]
onto [0 ... n-1]
.
The second one is how it is usually stated, that s(m, n)
is the cardinality of the surjections from [0 ... m-1]
onto [0 ... n-1]
.
Lean uses type theory as its foundation (instead of set theory). In type theory, every object has a type that is inherent to it. nat
is the type of natural numbers, and the statement that 0
is a natural number is expressed as 0 : nat
. We say that 0
is of type nat
, and that nat
has 0
as an inhabitant.
Propositions (statements / assertions) are also types: their inhabitant is a proof of the proposition.
def
: We are going to introduce a definition (because a bijection is really a function, not just a proposition).
correctness
: the name of the definition
∀ m n
: for every m
and n
(Lean automatically infers that their type is nat
, because of what follows).
fin (s m n)
is the type of natural numbers that is smaller than s m n
. To make an inhabitant, one provides a natural number and a proof that it is smaller than s m n
.
A ≃ B
: bijection between the type A
and the type B
. Saying bijection is misleading, as one actually has to provide the inverse function.
{ f : fin m → fin n // function.surjective f }
the type of surjections from fin m
to fin n
. This syntax builds a subtype from the type fin m → fin n
, i.e. the type of functions from fin m
to fin n
. The syntax is { var : base type // proposition about var }
.
λ m
: ∀ var, proposition / type involving var
is really a function that takes var
as an input, so λ m
introduces the input. ∀ m n,
is short-hand for ∀ m, ∀ n,
nat.rec_on m
: do recursion on m
. To define something for m
, define the thing for 0
and then given the thing for k
, build the thing for k+1
. One would notice that this is similar to induction, and indeed this is a result of the Church-Howard correspondence. The syntax is nat.rec_on var (thing when var is 0) (for all k, given "thing when k is k", build thing when var is "k+1")
.
Heh, this is getting long and I'm only on the third line of correctness
...