HolSmt: implement div and mod, fix proof replay, fix translation

[someplaceguy]

Hi!

This PR implements support for DIV, MOD, $/, $%, quot and rem, i.e. all div and mod operators for num and int. It also enables proof replay for all the self-tests that contained these operators. No changes were made outside HolSmt.

In total, 78 more self-tests are now passing (with Z3 v4 proof replay). In fact, I believe all arithmetic test cases are now passing, including with proof replay, with the exception of the word tests (and one which I added and mention below).

The support for the div and mod operators were implemented using the following approach:

1. First, I defined two functions in HolSmtTheory called smtdiv and smtmod, which implement the semantics of SMT-LIB's integer division and modulo operators.
   • These two operators have different definitions than all of HOL4's div and mod operators; however smtdiv was defined based on $/ and smtmod based on $% for simplicity.
2. A test case was added to selftests.sml which verifies that smtdiv and smtmod exactly match the SMT-LIB definition.
   • Initially, I was planning on manually proving this theorem, but it appears to be quite laborious to do so.
   • However, as always, Z3 can prove this easily (hence why this was proved in selftests.sml).
   • Unfortunately, we can't reconstruct this proof (because one of the proof steps seems to rely on nonlinear arithmetic), so the proof is not really meaningful...
3. Theorems were added to HolSmtTheory which define HOL4's div and mod operators in terms of smtdiv and smtmod (these are easier to prove). These theorems are now added to the proving context by default, so that SMT solvers can translate HOL4's div and mod operators into the equivalent SMT-LIB div and mod operators which they natively support.
4. SMT-LIB translation and parser support were added for smtdiv and smtmod.
5. Support was added to the linear arithmetic proof handlers so that they can prove goals that have smtdiv and smtmod (by rewriting with their definitions into equivalent HOL4 $/ and $% operations).

This PR also implements the following:

1. Fixed the translation of let ... and ... in ..., i.e. the one with parallel definitions, into the SMT-LIB language. This translation had never actually worked before, only let ... ; ... in ... was working properly.
2. Fixed slowness (more like an apparent hang) due to the workaround for #1203. Apparently, COOPER_PROVE is much slower than ARITH_PROVE in some cases, so now we try the latter before falling back to the former.
3. Major improvements in the arithmetic proving procedures:
   • Implemented a workaround for #1209.
   • Implemented some workarounds for #1207.
   • The generalize_ite procedure was removed, as it seems to be unnecessary and was causing some arithmetic proof steps to fail.
   • As mentioned above, added support for smtdiv and smtmod.
   • Since both the th_lemma_arith and rewrite arithmetic proof handlers need the above fixes, these arithmetic proving procedures now use a common implementation.
4. Implemented a workaround for a Z3 bug where it adds an hypothesis but then forgets to discharge it.
   • Fortunately, such hypotheses always seem to be of the form P = P, so it's easy to discharge them ourselves.
   • However, I am planning to file a Z3 bug (or even a PR) once I get an opportunity to debug this issue.
5. Implemented a handler for the iff-false Z3 proof inference rule.

I'm happy with the results, although I was a bit surprised by how hard it was to fix proof replay for these tests. I was expecting Z3 to throw more curve-balls, but this time Z3 did not give me much trouble.

Instead, the major problems were the limitations in the HOL4 integer arithmetic decision procedures, especially #1207. I implemented some workarounds (i.e. I try to prove the goals using some additional tactics, including arithmetic simplifications) but I don't expect these to be reliable and in fact, if I change some theorems around a bit I do encounter some linear arithmetic steps which HOL4 cannot prove automatically even with my workarounds.

Anyway, I think this concludes my work for the near future, as the next issues to tackle are quite hard to solve.

Thanks!

cc @tjark

[someplaceguy]

Added one commit to update the HolSmt documentation regarding recent improvements.

[mn200]

Can you put the Euclidean div and mod constants (perhaps call them ediv and emod) into integerScript.sml please?

[someplaceguy]

Can you put the Euclidean div and mod constants (perhaps call them ediv and emod) into integerScript.sml please?

Sure, but how would you like me to do that? Just add those definitions to integerScript.sml as they are (except for the renaming)? Anything else?

For reference, I took a look at how int_quot and int_rem are defined and there seems to be a lot going on there, e.g.:

