Limitations of meta programming in Lean

Stream: new members

[Yasmine Sharoda]

Hello,
I have been reading about meta programming in Lean and I am under the impression that one can only generate expressions as described by the type expr.
Is that true? Is it possible to generate inductive types or structures?

[Kevin Buzzard]

Hi! I don't know a thing about metaprogramming in Lean but I just tried this:

meta inductive mynat
| zero : mynat
| succ : mynat → mynat

and it worked fine. I would thoroughly recommend Rob Lewis' videos on metaprogramming, hang on, I'll dig out the link.

[Kevin Buzzard]

https://www.youtube.com/playlist?list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2

[Yasmine Sharoda]

Thanks for answering.. I actually meant writing a program that generates the inductive type based on some input.
An example is: given a type class describing monoid, generate the monoid term language as an inductive type. This requires some introspection of a given type class.

[Yasmine Sharoda]

Kevin Buzzard said:

https://www.youtube.com/playlist?list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2

Those are really good tutorials.. I have just been watching them and found them very useful.

[Adam Topaz]

You can always use emit_code_here and construct whatever you want as if it was just lean code. But I don't know if this is what you're looking for.

Am I correct in guessing that when an inductive type is defined, that it's equivalent to a bunch of constants being defined?

[Adam Topaz]

By constant I mean writing constant a : ...

[Reid Barton]

There's docs#environment.add_inductive and docs#environment.add_ginductive

[Adam Topaz]

TIL :up:

[Yasmine Sharoda]

Reid Barton said:

There's docs#environment.add_inductive and docs#environment.add_ginductive

that's the closest to what I am looking for. Thank you
I have more questions:

• what is the difference between context, accessed using local_context, and the environment?
• how can one access the current environment?

[Yasmine Sharoda]

Adam Topaz said:

You can always use emit_code_here and construct whatever you want as if it was just lean code. But I don't know if this is what you're looking for.

Am I correct in guessing that when an inductive type is defined, that it's equivalent to a bunch of constants being defined?

Thanks for the insights.
What I really need is a meta program to manipulate lean definitions and generate inductive types. The output is determined based on the input, so emitting code won't be useful.
An inductive type can be seen as a bunch of constants, but for my purpose I need the "packaging".

[Adam Topaz]

Oh, I meant something silly like this:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universes/near/214247264

[Yasmine Sharoda]

Adam Topaz said:

Oh, I meant something silly like this:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universes/near/214247264

That is a string-based version of what I am trying to do.. I actually want to be able to be given any algebraic structure (a la universal algebra) and generate (among other things) its raw version. So I need to be able to be able to talk in the meta program about the "components" of the structure.

[Adam Topaz]

Yes, I understand, and agree that writing proper meta code with expr is the right approach. It would be really cool to have some automation to generate the "raw" version of classes by stripping out the Prop-valued fields.

[Reid Barton]

Yasmine Sharoda said:

Reid Barton said:

There's docs#environment.add_inductive and docs#environment.add_ginductive

that's the closest to what I am looking for. Thank you
I have more questions:

• what is the difference between context, accessed using local_context, and the environment?
• how can one access the current environment?

In brief,

• the environment contains everything defined "at top level", like defs and axioms, while the local context contains the hypotheses in the proof state, like function arguments and variables bound by have,
• tactic.get_env.

[Yasmine Sharoda]

This is really helpful, thank you.
I still have one more problem trying to define a unit type U with a constructor u. Here is the code:

meta def mk_const (n : name) : expr :=
 expr.const n [level.zero]

meta def uType : tactic environment :=
 do e ← get_env,
    new_env ← environment.add_inductive e `U [] 0 (expr.sort level.zero) [(`u, mk_const `U)] ff,
    return new_env

#eval uType

and I get the following error at #eval uType:

incorrect number of universe levels parameters for 'U', #0 expected, #1 provided

[Rob Lewis]

You don't need to give level.zero as an argument to expr.const in mk_const. U doesn't take any universe arguments, so you don't need to provide any.

open tactic

meta def mk_const (n : name) : expr :=
 expr.const n []

meta def uType : tactic environment :=
 do e ← get_env,
    new_env ← environment.add_inductive e `U [] 0 (expr.sort level.zero)
     [(`u, mk_const `U)]
    ff,
    return new_env

run_cmd uType >>= set_env

#check U
#check u

[Yasmine Sharoda]

that solves the problem. thank you