A Fist Concrete Proof#

We will demonstrate not only how to prove properties in Lean but also why the methods work, connecting the seemingly magical world of tactics to the solid ground of proof objects, with which we are more familiar from Agda.

We'll start by reviewing a concrete, fundamental example: computing the probability of choosing a specific binary vector (key) at random.

This will allow us to bring the ideas down to earth and immediately dive into and discuss the tactic vs. proof object dichotomy.

Let's start with the

Claim. The probability of randomly choosing a specific 3-bit key is 1/8.

In Lean, the theorem and its tactic-based proof are very concise.

But before we get to the proof, we need to formally state the claim!

For this we first define the uniform distribution over keys as follows.

import Mathlib.Probability.Distributions.Uniform

-- (Assuming a file OTP.Basic with the definition of Key)
open OTP
-- Recall, we define `Key n` as vectors of booleans.
-- This is equivalent to `Fin n → Bool` or other n-bit types.

-- Here is the uniform distribution over keys of length n.
noncomputable def μK {n : ℕ} : PMF (Key n) := PMF.uniformOfFintype (Key n)

Now we can state the claim along with its short proof.

-- Claim: the probability of choosing key [true, false, true] is 1/8.
example : μK ⟨[true, false, true], rfl⟩ = (1/8 : ENNReal) :=
 -- and here's the tactic-based proof in Lean:
  by simp [μK, PMF.uniformOfFintype_apply]; rfl

This is great for a user who knows what simp means and does, but it may seem like a magical incantation for the newcomer. So we should unpack it.

Also, we should address the following natural question after dissecting the proof.

Why is our uniform distribution marked noncomputable?

Dissecting the Proof#

Deconstructing `simp`#

The simp tactic is an automated rewriter.

It tries to simplify the main goal by applying a list of theorems (called a "simpset") from left to right, over and over, until no more simplifications can be made.

When you write simp [foo, bar], you are telling Lean:

"Please use your standard simpset, plus the definitions/lemmas foo and bar to the set of tools you can use to simplify or reduce the goal."

Step 1: Unfolding the Definition of `μK`#

Let's break down the proof step-by-step, showing the tactic at each stage, and then discuss the proof object it's building.

🥅 Goal State Before the Tactic 🥅

⊢ μK ⟨[true, false, true], rfl⟩ = 1 / 8

Here, ⊢ indicates the goal we are trying to prove.

The Tactic simp [μK] or rw [μK]

tells Lean to substitute μK with its definition.

🥅 Goal State After the Tactic 🥅

⊢ PMF.uniformOfFintype (Key 3) ⟨[true, false, true], rfl⟩ = 1 / 8

Why this works#

Looking under the hood,

μK is defined as PMF.uniformOfFintype (Key n).
simp (and the more targeted rw) can access all definitions in context.
It sees the term μK in the goal and replaces it with its definition; a simple substitution.

The Equivalent Proof Term

In a term-based proof, the substitution is achieved using functions that show equality is respected by function application.

If we have a proof h : μK = PMF.uniformOfFintype (Key 3), we can use it to rewrite the goal.

The definition itself provides this proof h. The core idea is Eq.subst or Eq.rec.

A proof term for just this step would look like this:

-- Let P be the property we are trying to prove for the definition.
-- P := λ x => x ⟨[true, false, true], _⟩ = 1/8
-- Our goal is `P (μK)`
-- The definition of μK gives us `proof_of_definition : μK = PMF.uniformOfFintype (Key 3)`

-- The new proof term is:
Eq.subst proof_of_definition (new_goal : P (PMF.uniformOfFintype (Key 3)))

...which is a bit clunky.

A more common term-based idiom is to simply start with the definition already unfolded.

The tactic rw is essentially a mechanical way of applying Eq.subst.

Lean Feature: revealing proof terms

We can get Lean to reveal proof objects that are generated by tactics, and sometimes the result is even readable and comprehensible by mortal human beings.

The Feature

Lean has a tactic called show_term.

It executes the tactics within it and then, instead of closing the goal, it prints the raw proof term that was generated.

How to Demonstrate It:

Pick a simple proof, like our very first one.

In VS Code, change the proof to

-- Our theorem: The probability of the key [true, false, true] is 1/8.
example : μK ⟨[true, false, true], rfl⟩ = (1/8 : ENNReal) := by
  show_term -- Add this tactic
    simp [μK, PMF.uniformOfFintype_apply]; rfl

