0
$\begingroup$

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

Improve this question
$\endgroup$
2
  • 5
    $\begingroup$ 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.) $\endgroup$
    – Andrej Bauer
    Commented Aug 27, 2023 at 19:29
  • 2
    $\begingroup$ 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 $\endgroup$
    – cody
    Commented Aug 29, 2023 at 16:00

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.