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

[shigoel]

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

[dranov]

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]

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

[dranov]

Thank you, @PratherConid!

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