• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
    • Clex
      • Example-lexer
      • Sin
      • Matching-functions
      • Def-sin-progress
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Clex

Def-sin-progress

Prove basic progress properties of a lexing function.

The macro def-sin-progress can be used to prove basic progress properties about a function that updates sin.

Typically for any function (f ... sin) --> (mv ... sin) you will want to prove:

(defthm f-progress-weak
  (<= (len (strin-left (mv-nth ... (f ... sin))))
      (len (strin-left sin)))
  :rule-classes ((:rewrite) (:linear)))

(defthm f-progress-strong
  (implies hyp
           (< (len (strin-left (mv-nth ... (f ... sin))))
              (len (strin-left sin))))
  :rule-classes ((:rewrite) (:linear)))

Where hyp is some suitable hypothesis involving the inputs and/or other values returned by the function, e.g., frequently, that F produced a token instead of failing.

(def-sin-progress name &key (hyp 't)) just tries to prove these theorems automatically about the function named name, with the given hyp. See the example-lexer for some examples of using it.