Module 2
Propositions and proofs
- Understand that propositions are types and proofs are terms.
- Use the basic tactics: intro, exact, apply, constructor, cases, rfl, rw, simp.
- Propositional logic: →, ∧, ∨, ¬, ↔.
The playground runs the latest Lean in your browser. Locally, the file is Exercises/Logic.lean and you check it with lake exe check Logic.
Guide
Read: Theorem Proving in Lean 4, chapters 3 ("Propositions and Proofs") and 5 ("Tactics").
Central idea: in Lean, a proposition is a type and a proof is a value of
that type. Proving p → q means writing a function that turns proofs of p
into proofs of q.
Tactics in this module:
| If the goal or hypothesis is... | Use |
|---|---|
Goal p → q |
intro hp |
| You already have exactly what is asked | exact h |
Goal q and you have h : p → q |
apply h |
Goal p ∧ q or p ↔ q |
constructor |
Hypothesis h : p ∧ q |
obtain ⟨hp, hq⟩ := h |
Goal p ∨ q |
left or right |
Hypothesis h : p ∨ q |
cases h with … |
Goal ¬p |
intro hp (because ¬p is p → False) |
Hypothesis h : a = b |
rw [h] |
| An equality that holds by computation | rfl |
| Simplify automatically | simp |
Exercises: ex1 to ex5.
Extra practice: the Natural Number Game is the best way to get comfortable with tactics. Try to complete the Tutorial and Addition worlds.
Exercises
Solve them in the file, not here: the playground or VS Code shows the goal at each step. Tick an exercise once lake exe check marks it ✅ (or it compiles without sorry in the playground).
1ex1
theorem ex1 (p q r : Prop) : (p → q) → (q → r) → (p → r) := by
sorry2ex2
theorem ex2 (p q : Prop) : p ∧ q → p ∨ q := by
sorry3ex3
theorem ex3 (p q : Prop) : p ∨ q ↔ q ∨ p := by
sorry4ex4
theorem ex4 (p q : Prop) : (p → q) → ¬q → ¬p := by
sorry5ex5
theorem ex5 (a b : Nat) (h : a = b) : a + 0 = b := by
sorry