From 84672bf05d4055b620539ab2a266979aa3d63963 Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Tue, 12 Mar 2024 12:10:32 +0000 Subject: [PATCH] HolSmt: try harder to replay arithmetic proof steps This commit adds some tactics which help prove some arithmetic proof steps that intLib.{ARITH,COOPER}_TAC can't deal with. This allows us to enable proof replay for the remaining arithmetic test cases that didn't already have proof replay enabled, with the exception of the very last test case (because we can't replay nonlinear arithmetic proof steps). --- src/HolSmt/Z3_ProofReplay.sml | 16 ++++- src/HolSmt/selftest.sml | 116 +++++++++++++++++----------------- 2 files changed, 72 insertions(+), 60 deletions(-) diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml index c3720a87e5..551ff1272b 100644 --- a/src/HolSmt/Z3_ProofReplay.sml +++ b/src/HolSmt/Z3_ProofReplay.sml @@ -13,6 +13,7 @@ local open Z3_Proof + val op ++ = bossLib.++ val op >> = Tactical.>> val ERR = Feedback.mk_HOL_ERR "Z3_ProofReplay" @@ -474,7 +475,7 @@ local let fun cooper goal = profile "arith_prove(cooper)" intLib.COOPER_TAC goal - fun tactic (goal as (_, term)) = + fun arith_tactic (goal as (_, term)) = if term_contains_real_ty term then (* this is just a heuristic - it is quite conceivable that a term that contains type real is provable by integer @@ -489,6 +490,10 @@ local handle NotFound => cooper goal handle Feedback.HOL_ERR _ => cooper goal ) + val TRY = Tactical.TRY + val ap_tactic = + TRY AP_TERM_TAC >> TRY arith_tactic + >> TRY AP_THM_TAC >> TRY arith_tactic in Tactical.prove (t, (* rewrite the `smtdiv`, `smtmod` symbols so that the arithmetic @@ -497,7 +502,14 @@ local (* the next rewrites are a workaround for this issue: https://github.com/HOL-Theorem-Prover/HOL/issues/1207 *) >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT] - >> tactic) + (* if `arith_tactic` doesn't work at first, don't give up immediately; + instead let's try additional tactics *) + >> TRY arith_tactic + >> bossLib.RW_TAC (bossLib.arith_ss ++ intSimps.INT_RWTS_ss ++ + intSimps.INT_ARITH_ss ++ realSimps.REAL_ARITH_ss) + [Conv.GSYM integerTheory.INT_NEG_MINUS1] + >> TRY arith_tactic + >> Tactical.rpt (Tactical.CHANGED_TAC ap_tactic)) end (***************************************************************************) diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index 6850d79f7b..78497977ac 100644 --- a/src/HolSmt/selftest.sml +++ b/src/HolSmt/selftest.sml @@ -358,51 +358,51 @@ in (``(x:int) * 42 = 42 * x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``(~42:int) / ~42 = 1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) / ~42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(0:int) / ~42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(1:int) / ~42 = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) / ~42 = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~42:int) / ~1 = 42``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) / ~1 = 1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), - (``(0:int) / ~1 = 0``, [thm_AUTO, (*thm_CVC*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), + (``(0:int) / ~1 = 0``, [thm_AUTO, (*thm_CVC*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(1:int) / ~1 = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) / ~1 = ~42``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~42:int) / 1 = ~42``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) / 1 = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), - (``(0:int) / 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), - (``(1:int) / 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), + (``(0:int) / 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), + (``(1:int) / 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) / 1 = 42``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~42:int) / 42 = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) / 42 = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(0:int) / 42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(1:int) / 42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) / 42 = 1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), - (``(x:int) / 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), + (``(x:int) / 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) / ~1 = ~x``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) / 42 <= x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(x:int) / 42 <= ABS x``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3_v4(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3_v4, thm_Z3p_v4]), (``((x:int) / 42 = x) = (x = 0)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(x:int) / 42 = x <=> x = 0 \/ x = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) / 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(x:int) / 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(0:int) / 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), @@ -412,64 +412,64 @@ in (* cf. integerTheory.int_div *) (``(x:int) < 0 ==> (x / 1 = ~(~x / 1) + if ~x % 1 = 0 then 0 else ~1)``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) < 0 ==> (x / 42 = ~(~x / 42) + if ~x % 42 = 0 then 0 else ~1)``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``0 <= (x:int) ==> (x / ~42 = ~(x / 42) + if x % 42 = 0 then 0 else ~1)``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``0 <= (x:int) ==> (x / ~1 = ~(x / 1) + if x % 1 = 0 then 0 else ~1)``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) < 0 ==> (x / ~42 = ~x / 42)``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) < 0 ==> (x / ~1 = ~x / 1)``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~42:int) % ~42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) % ~42 = ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(0:int) % ~42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(1:int) % ~42 = ~41``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) % ~42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~42:int) % ~1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) % ~1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(0:int) % ~1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(1:int) % ~1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) % ~1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~42:int) % 1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) % 1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), - (``(0:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), - (``(1:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), + (``(0:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), + (``(1:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) % 1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~42:int) % 42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(~1:int) % 42 = 41``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(0:int) % 42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(1:int) % 42 = 1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(42:int) % 42 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), - (``(x:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), + (``(x:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) % ~1 = 0``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) % 42 < 42``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``((x:int) % 42 = x) = (x < 42)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``((x:int) % 42 = x) <=> (0 <= x) /\ (x < 42)``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) % 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(x:int) % 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(0:int) % 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), @@ -478,13 +478,13 @@ in (* cf. integerTheory.int_mod *) (``(x:int) % ~42 = x - x / ~42 * ~42``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) % ~1 = x - x / ~1 * ~1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) % 1 = x - x / 1 * 1``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``(x:int) % 42 = x - x / 42 * 42``, - [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]), + [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]), (``ABS (x:int) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]), (``(ABS (x:int) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),