search

leanprover-community / lean-auto

Experiments in automation for Lean
Apache License 2.0
66 stars 10 forks source link

Feature request: define SMT functions that match Lean names whenever possible for ease of debugging & readability #7

Open shigoel opened 9 months ago

shigoel commented 9 months ago

This would also make it easier for the user to interpret counterexamples in terms of identifiers in their conjecture.

dranov commented 4 months ago

We need this as well for our project and I'd be happy to implement it given some hints as to what might be the best or easiest way to do it, @PratherConid.

To give some context: we expect to have some goals that are sat and want to show some human-readable models to our users. Right now, it's very difficult to match the output from set_option trace.auto.smt.model true to what the user sees at the Lean level.

PratherConid commented 4 months ago

Thanks, @dranov! I've done some refactoring in ff56bdbb2a800edea572933eb800ad913cf2ba74. Now I think SMT functions' names basically match Lean names, but there still might be issues. @shigoel @dranov please take a look.

dranov commented 4 months ago

Thank you, @PratherConid!

It looks good so far – I'll report back if I run into any issues.