From e9cc653573bfdddc60d8585834cbb67bcfec723d Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 23 Jan 2024 15:43:06 +0000
Subject: [PATCH] HolSmt: remove unneeded proof and reenable more tests

It turns out that goals containing `int_min` and `int_max` were already being
rewritten into something that SMT-LIB can handle, so we can enable more tests
for cvc5 and Z3, including Z3 with proof reconstruction.
---
 src/HolSmt/SmtLib.sml   |  8 +++++---
 src/HolSmt/selftest.sml | 16 ++++++++--------
 2 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/HolSmt/SmtLib.sml b/src/HolSmt/SmtLib.sml
index 515fcc2912..2f69cc3f4b 100644
--- a/src/HolSmt/SmtLib.sml
+++ b/src/HolSmt/SmtLib.sml
@@ -567,13 +567,15 @@ in
   fun SIMP_TAC simp_let =
     let
       open Tactical simpLib
-      val INT_ABS = intLib.ARITH_PROVE
-                      ``!x. ABS (x:int) = if x < 0i then 0i - x else x``
+      (* TODO: In the future it'd probably be better to translate the
+         definitions of `ABS`, `int_min`, `int_max`, etc, or any other needed
+         user-defined functions automatically and pass those on to the SMT
+         solver, instead of doing these special-case rewrites here. *)
     in
       REPEAT Tactic.GEN_TAC THEN
       (if simp_let then Library.LET_SIMP_TAC else ALL_TAC) THEN
       SIMP_TAC pureSimps.pure_ss
-        [integerTheory.INT_MIN, integerTheory.INT_MAX, INT_ABS] THEN
+        [integerTheory.INT_MIN, integerTheory.INT_MAX, integerTheory.INT_ABS] THEN
       Library.WORD_SIMP_TAC THEN
       Library.SET_SIMP_TAC THEN
       Tactic.BETA_TAC
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 86c8191def..8841a4a104 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -415,18 +415,18 @@ in
     (``ABS (ABS (x:int)) = ABS x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
     (``ABS (x:int) = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
 
-    (``int_min (x:int) y <= x``, [thm_AUTO, thm_YO]),
-    (``int_min (x:int) y <= y``, [thm_AUTO, thm_YO]),
-    (``(z:int) < x /\ z < y ==> z < int_min x y``, [thm_AUTO, thm_YO]),
+    (``int_min (x:int) y <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``int_min (x:int) y <= y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(z:int) < x /\ z < y ==> z < int_min x y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``int_min (x:int) y < x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``int_min (x:int) 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:int) >= 0 ==> (int_min x 0 = 0)``, [thm_AUTO, thm_YO]),
+    (``(x:int) >= 0 ==> (int_min x 0 = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``int_max (x:int) y >= x``, [thm_AUTO, thm_YO]),
-    (``int_max (x:int) y >= y``, [thm_AUTO, thm_YO]),
-    (``(z:int) > x /\ z > y ==> z > int_max x y``, [thm_AUTO, thm_YO]),
+    (``int_max (x:int) y >= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``int_max (x:int) y >= y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(z:int) > x /\ z > y ==> z > int_max x y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``int_max (x:int) y > x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:int) >= 0 ==> (int_max x 0 = x)``, [thm_AUTO, thm_YO]),
+    (``(x:int) >= 0 ==> (int_max x 0 = x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (* real *)