Skip to content

4.20 Decidable Equality and Boolean Bridges

Reasoning often alternates between propositional equality `a = b` and boolean equality `a == b`.

lean proof-assistant type-theory functional-programming

Reasoning often alternates between propositional equality a = b and boolean equality a == b. In Lean, this bridge is mediated by decidable equality. It allows you to move between computation and proof.

Decidable equality

A type has decidable equality if for any a b : α, you can decide whether a = b or a ≠ b. This is captured by:

Decidable (a = b)

For many standard types such as Nat, instances are available:

#check inferInstance : Decidable (3 = 5)

This enables case analysis on equality:

example (a b : Nat) : a = b ∨ a ≠ b := by
  by_cases h : a = b
  · left; exact h
  · right; exact h

The tactic by_cases relies on decidability.

Boolean equality

Boolean equality is written a == b. It computes to true or false. It is useful in executable code and algorithms.

#eval (3 == 3)   -- true
#eval (3 == 5)   -- false

However, == lives in Bool, while = lives in Prop. Bridging between them requires lemmas.

Bridging lemmas

Lean provides standard connections:

#check decide_eq_true_eq
-- (a == b) = true ↔ a = b

In practice, simp handles many conversions automatically:

example (a b : Nat) :
  (a == b) = true → a = b := by
  intro h
  simpa using h

And conversely:

example (a b : Nat) (h : a = b) :
  (a == b) = true := by
  simpa [h]

The simplifier knows how to translate between boolean and propositional equality when instances are available.

Using decide

The function decide converts a decidable proposition into a boolean:

#eval decide (3 = 3)   -- true
#eval decide (3 = 5)   -- false

This allows you to compute with propositions. It is useful when integrating proofs with executable code.

example (a b : Nat) :
  decide (a = b) = true → a = b := by
  intro h
  exact of_decide_eq_true h

Rewriting with boolean conditions

In proofs involving conditionals, boolean equality appears frequently:

example (a b : Nat) (h : a = b) :
  if a == b then 1 else 0 = 1 := by
  simp [h]

The rewrite converts a == b to true, and the conditional simplifies.

Case analysis on equality

Decidable equality supports branching:

example (a b : Nat) :
  (if a = b then 1 else 0) = (if b = a then 1 else 0) := by
  by_cases h : a = b
  · simp [h]
  · simp [h]

Each branch simplifies independently.

Practical guidance

  • Use propositional equality = for proofs.
  • Use boolean equality == for computation.
  • Bridge between them with simp, decide, or explicit lemmas.
  • Use by_cases for case splits on equality.
  • Normalize boolean expressions early to simplify goals.

Summary

Decidable equality connects computation and reasoning. It allows equality to be tested, branched on, and rewritten across the boundary between Bool and Prop. This bridge is essential for combining algorithms with formal proofs.