• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Miscellaneous
      • Term
      • Ld
      • Hints
      • Type-set
      • Ordinals
        • O-p
        • O<
        • Proof-of-well-foundedness
        • Two-nats-measure
        • Nat-list-measure
          • Nat-list-<
        • Make-ord
        • O-first-coeff
        • E0-ord-<
        • O-first-expt
        • E0-ordinalp
        • O-rst
        • O-finp
        • O>=
        • O<=
        • O-infp
        • O>
      • Clause
      • With-prover-step-limit
      • ACL2-customization
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Set-subgoal-loop-limits
      • Gcl
      • Defsum
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Divp-by-casting
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Majority-vote
      • Def::doc
      • Syntax
      • Subgoal-loop-limits
      • Subversive-inductions
    • 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)))))