		Search-engine friendly clone of the ACL2 documentation.

Tutorial

Fty-examples

A list of FTY examples

FTY examples

Prerequisite read for this tutorial example is tutorial.

Smtlink supports types defined by ACL2::fty macros defprod, deflist, defalist and defoption. We show here an example for each type.

defprod

Define the function x^2+y^2

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

Define the defprod sandwich

nil

Then define the theorem to prove:

(defthm fty-defprod-theorem
  (implies (and (sandwich-p s1) (sandwich-p s2))
           (>= (x^2+y^2 (sandwich->bread s1)
                        (sandwich->bread s2))
               0))
  :hints (("Goal" :smtlink (:fty (sandwich))))
  :rule-classes nil)

This theorem says, given two sandwich-p, then the square sum of the bread field of the two sandwiches should be non-negative. This example doesn't quite make sense. Here we use this as an example to show how defprod defined types can be used in a theorem to be discharged by Smtlink.

We notice the :fty hint is used to tell Smtlink which set of FTY types we will use in proving this theorem. Here, we use the FTY type sandwich. Smtlink will check fty::flextypes-table for information about this FTY type.

Counter-examples for defprods like like:

Possible counter-example found:
((S2 (SANDWICH 0 (SYM 2))) (S1 (SANDWICH 0 (SYM 1))))

deflist

Define the theorem to prove:

(defthm fty-deflist-theorem
 (implies
  (and
    (integer-listp l)
    (consp (acl2::integer-list-fix l))
    (consp
         (acl2::integer-list-fix (cdr (acl2::integer-list-fix l)))))
  (>=
   (x^2+y^2
    (car (acl2::integer-list-fix l))
    (car (acl2::integer-list-fix (cdr (acl2::integer-list-fix l)))))
   0))
 :hints (("Goal" :smtlink (:fty (acl2::integer-list))))
 :rule-classes nil)

This theorem says, given a list of integers, if there are at least two elements, then the square sum of the two elements should be non-negative.

First, Smtlink only allows types defined by deflist that are true-listp. We notice the :fty hint is used to tell Smtlink which set of FTY types we will use in proving this theorem. Here, we use the FTY type acl2::integer-list. Smtlink will check fty::flextypes-table to make sure the given deflist type is a true-listp.

Second, we notice extra fixing functions ACL2::integer-list-fix functions are added. This is because Z3 lists are typed. The polymorphic functions like car when translated into Z3, also become typed. Therefore we need to inference which car we want to apply here. Currently Smtlink doesn't have type inference ability, therefore it requires the user to add fixing functions for telling it the types.

Counter-examples for deflists like like:

Possible counter-example found: ((L (CONS 0 (CONS 0 NIL))))

defalist

Define the defalist symbol-integer-alist

(defalist symbol-integer-alist
          :key-type symbolp
          :val-type integerp
          :true-listp t)

Then define the theorem to prove:

(defthm fty-defalist-theorem
 (implies
  (and (symbol-integer-alist-p l)
       (symbolp s1)
       (symbolp s2)
       (not (equal (assoc-equal s1 (symbol-integer-alist-fix l))
                   (magic-fix 'symbolp_integerp nil)))
       (not (equal (assoc-equal s2 (symbol-integer-alist-fix l))
                   (magic-fix 'symbolp_integerp nil))))
  (>=
   (x^2+y^2
    (cdr (magic-fix 'symbolp_integerp
                    (assoc-equal s1 (symbol-integer-alist-fix l))))
    (cdr (magic-fix 'symbolp_integerp
                    (assoc-equal s2 (symbol-integer-alist-fix l)))))
   0))
 :hints (("Goal" :smtlink (:fty (symbol-integer-alist))))
 :rule-classes nil)

This theorem says, given a symbol-integer-alist l, two symbols s1 and s2, if one can find both s1 and s2 in the alist l, then the values satisfy that their square sum is non-negative. I hope the square sum example hasn't bored you yet at this point.

Similar to deflists, we notice extra fixing functions symbol-integer-alist-fix functions are added due to similar reasons. In addition, we notice ACL2 doesn't have a type specification for the thing returned by an assoc-equal. To make sure cdr knows what its argument type is, we add a magic-fix function.

Counter-examples for defalists like like:

((S2 (SYM 2)) (L (K SYMBOL (SOME 0))) (S1 (SYM 1)))

Here, the counter-example for alist l is

(K SYMBOL (SOME 0))

This means in Z3 a constant array mapping from symbols to the maybe integer 0. Also, SYM stands for generated symbols for symbol counter-examples.

defoption

Define the defoption maybe-integer

(defoption maybe-integer integerp
           :parents (tutorial))

Define the fixed version of x^2+y^2

(define x^2+y^2-fixed ((x maybe-integer-p)
                       (y maybe-integer-p))
  :returns (res maybe-integer-p)
  (b* ((x (maybe-integer-fix x))
       (y (maybe-integer-fix y))
       ((if (equal x (maybe-integer-fix nil)))
        (maybe-integer-fix nil))
       ((if (equal y (maybe-integer-fix nil)))
        (maybe-integer-fix nil)))
    (maybe-integer-some (+ (* (maybe-integer-some->val x)
                              (maybe-integer-some->val x))
                           (* (maybe-integer-some->val y)
                              (maybe-integer-some->val y))))))

Then define the theorem to prove:

(defthm fty-defoption-theorem
  (implies (and (maybe-integer-p m1)
                (maybe-integer-p m2)
                (not (equal m1 (maybe-integer-fix nil)))
                (not (equal m2 (maybe-integer-fix nil))))
           (>= (maybe-integer-some->val (x^2+y^2-fixed m1 m2))
               0))
  :hints (("Goal" :smtlink (:fty (maybe-integer))))
  :rule-classes nil)

This theorem says, given a maybe-integer m1 and a maybe-integer m2, if they are not nils, then the square sum of their values is non-negative.

Similar to deflists and defalists, we notice extra fixing functions maybe-integer-fix functions are added due to similar reasons. In addition, we notice in definition of function x^2+y^2-fixed, even when one knows x and y are not nil, they are still maybe-integers. Therefore, field-accessors and constructors are required.

Counter-examples for defalists like like:

Possible counter-example found: ((M2 (SOME 0)) (M1 (SOME 0)))