A list of 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.

Define the function

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

Define the defprod

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

We notice the

Counter-examples for defprods like like:

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

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

Second, we notice extra fixing functions `ACL2::integer-list-fix`
functions are added. This is because Z3 lists are typed. The polymorphic
functions like

Counter-examples for deflists like like:

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

Define the defalist

(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

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,

Define the defoption

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

Define the fixed version of

(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

Counter-examples for defalists like like:

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