search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
606 stars 132 forks source link

intLib.ARITH_PROVE raises exception `NotFound` #1209

Closed someplaceguy closed 3 months ago

someplaceguy commented 3 months ago

The following expression unexpectedly raises a NotFound exception:

> intLib.ARITH_PROVE ``x (0i) + 0 % 5 = 0i``;
Exception- NotFound raised

I wouldn't expect it to prove the provided term, but usually when such procedures fail they raise a HOL_ERR exception (so I assume this is a bug?).

someplaceguy commented 3 months ago

BTW, I forgot to mention: interestingly, if I change the 5 to a 4, then it raises a HOL_ERR exception as expected:

> intLib.ARITH_PROVE ``x (0i) + 0 % 4 = 0i``;
Exception-
   HOL_ERR
     {message =
      "Tried to prove generalised goal (generalising x 0...) but it was false",
      origin_function = "OMEGA_CONV", origin_structure = "IntDP_Munge"}
   raised