Feature requests: Meaningful UNSAT cores and Models in Lean

[mww-aws]

Is it possible / meaningful to get UNSAT cores or models in a format that is meaningful in Lean?

We are representing domain models and some queries against those models. We would (if possible) like to get witnesses to proof failures expressed in a meaningful way back into Lean, and to get UNSAT cores that have meaning in Lean.

The underlying idea is that we want users to be able to "ask questions" about domain models by checking whether partially instantiated ground terms are conformant with the model and then presenting the results back in a meaningful way.

Mostly I am curious whether this is on your roadmap for any point in the future.

[PratherConid]

Yes! It will be one of the first features I'll implement after Jan 7th next year.

[PratherConid]

Now there's basic support for unsat cores. auto.smt.unsatCore.smtTerms shows the SMT terms of the unsat core, and auto.smt.printValuation prints the Lean expressions corresponding to SMT uninterpreted functions/sorts.
The next step I'll implement is to directly print Lean expressions corresponding to SMT terms in the unsat core.

[PratherConid]

237f06c implements Lean expression printing for SMT unsat cores. Use set_option trace.auto.smt.unsatCore.leanExprs true.