how to prove fintype of enumeration

Stream: general

[Thorsten Altenkirch]

Is there a tactic to prove:

[Thorsten Altenkirch]

inductive Sigma1 : Type
| a b c : Sigma1

def isFin1 : fintype Sigma1 := sorry

[Johan Commelin]

I assume you want it to be computable?

[Kevin Buzzard]

Just to be clear, you really want this to be some recursive type?

#check Sigma1.a -- Sigma1.a : Sigma1 → Sigma1 → Sigma1

I suspect Sigma1 is empty.

[Kevin Buzzard]

def foo : Sigma1 → false
| ⟨b, c⟩ := foo b

[Kevin Buzzard]

In case this is what you meant:

import tactic

@[derive fintype]
inductive Sigma1 : Type
| a : Sigma1
| b : Sigma1
| c : Sigma1

def isFin1 : fintype Sigma1 := infer_instance

[Thorsten Altenkirch]

I thought I changed this on zulip, sorry.

[Thorsten Altenkirch]

Ok, thank you!

[Thorsten Altenkirch]

Btw, I am defining :

• an alphabet Sigma is a finite type
• a word over Sigma is a list over Sigma
• a language is a set of words, i.e. word Sigma -> Prop
  what is the best way to do this?

section basics
variable Sigma : Type

-- the empty work ε
@[reducible]
def word : Type := list Sigma

def epsilon : word Sigma := []

@[reducible]
def lang : Type := word Sigma → Prop

end basics

But I never mention that Sigma has to be finite?

[Thorsten Altenkirch]

I guess I could define Alphabet as a record of a type with fintype?