05 — If and Only If

The Mathematics

This is the one. The namesake. The whole reason this site is called what it's called.

The biconditional P ↔ Q (read "P if and only if Q") means two things at once:

P → Q — "if P then Q" (the forward direction)
Q → P — "if Q then P" (the backward direction)

In other words, P and Q are logically equivalent. They're true in exactly the same situations. Mathematicians abbreviate "if and only if" as iff — and that little double arrow ↔ (or ⇔) packs a surprising amount of power into two tiny strokes.

When you see "P iff Q" in a textbook, you know you're looking at two implications bundled together. Every iff proof has two parts: prove the forward direction, then prove the backward direction.

In Lean 4:

constructor — splits P ↔ Q into two goals: P → Q and Q → P
h.mp — extracts the forward direction from h : P ↔ Q (gives P → Q)
h.mpr — extracts the backward direction (gives Q → P)

The names mp and mpr come from modus ponens and modus ponens reverse — the classical rule of inference that lets you go from "if P then Q" and "P" to "Q".

The Lean Proof

Let's start with a simple example. If we already have h : P ↔ Q and hp : P, we can get a proof of Q:

theorem iff_mp (P Q : Prop) (h : P ↔ Q) (hp : P) : Q := by
  exact h.mp hp

The .mp field extracts the forward implication, and we apply it to hp.

To build an iff from scratch, use constructor to split it into its two halves:

theorem iff_self (P : Prop) : P ↔ P := by
  constructor
  · intro hp
    exact hp
  · intro hp
    exact hp

Both directions are the identity — P implies P. Not the most thrilling theorem, but it shows the shape of every iff proof: constructor, then handle each direction.

Your Turn

Prove that iff is commutative. If P ↔ Q, then Q ↔ P. You'll need to split the goal and swap the two directions.

theorem iff_comm (P Q : Prop) (h : P ↔ Q) : Q ↔ P := by
  sorry

Think about it: if h gives you both P → Q and Q → P, and you need to prove Q → P and P → Q... it's just a swap.

Hint

Use constructor to split Q ↔ P into two goals.

The first goal is Q → P — that's h.mpr (the backward direction of h).

The second goal is P → Q — that's h.mp (the forward direction of h).

Solution

theorem iff_comm (P Q : Prop) (h : P ↔ Q) : Q ↔ P := by
  constructor
  · exact h.mpr
  · exact h.mp

We split the goal with constructor, then hand over the backward direction as the new forward direction and vice versa. The two halves of the biconditional simply trade places.

Bonus: Build an Iff from Scratch

Here's a meatier challenge. Prove that P ∧ Q ↔ Q ∧ P without any hypothesis — build the whole biconditional yourself. You'll need to combine what you learned about conjunction in the previous exercise with your new iff skills.

theorem and_iff_and_comm (P Q : Prop) : P ∧ Q ↔ Q ∧ P := by
  sorry

Bonus Hint

Use constructor to split the iff. Each direction is an implication, so use intro to get the hypothesis.

Then destructure the conjunction with angle brackets: intro ⟨hp, hq⟩ gives you both parts.

Rebuild the conjunction with the parts swapped: exact ⟨hq, hp⟩.

Bonus Solution

theorem and_iff_and_comm (P Q : Prop) : P ∧ Q ↔ Q ∧ P := by
  constructor
  · intro ⟨hp, hq⟩
    exact ⟨hq, hp⟩
  · intro ⟨hq, hp⟩
    exact ⟨hp, hq⟩

Each direction destructures a conjunction and rebuilds it with the components swapped. The iff just bundles both swaps together. Beautiful symmetry.

← Disjunction (or) Negation →