Test/Check a conjecture for counterexamples.

(acl2s::test? (equal (reverse (reverse x)) x)) (test? (implies (and (posp (car x)) (posp (cdr x))) (= (cdr x) (len x)))) (defun perm (x y) (if (endp x) (endp y) (and (member (car x) y) (perm (cdr x) (remove1 (car x) y))))) (test? (implies (and (consp X) (member a Y)) (equal (perm (remove a X) (remove a Y)) (perm X Y))))Note: test? is in ACL2S package.

(test? form [:hints hints] [acl2s-defaults keyword options] )

If no counterexample is found, there are three possibilities. First, it is
possible that the conjecture is false, in which case increasing the amount of
testing we do may lead to the discovery of a counterexample. Second, it is
also possible that ACL2 proves that the conjecture is true, in which case we
print a message reporting success. Finally, the conjecture may be true, but
ACL2 cannot prove it. For all of these three cases, we consider testing to
have succeeded, so

We can furthur control the behavior of test? using keyword options or

(defdata small-pos (enum '(1 2 3 4 5 6 7 8 9))) (test? (implies (and (integerp c1) (integerp c2) (integerp c3) (small-posp x1) (small-posp x2) (small-posp x3) (< x1 x2) (< x2 x3) (equal 0 (+ c1 c2 c3)) (equal 0 (+ (* c1 x1) (* c2 x2) (* c3 x3)))) (and (= 0 c1) (= 0 c2) (= 0 c3)))) (defun square-root1 (i ri) (declare (xargs :mode :program)) (if (>= (floor i ri) ri) ri (square-root1 i (floor (+ ri (floor i ri)) 2)))) (defun square-root (i) (declare (xargs :mode :program)) (square-root1 i (floor i 2))) (defun square (x) (* x x)) (test? (implies (natp i) (and (<= (square (square-root i)) i) (< i (square (1+ (square-root i))))))) (defdata triple (list pos pos pos)) (defun trianglep (v) (and (triplep v) (< (third v) (+ (first v) (second v))) (< (first v) (+ (second v) (third v))) (< (second v) (+ (first v) (third v))))) (defun shape (v) (if (trianglep v) (cond ((equal (first v) (second v)) (if (equal (second v) (third v)) "equilateral" "isosceles")) ((equal (second v) (third v)) "isosceles") ((equal (first v) (third v)) "isosceles") (t "scalene")) "error")) (acl2s-defaults :set num-trials 1000000) (acl2s-defaults :set testing-enabled :naive) (test? (implies (and (triplep x) (trianglep x) (> (third x) 256) (= (third x) (* (second x) (first x)))) (not (equal "isosceles" (shape x))))) (acl2s-defaults :set num-trials 1000) (acl2s-defaults :set testing-enabled t) (include-book "arithmetic/top-with-meta" :dir :system) (test? (implies (and (triplep x) (trianglep x) (> (third x) 256) (= (third x) (* (second x) (first x)))) (not (equal "isosceles" (shape x)))))

We note that in order to be able to generate counterexamples, we do not
allow ACL2 to use any of the following processes: induction, generalization,
and cross-fertilization. We do allow destructor-elimination, though in rare
cases, user defined elim rules may generalize the conjecture. Such situations
are recognized. If you want to enable the above processes, use