		Search-engine friendly clone of the ACL2 documentation.

Tutorial

Example-1

Example 1: the basics

Example 1

Prerequisite read for this tutorial example is tutorial.

The first example is a basic polynomial inequality. Let's say we want to prove below theorem:

Theorem 1. \forall x\in R and \forall y \in R, if \frac{9x^2}{8}+y^2 \le 1 and x^2-y^2 \le 1, then y < 3(x-\frac{17}{8})^2 - 3.

Suppose we've defined a function called x^2-y^2 like below:

(defun x^2-y^2 (x y)
  (- (* x x) (* y y)))

We define our theorem as:

(defthm poly-ineq-example
  (implies (and (real/rationalp x)
                (real/rationalp y)
                (<= (+ (* (/ 9 8) x x) (* y y)) 1)
                (<= (x^2-y^2 x y) 1))
           (< y
              (- (* 3 (- x (/ 17 8)) (- x (/ 17 8)))
                 3)))
  :hints (("Goal" :smtlink nil)))

Smtlink should just prove this inequality without any problem.

Like is shown in the example, :smtlink can be provided as a hint in the standard ACL2::hints in ACL2. In the most basic cases where Smtlink handles everything, no smt-hint are required to be provided, Hence :smtlink nil.

The output of this defthm should look similar to:

Using clause-processor Smtlink
Goal'
Goal''
SMT-goal-generator=>Expanding ... X^2-Y^2
Subgoal 2
Subgoal 2.2
Subgoal 2.2'
Using default SMT-trusted-cp...
; SMT solver: `python /tmp/py_file/smtlink.w59zR`: 0.52 sec, 7,904 bytes
Proved!
Subgoal 2.2''
Subgoal 2.1
Subgoal 2.1'
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFTHM POLY-INEQ-EXAMPLE ...)
Rules: ((:DEFINITION HIDE)
        (:DEFINITION HINT-PLEASE)
        (:DEFINITION NOT)
        (:DEFINITION TYPE-HYP)
        (:DEFINITION X^2-Y^2)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART ACL2::BOOLEAN-LIST-FIX$INLINE)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:EXECUTABLE-COUNTERPART UNARY-/)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE ACL2::COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
Hint-events: ((:CLAUSE-PROCESSOR ADD-HYPO-CP)
              (:CLAUSE-PROCESSOR EXPAND-CP-FN)
              (:CLAUSE-PROCESSOR PROCESS-HINT)
              (:CLAUSE-PROCESSOR SMT-TRUSTED-CP)
              (:CLAUSE-PROCESSOR TYPE-EXTRACT-FN)
              (:CLAUSE-PROCESSOR UNINTERPRETED-FN-CP))
Time:  0.60 seconds (prove: 0.60, print: 0.00, other: 0.00)
Prover steps counted:  1440
POLY-INEQ-EXAMPLE

Smtlink is a sequence of clause processors controlled by a computed hint. Calling smtlink from the :hints put the theorem clause though a clause processor looking for syntax errors in the smt-hint. If nothing wrong, it will generate a term to be recognized by the computed-hint SMT::SMT-computed-hint. The computed-hint then installs the next-to-be clause processor to work on the clause. The next is the verified clause processor for adding hypotheses. After that is the verified clause processor for function expansion.

SMT-goal-generator=>Expanding ... X^2-Y^2 shows function expansion is being conducted.

In this example, several subgoals are generated as a result of this clause processor. The first subgoal is the goal to be sent to the trusted clause processor that transliterates the term into the corresponding SMT form and writes it out to a file. An SMT solver is called upon the file and results are read back into ACL2. Below are the outputs from this clause processor called SMT-trusted-cp.

Using default SMT-trusted-cp...
; SMT solver: `python /tmp/py_file/smtlink.w59zR`: 0.52 sec, 7,904 bytes
Proved!

The second line tells the user what command is run to execute the SMT solving. "Proved!" indicates the SMT solver has successfully proved the theorem. When a theorem failed, a possible counter-example might be provided in the form:

Possible counter-example found: ((X ...) (Y ...))
One can access it through global variable SMT-cex by doing (@ SMT-
cex).

Other subgoals are auxiliary clauses generated by the verified clause-processors. They help ensure the soundness of Smtlink.