Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: all axioms used

Matthew Ballard (Jan 31 2022 at 14:53):

Jason Rute said:

Jesse Michael Han suggested that we could list all the axioms used. That should be a general solution for this sort of thing. (I assume a constant is considered an axiom, right?) However, I don’t know if there is currently a tactic which will tell you what axioms are used in an expression. Does anyone know if there is and if not what obstacles exist in making one?

What is the current state of such a tactic?

Reid Barton (Jan 31 2022 at 14:57):

It's not exactly a tactic, but #print axioms X will show you axioms used by the top-level declaration (e.g. definition/lemma) X

Matthew Ballard (Jan 31 2022 at 14:59):

Thanks, does this do const also?

Matthew Ballard (Jan 31 2022 at 15:05):

I should probably mention the context: I hand out an open-ended Lean assignment of the form "State and prove X". This might come with a library of axioms that make the problem reasonable.

Given the completed assignment, I would like to

  • scan for the construction of a term of the correct type
  • have Lean sign off on the proof (ie no sorry warnings or errors)
  • and filter any global constants to make sure only the allowed ones are in scope

Reid Barton (Jan 31 2022 at 15:06):

I think you mean does it also track constants that are used? Then yes.

Matthew Ballard (Jan 31 2022 at 15:07):

Great!

Reid Barton (Jan 31 2022 at 15:07):

Right, I think it's for exactly this kind of situation.
You might check out the setup on codewars (there's a stream of the same name here, but not active lately).

Matthew Ballard (Jan 31 2022 at 15:08):

I scanned through that but perhaps I should do so again.

Matthew Ballard (Jan 31 2022 at 15:08):

Thanks.

Alex J. Best (Jan 31 2022 at 15:09):

https://github.com/codewars/codewars-runner-cli/issues/773 and https://github.com/maxhaslbeck/proving-contest-backends/blob/master/Lean/grader.py might be helpful

Reid Barton (Jan 31 2022 at 15:09):

Maybe also get in touch with Donald Sebastian Leung who I think did most of the implementation work for that.

Matthew Ballard (Jan 31 2022 at 15:13):

Thanks to both of you. One more question: I can parse the output of #print axioms X directly in Lean, right? I get the sense that it is easier to farm the task out something else though.

Johan Commelin (Jan 31 2022 at 15:15):

No, it get's printed to stdout or something. I don't think you can grab that output within Lean itself.

Reid Barton (Jan 31 2022 at 15:15):

Right, it would be a bit tricky to parse the output in an automated way, so worth looking at prior art.

Matthew Ballard (Jan 31 2022 at 15:15):

Ah ok.

Matthew Ballard (Jan 31 2022 at 15:15):

But Lean 4 right? More precisely, this will be/is possible in Lean 4 correct?

Matthew Ballard (Jan 31 2022 at 15:21):

I will drop a link to the implementation output of the Codewars discussion for ease of reference (especially for future me).

Reid Barton (Jan 31 2022 at 15:27):

Wow, that's quite a helpful link!

Alex J. Best (Jan 31 2022 at 15:28):

Everything should be easier in Lean 4 indeed, here is the lean 4 print axioms command where you can call collect yourself https://github.com/leanprover/lean4/blob/89edc184fb7de86c4d9edb01f73aea95e6cc7f9d/src/Lean/Elab/Print.lean#L82

Matthew Ballard (Jan 31 2022 at 15:31):

Sweet.

Last updated: Dec 20 2023 at 11:08 UTC