		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Integers-from-to

Ordered list of all the integers in a range.

Signature
(integers-from-to min max) → ints
Arguments: min — Guard (integerp min).; max — Guard (integerp max).
Returns: ints — Type (integer-listp ints).

The range goes from min to max, both inclusive. If min exceeds max, the result is nil.

Definitions and Theorems

Function: integers-from-to-aux

(defun integers-from-to-aux (min max ints)
  (declare (xargs :guard (and (integerp min)
                              (integerp max)
                              (integer-listp ints))))
  (let ((__function__ 'integers-from-to-aux))
    (declare (ignorable __function__))
    (b* ((min (mbe :logic (ifix min) :exec min))
         (max (mbe :logic (ifix max) :exec max)))
      (cond ((> min max) ints)
            (t (integers-from-to-aux min (1- max)
                                     (cons max ints)))))))

Function: integers-from-to

(defun integers-from-to (min max)
  (declare (xargs :guard (and (integerp min) (integerp max))))
  (let ((__function__ 'integers-from-to))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((min (ifix min)) (max (ifix max)))
           (cond ((> min max) nil)
                 (t (cons min (integers-from-to (1+ min) max)))))
         :exec (integers-from-to-aux min max nil))))

Theorem: integer-listp-of-integers-from-to

(defthm integer-listp-of-integers-from-to
  (b* ((ints (integers-from-to min max)))
    (integer-listp ints))
  :rule-classes :rewrite)

Theorem: integers-from-to-of-ifix-min

(defthm integers-from-to-of-ifix-min
  (equal (integers-from-to (ifix min) max)
         (integers-from-to min max)))

Theorem: integers-from-to-of-ifix-max

(defthm integers-from-to-of-ifix-max
  (equal (integers-from-to min (ifix max))
         (integers-from-to min max)))

Theorem: integers-from-to-of-noninteger-min

(defthm integers-from-to-of-noninteger-min
  (implies (not (integerp min))
           (equal (integers-from-to min max)
                  (integers-from-to 0 max))))

Theorem: integers-from-to-of-noninteger-max

(defthm integers-from-to-of-noninteger-max
  (implies (not (integerp max))
           (equal (integers-from-to min max)
                  (integers-from-to min 0))))

Theorem: true-listp-of-integers-from-to

(defthm true-listp-of-integers-from-to
  (b* ((ints (integers-from-to min max)))
    (true-listp ints))
  :rule-classes :type-prescription)

Theorem: nat-listp-of-integers-from-to

(defthm nat-listp-of-integers-from-to
  (equal (nat-listp (integers-from-to min max))
         (or (> (ifix min) (ifix max))
             (natp (ifix min)))))

Theorem: pos-listp-of-integers-from-to

(defthm pos-listp-of-integers-from-to
  (equal (pos-listp (integers-from-to min max))
         (or (> (ifix min) (ifix max))
             (posp (ifix min)))))

Theorem: int-equiv-implies-equal-integers-from-to-1

(defthm int-equiv-implies-equal-integers-from-to-1
  (implies (int-equiv min min-equiv)
           (equal (integers-from-to min max)
                  (integers-from-to min-equiv max)))
  :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-integers-from-to-2

(defthm int-equiv-implies-equal-integers-from-to-2
  (implies (int-equiv max max-equiv)
           (equal (integers-from-to min max)
                  (integers-from-to min max-equiv)))
  :rule-classes (:congruence))

Theorem: integers-from-to-nil-when-min>max

(defthm integers-from-to-nil-when-min>max
  (implies (> (ifix min) (ifix max))
           (equal (integers-from-to min max) nil)))

Theorem: integers-from-to-iff-min<=max

(defthm integers-from-to-iff-min<=max
  (iff (integers-from-to min max)
       (<= (ifix min) (ifix max))))

Theorem: consp-of-integers-from-to-equal-min<=max

(defthm consp-of-integers-from-to-equal-min<=max
  (equal (consp (integers-from-to min max))
         (<= (ifix min) (ifix max))))

Theorem: integers-from-to-separate-min

(defthm integers-from-to-separate-min
  (implies (and (integerp min)
                (integerp max)
                (<= min max))
           (equal (integers-from-to min max)
                  (cons min (integers-from-to (1+ min) max)))))

Theorem: integers-from-to-separate-max

(defthm integers-from-to-separate-max
  (implies (and (integerp min)
                (integerp max)
                (<= min max))
           (equal (integers-from-to min max)
                  (append (integers-from-to min (1- max))
                          (list max)))))

Theorem: member-equal-of-integers-from-to

(defthm member-equal-of-integers-from-to
  (iff (member-equal x (integers-from-to min max))
       (and (integerp x)
            (<= (ifix min) x)
            (<= x (ifix max)))))

Theorem: len-of-integers-from-to

(defthm len-of-integers-from-to
  (equal (len (integers-from-to min max))
         (nfix (1+ (- (ifix max) (ifix min))))))

Subtopics

Integers-from-to-as-set: Theorems about integers-from-to as a finite set.
Insertion-sort-of-integers-from-to: Applying insertion sort to an ordered list of integers in a range yields the same list.