Rational number arithmetic (operations and comparisons) doesn’t EVAL

[mn200]

This is disgusting:

> EVAL ``3/4 <= 5/8:rat``;
val it =
   ⊢ 3 / 4 ≤ 5 / 8 ⇔
     ((if FST (rep_frac (rep_rat (5 / 8 − 3 / 4))) = 0 then 0
       else if FST (rep_frac (rep_rat (5 / 8 − 3 / 4))) < 0 then -1
       else 1) =
      1) ∨ (3 / 4 = 5 / 8): thm

[xqyww123]

This simple code does the calculation including comparison

local open ratTheory fracTheory
val l1 = [rat_0_def, rat_1_def, RAT_AINV_CALCULATE,
  RAT_MINV_CALCULATE, RAT_ADD_CALCULATE,
  RAT_MUL_CALCULATE, RAT_LES_CALCULATE,
  RAT_LEQ_CALCULATE, RAT_EQ_CALCULATE, RAT_SUB_ADDAINV, RAT_DIV_MULMINV]
val l2 = [FRAC_MINV_SAVE, SGN_def, FRAC_MUL_SAVE,
  FRAC_ADD_SAVE, FRAC_AINV_SAVE, FRAC_0_SAVE, FRAC_1_SAVE,
  FRAC_NMR_SAVE, FRAC_DNM_SAVE]
in 
val CALC_CONV = (SIMP_CONV int_ss [rat_cons_def, RAT_SAVE_NUM, SGN_def]
  THENC fracLib.FRAC_SAVE_CONV THENC SIMP_CONV int_ss (l1@l2) THENC
  SIMP_CONV int_ss [RAT_SAVE_TO_CONS])
end

 (* 2 / 3 * -(3 / 4) − 3 / 4 = -60 // 48 *)
CALC_CONV ``(2 /3) * -(3 / 4) - 3 / 4``
(* ⊢ 2 // 3 * -(3 // 4) ≤ 3 / 4 ⇔ T *)
CALC_CONV ``(2 //3) * -(3 // 4) <= 3 / 4``
(* ⊢ 2 // 4 = 1 // 2 ⇔ T *)
CALC_CONV `` 2 // 4 = 1 // 2``

despite it returns result in form of rat_cons (1 // 2 rather than 1 / 2, the rat_cons seems some intermediate tool) and without normalization.

My plan is to calculate the normalized result in SML and prove the equivalence of the normalization by this conversion again.

I will make it together with a simpset fragment in my rest time

[binghe]

Re Holinfo How to prove basic equivalency of rational.pdf

Here are some related email discussions in hol-info at the beginning of 2019. I want to fix the entire ratTheory with the ultimate goal to substitute the rational-related code in probability scripts (see util_probTheory.real_rat_set_def) with theorems from ratTheory.

[mn200]

The existing code in src/real might be a guide to achieving this for the rationals. There are a surprisingly large number of rewrite theorems required to capture the various combinations (negations or not; fractional or not on both sides suggests 16 theorems per binary operator).

[binghe]

The existing code in src/real might be a guide to achieving this for the rationals. There are a surprisingly large number of rewrite theorems required to capture the various combinations (negations or not; fractional or not on both sides suggests 16 theorems per binary operator).

Thanks for the hints. Let's me dig further and try to fix it.