algebra.group.with_one

Stream: mathlib4

[Kevin Buzzard]

Here's an issue I ran into early on when porting algebra.group.with_one:

import Mathlib.Order.WithBot

def WithOne (α) :=
  Option α

instance : One (WithOne α) :=
  ⟨none⟩

instance : CoeTC α (WithOne α) :=
  ⟨some⟩

def unone {x : WithOne α} (hx : x ≠ 1) : α :=
  WithBot.unbot x hx

theorem unone_coe {x : α} (hx : (x : WithOne α) ≠ 1) : unone hx = x :=
  rfl
/-
failed to synthesize instance
  OfNat (Option α) 1
-/

It can be fixed by replacing 1 with (1 : WithOne α) or also, amusingly, with _, but the latter makes the lemma unreadable and the former is going to get old very soon... . Is there a way of making 1 work?

[Ruben Van de Velde]

Oh, that's the same issue as with WithBot, I think

[Ruben Van de Velde]

Which was solved by defining WithBot.some?

[Mario Carneiro]

Yes, this is a bad instance:

instance : CoeTC α (WithOne α) :=
  ⟨some⟩

because it says it's going to convert a α -> WithOne α but it is actually a function with the type α -> Option α

[Mario Carneiro]

which is bad when coercions are eagerly unfolded to their definitions

[Mario Carneiro]

I would call it WithBot.coe instead of WithBot.some. The use of some here was abuse from the beginning

[Kevin Buzzard]

OK thanks, I'm being inspired by WithBot. I'll call it coe.

[Eric Wieser]

This was fine in mathlib3 because we could use the global coe as the name for the operation, but we can't now that it unfolds

[Scott Morrison]

Oh! @Kevin Buzzard, note that we've just split this file in mathlib3. It is now algebra.group.with_one.defs that needs porting.

[Scott Morrison]

algebra.group.with_one itself no longer exists.

[Kevin Buzzard]

Oh nice! Thanks for letting me know!