Proof irrelevance and subsingleton elimination

Plain-language version: Two kinds of equality

Two rules govern how proofs behave in Lean. Definitional proof irrelevance makes any two proofs of the same proposition definitionally equal. Restricted elimination allows a proof to be taken apart to produce data only when the proposition is a subsingleton, one that by its shape can have at most one proof. The first rule says that the content of a proof never matters; the second is what keeps that consistent. This page states both rules, lists which propositions pass the test, explains why the test is needed, and sets out the cost: together with the accessibility predicate, the two rules make Lean's definitional equality undecidable.

Definitional proof irrelevance

Carneiro's presentation of Lean's type theory includes the rule

$\frac{\Gamma ⊢p:\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}\Gamma ⊢h:p\Gamma ⊢h^{\prime }:p}{\Gamma ⊢h\equiv h^{\prime }}$

It is a rule of definitional equality, so the checker applies it during conversion, without any proof term. The reference manual lists it among the defining properties of Prop, beside the erasure of propositions from compiled code.

example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl

example (h₁ h₂ : 0 < 5) : (⟨5, h₁⟩ : {n : Nat // 0 < n}) = ⟨5, h₂⟩ := rfl

example (α : Type) (h₁ h₂ : Nonempty α) : Classical.choice h₁ = Classical.choice h₂ := rfl

All three are accepted. The second shows the practical use: elements of a subtype are equal as soon as their values are, whatever proofs they carry. The third shows that global choice returns one element per type, not one per proof. Carneiro, writing in 2019, notes that Coq then had proof irrelevance only as an axiom asserting a propositional equality, and calls Lean's definitional version "a major departure for the theory".

Why elimination must be restricted

Suppose a program could inspect which constructor built a proof of a disjunction, and so return true on Or.inl trivial : True ∨ True and false on Or.inr trivial. Those two proofs have the same type, so proof irrelevance makes them definitionally equal, the two results would be definitionally equal, and true = false would follow by rfl. One of the two rules has to give way. Lean keeps proof irrelevance and forbids the inspection: having been given a proof, a program must not be able to tell which proof it received. Lean refuses the function:

def which (h : True ∨ True) : Bool :=
  match h with
  | .inl _ => true
  | .inr _ => false

The message begins Tactic `cases` failed with a nested error: and continues Tactic `induction` failed: recursor `Or.casesOn` can only eliminate into `Prop`. The restriction is visible in the recursors themselves. The motive of Or.rec and of Exists.rec returns Prop, while the motives of True.rec, False.rec and And.rec return an arbitrary Sort u_1:

#check @True.rec
#check @False.rec
#check @And.rec
#check @Or.rec
#check @Exists.rec

@True.rec : {motive : True → Sort u_1} → motive True.intro → (t : True) → motive t
False.rec : (motive : False → Sort u_1) → (t : False) → motive t
@And.rec : {a b : Prop} → {motive : a ∧ b → Sort u_1} → ((left : a) → (right : b) → motive ⋯) → (t : a ∧ b) → motive t
@Or.rec : ∀ {a b : Prop} {motive : a ∨ b → Prop},
  (∀ (h : a), motive ⋯) → (∀ (h : b), motive ⋯) → ∀ (t : a ∨ b), motive t
@Exists.rec : ∀ {α : Sort u_1} {p : α → Prop} {motive : Exists p → Prop},
  (∀ (w : α) (h : p w), motive ⋯) → ∀ (t : Exists p), motive t

The rule

An inductive type in Prop may be eliminated into any universe, which is large elimination, when it is a syntactic subsingleton. The reference manual states the test as two conditions: there is at most one constructor, and every argument of that constructor either has a proposition as its type or is a parameter or an index of the type. Carneiro's formulation is that there is at most one constructor and every non-recursive argument of it either has a proposition as its type or appears directly in the constructor's output type. Otherwise the motive of the recursor must return Prop. The test is deliberately conservative: it does not ask for a proof that the proposition has at most one proof, only for a shape that guarantees it.

The standard cases:

• True has one constructor with no arguments, and False has none. From h : False, h.elim produces an element of any type.
• And has one constructor whose arguments are proofs.
• Eq has one constructor, Eq.refl a, whose argument is fixed by the type's parameters. This is why a proof of an equation can rewrite the type of data, the operation called transport on propositional equality.
• Acc, the accessibility predicate, has one constructor Acc.intro x h. Its argument x appears in the result type Acc r x and its argument h is a proof, so it too eliminates into any universe. Carneiro singles it out as the source of proof by well-founded recursion.

Or fails because it has two constructors. Exists and Nonempty fail because their constructor stores a witness that is neither a proof nor part of the type. Their proofs therefore cannot yield the witness as data; that requires Classical.choose, as on classical logic from choice. Where the witness is wanted as data, the subtype {x // p x}, which lives in Type, carries it.

def fromFalse (h : False) : Nat := h.elim

def castAlong {α β : Type} (h : α = β) (x : α) : β := h ▸ x

def bothThen {p q : Prop} (h : p ∧ q) (f : p → q → Nat) : Nat :=
  match h with
  | ⟨hp, hq⟩ => f hp hq

set_option pp.proofs true in
#check @Acc.rec

@Acc.rec : {α : Sort u_2} →
  {r : α → α → Prop} →
    {motive : (a : α) → Acc r a → Sort u_1} →
      ((x : α) →
          (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (h y a)) → motive x (Acc.intro x h)) →
        {a : α} → (t : Acc r a) → motive a t

For subsingletons the checker also applies an extra reduction, which Carneiro calls K-like reduction: by proof irrelevance the major premise may be replaced by the constructor, and the ordinary computation rule then fires. It applies only when every argument of the constructor can be read off the type, which is the reason for the shape of the test. For Eq it makes transport along any proof of a = a reduce to the identity.

The cost: definitional equality is undecidable

Proof irrelevance and the large eliminator of Acc together break the decidability of definitional equality. Carneiro's argument runs as follows. From a proof a : Acc r x one can project, with the eliminator, a function giving accessibility of every smaller element; call it a.inv. Rebuilding with the constructor gives a proof of the same proposition, so by proof irrelevance a and Acc.intro x a.inv are definitionally equal:

example {α : Sort u} {r : α → α → Prop} {x : α} (a : Acc r x) :
    a = Acc.intro x (fun _ h => a.inv h) := rfl

That step turns any proof, even an opaque variable, into a constructor on which the recursor can compute. Now take a decidable predicate $P$ on the natural numbers, such as "machine $M$ runs for at least $n$ steps without halting", and a function $f$ defined by recursion on Acc for the relation $>$, which at $n$ returns a fixed value if $P(n)$ fails and otherwise calls itself at $n+1$. The relation $>$ on the natural numbers is not well founded, so a hypothesis $a:\mathrm{A}\mathrm{c}\mathrm{c}(>)0$ is unprovable, but definitional equality is judged in every context, inconsistent ones included. In that context each use of the equation above lets $f0a$ take one more step of the search. If $P(n)$ fails for some $n$, the search ends and $f0a$ is definitionally equal to the fixed value; if $P$ holds everywhere, every term definitionally equal to $f0a$ still contains a call of $f$. Deciding that one definitional equality would decide whether $M$ halts.

Lean's checker cannot implement an undecidable relation. It implements a decidable approximation, which Carneiro calls algorithmic equality, and the two must differ: the chain of equalities above holds step by step, but the checker, which does not perform the "creative" re-expansion of a normal term, does not relate its two ends. Algorithmic equality is therefore not transitive. The reference manual records the same fact: definitional equality as Lean checks it is reflexive and symmetric, but not transitive. Carneiro also shows that, measured against the algorithmic relation, typing fails subject reduction: a term can be well typed and reduce to one that the checker rejects.

None of this lets the checker accept a false theorem. Algorithmic equality implies the ideal definitional equality for well-typed terms, so whatever the checker accepts is derivable in the theory; Carneiro uses exactly this step in his consistency proof. The defect is incompleteness, not unsoundness. Abel and Coquand later showed a related failure: with an impredicative Prop and proof-irrelevant equality, reduction need not terminate at all. That result, and why the checker remains sound regardless, are treated on consistency and the metatheory. Abel and Coquand also note the other design: Agda and Coq had recently gained a proof-irrelevant universe of strict propositions in which equality can be defined but cannot be eliminated into types that are not themselves strict propositions, and under that restriction normalisation and decidable type checking have been proved for the predicative case.

Next

Consistency and the metatheory asks what is known about the soundness of the whole system.