• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • 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-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

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