Lean 4 Theorem Proving

What is a Proof?

A proposition is a type. A proof is a value of that type.

-- "1 + 1 = 2" is a type
-- A proof is a value that satisfies it
theorem two : 1 + 1 = 2 := by decide

If the proposition is true, you can build a proof. If false, you can't -- the file won't compile:

theorem ok : 1 + 1 = 2 := by decide        -- compiles
-- theorem bad : 1 + 1 = 3 := by decide    -- build error

The Infoview

Open it: Ctrl+Shift+P → "Lean 4: Infoview: Toggle"

It shows the proof state -- what you have and what you still need to prove. Place your cursor after each line to watch it change.

n : Nat          ← hypotheses (what you have)
h : n > 5        ← hypotheses
⊢ n > 3          ← goal (what you need to prove)

Everything above ⊢ is what you know. Below ⊢ is what you must prove. Tactics transform this state until the goal is gone.

Levels of Proof

There are two kinds of proofs in the ENC spec. Understanding this split is the key to not getting confused.

Level 1: Computation -- "just check it"

The schema is concrete. All values are known. Lean can compute the answer:

def mySchema : Schema := { entries := [ ... ] }   -- concrete data

-- Lean evaluates permits at compile time and checks the result
theorem anyone_reads :
    mySchema.permits "Any" "Post" .R = true := by native_decide

native_decide = "evaluate the function, check the result." About 50 of the 142 theorems in the spec are pure native_decide.

Level 2: Reasoning -- "prove it step by step"

The inputs are abstract. You can't compute -- you must reason:

-- a and b are unknown. Can't evaluate sha256 (it's an axiom).
-- Must build a logical chain.
theorem H_injective :
    ∀ (a b : List CborField), H a = H b → a = b := by
  intro a b hab
  unfold H at hab
  have hcbor := sha256_injective _ _ hab
  exact cborEncode_injective _ _ hcbor

Most of what follows teaches Level 2. Level 1 you already understand -- it's just native_decide. Level 3 (typeclass obligations) uses a mix of both -- see Section 20.

Tactics That Solve Things Automatically

These tactics try to close the goal entirely. Use them first. Only go manual if they fail.

native_decide / decide

Evaluate a concrete computation:

theorem ex1 : 3 < 10 := by decide
theorem ex2 : "hello".length = 5 := by native_decide
theorem ex3 : mySchema.permits "Any" "Post" .R = true := by native_decide

Only works when all values are known and types have DecidableEq.

simp

Apply simplification rules:

theorem ex1 (n : Nat) : n + 0 = n := by simp
theorem ex2 (n : Nat) : 0 + n = n := by simp
theorem ex3 : [1, 2, 3].length = 3 := by simp

simp_all is more aggressive -- also simplifies hypotheses.

omega

Solve arithmetic (Nat and Int):

theorem ex1 (n : Nat) : n + 1 > n := by omega
theorem ex2 (a b : Nat) : a + b = b + a := by omega
theorem ex3 (n : Nat) (h : n > 5) : n > 3 := by omega

Notice: omega sees (h : n > 5) in the hypotheses automatically. No need to name it with intro first -- omega scans all available info.

rfl

Both sides are definitionally the same:

theorem ex : 42 = 42 := by rfl

When automatic tactics fail

If native_decide, simp, omega, and rfl all fail, you need manual tactics. That's the rest of this guide.

intro -- Open the Box

When the goal starts with ∀ (for all) or → (implies), intro names those things so you can use them:

theorem ex : ∀ (a b : ByteArray), sha256 a = sha256 b → a = b := by
  intro a b hab

Before intro:

⊢ ∀ (a b : ByteArray), sha256 a = sha256 b → a = b

After intro:

a : ByteArray
b : ByteArray
hab : sha256 a = sha256 b
⊢ a = b

intro unpacked the ∀ and → into named hypotheses. Now you can use a, b, and hab in subsequent steps.

When to use intro: only when you need to reference hypotheses by name in later steps. If omega or simp solves the whole thing, skip intro:

-- omega handles intro internally, so just:
theorem ex (n : Nat) (h : n > 5) : n > 3 := by omega

-- But here you need hab by name for manual steps:
theorem ex : ∀ (a b : List CborField), H a = H b → a = b := by
  intro a b hab          -- need hab for the next steps
  unfold H at hab        -- use hab here
  ...

unfold -- Expand a Definition

Replace a function name with its body:

def double (n : Nat) := n + n

theorem ex : double 5 = 10 := by
  unfold double
  -- goal changes from: double 5 = 10
  -- to: 5 + 5 = 10
  decide

unfold f at h expands inside a hypothesis:

