Zulip Chat Archive

Stream: new members

Topic: Nested Type Classes


view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:04):

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

view this post on Zulip Eric Wieser (Dec 08 2020 at 19:14):

Does attribute [instance] Foo.bar_dec work?

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:15):

Thanks, it does work!

view this post on Zulip Yury G. Kudryashov (Dec 08 2020 at 19:18):

[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.

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:21):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:38):

By "global" I assume you mean variable

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:39):

Oh right

view this post on Zulip Reid Barton (Dec 08 2020 at 19:39):

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

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:40):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:40):

no, this is completely unrelated

view this post on Zulip Reid Barton (Dec 08 2020 at 19:40):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:41):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:42):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:42):

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

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:42):

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.

view this post on Zulip Reid Barton (Dec 08 2020 at 19:44):

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

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:46):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:47):

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.

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:51):

you mean as an alternative to

variable [Foo]
open Foo

?

view this post on Zulip Henning Dieterichs (Dec 08 2020 at 19:53):

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?

view this post on Zulip Reid Barton (Dec 08 2020 at 19:55):

Why?

view this post on Zulip Reid Barton (Dec 08 2020 at 19:56):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:56):

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

view this post on Zulip Reid Barton (Dec 08 2020 at 19:56):

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

view this post on Zulip Henning Dieterichs (Dec 09 2020 at 10:24):

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].

view this post on Zulip Reid Barton (Dec 09 2020 at 10:27):

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


Last updated: May 15 2021 at 02:11 UTC