# 4.19 Proof Irrelevance and Equality of Proofs

# 4.19 Proof Irrelevance and Equality of Proofs

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:

```lean
h₁ h₂ : P  ⟹  h₁ = h₂
```

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

```lean
#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:

```lean
structure NonZero where
  val : Nat
  prop : val ≠ 0
```

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

```lean
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:

```lean
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:

```lean
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:

```lean
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.