Custom structure constructors with `where`

Stream: mathlib4

[Bhavik Mehta]

Throughout mathlib, we often have alternate constructors for structures or classes for convenience (for example, Equiv.ofBijective). Is it possible to extend Lean's where notation to allow these as well?
I'm imagining something like

def myEquiv {α β : Type*} {f : α → β} (hf : f.Bijective) : α ≃ β
    where (mk := Equiv.ofBijective)
  f := f
  hf := hf

so I can specify the constructor I want to use, then the rest would elaborate as if Equiv.ofBijective was the actual constructor instead of Equiv.mk. (I'm flexible on the (mk :=_) notation)

[Kyle Miller]

I've thought something like this would be neat. It would also let you apply a transformation function or elaborator to the result.

[Kyle Miller]

An alternative design though is to make a version of Equiv.ofBijective that takes a structure designed just for it, and then you would write

def myEquiv {α β : Type*} {f : α → β} (hf : f.Bijective) : α ≃ β :=
  Equiv.ofBijective' {
    toFun := f
    bijective := hf
  }

Now that {..} notation supports everything that where does, this loses nothing, and it doesn't take implementing new core features.

[Bhavik Mehta]

Hmm, I think this would mean we'd end up with loads of extra structures around mathlib. That said, I was hoping that there'd be a way of extending where in batteries/mathlib instead of adding bits to core

[Kyle Miller]

Yes, it would mean making more structures, but is there any harm in that? I assumed they'd be documented with "alternative formulation for X, use X.ofY to use" to keep any theory from being built up.

Of course there's also

def myEquiv {α β : Type*} {f : α → β} (hf : f.Bijective) : α ≃ β :=
  Equiv.ofBijective
    (f := f)
    (hf := hf)

[Kyle Miller]

(The where syntax isn't extensible outside of core.)

[Bhavik Mehta]

Does this one allow (f x := f x) like where does?

[Kyle Miller]

No, that's just available to { ... } and where

[Kevin Buzzard]

I ran into this just the other day, when I was making restricted products of groups. My thought process was:

• given a bunch of groups and some structure, I want to make a new group.
• Let's use the default constructor -- oh this stinks because I have to prove too many axioms.
• Oh, but I remember Chris Hughes PR'ed things like docs#Group.ofLeftAxioms which means I only have to prove the minimal axioms
• Oh but then I lose all the nice structure provided by the default structure constructor and my code becomes unreadable.

[Yaël Dillies]

Kyle Miller said:

An alternative design though is to make a version of Equiv.ofBijective that takes a structure designed just for it

This is precisely the MinimalAxioms design, eg docs#Order.Frame.MinimalAxioms

[Daniel Weber]

Bhavik Mehta said:

Throughout mathlib, we often have alternate constructors for structures or classes for convenience (for example, Equiv.ofBijective). Is it possible to extend Lean's where notation to allow these as well?
I'm imagining something like

def myEquiv {α β : Type*} {f : α → β} (hf : f.Bijective) : α ≃ β
    where (mk := Equiv.ofBijective)
  f := f
  hf := hf

so I can specify the constructor I want to use, then the rest would elaborate as if Equiv.ofBijective was the actual constructor instead of Equiv.mk. (I'm flexible on the (mk :=_) notation)

Another bonus of this is that it (hopefully) would allow for something like (mk := @AddHom.mk _ _ _ noncanonicalInstance)

[Eric Wieser]

Or just (mk := @AddHom.mk _ _ _ (_))

[Bhavik Mehta]

Yaël Dillies said:

Kyle Miller said:

An alternative design though is to make a version of Equiv.ofBijective that takes a structure designed just for it

This is precisely the MinimalAxioms design, eg docs#Order.Frame.MinimalAxioms

Similarly docs#CategoryTheory.Adjunction.CoreHomEquiv and docs#CategoryTheory.Adjunction.CoreHomEquivUnitCounit