HolSmt: initial support for the exponential function

This initial support is very limited and only consists in adding a
couple of useful theorems to the proving context.

Hopefully, in the future more extensive support is implemented by
adding support for Z3's native power operator, which should allow
HolSmt to prove a lot more goals. This implementation would need to be
similar to the implementation of integer division, since it doesn't
exactly match HOL4's exponential functions.

The latter would also have a couple of limitations, namely:

1. it would only work for Z3, since this operator is a Z3 extension
and not part of the SMT-LIB standard
2. proof reconstruction would not work

Author: someplaceguy

src/HolSmt/SmtLib.sml

@@ -622,25 +622,39 @@ in
   fun SIMP_TAC simp_let =
   let
     open Tactical simpLib
-    (* TODO: In the future we should add all relevant theorems automatically,
-       either based on which symbols are used (recursively) or, perhaps more
-       simply, just translate all the theorems defined in all the theories that
-       are being used. For now we just manually add a few useful ones. *)
     val facts =
     let
-      open arithmeticTheory integerTheory
+      open arithmeticTheory integerTheory realTheory realaxTheory
     in
       if !include_theorems then [
+        (* NOTE: when adding a theorem to the list below, make sure that it
+           doesn't have any free var -- otherwise, ASSUME_TAC will specialize
+           the theorem to any free var in the goal that happens to have the same
+           name, which very often is not what is desired. As an example,
+           integerTheory's `INT_POW` should not be added -- instead, add
+           `int_exp`. If no appropriate quantified theorem is available,
+           `Drule.GEN_ALL` can be used to quantify all free vars in a theorem.
+
+           Also, make sure the theorem is really needed -- some theorems seem to
+           cause an explosion in the time needed to solve some goals, often
+           making Z3 unable to solve them -- and it's not always easy to tell a
+           priori which ones do. As an example, arithmeticTheory.EXP_1 doesn't
+           seem to cause issues, but EXP_2 prevents Z3 from solving
+           ``x DIV 42 <= x``. *)
+
         (* arithmeticTheory *)
-        GREATER_DEF, GREATER_EQ, MIN_DEF, MAX_DEF,
+        EXP, EXP_1, EXP_POS, GREATER_DEF, GREATER_EQ, MAX_DEF, MIN_DEF,
         (* integerTheory *)
         INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN, INT_OF_NUM,
         INT_POS, NUM_OF_INT, NUM_INT_MUL, NUM_INT_EDIV, NUM_INT_EMOD,
-        INT_DIV_EDIV, INT_MOD_EMOD, INT_QUOT_EDIV, INT_REM_EMOD,
+        INT_DIV_EDIV, INT_MOD_EMOD, INT_QUOT_EDIV, INT_REM_EMOD, int_exp,
+        (* realTheory *)
+        abs, POW_2, POW_ONE, REAL_POW_LT,
+        (* realaxTheory *)
+        real_max, real_min, real_pow,
         (* others *)
         int_arithTheory.INT_NUM_SUB,
-        markerTheory.Abbrev_def,
-        realaxTheory.real_min, realaxTheory.real_max, realTheory.abs
+        markerTheory.Abbrev_def
       ] else []
     end
   in

src/HolSmt/selftest.sml

@@ -105,11 +105,24 @@ fun mk_test_fun is_configured expect_fun name smt_tac =
 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_quot,
-      integerTheory.int_rem, integerTheory.EDIV_DEF, integerTheory.EMOD_DEF,
-      boolTheory.LET_THM]
-      t
+    val simp_thms =
+    let
+      open arithmeticTheory integerTheory realTheory
+    in
+      [
+        (* arithmeticTheory *)
+        EXP, EXP_1, EXP_2,
+        (* integerTheory *)
+        EDIV_DEF, EMOD_DEF, INT_ABS, INT_MAX, INT_MIN, int_exp, int_quot,
+        int_rem,
+        (* realTheory *)
+        EXP_2, POW_2, REAL_POW_LT,
+        (* others *)
+        boolTheory.LET_THM
+      ]
+    end
+    val t_eq_t' =
+      simpLib.SIMP_CONV simpset simp_thms t
       handle Conv.UNCHANGED =>
         Thm.REFL t
     val t' = boolSyntax.rhs (Thm.concl t_eq_t')
