vecs-ints - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))

local

(local (include-book "ihs/math-lemmas" :dir :system))

local

(local (in-theory (disable floor)))

int-to-vfunction

(defun int-to-v
  (x n)
  (declare (xargs :guard (and (integerp x) (natp n))))
  (if (zp n)
    nil
    (let ((rest (int-to-v (ash x -1) (1- n))))
      (cons (logbitp 0 x) rest))))

nat-to-vmacro

(defmacro nat-to-v (&rest args) (cons 'int-to-v args))

other

(add-macro-alias nat-to-v int-to-v)

v-to-natfunction

(defun v-to-nat
  (a)
  (declare (xargs :guard t))
  (if (atom a)
    0
    (let ((rst (* 2 (v-to-nat (cdr a)))))
      (+ (if (car a)
          1
          0)
        rst))))

v-to-intfunction

(defun v-to-int
  (a)
  (declare (xargs :guard t))
  (if (atom a)
    0
    (if (atom (cdr a))
      (if (car a)
        -1
        0)
      (let ((rest (* 2 (v-to-int (cdr a)))))
        (+ (if (car a)
            1
            0)
          rest)))))

int-to-fvfunction

(defun int-to-fv
  (x n)
  (declare (xargs :guard (and (integerp x) (natp n))))
  (if (zp n)
    nil
    (let ((rest (int-to-fv (ash x -1) (1- n))))
      (cons (if (logbitp 0 x)
          '(t)
          '(nil . t))
        rest))))

nat-to-fvmacro

(defmacro nat-to-fv (&rest args) (cons 'int-to-fv args))

other

(add-macro-alias nat-to-fv int-to-fv)

fv-to-natfunction

(defun fv-to-nat
  (a)
  (declare (xargs :guard t))
  (if (atom a)
    0
    (let ((rest (fv-to-nat (cdr a))))
      (if (integerp rest)
        (cond ((equal (car a) '(t)) (+ 1 (* 2 rest)))
          ((equal (car a) '(nil . t)) (* 2 rest))
          (t 'x))
        rest))))

fv-to-intfunction

(defun fv-to-int
  (a)
  (declare (xargs :guard t))
  (if (atom a)
    0
    (if (atom (cdr a))
      (cond ((equal (car a) '(t)) -1)
        ((equal (car a) '(nil . t)) 0)
        (t 'x))
      (let ((rest (fv-to-int (cdr a))))
        (if (integerp rest)
          (cond ((equal (car a) '(t)) (+ 1 (* 2 rest)))
            ((equal (car a) '(nil . t)) (* 2 rest))
            (t 'x))
          rest)))))

consp-int-to-vtheorem

(defthm consp-int-to-v
  (equal (consp (int-to-v n len)) (not (zp len))))

len-int-to-vtheorem

(defthm len-int-to-v
  (equal (len (int-to-v n len)) (nfix len)))

boolean-listp-int-to-vtheorem

(defthm boolean-listp-int-to-v
  (boolean-listp (int-to-v x n)))

v-to-nat-type-rwtheorem

(defthm v-to-nat-type-rw
  (and (integerp (v-to-nat a))
    (natp (v-to-nat a))
    (<= 0 (v-to-nat a))))

v-to-nat-lineartheorem

(defthm v-to-nat-linear
  (and (<= 0 (v-to-nat a)) (< (v-to-nat a) (expt 2 (len a))))
  :rule-classes ((:linear :trigger-terms ((v-to-nat a)))))

v-to-int-linear-1theorem

(defthm v-to-int-linear-1
  (<= (- (expt 2 (+ -1 (len a)))) (v-to-int a))
  :rule-classes ((:linear :trigger-terms ((v-to-int a)))))

v-to-int-linear-2theorem

(defthm v-to-int-linear-2
  (< (v-to-int a) (expt 2 (+ -1 (len a))))
  :hints (("goal" :induct (v-to-int a)) (and stable-under-simplificationp
      '(:expand ((expt 2 (len (cdr a)))))))
  :rule-classes ((:linear :trigger-terms ((v-to-int a)))))

local

(local (encapsulate nil
    (local (defthmd expt-2-positive-integer-is-even-1
        (implies (and (integerp exp) (< 0 exp))
          (integerp (* 1/2 (expt 2 exp))))))
    (defthm expt-2-positive-integer-is-even
      (implies (and (equal (expt 2 exp) (- n))
          (integerp exp)
          (< 0 exp)
          (integerp n))
        (integerp (* 1/2 n)))
      :hints (("Goal" :use ((:instance expt-2-positive-integer-is-even-1)))))))

v-to-nat-int-to-vtheorem

(defthm v-to-nat-int-to-v
  (implies (and (integerp n) (<= 0 n) (< n (expt 2 len)))
    (equal (v-to-nat (int-to-v n len)) n)))

local

(local (progn (defthm integerp-half-exp-2-greater-0
      (implies (and (integerp n) (< 0 n))
        (integerp (* 1/2 (expt 2 n)))))
    (defthm integer-lower-bound-floor
      (implies (and (integerp k) (rationalp r) (<= k r))
        (<= k (floor r 1)))
      :rule-classes nil)
    (defthm product-integer-lower-bound-floor
      (implies (and (integerp k)
          (integerp n)
          (rationalp f)
          (integerp (* f k))
          (<= 0 f)
          (<= k n))
        (<= (* f k) (floor (* f n) 1)))
      :hints (("goal" :use ((:instance integer-lower-bound-floor
            (r (* f n))
            (k (* f k))))))
      :rule-classes nil)
    (defthm expt-2-lte-zero
      (implies (and (integerp x) (<= x 0))
        (and (< 0 (expt 2 x)) (<= (expt 2 x) 1)))
      :rule-classes nil)))

local

(local (defthm lousy-lemma-1
    (implies (and (< (floor (* 1/2 n) 1) (- (* 1/2 (expt 2 (+ -1 len)))))
        (<= (- (expt 2 (+ -1 len))) n)
        (integerp n)
        (natp len)
        (< 1 len))
      (equal (+ 1
          (* 2 (v-to-int (int-to-v (floor (* 1/2 n) 1) (+ -1 len)))))
        n))
    :hints (("Goal" :use ((:instance product-integer-lower-bound-floor
          (n n)
          (k (- (expt 2 (+ -1 len))))
          (f 1/2)))))))

local

(local (defthm lousy-lemma-2
    (implies (and (zp len)
        (integerp n)
        (<= (- (* 1/2 (expt 2 len))) n)
        (< (* 2 n) (expt 2 len)))
      (equal (equal 0 n) t))
    :hints (("goal" :use ((:instance expt-2-lte-zero (x len)))))))

v-to-int-int-to-vtheorem

(defthm v-to-int-int-to-v
  (implies (and (integerp n)
      (<= (- (expt 2 (1- (ifix len)))) n)
      (< n (expt 2 (1- (ifix len)))))
    (equal (v-to-int (int-to-v n len)) n)))

int-to-v-v-to-nattheorem

(defthm int-to-v-v-to-nat
  (implies (and (boolean-listp lst) (equal len (len lst)))
    (equal (int-to-v (v-to-nat lst) len) lst)))

int-to-v-v-to-inttheorem

(defthm int-to-v-v-to-int
  (implies (and (boolean-listp lst) (equal len (len lst)))
    (equal (int-to-v (v-to-int lst) len) lst)))

consp-int-to-fvtheorem

(defthm consp-int-to-fv
  (equal (consp (int-to-fv n len)) (not (zp len))))

len-int-to-fvtheorem

(defthm len-int-to-fv
  (equal (len (int-to-fv n len)) (nfix len)))

fv-const-bool-listpfunction

(defun fv-const-bool-listp
  (a)
  (if (atom a)
    (equal a nil)
    (and (or (equal (car a) '(t)) (equal (car a) '(nil . t)))
      (fv-const-bool-listp (cdr a)))))

fv-const-bool-listp-int-to-fvtheorem

(defthm fv-const-bool-listp-int-to-fv
  (fv-const-bool-listp (int-to-fv x n)))

fv-to-nat-type-rwtheorem

(defthm fv-to-nat-type-rw
  (implies (fv-const-bool-listp a)
    (and (integerp (fv-to-nat a))
      (natp (fv-to-nat a))
      (<= 0 (fv-to-nat a))))
  :rule-classes (:rewrite :type-prescription))

fv-to-nat-lineartheorem

(defthm fv-to-nat-linear
  (implies (fv-const-bool-listp a)
    (and (<= 0 (fv-to-nat a))
      (< (fv-to-nat a) (expt 2 (len a)))))
  :rule-classes ((:linear :trigger-terms ((fv-to-nat a)))))

fv-to-int-type-rwtheorem

(defthm fv-to-int-type-rw
  (implies (fv-const-bool-listp a) (integerp (fv-to-int a)))
  :rule-classes (:rewrite :type-prescription))

fv-to-int-lineartheorem

(defthm fv-to-int-linear
  (implies (fv-const-bool-listp lst)
    (and (<= (- (expt 2 (1- (len lst)))) (fv-to-int lst))
      (< (fv-to-int lst) (expt 2 (1- (len lst))))))
  :hints (("goal" :induct (fv-to-int lst)) (and stable-under-simplificationp
      '(:expand ((expt 2 (len (cdr lst)))))))
  :rule-classes (:rewrite (:linear :trigger-terms ((fv-to-int lst)))))

fv-to-nat-int-to-fvtheorem

(defthm fv-to-nat-int-to-fv
  (implies (and (integerp n) (<= 0 n) (< n (expt 2 len)))
    (equal (fv-to-nat (int-to-fv n len)) n)))

local

(local (defthm lousy-lemma-3
    (implies (and (< (floor (* 1/2 n) 1) (- (* 1/2 (expt 2 (+ -1 len)))))
        (<= (- (expt 2 (+ -1 len))) n)
        (< 1 len)
        (natp len)
        (integerp n))
      (equal (+ 1
          (* 2 (fv-to-int (int-to-fv (floor (* 1/2 n) 1) (+ -1 len)))))
        n))
    :hints (("Goal" :use ((:instance product-integer-lower-bound-floor
          (n n)
          (k (- (expt 2 (+ -1 len))))
          (f 1/2)))))))

fv-to-int-int-to-fvtheorem

(defthm fv-to-int-int-to-fv
  (implies (and (integerp n)
      (<= (- (expt 2 (1- (ifix len)))) n)
      (< n (expt 2 (1- (ifix len)))))
    (equal (fv-to-int (int-to-fv n len)) n)))

int-to-fv-fv-to-nattheorem

(defthm int-to-fv-fv-to-nat
  (implies (and (fv-const-bool-listp lst) (equal len (len lst)))
    (equal (int-to-fv (fv-to-nat lst) len) lst)))

int-to-fv-fv-to-inttheorem

(defthm int-to-fv-fv-to-int
  (implies (and (fv-const-bool-listp lst) (equal len (len lst)))
    (equal (int-to-fv (fv-to-int lst) len) lst)))

logbitp-of-v-to-nattheorem

(defthm logbitp-of-v-to-nat
  (equal (logbitp n (v-to-nat a))
    (if (nth (nfix n) a)
      t
      nil))
  :hints (("Goal" :induct (nth n a) :in-theory (enable v-to-nat))))