norm_cast not seeing coercion?

Stream: lean4

[Arien Malec]

I'm translating @Kevin Buzzard's Complex Number Game to Lean 4, and tripping over issues.

@[ext] structure Complex where
  mk :: (re: Float) (im: Float)

instance : Coe Float Complex where
  coe f := ⟨f,0⟩

@[simp, norm_cast] theorem of_float_inj {a b: Float} : (a : Complex) = b ↔ a = b := sorry

gives me

 { re := a, im := 0 } = { re := b, im := 0 }

(BTW: is Real not a thing in Lean 4?)

[James Gallicchio]

Noncomputable reals will probably live in mathlib4, which is currently a partial port of lean3 mathlib :)
https://github.com/leanprover-community/mathlib4

[Gabriel Ebner]

Ah, I don't think I documented this part!

[Gabriel Ebner]

For norm_cast to work correctly, you need to register the coercion.

[Gabriel Ebner]

This also enables the ↑ notation in the delaborator.

[Gabriel Ebner]

The easiest way to do this is to declare a separate function for the coercion and tag it with @[coe]:

[Gabriel Ebner]

@[coe] def Float.toComplex (f : Float) : Complex := ⟨f, 0⟩
instance : Coe Float Complex where coe := Float.toComplex

[Gabriel Ebner]

We're going to have some nice syntax on top of this that will automate the function+instance dance.

[Gabriel Ebner]

See also https://github.com/leanprover-community/mathlib4/issues/172