When the cursor is on the show_term line, the "Lean Infoview" panel will display the generated proof term.
Warning (and the point)

The term is long, ugly, and full of machine-generated names.

It looks something like Eq.trans (PMF.uniformOfFintype_apply ... ) (congr_arg Inv.inv (Fintype.card_vector ...)).
Explanation

For Agda developers, it's natural to ask: where is the proof object?

Tactic proofs generate proof objects. We can ask Lean to show us the term it generated using the show_term tactic.

Apparently, the result is extremely verbose and not really meant for human consumption.

This is the fundamental trade-off: tactics let us write short, conceptual proofs at the expense of creating these complex, machine-readable proof terms under the hood.

Step 2: Unfolding Definition of Uniform PMF#

Now we apply the definition of what uniformOfFintype evaluates to for a given input.

🥅 Goal State Before the Tactic 🥅

⊢ PMF.uniformOfFintype (Key 3) ⟨[true, false, true], rfl⟩ = 1 / 8

The Tactic simp [PMF.uniformOfFintype_apply]

The lemma PMF.uniformOfFintype_apply states:

If a is an inhabitant of the finite type α, then

PMF.uniformOfFintype α a is equal to (Fintype.card α)⁻¹.

🥅 Goal State After the Tactic 🥅

⊢ (Fintype.card (Key 3))⁻¹ = 1 / 8

Why this works#

Looking under the hood,

simp finds a lemma PMF.uniformOfFintype_apply in the library;
This lemma matches the pattern PMF.uniformOfFintype (Key 3) ... on the lhs of our goal;
simp using the lemma to rewrites the lhs as (Fintype.card (Key 3))⁻¹.

The Equivalent Proof Term

This is a direct application of the lemma.

The proof term for the rewrite is PMF.uniformOfFintype_apply (Key 3) ⟨...⟩.

Applying this equality to our goal transforms it.

A proof would look like:

-- h₁ : PMF.uniformOfFintype (Key 3) ⟨...⟩ = (Fintype.card (Key 3))⁻¹
-- This comes from the lemma PMF.uniformOfFintype_apply
-- We use this to transform the goal into proving:
-- ⊢ (Fintype.card (Key 3))⁻¹ = 1 / 8

This is again a form of Eq.subst.

The rw tactic is the most direct parallel: rw [PMF.uniformOfFintype_apply].

Step 3: Computing the Cardinality and Final Simplification#

This is where simp really shines by combining computation and proof.

🥅 Goal State Before the Tactic 🥅

⊢ (Fintype.card (Key 3))⁻¹ = 1 / 8

The Tactic simp; rfl

We don't need to provide any more lemmas. The rest is handled by Lean's built-in capabilities.

🥅 Goal State After the Tactic 🥅

The goal is solved!

Why this works#

Looking under the hood,

Typeclass Inference. Lean needs to know the size of Key 3. The type Key 3, which is Vector Bool 3, has an instance of the Fintype typeclass. This instance provides a computable function to get the number of elements.
Computation. The simp tactic (or the norm_num tactic it calls internally) executes the cardinality function, simplifying Fintype.card (Key 3) to 8. The goal becomes (8 : ENNReal)⁻¹ = 1/8.
Normalization. The simp engine has lemmas about ENNReal arithmetic. It knows that 8⁻¹ is the same as 1/8.
Reflexivity. The goal becomes 1/8 = 1/8. simp reduces both sides to the same term, and the final rfl tactic confirms this equality and closes the goal.

The Equivalent Proof Term

A term-based proof must explicitly provide proofs for each of these steps.

-- A lemma that proves card (Key 3) = 8
have card_proof : Fintype.card (Key 3) = 8 := by-- ... proof using vector cardinality lemmas

-- We use this proof to rewrite the goal
-- The goal becomes ⊢ 8⁻¹ = 1/8
-- This is true by reflexivity, since 8⁻¹ is just notation for 1/8 in ENNReal.
-- The final term is:
rfl

The simp tactic automated the process of finding card_proof, applying it, and then seeing that the result was definitionally equal.

The full proof term generated by our original by simp [...] is effectively a composition of all these steps, applying congruence lemmas (congr_arg) and transitivity (Eq.trans) to chain all the intermediate equalities together into one grand proof that the starting expression equals the final one.

Why noncomputable?

This is subtle! Even though we're dealing with finite types, these definitions are noncomputable because:

