Contents

8. Decidable Equality and Small-Scale Reflection

The arc of construction closed with chapter 7; what remains is a coda, on a habit these lectures have practiced from the first page without naming it. Every question here has been answered twice over. Where a page needed certainty that runs, it pinned a #guard, a boolean program the build executes; where it needed certainty that explains, it stated a theorem, evidence the kernel checks. The conversion check of chapter 2 is one large boolean, answering definitional equality; the typing derivations of chapter 6 are evidence, data certifying their judgment. Neither kind subsumes the other: a boolean computes its verdict and carries no reasons, evidence carries the reasons and does not compute. Keeping each boolean wired to the proposition it answers is a discipline with a name, small-scale reflection, and a classic home: ssreflect, the proof language of the Mathematical Components library, whose name abbreviates exactly that phrase. This closing chapter rebuilds the discipline's central device on the course's own types, and ends where it has newly arrived, in Lean.

Evidence and computation

The divide is staged most plainly in PLFA's Decidable chapter, on the ordering of natural numbers: an inductive family whose two constructors are the two reasons one number can be at most another, beside a recursive boolean program that compares them, with functions converting each answer into the other. The chapter then defines the type that ends the rivalry, Dec A, an answer that is either yes with evidence or no with a refutation. Lean ships the same type under another name, and the course has been using it since its first #guard:

/--
info: inductive Decidable : Prop → Type
number of parameters: 1
constructors:
Decidable.isFalse : {p : Prop} → ¬p → Decidable p
Decidable.isTrue : {p : Prop} → p → Decidable p
-/
#guard_msgs in
#print Decidable

An answer of type Decidable p is evidence either way: a proof of p under isTrue, a refutation under isFalse. And the family lands in Type, not Prop, so programs may branch on which answer arrived; the choice chapter 6 made for its judgments, PLFA's Set said aloud, is made here by the standard library itself. The function decide projects the boolean out of the evidence, forgetting the reasons.

Deciding equality

Equality is the proposition these lectures have most often answered by boolean: the round-trip guards of chapter 1, the tree comparisons of chapter 2, the machine-agreement pins of chapter 7. The evidence-carrying version of such a comparison is a decision procedure for equality, and for a first-order type it writes itself by structural recursion. Here is the hand-written one for chapter 6's Ty:

def Ty.decEq : (a b : Ty) -> Decidable (a = b)
  | .unit, .unit => .isTrue rfl
  | .unit, .arrow _ _ => .isFalse nofun
  | .arrow _ _, .unit => .isFalse nofun
  | .arrow dom cod, .arrow dom' cod' =>
    match Ty.decEq dom dom', Ty.decEq cod cod' with
    | .isTrue rfl, .isTrue rfl => .isTrue rfl
    | .isFalse hd, _ => .isFalse fun h => hd (Ty.arrow.inj h).1
    | _, .isFalse hc => .isFalse fun h => hc (Ty.arrow.inj h).2

instance : DecidableEq Ty := Ty.decEq

Three moves cover everything. A constructor clash is refuted by nofun, the function with no cases, since no equation between different constructors can be matched. When both components decide isTrue, matching the proofs as rfl rewrites the goal until rfl closes it. And when either component fails, the generated injectivity theorem Ty.arrow.inj turns a claimed equality of arrows into the component equality the refutation refutes. The closing instance line registers the procedure as DecidableEq Ty; the deriving DecidableEq handler would have produced the same shape mechanically, and writing it once by hand is how to know what the handler writes.

example : Ty.arrow .unit .unit = .arrow .unit .unit := by decide

example : Ty.arrow .unit .unit ≠ .unit := by decide

#guard Ty.arrow .unit .unit == Ty.arrow .unit .unit

