someplaceguy
commented
1 month ago FYI, as a curiosity, this week I was playing around with proving some theorems and I came across an interesting example where HolSmt was able to prove a goal much more easily than what I could do manually with metis_tac, ARITH_TAC, rw and friends.
Namely, I had defined this recursive function:
Definition n_trits_def:
n_trits n = if n < 3 then 1n else 1 + n_trits (n DIV 3)
EndAnd I wanted to prove this theorem: (n <> 0 /\ n_trits n = k) <=> (3 ** (k - 1) <= n /\ n < 3 ** k).
At first, I proved the theorem without HolSmt, which came out like this (please don't judge :sweat_smile:):
Theorem n_trits_bounds:
(n <> 0 /\ n_trits n = k) <=> (3 ** (k - 1) <= n /\ n < 3 ** k)
Proof
qid_spec_tac `n`
>> Induct_on `k`
>> rw[Once n_trits_def]
>- (
EQ_TAC
>> rw[]
>- (
`1 <= 3 ** k` by rw[]
>> rw[]
)
>> `3 ** k < 3 ** 1` by metis_tac[LESS_EQ_LESS_TRANS, EXP_1]
>> fs[]
)
>> last_x_assum $ qspec_then `n DIV 3` assume_tac
>> EQ_TAC
>- (
strip_tac
>> `n_trits (n DIV 3) = k` by rw[]
>> `n DIV 3 <> 0` by rw[DIV_EQ_0]
>> conj_tac
>- (
`(3 ** SUC (k - 1)) <= (n DIV 3) * 3` by rw[EXP]
>> Cases_on `k = 0`
>- rw[]
>> metis_tac[num_CASES, SUC_SUB1, LESS_EQ_TRANS, DIV_MULT_LE, DECIDE ``0 < 3``]
)
>> metis_tac[EXP, DIV_LT_X, DECIDE ``0 < 3``, MULT_COMM]
)
>> rw[]
>> `n_trits (n DIV 3) = k` suffices_by rw[]
>> Cases_on `k = 0`
>- fs[]
>> `?p. k = SUC p` by metis_tac[num_CASES]
>> `k - 1 = p` by rw[]
>> fs[]
>> `(3 ** SUC p) DIV 3 <= n DIV 3` by ARITH_TAC
>> metis_tac[EXP, MULT_COMM, MULT_DIV, DIV_LT_X, DECIDE ``0 < 3``]
QEDI'm sure this could be greatly improved and simplified (perhaps with recInduct?), especially for someone with more expertise, but to be honest I didn't want to spend more effort on this.
When I attempted to prove this theorem with HolSmt I only needed the following:
Theorem n_trits_bounds:
(n <> 0 /\ n_trits n = k) <=> (3 ** (k - 1) <= n /\ n < 3 ** k)
Proof
qid_spec_tac `n`
>> Induct_on `k`
>> rw[Once n_trits_def]
>> z3o_tac[]
QEDNote:
- This is not really representative of HolSmt's performance, it's just the most extreme example I ran into so far (excluding the HolSmt self-tests related to words, which are probably even more extreme).
- Again, this is using Z3 as an oracle, thus not using the HOL4 kernel to verify the proof is correct. However, so far I have never detected any soundness issues in Z3 or HolSmt; and although I'm sure Z3 still has such issues in more obscure functionality, the core functionality seems pretty solid (as far as I can tell).
- I expected Z3 to be able to solve at least the first inductive subgoal (which was solved by
rw[Once n_trits_def]) if I providedn_trits_deftoz3o_tac[], but surprisingly it wasn't able to do so -- probably because of the recursive function definition issue that I mentioned before.
Still, I found it very surprising that its performance was so good in this instance, especially considering that:
- I'm not even using Z3's native power operator yet!
- This theorem is just about
nums, which are more difficult for SMT solvers to handle since they don't support them natively - It also requires reasoning about division (
numdivision, even), which SMT solvers don't support directly because in their theory, division has different behavior
mn200
binghe
tjark
This week I've had the opportunity to use HolSmt more extensively and noticed a few shortcomings. This PR fixes a few of them.
It contains the following 3 minor improvements:
Allow SMT solvers to peek under abbreviations
Otherwise, they would only be able to see the variables that are being abbreviated to, but not the terms being abbreviated. This problem was causing some goals that can be solved with
metis_tacto fail with HolSmt. The fix is to add the definition of theAbbrevsymbol to the list of theorems that are added to the assumptions prior to calling the SMT solver.Add
z3_tacandz3o_tactacticsThese accept a list of theorems, like
metis_tac. The free vars in the theorems are automatically quantified withDrule.GEN_ALLand added to the list of assumptions in the goal, prior to sending the goal to the SMT solver.This is needed to avoid any passed-in theorems to be specialized to free vars in the goal that happen to have the same name, which is almost always not what the user wants (and if the user really wants it, they can always assume such theorems manually if needed). This matches the behavior of
metis_tac, thus avoiding unwanted surprises.Note: in particular, when using these tactics and HolSmt is configured to call Z3 with a timeout,
z3o_tac[]basically works as a (usually) more powerful "metis_tac[]+DECIDE_TAC/intLib.ARITH_TAC+RealField.REAL_ARITH_TAC+wordsLib.WORD_DECIDE+blastLib.BBLAST_TAC+HolSatLib.SAT_ORACLE+ nonlinear int and real arithmetic DP", all at once (and usually faster as well) -- although keep in mind thatz3o_tacworks as an external oracle, which is not appropriate in some circumstances. However, even in these cases it's probably still great for prototyping, i.e. as something in-between a full proof andcheat. The main limitation I've found in arithmetic-related goals is that Z3 often seems to get stuck finding proofs if the user provides definitions of recursive functions (similar torw[recursive_function_def]without theOncemodifier). This could be solved in the future using the same technique that F* uses to encode recursive function definitions: by adding a (configurable) fuel parameter that limits how many times a function definition can be unfolded during the proof search.Initial support for the
num,intandrealexponential functionsUnfortunately, this feature is more complicated than it seems. For now, all I did was add a couple of useful theorems to the proving context, so that the SMT solvers can "understand" what these exponential functions are supposed to do, but this only allows them to solve some simpler goals. As you can see from the self-tests, the coverage is extremely spotty: some
numandrealtheorems can be solved, but other simple ones can't, and almost nointtheorems can be solved. This is in part due to some theorems causing SMT solvers to become stuck finding a proof and also in part due to some theorems that are missing in HOL4. However, even if such missing theorems would be added, I wouldn't expect them to go very far in terms of solving goals efficiently. That said, it's still surprising to me that Z3 can solve a lot morenumtheorems thanintones, given that Z3 doesn't even support natural numbers natively.Since I'm currently working with goals with many exponentials, I am planning to improve this feature in an upcoming PR. Namely, it turns out that Z3 also has native support for an exponential/power operator. If other arithmetic operators are any indication, I would expect Z3's native power operator to solve a lot more goals than relying on adding theorems to the proving context. However, these operators in the Z3 and HOL4 theories all have different domains and codomains. Namely (written below in SML signature syntax):
val ** : num -> num -> numval ** : int -> num -> intval pow : real -> num -> realval ^ : int -> int -> realval ^ : real -> real -> realAs you can see, Z3's native power operators do not exactly match any of HOL4's operators, so implementing support for them would be similar to the previous implementation of integer division (which also didn't match any of HOL4's division functions). Namely, this would require:
**]:val z3ipow_def = bossLib.Define `z3ipow x y = if 0 <= y then real_of_int (x ** (Num y)) else 1 / (real_of_int (x ** (Num (-y))))`pow]:val z3ipow_def = bossLib.Define `z3ipow x y = if 0 <= y then (real_of_int x) pow (Num y) else 1 / ((real_of_int x) pow (Num (-y)))`real_of_int, if it's not implemented yet)Note, however, that Z3's native power operators are a Z3 extension and not part of the SMT-LIB standard. Therefore, since it would only work for Z3 and proof reconstruction would not work, HolSmt would only use it with
z3o_tacorZ3_ORACLE_{TAC,PROVE}and not with the other tactics.Note: no code outside HolSmt was changed in this PR.
cc @tjark