CMU 15-671  Models of Software Systems  Fall 1995

Other Proof Techniques and Proof Hints

Garlan & Wing  Handout 3  11 September 1995

Natural deduction and equational reasoning, which you have seen already, and induction, which you will see shortly, are examples of different proof techniques to have in your bag of proof tricks. This handout covers some others. All but the first are probably familiar to you, which is why we are not going to dwell on any of them. Much of this handout is inspired by [GS]; parts are copied verbatim from Chapters 3 and 4.

1 One Point Rule

The One Point Rule is useful for dealing with existential quantifiers. It says that if you have an existentially quantified statement and part of it pins down an exact value for the quantified variable, then you can remove the quantification and replace the variable by the value whereever that variable appears in the rest of the statement.

\frac{∃ x : S • (p ∧ x = t)}{t ∈ S ∧ p[t/x]} ¬(occurs(x, t))

Note the side condition that you must check before applying this rule: The variable, x, must not be free in the term, t, that you are using in the substitution.

For example, ∃ n : � • (n < 10 ∧ n = 2 ∗ 3) is equivalent to 2 ∗ 3 ∈ � ∧ 2 ∗ 3 < 10. The first conjunct checks that the term is member of the right set; it is usually easy to discharge that check. Then, you are left with just the part of the predicate in which the substitution has been made, e.g., 2 ∗ 3 < 10.

2 Implication [GS]

If your predicate has an implication in it, sometimes it’s easier to work with the equivalent disjunctive formulation:

p ⇒ q ≡ ¬p ∨ q

Here are some other useful properties about implication and boolean constants:

p ⇒ p ≡ true (Reflexivity) p ⇒ true ≡ true (Right zero) true ⇒ p ≡ p (Left identity) p ⇒ false ≡ ¬p false ⇒ p ≡ true

Here are some useful theorems about implication:

p ∧ q ⇒ r ≡ p ⇒ (q ⇒ r) (Shunting) p ∧ (p ⇒ q) ≡ p ∧ q p ∨ (p ⇒ q) ≡ true

\begin{matrix}c \\ ◯ \end{matrix}1995 Jeannette M. Wing

3 Assuming the Antecedent [GS]

It is common in mathematics to prove an implication p ⇒ q by assuming the antecedent p and proving the consequent q. By “assuming the antecedent” we momentarily think of it as an axiom and thus equivalent to true. The formal justification of this proof technique relies on the Deduction Theorem from mathematical logic.^{1}

Here is a simple example (from [GS]): Suppose we want to prove a ∧ b ⇒ (a = b). In the proof we get to assume the conjuncts of the antecedent. We are required to prove a = b:

Proof:

Assume a, b.

a = % Assumption of a.

true = % Assumption of b.

b

Warning: For the proof of p ⇒ q, the Deduction Theorem requires that all variables in the assumed expression, p, be viewed as constants throughout the proof of q, so that you cannot substitute expressions in for the “variables” that appear in the assumptions. The following incorrect proof of (b = c) ⇒ (d = c) (which is not valid) shows why this is necessary. The proof is incorrect because b in the assumption is replaced.

Proof (Incorrect):

Assume b = c.

d = % Assumption of (b = c)[d/b], i.e., d = c

c

Notice that the expression in which we are attempting to do the substitution is b = c.

4 Case Analysis [GS]

A proof of r by case analysis proceeds as follows. Find the cases p and q such that p ∨ q holds. Then show that r holds in each case: p ⇒ r and q ⇒ r. The justification of this proof technique relies on this property of implication:

(p ⇒ r) ∧ (q ⇒ r) ≡ (p ∨ q ⇒ r) (Case Analysis)

Notice the common (and simpler) version of this property when q ≡ ¬p:

(p ⇒ r) ∧ (¬p ⇒ r) ≡ r (Simple Case Analysis)

This proof technique generalizes to a case analysis of more than two cases in the obvious way: The disjunction of all the cases must be true and each case must imply r.

5 Proof by Contradiction [GS]

It is common in mathematics to prove a theorem p by assuming it is false and deriving a contradiction, i.e., derive false or something equivalent to false, like q ∧ ¬q. The justification for this proof technique is the following property about implication, repeated from Section 2:

1Deduction Theorem: Suppose adding p_{1},…, p_{n} as axioms to propositional logic, with the variables of the p_{i} considered to be constants, allows q to be proved. Then p_{1} ∧… ∧ p_{n} ⇒ q is a theorem.

p ⇒ false ≡ ¬p

By substituting ¬p for p and using double negation, we derive the theorem:

¬p ⇒ false ≡ p (Proof by Contradiction)

Hence, having proved that ¬p ⇒ false is a theorem, you may conclude that p is a theorem.

6 Proof by Contrapositive [GS]

A typical proof of the implication p ⇒ q might proceed as follows (notice a combination of proof techniques, assuming the antecedent and proof by contradiction):

• Assume p.

• Prove q by contradiction. That is, assume ¬q and prove false.

This technique is really a proof by contrapositive in disguise:

p ⇒ q ≡ ¬q ⇒ ¬p (Contrapositive)

7 Proof Hints

• Use the structure of an expression to guide what proof step to take next.

– Look for subexpressions that you can replace with equivalent expresssions.

– Use algebraic and logical properties of logical connectives and quantifiers to rewrite formulae. For example, use the One Point Rule to eliminate the existential; use properties of implication (Section 2) to get rid of implications; use properties about quantifiers to move them outward across connectives.

• Use lemmas and auxiliary definitions to add structure to your proof.

– Introduce them to avoid repeating the same subexpressions or subproofs. (Sound familiar from your programming experience?)

– Use them to make your proofs more readable, shorter, and more modular.

• Suppose you have an expression, e, given in terms of an operator f . (In fact you may introduced f yourself following the hint above.)

– Expand the expression e by replacing f with its definition.

– Then use properties about operators, g, in f ’s definition to manipulate and simplify the expanded e.

– At the end, reintroduce (if convenient or necessary) the original f using its definition (in the other direction).