elaboration of coercions

Stream: lean4

[Kevin Buzzard]

I'm still wrestling with the new normal for coercions. In Lean 3 I was familiar with this:

import algebra.group.with_one.defs

theorem coe_inv {α : Type*} [has_inv α] (a : α) :
  ((a⁻¹ : α) : with_one α) = a⁻¹ :=
  rfl

#check coe_inv -- ↑a⁻¹ = (↑a)⁻¹

What happens here is that the LHS has type with_one \alpha (a type synonym for option \alpha) so inv is elaborated as with_one.inv and then a is coerced from \alphato with_one \alpha. In Lean 4 this common mathlib idiom behaves differently:

class Inv (α : Type u) where
  /-- Invert an element of α. -/
  inv : α → α

postfix:max "⁻¹" => Inv.inv

instance (α : Type u) [Inv α] : Inv (Option α) :=
  ⟨λ a => match a with
     | Option.none => Option.none
     | Option.some x => Option.some x⁻¹
  ⟩

theorem coe_inv [Inv α] (a : α) : ((a⁻¹ : α) : Option α) = a⁻¹ :=
  rfl

#check coe_inv -- some a⁻¹ = some a⁻¹

For some reason elaboration is behaving differently; the same code is giving us a syntactic tautology. This looks like something which we'll have to be careful about when porting. Why is it happening, out of interest? Of course it's easily fixed with (a : Option α)⁻¹ but this is everywhere in mathlib.

[Kevin Buzzard]

((a⁻¹ : α) : Option α) = (↑a)⁻¹ works, by the way (and is what I'm using on the ground)

[Mario Carneiro]

this looks like something that should be reported as an issue

[Kevin Buzzard]

https://github.com/leanprover/lean4/issues/1915

[Eric Wieser]

Presumably ↑(a⁻¹) = ((↑a)⁻¹ : Option α) also works?