; A Little Proof Hack: Enumerating the Values of a Term ; J Strother Moore ; November, 2013 ; (certify-book "enumerate") ; If you attach the hint ; :use ((:instance enumerate (term x) (i -2) (j 3))) ; to a goal, (p x), you get the following new subgoals (in some pretty ; random order!): ; (P -2) ; (P -1) ; (P 0) ; (P 1) ; (P 2) ; (P 3) ; (IMPLIES (< X -2) (P X)) ; (IMPLIES (< 3 X) (P X)) ; (IMPLIES (NOT (INTEGERP X)) (P X)) ; For the hint to work properly, i and j should be quoted integer constants. ; Example Use: The following is not a theorem but the thm command will ; show the cases generated by the enumerate hint. #|| (defstub p (x) t) (thm (p x) :hints (("Goal" :use (:instance enumerate (term x) (i -2)(j 3)))) :otf-flg t) ||# (in-package "ACL2") (defun enumerate! (term i j) (declare (xargs :measure (acl2-count (nfix (- (+ 1 (ifix j)) (ifix i)))))) (cond ((and (integerp i) (integerp j) (<= i j)) (if (equal term i) t (enumerate! term (+ i 1) j))) (t nil))) (defthm enumerate (implies (and (integerp term) (integerp i) (integerp j) (<= i term) (<= term j)) (enumerate! term i j)) :rule-classes nil) (defthm enumerate-expander (and (implies (and (syntaxp (and (quotep i) (quotep j))) (integerp i) (integerp j) (< j i)) (equal (enumerate! term i j) nil)) (implies (and (syntaxp (and (quotep i) (quotep j))) (integerp i) (integerp j) (<= i j)) (equal (enumerate! term i j) (or (equal term i) (enumerate! term (+ i 1) j)))))) (in-theory (disable enumerate!))