# The `Fintype`

derive handler #

This file defines a derive handler to automatically generate `Fintype`

instances
for structures and inductive types.

The following is a prototypical example of what this can handle:

```
inductive MyOption (α : Type*)
| none
| some (x : α)
deriving Fintype
```

This deriving handler does not attempt to process inductive types that are either recursive or that have indices.

To get debugging information, do `set_option trace.Elab.Deriving.fintype true`

and `set_option Elab.ProxyType true`

.

There is a term elaborator `derive_fintype%`

implementing the derivation of `Fintype`

instances.
This can be useful in cases when there are necessary additional assumptions (like `DecidableEq`

).
This is implemented using `Fintype.ofEquiv`

and `proxy_equiv%`

, which is a term elaborator
that creates an equivalence from a "proxy type" composed of basic type constructors. If Lean
can synthesize a `Fintype`

instance for the proxy type, then `derive_fintype%`

succeeds.

## Implementation notes #

There are two kinds of `Fintype`

instances that we generate, depending on the inductive type.

If it is an enum (an inductive type with only 0-ary constructors), then we generate the
complete `List`

of all constructors; see `Mathlib.Deriving.Fintype.mkFintypeEnum`

for more
details. The proof has $O(n)$ complexity in the number of constructors.

Otherwise, the strategy we take is to generate a "proxy type", define an equivalence between
our type and the proxy type (see `proxy_equiv%`

), and then use `Fintype.ofEquiv`

to pull a
`Fintype`

instance on the proxy type (if one exists) to our inductive type. For example, with
the `MyOption α`

type above, we generate `Unit ⊕ α`

. While the proxy type is not a finite type
in general, we add `Fintype`

instances for every type parameter of our inductive type (and
`Decidable`

instances for every `Prop`

parameter). Hence, in our example we get
`Fintype (MyOption α)`

assuming `Fintype α`

.

There is a source of quadratic complexity in this `Fintype`

instance from the fact that an
inductive type with `n`

constructors has a proxy type of the form `C₁ ⊕ (C₂ ⊕ (⋯ ⊕ Cₙ))`

,
so mapping to and from `Cᵢ`

requires looking through `i`

levels of `Sum`

constructors.
Ignoring time spent looking through these constructors, the construction of `Finset.univ`

contributes just linear time with respect to the cardinality of the type since the instances
involved compute the underlying `List`

for the `Finset`

as `l₁ ++ (l₂ ++ (⋯ ++ lₙ))`

with
right associativity.

Note that an alternative design could be that instead of using `Sum`

we could create a
function `C : Fin n → Type*`

with `C i = ULift Cᵢ`

and then use `(i : Fin n) × C i`

for
the proxy type, which would save us from the nested `Sum`

constructors.

This implementation takes some inspiration from the one by Mario Carneiro for Mathlib 3.
A difference is that the Mathlib 3 version does not explicitly construct the total proxy type,
and instead it opts to construct the underlying `Finset`

as a disjoint union of the `Finset.univ`

for each individual constructor's proxy type.

The term elaborator `derive_fintype% α`

tries to synthesize a `Fintype α`

instance
using all the assumptions in the local context; this can be useful, for example, if one
needs an extra `DecidableEq`

instance. It works only if `α`

is an inductive
type that `proxy_equiv% α`

can handle. The elaborator makes use of the
expected type, so `(derive_fintype% _ : Fintype α)`

works.

This uses `proxy_equiv% α`

, so as a side effect it defines `proxyType`

and `proxyTypeEquiv`

in
the namespace associated to the inductive type `α`

.

## Instances For

## Instances For

Derive a `Fintype`

instance for enum types. These come with a `toCtorIdx`

function.

We generate a more optimized instance than the one produced by `mkFintype`

.
The strategy is to (1) create a list `enumList`

of all the constructors, (2) prove that this
is in `toCtorIdx`

order, (3) show that `toCtorIdx`

maps `enumList`

to `List.range numCtors`

to show
the list has no duplicates, and (4) give the `Fintype`

instance, using 2 for completeness.

The proofs are all linear complexity, and the main computation is that
`enumList.map toCtorIdx = List.range numCtors`

, which is true by `refl`

.