The tactic decide is the payoff of evidence that computes: it asks the kernel to run the decision procedure during type checking and accepts the evidence the run produces, a proof by computation, checked by the same judge as every theorem in these lectures. The last line runs the instance's boolean through the evaluator instead, which is all #guard ever did. The wall of chapter 1 reappears from the proof side: a partial def exports no equations, so the kernel cannot run it, and decide inherits exactly the limitation that stopped rfl there, while #guard, running the untrusted evaluator, never notices.

Small-scale reflection

A decision procedure bundles the boolean with its proposition, but most booleans arrive unbundled: written for speed, or written first, like every comparison function in this course. In the Mathematical Components library the bundling is a separate, reusable statement: ssreflect's reflect P b is the inductive predicate asserting that the proposition P holds exactly when the boolean b is true. Rebuilt over the course's Lean, it is an indexed family:

inductive Reflect (p : Prop) : Bool -> Prop where
  | isTrue (h : p) : Reflect p true
  | isFalse (h : ¬p) : Reflect p false

The two constructors mirror Decidable's, and the one change is load-bearing: the boolean is an index, so stating Reflect p b about a particular program b is a theorem tying that program to that proposition. Lean's Decidable then turns out to have been a reflection view all along:

theorem Reflect.of (p : Prop) [inst : Decidable p] : Reflect p (decide p) :=
  match inst with
  | .isTrue h => .isTrue h
  | .isFalse h => .isFalse h

example : Reflect (Ty.arrow .unit .unit = .arrow .unit .unit) true :=
  Reflect.of _

The match sends each answer to the constructor of the same name, and the index decide p reduces as the instance does, which is why the example can state its view at the literal true. Two bridges complete the toolkit:

theorem Reflect.iff {p : Prop} {b : Bool} : Reflect p b -> (p <-> b = true)
  | .isTrue h => ⟨fun _ => rfl, fun _ => h⟩
  | .isFalse h => ⟨fun hp => absurd hp h, nofun⟩

theorem Reflect.of_iff {p : Prop} {b : Bool} (h : p <-> b = true) :
    Reflect p b :=
  match b, h with
  | true, h => .isTrue (h.mpr rfl)
  | false, h => .isFalse fun hp => nomatch h.mp hp

One direction eliminates a view into the biconditional it asserts; the other introduces a view from that biconditional, case-splitting on the boolean. These are the moves an ssreflect proof makes every few tokens, switching between the proposition it reasons about and the boolean it computes with, so the language spells the switch with a single slash. The same design has arrived in Lean: LeanSSR carries this Reflect as a type class with the boolean an output parameter, found by instance search rather than stated by hand, and ports the tactic language around it. The accompanying paper, Small Scale Reflection for the Working Lean User, doubles as a tutorial and a measurement: sequence lemmas ported from Mathematical Components, finite-set proofs redone against Mathlib, and the proof sizes compared.

What alpha-equivalence reflects

A reflection view forces one honest question: which proposition does this boolean answer? The sharpest specimen in these lectures is chapter 2's alphaEq, the comparison that deliberately ignores binder names. Put it beside propositional equality on the same two terms:

#guard Tm.alphaEq (.lam "x" none (.var 0)) (.lam "y" none (.var 0))

example : Tm.lam "x" none (.var 0) ≠ .lam "y" none (.var 0) :=
  fun h => absurd (Tm.lam.inj h).1 (by decide)

Both answers are right. The two lambdas are the same program, which is the question alphaEq answers; they are different trees, because the printing names differ, which is the question = asks about Tm, and the term proof splits the lambda with its injectivity theorem and refutes "x" = "y" by decide, string equality being decidable too. So Reflect (t = u) (Tm.alphaEq t u) is simply false, and the view alphaEq does support, equality up to printing names, is a relation these lectures never wrote down. Reflection is the discipline of writing it down. The conversion check of chapter 2 is the same confession at full scale: the boolean it computes answers definitional equality, and the theorem naming that connection is the correctness of normalization by evaluation itself, metatheory these lectures gesture at and do not prove.

Further reading