Library Coq.Logic.FinFun
Functions on finite domains
Main result : for functions
f:A->A with finite
A,
f injective <-> f bijective <-> f surjective.
General definitions
Finiteness is defined here via exhaustive list enumeration
In many following proofs, it will be convenient to have
list enumerations without duplicates. As soon as we have
decidability of equality (in Prop), this is equivalent
to the previous notion.
Injections characterized in term of lists
Surjection characterized in term of lists
Main result :
An injective and surjective function is bijective.
We need here stronger hypothesis : decidability of equality in Type.
First, we show that a surjective f has an inverse function g such that
f.g = id.
Same, with more knowledge on the inverse function: g.f = f.g = id
An example of finite type : Fin.t
Instead of working on a finite subset of nat, another
solution is to use restricted nat->nat functions, and
to consider them only below a certain bound n.
We show that this is equivalent to the use of Fin.t n.
We can now use Proof via the equivalence ...