auto-coercions

Stream: Is there code for X?

[Kyle Miller]

What's the mechanism in Lean that inserts automatic coercions for functions? Here's an example:

example {α β : Type} (f : α ↪ β) : function.injective f := ...

Lean inserts a coercion arrow, so it's actually function.injective ⇑f.

(Is this something can be enabled for other types? I'd imagine you give a type and a coercion function, and then when you pass an argument to a function that doesn't have the expected type, the expected type's coercion function is inserted.)

[Floris van Doorn]

There is a minimal amount of documentation of this feature in this file: https://github.com/leanprover-community/lean/blob/master/library/init/coe.lean

[Kyle Miller]

An example application: if a structure B extends another structure A, you cannot pass something of type B to a function expecting something of type A, but it would be convenient if Lean automatically inserted the B.to_A function.

[Floris van Doorn]

Also https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes

[Floris van Doorn]

I think in Lean 2 a coercion from an extended structure to the original structure was automatically generated.
In Lean 3 / mathlib almost all extending of structures actually happens on classes, so that feature is not very applicable.

[Floris van Doorn]

The basic usage is that if you define

instance : has_coe B A := ...

then a coercion from B to A is automatically inserted.

[Floris van Doorn]

Also look at the variants docs#has_coe_to_fun and docs#has_coe_to_sort

[Kyle Miller]

What's nice about has_coe_to_fun is that the coercion is able to direct the type it gets coerced to, but has_coe cannot, so it sometimes needs some help with explicit type annotations.

I've noticed that classes are used to do this sort of polymorphism, but not everything can be a class because there aren't always good parameters to attach them to.

[Kyle Miller]

I was imagining, in certain cases, being able to define your own has_coe_to_fun-like thing where the thing being coerced can specify some of the type variables in the coercion.

[Kyle Miller]

Should I take it that somewhere deep in the elaborator, Lean 3 knows about has_coe_to_fun and will automatically insert coercions?

[Floris van Doorn]

Yeah, has_coe, has_coe_to_fun and has_coe_to_sort are hard-coded somewhere in the elaborator in C++.

[Kyle Miller]

Assuming for a moment it makes sense to have structures with no parameters, is there any way to get this coercion to work? The class resolution trace says "failed is_def_eq", which I think is because it's not able to solve for the universe variables -- there's no way to tell has_coe that has_coe (B a) A.{v} does not exist for v not equal to u.

universes u

structure A :=
(X : Type u)

structure B (a : A) :=
(X' : set a.X)

def B.to_A {a : A} (b : B a) : A :=
{ X := subtype b.X' }

instance B_to_A' (a : A) : has_coe (B a) A :=
{ coe := B.to_A }

-- "A.X b" is not ok, since cannot coerce b to be of type A
example (a : A) (b : B a) : ∀ (x : A.X b), x = x := sorry

-- OK
example (a : A) (b : B a) : ∀ (x : A.X b.to_A), x = x := sorry

-- OK
example (a : A.{u}) (b : B a) : ∀ (x : A.X.{u} b), x = x := sorry

[Kyle Miller]

This would work:

universes u v

structure A :=
(X : Type u)

structure B (a : A) :=
(X' : set a.X)

def B.to_A {a : A} (b : B a) : A :=
{ X := subtype b.X' }

class has_coe_to_A (β : Type u) :=
(coe : β → A.{v})

notation `⇧`:max x:max := has_coe_to_A.coe x

instance (a : A) : has_coe_to_A (B a) :=
{ coe := B.to_A }

example (a : A) (b : B a) : ∀ (x : A.X ⇧b), x = x := sorry

It'd be nice if the ⇧ could be automatically inserted.

[Reid Barton]

I haven't looked at your example closely, but I thought that Lean no longer hesitates to use an instance even if it would mean assigning a universe level metavariable.

[Kyle Miller]

With the first setup, here's a pair where the only difference is whether both universes are explicitly given:

example (a : A.{u}) (b : B a) : ∀ (x : A.X b), x = x := sorry  -- not OK
example (a : A.{u}) (b : B a) : ∀ (x : A.X.{u} b), x = x := sorry -- OK

[Reid Barton]

Did I imagine that? It does quite look like that is what is going wrong

[Reid Barton]

I guess I was thinking of https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.233221.20remove.20universe.20annotations.20in.20category_theory/near/202266781 but it seems that nobody really knows what happened there.

[Kyle Miller]

That's amusing no one really knows what happened -- I guess I should take closer look at the category theory library to see what it's doing that might help class resolution out. Do you think that this B_to_A coercion should work in principle?

[Kyle Miller]

Thanks @Floris van Doorn and @Reid Barton for your comments and for helping me understand auto-coercions better. I didn't realize that has_coe.coe was automatically inserted, probably because in my application (the simple graphs API) it didn't obviously work so I didn't think to inspect the class resolution trace.

Would it be possible or reasonable to make it so that class resolution will use an instance to solve for universe metavariables in the special case that they are unconstrained by the type variables? The underlying assumption is that no one would ever define any other instances, so, using the language of logic programming, it's seems safe to take a closed-world assumption here.

The #mwe from above is supposed to represent a structure that is not naturally a class (i.e., mathematical objects that are not referred to by synecdoche) that has a notion of sub-object -- and from the perspective of objects that are referred to by synecdoche (i.e., pretty much algebraic object in mathlib), it's a bundled structure. Everything I've been going on about with the synecdoche problem this summer seems like it would be resolved if this has_coe instance would work.

In the meantime, I've reorganized the simple_graphs2 branch, which has been a test-bed for experimenting with different approaches, to use a custom coercion class and coercion arrow that is specifically for coercion to simple graphs. This enforces that the universe is a function of the type being coerced.

The arrow is defined here. It's not so bad putting the arrow where it's needed, but it would just be a little more convenient not having to place the arrows at all.

(The way this differs from what I was doing before is that, before you'd essentially have to prove all your generic theorems with respect to types that have a has_coe_to_simple_graph instance. It was ok, but it always felt awkward, and it made some constructions more difficult than they needed to be, I think. Recently I gained some confidence that structures with unconstrained universe variables would be OK, and it does seem to work out fine for simple graphs.)

[Kyle Miller]

I didn't want to break convention with coercion arrows, but something I noticed is that if it instead were a postfix operation

postfix ` ↟ `:max_plus

then you can write stuff like G↟.adj rather than (↟G).adj

[Kyle Miller]

(It's reminiscent of how in Pascal, they used a postfix pointer dereferencing operator. Using C-like notation, you can do x*.foo rather than needing a separate x->foo.)

[Kyle Miller]

Another reason not defining it this way, beyond convention, is that using this postfix arrow along with generalized field access notation means it can't be seamlessly be replaced by has_coe, due to the fact that the field access notation needs to be able to determine the name of the type to resolve. Still, it seems like nice notational hack to consider.

[Floris van Doorn]

I think generally we want to coerce objects only to other objects of the same universe (or at least, a universe determined by the object in question). I don't know how hard it is to change the type-class mechanism to incorporate your suggestion
Why doesn't has_coe (simple_graph_on V) simple_graph, or any of your other examples, work? It looks like the universe of the target is the same (or at least determined) by the coerced object.
Also, I would encourage you to not add too many coercions. The coercions from simple_graph_on and of_edge_set' should probably just be named operations. The former is very similar to docs#category_theory.bundled whose constructor is also not a coercion.
I feel strongly that we should not have a dedicated global notation to coerce specifically to simple_graph.

[Kyle Miller]

The issue with has_coe (simple_graph_on V) simple_graph is that Lean can figure out the universe for simple_graph_on V, so then it would know how to coerce to simple_graph.{u} for V : Type u, but then class inference can't make the leap that this instance should be used, because all it knows is that it needs a simple_graph.{v} for some v. I assume it's because someone might later introduce an instance like has_coe (simple_graph_on V) simple_graph.{u+1}, even though we know this is highly unlikely.

I agree I don't need of_edge_set' to have a coercion -- it's only there to show that two ways of defining subgraphs are equivalent and it should only be a local instance -- but it's useful having simple_graph_on being coerceable. There are many cases where you'd like ready access to the vertex type for rewriting, so it's worth making things like path_graph be a simple_graph_on rather than a simple_graph when possible -- and ideally you wouldn't need to pervasively clutter code with casts to the simple_graph type. One place it's useful is in working with walks in a graph as homomorphisms ↟(path_graph length) →g G, where the vertex type is fin (length + 1). In any case, there are only really two types right now where it's convenient to have a coercion to simple_graph: simple_graph_on and subgraph. There probably wouldn't ever be many more than this.

I also agree that there shouldn't be a dedicated global notation for coercing to simple graphs. I'm hoping has_coe will work and then it can be removed entirely. But if not, then I can revert to the method I was previously using without too many changes, or I can just give the tree arrow as local notation. (An audacious proposal is for this to be a special coercion notation that is overloaded for specific coercion destinations. Like how :: is overloaded.)