@@ -252,15 +265,15 @@ in
       [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``SUC (x + y) = (SUC x + SUC y)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
 
-    (``(x:num) + 0 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:num) + 0 = x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``0 + (x:num) = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
-    (``(x:num) + y = y + x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:num) + y = y + x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:num) + (y + z) = (x + y) + z``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``((x:num) + y = 0) <=> (x = 0) /\ (y = 0)``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
-    (``(x:num) - 0 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:num) - 0 = x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:num) - y = y - x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:num) - y - z = x - (y + z)``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
@@ -317,6 +330,22 @@ in
     (``((x:num) = x DIV 42 * 42 + x MOD 42) /\ x MOD 42 < 42``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
+    (``(x:num) ** 0 = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``(x:num) ** 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:num) ** 1 = x``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``(0:num) ** 1 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(1:num) ** x = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``(1:num) ** x = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:num) ** 2 = x * x``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(x:num) ** 2 = 2``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:num) ** 3 = x * x * x``, [(*thm_AUTO, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(x:num) ** 3 = 4``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 < (x:num) ** y``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 <= (x:num) ** y``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``0 < (1:num) ** y``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``0 < (2:num) ** y``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p]),
+    (``0 < (42:num) ** y``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p]),
+
     (``MIN (x:num) y <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``MIN (x:num) y <= y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(z:num) < x /\ z < y ==> z < MIN x y``,
@@ -581,6 +610,28 @@ in
     (``(x:int) rem 42 = x - x quot 42 * 42``,
       [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
 
+    (``(x:int) ** 0 = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``(x:int) ** 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) ** 1 = x``, [(*thm_AUTO, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(0:int) ** 1 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(1:int) ** x = 1``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(1:int) ** x = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(-1:int) ** 1 = -1``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(-1:int) ** 2 = 1``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(-3:int) ** 1 = -3``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(-3:int) ** 2 = 9``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(x:int) ** 2 = x * x``, [(*thm_AUTO, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(x:int) ** 2 = 2``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) ** 3 = x * x * x``, [(*thm_AUTO, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(x:int) ** 3 = 4``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 < (x:int) ** y``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 <= (x:int) ** y``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 < (1:int) ** y``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``0 < (2:int) ** y``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``0 < (-2:int) ** y``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 < (42:int) ** y``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``0 < (-42:int) ** y``, [sat_CVC, sat_Z3, sat_Z3p]),
+
     (``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]),
     (``(x:int) >= 0 ==> (ABS x = x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
@@ -631,6 +682,26 @@ in
     (``x < 0 ==> (x:real) / 42 > x``,
       [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
 
+    (``(x:real) pow 0 = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``(x:real) pow 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:real) pow 1 = x``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(0:real) pow 1 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(1:real) pow x = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``(1:real) pow x = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(-1:real) pow 1 = -1``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(-1:real) pow 2 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p]),
+    (``(-3:real) pow 1 = -3``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``(-3:real) pow 2 = 9``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p]),
+    (``(x:real) pow 2 = x * x``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p]),
+    (``(x:real) pow 3 = x * x * x``, [thm_AUTO(*, thm_CVC, thm_Z3, thm_Z3p*)]),
+    (``0 < (x:real) pow y``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 <= (x:real) pow y``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 < (1:real) pow y``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``0 < (2:real) pow y``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``0 < (-2:real) pow y``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``0 < (42:real) pow y``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+    (``0 < (-42:real) pow y``, [sat_CVC, sat_Z3, sat_Z3p]),
+
     (``abs (x:real) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(abs (x:real) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:real) >= 0 ==> (abs x = x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),