Practise it in the Academy:Decide a finite fact →

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. Use it for concrete facts that can be checked by evaluation, such as a statement about specific small numbers.

The Idea: Computation as Proof

Some mathematical statements can be checked just by calculating. Is 2 + 2 = 4? Calculate it and see. Is 15 divisible by 3? Check if 15 % 3 = 0. Thedecide tactic turns this intuition into actual proofs.

Instead of constructing a proof by hand, decide asks: "Can I just compute whether this is true?" If yes, the computation itself becomes the proof.

What is Decidability?

A proposition is decidable if there's an algorithm to determine whether it's true or false. In Lean, this is captured by theDecidable typeclass:

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))

When a proposition has a Decidable instance, Lean can evaluate it to true or false. The decide tactic uses this evaluation as a proof.

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
5example : 17 ≠ 18 := by decide
6
7-- Boolean conditions
8example : true ∧ true := by decide
9example : ¬false := by decide
10example : true ∨ false := by decide
11example : false → true := by decide  -- Implication with false premise
12
13-- List operations (with finite lists)
14example : [1, 2, 3].length = 3 := by decide
15example : [1, 2, 3].contains 2 = true := by decide
16example : [1, 2].head? = some 1 := by decide
17example : ([] : List Nat).isEmpty = true := by decide  -- the element type must be known

decide vs rfl

Both decide and rfl can prove things by computation, but they work differently:

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-- ✅ decide handles inequalities
12example : 1 < 2 := by decide
13-- example : 1 < 2 := rfl  -- wouldn't work (< isn't definitional)
14
15-- ✅ decide can prove membership
16example : 3 ∈ [1, 2, 3, 4] := by decide
17-- This would be harder with rfl

When to Use Which?

Situation	Use
Equality of computed values	`rfl` (lighter)
Inequalities (<, ≤, etc.)	`decide`
Negations (¬)	`decide`
List/array membership	`decide`
Large computations	`native_decide`

Decidable Instances: What Works

Many common types and operations have Decidable instances in the standard library:

lean

1-- Equality on basic types
2example : "hello" = "hello" := by decide
3example : 'a' = 'a' := by decide
4example : (5 : Nat) = 5 := by decide
5
6-- Comparisons on ordered types
7example : (5 : Nat) ≤ 10 := by decide
8example : ((-3) : Int) < 0 := by decide
9
10-- List membership (for elements with DecidableEq)
11example : 3 ∈ [1, 2, 3, 4] := by decide
12example : 5 ∉ [1, 2, 3, 4] := by decide
13example : 'x' ∈ ['a', 'b', 'x', 'y'] := by decide
14
15-- Option comparisons
16example : (some 5 : Option Nat) ≠ none := by decide
17example : (none : Option Nat) = none := by decide
18
19-- Boolean expressions
20example : ([1,2,3].all (· < 10)) = true := by decide
21example : ([1,2,3].any (· > 2)) = true := by decide

When decide Fails

decide fails when the proposition involves variables (unknown values) or types without Decidable instances:

lean

1-- ❌ Variables: Can't compute without knowing the values
2-- example (n : Nat) : n = n := by decide  -- Fails!
3example (n : Nat) : n = n := rfl  -- Use rfl instead
4
5-- ❌ Functions don't have DecidableEq by default
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 logic)
10
11-- ❌ Large structures without deriving DecidableEq
12structure Person where
13  name : String
14  age : Nat
15-- example : Person.mk "Alice" 30 = Person.mk "Alice" 30 := by decide  -- Fails!

ℹ

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

native_decide: For Large Computations

native_decide uses compiled native code instead of Lean's kernel, making it much faster for expensive computations:

lean

1-- native_decide is faster for large computations
2example : (List.range 1000).length = 1000 := by native_decide
3
4-- Trial division (expensive to check in the kernel):
5-- 97 has no divisor from 2 to 96, and 100 has one
6example : (List.range 95).all (fun k => 97 % (k + 2) != 0) := by native_decide
7example : ¬(List.range 98).all (fun k => 100 % (k + 2) != 0) := by native_decide
8
9-- Large list operations
10example : (List.range 100).sum = 4950 := by native_decide
11
12-- Checking all elements of a large list
13example : (List.range 50).all (· < 100) := by native_decide

