Type synonym boilerplate

Stream: mathlib4

[Johan Commelin]

Mathlib has quite a lot of type synonyms. Another one was added in this PR:

feat: Type synonym for the specialisation order #6985

Every type synonym goes through the dance of setting up an equiv and some simp-lemmas, etc...
Can we automate away this boilerplate, so that setting up an irreducible type synonym becomes a 1- or 2-liner?

[Jireh Loreaux]

it would be extra nice if we could choose the kind of equiv we want (e.g., ≃ₗ[R]), with all rfl proofs of course.

[Alex J. Best]

Jireh Loreaux said:

it would be extra nice if we could choose the kind of equiv we want (e.g., ≃ₗ[R]), with all rfl proofs of course.

A prerequisite of that would be to fix the delta deriving handler (in core) or reimplement it somehow as both sides would need typeclasses on them to make sense of the equiv

[Alex J. Best]

That said, I think its now quite easy to write commands to elaborate such boilerplate in a fairly natural looking way e.g.

import Mathlib.Tactic

open Lean Elab Command Term Parser Category PrettyPrinter
set_option hygiene false in
def mkBoilerplate (n : Name) : CommandElabM Unit := do
  let n : Ident := mkIdentFrom (← getRef) n

  elabCommandTopLevel <| ←`(command|
    def $n (α : Type*) := α)

  elabCommandTopLevel <| ←`(command|
    namespace $n)
  elabCommandTopLevel <| ←`(command|
    variable {α β γ : Type*})

  elabCommandTopLevel <| ←`(command|
    /-- `toEquiv` is the "identity" function to the `$n` of a type. -/
    @[match_pattern] def toEquiv : α ≃ $n α := Equiv.refl _)
  elabCommandTopLevel <| ←`(command|
    /-- `ofEquiv` is the identity function from the `$n` of a type.  -/
    @[match_pattern] def ofEquiv : $n α ≃ α := Equiv.refl _)

  elabCommandTopLevel <| ←`(command|
    end $n)

#print mkBoilerplate
whatsnew in
#eval mkBoilerplate `Specialization
#eval mkBoilerplate `Additive'
#check Specialization.ofEquiv
#check Additive'.ofEquiv

[Alex J. Best]

This could of course be improved, the docstrings don't work and the first declaration added doesn't have a range (though the others do).
But I think using such commands to generate boilerplate would be worth it for $n > 1$ instances

[Patrick Massot]

As usual with such requests, we first need to collect half a dozen examples written by hand and see what is indeed repeated.

[Yaël Dillies]

docs#OrderDual, docs#Lex, docs#Finset.Colex, docs#WithUpperSetTopology, docs#Specialization, docs#Additive, docs#Multiplicative, docs#Opposite, docs#AddOpposite, docs#MulOpposite, docs#WithLp, docs#UniformFun, docs#Tropical etc... Those are the ones I can remember off the top of my head, so there's more.

[Yaël Dillies]

I made an effort for file#Order/Synonym to exactly represent what the boilerplate should look like

[Yaël Dillies]

On the other hand, docs#Specialization is a throwaway synonym. Its sole purpose is to construct the functor Top => Preord. I don't think it'll see any more use.

[Alex J. Best]

Yaël Dillies said:

On the other hand, docs#Specialization is a throwaway synonym. Its sole purpose is to construct the functor Top => Preord. I don't think it'll see any more use.

I think thats all the more reason to automate it (I can imagine automation failing for things which have more specific requirements due to being used more widely)