HolSmt: usability improvements, initial support for exponentials #1247
Conversation
Otherwise, they won't be able to see what the variables are being abbreviated to. This problem would cause some goals that can be solved with metis_tac[] to fail with HolSmt. The fix is to add the definition of the `Abbrev` symbol to the list of theorems that are added to the assumptions prior to calling the SMT solver.
These accept a list of theorems, like `metis_tac`. The free vars in the theorems are automatically quantified with `Drule.GEN_ALL` and 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.
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
|
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 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: At first, I proved the theorem without HolSmt, which came out like this (please don't judge 😅): 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 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:
Still, I found it very surprising that its performance was so good in this instance, especially considering that:
|
|
Note that there is a |
|
Thanks for all the cool work! |
That's good to know, thanks! Unfortunately, even though they have the same type, the definition of Believe it or not, I cannot find a definition for Z3's real power operator anywhere, but from the source code I can tell that Z3 simplifies In HOL4, however, I have proven a theorem that states the opposite when using Theorem RPOW_1_NOT:
~(!x. x powr 1 = x)
Proof
rw[]
>> qexists_tac `-1`
>> rw[rpow_def]
>> qspec_then `ln (-1)` assume_tac EXP_POS_LE
>> pop_assum mp_tac
>> RealField.REAL_ARITH_TAC
QEDThis is because the theorem I can prove in Z3 is not true in HOL4 for negative That said, if I can somehow infer exactly what definition Z3 is using for its real power operator, I could probably make HolSmt handle |
|
Yes, This is reasonable, because |
Is that true, though? As far as I can tell, it's not just that In contrast, in Z3 I can prove that As a disclaimer, I am not a mathematician, or logician, or computer scientist... but as far as I can see, I think Z3's definition makes more sense to me, because like you say, when you can prove that However, in HOL4, even when you prove that |
This is because, by HOL4's definition of I think extending the domain of the existing |
|
On Fri, 2024-05-31 at 21:48 -0700, Chun Tian wrote:
I think extending the domain of the existing powr (to match Z3's behavior) is possible: the extended definition should include the case "the power is the real value of integers", so that for any integer n,x powr &n is defined for whatever x:real. But this change may introduce minor incompatibilities. I can have a try.
Given its type (real -> real -> real), it might make sense to extend powr to arbitrary real exponents?
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
|
I meant that, when the base is negative, the exponent must be integer (of type :real), e.g. P. S. Those undefined values are actually complex numbers with non-zero imaginary parts. |
Interestingly, Z3 doesn't support complex numbers (although you can encode them as a pair of reals), but even so, It also does something special with irrational algebraic numbers when processing the power operator, but it was a bit too dense for me to follow when I last looked into it... |
|
Currently, and in part based on what I wrote on my previous comment, I am heavily leaning into not adding specialized support for For example, that Z3 considers two power expressions, each of them a complex number, to be equal to each other even when their imaginary parts are different is not something that I was expecting. Furthermore, their processing of irrational numbers is also a bit hard for me to understand. When both operands are integers, then defining the power operator is more feasible, but even then there are some differences compared to HOL4. For example, I discovered that Z3 considers Even taking into account the above, it does seem straightforward to define the integer version of the power operator, but even so, I'd still like to be 100% sure that there are no more surprises and that what Z3 is doing is sound -- in particular, I'm worried about the rewrites that it does when the operands are not constant values / integer literals. Note that Z3 doesn't actually have two separate power operators (one for integers and one for reals), they are both the same operator. This means that even if both operands are integers, the function that processes the power operator still does everything that is needed to handle real values, which makes for less duplicate code, but at the same time it makes it harder to understand than would otherwise be required when only dealing with integers... Edit: for future reference, here you can see the Z3 code I'm looking at: https://github.com/Z3Prover/z3/blob/770c51ad2b257e59710041894581ec0411000018/src/ast/rewriter/arith_rewriter.cpp#L1513-L1679 Note: I think I just figured out that in Z3, their "numeral" terminology represents |
|
See #1252 for a proposal on extending the application domain of |
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 to
rw[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