# Formalization of partial functions for combinatorial counting

I need assistance in defining axioms for partial functions in total function theory that is available in Coq. Specifically, I'm looking for a constructive definition of a partial function that includes a constructor for obtaining a partial function from a smaller finite domain.

My use case involves formalizing the problem of counting the number of mappings from the set $$\{0, 1, 2\}$$ to $$\{0, 1, \ldots, 4\}$$. This can be represented as the size of the set of all such functions .Additionally, I am open to including the function extensionality axiom also thinking about using a default element in domain and range hear.

I formalized multiplication principles and solved the number of permutations problem using it.

assistance would be greatly appreciated

• Please describe the class of counting problems more precisely. Are you are counting just functions from $A$ to $B$? If so, you do not need any partial functions. Instead, prove $A^{B + C} \cong A^B \times A^C$, then $A^\mathsf{unit} \cong A$, then $\mathsf{Fin}(n + 1) \cong \mathsf{Fin}(n) + \mathsf{unit}$. (You will need function extensionality.) Commented Aug 27, 2023 at 19:29
• It might be worth drawing inspiration from (the very complete) proof of a similar fact in ssreflect: math-comp.github.io/htmldoc/mathcomp.ssreflect.finfun.html
– cody
Commented Aug 29, 2023 at 16:00