Creating a class that collects other classes

Stream: new members

[Tej Chajed]

I have a class that groups a bunch of instances. Is there a convenient way to make each field an instance? Here's what the code looks like:

class schema :=
  (T R : Type).

class schema_ok (S: schema) :=
  (inst_1 : decidable_eq S.T)
  (inst_2 : decidable_eq S.R).

instance (S: schema) [schema_ok S] : decidable_eq S.T := schema_ok.inst_1.
instance (S: schema) [schema_ok S] : decidable_eq S.R := schema_ok.inst_2.

I want to automate the instances at the bottom (my actual use case has a much bigger schema and schema_ok).

[Anne Baanen]

Instead of definining new decidable_eq instances copying the fields, you can write attribute [instance] schema_ok.inst_1 schema_ok.inst_2.

[Anne Baanen]

In different circumstances you can also use the extends keyword, e.g. for monoid we define

class monoid (M : Type u)
  extends semigroup M, mul_one_class M :=
(npow : ℕ → M → M := npow_rec)
(npow_zero' : ∀ x, npow 0 x = 1 . try_refl_tac)
(npow_succ' : ∀ (n : ℕ) x, npow n.succ x = x * npow n x . try_refl_tac)

This will automatically generate instances monoid.to_semigroup and monoid.to_mul_one_class.

Unfortunately in your case, decidable_eq T := ∀ x y, decidable (x = y) is not a structure so you can't extend it, and I don't think you can extend the same structure twice either, because the field names would overlap.

[Anne Baanen]

There's also the option of unbundling: turn the decidable_eq fields into parameters

class schema_ok (S: schema) [decidable_eq S.T] [decidable_eq S.R]

This means we don't need the schema_ok.to_decidable_eq instances at all, but it does cause type signatures to become much longer so it's generally a good idea to keep them bundled as you originally had.

[Eric Wieser]

attribute [instance] schema_ok._inst_1 schema_ok._inst_2 would work in place of the last two lines in the top post