• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
      • Type-prescription
      • Rewrite
      • Meta
      • Linear
      • Definition
      • Clause-processor
      • Tau-system
      • Forward-chaining
      • Equivalence
      • Congruence
      • Free-variables
      • Executable-counterpart
      • Induction
      • Type-reasoning
      • Compound-recognizer
      • Rewrite-quoted-constant
      • Elim
      • Well-founded-relation-rule
        • Nat-list-<
      • Built-in-clause
      • Well-formedness-guarantee
      • Patterned-congruence
      • Rule-classes-introduction
      • Refinement
      • Guard-holders
      • Type-set-inverter
      • Generalize
      • Corollary
      • Induction-heuristics
      • Well-founded-relation
      • Backchaining
      • Default-backchain-limit
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Miscellaneous
    • Output-controls
    • Bdd
    • Macros
    • Installation
    • Mailing-lists
  • 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)))))