theorem ex (hab : H a = H b) : ... := by
  unfold H at hab
  -- hab changes from: H a = H b
  -- to: sha256 (cborEncode a) = sha256 (cborEncode b)

have -- Add an Intermediate Fact

"From what I know, I can also conclude this":

theorem ex : ∀ (a b : List CborField), H a = H b → a = b := by
  intro a b hab
  unfold H at hab
  -- hab : sha256 (cborEncode a) = sha256 (cborEncode b)
  have hcbor := sha256_injective _ _ hab
  -- NEW: hcbor : cborEncode a = cborEncode b
  exact cborEncode_injective _ _ hcbor

have hcbor := sha256_injective _ _ hab applies the axiom sha256_injective to hab and names the result hcbor.

The _ means "infer this argument." Lean figures out what a and b are from context.

have can also use tactics:

have proof : b ≠ 0 := by omega    -- prove b ≠ 0 using omega

exact -- Done

"This is the proof. Goal closed."

theorem ex (h : 1 = 1) : 1 = 1 := by
  exact h

exact takes a proof term and checks if it matches the goal exactly. If yes, done.

rw -- Rewrite

Replace one thing with another using an equation:

theorem ex (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]
  -- h says a = b
  -- replaces a with b in the goal
  -- goal becomes: b + 1 = b + 1
  -- Lean closes this automatically

rw [← h] rewrites backwards (replaces b with a).

rw [h] at h2 rewrites inside a hypothesis instead of the goal.

cases -- Split by Constructor

For inductive types, check every possible case:

theorem bool_em (b : Bool) : b = true ∨ b = false := by
  cases b
  · right; rfl     -- case b = false: choose right side
  · left; rfl      -- case b = true: choose left side

· focuses on one sub-goal. cases creates one sub-goal per constructor.

For exhaustive checking of all combinations:

theorem prefix_inj : ∀ (p q : Prefix), p.toByte = q.toByte → p = q := by
  intro p q h
  cases p <;> cases q <;> simp_all [Prefix.toByte]

<;> applies the next tactic to ALL sub-goals. cases p <;> cases q creates 7x7=49 combinations, then simp_all solves each.

constructor -- Split And

A ∧ B means "prove both A and B." constructor splits it:

theorem ex : 1 < 2 ∧ 3 < 4 := by
  constructor          -- two goals: (1) 1 < 2 and (2) 3 < 4
  · decide             -- solve goal 1
  · decide             -- solve goal 2

Shorthand -- apply tactic to all goals:

theorem ex : 1 < 2 ∧ 3 < 4 := by
  constructor <;> decide

For 3+ parts, use refine:

theorem ex : 1 = 1 ∧ 2 = 2 ∧ 3 = 3 := by
  refine ⟨?_, ?_, ?_⟩ <;> rfl

⟨?_, ?_, ?_⟩ creates one hole per conjunct. <;> rfl fills them all. This is the most common pattern in the ENC spec:

theorem five_things : P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> native_decide

left / right -- Choose Or

A ∨ B means "prove either A or B." Pick a side:

theorem ex : 1 = 1 ∨ 1 = 2 := by
  left       -- "I'll prove the left side"
  rfl

use -- Prove Exists

∃ n, P n means "there exists an n where P holds." Provide the witness:

theorem ex : ∃ n : Nat, n > 5 := by
  use 6        -- "6 is such a value"
  decide       -- prove 6 > 5

Axioms

Declare a fact without proof:

axiom sha256 (input : ByteArray) : Hash
axiom sha256_injective : ∀ (a b : ByteArray), sha256 a = sha256 b → a = b

Use for things you can't prove (crypto assumptions). Everything built on axioms must be noncomputable.

Safety rule: only axiomatize what is known to be true. State less, not more.

#print axioms myTheorem shows which axioms a theorem depends on.

The Full Chain -- H_injective

The most important proof in the spec. Read with Infoview open:

axiom sha256_injective :
  ∀ (a b : ByteArray), sha256 a = sha256 b → a = b

axiom cborEncode_injective :
  ∀ (a b : List CborField), cborEncode a = cborEncode b → a = b

noncomputable def H (fields : List CborField) : Hash :=
  sha256 (cborEncode fields)

The proof:

theorem H_injective :
    ∀ (a b : List CborField), H a = H b → a = b := by

Line 1: intro a b hab

⊢ ∀ (a b), H a = H b → a = b

a : List CborField
b : List CborField
hab : H a = H b
⊢ a = b

Unpacked ∀ and →. Named everything.

Line 2: unfold H at hab

hab : H a = H b
⊢ a = b

hab : sha256 (cborEncode a) = sha256 (cborEncode b)
⊢ a = b

Replaced H with its definition. Now we can see the sha256 and cborEncode.

