• 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
          • Generalizing-key-checkpoints
          • Logic-knowledge-taken-for-granted-q1-answer
          • Practice-formulating-strong-rules-6
          • 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

Logic-knowledge-taken-for-granted-equals-for-equals

Substitution of equals for equals

Anytime you have an equality hypothesis relating two terms, e.g.,

(equal lhs rhs) 

it is legal to substitute one for the other anyplace else in the formula. Doing so does not change the truth value of the formula.

You can use a negated equality this way provided it appears in the conclusion. For example, it is ok to transform

(implies (true-listp x)
         (not (equal x 23)))

to

(implies (true-listp 23)
         (not (equal x 23)))

by substitutions of equals for equals. That is because, by propositional calculus, we could rearrange the formulas into their contrapositive forms:

(implies (equal x 23)
         (not (true-listp x)))

and

(implies (equal x 23)
         (not (true-listp 23)))

and see the equality as a hypothesis and the substitution of 23 for x as sensible.

Sometimes people speak loosely and say ``substitution of equals for equals'' when they really mean ``substitutions of equivalents for equivalents.'' Equality, as tested by EQUAL, is only one example of an equivalence relation. The next most common is propositional equivalence, as tested by IFF. You can use propositional equivalence hypotheses to substitute one side for the other provided the target term occurs in a propositional place, as discussed at the bottom of propositional calculus.

Now use your browser's Back Button to return to the example proof in logic-knowledge-taken-for-granted.