Nested Type Classes

Stream: new members

[Henning Dieterichs]

I have this structure:

class Foo :=
  (Bar : Type)
  [bar_dec: decidable_eq Bar]

variable [Foo]
open Foo

def x (b1: Bar) (b2: Bar) :=
  if b1 = b2 then 0 else 1

It complains that b1 = b2 is not decidable, even though bar_dec should be in scope. How can I fix this?

This works, but I would prefer to put the decidable_eq type class into Foo, so that open Foo is enough to have decidable_eq for Bar:

class Foo :=
  (Bar : Type)

variable [Foo]
open Foo

variable [decidable_eq Bar]

def x (b1: Bar) (b2: Bar) :=
  if b1 = b2 then 0 else 1

[Eric Wieser]

Does attribute [instance] Foo.bar_dec work?

[Henning Dieterichs]

Thanks, it does work!

[Yury G. Kudryashov]

[bar_dec: decidable_eq Bar] in the definition of class Foo means that Lean will try to find [decidable_eq Bar] when you define an instance of Foo. If you want Lean to use this projection when it is looking for [decidable_eq Bar], you need to write attribute [instance] Foo.bar_dec.

[Henning Dieterichs]

What is the difference between a global [bar_dec: decidable_eq Bar] and [decidable_eq Bar]? The later one is automatically discovered by lean, the first one not

[Reid Barton]

By "global" I assume you mean variable

[Henning Dieterichs]

Oh right

[Reid Barton]

If Lean decides to include a variable in a def/lemma, then it will also automatically include any unnamed [] variables that mention it

[Henning Dieterichs]

and attribute [instance] Foo.bar_dec enables this for a named [] variable?

[Reid Barton]

no, this is completely unrelated

[Reid Barton]

it just makes Foo.bar_dec into a (global) instance

[Reid Barton]

Your example is minimized to the point of being confusing--normally we wouldn't have a class with zero arguments

[Reid Barton]

I'm not sure whether variable [Foo] does anything really

[Reid Barton]

but in any case, we wouldn't write it in the real world

[Henning Dieterichs]

I was recommended to use a class to declare a bunch of variables (i.e. fields) so I don't need to redeclare them for every file. open Foo would be sufficient.

[Reid Barton]

That's sort of tempting but it would result in an awkward API unless you restate everything at the end in a more normal style

[Henning Dieterichs]

I don't think anyone will use my theorems, so I think that is fine :D It's about (abstract) program verification.

[Reid Barton]

If you never plan to actually construct any instances of Foo then it might be okay. I would recommend using something like variables [foo : Foo] include foo then.

[Henning Dieterichs]

you mean as an alternative to

variable [Foo]
open Foo

?

[Henning Dieterichs]

hmm, I still need to do the open with variables [foo : Foo] include foo.
If include is including that in every definition, shouldn't be variable [Foo] be equivalent to variable [foo: Foo] include foo?

[Reid Barton]

Why?

[Reid Barton]

Maybe variable [Foo] has a special case for 0-argument classes?

[Reid Barton]

open has nothing to do with this, it's just for namespacing

[Reid Barton]

If variable [Foo] already forces the instance to be included everywhere then you don't need my suggestion.

[Henning Dieterichs]

If variable [Foo] already forces the instance to be included everywhere then you don't need my suggestion.

Seem like variable [Foo] forces the instance to be included everywhere! That's what confused me since it didn't happen for variable [foo: Foo].

[Reid Barton]

Oh I guess the rule must be "include a [] variable if all the variables it mentions are included", so that makes sense.