SMT names that match Lean names

leanprover-community / lean-auto

Experiments in automation for Lean

Apache License 2.0

72 stars 12 forks source link

SMT names that match Lean names #26

Closed dranov closed 5 months ago

dranov commented 6 months ago

This is a draft PR addressing #7. I am still working on this, but want some feedback early.

As of now, sorts and terms in SMT-LIB get names that are derived from the Lean names. There are a few remaining hiccups:

[ ] etoms are still named stmi_<N>
[ ] inductive data types have constructors named cifvar_<N>– I'm not sure what is going on there
[x] disposable names, used for quantifier binders, still have uninformative names, e.g. stmd_80

See the test case in Test/SmtTranslation/Names.lean for a large example.

As part of this PR, I also want to give the valid_fact_<N> assertions (part of unsat cores) potentially more user-readable names, matching the hypothesis in the Lean context where auto is called. That seems more straightforward.

dranov commented 6 months ago

@PratherConid I'm not sure where to get etom names. What do they correspond to on the Lean side? Could you please point me in the right direction?

dranov commented 5 months ago

With regards to disposableName (used in lamQuantified2STerm), is the original Lean name of the binder kept anywhere?

PratherConid commented 5 months ago

No, Lean-auto does not keep the name of the original binder. I did not include it in LamTerm because it might affect the performance of the checker.

PratherConid commented 5 months ago

I think you can also ignore this for now. Supporting SMT binder names that correspond to Lean binder names will require systematic changes to the codebase. An easier approach would be giving binders names like a, b, c.

dranov commented 5 months ago

Alright, that's fair. For now I've settled on taking the binder names from the associated sorts, so for instance you now get n<idx> for a binder of sort node rather than smtd_<idx>.

dranov commented 5 months ago

I've removed the unrelated commit making DTr less stringly-typed. I will probably make a separate PR containing that commit to give assertions names closer to the Lean names.

dranov commented 5 months ago

@PratherConid I guess this is good enough for now. Could you please take a look, clean-up as necessary, and merge?

PratherConid commented 5 months ago

← PrettyPrinter.formatTerm (← PrettyPrinter.delab e).raw might also be used to pretty-print DTr.

PratherConid commented 5 months ago

I'll merge the pull request for now.

PratherConid commented 5 months ago

Made some significant changes in ff56bdbb2a800edea572933eb800ad913cf2ba74, behaviour on SMTTranslation/Names.lean becomes a bit different.