• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
      • Maybe-stringp
      • Maybe-natp
      • Two-nats-measure
      • Impossible
      • Bytep
      • Nat-list-measure
        • Nat-list-<
      • Maybe-posp
      • Nibblep
      • Organize-symbols-by-pkg
      • Organize-symbols-by-name
      • Lnfix
      • Good-valuep
      • Streqv
      • Chareqv
      • Symbol-package-name-non-cl
      • Arith-equivs
      • Induction-schemes
      • Maybe-integerp
      • Char-fix
      • Pos-fix
      • Symbol-package-name-lst
      • Mbt$
      • Maybe-bitp
      • Good-pseudo-termp
      • Str-fix
      • Maybe-string-fix
      • Nonkeyword-listp
      • Lifix
      • Bfix
      • Std/basic/if*
      • Impliez
      • Tuplep
      • Std/basic/intern-in-package-of-symbol
      • Lbfix
      • Std/basic/symbol-name-lst
      • True
      • Std/basic/rfix
      • Std/basic/realfix
      • Std/basic/member-symbol-name
      • Std/basic/fix
      • False
      • Std/basic/nfix
      • Std/basic/ifix
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Nat-list-measure
• Well-founded-relation-rule

Nat-list-<

An alternate well-founded-relation that allows lists of naturals to be used directly as measures.

This is essentially syntactic sugar for nat-list-measure. We introduce nat-list-< as a well-founded-relation-rule, so that instead of writing:

(defun f (a b c)
  (declare (xargs :measure (nat-list-measure (list a b c))))
  ...)

You can instead write:

(defun f (a b c)
  (declare (xargs :measure (list a b c)
                  :well-founded-relation nat-list-<))
  ...)

That's more verbose in this example, but in practice it can often end up being more concise. In particular:

• You can use set-well-founded-relation to install nat-list-< as your well-founded relation ahead of time.
• In a big mutual-recursion, you only need to give the :well-founded-relation to a single definition.

Definitions and Theorems

Function: nat-list-<

(defun nat-list-< (a b)
  (o< (nat-list-measure a)
      (nat-list-measure b)))

Theorem: nat-list-wfr

(defthm nat-list-wfr
  (and (o-p (nat-list-measure x))
       (implies (nat-list-< x y)
                (o< (nat-list-measure x)
                    (nat-list-measure y))))
  :rule-classes :well-founded-relation)

Theorem: open-nat-list-<

(defthm open-nat-list-<
 (implies
  (syntaxp (and (cons-list-or-quotep a)
                (cons-list-or-quotep b)))
  (equal (nat-list-< a b)
         (or (< (len a) (len b))
             (and (equal (len a) (len b))
                  (if (consp a)
                      (or (< (nfix (car a)) (nfix (car b)))
                          (and (equal (nfix (car a)) (nfix (car b)))
                               (nat-list-< (cdr a) (cdr b))))
                    (< (nfix a) (nfix b))))))))

Theorem: natp-nat-list-<

(defthm natp-nat-list-<
  (implies (and (atom a) (atom b))
           (equal (nat-list-< a b)
                  (< (nfix a) (nfix b)))))