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:
- A list
lof elements - A proof that
lhas no duplicates - 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:
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:
mk_sigmaconstructs the typeΓinfinset_in.mkmk_sigma_elimconstructs the functionfinfinset_in.mkmk_sigma_elim_injproves thatfis injectivemk_sigma_elim_eqproves that∀ a, enum (f a) = kmk_finsetconstructs the finsetS = {foo.zero} ∪ ...by recursion on the variantsmk_finset_totalconstructs the proof|- foo.zero ∈ S; |- foo.one a ∈ S; |- foo.two a b ∈ Sby recursion on the subgoals coming out of the initialcasesmk_fintype_instanceputs it all together to produce a proof offintype foo. The construction offoo.enumis also done in this function.
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
- derive_fintype.finset_above α enum n = {s // ∀ (x : α), x ∈ s → n ≤ enum x}
Construct a fintype instance from a completed finset_above.
This is the case for a simple variant (no arguments) in an inductive type.
Equations
- derive_fintype.finset_above.cons n a h s = ⟨finset.cons a s.val _, _⟩
The base case is when we run out of variants; we just put an empty finset at the end.
Equations
Equations
- derive_fintype.inhabited α enum n = {default := derive_fintype.finset_above.nil n}
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
- derive_fintype.finset_in P = {s // ∀ (x : α), x ∈ s → P x}
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
- derive_fintype.finset_in.mk Γ f inj mem = ⟨finset.map {to_fun := f, inj' := inj} finset.univ, _⟩
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
- derive_fintype.finset_above.union n s t = ⟨s.val.disj_union t.val _, _⟩
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.
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.)