• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
        • Name-database
        • Vl-gc
        • Symbol-list-names
        • Ints-from
        • Nats-from
          • Nats-from-exec
        • 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

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__))
    (mbe :logic
         (let ((a (lnfix a)) (b (lnfix b)))
           (if (zp (- b a))
               nil
             (cons a (nats-from (+ 1 a) b))))
         :exec (with-local-nrev (nats-from-exec a b nrev)))))

Theorem: nats-from-exec-removal

(defthm nats-from-exec-removal
  (equal (nats-from-exec a b nrev)
         (append nrev (nats-from 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)))

Subtopics

Nats-from-exec