From 60269d4a4b20564659ea8f9cf5e1aae5d35377e6 Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Sun, 17 Mar 2024 11:38:58 +0000 Subject: [PATCH] HolSmt: don't get rid of `quot` and `rem` in arithmetic rules It should not be necessary to rewrite these symbols with their definitions, because from the perspective of SMT solvers, these should just be functions like any others. Therefore, when replaying arithmetic proof steps, the proof handler should not need to understand what `quot` and `rem` are. This is a partial revert of the following commit: 6220a17848fd58bcb54bb9df9df6b55d5859abf0 It's not clear to me why I introduced this change in the first place, since the tests do work fine without it. Also, there doesn't seem to be any performance regression. --- src/HolSmt/Z3_ProofReplay.sml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml index e0195cc7d5..d6e06b5fd2 100644 --- a/src/HolSmt/Z3_ProofReplay.sml +++ b/src/HolSmt/Z3_ProofReplay.sml @@ -495,8 +495,7 @@ 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, - integerTheory.int_quot, integerTheory.int_rem] + >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT] (* if `arith_tactic` doesn't work at first, don't give up immediately; instead let's try additional tactics *) >> TRY arith_tactic