From 6220a17848fd58bcb54bb9df9df6b55d5859abf0 Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Thu, 14 Mar 2024 16:13:25 +0000 Subject: [PATCH] HolSmt: replay goals containing `quot` and `rem` HOL4's integer arithmetic decision procedures cannot handle `quot` and `rem`, so proof steps containing these symbols were failing to replay. This commit rewrites goals containing these symbols to increase the chances of a successful replay. `thm_AUTO` was similarly improved, as it had the same limitation and was failing to prove some of the self-tests. --- src/HolSmt/Z3_ProofReplay.sml | 3 ++- src/HolSmt/selftest.sml | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml index d6e06b5fd2..e0195cc7d5 100644 --- a/src/HolSmt/Z3_ProofReplay.sml +++ b/src/HolSmt/Z3_ProofReplay.sml @@ -495,7 +495,8 @@ local PURE_REWRITE_TAC[integerTheory.EDIV_DEF, integerTheory.EMOD_DEF] (* 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] + >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT, + integerTheory.int_quot, integerTheory.int_rem] (* if `arith_tactic` doesn't work at first, don't give up immediately; instead let's try additional tactics *) >> TRY arith_tactic diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index e32a7310dd..5eb06b9b85 100644 --- a/src/HolSmt/selftest.sml +++ b/src/HolSmt/selftest.sml @@ -106,7 +106,8 @@ fun auto_tac (_, t) = let val simpset = bossLib.++ (bossLib.srw_ss (), wordsLib.WORD_ss) val t_eq_t' = simpLib.SIMP_CONV simpset [integerTheory.INT_ABS, - integerTheory.INT_MAX, integerTheory.INT_MIN] + integerTheory.INT_MAX, integerTheory.INT_MIN, integerTheory.int_quot, + integerTheory.int_rem] t handle Conv.UNCHANGED => Thm.REFL t