Zulip Chat Archive

Stream: new members

Topic: Infer typeclass from within structure


Jake Levinson (Sep 12 2021 at 05:17):

Here is a #mwe of the issue I'm running into. I have a typeclass I want to use as an inferred argument [my_class X] and a structure that bundles the data of an X : Type and a corresponding my_class X instance. But then the instance doesn't seem to be visible for automatic typeclass inference later on.

Toy example:

class my_class (X : Type) := (elem [] : X)

open my_class

def cool_map {X Y : Type} [my_class X] [my_class Y] (f : X  Y) :=
  f (elem X) = elem Y

structure cool_structure (Y : Type) [my_class Y] :=
  (X : Type)
  (α : my_class X)
  (f : X  Y)
  (h : cool_map f)

lemma some_lemma {Y : Type} [my_class Y] (C : cool_structure Y)
  (g : Y  Y) (hg : g (elem Y) = elem Y) : cool_map (g  C.f) := sorry

/-
failed to synthesize type class instance for
Y : Type,
_inst_1 : my_class Y,
C : cool_structure Y,
g : Y → Y,
hg : g (elem Y) = elem Y
⊢ my_class C.X
-/

Of course, there is a my_class C.X instance, namely C.α. If I write @cool_map _ _ C.α _ (g ∘ C.f) then it works, but this is sort of annoying (even in this toy example it takes a bunch of dashes; in my actual example I want to avoid the @ notation).

Is there a way to make this kind of structure work? Or, a better way to do this? It seems like a design question (what goes in the structure and what stays outside of it) that would come up a lot...

Mario Carneiro (Sep 12 2021 at 05:21):

Of course, there is a my_class C.X instance, namely C.α.

But that's not an instance: You never declared it as such. If you use instance : my_class C.X := C.α then it should work

Eric Wieser (Sep 12 2021 at 07:40):

Or just attribute [instance] C.α

Jake Levinson (Sep 12 2021 at 14:54):

Ah, I see. Looks like either of those lines can go right below the structure definition:

instance (Y : Type) [my_class Y] (C : cool_structure Y) : my_class C.X := C.α
or
attribute [instance] cool_structure.α

That's exactly what I needed. Thank you both!

Adam Topaz (Sep 12 2021 at 15:00):

The usual thing to do is to declare a has_coe_to_sort using your cool_structure.X and then declare a my_class C instance for C : cool_structure using C.\alpha.
Take a look e.g. at the code around src#Group

Jake Levinson (Sep 12 2021 at 16:43):

Followup question to all this (possibly related to Adam Topaz's suggestion re: coercions, I think this question is undoubtedly already answered by the choices made in defining group and ring maps, but the code in src#Group is quite abstract for me, I don't get what's going on in it).

In the toy setting above (I guess my toy example was maps of pointed sets, plus "pointed sets over a base pointed set" or something). Would it be better to have defined cool_map as a structure containing both the map and the property? So instead of

def cool_map {X Y : Type} [my_class X] [my_class Y] (map : X → Y) := map (elem X) = elem Y)

I would do

structure cool_map {X Y : Type} [my_class X] [my_class Y] :=
  (map : X  Y)
  (h : map (elem X) = elem Y)

instance {X Y : Type} [my_class X] [my_class Y] : has_coe_to_fun (cool_map X Y) :=
  { F := λ _, X  Y, coe := λ α, α.map }

Maybe I would rather use this approach since, for one thing, it makes cleaner theorem statements to have the information in a cool_map packaged together. Likewise for continuous functions or whatever other category.

But, then I am not sure the best way to declare other structures on top of it. For example, say I want to define a cool_equiv X Y that consists of an equiv X Y using cool_maps instead of arbitrary functions. In this situation I would want to be able to go either from a cool_equiv (or whatever) to a normal equiv, or to the associated cool_maps. I can say

structure cool_equiv (X Y : Type) [my_class X] [my_class Y] extends equiv X Y :=
  (cool : to_fun (elem X) = elem Y)
  (inv_cool : inv_fun (elem Y) = elem X)

variables {X Y : Type} [my_class X] [my_class Y] (φ : cool_equiv X Y)
def cool_equiv.to_cool_map : cool_map X Y := φ.to_fun, φ.cool
def cool_equiv.inv_cool_map : cool_map Y X := φ.inv_fun, φ.inv_cool

or I can instead package in the cool_maps and write the coercion to equiv X Y separately.

structure cool_equiv' (X Y : Type) [my_class X] [my_class Y] :=
  (to_cool_map : cool_map X Y)
  (inv_cool_map : cool_map Y X)
  (left_inv : function.left_inverse inv_cool_map to_cool_map)
  (right_inv : function.right_inverse inv_cool_map to_cool_map)

variables {X Y : Type} [my_class X] [my_class Y]
instance : has_coe (cool_equiv' X Y) (equiv X Y) :=
  λ φ, equiv.mk φ.to_cool_map φ.inv_cool_map φ.left_inv φ.right_inv

I'm just wondering which of these approaches is better, and/or if either would cause me pain further down the road. Or, maybe there's some other way that's better?

Adam Topaz (Sep 12 2021 at 17:13):

@Jake Levinson is there some mathematical concept you're trying to model here? Pointed types?

Yakov Pechersky (Sep 12 2021 at 17:18):

The way ring_equivs are set up are independent of ring_hom. One does not need two ring_hom to make a ring_equiv. But I think there is a helper constructor that can take two ring_homs and make a ring_equiv, with the proper constraint that they are inverses

Yakov Pechersky (Sep 12 2021 at 17:19):

So I think that implies that the structure extends equiv is the better approach.

Yakov Pechersky (Sep 12 2021 at 17:21):

You can always bake in the forward direction proof of coolness by doing

my_cool_equiv := { ..my_cool_hom, other_field := _, }

Adam Topaz (Sep 12 2021 at 17:31):

It doesn't really matter if you make the right API e.g. you can just define a cool_equiv.to_equiv function and a cool_equiv.mk' constructor

Jake Levinson (Sep 12 2021 at 23:19):

Adam Topaz said:

Jake Levinson is there some mathematical concept you're trying to model here? Pointed types?

The actual example that prompted my post isn't so different from pointed types: continuous fiber bundle maps, and in particular the "continuous" part. I had already made some working API for "maps of fiber bundles" without any continuity conditions, so I was trying to extend my various fiber-bundle-related structures to add hypotheses about all the maps being continuous. I ran into the issue sketched about above when defining a cts_bundle_equiv since I had to decide how to relate it to bundle_equiv and cts_bundle_map which I had defined previously.

(I also ran into the simpler version of this question when defining continuous functions originally, and for whatever reason chose the other way -- defining cts as a property of functions rather than as part of a cts_map structure.)

Adam Topaz (Sep 12 2021 at 23:48):

I see. Presumably you need to add docs#continuous properties for the functions you use, or perhaps use bundled continuous maps instead of functions (we have such bundled continuous maps in mathlib)

Adam Topaz (Sep 12 2021 at 23:49):

docs#continuous_map


Last updated: Dec 20 2023 at 11:08 UTC