Comments (5)
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``;
from hol.
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``;
from hol.
Goals containing quot
or rem
also fail (even though the same goals containing /
and %
succeed), e.g.:
> intLib.ARITH_PROVE ``x quot 42 <= ABS x``;
> intLib.ARITH_PROVE ``x rem 42 < 42``;
If I get rid of the quot
and rem
symbols with rw[int_quot, int_rem]
then the goals can be proved (in these cases).
from hol.
So these are interesting; thanks! The &(x - x) = 0i
is caused by the fact that the procedure doesn't think to try to distribute the &
s over the subtraction. That's easy to fix (see 1a1b46d). Others will require a bit more thought and investigation into how normalisation is happening.
from hol.
@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!
from hol.
Related Issues (20)
- Limits on the number of jobs for Holmake? HOT 2
- SAT_ORACLE gives wrong answers HOT 11
- "intLib.ARITH_PROVE ``0n = x * Num 0i``" fails unexpectedly HOT 1
- intLib.ARITH_PROVE raises exception `NotFound` HOT 1
- Ignore assumption directive for simplifier
- Add spec form to cover both `INST` and `SPEC` of theorems
- Add a q.subpat_{x_,}assum
- A broken generated HTML theory in non-Unicode mode HOT 2
- Moscow ML builds broken after `cv_translator` HOT 1
- General modern "quotation" syntax support
- Q.PAT_X_ASSUM returns bad errors
- C++ compilation failure of `src/HolSat/sat_solvers/zc2hs` on macOS HOT 4
- Fix intLib to avoid noisy output HOT 1
- Unexpected error with `DefnBase.one_line_ify`
- add patCases_on tactic
- reorder and rename quantifiers by specifying pattern(s) underneath HOT 1
- case_pred_disj_of ``:'a # 'b`` fails
- EVAL monitoring should be able to stop the computation HOT 3
- Error trying to build on MacOs HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from hol.