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
    Aug 27 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
    Aug 29 at 16:00

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.