Skip to content

Commit

Permalink
HolSmt: try harder to replay arithmetic proof steps
Browse files Browse the repository at this point in the history 
This commit adds some tactics which help prove some arithmetic proof
steps that intLib.{ARITH,COOPER}_TAC can't deal with.

These are basically some workarounds for:

HOL-Theorem-Prover#1207

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).

That said, I don't expect these workarounds to be very reliable.

Ideally, it would be better to improve HOL4's linear arithmetic
decision procedures.
  • Loading branch information
@someplaceguy
someplaceguy committed Mar 12, 2024
1 parent 5db3618 commit 351fe74
Show file tree
Hide file tree
Showing 2 changed files with 72 additions and 60 deletions.
16 changes: 14 additions & 2 deletions src/HolSmt/Z3_ProofReplay.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ local

open Z3_Proof

val op ++ = bossLib.++
val op >> = Tactical.>>

val ERR = Feedback.mk_HOL_ERR "Z3_ProofReplay"
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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

(***************************************************************************)
Expand Down
116 changes: 58 additions & 58 deletions src/HolSmt/selftest.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]),
Expand All @@ -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]),
Expand All @@ -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]),
Expand Down

0 comments on commit 351fe74

Please sign in to comment.