• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
        • Name-database
        • Vl-gc
        • Symbol-list-names
        • Ints-from
        • Nats-from
        • Make-lookup-alist
        • Redundant-mergesort
        • Longest-common-prefix
        • Vl-remove-keys
        • Vl-plural-p
        • Vl-merge-contiguous-indices
        • Sum-nats
        • Vl-edition-p
        • Vl-maybe-integer-listp
        • Fast-memberp
        • Nat-listp
        • Max-nats
        • Longest-common-prefix-list
        • Character-list-listp
        • Vl-character-list-list-values-p
        • Remove-from-alist
        • Prefix-of-eachp
        • Vl-string-keys-p
        • Vl-maybe-nat-listp
        • Vl-string-list-values-p
        • String-list-listp
        • Vl-string-values-p
        • Explode-list
        • True-list-listp
        • Symbol-list-listp
        • All-have-len
        • Pos-listp
        • Min-nats
        • Debuggable-and
        • Vl-starname
        • Remove-equal-without-guard
        • String-fix
        • Anyp
        • Vl-maybe-string-list
        • Longer-than-p
        • Fast-alist-free-each-alist-val
        • Not*
        • Free-list-of-fast-alists
        • *nls*
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Utilities

Ints-from

(ints-from a b) enumerates the integers from [a, b).

Signature

(ints-from a b) → *

Arguments

a — Guard (integerp a).

b — Guard (integerp b).

Definitions and Theorems

Function: ints-from

(defun ints-from (a b)
       (declare (xargs :guard (and (integerp a) (integerp b))))
       (declare (xargs :guard (<= a b)))
       (let ((__function__ 'ints-from))
            (declare (ignorable __function__))
            (let ((a (lifix a)) (b (lifix b)))
                 (if (mbe :logic (zp (- b a)) :exec (= a b))
                     nil (cons a (ints-from (+ 1 a) b))))))

Theorem: true-listp-of-ints-from

(defthm true-listp-of-ints-from
        (true-listp (ints-from a b))
        :rule-classes :type-prescription)

Theorem: integer-listp-of-ints-from

(defthm integer-listp-of-ints-from
        (integer-listp (ints-from a b)))

Theorem: consp-of-ints-from

(defthm consp-of-ints-from
        (equal (consp (ints-from a b))
               (< (ifix a) (ifix b))))

Theorem: ints-from-self

(defthm ints-from-self
        (equal (ints-from a a) nil))

Theorem: member-equal-ints-from

(defthm member-equal-ints-from
        (iff (member-equal x (ints-from a b))
             (and (integerp x)
                  (<= (ifix a) x)
                  (< x (ifix b)))))

Theorem: no-duplicatesp-equal-of-ints-from

(defthm no-duplicatesp-equal-of-ints-from
        (no-duplicatesp-equal (ints-from a b)))

Theorem: ints-from-of-ifix-a

(defthm ints-from-of-ifix-a
        (equal (ints-from (ifix a) b)
               (ints-from a b)))

Theorem: ints-from-int-equiv-congruence-on-a

(defthm ints-from-int-equiv-congruence-on-a
        (implies (acl2::int-equiv a a-equiv)
                 (equal (ints-from a b)
                        (ints-from a-equiv b)))
        :rule-classes :congruence)

Theorem: ints-from-of-ifix-b

(defthm ints-from-of-ifix-b
        (equal (ints-from a (ifix b))
               (ints-from a b)))

Theorem: ints-from-int-equiv-congruence-on-b

(defthm ints-from-int-equiv-congruence-on-b
        (implies (acl2::int-equiv b b-equiv)
                 (equal (ints-from a b)
                        (ints-from a b-equiv)))
        :rule-classes :congruence)

Theorem: take-of-ints-from

(defthm
     take-of-ints-from
     (equal (take k (ints-from a b))
            (if (< (ifix k)
                   (nfix (- (ifix b) (ifix a))))
                (ints-from a (+ (ifix a) (ifix k)))
                (append (ints-from a b)
                        (replicate (- (ifix k)
                                      (nfix (- (ifix b) (ifix a))))
                                   nil)))))

Theorem: nthcdr-of-ints-from

(defthm nthcdr-of-ints-from
        (equal (nthcdr k (ints-from a b))
               (if (< (nfix k)
                      (nfix (- (ifix b) (ifix a))))
                   (ints-from (+ (ifix a) (nfix k)) b)
                   nil)))

Theorem: len-of-ints-from

(defthm len-of-ints-from
        (equal (len (ints-from a b))
               (nfix (- (ifix b) (ifix a)))))

Theorem: car-of-ints-from

(defthm car-of-ints-from
        (equal (car (ints-from a b))
               (if (< (ifix a) (ifix b))
                   (ifix a)
                   nil)))

Theorem: nth-of-ints-from

(defthm nth-of-ints-from
        (equal (nth n (ints-from a b))
               (if (< (nfix n)
                      (nfix (- (ifix b) (ifix a))))
                   (+ (ifix a) (nfix n))
                   nil)))

Theorem: setp-of-ints-from

(defthm setp-of-ints-from
        (setp (ints-from a b)))