intLib.{ARITH,COOPER}_PROVE can't prove certain goals

[someplaceguy]

I'm running into an issue where both intLib.ARITH_PROVE and intLib.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:

> intLib.ARITH_PROVE ``x - x = 0n``;
> intLib.ARITH_PROVE ``x - &a <= (x:int)``;
> intLib.ARITH_PROVE ``x - a <= (x:num)``;

And here are a couple of examples where they fail:

> intLib.ARITH_PROVE ``&(x - x) = 0i``;
> intLib.ARITH_PROVE ``&(x - a) <= ((&x) : int)``;

Here's the failure message, which is similar for both failures:

Exception-
   HOL_ERR
     {message =
      "Tried to prove generalised goal (generalising &(x - a)...) but it was false",
      origin_function = "OMEGA_CONV", origin_structure = "IntDP_Munge"}
   raised

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.

[someplaceguy]

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``;

[someplaceguy]

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``;

[someplaceguy]

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).

[mn200]

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 1a1b46d9be). Others will require a bit more thought and investigation into how normalisation is happening.

[someplaceguy]

@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!