OpenTheory issues after moving some definitions and theorems into realaxTheory

[binghe]

Hi,

I'm sorry to report that, the OpenTheory packages (in particular, hol-real) built after #1043 (the new REAL_ARITH_TAC) now have a lot of leaking assumptions not covered by OpenTheory base package and hol-base et al.. Note that this was only caused by my willing of using REAL_ARITH in realScript.sml, in which many definitions and theorems have to be moved to realaxScript.sml which is (by design) not included in OT packages. Actually I was trying to fix this issue when I saw the OT building failure of $(HOLDIR)/src/real/prove_real_assumsScript.sml but apparently my fixes are not correct: indeed I have proved all leaking assumptions, but it seems that the logical constants (mostly real operators) in these assumptions are not the correct one. Below is the error output when installing the current hol-real:

opentheory install --reinstall hol4-real.thy
uninstalled package hol-real-1.2
WARNING: 7 axioms:
  |- realax.real_0 = 0
  |- realax.real_1 = 1
  |- realax.inv 0 = 0
  |- !x y. realax./ x y = x * realax.inv y
  |- prove_real_assums.real_of_num 0 = realax.real_0 /\
     !n.
       prove_real_assums.real_of_num (suc n) =
       prove_real_assums.real_of_num n + realax.real_1
  |- 0 = realax.real_0 /\
     !n. fromNatural (suc n) = fromNatural n + realax.real_1
  |- !x. ~(x = 0) ==> realax.inv x * x = 1
WARNING: redundant show: "Data.List"
WARNING: 2 ungrounded external constants: prove_real_assums.real_of_num realax./
WARNING: 51 unsatisfied assumptions:
  |- !x. ~(x < x)
  |- 0 < 1
  |- 0 <= 1
  |- !n. 0 <= fromNatural n
  |- ~(1 = 0)
  |- !n. 0 < fromNatural (suc n)
  |- !n. abs (fromNatural n) = fromNatural n
  |- !x. 0 <= x * x
  |- !x. x + 0 = x
  |- !x. prove_real_assums.real_of_num 0 + x = x
  |- !x. x ^ 0 = prove_real_assums.real_of_num 1
  |- !x. x * 0 = 0
  |- !x. x + ~x = 0
  |- !x. 0 * x = 0
  |- !x. ~x + x = prove_real_assums.real_of_num 0
  |- !x. x * 1 = x
  |- !x. prove_real_assums.real_of_num 1 * x = x
  |- !y x. x < y <=> ~(y <= x)
  |- !x y. x <= y <=> ~(y < x)
  |- !x. 0 <= x \/ 0 <= ~x
  |- !x. ~x < 0 <=> 0 < x
  |- !x n. fromNatural x ^ n = fromNatural (x ^ n)
  |- !m n.
       prove_real_assums.real_of_num m =
       prove_real_assums.real_of_num n <=> m = n
  |- !x. abs x = if prove_real_assums.real_of_num 0 <= x then x else ~x
  |- !x y. x < x + y <=> 0 < y
  |- !x y. x <= x + y <=> 0 <= y
  |- !x y. 0 < x - y <=> y < x
  |- !x y. 0 <= x - y <=> y <= x
  |- !x y. x - y = 0 <=> x = y
  |- !n. ~(fromNatural n = 0) <=> 0 < fromNatural n
  |- !x y. x = y \/ x < y \/ y < x
  |- !x y. x <= ~y <=> x + y <= 0
  |- !x y. ~x <= y <=> 0 <= x + y
  |- !x y. x + y = 0 <=> x = ~y
  |- !x y. x + y = 0 <=> y = ~x
  |- !x y z. y < z ==> x + y < x + z
  |- !x y z. x < y /\ y < z ==> x < z
  |- !x.
       ~(x = prove_real_assums.real_of_num 0) ==>
       inv x * x = prove_real_assums.real_of_num 1
  |- !x. x = 0 \/ 0 < x \/ 0 < ~x
  |- !x y. ~(y = prove_real_assums.real_of_num 0) ==> x / y = x * inv y
  |- !x y. x * y = 0 <=> x = 0 \/ y = 0
  |- !x y. 0 < x /\ 0 < y ==> 0 < x * y
  |- !x y. 0 < x /\ 0 < y ==> 0 < x + y
  |- !x y. 0 < x /\ 0 <= y ==> 0 < x + y
  |- !x y.
       prove_real_assums.real_of_num 0 <= x /\
       prove_real_assums.real_of_num 0 <= y ==>
       prove_real_assums.real_of_num 0 <= x * y
  |- !x y. 0 <= x /\ 0 < y ==> 0 < x + y
  |- !x y. 0 <= x /\ 0 <= y ==> 0 <= x + y
  |- (!x. x ^ 0 = 1) /\ !x n. x ^ suc n = x * x ^ n
  |- (!x. ~x = ~1 * x) /\ !x y. x - y = x + ~1 * y
  |- !P.
       (!x. P x ==> 0 < x) /\ (?a. P a) /\ (?z. !x. P x ==> x < z) ==>
       ?s. !y. (?x. P x /\ y < x) <=> y < s
  |- (!x y z. x + (y + z) = x + y + z) /\ (!x y. x + y = y + x) /\
     (!x. 0 + x = x) /\ (!x y z. x * (y * z) = x * y * z) /\
     (!x y. x * y = y * x) /\ (!x. 1 * x = x) /\ (!x. 0 * x = 0) /\
     (!x y z. x * (y + z) = x * y + x * z) /\ (!x. x ^ 0 = 1) /\
     !x n. x ^ suc n = x * x ^ n

I believe the potential fixes to this issue should involve only small changes at the beginning of prove_real_assumsScript.sml, because I do have all the "proofs" of the above assumptions, each represent one definition/theorem newly moved into realaxTheory. Let's keep this issue recorded and close it once it's fixed. (I apologize for bringing this extra issue, which can be prevented if I didn't insist on a "perfect" port of REAL_ARITH fully aligned with HOL-Light).

P. S. Perhaps another easier solution is to create a new theory between realaxTheory and realTheory, and this new theory will be included in the OT package hol-real (just like they were still in realTheory), but I think this solution should be considered as a "dirty trick" for non-OT builds and users, and thus not considered currently.

Regards,

Chun Tian

[binghe]

From the error messages it seems that OpenTheory's fromNatural should be the same thing as HOL4's real_of_num. Currently they are not mapped correctly.

[binghe]

There are also 2 irrelevant unsatisfied assumptions when installing hol-ring. Don't know which recent changes caused them but should be easy to fix:

opentheory install --reinstall hol4-ring.thy
uninstalled package hol-ring-1.2
WARNING: 2 unsatisfied assumptions:
  |- ~(ternaryComparisons.EQUAL = ternaryComparisons.LESS)
  |- ~(ternaryComparisons.GREATER = ternaryComparisons.EQUAL)

[binghe]

Q: What's the difference between "skipthm" and "delproof" in *.otd files?

A (Ramana Kumar): They are orthogonal. looks like skipthm takes the theorem out of the exports, whereas delproof makes the theorem appear as if an axiom. i.e., makes it one of the imports

https://github.com/HOL-Theorem-Prover/HOL/blob/d63dce1e16f961fc3b1e608fe90c03fbcb225982/src/opentheory/postbool/loggingHolKernel.sml#L25

[binghe]

I'm glad to report that this issue has been fixed. Now I'm doing the whole build testing, will submit a PR soon.