Real Number Arithmetic
```
noncomputable def μK {n : ℕ} : PMF (Key n) := uniformOfFintype (Key n)
```
The probability values are in ℝ≥0∞ (extended non-negative reals), not rationals:
- 1/2ⁿ is computed as real division, not rational division
- Real arithmetic is inherently noncomputable in constructive mathematics
- Even though we "know" the answer is rational, the type system uses reals
Infinite Summations

Even for finite types, PMF uses infinite summation machinery:
```
∑' a : α, p a  -- This is an infinite sum operator
```
- The ∑' notation works for both finite and infinite types.
- It's defined using limits and topology.
- Even when α is finite, we use the general machinery.
Classical Logic

PMF operations often use classical logic (excluded middle):
```
open Classical  -- Needed for many probability operations
```
This makes things noncomputable in Lean's constructive logic.

Why Can We Still Prove `= 1/8`?#

Here's the beautiful part:

noncomputable doesn't mean we can't reason about values!

Proofs vs Computation#

-- We can't compute this:
#eval μK ⟨[true, false, true], by decide⟩  -- Error: noncomputable

-- But we CAN prove this:
example : μK ⟨[true, false, true], by decide⟩ = 1/8 := by
  simp [μK, uniformOfFintype_apply]
  -- Proves that (card (Key 3))⁻¹ = 8⁻¹ = 1/8

What's Happening?#

Definitional unfolding: Even though μK is noncomputable, we can unfold its definition in proofs.
Symbolic reasoning: We prove 1/card(Key 3) = 1/8 symbolically, not by computation.
Type class inference: Lean knows Fintype (Key 3) and can reason about cardinalities.
Real number lemmas: Mathlib has lemmas about real arithmetic that we use in proofs.

The Philosophical Point#

The separation of computation and reasoning is fundamental.

Computation: Running an algorithm to get a concrete answer.
Reasoning: Proving properties about mathematical objects.

In formal mathematics, we often work with noncomputable objects (like real numbers, infinite sets, choice functions) but can still prove precise theorems about them.

Summary#

In Lean, probability distributions are functions from outcomes to probabilities, bundled with a proof that probabilities sum to 1.
Even though we work with finite spaces, these are marked noncomputable because they use real number arithmetic and infinite summation machinery.
This doesn't limit our reasoning---we can still prove exact results like "each key has probability 1/8."
The distinction between computation and proof is fundamental: we reason symbolically about these mathematical objects without needing to compute their values.
Practical Analogy
- Computable: a calculator gives you 0.125 when you type 1 ÷ 8.
- Noncomputable with proofs: we can show algebraically that 1/8 = 0.125 without calculating
PMFs in Lean are the second kind---we work with them symbolically and prove properties, rather than computing decimal expansions.

Proof Term Perspective#

Tactic Proof Step	What it Does	Underlying Proof Term Concept
`by simp [μK, ...]`	A powerful, automatic rewrite sequence.	A complex, generated term chaining together multiple equalities; a function that takes no arguments and returns a proof of `LHS = RHS`.
`rw [μK]`	Replaces `μK` with its definition.	Application of `Eq.subst` or `Eq.rec` using definitional equality of `μK`.
`rw [lem]`	Rewrites goal using a proven lemma `lem : A = B`.	Application of `Eq.subst` using lemma `lem` as proof of equality.
`rfl`	Solves a goal of the form `A = A`.	The constructor for equality, `Eq.refl A`; it's a direct proof object.

From a constructive "proof term" perspective, a tactic proof is essentially a program that writes a proof term, thus tactic writing is metaprogramming.
simp is a very high-level command, like a call to a complex library, while rw and rfl are more like fundamental operations.

This first example was heavy on simp. Next, let's tackle a proof that requires more manual, step-by-step tactics like intro, apply, and let, which have even clearer one-to-one correspondences with proof-term constructs like fun, function application, and let ... in ....

A Fist Concrete Proof#

Dissecting the Proof#

Deconstructing simp#

Step 1: Unfolding the Definition of μK#

Why this works#

Step 2: Unfolding Definition of Uniform PMF#

Why this works#

Step 3: Computing the Cardinality and Final Simplification#

Why this works#

Why Can We Still Prove = 1/8?#

Proofs vs Computation#

What's Happening?#

The Philosophical Point#

Summary#

Proof Term Perspective#

Deconstructing `simp`#

Step 1: Unfolding the Definition of `μK`#

Why Can We Still Prove `= 1/8`?#