-
Notifications
You must be signed in to change notification settings - Fork 131
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
intLib.{ARITH,COOPER}_PROVE can't prove certain goals #1207
Comments
I found a similar issue with a different arithmetic operator. This succeeds: > intLib.ARITH_PROVE ``&x % 1 >= 0i``; But this fails: > intLib.ARITH_PROVE ``&x % &Num 1 >= 0i``; |
I also found an issue only containing integers. These succeed: > intLib.ARITH_PROVE ``ABS 1 = 1``;
> intLib.ARITH_PROVE ``1 % 1 = 0``; But this fails: > intLib.ARITH_PROVE ``1 % ABS 1 = 0``; |
The `th_lemma_arith` was running into several issues. The following changes were made: 1. The `generalize_ite` procedure was removed, since the arithmetic decision procedures can handle `if ... then ... else ...` now. It was causing replay failures because some terms were not provable unless the decision procedures could inspect the `if` bodies. 2. The arithmetic decision procedures don't understand `smtdiv` and `smtmod`; so before proving the term, we now rewrite it with the definitions of these functions. 3. A workaround was also implemented for some instances of the following issue: HOL-Theorem-Prover#1207 Namely, the integer decision procedures cannot decide some terms containing `ABS` and `Num`, so we rewrite them when possible.
This commit adds some tactics which help prove some arithmetic proof steps that intLib.{ARITH,COOPER}_TAC can't deal with. These are basically some workarounds for: HOL-Theorem-Prover#1207 This allows us to enable proof replay for the remaining arithmetic test cases that didn't already have proof replay enabled, with the exception of the very last test case (because we can't replay nonlinear arithmetic proof steps). That said, I don't expect these workarounds to be very reliable. Ideally, it would be better to improve HOL4's linear arithmetic decision procedures.
Goals containing > intLib.ARITH_PROVE ``x quot 42 <= ABS x``;
> intLib.ARITH_PROVE ``x rem 42 < 42``; If I get rid of the |
Addresses a couple of cases from github issue #1207
So these are interesting; thanks! The |
@mn200 Thank you for looking into this and for fixing #1203! Unfortunately, I still cannot remove the workaround for #1203 from HolSmt because now I'm experiencing a slightly different issue. From the user perspective, this slightly different issue is a mix between #1203 and the problems I've been reporting in this issue: > intLib.ARITH_PROVE ``x <= -42 \/ 1 < (41 * x) % 42 \/ -21 < (41 * x) / 42``;
Exception-
HOL_ERR
{message =
"Tried to prove generalised goal (generalising x...) but it was false",
origin_function = "OMEGA_CONV", origin_structure = "IntDP_Munge"}
raised So as you can see, the error is similar to the ones in this issue. However, unlike the other issues I reported here (but similarly to #1203), this time COOPER_PROVE does succeed: > intLib.COOPER_PROVE ``x <= -42 \/ 1 < (41 * x) % 42 \/ -21 < (41 * x) / 42``;
val it = [] |- x <= -42 \/ 1 < (41 * x) % 42 \/ -21 < 41 * x / 42: thm As a result, for now, I've kept COOPER_PROVE as a fallback for proving arithmetic rules in HolSmt when ARITH_PROVE fails. Thanks! |
Thanks to someplaceguy for reporting these. Progress of sorts with github issue #1207
The `th_lemma_arith` was running into several issues. The following changes were made: 1. The `generalize_ite` procedure was removed, since the arithmetic decision procedures can handle `if ... then ... else ...` now. It was causing replay failures because some terms were not provable unless the decision procedures could inspect the `if` bodies. 2. The arithmetic decision procedures don't understand `smtdiv` and `smtmod`; so before proving the term, we now rewrite it with the definitions of these functions. 3. A workaround was also implemented for some instances of the following issue: #1207 Namely, the integer decision procedures cannot decide some terms containing `ABS` and `Num`, so we rewrite them when possible.
This commit adds some tactics which help prove some arithmetic proof steps that intLib.{ARITH,COOPER}_TAC can't deal with. These are basically some workarounds for: #1207 This allows us to enable proof replay for the remaining arithmetic test cases that didn't already have proof replay enabled, with the exception of the very last test case (because we can't replay nonlinear arithmetic proof steps). That said, I don't expect these workarounds to be very reliable. Ideally, it would be better to improve HOL4's linear arithmetic decision procedures.
I'm running into an issue where both
intLib.ARITH_PROVE
andintLib.COOPER_PROVE
are failing to prove certain goals, even though it seems like they should be able to handle them.Here are a few examples where they succeed:
And here are a couple of examples where they fail:
Here's the failure message, which is similar for both failures:
All of the above is valid for
COOPER_PROVE
as well.I'm assuming this is a different issue than #1203 due to having a very different error message and due to the fact that
COOPER_PROVE
succeeds in #1203, but here it fails.Unfortunately, this prevents HolSmt from replaying some Z3 proofs.
The text was updated successfully, but these errors were encountered: