• 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-5

Rules suggested by (SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))

What rules come to mind when looking at the following subterm of a Key Checkpoint? Think of strong rules (see strong-rewrite-rules).

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

When is x a subset of (append y z)? Clearly it is if x is a subset of y or x is a subset of z. We could write that:

(defthm subsetp-append-2-weak
  (implies (or (subsetp x y)
               (subsetp x z))
           (subsetp x (append y z))))

The rule generated from this is: ``if you ever encounter (an instance of) (SUBSETP x (APPEND y z)), backchain to the or above and try to establish it. If you can establish it, replace the target by T.''

This does not fully characterize the situation though. For example, '(1 2 3 4) is a subset of (append '(1 3) '(2 4)) without being a subset of either argument of the append.

However, no obvious equivalence comes to mind — indeed, to express any of the ideas floating around here requires defining and introducing more functions, which is not recommended unless those functions are already in the problem.

For example, if you defined the concept of ``set-minus'' so that (set-minus x y) consists of those elements of x not in y, then you could prove:

(defthm subset-append-2-strong-but-messy
  (equal (subsetp x (append y z))
         (and (subsetp (set-minus x z) y)
              (subsetp (set-minus x y) z))))

But this rewrite rule would ``trade'' append away and introduce set-minus. That might be a good strategy if set-minus were already in the problem. But if it were not, it might not be. We wouldn't recommend this rule unless it were helpful in normalizing the expressions in the problem.

We recommend sticking with the weak version of the rule,

(defthm subsetp-append-2-weak
  (implies (or (subsetp x y)
               (subsetp x z))
           (subsetp x (append y z)))).

This illustrates the fact that sometimes there is no strong version of a rule!

Use your browser's Back Button now to return to practice-formulating-strong-rules.