From e1813ffa1fa7611203ed730c8fafc942ccf9404a Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 3 Oct 2023 15:55:36 +1100 Subject: [PATCH] Fix simplification of real$NUM_CEILING Closes #1149 --- src/real/realSimps.sml | 22 ++++++++++-- src/real/selftest.sml | 82 +++++++++++++++++++++++------------------- 2 files changed, 65 insertions(+), 39 deletions(-) diff --git a/src/real/realSimps.sml b/src/real/realSimps.sml index d81303ca78..b82b25ce58 100644 --- a/src/real/realSimps.sml +++ b/src/real/realSimps.sml @@ -19,7 +19,7 @@ val arith_ss = boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ numSimps.ARITH_ss ++ val SSFRAG = simpLib.register_frag o simpLib.SSFRAG -val real_SS = simpLib.SSFRAG +val real_SS = SSFRAG {name = SOME"real", ac = [], congs = [], @@ -65,7 +65,7 @@ val real_SS = simpLib.SSFRAG "REAL_MAX_REFL", "REAL_LE_MAX1", "REAL_LE_MAX2", "REAL_MAX_ADD", "REAL_MAX_SUB"]}; -val real_ac_SS = simpLib.SSFRAG { +val real_ac_SS = SSFRAG { name = SOME"real_ac", ac = [(SPEC_ALL REAL_ADD_ASSOC, SPEC_ALL REAL_ADD_SYM), (SPEC_ALL REAL_MUL_ASSOC, SPEC_ALL REAL_MUL_SYM)], @@ -229,9 +229,25 @@ val m = mk_var("m", numSyntax.num) fun to_numeraln th = INST [n |-> mk_comb(numSyntax.numeral_tm, n), m |-> mk_comb(numSyntax.numeral_tm, m)] th +val ltnb12 = TAC_PROOF(([], “0 < NUMERAL (BIT1 n) /\ 0 < NUMERAL (BIT2 n)”), + REWRITE_TAC[arithmeticTheory.NUMERAL_DEF, + arithmeticTheory.BIT1, + arithmeticTheory.BIT2, + arithmeticTheory.ADD_CLAUSES, + prim_recTheory.LESS_0]) +val let_id = TAC_PROOF(([], “LET (\n. n) x = x”), + SIMP_TAC boolSimps.bool_ss [LET_THM]) + val op_rwts = - [to_numeraln mult_ints, to_numeraln add_ints, flr, NUM_CEILING_NUM_FLOOR, + [to_numeraln mult_ints, to_numeraln add_ints, flr, REAL_DIV_LZERO, REAL_NEGNEG] @ + (transform [(x,posneg)] $ SPEC x NUM_CEILING_NUM_FLOOR) @ + (transform [(x,posneg), (y,nb12)] ( + SPEC (mk_div(x,y)) NUM_CEILING_NUM_FLOOR) + |> map (SIMP_RULE arith_ss [REAL_LE_LDIV_EQ, REAL_LT, REAL_LE, + REAL_MUL_LZERO, REAL_NEG_LE0, + ltnb12, flr, let_id])) @ + transform [(x,posneg0)] (SPEC_ALL REAL_ADD_LID) @ transform [(x,posneg)] (SPEC_ALL REAL_ADD_RID) @ transform [(x,posneg0)] (SPEC_ALL REAL_MUL_LZERO) @ diff --git a/src/real/selftest.sml b/src/real/selftest.sml index 91ef4996fe..4562ab3d1a 100644 --- a/src/real/selftest.sml +++ b/src/real/selftest.sml @@ -11,43 +11,57 @@ val REAL_ARITH1 = RealArith.REAL_ARITH; (* The new port, also suppports rational coefficients *) val REAL_ARITH2 = RealField.REAL_ARITH; -val s = SIMP_CONV (bossLib.std_ss ++ REAL_REDUCE_ss) [] +val s = SIMP_CONV (bossLib.std_ss ++ REAL_REDUCE_ss) [LET_THM] -fun test (problem, result) = let +fun test conv nm (problem, result) = let val t2s = trace ("Unicode", 0) term_to_string - val padr = StringCvt.padRight #" " - val padl = StringCvt.padLeft #" " - val p_s = padr 30 (t2s problem) - val r_s = padl 10 (t2s result) - val _ = tprint (p_s ^ " = " ^ r_s) - val th = QCONV s problem - val answer = rhs (concl th) in - if aconv answer result then OK() - else die ("FAILED!\n Got "^term_to_string answer) + convtest("[" ^ nm ^ "] " ^ t2s problem ^ " = " ^ t2s result, + conv, problem, result) end; -val tests = [(``~~3r``, ``3r``), - (``3r + 4``, ``7r``), - (``3 - 4r``, ``~1r``), - (``abs (~20r)``, ``20r``), - (``abs (1/6)``, ``1/6``), - (``abs (~3/6)``, ``1/2``), - (``abs 0``, ``0``), - (``3r * 3/4``, ``9/4``), - (``6/~8``, ``~3/4``), - (``1/3 + 1/2``, ``5/6``), - (``1/2 = 0``, ``F``), - (``0 + 3r``, ``3r``), - (``3r * 0``, ``0r``), - (``~0r``, ``0r``), - (``1r - 0``, ``1r``), - (``1 / 10 + 0r``, ``1r/10``), - (``0r + 1 / 10``, ``1r/10``), - (``1/2 * 0r``, ``0r``), - (``0r * 1/2``, ``0r``)] - -val _ = List.app test tests +val real_reduce_simp_tests = [ + (“~~3r” , “3r”), + (“3r + 4” , “7r”), + (“3 - 4r” , “~1r”), + (“abs (~20r)” , “20r”), + (“abs (1/6)” , “1/6”), + (“abs (~3/6)” , “1/2”), + (“abs 0” , “0”), + (“3r * 3/4” , “9/4”), + (“6/~8” , “~3/4”), + (“1/3 + 1/2” , “5/6”), + (“1/2 = 0” , “F”), + (“0 + 3r” , “3r”), + (“3r * 0” , “0r”), + (“~0r” , “0r”), + (“1r - 0” , “1r”), + (“1 / 10 + 0r” , “1r/10”), + (“0r + 1 / 10” , “1r/10”), + (“1/2 * 0r” , “0r”), + (“0r * 1/2” , “0r”), + (“flr 10” , “10n”), + (“clg 12” , “12n”), + (“flr (1/10)” , “0n”), + (“clg (1/10)” , “1n”), + (“flr (131/10)”, “13n”), + (“clg (131/10)”, “14n”), + (“flr (-2/4)” , “0n”), + (“clg (-2/4)” , “0n”) +] + +val _ = List.app (test s "simp") real_reduce_simp_tests +val _ = List.app (test EVAL "EVAL") real_reduce_simp_tests + +fun isunch UNCHANGED = true | isunch _ = false +val _ = List.app (shouldfail {testfn = s, printresult = thm_to_string, + printarg = fn t => "Testing SIMP_CONV “" ^ + term_to_string t ^ + "” raises UNCHANGED", + checkexn = isunch}) + [“flr x”, “clg x”, “flr (10/x)”, “clg (10/x)”, + “flr (-x/5)”, “clg(-x/5)”] + val _ = List.app (fn (s1,s2) => tpp_expected @@ -55,10 +69,6 @@ val _ = List.app [("realinv 2", "2⁻¹"), ("inv (TC R)", "R⁺ ᵀ")] val _ = tpp "¬p ∧ q" (* UOK *) -fun UNCH_test (n,c,t) = - shouldfail {checkexn = fn Conv.UNCHANGED => true | _ => false, - printarg = fn t => "UNCHANGED " ^ n ^ ": " ^ term_to_string t, - printresult = thm_to_string, testfn = c} t fun nftest (r as (n,c,t1,t2)) = let fun test (t1,t2) = (Exn.capture c t1, Exn.capture c t2)