Integrate with an SMT Solver

[h0nzZik]

The SMTCoq plugin (https://smtcoq.github.io/) can be used in Coq to solve some goals automatically. I wonder if we could reuse SmtCoq for solving propositional and first-order goals in matching logic.

Essentially, the plugin converts the goal to a query that is sent to an SMT solver, then takes the proof object generated by the solver, represents it as a term inhabiting some inductive type, and lifts it up to the Coq level. We could reuse the interaction with the SMT, and only write our own conversion from a ML goal to FOL, and then the lifting of the proof object to the type of ML proof.

[daniel-horpacsi]

Section 4.3 in the AML technical report presents a conservative extension theorem for MSFOL, which may be of use when it comes to reasoning about the conversions.