Example-2
Example 2: something wild
Example 2
Prerequisite read for this tutorial example is tutorial.
Smtlink is extensible, with the user's understanding that the extended part
is not verified and therefore is the user's responsibility to ensure its
soundness. A different trust tag is installed if this customized Smtlink is
used. Such ability makes Smtlink very powerful. Here's an example to show the
usage.
Let's say we want to prove the theorem:
Theorem 2.
\forall x,y,z\in R, and \forall m,n \in Z, if 0 \le z \le 1 and
0 \le m \le n , then 2xy\cdot z^n \le (x^2+y^2)z^m.
In smtlink/z3_interface/, file RewriteExpt.py is a Python class
extending from the default class in ACL2_to_Z3.py. One could imaging defining
one's own file that does magical things in the SMT solver. What
RewriteExpt.py does is that it uses basic rewrite lemmas about expt
to help the SMT solver to solve. In order to make Smtlink uses the custom
version instead of the default, one needs to define and attach a new
configuration:
(defun my-smtlink-expt-config nil
(declare (xargs :guard t))
(change-smtlink-config (default-smt-cnf)
:smt-module "RewriteExpt"
:smt-class "to_smt_w_expt"))
(defattach custom-smt-cnf my-smtlink-expt-config)
Defining the function x^2+y^2
(defun x^2+y^2 (x y)
(+ (* x x) (* y y)))
Then define the theorem to prove:
(encapsulate nil
(local (include-book "arithmetic-5/top"
:dir :system))
(defthm poly-of-expt-example
(implies (and (real/rationalp x)
(real/rationalp y)
(real/rationalp z)
(integerp m)
(integerp n)
(< 0 z)
(< z 1)
(< 0 m)
(< m n))
(<= (* 2 (expt z n) x y)
(* (expt z m) (x^2+y^2 x y))))
:hints
(("Goal"
:smtlink-custom
(:functions
((expt :formals ((r real/rationalp) (i real/rationalp))
:returns ((ex real/rationalp))
:level 0))
:hypotheses (((< (expt z n) (expt z m)))
((< 0 (expt z m)))
((< 0 (expt z n))))
:int-to-rat t)))))
Notice the :hints keyword used this time is :smtlink-custom. It
allows the customized version of Smtlink to be applied to the current
clause. Take a read in smt-hint for a detailed description of each
keyword. Here we will only describe what's used in this example.
In the hints, :function tells Smtlink to treat expt as an
uninterpreted function. :formals tells us the input argument types of the
uninterpreted function and :returns tells us the output argument type.
:levels specifies an expansion level of 0, making the function an
uninterpreted function.
:hypotheses provides a list of hypotheses that the user believes to be
true and can help with the proof. The hypotheses will be insert into the
hypotheses when generating the SMT problem. They will be proved correctness
as part of the returned clauses from the verified clause processor.
:int-to-rat tells Smtlink to raise integers to rationals when
translating the clause into a SMT problem. This is because of the limitation in
Z3. Integers mixed with real numbers are hard for Z3. We prove the given
theorem by proving a more general statement in the SMT solver.
Another observation is that, we are including the arithmetic-5 book for
proving the returned auxiliary clauses, which requires arithmetic
reasoning.
