Skip to content

4.19 Proof Irrelevance and Equality of Proofs

In Lean, propositions live in `Prop`, a universe where proof irrelevance holds.

lean proof-assistant type-theory functional-programming

In Lean, propositions live in Prop, a universe where proof irrelevance holds. This means that any two proofs of the same proposition are considered equal. The identity of a proof object does not matter; only its existence matters. This property simplifies reasoning about equalities that involve proofs.

Proof irrelevance principle

The core idea is:

h₁ h₂ : P  ⟹  h₁ = h₂

for any proposition P. Lean provides this as a theorem:

#check proof_irrel
-- proof_irrel : ∀ {P : Prop} (h₁ h₂ : P), h₁ = h₂

This allows you to replace one proof with another without affecting correctness.

Rewriting with proof equalities

Suppose a structure contains a proof field:

structure NonZero where
  val : Nat
  prop : val ≠ 0

If two values differ only in the proof component, they are equal:

example (n : Nat)
  (h₁ h₂ : n ≠ 0) :
  NonZero.mk n h₁ = NonZero.mk n h₂ := by
  apply congrArg
  -- reduces to equality of proofs
  apply proof_irrel

In practice, extensionality combined with proof irrelevance eliminates proof components.

Simplifying structures with proofs

When using ext, proof fields often disappear automatically:

example (n : Nat)
  (h₁ h₂ : n ≠ 0) :
  { val := n, prop := h₁ } =
  { val := n, prop := h₂ } := by
  ext
  · rfl
  · apply proof_irrel

The data field is handled normally. The proof field collapses by irrelevance.

Interaction with rewriting

Proof irrelevance ensures that rewriting does not depend on which proof is used. This is important when multiple derivations exist:

example (P : Prop) (h₁ h₂ : P) :
  h₁ = h₂ :=
  proof_irrel _ _

As a result, you rarely need to track proof identities. Rewriting focuses on values and structure, not on proofs.

Dependent contexts

In dependent types, proof irrelevance stabilizes rewriting. If a type depends on a proof, replacing that proof does not change the type:

example (P : Prop) (h₁ h₂ : P)
  (Q : P -> Prop) :
  Q h₁ -> Q h₂ := by
  intro hq
  have : h₁ = h₂ := proof_irrel _ _
  cases this
  exact hq

The equality allows transport between dependent instances.

Limits of proof irrelevance

Proof irrelevance applies only to Prop. In Type, values are computational and their identity matters. For example, two lists with the same elements are not automatically equal; you must prove equality explicitly.

Practical guidance

  • Ignore differences between proofs unless they affect computation.
  • Use proof_irrel to resolve equality of proof fields.
  • Combine with ext to simplify structured equalities.
  • Avoid encoding data in Prop when identity matters.
  • Treat proofs as annotations, not as computational content.

Summary

Proof irrelevance collapses all proofs of a proposition into a single canonical identity. This removes unnecessary distinctions and simplifies rewriting in structures and dependent contexts. It allows you to focus on data and structure while treating proofs as interchangeable witnesses.