Strategy: Split the goal

Pattern recognition

When you see: a goal of the form P ∧ Q or P ↔ Q

Strategy: Prove each half separately.

Tactic: constructor

When your goal is a conjunction or biconditional, you can't prove it in one shot. You need to split it into pieces and prove each one. The constructor tactic does exactly this — it replaces one goal with two (or more) subgoals.

This works because P ∧ Q is defined as a structure with two fields, and P ↔ Q is (P → Q) ∧ (Q → P). The constructor tactic asks you to provide each field.

Watch the strategy in action

The rule

Goal shape:  P ∧ Q       (or P ↔ Q)
Action:      constructor
Effect:      Goal splits into two: first prove P, then prove Q
Think:       "I need to prove both halves."

Your turn

Prove that conjunction is associative: (P ∧ Q) ∧ R ↔ P ∧ (Q ∧ R). You will need constructor multiple times.

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

Hint

Start with constructor to split the iff into two implications. Each implication needs intro h, then obtain to destructure the conjunction, then exact ⟨...⟩ to rebuild it.

Solution

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

← Direct proof Case analysis →