How to get implicitly defined instances

Stream: new members

[Praneeth Kolichala]

I'm completely new to Lean and formalization, and I was thinking of formalizing some easy results in complexity theory, involving space complexity. I've looked at the existing Turing machine libraries in mathlib, and I wanted to make a "bounded stack" type, which is a list that can only have less than $M$ elements. I especially want it to be a fintype so that I can use the existing cardinality methods, and e.g. show that there are $2^{O(M)}$ possible configurations for a TM whose stacks are limited by a memory bound $M$.

I tried the following:

-- The set of all possible memory configurations
def all_bounded_stacks_set :
  finset (Π k : K, Σ n : fin M, vector (Γ k) n) := finset.univ

Here, $K$ is a set which indexes the stacks, and $\Gamma : K \rightarrow \text{Type}$ is a function which gives the type of each stack (this is the modeled after the original turing_machine.lean file). Unfortunately, this didn't work. For context, the section parameters go like:

section
parameters {K : Type*} [K_eq : decidable_eq K] [K_fin : fintype K]
parameters (Γ : K → Type*) (Γ_fin : ∀k : K, fintype (Γ k)) -- Type of stack elements
parameters (Λ : Type*) (Λ_fin : fintype Λ) -- Type of function labels
parameters (σ : Type*) (σ_fin : fintype σ) -- Type of variable settings


section bounded_space
-- The global bound
parameter (M : ℕ)

...

I eventually realized that the issue was that my assumptions like K_eq and Γ_fin were not being used by Lean's inference engine, so I solved it by doing

def all_bounded_stacks_set :
  finset (Π k : K, Σ n : fin M, vector (Γ k) n) :=
  let __ := Γ_fin,
      ___ := K_eq,
      ____ := K_fin
  in finset.univ

Is there a better way? What I'd really like to do is not have to rely on the inference as much, because I can never tell what I'm actually missing for Lean to understand, and it's just really frustrating. For example, if I replace the above with

def all_bounded_stacks := (Π k : K, Σ n : fin M, vector (Γ k) n)

def all_bounded_stacks_set :
  finset all_bounded_stacks :=
  let __ := Γ_fin,
      ___ := K_eq,
      ____ := K_fin
  in finset.univ

it fails, maybe because it is too deep.

So if I want to use finset.univ explicitly, @finset.univ requires the type T and a proof of finiteness, fintype T. But I don't know how to "retrieve" the implied instance from mathlib. In order to get all_bounded_stacks_fintype I had to make everything explicit:

-- A single bounded stack
def bounded_stack (k : K) := (Σ n : fin M, vector (Γ k) n)

-- A single bounded stack has only finitely many possibilities
def bounded_stack_fintype (k : K) : fintype (bounded_stack k) :=
  (@sigma.fintype (fin M) (λ (n : fin M), vector (Γ k) ↑n) (fin.fintype M)
     (λ (a : fin M), @vector.fintype (Γ k) (Γ_fin k) ↑a))

-- All K bounded stacks
def all_bounded_stacks := (Π k : K, bounded_stack k)

def all_bounded_stacks_fintype :
  fintype all_bounded_stacks :=
   @pi.fintype K bounded_stack K_eq K_fin bounded_stack_fintype

There must be a better way to get the fintype. Moreover, some of the instance types (e.g. product) don't have a name, so I don't know how to get them. For example, I don't know how to make this work at all, not even by explicitly writing everything out:

def bounded_cfg := (option Λ) × σ × all_bounded_stacks

def bounded_cfg_set : (finset bounded_cfg) :=
  let __ := all_bounded_stacks_fintype,
      ___ := Λ_fin,
      ____ := σ_fin
  in finset.univ -- This fails

Any suggestions?

[Martin Dvořák]

This looks extremely interesting and ambitious! Imma read your post and comment on it later.

[Yakov Pechersky]

Is this close to what you were aiming for?

import computability.turing_machine

variables {K : Type*} [decidable_eq K] [fintype K]
variables (Γ : K → Type*) [Π k, fintype (Γ k)] -- Type of stack elements
variables (Λ : Type*) [fintype Λ] -- Type of function labels
variables (σ : Type*) [fintype σ] -- Type of variable settings
variables (M : ℕ) -- max stack size

def bounded_stacks : Type* := Π k : K, Σ n : fin M, vector (Γ k) n

instance {k : K} : fintype (bounded_stacks Γ M) := pi.fintype

[Eric Wieser]

Inference fails in your example because named typeclass arguments are not included by default

[Eric Wieser]

Meanwhile, you forgot to put Γ_fin in square brackets.

[Martin Dvořák]

@Praneeth Kolichala
If the suggested "patch" works, will you please upload the whole code with all imports etc so that I can play with it?