# 4.20 Decidable Equality and Boolean Bridges

# 4.20 Decidable Equality and Boolean Bridges

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:

```lean
Decidable (a = b)
```

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

```lean
#check inferInstance : Decidable (3 = 5)
```

This enables case analysis on equality:

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

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

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

In practice, `simp` handles many conversions automatically:

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

And conversely:

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

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

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

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

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