Line 3: have hcbor := sha256_injective _ _ hab

hab : sha256(cbor a)
    = sha256(cbor b)
⊢ a = b

hab : sha256(cbor a) = sha256(cbor b)
hcbor : cborEncode a = cborEncode b
⊢ a = b

Applied the sha256 axiom: "if sha256 outputs are equal, inputs are equal." Created new fact hcbor.

Line 4: exact cborEncode_injective _ _ hcbor

hcbor : cborEncode a
      = cborEncode b
⊢ a = b

(no goals -- proof complete)

Applied the cbor axiom: "if cbor outputs are equal, inputs are equal." Goal a = b matches exactly. Done.

The whole chain

Proof as Transformation

Every proof is a path from hypotheses to goal. Tactics are the steps:

Like group theory. You compose transformations until you reach the target. If no path exists, the proposition might be false -- or you're missing an axiom.

The compiler doesn't guess the path. You build it explicitly, one tactic at a time.

Converting Between Propositions

Sometimes you have a proof of A but need a proof of B, where A and B are related but not identical:

-- You have: h : b > 0
-- You need: b ≠ 0
-- They're related but different propositions
have proof : b ≠ 0 := by omega

omega is smart enough to bridge arithmetic propositions. For non-arithmetic, use other tactics:

-- rw bridges with equations
-- have: h : a = b
-- need: f a = f b
rw [h]

-- exact bridges with direct match
-- have: h : A ∧ B
-- need: A
exact h.1        -- .1 extracts the first part of ∧

-- need: B
exact h.2        -- .2 extracts the second part

How to Read Logical Symbols

How to prove each

How to use each (when you have it as hypothesis)

sorry -- Skip For Now

theorem todo : something complicated := by sorry

Compiles with a warning. Zero sorry = everything is proven. The ENC spec has 1 sorry (a placeholder in Composition.lean for an advanced cross-app proof).

Common Patterns in the ENC Spec

The spec has 142 theorems across 54 modules (56 build targets). Here are the patterns.

Pattern 1: Single property (~50 theorems)

theorem anyone_reads :
    schema.permits "Any" "Post" .R = true := by native_decide

Pattern 2: Two properties

theorem owner_access :
    schema.permits "Owner" "Post" .C = true ∧
    schema.permits "Owner" "Post" .R = true := by
  constructor <;> native_decide

Pattern 3: Many properties

theorem full_check :
    P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> native_decide

Pattern 4: Injectivity chain (axiom-based)

theorem f_injective : ∀ a b, f a = f b → a = b := by
  intro a b h
  unfold f at h
  have h2 := inner_injective _ _ h
  exact base_injective _ _ h2

Pattern 5: Exhaustive cases

theorem all_cases : ∀ p q, p.toByte = q.toByte → p = q := by
  intro p q h
  cases p <;> cases q <;> simp_all [toByte]

Pattern 6: Typeclass obligation -- existential witness

Used in typeclass instances to prove "every event type is creatable by some role":

all_creatable := by
  intro et het
  simp [List.Mem] at het           -- normalize list membership
  rcases het with rfl | rfl | rfl  -- split into one case per event type
  · exact ⟨"Owner", by native_decide⟩   -- witness: Owner can create this
  · exact ⟨"Owner", by native_decide⟩
  · exact ⟨"Any", by native_decide⟩

rcases destructures the membership proof into one case per list element. For each case, ⟨role, proof⟩ provides the witness (which role) and proves the schema permits it.

Pattern 7: Typeclass obligation -- unfold + rfl

Used when a typeclass field says "this function equals that function":

reduces_to_createCommit := by intro w; cases w <;> rfl

cases w splits the write inductive into constructors, then rfl confirms each case is definitionally equal to createCommit.

Pattern 8: Typeclass obligation -- arithmetic bound

Used for proving component counts, list lengths, etc.:

components_nonempty := by omega    -- proves componentCount > 0

Pattern 9: Meta-theorem -- derive from typeclass

The composition meta-theorem extracts proofs from typeclass obligations:

theorem composition_from_typeclass (A W K Idx Q S : Type)
    [inst : ENCApp A W K Idx Q S] :
    (∀ w id enc exp, inst.buildCommit w id enc exp = ...) ∧  -- C1
    (∀ k m, inst.decrypt k (inst.encrypt k m) = some m) ∧    -- C3
    (∀ et, et ∈ inst.eventTypes → ∃ role, ...) ∧             -- C4
    (inst.componentCount > 0) :=                               -- C6
  ⟨inst.reduces_to_createCommit, inst.roundtrip,
   inst.all_creatable, inst.components_nonempty⟩

Tactic Cheat Sheet

Try these first (automatic)

Use these for manual proofs