Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hi,
This PR brings HOL-Light's
INTEGER_TAC
(andINTEGER_RULE
) into HOL4. It is a by-product of another ongoing work of porting HOL-Light'sRING_TAC
to HOL4. The underlying implementation is based on theNormalizer
andGrobner
packages used byREAL_ARITH_TAC
andREAL_FIELD_TAC
. Insrc/integer/selftest.sml
, there are two examples:An intermediate function,
INT_RING :term -> thm
, can be useful as the simplification step of more advanced decision procedures, namelyCOOPER_TAC
andOMEGA_TAC
. I put the related code intointegerRingLib
without depending onCooper
andOmega
packages, so that later this work can be integrated into them.The main implementation of
INTEGER_TAC
is currently inintLib.sml
.It uses some code (
CONJ_ACI_RULE
, etc.) previously innormalForms.sml
without signatures. Now I have move these code toCanon
package (which seems a partial port of HOL-Light'scanon.ml
).In
mesonLib
, I added HOL-Light compatibleMESON
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 byINTEGER_TAC
) ported from HOL-Light. In theory the singleREDUCE_CONV
can also do the job, but these new conversions have better performance (by doing much less rewritings on large inputs), e.g.:The «HOL Description» was broken by new code added into
intLib
, because there is some code manipulating the overload ofint_add
. I resolved the manual PDF building by movingload "intLib"
to earlier places.Let's see how the CI tests will go (perhaps there are missing code in the PR branch).
Chun