Lean for All

Day 14: Week 2 review: a proof is a story🔗

Read a whole short proof as an argument in plain English, and pick each next step.

Here is this week in one table, matching the shape of the goal or hypothesis to the tactic:

  • goal P → Q or ∀ x, …: intro

  • goal P ∧ Q or P ↔ Q: constructor (two goals)

  • goal P ∨ Q: left or right

  • goal ∃ x, …: refine ⟨witness, ?_⟩, exists, exact ⟨witness, proof⟩

  • goal exactly a hypothesis: exact h or assumption

  • have h : P ∧ Q: h.1, h.2, obtain ⟨hp, hq⟩ := h

  • have h : P ∨ Q: rcases h with hp | hq (two cases)

  • have h : ∃ x, …: obtain ⟨x, hx⟩ := h

  • have h : a = b: rw [h], rw [← h]

  • use a theorem: exact thm h, apply thm, have

  • arithmetic or computation: omega, decide, simp, rfl

Read a proof as a story, one sentence per step. Hover over each tactic to check it against the goal display.

theorem either_way (P Q R : Prop) (hpr : P → R) (hqr : Q → R) : P ∨ Q → R := P:PropQ:PropR:Prophpr:P → Rhqr:Q → R⊢ P ∨ Q → R P:PropQ:PropR:Prophpr:P → Rhqr:Q → Rh:P ∨ Q⊢ R P:PropQ:PropR:Prophpr:P → Rhqr:Q → Rhp:P⊢ RP:PropQ:PropR:Prophpr:P → Rhqr:Q → Rhq:Q⊢ R P:PropQ:PropR:Prophpr:P → Rhqr:Q → Rhp:P⊢ R All goals completed! 🐙 P:PropQ:PropR:Prophpr:P → Rhqr:Q → Rhq:Q⊢ R All goals completed! 🐙

Assume P or Q (intro h). There are two cases. If P holds, then R follows by hpr. If Q holds, then R follows by hqr. Either way, R.

That is an ordinary proof by cases, written in Lean.

One last habit for auditors. After following a proof, ask: which hypotheses did it really need, and can they all hold together?

theorem odd_and_even (n : Nat) (h1 : n % 2 = 0) (h2 : n % 2 = 1) : n = 12345 := n:Nath1:n % 2 = 0h2:n % 2 = 1⊢ n = 12345 All goals completed! 🐙

The “story” is one word, because there is nothing to argue: no number is both even and odd. The proof is correct, and the theorem is empty.

Check yourself🔗