• Top
  • Documentation
  • Books
  • 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-plural-p
        • Vl-remove-keys
        • Vl-merge-contiguous-indices
        • Vl-edition-p
        • Sum-nats
        • 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
        • True-list-listp
        • Symbol-list-listp
        • Explode-list
        • All-have-len
        • Pos-listp
        • Min-nats
        • Debuggable-and
        • Vl-starname
        • Remove-equal-without-guard
        • Vl-maybe-string-list
        • String-fix
        • Longer-than-p
        • Anyp
        • Fast-alist-free-each-alist-val
        • Not*
        • Free-list-of-fast-alists
        • *nls*
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 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)))