Zulip Chat Archive

Stream: general

Topic: adding type classes to structures


Thorsten Altenkirch (Jul 18 2022 at 10:21):

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 (Jul 18 2022 at 10:25):

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 (Jul 18 2022 at 10:34):

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

Yaël Dillies (Jul 18 2022 at 10:38):

Ah then

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

Eric Wieser (Jul 18 2022 at 10:44):

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

Eric Wieser (Jul 18 2022 at 10:44):

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

Thorsten Altenkirch (Jul 22 2022 at 12:01):

Eric Wieser said:

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

exactly how does this work?

Kevin Buzzard (Jul 22 2022 at 12:46):

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

Thorsten Altenkirch (Jul 22 2022 at 12:59):

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

Johan Commelin (Jul 22 2022 at 13:03):

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

Thorsten Altenkirch (Jul 22 2022 at 13:05):

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


Last updated: Dec 20 2023 at 11:08 UTC