How should I think of the arrow in ↑Subset?

Stream: new members

[Rado Kirov]

I am toying around with subsets:

def S : Set ℤ := { x : ℤ | x > 0 }
example (s : S) : ... := by ...

In the Lean Info window I see s: ↑S. Should I think of ↑S as a placeholder for ℤ or more like it's S but the arrow is a reminder that S is a sub type (so I can expect to be able to do s.property and Coe to the larger type)? Or it has some other meaning different from S proper.

Also, how does one define a subset of a subset? I got both of those to compile, but not sure which is better (if there is even any notion of better).

def SS : Set S := { x : S | x > (1 : ℤ) } -- the cast for 1 is needed
def SS': Set ℤ := { x ∈ S | x > 1 }
 ```

[Kyle Miller]

If you hover over the arrow you can see what it represents

[Kyle Miller]

For subset of a subset, probably the second is best if you don't have a reason to use the first. The first remembers it's a subset of S so to speak, but the second you'd need to do an (easy) proof that it's a subset of S.

[Rado Kirov]

If you hover over the arrow you can see what it represents

I see, S: Set α means that S is a α → Prop, while ↑S is Subtype S (which is called Elem). So one is just a structure boxed (not sure if that is even the right terminology), but basically a structure wrapper around the same stuff. So the ↑ denotes that transition.

I guess the magic was I was even allowed to write (x : S) to begin with, because S is just a specific function, what does it mean to have a specific function as a type. It is true that instance : CoeSort (Set α) (Type u) := ⟨Elem⟩ does the magic coersion right at the (x: S) declaration?

[Rado Kirov]

There is also ↥ which is subtly different? Clicking through it goes straight to Subtype without Elem?

[Rado Kirov]

I see ↑ is for subsets as a specific instance of subtypes which get ↥.

[Robert Maxton]

There are three coercion arrows:

• ↥ represents CoeSort, a coersion that allows you to take a type α that is not explicitly Sort u and use it as if it were a Sort u anyway. Only explicit types (things of type Sort u) can have values, so any time you have a 'type-like' type that has 'elements' of some kind you want a CoeSort instance to work with it.
• ⇑ represents CoeFun. Similarly to CoeSort, CoeFun allows you to take a type β that isn't an explicit function type (of type α → γ) and use it as if it were a function anyway. Things like Equiv get CoeFun instances.
• ↑ represents a 'general' coersion that doesn't fall into one of the above two categories.

[Rado Kirov]

Got it, one final q if you will indulge me (somehow I keep being draw in to internals of how lean works, instead of actually using it to prove stuff haha). This goofy example helped me grok CoeSort
making a specific natural number automatically cast to a Prop so it can be used as a sort:

def NonZero (x: ℕ): Prop := x != 0
def x := 3
instance : CoeSort ℕ Prop where
  coe x := NonZero x

example (hx : x) := by
  sorry

but how come I don't see any arrow (no ↥ or ↑) in the info view? I see the explicit coersion hx : NonZero x.

[Aaron Liu]

You have to mark NonZero as @[coe] for the arrow to show up.

[Rado Kirov]

Nice! Wait why ↑ not ↥ if I used CoeSort? What's a similarly small goofy example to show ↥?

[Kyle Miller]

The way coercions work is that the system looks for a coercion and then substitutes the definition of the coercion, so in your example rather than seeing CoeSort.coe x you see NonZero x as the result.

The @[coe] attribute is used for pretty printing (and for tactics that need to identify what is a "coercion function"). Adding @[coe] to NonZero marks it as being a coercion function, and pretty printing prints it with an up arrow. There's currently no @[coe_sort] attribute, just @[coe]. Pretty printing has no (efficient) way to tell which instances there are for which coercion class.