HOL-Light's INTEGER_TAC

[binghe]

Hi,

This PR brings HOL-Light's INTEGER_TAC (and INTEGER_RULE) into HOL4. It is a by-product of another ongoing work of porting HOL-Light's RING_TAC to HOL4. The underlying implementation is based on the Normalizer and Grobner packages used by REAL_ARITH_TAC and REAL_FIELD_TAC. In src/integer/selftest.sml, there are two examples:

> INTEGER_RULE “w * y + x * z - (w * z + x * y) = (w - x) * (y - z:int)”;
val it = |- w * y + x * z - (w * z + x * y) = (w - x) * (y - z): thm
> INTEGER_RULE “a int_divides &n <=> a int_divides -&n”;
2 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
Translating certificate to HOL inferences
2 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
Translating certificate to HOL inferences
val it = |- a int_divides &n <=> a int_divides -&n: thm

An intermediate function, INT_RING :term -> thm, can be useful as the simplification step of more advanced decision procedures, namely COOPER_TAC and OMEGA_TAC. I put the related code into integerRingLib without depending on Cooper and Omega packages, so that later this work can be integrated into them.

The main implementation of INTEGER_TAC is currently in intLib.sml.

It uses some code (CONJ_ACI_RULE, etc.) previously in normalForms.sml without signatures. Now I have move these code to Canon package (which seems a partial port of HOL-Light's canon.ml).

In mesonLib, I added HOL-Light compatible MESON function, which has currently multiple copies in proofs ported from HOL-Light (I will clean them up later).

In intReduce, I added some integer arithmetic conversions (they are used by INTEGER_TAC) ported from HOL-Light. In theory the single REDUCE_CONV can also do the job, but these new conversions have better performance (by doing much less rewritings on large inputs), e.g.:

> Count.apply intReduce.REDUCE_CONV ``&1000 * -&1000``;
runtime: 0.00147s,    gctime: 0.00000s,     systime: 0.00328s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 1953; Total: 1953
val it = |- 1000 * -1000 = -1000000: thm

> Count.apply intReduce.INT_MUL_CONV ``&1000 * -&1000``;
runtime: 0.00003s,    gctime: 0.00000s,     systime: 0.00003s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 10; Total: 10
val it = |- 1000 * -1000 = -1000000: thm

The «HOL Description» was broken by new code added into intLib, because there is some code manipulating the overload of int_add. I resolved the manual PDF building by moving load "intLib" to earlier places.

Let's see how the CI tests will go (perhaps there are missing code in the PR branch).

Chun

[mn200]

Could you write some documentation (perhaps in DESCRIPTION’s libraries.stex) on what this tactic does and does not do?

[binghe]

Could you write some documentation (perhaps in DESCRIPTION’s libraries.stex) on what this tactic does and does not do?

will try that

[binghe]

I have added a paragraph in «HOL Description» (and next-release.md) about INTEGER_TAC (after \paragraph{intLib} about OMEGA_CONV and ARITH_CONV:

In addition, the \ml{intLib.INTEGER_RULE} (and its tactic version \ml{intLib.INTEGER_TAC})
ported from HOL-Light can solve some simple equations about divisibility of integers,
e.g.~\holtxt{d int_divides m ==> d int_divides (m * n)}.
As part of the procedure, multivariate polynomials of integer are expanded to their
``normal forms'' (with respect to certain ordering), and thus equations between equivalent
such polynomials can be decided,
e.g.~\holtxt{w * y + x * z - (w * z + x * y) = (w - x) * (y - z)}.

[binghe]

The last commit fixed a bug in DISJ_ACI_RULE (used indirectly by REAL_ARITH, now the signature is exposed), caused by the semantic difference of UNDISCH between HOL4 and HOL-Light. In HOL4, the document of UNDISCH clearly says that {UNDISCH} treats {"~u"} as {"u ==> F"} while in HOL-Light there's no such behavior. Therefore the code repeat UNDISCH (TAUT ‘~a ==> ~b ==> ~(a \/ b)’) gives different results between the two systems and has caused the bug (which is exposed by the forthcoming RING_TAC).

[mn200]

Thanks for this!