lean-pl-tutorials/tutorial-01-basics/04-quantifiers-and-equality.org

• Unit 4 — Quantifiers and Equality
  • Goals
  • Source
  • Concepts
  • Exercises
    • Exercise 4.1 — Universal quantifier
    • Exercise 4.2 — Existential quantifier
    • Exercise 4.3 — Equality and rewriting

Unit 4 — Quantifiers and Equality

Tutorial 1: Lean 4 Fundamentals · ← Back to README

Goals

• Use ∀ (forall) and ∃ (exists) quantifiers
• Manipulate equality with rfl, rw, calc
• Combine quantifiers with logical connectives

Source

Theorem Proving in Lean 4 (TPIL), Chapter 4 → https://leanprover.github.io/theorem_proving_in_lean4/

Concepts

Concept	Lean
Universal ∀ x, P x	intro x to prove; h x or apply h to use
Existential ∃ x, P x	⟨x, h⟩ to prove; rcases h with ⟨x, hx⟩ to use
Equality a = b	rfl when definitional; rw [h] when propositional
calc block	Chain equalities: calc a = b : h1; _ = c := h2=

Exercises

Exercise 4.1 — Universal quantifier

-- (a) Prove a simple forall
theorem all_imp (P Q : Nat → Prop) (h : ∀ n, P n → Q n) (x : Nat) (hp : P x) : Q x :=
  by
    sorry

-- (b) Distributing ∀ over ∧
theorem forall_and_distrib (P Q : Nat → Prop) : (∀ n, P n ∧ Q n) ↔ (∀ n, P n) ∧ (∀ n, Q n) :=
  by
    constructor
    · sorry  -- left-to-right
    · sorry  -- right-to-left

-- (c) Prove that if every natural is even, then 42 is even
-- (Use: `Even n := ∃ k, n = 2*k`)
def Even (n : Nat) : Prop := ∃ k, n = 2 * k

theorem all_even_implies_42 : (∀ n, Even n) → Even 42 :=
  by
    sorry

Exercise 4.2 — Existential quantifier

-- (a) Prove existence
theorem exists_square (a : Nat) : ∃ n, n = a * a :=
  by
    sorry

-- (b) Distributing ∃ over ∨
theorem exists_or_distrib (P Q : Nat → Prop) : (∃ n, P n ∨ Q n) ↔ (∃ n, P n) ∨ (∃ n, Q n) :=
  by
    constructor
    · sorry
    · sorry

-- (c) Prove: if something is both even and greater than 10, then something is greater than 5
theorem even_and_gt10_implies_gt5 : (∃ n, Even n ∧ n > 10) → (∃ n, n > 5) :=
  by
    sorry

Exercise 4.3 — Equality and rewriting

-- (a) Prove symmetry and transitivity of equality (without using `symm`/`trans`)
theorem eq_symm {α : Type} (a b : α) (h : a = b) : b = a :=
  by
    sorry

theorem eq_trans {α : Type} (a b c : α) (h1 : a = b) (h2 : b = c) : a = c :=
  by
    sorry

-- (b) Use `calc` to prove a chain of identities
theorem calc_example (a b c d : Nat) (h1 : a = b) (h2 : b = c + 1) (h3 : c + 1 = d) : a = d :=
  by
    sorry

-- (c) Rewrite inside a goal
theorem rewrite_example (a b : Nat) (h : a = b + 1) : a * 2 = (b + 1) * 2 :=
  by
    sorry

---

← Previous: Unit 3 · Next: Unit 5 — Advanced Tactics