		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Nat=>lendian*

Convert a natural number to its minimum-length little-endian list of digits.

Signature
(nat=>lendian* base nat) → digits
Arguments: base — Guard (dab-basep base).; nat — Guard (natp nat).
Returns: digits — Type (dab-digit-listp base digits).

The resulting list is empty if nat is 0. The * in the name of this function can be read as `zero or more' (as in typical regular expression notation).

See also nat=>lendian+ and nat=>lendian.

The theorem len-of-nat=>lendian*-leq-width is proved from a variant of it where width is universally quantified. This variant is proved via an induction scheme similar to nat=>lendian* but without width. Base case and induction step are proved individually; the induction step uses an arithmetic lemma. The arithmetic-5 library is needed for several of these proofs. There might be a simpler proof that, in particular, does not involve introducing a defun-sk.

Definitions and Theorems

Function: nat=>lendian*

(defun nat=>lendian* (base nat)
 (declare (xargs :guard (and (dab-basep base) (natp nat))))
 (let ((__function__ 'nat=>lendian*))
  (declare (ignorable __function__))
  (mbe
   :exec (rev (nat=>digits-exec base nat nil))
   :logic
   (cond
      ((zp nat) nil)
      (t (cons (mod nat (dab-base-fix base))
               (nat=>lendian* base
                              (floor nat (dab-base-fix base)))))))))

Theorem: return-type-of-nat=>lendian*

(defthm return-type-of-nat=>lendian*
  (b* ((digits (nat=>lendian* base nat)))
    (dab-digit-listp base digits))
  :rule-classes :rewrite)

Theorem: nat-listp-of-nat=>lendian*

(defthm nat-listp-of-nat=>lendian*
  (b* ((digits (nat=>lendian* base nat)))
    (nat-listp digits))
  :rule-classes :rewrite)

Theorem: consp-of-nat=>lendian*

(defthm consp-of-nat=>lendian*
  (implies (not (zp nat))
           (b* ((digits (nat=>lendian* base nat)))
             (consp digits)))
  :rule-classes :type-prescription)

Theorem: consp-of-nat=>lendian*-iff-not-zp

(defthm consp-of-nat=>lendian*-iff-not-zp
  (equal (consp (nat=>lendian* base nat))
         (not (zp nat))))

Theorem: nat=>digits-exec-to-nat=>lendian*

(defthm nat=>digits-exec-to-nat=>lendian*
  (implies (and (dab-basep base)
                (natp nat)
                (dab-digit-listp base current-digits))
           (equal (nat=>digits-exec base nat current-digits)
                  (append (rev (nat=>lendian* base nat))
                          current-digits))))

Theorem: nat=>lendian*-of-0

(defthm nat=>lendian*-of-0
  (equal (nat=>lendian* base 0) nil))

Theorem: len-0-of-nat=>lendian*

(defthm len-0-of-nat=>lendian*
  (equal (equal (len (nat=>lendian* base x)) 0)
         (zp x)))

Theorem: expt-of-len-of-nat=>lendian*-is-upper-bound

(defthm expt-of-len-of-nat=>lendian*-is-upper-bound
  (implies (and (natp nat) (dab-basep base))
           (< nat
              (expt base (len (nat=>lendian* base nat)))))
  :rule-classes :linear)

Theorem: nat=>lendian*-does-not-end-with-0

(defthm nat=>lendian*-does-not-end-with-0
  (not (equal (car (last (nat=>lendian* base nat)))
              0)))

Theorem: len-of-nat=>lendian*-leq-width

(defthm len-of-nat=>lendian*-leq-width
 (implies (and (natp nat)
               (dab-basep base)
               (natp width))
          (equal (<= (len (nat=>lendian* base nat))
                     width)
                 (< nat (expt base width))))
 :rule-classes
 ((:rewrite :corollary
            (implies (and (natp nat)
                          (dab-basep base)
                          (natp width))
                     (equal (> (len (nat=>lendian* base nat)) width)
                            (>= nat (expt base width))))
            :hints (("Goal" :in-theory '(not))))))

Theorem: nat=>lendian*-of-digit-+-base-*-nat

(defthm nat=>lendian*-of-digit-+-base-*-nat
  (implies (and (dab-basep base)
                (dab-digitp base x)
                (natp y))
           (equal (nat=>lendian* base (+ x (* base y)))
                  (if (equal y 0)
                      (if (equal x 0) nil (list x))
                    (cons x (nat=>lendian* base y))))))

Theorem: nat=>lendian*-of-dab-base-fix-base

(defthm nat=>lendian*-of-dab-base-fix-base
  (equal (nat=>lendian* (dab-base-fix base) nat)
         (nat=>lendian* base nat)))

Theorem: nat=>lendian*-dab-base-equiv-congruence-on-base

(defthm nat=>lendian*-dab-base-equiv-congruence-on-base
  (implies (dab-base-equiv base base-equiv)
           (equal (nat=>lendian* base nat)
                  (nat=>lendian* base-equiv nat)))
  :rule-classes :congruence)

Theorem: nat=>lendian*-of-nfix-nat

(defthm nat=>lendian*-of-nfix-nat
  (equal (nat=>lendian* base (nfix nat))
         (nat=>lendian* base nat)))

Theorem: nat=>lendian*-nat-equiv-congruence-on-nat

(defthm nat=>lendian*-nat-equiv-congruence-on-nat
  (implies (nat-equiv nat nat-equiv)
           (equal (nat=>lendian* base nat)
                  (nat=>lendian* base nat-equiv)))
  :rule-classes :congruence)

Subtopics

Nat=>digits-exec: Tail-recursive code for the execution of nat=>bendian* and nat=>lendian* (and, indirectly, of their variants).