Generalizing a lemma from a lemma for subsets of finite types to finite sets

Cyril Cohen published an extension to the Mathematical Components library to handle finite subsets of types.  In the course of experimenting with this extension, I need to generalize a lemma that already exists for finite subsets of finite types to finite sets.

The lemma is stated in the Mathematical Components library as follows:

Section CardFunImage.

Variables aT rT : finType.
Variables (f : aT -> rT) (D : pred aT).

Lemma imset_injP : reflect {in D &, injective f} (#|f @: D| == #|D|).

I wish to have the same lemma for finite sets. I express it in the following manner. Note that the notation of cardinals has to change, because #| … | is for predicates on finite types. The similar notion of cardinals for finite subset of arbitrary types is written #|`… |

  reflect{in D &, injective f} (#|` [fset f x | x in D] | == #|` D |).

I also need to change the type for D, because a predicate won’t be enough. There is a good reason: constructing the finite set of images of f for an arbitrary predicate on aT is not computable. On the other hand, if D is a known to be a finite set, it means it comes with an enumeration of its elements, which makes it possible to enumerate all elements of the image.

Proving this lemma is hard. I first try to just apply imset_injP, hoping coercions and canonical structure computations would fill in the necessary blanks, but that fails. Then I looked at the way imset_injP is proved. It relies on another theorem named image_injP, but this last theorem also relies on finite types. Here is an experiment we can make:

Check @image_injP [finType of D] [finType of (f @` D) _ predT.

image_injP
     : reflect {in predT &, injective ?s}
         (#|[seq ?s x | x in predT]| == #|predT|)

For this quick experiment, I had to leave a place holder _ for the third argument, because I did not know how to quicky transform f of type aT -> rT into a function between the finite types given as first and second argument.

A similar experiment with imset_injP uses the following formula:

Check @imset_injP [finType of D] [finType of (f @` D)] _ pred

To lift a function from type aT -> rT into a function between finite type D and f @` D, I finally chose to rely on Coq’s proof mode, as follows

Section experiment_draft.
Variable d1 : D.

Check f (val d1).
Check [finType of (f @` D)].

Definition fd : D -> [finType of (f @` D)].
Proof. 
move => d; exists (f (val d)); apply: in_imfset; case: d; move => e e_in; exact e_in.
Defined.

In these experiments, we see that d1 cannot be passed directly as argument to f, because d1 is not in type aT. But d1 is a qualified value, so just retrieving the value brings us back to aT. Now, the value f (val d1) is in type rT. Because we threw away the information that (val d1) is in D, we are missing the information that f (val d1) is in f @` D, but we can recover this thanks to lemma in_imfset.