Deriving Instance for Inductives that have arguments

Stream: metaprogramming / tactics

[Ernest Ng]

Hi! I'm currently trying to implement my own deriving instance. Here's the context:

-- A typeclass that describes whether the proposition `P` is  partially decidable
-- (details are not important)
-- I'd like the user to be able to write `deriving DecOpt` for an `inductive` relation
class DecOpt (P : Prop) where
  ...

-- Here's an example inductive relation:
-- `typing Γ e τ` represents a typing derivation `Γ ⊢ e : τ`
-- (assume that the `type` and `term` inductives have already been defined)
inductive typing: List type → term → type → Prop where
   ...

I'd like the user to be able to write deriving instance DecOpt for (typing Γ e τ), but Lean complains that this is invalid syntax. Alternatively, if the user just writes deriving DecOpt underneath the definition of the typing inductive, the named arguments Γ, e, τ are not available to the deriving handler and the code is ill-typed (since DecOpt expects a Prop as its argument). Is there a way to implement a deriving handler for inductives that are parameterized by 1 or more arguments? Thanks!

[Ernest Ng]

If this is not possible, would it be advisable for me to just implement a command elaborator instead? (e.g. implement an elaborator for the command #derive_decopt such that the user can write #derive_decopt typing Γ e τ)

[Robin Arnez]

I'm not sure why you'd need to provide these explicitly unless you want to have concrete values for Γ, e and τ. Otherwise you should be able to access the inductive definition and make such parameters yourself..?

[Ernest Ng]

Oh right, good point, thanks! I guess I can always generate fresh names for each of these parameters.

[Kyle Miller]

Have you been referring to the existing deriving handlers?

[Ernest Ng]

Yep! I've been looking at the source code for the Beq deriving handler as well as the section in the language reference

[Kyle Miller]

I was asking because these deriving handlers all handle this issue.

There are also some more deriving handlers in Mathlib that might be useful to look at, for example Mathlib/Tactic/Derive*.lean. The Fintype handler is the briefest, where it uses Deriving.mkHeader to create the header with the fresh names: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/DeriveFintype.lean#L91-L102

[Ernest Ng]

Thanks a lot! The Fintype handler code is very helpful -- I'll look into using mkHeader!

[Kyle Miller]

BEq uses it too: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving/BEq.lean#L16

[Ernest Ng]

Ah yes good point thanks!