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

• Utilities

Nats-from

(nats-from a b) enumerates the naturals from [a, b).

Signature

(nats-from a b) → *

Arguments

a — Guard (natp a).

b — Guard (natp b).

Definitions and Theorems

Function: nats-from

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

Theorem: true-listp-of-nats-from

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

Theorem: nat-listp-of-nats-from

(defthm nat-listp-of-nats-from
  (nat-listp (nats-from a b)))

Theorem: consp-of-nats-from

(defthm consp-of-nats-from
  (equal (consp (nats-from a b))
         (< (nfix a) (nfix b))))

Theorem: nats-from-self

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

Theorem: member-equal-nats-from

(defthm member-equal-nats-from
  (iff (member-equal x (nats-from a b))
       (and (natp x)
            (<= (nfix a) x)
            (< x (nfix b)))))

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

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

Theorem: take-of-nats-from

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

Theorem: nthcdr-of-nats-from

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

Theorem: len-of-nats-from

(defthm len-of-nats-from
  (equal (len (nats-from a b))
         (nfix (- (nfix b) (nfix a)))))

Theorem: car-of-nats-from

(defthm car-of-nats-from
  (equal (car (nats-from a b))
         (if (< (nfix a) (nfix b))
             (nfix a)
           nil)))

Theorem: nth-of-nats-from

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

Theorem: setp-of-nats-from

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