Metaprograming: making instance within a `Telescope`

Stream: lean4

[Cody Roux]

Another minor metaprograming question (please tell me if I should be creating threads with larger scope).

I'm trying to declare a command that takes in a lambda and creates an instance parametrized by those same vars. E.g. one could imagine a method

#derive_with_params (fun x : Nat => Inhabited Nat)

that generates a command like:

instance myInstance (x : Nat) : Inhabited Nat := ...

I've been trying to do this with one big lambdaTelescope, but CommandElabM does not implement the required interface, namely MonadControlT MetaM. Term.TermElabM does, but AFAIKT this does not allow me to define a new instance in an easy way (though it is easy to lift a TermElabM to a CommandElabM).

Any suggestions to get around this? Is there some way to

A) Define a MonadControlT MetaM for CommandElabM or
B) Do things in a different way to avoid this issue?

Thanks!

[Floris van Doorn]

Is it important for you to generate the syntax for the instance command? It's probably easier to directly call docs#Lean.addAndCompile, which adds a declaration to the environment (after that you will have to add the @[instance] attribute with docs#Lean.Meta.addInstance).

[Cody Roux]

Are those the only 2 things that happen on an instance declaration?

[Cody Roux]

I am a bit nervous about having to come up with all the fields here: https://leanprover-community.github.io/mathlib4_docs/Lean/Declaration.html#Lean.DefinitionVal

[Cody Roux]

And it's worth noting that the body will be a fixpoint, so someone will need to elaborate this term

[Floris van Doorn]

Well, there is more, like configuring jump-to-definition. But you have to do something differently there anyway, as the syntax doesn't literally exist anywhere in the file.

[Floris van Doorn]

You can take a look at what @[to_additive] or @[simps] do, which both add declarations. Search for addDecl and surrounding code. @[to_additive] does quite a bit more, like copying attributes and generating equational lemmas eagerly (and applying to_additive to them), but that shouldn't be necessary for you.

[Jannis Limperg]

If you want to stick with the syntax-based approach, you should be able to construct the command syntax (Lean.Command) in TermElabM, pass it up to CommandElabM via liftTermElabM, and elabCommand there.

[Cody Roux]

That does seem a bit easier in the short term

[Jannis Limperg]

Btw, I thought there was a convention that commands prefixed with a hash are not supposed to change the environment. But not sure whether people are still sticking to that.

[Cody Roux]

oh, that's good to know!

[Cody Roux]

(originally I think @Ernest Ng designed this as a "you can declare this instance" message)

[Jannis Limperg]

I should mention that the syntactic approach is unreliable if you delaborate Expr to Syntax anywhere. The delaborator is known not to be round-tripping in certain cases, so the generated command may fail to elaborate even though your Expr is correct. There are some pretty-printing options that partly fix the issue, most prominently pp.analyze and its sub-options. But the 'correct' way to do it is to stay in Expr land, like Floris says.

[Cody Roux]

Several disadvantages to that, unfortunately:

1. It'd be a big rewrite at this point
2. It's hard to write big pattern matches directly in Expr (deriving BEq doesn't do it!)
3. You can't generate code from recursors AFAIK (has that changed?)