2.3 Conjunction

Conjunction represents “and”. A proof of P ∧ Q contains two pieces of evidence: a proof of P and a proof of Q. In Lean, conjunction behaves like a pair whose fields are logical proofs.

Problem

You want to prove or use a statement of the form:

P ∧ Q

To prove it, you must prove both sides. To use it, you may extract either side.

Solution

Use constructor to split a conjunction goal into two goals.

theorem make_conjunction (P Q : Prop) : P -> Q -> P ∧ Q := by
  intro hp
  intro hq
  constructor
  · exact hp
  · exact hq

After constructor, Lean creates two goals:

⊢ P
⊢ Q

Each goal is solved using the corresponding hypothesis.

Extracting the Left and Right Sides

If you have:

h : P ∧ Q

then h.left is a proof of P, and h.right is a proof of Q.

theorem conjunction_left (P Q : Prop) : P ∧ Q -> P := by
  intro h
  exact h.left

theorem conjunction_right (P Q : Prop) : P ∧ Q -> Q := by
  intro h
  exact h.right

These projections are the most direct way to use a conjunction.

Case Analysis on a Conjunction

You can also decompose a conjunction with cases.

theorem conjunction_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  cases h with
  | intro hp hq =>
    constructor
    · exact hq
    · exact hp

The command cases h replaces the conjunction proof with its two components:

hp : P
hq : Q

Then the goal Q ∧ P is proved by constructing both parts in reverse order.

Term Form

The same proof can be written without tactics.

theorem conjunction_swap_term (P Q : Prop) : P ∧ Q -> Q ∧ P :=
  fun h => And.intro h.right h.left

The constructor And.intro takes a proof of the left side and a proof of the right side.

Its shape is:

And.intro : P -> Q -> P ∧ Q

So to build Q ∧ P, we pass h.right : Q first and h.left : P second.

Nested Conjunctions

Conjunctions associate to the right only according to the syntax you write. The propositions below are different shapes:

(P ∧ Q) ∧ R
P ∧ (Q ∧ R)

They contain the same logical information, but the proof objects are nested differently.

theorem reassociate_conjunction
    (P Q R : Prop) :
    (P ∧ Q) ∧ R -> P ∧ (Q ∧ R) := by
  intro h
  constructor
  · exact h.left.left
  · constructor
    · exact h.left.right
    · exact h.right

The hypothesis has type:

h : (P ∧ Q) ∧ R

So:

h.left       : P ∧ Q
h.left.left  : P
h.left.right : Q
h.right      : R

The proof rebuilds the conjunction in the requested shape.

Building Conjunctions Step by Step

Sometimes it is clearer to name intermediate proofs.

theorem conjunction_with_have
    (P Q R : Prop)
    (hp : P)
    (hq : Q)
    (hr : R) :
    P ∧ (Q ∧ R) := by
  have hqr : Q ∧ R := by
    constructor
    · exact hq
    · exact hr
  constructor
  · exact hp
  · exact hqr

This style is useful when one side of the conjunction is itself a nontrivial proof.

Using Pattern Matching in intro

Lean can destruct a conjunction as soon as it is introduced.

theorem conjunction_swap_intro_pattern
    (P Q : Prop) :
    P ∧ Q -> Q ∧ P := by
  intro ⟨hp, hq⟩
  exact ⟨hq, hp⟩

The notation:

⟨hp, hq⟩

means that the proof of P ∧ Q is decomposed into its two components.

The same notation can also construct conjunctions:

⟨hq, hp⟩

constructs a proof of Q ∧ P.

Conjunction and simp

Simple conjunction projections are often solved by simp.

theorem simp_conjunction_left (P Q : Prop) : P ∧ Q -> P := by
  intro h
  simp [h]

theorem simp_conjunction_comm (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left

For beginner code, prefer explicit projections or cases. They show the proof shape clearly.

Common Patterns

To prove:

⊢ P ∧ Q

use:

constructor

and prove both goals.

To use:

h : P ∧ Q

use:

h.left
h.right

or:

cases h with
| intro hp hq => ...

To build a conjunction directly, use:

exact ⟨hp, hq⟩

Common Pitfalls

Do not treat h : P ∧ Q as two hypotheses until you extract them. Lean sees one hypothesis whose type is a conjunction.

Do not reverse the order when constructing a conjunction. To prove P ∧ Q, the first proof must have type P, and the second proof must have type Q.

Do not assume nested conjunctions have the same syntactic shape. P ∧ Q ∧ R is parsed as P ∧ (Q ∧ R), so projections must follow that structure.

Takeaway

A conjunction is a pair of proofs. To prove P ∧ Q, prove P and prove Q. To use P ∧ Q, extract its left and right components. This pair-like behavior explains constructor, .left, .right, cases, and the angle-bracket notation.