1. int_quot is actually defined based on the natural numbers (instead of being defined based on int_div like I did). This would be easy enough to do.
2. int_quot (and int_div) are constant specifications instead of constant definitions (which require proving a theorem, although that seems quite doable). Should I use constant specifications as well?
3. Infix constants are also defined, although this seems trivial.
4. Some quot-related theorems are proved. I guess I could try to prove similar ones, although it would take me some time... However, INT_QUOT_UNIQUE seems incredibly daunting to prove...
5. rem also has quite a few theorems and a few daunting ones as well...
6. Furthermore, these two operators also have theorems used for rewrites. I think I understand the *_REDUCE theorems but not the INT_{QUOT,REM}_CALCULATE ones.
7. These operators also have syntax manipulation functions defined in intSyntax.{sig,sml} (this seems trivial to add).
8. For completion I assume simplification rules are added somewhere, although I can't figure out where?
9. And then presumably these operators have support in the omega and cooper decision procedures, although I can't even find the string "quot" in there? (And even if I did, I doubt I'd be able to figure out how to add support for ediv and emod there...).

So, which of the above should I do?

[binghe]

Can you put the Euclidean div and mod constants (perhaps call them ediv and emod) into integerScript.sml please?

Sure, but how would you like me to do that? Just add those definitions to integerScript.sml as they are (except for the renaming)? Anything else?

For reference, I took a look at how int_quot and int_rem are defined and there seems to be a lot going on there, e.g.:

1. int_quot is actually defined based on the natural numbers (instead of being defined based on int_div like I did). This would be easy enough to do.
2. int_quot (and int_div) are constant specifications instead of constant definitions (which require proving a theorem, although that seems quite doable). Should I use constant specifications as well?
3. Infix constants are also defined, although this seems trivial.
4. Some quot-related theorems are proved. I guess I could try to prove similar ones, although it would take me some time... However, INT_QUOT_UNIQUE seems incredibly daunting to prove...
5. rem also has quite a few theorems and a few daunting ones as well...
6. Furthermore, these two operators also have theorems used for rewrites. I think I understand the *_REDUCE theorems but not the INT_{QUOT,REM}_CALCULATE ones.
7. These operators also have syntax manipulation functions defined in intSyntax.{sig,sml} (this seems trivial to add).
8. For completion I assume simplification rules are added somewhere, although I can't figure out where?
9. And then presumably these operators have support in the omega and cooper decision procedures, although I can't even find the string "quot" in there? (And even if I did, I doubt I'd be able to figure out how to add support for ediv and emod there...).

So, which of the above should I do?

I think @mn200 simply meant that you can move the definitions of smtdiv and smtmod (renamed to ediv and emod) and related theorems (from SMT_NUM_ADD to SMT_INT_REM), i.e. all you added into HolSmtScript.sml, to integerScript.sml. In this way, the definitions and theorems can be reused by potential other users in the future.

[mn200]

@binghe has it right; what you have already is a good starting point for future work, and it would be better to have that work happen in integerTheory.

[someplaceguy]

Added 7 more commits:

1. Fix a possible bug in a previously implemented workaround for a Z3 bug where a hypothesis is introduced but not discharged. Instead of avoiding to introduce the assumption, now HolSmt will get rid of it at the end of the proof replay procedure. This should make proof replay more robust, as it is possible that Z3 might introduce a hypothesis of the form P = P and then not forget to discharge it, in which case lemma might require the hypothesis to be there.
2. Moved the Euclidean div and mod definitions to integerTheory, as well as the theorems that had been added to HolSmt, as requested by @binghe and @mn200.
3. Changed HolSmt to use integerTheory's definition of ediv and emod, as well as the theorems that were moved there, thus removing the definitions and theorems from HolSmt.
4. Removed workaround for #1209 as it is now fixed (thank you @mn200!)
5. Fixed replay of goals containing quot and rem due to #1207.
6. Add 73 new tests exercising quot and rem, all with Z3 proof replay enabled. Perplexingly, I had forgotten to add these.
7. Add some simps to thm_AUTO, which help make advances in proving the last self-test but do not yet allow it to succeed.

Note: I wasn't sure what to name the newly added definitions and theorems in integerTheory, nor where to put them exactly, so let me know if you'd like me to make any further changes.

Thanks!

[someplaceguy]

Added one more commit which ignores indices in rewrite proof rules instead of failing to parse the proof certificates with an error. This way we don't fail to parse proof certificates in case e.g. a future version of Z3 adds an index to these proof rules.

[someplaceguy]

Added one more commit which partially reverts a previous one, which had added a change that was actually unnecessary.

I realized this was unnecessary after thinking about it (and realizing it didn't make much sense), however I don't understand why I introduced that change in the first place, since I cannot reproduce those test failures and nothing relevant was changed in the mean time...

[someplaceguy]

Added 2 more commits, which fix issues when parsing SMT-LIB commands.

This part of the parser is used only for importing SMT-LIB problems into HOL4, which is useful for testing HolSmt but is not the main use case of HolSmt.

[someplaceguy]

Added one more commit with a simple fix, this time fixing an error when parsing some Z3 proof certificates.

[someplaceguy]

Added one commit to remove the workaround for #1203, since it's no longer necessary. Thanks @mn200!

[mn200]

Thanks for all of this work!