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.

def Mathlib.Deriving.Fintype.«termDerive_fintype%_» : Lean.ParserDescr

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 α.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Deriving.Fintype.mkFintype (declName : Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Deriving.Fintype.mkFintypeEnum (declName : Lean.Name) : Lean.Elab.Command.CommandElabM Unit

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Deriving.Fintype.mkFintypeInstanceHandler (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

• One or more equations did not get rendered due to their size.