⚠

native_decide trusts the compiler—it doesn't verify the computation in the kernel. For critical proofs where correctness is paramount, prefer decide.

Creating Decidable Instances

For your own types, you can derive or define Decidableinstances to enable decide:

Deriving DecidableEq

lean

1-- Automatically generate equality decisions
2structure Person where
3  name : String
4  age : Nat
5deriving DecidableEq  -- Now decide works on Person equality!
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-- Works for enums too
11inductive Color
12  | red | green | blue
13deriving DecidableEq
14
15example : Color.red ≠ Color.blue := by decide

Custom Decidable Instances

lean

1-- Define your own decidable predicates
2def isEven (n : Nat) : Prop := n % 2 = 0
3
4-- Make it decidable by connecting to Bool
5instance (n : Nat) : Decidable (isEven n) := 
6  if h : n % 2 = 0 then isTrue h else isFalse h
7
8example : isEven 4 := by decide
9example : ¬isEven 5 := by decide

Deep Dive: How decide Works Under the Hood

decide extracts a proof from aDecidable instance through these steps:

Find a Decidable p instance for proposition p
Evaluate decide p to get true or false
If true, extract the proof of p from the instance
If false, extract the proof of ¬p

lean

1-- The key lemma used by decide
2#check @of_decide_eq_true
3-- of_decide_eq_true : decide p = true → p
4
5-- So decide:
6-- 1. Evaluates "decide p" to true (or false)
7-- 2. If true, applies of_decide_eq_true
8-- 3. The kernel verifies that decide p really equals true
9
10-- This is why it's slower than rfl—it involves more steps

Practical Examples

Finite Verification

Sometimes you need to check a property holds for all values in a finite set:

lean

1-- Check a property for specific values
2example : ∀ n ∈ [0, 1, 2, 3, 4], n < 5 := by decide
3
4-- Verify a truth table
5example : ∀ a ∈ [true, false], ∀ b ∈ [true, false],
6    (a && b) = (b && a) := by decide  -- parentheses: = binds tighter than &&
7
8-- Check small cases exhaustively
9example : ∀ n ∈ [0, 1, 2, 3], n * n ≤ 9 := by decide

Array and String Operations

lean

1-- Prove array operations are valid
2def myArray : Array Nat := #[1, 2, 3, 4, 5]
3
4example : myArray.size = 5 := by native_decide
5
6-- String checks: length reduces in the kernel, but most String
7-- functions do not, so decide gets stuck and native_decide is needed
8example : "hello".length = 5 := by decide
9example : "hello".startsWith "hel" := by native_decide
10example : "world".contains 'o' := by native_decide
11example : "lean4".endsWith "4" := by native_decide

Simple Logic

lean

1-- Quick proofs of simple logical facts
2example : ¬(true ∧ false) := by decide
3example : true ∨ false := by decide
4example : false → true := by decide
5example : ¬¬true := by decide
6
7-- De Morgan's law for specific values
8example : ¬(true ∧ false) = (¬true ∨ ¬false) := by decide

Common Mistakes

Using decide with Variables

lean

1-- ❌ Wrong: can't decide facts about unknown values
2-- example (n : Nat) : n = n := by decide
3
4-- ✅ Right: use rfl for reflexive equality
5example (n : Nat) : n = n := rfl

Expecting decide to Handle Symbolic Reasoning

lean

1-- ❌ Wrong: decide only computes, doesn't reason symbolically
2-- example (n : Nat) : n + 0 = n := by decide
3
4-- ✅ Right: use simp or omega for symbolic properties
5example (n : Nat) : n + 0 = n := by simp
6example (n : Nat) : n + 0 = n := by omega

Exercise 1: Basic Decidability

Use decide to prove this membership fact.

lean

1example : 'a' ∈ ['a', 'b', 'c'] := by decide

Exercise 2: Disjunction

Use decide to prove a small propositional statement.

lean

1example : (2 = 3) ∨ (2 = 2) := by decide

Exercise 3: String Check

Use decide to verify a string property.

lean

1example : "hello".length > 3 := by decide

omega Next: simp Attributes