subtyping

Stream: general

[Bernd Losert]

Say I have the following setup:

struct point : Type
struct color_point extends point: Type
f : point -> nat
p : color_point

Now I want to do f p, but this doesn't work because the types don't match and subtyping is not a thing a lean. What do you do in this case? Do I have to make a point from p? What's the idiomatic way to do this?

[Kevin Buzzard]

You could make a coercion from color_point to point, or you can use p.point.

[Bernd Losert]

I tried coe p, but that didn't work. I just tried p.point and it gives me:

invalid field notation, 'point' is not a valid "field" because environment does not contain 'color_point.point'

[Eric Wieser]

Can you turn your example above into code that actually compiles? Is this lean3 or lean4?

[Bernd Losert]

It's lean 3.

[Eric Wieser]

Probably you want p.to_point

[Bernd Losert]

Here's the code:

structure point (α : Type*) :=
mk :: (x : α) (y : α)

inductive color
| red | green | blue

structure color_point (α : Type*) extends point α :=
mk :: (c : color)

def p : color_point nat := { x := 0, y := 1, c := color.red }
def foo (p : point nat) : nat := p.x
#check foo (p.point)

[Bernd Losert]

Ah, to_point works nicely. Thank you.

[Eric Wieser]

If you don't like .to_point as the name, you can change it with:

structure color_point (α : Type*) extends to_not_colored_point : point α :=

[Eric Wieser]

(I think)

[Bernd Losert]

That works to. Cool.

[Eric Wieser]

A good trick here is #print prefix color_point, which shows you all the generated names that structure gave you

[Eric Wieser]

Which would have told you to use to_point

[Bernd Losert]

Aha. I didn't know about prefix. Good to know.

[Bernd Losert]

Wow, that's a lot generated functions.

[Bernd Losert]

If you a group g and you want to get at the semigroup, is it just g.to_semigroup or do you have to use to_monoid first?

[Kevin Buzzard]

Here's how the coercion would work:

instance (α) : has_coe (color_point α) (point α) := ⟨color_point.to_point⟩
#check foo p -- foo ↑p : ℕ

The up-arrow is notation for has_coe.coe, which in this case is color_point.to_point. You could also write instance (α) : has_coe (color_point α) (point α) := { coe := color_point.to_point } -- it's the same thing.

[Kevin Buzzard]

Re the group question: are you rolling your own groups, are you bundling the type into the group etc etc? Can you post code? I'm not clear what g is. In Lean we do (G : Type) [group G] and then type class inference knows G has a semigroup structure.

[Bernd Losert]

Bernd Losert said:

If you a group g and you want to get at the semigroup, is it just g.to_semigroup or do you have to use to_monoid first?

Looks like g.to_semigroup works.

[Bernd Losert]

At least, that's what I infer after extending the color_point struct one-level higher.

[Bernd Losert]

Didn't realize there was a has_coe class. Good to know.

[Kevin Buzzard]

In mathlib, groups are not done in the same way as color_points. They are classes, and the questions you're asking are handled by type class inference. I still don't know what g is but if it's the group structure on the type as opposed to the type itself then in Lean it would be called _inst_1 (an auto-generated name) and humans would not have to worry about your question at all.

[Bernd Losert]

But classes are just structs with a class attribute, so I think the same mechanism will work for classes.

[Kevin Buzzard]

Yes but humans don't name instances of classes so you can't write g.to_semigroup. Can you post some code?

[Kevin Buzzard]

import tactic

example (G : Type) [group G] (a b c : G) : (a * b) * c = a * (b * c) := semigroup.mul_assoc a b c

It happened by itself, no g.to_semigroup.

[Bernd Losert]

You can if you're making a function where instead of [group a], you write (g : group a). I just used groups as an example. My actual working code involves convergence systems.

[Kevin Buzzard]

Oh sure you can override the system, I have no idea what contortions you'd have to go through then. Did you know that fields are additive monoids? I use this, but I have no idea how many .to_?s I need to add to prove it.

[Kevin Buzzard]

Whyever would you want to override the type class system though?

[Kevin Buzzard]

import tactic

def foo (G : Type) [group G] (a b c : G) : (a * b) * c = a * (b * c) := semigroup.mul_assoc a b c

set_option pp.all true
#print foo
/-
def foo : ∀ (G : Type) [_inst_1 : group.{0} G] (a b c : G),
  @eq.{1} G
    (@has_mul.mul.{0} G
       (@has_mul.mk.{0} G
          (@semigroup.mul.{0} G
             (@monoid.to_semigroup.{0} G (@div_inv_monoid.to_monoid.{0} G (@group.to_div_inv_monoid.{0} G _inst_1)))))
       (@has_mul.mul.{0} G
          (@has_mul.mk.{0} G
             (@semigroup.mul.{0} G
                (@monoid.to_semigroup.{0} G
                   (@div_inv_monoid.to_monoid.{0} G (@group.to_div_inv_monoid.{0} G _inst_1)))))
          a
          b)
       c)
    (@has_mul.mul.{0} G
       (@mul_one_class.to_has_mul.{0} G
          (@monoid.to_mul_one_class.{0} G (@div_inv_monoid.to_monoid.{0} G (@group.to_div_inv_monoid.{0} G _inst_1))))
       a
       (@has_mul.mul.{0} G
          (@mul_one_class.to_has_mul.{0} G
             (@monoid.to_mul_one_class.{0} G
                (@div_inv_monoid.to_monoid.{0} G (@group.to_div_inv_monoid.{0} G _inst_1))))
          b
          c)) :=
λ (G : Type) [_inst_1 : group.{0} G] (a b c : G),
  @semigroup.mul_assoc.{0} G
    (@monoid.to_semigroup.{0} G (@div_inv_monoid.to_monoid.{0} G (@group.to_div_inv_monoid.{0} G _inst_1)))
    a
    b
    c
-/

Looks like under the hood it goes group.to_div_inv_monoid, div_inv_monoid.to_monoid, monoid.to_semigroup.

[Bernd Losert]

It's not about overriding, but about defining functions that don't use instance arguments but regular arguments. For example, https://leanprover-community.github.io/mathlib_docs/topology/order.html#topological_space.induced

[Kyle Miller]

Bernd Losert said:

But classes are just structs with a class attribute, so I think the same mechanism will work for classes.

They also have instances for all the things they extend, making it convenient to use lemmas about, say, a semigroup, when what you have is a group.

[Bernd Losert]

Yes. That's true. In my case though, I'm making functions that basically producing values to use as instances, just like the topological_space.inducedfunction I linked above.

[Kyle Miller]

The tradeoff between classes and structures is that [group a] should mean a has a single group structure ever, but you get to more conveniently use lemmas due to typeclass search, and (g : group a) means you can use multiple group structures on the same type and more easily compare them, but then having a hierarchy of types of structures is more inconvenient.

Topological spaces have the annoying property that most of the time a class is good, but sometimes you do want to deal with multiple topologies on the same type (there's a lattice of topologies after all), which can get difficult to manipulate.

[Kevin Buzzard]

The reason that induced is a def and not an instance is that type class inference will never be able to find the f so it were an instance it would never fire.

[Bernd Losert]

Since convergence spaces are like topological spaces, I'm going to run into all the sames issues I guess.

[Bernd Losert]

I'm going to basically copy/paste the topology code in mathlib, but using convergence spaces.