Example 1: the basics

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:

Suppose we've defined a function called

(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,

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

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

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.