Fixed OpenTheory build issues (#1045) introduced in #1043

[binghe]

Hi,

this PR fixes the OpenTheory build issues described in #1045, i.e. a lot of leaking assumptions when installing hol-real. As I mentioned in #1045, these issues were introduced when I was moving some real theorems from realTheory to realaxTheory but realaxTheory is not included in the "hol-real" OT package.

The key of my current solution is to build realax.ot.art and include it in "hol-real" OT package. Only in this way, I don't need to copy a large piece of code from realaxScript.sml to prove_real_assumsScript.sml and the number of real assumptions can also be minimized (from 76 back to 21, the same as before #1043).

Let's recall why previously realaxTheory was excluded from hol-real: that's because realaxTheory contains a lot of treal and hreal theorems and the higher order quotient from treal/hreal to the final real type, and these theorems shouldn't be included in OT articles because HOL4 wants to use OpenTheory's own real package as the basis of real numbers, and the bridge is done by $(HOLDIR)/src/prove_real_assumsScript.sml.

So, I did two things to realaxScript.sml: first, I move all HREAL and TREAL theorems to the upstream hrealTheory; this should be fine as nobody except realax itself should use any of these theorems. Second, I created a big realax.otd where I carefully eliminated all theorems irrelevant with the OT exports. In another word, all theorems using hreal and treal stuff are either skipped or with proofs deleted in the final realax.ot.art. (the movements of HREAL and TREAL theorems actually makes realax.otd shorter, because otherwise also these theorems must be explicitly excluded.)

Once realax.ot.art is ready, in $(HOLDIR)/src/prove_real_assumsScript.sml I recovered the old, shorter contents of this file (before #1043) but still keep my other improvements to this file (i.e. reading axioms from OT real-1.61 and only use them to prove other assumptions.). Now prove_real_assumsScript.sml is as short as before, and more importantly, in the future, if more (or less) theorems were moved from realTheory to realaxTheory (because RealAirth needs it, maybe), no further changes are required in prove_real_assumsScript.sml.

P. S. in ternaryComparisonsTheory I added the following two new theorems to handle the leaking assumptions when installing hol-ring, since I failed to find where these two theorems were actually used:

   [ordering_distinct1]  Theorem      
      ⊢ EQUAL ≠ LESS
   
   [ordering_distinct2]  Theorem      
      ⊢ GREATER ≠ EQUAL

Regards,

Chun Tian

[binghe]

For the first time, prove_real_assumsScript.sml are fully commented and I'm glad to say that I finally understood every line in this file and the idea (of Ramana Kumar @xrchz) behind them. For example, why at the beginning we have the following "strange" definitions:

val REAL_0 = new_definition("REAL_0",concl realaxTheory.REAL_0);
val REAL_1 = new_definition("REAL_1",concl realaxTheory.REAL_1);

Now I have left the following comments for future maintainers:

(* NOTE: the purpose of the following two definitions is to replace HOL4's
   "invalid" definitions of “real_0” and “real_1” (in realaxTheory), from

   |- real_0 = real_ABS treal_0
   |- real_1 = real_ABS treal_1

   to

   |- real_0 = real_of_num 0
   |- real_1 = real_of_num 1

   where “real_of_num” (Number.Real.fromNatural) is provided by OT's real-1.61.
  (In HOL4, “real_0|1” are more primitive and “real_of_num” is defined upon
  “real_0|1”. In OpenTheory, on the other hand, there's no “real_0|1” at all,
   while Number.Real.fromNatural is defined in a completely different way.)

   For this purpose, the existing constants “real_0” and “real_1” defined in
   realaxTheory must be deleted when exporting OT articles (by the following
   two lines in realax.otd):

   delconst real_0
   delconst real_1

   Furthermore, when reading OT articles generated by HOL4, all occurrences of
  “realax$real_0” and “realax$real_1” must be redirected to the new definitions
   here. This is done by the ML function "const_name" (below), having the
   following two lines:

   | const_name (["HOL4","realax"],"real_0") = {Thy=Thy,Name="real_0"}
   | const_name (["HOL4","realax"],"real_1") = {Thy=Thy,Name="real_1"}

   Finally, all occurrences of “real_of_num” in the present theory will be
   also replaced by Number.Real.fromNatural. This is done by the following
   line in $(HOLDIR)/src/opentheory/hol4.int:

   const "HOL4.realax.real_of_num" as "Number.Real.fromNatural"

 *)

[binghe]

Now realaxScript.sml begins by calling quotient.define_equivalence_type to define the "real" type, and then the proof of a set of "primitive" real theorems just enough for RealArith package. All internal TREAL and HREAL theorems for only the construction of real numbers are now moved to upstream theorems, mostly in hrealTheory.

For user code who was opening realaxTheory, this may sound like an incompatible change but I believe actually nobody (should) use any of those TREAL and HREAL intermediate theorems.

[xrchz]

Bravo. Thanks for doing all this and sorry my contributions weren't more easily decipherable.

[binghe]

Bravo. Thanks for doing all this and sorry my contributions weren't more easily decipherable.

You're welcome (and thanks for your answers to all my related questions, mostly in private).

[binghe]

A new build of hol4-large-numbers.art (version 1.1) is available at https://www.dropbox.com/s/swgbu6bf1fehz7h/hol4-large-numbers-1.1.7z?dl=0

Some statistics:

Inference rules:
eqMp ............... 6,103,723
subst .............. 5,161,610
deductAntisym ...... 4,954,952
appThm ............. 1,378,873
betaConv ............. 633,396
absThm ............... 419,549
trans ................ 399,090
refl ................. 206,824
sym .................. 173,061
assume ............... 140,427
proveHyp .............. 14,509
defineConst ............ 1,075
defineConstList ........... 72
defineTypeOp .............. 23
axiom ...................... 3
Total ............. 19,587,187

[mn200]

Sorry to have left this so long!

[binghe]

Sorry to have left this so long!

It's OK (except that I was a little worry about your safety (and my future) ^_^)