mathlib documentation

tactic.​derive_fintype

tactic.​derive_fintype

Derive handler for fintype instances

This file introduces a derive handler to automatically generate fintype instances for structures and inductives.

Implementation notes

To construct a fintype instance, we need 3 things:

  1. A list l of elements
  2. A proof that l has no duplicates
  3. A proof that every element in the type is in l

Now fintype is defined as a finset which enumerates all elements, so steps (1) and (2) are bundled together. It is possible to use finset operations that remove duplicates to avoid the need to prove (2), but this adds unnecessary functions to the constructed term, which makes it more expensive to compute the list, and it also adds a dependence on decidable equality for the type, which we want to avoid.

Because we will rely on fintype instances for constructor arguments, we can't actually build a list directly, so (1) and (2) are necessarily somewhat intertwined. The inductive types we will be proving instances for look something like this:

@[derive fintype]
inductive foo
| zero : foo
| one : bool  foo
| two :  x : fin 3, bar x  foo

The list of elements that we generate is

{foo.zero}
 (finset.univ : bool).map (λ b, finset.one b)
 (finset.univ : Σ' x : fin 3, bar x).map (λ x, y⟩, finset.two x y)

except that instead of , that is finset.union, we use finset.disj_union which doesn't require any deduplication, but does require a proof that the two parts of the union are disjoint. We use finset.cons to append singletons like foo.zero.

The proofs of disjointness would be somewhat expensive since there are quadratically many of them, so instead we use a "discriminant" function. Essentially, we define

def foo.enum : foo  
| foo.zero := 0
| (foo.one _) := 1
| (foo.two _ _) := 2

and now the existence of this function implies that foo.zero is not foo.two and so on because they map to different natural numbers. We can prove that sets of natural numbers are mutually disjoint more easily because they have a linear order: 0 < 1 < 2 so 0 ≠ 2.

To package this argument up, we define finset_above foo foo.enum n to be a finset s together with a proof that all elements a ∈ s have n ≤ enum a. Now we only have to prove that enum foo.zero = 0, enum (foo.one _) = 1, etc. (linearly many proofs, all rfl) in order to prove that all variants are mutually distinct.

We mirror the finset.cons and finset.disj_union functions into finset_above.cons and finset_above.union, and this forms the main part of the finset construction.

This only handles distinguishing variants of a finset. Now we must enumerate the elements of a variant, for example {foo.one ff, foo.one tt}, while at the same time proving that all these elements have discriminant 1 in this case. To do that, we use the finset_in type, which is a finset satisfying a property P, here λ a, foo.enum a = 1.

We could use finset.bind many times to construct the finset but it turns out to be somewhat complicated to get good side goals for a naturally nodup version of finset.bind in the same way as we did with finset.cons and finset.union. Instead, we tuple up all arguments into one type, leveraging the fintype instance on psigma, and then define a map from this type to the inductive type that untuples them and applies the constructor. The injectivity property of the constructor ensures that this function is injective, so we can use finset.map to apply it. This is the content of the constructor finset_in.mk.

That completes the proofs of (1) and (2). To prove (3), we perform one case analysis over the inductive type, proving theorems like

foo.one a  {foo.zero}
   (finset.univ : bool).map (λ b, finset.one b)
   (finset.univ : Σ' x : fin 3, bar x).map (λ x, y⟩, finset.two x y)

by seeking to the relevant disjunct and then supplying the constructor arguments. This part of the proof is quadratic, but quite simple. (We could do it in O(n log n) if we used a balanced tree for the unions.)

The tactics perform the following parts of this proof scheme:

def derive_fintype.​finset_above (α : Type u_1) :
(α → )Type u_1

A step in the construction of finset.univ for a finite inductive type. We will set enum to the discriminant of the inductive type, so a finset_above represents a finset that enumerates all elements in a tail of the constructor list.

Equations
def derive_fintype.​mk_fintype {α : Type u_1} (enum : α → ) (s : derive_fintype.finset_above α enum 0) :
(∀ (x : α), x s.val)fintype α

Construct a fintype instance from a completed finset_above.

Equations
def derive_fintype.​finset_above.​cons {α : Type u_1} {enum : α → } (n : ) (a : α) :
enum a = nderive_fintype.finset_above α enum (n + 1)derive_fintype.finset_above α enum n

This is the case for a simple variant (no arguments) in an inductive type.

Equations
theorem derive_fintype.​finset_above.​mem_cons_self {α : Type u_1} {enum : α → } {n : } {a : α} {h : enum a = n} {s : derive_fintype.finset_above α enum (n + 1)} :

theorem derive_fintype.​finset_above.​mem_cons_of_mem {α : Type u_1} {enum : α → } {n : } {a : α} {h : enum a = n} {s : derive_fintype.finset_above α enum (n + 1)} {b : α} :

def derive_fintype.​finset_above.​nil {α : Type u_1} {enum : α → } (n : ) :

The base case is when we run out of variants; we just put an empty finset at the end.

Equations
@[instance]
def derive_fintype.​inhabited (α : Type u_1) (enum : α → ) (n : ) :

Equations
@[nolint]
def derive_fintype.​finset_in {α : Type u_1} :
(α → Prop)Type u_1

This is a finset covering a nontrivial variant (with one or more constructor arguments). The property P here is λ a, enum a = n where n is the discriminant for the current variant.

Equations
def derive_fintype.​finset_in.​mk {α : Type u_1} {P : α → Prop} (Γ : Type u_2) [fintype Γ] (f : Γ → α) :
function.injective f(∀ (x : Γ), P (f x))derive_fintype.finset_in P

To construct the finset, we use an injective map from the type Γ, which will be the sigma over all constructor arguments. We use sigma instances and existing fintype instances to prove that Γ is a fintype, and construct the function f that maps ⟨a, b, c, ...⟩ to C_n a b c ... where C_n is the nth constructor, and mem asserts enum (C_n a b c ...) = n.

Equations
theorem derive_fintype.​finset_in.​mem_mk {α : Type u_1} {P : α → Prop} {Γ : Type u_2} {s : fintype Γ} {f : Γ → α} {inj : function.injective f} {mem : ∀ (x : Γ), P (f x)} {a : α} (b : Γ) :
f b = aa (derive_fintype.finset_in.mk Γ f inj mem).val

def derive_fintype.​finset_above.​union {α : Type u_1} {enum : α → } (n : ) :
derive_fintype.finset_in (λ (a : α), enum a = n)derive_fintype.finset_above α enum (n + 1)derive_fintype.finset_above α enum n

For nontrivial variants, we split the constructor list into a finset_in component for the current constructor and a finset_above for the rest.

Equations
theorem derive_fintype.​finset_above.​mem_union_left {α : Type u_1} {enum : α → } {n : } {s : derive_fintype.finset_in (λ (a : α), enum a = n)} {t : derive_fintype.finset_above α enum (n + 1)} {a : α} :

theorem derive_fintype.​finset_above.​mem_union_right {α : Type u_1} {enum : α → } {n : } {s : derive_fintype.finset_in (λ (a : α), enum a = n)} {t : derive_fintype.finset_above α enum (n + 1)} {a : α} :

Construct the term Σ' (a:A) (b:B a), C a b from Π (a:A) (b:B a), C a b → T (the type of a constructor).

Prove the goal (Σ' (a:A) (b:B a), C a b) → T (this is the function f in finset_in.mk) using recursive psigma.elim, finishing with the constructor. The two arguments are the type of the constructor, and the constructor term itself; as we recurse we add arguments to the constructor application and destructure the pi type of the constructor. We return the number of psigma.elim applications constructed, which is one less than the number of constructor arguments.

Prove the goal a, b |- f a = f b → g a = g b where f is the function we constructed in mk_sigma_elim, and g is some other term that gets built up and eventually closed by reflexivity. Here a and b have sigma types so the proof approach is to case on a and b until the goal reduces to C_n a1 ... am = C_n b1 ... bm → ⟨a1, ..., am⟩ = ⟨b1, ..., bm⟩, at which point cases on the equality reduces the problem to reflexivity.

The arguments are the number m returned from mk_sigma_elim, and the hypotheses a,b that we need to case on.

Prove the goal a |- enum (f a) = n, where f is the function constructed in mk_sigma_elim, and enum is a function that reduces to n on the constructor C_n. Here we just have to case on a m times, and then reflexivity finishes the proof.

Prove the goal |- finset_above T enum k, where T is the inductive type and enum is the discriminant function. The arguments are args, the parameters to the inductive type (and all constructors), k, the index of the current variant, and cs, the list of constructor names. This uses finset_above.cons for basic variants and finset_above.union for variants with arguments, using the auxiliary functions mk_sigma, mk_sigma_elim, mk_sigma_elim_inj, mk_sigma_elim_eq to close subgoals.

Prove the goal |- Σ' (a:A) (b: B a), C a b given a list of terms a, b, c.

This function is called to prove a : T |- a ∈ S.1 where S is the finset_above constructed by mk_finset, after the initial cases on a : T, producing a list of subgoals. For each case, we have to navigate past all the variants that don't apply (which is what the tac input tactic does), and then call either finset_above.mem_cons_self for trivial variants or finset_above.mem_union_left and finset_in.mem_mk for nontrivial variants. Either way the proof is quite simple.

Proves |- fintype T where T is a non-recursive inductive type with no indices, where all arguments to all constructors are fintypes.

Tries to derive a fintype instance for inductives and structures.

For example:

@[derive fintype]
inductive foo (n m : )
| zero : foo
| one : bool  foo
| two : fin n  fin m  foo

Here, @[derive fintype] adds the instance foo.fintype. The underlying finset definitionally unfolds to a list that enumerates the elements of the inductive in lexicographic order.

If the structure/inductive has a type parameter α, then the generated instance will have an argument fintype α, even if it is not used. (This is due to the implementation using instance_derive_handler.)