subtypes and `(a : α)`

Stream: lean4

[David Renshaw]

In Lean 3 we have:

def extract_val {α : Type} (p : α → Prop) (a : {x // p x}) := (a : α)
#print extract_val

-- 115:1: def extract_val : Π {α : Type} (p : α → Prop), {x // p x} → α :=
--  λ {α : Type} (p : α → Prop) (a : {x // p x}), ↑a

i.e. (a : α) expands to ↑a, which further elaborates to some coe stuff.

In Lean 4 we instead have:

def extract_val {α : Type} (p : α → Prop) (a : {x // p x}) := (a : α)
#print extract_val

-- def extract_val : {α : Type} → (p : α → Prop) → (Subtype fun (x : α) => p x) → α :=
--  fun {α : Type} (p : α → Prop) (a : Subtype fun (x : α) => p x) => a.val

i.e. (a : α) expands directly to a.val, with no apparent intermediate steps.

My question is: where is the logic governing that expansion in the Lean 4 version? Is it still going through coe somehow, but getting normalized before I can print it? Or is there some other magic somewhere?

[Mario Carneiro]

It uses coe like lean 3, but the definition of the coercion is used directly rather than using the generic arrow

[Gabriel Ebner]

David Renshaw said:

My question is: where is the logic governing that expansion in the Lean 4 version?

As Mario said, you still declare the coercions by adding instances for the Coe type class. The expansion is done here:
https://github.com/leanprover/lean4/blob/479edbe2359b549c59b7d3de6e61a7f576e0df00/src/Lean/Elab/BuiltinNotation.lean#L243-L249
https://github.com/leanprover/lean4/blob/d0996fb9450dc37230adea9d10ecfdf10330ef67/src/Lean/Meta/Coe.lean#L24-L40

[David Renshaw]

It uses coe like lean 3, but the definition of the coercion is used directly rather than using the generic arrow

The uparrow is notation for coe:
https://github.com/leanprover/lean4/blob/32bea737089f5153cef65e480601e2e610973222/src/Init/Coe.lean#L62

So I'm a bit confused about what would be different about using one or the other.

[David Renshaw]

https://github.com/leanprover/lean4/blob/d0996fb9450dc37230adea9d10ecfdf10330ef67/src/Lean/Meta/Coe.lean#L24-L40

This appears to validate my hypothesis that the main difference between Lean 3 and Lean 4 here is that Lean 4 is doing more normalization sooner.

[Gabriel Ebner]

David Renshaw said:

It uses coe like lean 3, but the definition of the coercion is used directly rather than using the generic arrow

The uparrow is notation for coe:
https://github.com/leanprover/lean4/blob/32bea737089f5153cef65e480601e2e610973222/src/Init/Coe.lean#L62

I'd avoid the uparrow completely since it produces a different expression than the type annotation. We should probably change it to a custom elaborator so that it does the same thing as the regular coercion.

[Gabriel Ebner]

Is it still going through coe somehow, but getting normalized before I can print it?

Missed this one, you're almost right except for the time point. The normalization happens during elaboration.

[Mario Carneiro]

Should we reverse the transformation in delab / pretty printing? I see arguments both ways

[Gabriel Ebner]

I think a pp.coe option would be good for common stuff (like Int.ofNat, etc.). But we can add this very easily in mathlib.

[Mario Carneiro]

As in, we have one pp.coe option that turns on all uses of the arrow instead of coe-unfoldings, or we have an attribute that selects particular coercions that are affected by pp.coe and others are always expanded?

[Gabriel Ebner]

One pp.coe option that prints the arrow instead of the specific functions.

[Gabriel Ebner]

(Or even nothing.)

[Mario Carneiro]

I would go for using the arrow by default (not nothing and not the expansion), and the others can be pp options

[Mac]

Mario Carneiro said:

Should we reverse the transformation in delab / pretty printing? I see arguments both ways

I'm curious: how would one reverse the coe? Isn't the information that a function application came from a coe lost during elaboration?

[Mario Carneiro]

I believe you can attach the delab to whatever expression is used in the coe, unless it is too basic (i.e. an identity function or a lambda or other built in syntax)

[Mario Carneiro]

I think we will need to have a best practice around using only coes of the form func x or things only marginally more complicated than that, so that there is a definition to attach the delab to