Module 5 · Lesson 2

decide — Decidable Propositions

decide proves decidable propositions by computation. If Lean can compute whether something is true or false, decide handles it.

What is Decidability?

A proposition is decidable if there's an algorithm to determine whether it's true or false. Lean has aDecidable typeclass for this:

lean

1-- The Decidable typeclass
2#check @Decidable
3-- class Decidable (p : Prop) where
4--   decide : Bool
5--   -- with proof that decide = true ↔ p
6
7-- Many propositions are decidable
8#check (inferInstance : Decidable (2 + 2 = 4))
9#check (inferInstance : Decidable (5 < 10))
10#check (inferInstance : Decidable ([1, 2, 3].contains 2))

Key Takeaway

decide works on any proposition with aDecidable instance. It evaluates the decision procedure and uses the result as a proof.

Basic Usage

lean

1-- Numeric comparisons
2example : 2 + 2 = 4 := by decide
3example : 10 > 5 := by decide
4example : 100 % 7 = 2 := by decide
5
6-- Boolean conditions
7example : true ∧ true := by decide
8example : ¬false := by decide
9example : true ∨ false := by decide
10
11-- List operations
12example : [1, 2, 3].length = 3 := by decide
13example : [1, 2, 3].contains 2 = true := by decide
14example : [1, 2].head? = some 1 := by decide

decide vs rfl

lean

1-- rfl: definitional equality (computation)
2example : 2 + 2 = 4 := rfl
3
4-- decide: also works, but through Decidable
5example : 2 + 2 = 4 := by decide
6
7-- decide can prove more than rfl
8example : ¬(3 = 5) := by decide  -- decide works
9-- example : ¬(3 = 5) := rfl     -- rfl wouldn't work directly
10
11-- rfl is lighter, decide is more powerful
12example : 1 < 2 := by decide
13-- example : 1 < 2 := rfl  -- wouldn't work (< isn't definitional)

Decidable Instances

lean

1-- Many standard types have Decidable instances
2
3-- Equality on basic types
4example : "hello" = "hello" := by decide
5example : 'a' = 'a' := by decide
6
7-- Comparisons on Nat, Int
8example : (5 : Nat) ≤ 10 := by decide
9example : ((-3) : Int) < 0 := by decide
10
11-- List membership (for Decidable equality elements)
12example : 3 ∈ [1, 2, 3, 4] := by decide
13example : 5 ∉ [1, 2, 3, 4] := by decide
14
15-- Option
16example : (some 5 : Option Nat) ≠ none := by decide

ℹ

decide runs at kernel level—it actually computes the answer. This means it can be slow for large computations.

When decide Fails

lean

1-- Variables aren't decidable (can't compute)
2-- example (n : Nat) : n = n := by decide  -- fails
3example (n : Nat) : n = n := rfl  -- use rfl instead
4
5-- Functions without Decidable equality
6-- example (f g : Nat → Nat) : f = f := by decide  -- fails
7
8-- Propositions without Decidable instance
9-- example (P : Prop) : P ∨ ¬P := by decide  -- fails (classical)

native_decide

native_decide uses compiled native code for faster computation:

lean

1-- native_decide is faster for large computations
2example : (List.range 1000).length = 1000 := by native_decide
3
4-- Primality testing
5example : Nat.Prime 97 := by native_decide
6example : ¬Nat.Prime 100 := by native_decide
7
8-- Large list operations
9example : (List.range 100).sum = 4950 := by native_decide

⚠

native_decide trusts the compiler—it doesn't verify the computation in the kernel. Use decidefor critical proofs.

Deep Dive: How decide Works

decide extracts a proof from aDecidable instance:

lean

1-- Decidable provides a Bool and a proof
2-- If the Bool is true, we get a proof of p
3-- If false, we get a proof of ¬p
4
5-- decide uses this:
6#check @of_decide_eq_true
7-- of_decide_eq_true : decide p = true → p
8
9-- So decide:
10-- 1. Evaluates "decide p" to true or false
11-- 2. If true, applies of_decide_eq_true
12-- 3. If false, applies of_decide_eq_false to prove ¬p

Custom Decidable Instances

lean

1-- Define your own decidable propositions
2structure Person where
3  name : String
4  age : Nat
5deriving DecidableEq  -- auto-generate Decidable (a = b)
6
7example : (Person.mk "Alice" 30) = (Person.mk "Alice" 30) := by decide
8example : (Person.mk "Alice" 30) ≠ (Person.mk "Bob" 25) := by decide
9
10-- Custom decidable predicate
11def isEven (n : Nat) : Bool := n % 2 = 0
12
13instance : Decidable (isEven n = true) := 
14  inferInstance  -- Bool equality is decidable
15
16example : isEven 4 = true := by decide

Examples

Finite Verification

lean

1-- Check a property for specific values
2example : ∀ n ∈ [0, 1, 2, 3, 4], n < 5 := by decide
3
4-- Verify a small theorem instance
5example : ∀ a ∈ [true, false], ∀ b ∈ [true, false], a && b = b && a := by decide

Array Bounds

lean

1-- Prove array operations are valid
2def myArray : Array Nat := #[1, 2, 3, 4, 5]
3
4example : myArray.size = 5 := by decide
5example : myArray[0]! = 1 := by native_decide

String Operations

lean

1example : "hello".length = 5 := by decide
2example : "hello".startsWith "hel" := by decide
3example : "world".contains 'o' := by decide

omega Next: ring