Lean - Propositions & Proofs (the Proving Core)

Meetup 3 — Propositions & Proofs (the Proving Core)
This is the conceptual core of the series: writing proofs in Lean. We'll work with the logical connectives — and, or, not, implication — together with the quantifiers and equality, and learn to construct proofs directly, by hand. Building proofs this way first gives a clear
sense of what a proof actually is before we automate the process with tactics in the next session. This is the most demanding material in the series, so the evening is paced deliberately, with plenty of room for questions and discussion. A little familiarity with the previous
session's introduction to propositions-as-types will help.
Reading (before the meetup)
- TPiL Ch 3–4: Propositions and Proofs → Quantifiers and Equality
In session
- Implication, And/Or/Not, ∀/∃, equality, Iff.
- Building proof terms by hand (tactics come next meetup).
Exercises — TPiL Ch 3 · Propositions and Proofs (§3.7)
- Exercise 1 (all parts), Exercise 3
Exercises — TPiL Ch 4 · Quantifiers and Equality (§4.6)
- Exercise 1, Exercise 3