• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
          • Logic-knowledge-taken-for-granted
          • Logic-knowledge-taken-for-granted-inductive-proof
          • Introduction-to-rewrite-rules-part-1
          • Introduction-to-key-checkpoints
          • Introduction-to-rewrite-rules-part-2
          • Logic-knowledge-taken-for-granted-propositional-calculus
          • Geneqv
          • Introduction-to-a-few-system-considerations
          • Refinement-failure
          • Introduction-to-the-database
          • Programming-knowledge-taken-for-granted
          • Logic-knowledge-taken-for-granted-rewriting
          • Introductory-challenge-problem-4-answer
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Introduction-to-hints
          • Dealing-with-key-combinations-of-function-symbols
          • Architecture-of-the-prover
          • Further-information-on-rewriting
          • Frequently-asked-questions-by-newcomers
          • Specific-kinds-of-formulas-as-rewrite-rules
          • Strong-rewrite-rules
          • Practice-formulating-strong-rules-3
          • Practice-formulating-strong-rules-1
          • Practice-formulating-strong-rules-6
          • Generalizing-key-checkpoints
          • Logic-knowledge-taken-for-granted-q1-answer
          • Example-inductions
          • Logic-knowledge-taken-for-granted-q2-answer
          • Logic-knowledge-taken-for-granted-rewriting-repeatedly
          • Introductory-challenge-problem-4
          • Equivalent-formulas-different-rewrite-rules
          • Post-induction-key-checkpoints
          • Special-cases-for-rewrite-rules
          • Example-induction-scheme-with-accumulators
          • Practice-formulating-strong-rules-5
          • Practice-formulating-strong-rules
          • Practice-formulating-strong-rules-2
          • Introductory-challenges
          • Logic-knowledge-taken-for-granted-equals-for-equals
          • Logic-knowledge-taken-for-granted-evaluation
          • Example-induction-scheme-nat-recursion
          • Example-induction-scheme-down-by-2
          • Logic-knowledge-taken-for-granted-instance
          • Introductory-challenge-problem-3-answer
          • Example-induction-scheme-on-lists
          • Example-induction-scheme-upwards
          • Example-induction-scheme-with-multiple-induction-steps
          • Practice-formulating-strong-rules-4
          • Logic-knowledge-taken-for-granted-q3-answer
          • Example-induction-scheme-binary-trees
          • Introductory-challenge-problem-3
          • Introductory-challenge-problem-1
          • Logic-knowledge-taken-for-granted-base-case
          • Introductory-challenge-problem-1-answer
          • Example-induction-scheme-on-several-variables
          • Introductory-challenge-problem-2-answer
          • Introductory-challenge-problem-2
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Introduction-to-the-theorem-prover

Practice-formulating-strong-rules

A few simple checkpoints suggesting strong rules

Consider these definitions:

(defun rev (x)
  (if (endp x)
      nil
      (append (rev (cdr x)) (list (car x)))))

(defun nats-below (j)
  (if (zp j)
      '(0)
      (cons j (nats-below (- j 1)))))

We assume you are familiar with such ACL2 built-ins as append, member, subsetp and true-listp. When we use throw-away names like FOO, BAR, and MUM below we mean to suggest some arbitrary function you shouldn't think about! We're just trying to train your eye to ignore irrelevant things.

Below are some terms that should suggest rewrite rules to you. Imagine that each of these terms occurs in some Key Checkpoint. What rules come to mind? Try to think of the strongest rules you can.

Term 1:

(TRUE-LISTP (APPEND (FOO A) (BAR B)))

Answers: See practice-formulating-strong-rules-1

Term 2:

(TRUE-LISTP (REV (FOO A)))

Answers: See practice-formulating-strong-rules-2

Term 3:

(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))

Answers: See practice-formulating-strong-rules-3

Term 4:

(SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))

Answers: See practice-formulating-strong-rules-4

Term 5:

(SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))

Answers: See practice-formulating-strong-rules-5

Term 6:

(MEMBER (FOO A) (NATS-BELOW (BAR B)))

Answers: See practice-formulating-strong-rules-6

We recommend doing all of these little exercises. When you're finished, use your browser's Back Button to return to strong-rewrite-rules.