Module 3 · Lesson 2

have & let — Intermediate Results

have and let introduce intermediate results into your proof. They help break complex proofs into manageable steps.

have: Proving an Intermediate Fact

have h : T := ... proves something of typeT and names it h:

lean

1example (n : Nat) (h : n > 0) : n * 2 > 0 := by
2  have pos : n > 0 := h
3  -- pos : n > 0 is now in context
4  omega
5
6-- More useful: proving something new
7example (a b : Nat) (ha : a > 5) (hb : b > 3) : a + b > 8 := by
8  have hab : a + b > 5 + 3 := by omega
9  omega

have with Tactics

Use have h : T := by ... to prove the intermediate result with tactics:

lean

1example (P Q R : Prop) (hp : P) (hpq : P → Q) (hqr : Q → R) : R := by
2  have hq : Q := by
3    apply hpq
4    exact hp
5  have hr : R := by
6    apply hqr
7    exact hq
8  exact hr
9
10-- Or more concisely:
11example (P Q R : Prop) (hp : P) (hpq : P → Q) (hqr : Q → R) : R := by
12  have hq : Q := hpq hp
13  exact hqr hq

Key Takeaway

have creates a named intermediate result. It's for proofs—the value is opaque and only its type matters.

let: Introducing a Definition

let introduces a local definition where the value is visible (not opaque):

lean

1example : 10 = 5 + 5 := by
2  let x := 5
3  -- x : Nat := 5  (value is visible)
4  rfl
5
6example (n : Nat) : n + n = 2 * n := by
7  let m := n + n
8  -- m : Nat := n + n
9  show m = 2 * n
10  ring

have vs let

lean

1-- have: value is opaque (for proofs)
2example (h : 2 + 2 = 4) : True := by
3  have proof : 2 + 2 = 4 := h
4  -- proof is just "something of type 2 + 2 = 4"
5  trivial
6
7-- let: value is transparent (for computation)
8example : (5 + 5) * 2 = 20 := by
9  let ten := 5 + 5
10  -- ten is definitionally equal to 10
11  rfl  -- works because ten unfolds to 10

ℹ

Use have for proofs and intermediate propositions. Use let for computational values you want to reuse.

have this

have : T := ... without a name creates a hypothesis called this:

lean

1example (n : Nat) (h : n > 5) : n > 0 := by
2  have : n > 5 := h
3  -- this : n > 5
4  omega
5
6-- Useful for quick intermediate steps
7example (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by
8  have : (a + b) * (a + b) = (a + b)^2 := by ring
9  ring

Type Inference

Lean can often infer the type:

lean

1example (P Q : Prop) (hp : P) (hpq : P → Q) : Q := by
2  have hq := hpq hp  -- Type inferred as Q
3  exact hq
4
5example : ∃ n : Nat, n > 10 := by
6  let x := 42
7  have h := show x > 10 by omega
8  exact ⟨x, h⟩

Structuring Complex Proofs

lean

1theorem sqrt_two_irrational (p q : Nat) (hq : q ≠ 0) 
2    (h : p * p = 2 * q * q) : False := by
3  -- Step 1: Show p must be even
4  have hp_even : 2 ∣ p := by
5    sorry
6  -- Step 2: Let p = 2k
7  have ⟨k, hk⟩ := hp_even
8  -- Step 3: Show q must be even
9  have hq_even : 2 ∣ q := by
10    sorry
11  -- Step 4: Contradiction (infinite descent)
12  sorry

Deep Dive: have with Pattern Matching

You can destructure as you introduce:

lean

1example (h : ∃ n : Nat, n > 5 ∧ n < 10) : True := by
2  have ⟨n, hn_gt, hn_lt⟩ := h
3  -- n : Nat
4  -- hn_gt : n > 5
5  -- hn_lt : n < 10
6  trivial
7
8example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
9  have ⟨hp, hq⟩ := h
10  exact ⟨hq, hp⟩

suffices: Backward have

suffices is like havebut works backward:

lean

1example (n : Nat) : n + n ≥ n := by
2  suffices h : n ≤ n + n by omega
3  -- Now we prove: n ≤ n + n
4  omega
5
6-- Equivalent to:
7example (n : Nat) : n + n ≥ n := by
8  have h : n ≤ n + n := by omega
9  omega

ℹ

suffices h : S by tac means "it suffices to prove S; here's how S implies the goal (by tac), and now I'll prove S."

Examples

Building Up a Proof

lean

1example (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
2  have hab : a ≤ b := h1
3  have hbc : b ≤ c := h2
4  exact Nat.le_trans hab hbc

Naming Complex Expressions

lean

1example (f : Nat → Nat) (h : ∀ n, f n = n + 1) : f (f 0) = 2 := by
2  let x := f 0
3  have hx : x = 1 := by simp [h]
4  have hfx : f x = 2 := by simp [h, hx]
5  simp [hfx]

Proof with Intermediate Lemma

lean

1example : ∀ n : Nat, n = 0 ∨ n > 0 := by
2  intro n
3  have h := Nat.eq_zero_or_pos n
4  -- h : n = 0 ∨ 0 < n
5  exact h

intro Next: obtain