Strategy: Contrapositive

Pattern recognition

When you see: a goal P → Q where proving directly is hard, but ¬Q → ¬P is easier

Strategy: Prove the contrapositive instead.

Tactic: contrapose

The contrapositive of P → Q is ¬Q → ¬P. They are logically equivalent (in classical logic). Sometimes the contrapositive is much easier to prove — especially when the conclusion Q is something concrete you can negate.

The contrapose tactic transforms the goal from P → Q to ¬Q → ¬P. You can also use contrapose! which additionally pushes negations inward (turning ¬(a = b) into a ≠ b, etc.).

Watch the strategy in action

The rule

Goal shape:  P → Q       (where direct proof is hard)
Action:      contrapose
Effect:      Goal becomes ¬Q → ¬P
Think:       "Instead of 'if P then Q', prove 'if not Q then not P'."

Variant:     contrapose!
Effect:      Same, but also simplifies negations
             (e.g., ¬(a ≤ b) becomes b < a)

Your turn

Prove: if n * m = 0 then n = 0 ∨ m = 0. The contrapositive is easier: if neither is zero, their product isn't zero.

theorem mul_eq_zero (n m : Nat) : n * m = 0 → n = 0 ∨ m = 0 := by
  sorry

Hint

Use contrapose! to get the goal n ≠ 0 ∧ m ≠ 0 → n * m ≠ 0. Then intro ⟨hn, hm⟩ and use omega or Nat.mul_pos.

Solution

theorem mul_eq_zero (n m : Nat) : n * m = 0 → n = 0 ∨ m = 0 := by
  contrapose!
  intro ⟨hn, hm⟩
  exact Nat.mul_pos (Nat.pos_of_ne_zero hn) (Nat.pos_of_ne_zero hm)

Or more concisely:

theorem mul_eq_zero (n m : Nat) : n * m = 0 → n = 0 ∨ m = 0 := by
  contrapose!
  intro ⟨hn, hm⟩
  omega

← Rewriting ← All tracks