Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Parsing strings with `def` or `theorem` keywords


Anand Rao (Jul 14 2022 at 05:50):

I would like to be able to parse strings like "theorem foo (m n : ℤ) : m + n = n + m", which contain keywords such as theorem or def, to lean3 expressions.

I am aware that standalone expressions like ∀ (m n : ℤ), m + n = n + m can be parsed by using lean.parser.with_input interactive.types.texpr, and I tried inspecting the source for similar functions but could not infer much. I expect that lean should have a built-in mechanism of converting a statement like theorem foo (m n : ℤ) : m + n = n + m to theorem foo : ∀ (m n : ℤ), m + n = n + m (where all the parameters are pushed to the right of the colon with universal quantification), because I usually see the latter when I #check theorem names.

Is there a way for me to parse strings that contain theorem or def keywords? Alternatively, is there an in-built function that pushes all the parameters to the right of the colon, so that I can simply discard everything to the left of the colon and run the usual `lean.parser.with_input interactive.types.texpr?

Eric Wieser (Jul 14 2022 at 07:14):

Can you elaborate a bit on your motivation?

Anand Rao (Jul 14 2022 at 14:44):

This is meant for checking the output of a language model.

Eric Wieser (Jul 14 2022 at 15:29):

You could write the string out to a file, append a short metaprogram to inspect the definition it generates and dump it to stdout, and then use io.cmd ["lean", your_file] to get the result

Eric Wieser (Jul 14 2022 at 15:32):

Is the language model written in lean itself?

Eric Wieser (Jul 14 2022 at 15:34):

Maybe this answers your question:

import tactic.core

run_parser do
  lean.parser.emit_command_here "def foo : ℕ := 1",
  d  tactic.get_decl `foo,
  tactic.trace d

Eric Wieser (Jul 14 2022 at 15:36):

If you don't even know what the name of the theorem that the language model output was, you could list all the existing names, then emit the model code, then see what new names appeared


Last updated: Dec 20 2023 at 11:08 UTC