Prove an equivalence
P ↔ Q is two implications. constructor gives you both.
In this course 5 / 11
P ↔ Q, typed \iff, says each side implies the other. A proof of it is the pair of implications P → Q and Q → P, so constructor splits an ↔ goal into two, exactly as it did for ∧.
The two new goals are implications, so a branch normally opens with intro. When you already hold the implication as a hypothesis, exact closes the branch immediately, and that is the shape of your exercise.
Order matters: the first goal is the forward direction P → Q, the second is Q → P. Swapping them gives a type mismatch that names both propositions, so the fix takes one glance at the message.
Equivalences are worth building because they can be used like equations. Once you hold h : P ↔ Q, rw [h] rewrites P into Q inside another goal. The Rewriting and automation course uses that often.
Worked example
example (A : Prop) (ha : A) : A ↔ (2 + 2 = 4) := by
constructor
· intro _
rfl
· intro _
exact haNeither direction is a hypothesis here, so both branches start with intro and then do real work: one computes, the other uses ha. In your exercise both implications are already in the context.
P ↔ Q is a pair of implications. constructor splits it, and each direction is proven on its own.
Combine hpq and hqp into a proof of P ↔ Q.
Suggested steps
- Split the equivalence into its two implications
- Prove the forward direction
- Prove the backward direction
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct