Lean for All

Day 11: Or and there-exists🔗

Follow left/right, rcases on an “or”, and witnesses for ∃.

To prove P ∨ Q, it is enough to prove one side. left commits to P, right commits to Q:

theorem pick_side : 2 = 3 ∨ 2 = 2 := ⊢ 2 = 3 ∨ 2 = 2 ⊢ 2 = 2 All goals completed! 🐙

After right the goal is ⊢ 2 = 2, and rfl closes it. Choosing left would leave ⊢ 2 = 3, which nothing can prove. The step is allowed, but the proof gets stuck.

Using h : P ∨ Q is different. You know one side holds, not which. So the proof splits into two cases, and both must be finished:

theorem small (n : Nat) (h : n = 1 ∨ n = 2) : n < 3 := n:Nath:n = 1 ∨ n = 2⊢ n < 3 n:Nath1:n = 1⊢ n < 3n:Nath2:n = 2⊢ n < 3 n:Nath1:n = 1⊢ n < 3 All goals completed! 🐙 n:Nath2:n = 2⊢ n < 3 All goals completed! 🐙

After rcases h with h1 | h2:

case inl
n : Nat
h1 : n = 1
⊢ n < 3
case inr
n : Nat
h2 : n = 2
⊢ n < 3

Each case has only one of the two facts.

To prove ∃ n, …, name a witness and show it works. refine ⟨4, ?_⟩ says “take n = 4” and leaves the check as the goal:

theorem four : ∃ n : Nat, n + 3 = 7 := ⊢ ∃ n, n + 3 = 7 ⊢ 4 + 3 = 7 All goals completed! 🐙

The goal goes from ⊢ ∃ n, n + 3 = 7 to ⊢ 4 + 3 = 7. Two shorter ways do the same in one line: exists 4 (which also tries to close the check itself) and exact ⟨4, by decide⟩.

Using h : ∃ n, … gives you some number with the property, but you do not choose which:

theorem above (h : ∃ n : Nat, n > 5) : ∃ m : Nat, m > 4 := h:∃ n, n > 5⊢ ∃ m, m > 4 x:Nathx:x > 5⊢ ∃ m, m > 4 exact ⟨x, x:Nathx:x > 5⊢ x > 4 All goals completed! 🐙⟩

After obtain:

x : Nat
hx : x > 5
⊢ ∃ m, m > 4

All you know about x is hx. It might be 6 or a million.

For an auditor: an “or” hypothesis means every case must be handled, and an ∃ hypothesis gives you an unknown value, not a convenient one.

Check yourself🔗