• 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
      • 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
          • Geneqv
          • Logic-knowledge-taken-for-granted-propositional-calculus
          • Refinement-failure
          • Introduction-to-a-few-system-considerations
          • 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
        • Tours
        • Emacs
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Workshops
        • 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
            • Geneqv
            • Logic-knowledge-taken-for-granted-propositional-calculus
            • Refinement-failure
            • Introduction-to-a-few-system-considerations
            • 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
          • Tours
          • Emacs
        • Version
        • How-to-contribute
        • Acknowledgments
        • Using-ACL2
        • Releases
        • Pre-built-binary-distributions
        • Common-lisp
        • Installation
        • Mailing-lists
        • Git-quick-start
        • Copyright
        • ACL2-help
    • Miscellaneous
    • Output-controls
    • Bdd
    • Macros
    • Installation
    • Mailing-lists
  • 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.