adding type classes to structures

Stream: general

[Thorsten Altenkirch]

What is the best way to add a type class to a structure? E.g. we define

structure dfa(Sigma : Type)  : Type 1 :=
  (Q : Type)
  (init : Q)
  (final : Q → Prop)
  (δ : Q → Sigma → Q)

but we want to say that Q is finite and δ is decidable.

[Yaël Dillies]

structure dfa (Sigma : Type*)  : Type* :=
(Q : Type*)
[fintype Q]
(init : Q)
(final : Q → Prop)
(δ : Q → Sigma → Q)

is one option. I'm not sure what you mean by "δ is decidable". Maybe you mean decidable_eq Q?

[Thorsten Altenkirch]

Thank you. I meant to say that final is decidable.

[Yaël Dillies]

Ah then

structure dfa (Sigma : Type*)  : Type* :=
(Q : Type*)
[fintype Q]
(init : Q)
(final : Q → Prop)
[decidable_pred final]
(δ : Q → Sigma → Q)

[Eric Wieser]

You also want to follow on with attribute [instance] dfa._inst_1 dfa._inst_2

[Eric Wieser]

Which is to say, don't leave them nameless like @Yaël Dillies did!

[Thorsten Altenkirch]

Eric Wieser said:

Which is to say, don't leave them nameless like Yaël Dillies did!

exactly how does this work?

[Kevin Buzzard]

They're just saying "if you write [hf : fintype Q] then you can write attribute [instance] hf

[Thorsten Altenkirch]

[fintype Q} does not imply [decidable_eq Q], right?

[Johan Commelin]

That's right. It's a bug or a feature, depending on whom you talk to.

[Thorsten Altenkirch]

I guess I feel tempted to introduce a type class: dec_fintype. At least that is what I need for automata theory.