Home / Tracks / Logic / Conjunction

Conjunction (and)

The mathematics

Conjunction P ∧ Q means "both P and Q are true." It's the logical "and." Simple enough in everyday language: "It's sunny and warm." Both parts must hold.

To prove a conjunction, you need to prove both halves separately. There's no shortcut — you have to do the work twice. In Lean 4, the constructor tactic splits a conjunction goal into two subgoals.

To use a conjunction you already have, you break it apart into its two pieces. If you know h : P ∧ Q, you can extract the proof of P and the proof of Q individually. In Lean 4, obtain ⟨hp, hq⟩ := h does exactly this, giving you hp : P and hq : Q.

The Lean 4 proof

Here are the key tactics for working with conjunction:

constructor — When your goal is P ∧ Q, this splits it into two goals: first prove P, then prove Q.

obtain ⟨hp, hq⟩ := h — When you have h : P ∧ Q in context, this destructures it into hp : P and hq : Q. The angle brackets ⟨ ⟩ are typed as \langle and \rangle in Lean.

And.intro — The term-mode way to build a conjunction: And.intro hp hq produces a proof of P ∧ Q from proofs of P and Q. You can also use anonymous constructor syntax: ⟨hp, hq⟩.

-- Prove a conjunction by proving both sides
theorem and_intro (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  · exact hp
  · exact hq

-- Same thing using anonymous constructor syntax
theorem and_intro' (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  exact ⟨hp, hq⟩

-- Destructure a conjunction and swap the halves
theorem and_comm_example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  obtain ⟨hp, hq⟩ := h
  exact ⟨hq, hp⟩

-- You can also use .1 and .2 to access the components
theorem and_left (P Q : Prop) (h : P ∧ Q) : P := by
  exact h.1

Your turn

Prove that conjunction is commutative: if P ∧ Q, then Q ∧ P. Replace sorry with a proof.

theorem and_comm (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  sorry

theorem and_comm (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  obtain ⟨hp, hq⟩ := h
  exact ⟨hq, hp⟩