How to define a coercion

Stream: general

[Miguel Marco]

I am trying to write some API for working with subsets of subtypes, and I found the following error: when I tried to define a coercion from the sets of a subtype to sets of the initial type, like this:

variable {X : Type} {A : Set X}

def SubSet.Coe : Set A → Set X := fun U => { (x.val) | x ∈ U}

instance : Coe (Set A) (Set X) where
  coe := SubSet.Coe

I get this error:

instance does not provide concrete values for (semi-)out-params
  Coe (Set ↑?A) (Set X)

what does that mean? What would be the right way to do it?

Also, is there a particular reason why this has not been done already in mathlib?

[Yaël Dillies]

We just use Set.image (\u) s

[Miguel Marco]

Yes, but my question is about how to make it a coercion, in such a way that we can "automatically" convert sets of ↑Ato sets of X.

[Miguel Marco]

Sorry, I had put the error message twice instead of the code that causes it. Edited now.

[Yaël Dillies]

Have you tried using CoeT instead of Coe?

[Miguel Marco]

If I Try

instance (X : Type) (A : Set X) : CoeT (Set A) (Set X) where
  coe :=  fun U => { (x.val ) | x ∈ U}

lean seems to enter in an infinite loop: it stays forever with a high CPU usage. maybe i introduced a cycle in the coercion graph?

[Mac Malone]

@Miguel Marco Your initial example confuses me, particularly the term Set A. The mathlib Set has type Type u -> Type u and A in your example has type Set X which is not a Type u, so Set A is not well-typed. What are you trying to do here?

[Mac Malone]

Oh, I guess this is my inexperience with mathlib talking. The set is being coerced into a type.

[Miguel Marco]

Mac Malone said:

Oh, I guess this is my inexperience with mathlib talking. The set is being coerced into a type.

Exactly. What I want is to "extend" this coercion to sets.

[Mac Malone]

@Miguel Marco Okay, thanks for the explanation! The problem here is that during synthetization of a Coe instance, Lean is tries to solve for the LHS using information from the RHS. In the instance Coe (Set A) (Set X). the RHS Set X provides Lean no information on what A should be. Thus, Lean errors when you tried to provide it such an instance. What you would like to do is flip this so that Coe (Set A) (Set X) uses the information from the LHS Set A where A : Set X to help Lean determine the X in the RHS. To do this you can use CoeOut like so:

instance {A : Set X} : CoeOut (Set A) (Set X) where
  coe := SubSet.Coe

With CoeOut, unlike Coe, Lean tries to solve for the RHS using information from the LHS during synthetization.

[Miguel Marco]

I see, thanks. It works.

My problem now is that, in the InfoView, I don't get the nice notation ↑U but Lean.Internal.coeM U. Is there a way to fix it?

[Miguel Marco]

I claimed victory too early. There seems to be a coercion already defined, called Lean.Internal.coeM , but I am not sure it is what I want. And it seems to be conflicting with ↑Unotation.

[Anatole Dedecker]

This was discussed a few times before. We used to have no such coercion, but in Lean4 this coercion comes "for free" from the fact that Set is a monad. The problems are that (1) the underlying definition is not convenient (2) it’s not nicely pretty printed and (3) it’s clearly marked as an internal definition (necessary for coercions in do notation) that shouldn’t be invoked explicitly. I think we should decide either to disable it outside of do notation (if that’s even possible) or ask for it to be renamed if we’re willing to use it in Mathlib

[Miguel Marco]

Anatole Dedecker said:

This was discussed a few times before. We used to have no such coercion, but in Lean4 this coercion comes "for free" from the fact that Set is a monad. The problems are that (1) the underlying definition is not convenient (2) it’s not nicely pretty printed and (3) it’s clearly marked as an internal definition (necessary for coercions in do notation) that shouldn’t be invoked explicitly. I think we should decide either to disable it outside of do notation (if that’s even possible) or ask for it to be renamed if we’re willing to use it in Mathlib

Is there a way to override it?

[Yaël Dillies]

I'm hitting this problem as well in LeanCamCombi. Is there any way to disable Lean.Internal.coeM locally?

[Alex J. Best]

Why do you want to disable it, it should be possible to unfold it (with simp) and prove things about it.
You could try attribute [-coe_decl] Lean.Internal.coeM or whatever the syntax to remove attributes is (untested)

[Alex J. Best]

Ok turns out it can't be erased, #mwe ?